feat: make generalize_proofs handle proofs under binders (#12472)

The `generalize_proofs` tactic had a bug where it would not generalize proofs that appeared under binders correctly, creating terms with fvars from the wrong context. The tactic has been refactored, and it now abstracts the proofs (universally quantifying all the bound variables that appear in the proof) before lifting them to the local context.

This feature can be controlled with the `abstract` option. Using `generalize_proofs (config := { abstract := false })` turns off proof abstraction and leaves alone those proofs that refer to bound variables.

Other new features:
- `generalize_proofs at h` for a let-bound local hypothesis `h` will clear its value.
- `generalize_proofs at h` for a duplicate proposition will eliminate `h` from the local context.
- Proofs are recursively generalized for each new local hypothesis. This can be turned off with `generalize_proofs (config := { maxDepth := 0 })`.
- `generalize_proofs at h` will no longer generalize proofs from the goal.
- The type of the generalized proof is carefully computed by propagating expected types, rather than by using `inferType`. This gives local hypotheses in more useful forms.

(This PR serves as a followup to [this comment](#447 (comment)).)

Author: kmill

Mathlib/Algebra/Category/GroupCat/Limits.lean

@@ -520,18 +520,14 @@ def kernelIsoKer {G H : AddCommGroupCat.{u}} (f : G ⟶ H) :
     refine equalizer.hom_ext ?_
     ext x
     dsimp
-    generalize_proofs _ h1 h2
-    erw [DFunLike.congr_fun (kernel.lift_ι f _ h1) ⟨_, h2⟩]
-    rfl
+    apply DFunLike.congr_fun (kernel.lift_ι f _ _)
   inv_hom_id := by
     apply AddCommGroupCat.ext
     simp only [AddMonoidHom.coe_mk, coe_id, coe_comp]
     rintro ⟨x, mem⟩
     refine Subtype.ext ?_
     simp only [ZeroHom.coe_mk, Function.comp_apply, id_eq]
-    generalize_proofs _ h1 h2
-    erw [DFunLike.congr_fun (kernel.lift_ι f _ h1) ⟨_, mem⟩]
-    rfl
+    apply DFunLike.congr_fun (kernel.lift_ι f _ _)
 set_option linter.uppercaseLean3 false in
 #align AddCommGroup.kernel_iso_ker AddCommGroupCat.kernelIsoKer
 

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

@@ -57,11 +57,11 @@ theorem RespectsIso.basicOpen_iff (hP : RespectsIso @P) {X Y : Scheme} [IsAffine
   congr
   delta IsLocalization.Away.map
   refine' IsLocalization.ringHom_ext (Submonoid.powers r) _
-  generalize_proofs h1 h2 h3
+  generalize_proofs
   haveI i1 := @isLocalization_away_of_isAffine X _ (Scheme.Γ.map f.op r)
   -- Porting note: needs to be very explicit here
   convert
-    (@IsLocalization.map_comp (hy := h3) (Y.presheaf.obj <| Opposite.op (Scheme.basicOpen Y r))
+    (@IsLocalization.map_comp (hy := ‹_ ≤ _›) (Y.presheaf.obj <| Opposite.op (Scheme.basicOpen Y r))
     _ _ (isLocalization_away_of_isAffine _) _ _ _ i1).symm using 1
   change Y.presheaf.map _ ≫ _ = _ ≫ X.presheaf.map _
   rw [f.val.c.naturality_assoc]

Mathlib/Combinatorics/SimpleGraph/Partition.lean

@@ -147,7 +147,8 @@ theorem partitionable_iff_colorable {n : ℕ} : G.Partitionable n ↔ G.Colorabl
   · rintro ⟨C⟩
     refine' ⟨C.toPartition, C.colorClasses_finite, le_trans _ (Fintype.card_fin n).le⟩
     generalize_proofs h
-    haveI : Fintype C.colorClasses := C.colorClasses_finite.fintype
+    change Set.Finite (Coloring.colorClasses C) at h
+    have : Fintype C.colorClasses := C.colorClasses_finite.fintype
     rw [h.card_toFinset]
     exact C.card_colorClasses_le
 #align simple_graph.partitionable_iff_colorable SimpleGraph.partitionable_iff_colorable

Mathlib/Data/PFun.lean

@@ -328,11 +328,9 @@ theorem fix_fwd {f : α →. Sum β α} {b : β} {a a' : α} (hb : b ∈ f.fix a
 def fixInduction {C : α → Sort*} {f : α →. Sum β α} {b : β} {a : α} (h : b ∈ f.fix a)
     (H : ∀ a', b ∈ f.fix a' → (∀ a'', Sum.inr a'' ∈ f a' → C a'') → C a') : C a := by
   have h₂ := (Part.mem_assert_iff.1 h).snd
-  -- Porting note: revert/intro trick required to address `generalize_proofs` bug
-  revert h₂
-  generalize_proofs h₁
-  intro h₂; clear h
-  induction' h₁ with a ha IH
+  generalize_proofs at h₂
+  clear h
+  induction' ‹Acc _ _› with a ha IH
   have h : b ∈ f.fix a := Part.mem_assert_iff.2 ⟨⟨a, ha⟩, h₂⟩
   exact H a h fun a' fa' => IH a' fa' (Part.mem_assert_iff.1 (fix_fwd h fa')).snd
 #align pfun.fix_induction PFun.fixInduction
@@ -341,9 +339,8 @@ theorem fixInduction_spec {C : α → Sort*} {f : α →. Sum β α} {b : β} {a
     (H : ∀ a', b ∈ f.fix a' → (∀ a'', Sum.inr a'' ∈ f a' → C a'') → C a') :
     @fixInduction _ _ C _ _ _ h H = H a h fun a' h' => fixInduction (fix_fwd h h') H := by
   unfold fixInduction
-  -- Porting note: `generalize` required to address `generalize_proofs` bug
-  generalize @fixInduction.proof_1 α β f b a h = ha
-  induction ha
+  generalize_proofs
+  induction ‹Acc _ _›
   rfl
 #align pfun.fix_induction_spec PFun.fixInduction_spec
 

Mathlib/NumberTheory/Cyclotomic/Gal.lean

@@ -56,16 +56,10 @@ theorem autToPow_injective : Function.Injective <| hμ.autToPow K := by
   intro f g hfg
   apply_fun Units.val at hfg
   simp only [IsPrimitiveRoot.coe_autToPow_apply] at hfg
-  -- Porting note: was `generalize_proofs hf' hg' at hfg`
-  revert hfg
-  generalize_proofs hf' hg'
-  intro hfg
+  generalize_proofs hf' hg' at hfg
   have hf := hf'.choose_spec
   have hg := hg'.choose_spec
-  -- Porting note: was `generalize_proofs hζ at hf hg`
-  revert hf hg
-  generalize_proofs hζ
-  intro hf hg
+  generalize_proofs hζ at hf hg
   suffices f (hμ.toRootsOfUnity : Lˣ) = g (hμ.toRootsOfUnity : Lˣ) by
     apply AlgEquiv.coe_algHom_injective
     apply (hμ.powerBasis K).algHom_ext
@@ -154,13 +148,11 @@ noncomputable def fromZetaAut : L ≃ₐ[K] L :=
 
 theorem fromZetaAut_spec : fromZetaAut hμ h (zeta n K L) = μ := by
   simp_rw [fromZetaAut, autEquivPow_symm_apply]
--- Porting note: `generalize_proofs` did not generalize the same proofs, making the proof different.
-  generalize_proofs h1 h2
-  nth_rewrite 4 [← (zeta_spec n K L).powerBasis_gen K]
-  have := Exists.choose_spec ((zeta_spec n K L).eq_pow_of_pow_eq_one hμ.pow_eq_one n.pos)
-  rw [PowerBasis.equivOfMinpoly_gen, h1.powerBasis_gen K, ZMod.coe_unitOfCoprime,
-    ZMod.val_cast_of_lt this.1]
-  exact this.2
+  generalize_proofs hζ h _ hμ _
+  nth_rewrite 4 [← hζ.powerBasis_gen K]
+  rw [PowerBasis.equivOfMinpoly_gen, hμ.powerBasis_gen K]
+  convert h.choose_spec.2
+  exact ZMod.val_cast_of_lt h.choose_spec.1
 #align is_cyclotomic_extension.from_zeta_aut_spec IsCyclotomicExtension.fromZetaAut_spec
 
 end IsCyclotomicExtension