bug fix: symm bug fix and FinEnum.lean change (#1683)

In [FinEnum.lean](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/FinEnum.lean#L166) there was a bug that prevented the `symm` tactic from working properly. After [discussing on zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Potential.20Bug.20in.20symm.20tactic), it's been fixed!
leanprover-community · Jan 25, 2023 · b940160 · b940160
1 parent e8dab8c
commit b940160
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Mathlib/Data/FinEnum.lean b/Mathlib/Data/FinEnum.lean
@@ -163,7 +163,7 @@ theorem Finset.mem_enum [DecidableEq α] (s : Finset α) (xs : List α) :
         simp only [union_sdiff_of_subset this, or_true_iff, Finset.union_sdiff_of_subset,
           eq_self_iff_true]
       · left
-        apply Eq.symm
+        symm
         simp only [sdiff_eq_self]
         intro a
         simp only [and_imp, mem_inter, mem_singleton]

diff --git a/Mathlib/Tactic/Relation/Symm.lean b/Mathlib/Tactic/Relation/Symm.lean
@@ -72,7 +72,7 @@ def symmAux (tgt : Expr) (k : Expr → Array Expr → Expr → MetaM α) : MetaM
 
 /-- Given a term `e : a ~ b`, construct a term in `b ~ a` using `@[symm]` lemmas. -/
 def symm (e : Expr) : MetaM Expr := do
-  symmAux (← inferType e) fun lem args body => do
+  symmAux (← instantiateMVars (← inferType e)) fun lem args body => do
     let .true ← isDefEq args.back e | failure
     mkExpectedTypeHint (mkAppN lem args) (← instantiateMVars body)
 
@@ -99,7 +99,7 @@ def symmAux (tgt : Expr) (k : Expr → Array Expr → Expr → MVarId → MetaM
 
 /-- Apply a symmetry lemma (i.e. marked with `@[symm]`) to a metavariable. -/
 def symm (g : MVarId) : MetaM MVarId := do
-  g.symmAux (← g.getType) fun lem args body g => do
+  g.symmAux (← g.getType') fun lem args body g => do
     let .true ← isDefEq (← g.getType) body | failure
     g.assign (mkAppN lem args)
     return args.back.mvarId!