term vs by exact term

Stream: mathlib4

[Eric Wieser]

I was under the impression when choosing between term and by exact term, the only real difference was a change in elaboration order of the surrounding code; but in this model, by exact term at the top level is the same as term.

Cleary, this model is incorrect:

import Mathlib.Order.Antichain

variable {α : Type*} (s : Set α) (r r' : α → α → Prop)

-- ok
theorem image_relIso (hs : IsAntichain r s) (φ : r ≃r r') : IsAntichain r' (φ '' s) :=
  hs.image_relEmbedding φ

-- ok
theorem image_relIso_by_refine' (hs : IsAntichain r s) (φ : r ≃r r') : IsAntichain r' (φ '' s) :=
  by refine' hs.image_relEmbedding φ

-- fails on the `φ`. Using `refine` instead is the same.
theorem image_relIso_by_exact (hs : IsAntichain r s) (φ : r ≃r r') : IsAntichain r' (φ '' s) :=
  by exact hs.image_relEmbedding φ

which gives the message

application type mismatch
  IsAntichain.image_relEmbedding hs φ
argument
  φ
has type
  r ≃r r' : Type u_1
but is expected to have type
  r ↪r ?m.779 : Type (max u_1 ?u.762)

[Eric Wieser]

In the term-mode proof, the ?m.779 metavariable has already been assigned to r'; but for some reason, in the tactic proof it has not

[Eric Wieser]

(this also relates to the #mathlib4 > refine vs refine' discussion)

[Kyle Miller]

This is something subtle I've seen before about how seriously the expected type is propagated in exact/refine.

-- ok
theorem image_relIso_by_exact_ascript (hs : IsAntichain r s) (φ : r ≃r r') : IsAntichain r' (φ '' s) :=
  by exact (hs.image_relEmbedding φ : IsAntichain r' (φ '' s))

[Eric Wieser]

I was sure I tried that and it failed, but am relieved to see it works after all. Do you think exact should be more serious here?

[Kyle Miller]

This fails by the way:

example (hs : IsAntichain r s) (φ : r ≃r r') : IsAntichain r' (φ '' s) := by
  have := hs.image_relEmbedding φ
  --                            ^
  -- fails: argument φ has type r ≃r r' but is expected to have type r ↪r ?m.1748

[Kyle Miller]

I don't get why there's a difference in behavior when you use a type ascription, to be perfectly honest. It seems to me that ((by exact x) : ty) and by exact (x : ty) should be the same, but they aren't here.