awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.AdicCompletion (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
m n_1 n : ℕ
hmn : m ≤ n
ih : AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f n) = liftAdicCompletionAux I f m
⊢ AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f (n + 1)) = liftAdicCompletionAux I f m
have succ : AlgHom.comp (Ideal.Quotient.factorₐ R sorry)
    (AlgHom.comp (Ideal.Quotient.factorₐ R sorry) (liftAdicCompletionAux I f (n + 1))) =
  liftAdicCompletionAux I f m
Tactic: rw [← Ideal.Quotient.factorₐ_comp _
      (Ideal.pow_le_pow_right n.le_succ) (Ideal.pow_le_pow_right hmn), AlgHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.AdicCompletion (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
m n : ℕ
hn : m ≤ n
⊢ AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f n) = liftAdicCompletionAux I f m
have base : AlgHom.comp (Ideal.Quotient.factorₐ R sorry) (liftAdicCompletionAux I f m) = liftAdicCompletionAux I f m
Tactic: induction n, hn using Nat.le_induction with
  | base => simp
  | succ n hmn ih =>
    rw [← Ideal.Quotient.factorₐ_comp _
      (Ideal.pow_le_pow_right n.le_succ) (Ideal.pow_le_pow_right hmn), AlgHom.comp_assoc]
    simpa
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.AdicCompletion (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
m n : ℕ
hn : m ≤ n
base : AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f m) = liftAdicCompletionAux I f m
⊢ AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f n) = liftAdicCompletionAux I f m
have succ : ∀ (n : ℕ) (hmn : m ≤ n)
  (ih : AlgHom.comp (Ideal.Quotient.factorₐ R sorry) (liftAdicCompletionAux I f n) = liftAdicCompletionAux I f m),
  AlgHom.comp (Ideal.Quotient.factorₐ R sorry) (liftAdicCompletionAux I f (n + 1)) = liftAdicCompletionAux I f m
Tactic: induction n, hn using Nat.le_induction with
  | base => simp
  | succ n hmn ih =>
    rw [← Ideal.Quotient.factorₐ_comp _
      (Ideal.pow_le_pow_right n.le_succ) (Ideal.pow_le_pow_right hmn), AlgHom.comp_assoc]
    simpa
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.AdicCompletion (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
⊢ ∃ (g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion I S)),
    AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)) g = f
have refine : AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I))
    (AdicCompletion.liftAlgHom I (liftAdicCompletionAux I f) sorry) =
  f
Tactic: refine ⟨AdicCompletion.liftAlgHom I (liftAdicCompletionAux I f)
    (factorₐ_comp_liftAdicCompletionAux_of_le I f), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.AdicCompletion (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
⊢ AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I))
      (AdicCompletion.liftAlgHom I (liftAdicCompletionAux I f) ⋯) =
    f
have H : ∀ (x : A),
  Eq.{u_3 + 1} (α := S ⧸ I)
    (((AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I))
              (AdicCompletion.liftAlgHom I (liftAdicCompletionAux I f) sorry) :
            AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)) :
          (a : A) → S ⧸ I)
        x :
      S ⧸ I)
    ((f : (a : A) → S ⧸ I) x : S ⧸ I)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.AdicCompletion (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
I : Ideal S
inst_6 : IsAdicComplete I S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
⊢ ∃ (g : A →ₐ[R] S), AlgHom.comp (Ideal.Quotient.mkₐ R I) g = f
have obtain : ∀ (g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion I S))
  (hg : AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)) g = f),
  ∃ (g : A →ₐ[R] S), AlgHom.comp (Ideal.Quotient.mkₐ R I) g = f
Tactic: obtain ⟨g, hg⟩ := exists_adicCompletionEvalOneₐ_comp_eq f
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.AdicCompletion (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
I : Ideal S
inst_6 : IsAdicComplete I S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion I S)
hg : AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)) g = f
⊢ ∃ (g : A →ₐ[R] S), AlgHom.comp (Ideal.Quotient.mkₐ R I) g = f
have refine : AlgHom.comp (Ideal.Quotient.mkₐ R I)
    (AlgHom.comp (AlgHom.restrictScalars R (↑(AdicCompletion.ofAlgEquiv I).symm : AdicCompletion I S →ₐ[S] S)) g) =
  f
Tactic: refine ⟨AlgHom.comp ((AdicCompletion.ofAlgEquiv I).symm.toAlgHom.restrictScalars R) g, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.AdicCompletion (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
I : Ideal S
inst_6 : IsAdicComplete I S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion I S)
hg : AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)) g = f
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I)
      (AlgHom.comp (AlgHom.restrictScalars R (↑(AdicCompletion.ofAlgEquiv I).symm : AdicCompletion I S →ₐ[S] S)) g) =
    f
have H : ∀ (x : A),
  Eq.{u_3 + 1} (α := S ⧸ I)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R I)
              (AlgHom.comp (AlgHom.restrictScalars R (↑(AdicCompletion.ofAlgEquiv I).symm : AdicCompletion I S →ₐ[S] S))
                g) :
            AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)) :
          (a : A) → S ⧸ I)
        x :
      S ⧸ I)
    ((f : (a : A) → S ⧸ I) x : S ⧸ I)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.AdicCompletion (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
f : S →ₐ[R] A
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := S) (β := A) (⇑f : (a : S) → A)
⊢ ∃ (g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion (ker f) S)), (AdicCompletion.kerProj hf).comp g = AlgHom.id R A
have obtain : ∀ (g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion (ker f) S))
  (hg :
    AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ (ker f))) g =
      (↑(Ideal.quotientKerAlgEquivOfSurjective hf).symm : A →ₐ[R] S ⧸ ker f)),
  ∃ (g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion (ker f) S)), (AdicCompletion.kerProj hf).comp g = AlgHom.id R A
Tactic: obtain ⟨g, hg⟩ := exists_adicCompletionEvalOneₐ_comp_eq
    (Ideal.quotientKerAlgEquivOfSurjective hf).symm.toAlgHom
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.AdicCompletion (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
f : S →ₐ[R] A
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := S) (β := A) (⇑f : (a : S) → A)
g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion (ker f) S)
hg :
  AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ (ker f))) g =
    (↑(Ideal.quotientKerAlgEquivOfSurjective hf).symm : A →ₐ[R] S ⧸ ker f)
⊢ ∃ (g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion (ker f) S)), (AdicCompletion.kerProj hf).comp g = AlgHom.id R A
have h : (AdicCompletion.kerProj hf).comp g = AlgHom.id R A
Tactic: use g
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.AdicCompletion (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
f : S →ₐ[R] A
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := S) (β := A) (⇑f : (a : S) → A)
g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion (ker f) S)
hg :
  AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ (ker f))) g =
    (↑(Ideal.quotientKerAlgEquivOfSurjective hf).symm : A →ₐ[R] S ⧸ ker f)
⊢ (AdicCompletion.kerProj hf).comp g = AlgHom.id R A
have h : ∀ (x : A), Eq (α := A) (((AdicCompletion.kerProj hf).comp g : (a : A) → A) x : A) ((AlgHom.id R A : (a : A) → A) x : A)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallySmooth R A
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : AlgHom.{u, v, u_1} R A (B ⧸ I)
P : Generators R A A := Generators.self R A
⊢ Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
have rw : Subsingleton ↥P.toExtension.cotangentComplex.ker
Tactic: rw [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallySmooth R A
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : AlgHom.{u, v, u_1} R A (B ⧸ I)
P : Generators R A A := Generators.self R A
⊢ ∃ (a : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
have hP : Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
  (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
Tactic: have hP : Function.Injective P.toExtension.cotangentComplex := by
    rw [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot]
    exact FormallySmooth.subsingleton_h1Cotangent
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallySmooth R A
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : AlgHom.{u, v, u_1} R A (B ⧸ I)
P : Generators R A A := Generators.self R A
hP :
  Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
⊢ ∃ (a : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
have obtain : ∀ (l : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent)
  (hl : l ∘ₗ P.toExtension.cotangentComplex = LinearMap.id),
  ∃ (a : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
Tactic: obtain ⟨l, hl⟩ := ((P.toExtension.exact_cotangentComplex_toKaehler.split_tfae'.out 0 1 rfl rfl).mp
    ⟨P.toExtension.subsingleton_h1Cotangent.mp FormallySmooth.subsingleton_h1Cotangent,
      Module.projective_lifting_property _ _ P.toExtension.toKaehler_surjective⟩).2
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallySmooth R A
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : AlgHom.{u, v, u_1} R A (B ⧸ I)
P : Generators R A A := Generators.self R A
hP :
  Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
l : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
⊢ ∃ (a : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
have obtain : ∀
  (g :
    A →ₐ[R]
      P.Ring ⧸
        HPow.hPow (α := Ideal P.Ring) (β := ℕ)
          (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2)
  (hg : AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) g = AlgHom.id R A),
  ∃ (a : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
Tactic: obtain ⟨g, hg⟩ := retractionKerCotangentToTensorEquivSection (R := R) P.algebraMap_surjective
    ⟨⟨⟨Cotangent.val, by simp⟩, by simpa using Cotangent.val_smul' (P := P.toExtension)⟩ ∘ₗ
      l.restrictScalars P.toExtension.Ring, LinearMap.ext fun x ↦ congr($hl x)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallySmooth R A
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : AlgHom.{u, v, u_1} R A (B ⧸ I)
P : Generators R A A := Generators.self R A
hP :
  Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
l : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g :
  A →ₐ[R]
    P.Ring ⧸
      HPow.hPow (α := Ideal P.Ring) (β := ℕ)
        (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2
hg : AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) g = AlgHom.id R A
σ : (b : B ⧸ I) → B := Function.surjInv (f := (⇑(algebraMap B (B ⧸ I)) : (a : B) → B ⧸ I)) ⋯
x : P.Ring
⊢ Eq (α := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval (σ ∘ (⇑f : (a : A) → B ⧸ I)) : (a : MvPolynomial A R) → B) x) :
      B ⧸ I)
    ((f : (a : A) → B ⧸ I) ((algebraMap P.Ring A : (a : P.Ring) → A) x) : B ⧸ I)
have rw : Eq.{u_1 + 1} (α := B ⧸ I) ((aeval (_root_.id ∘ (⇑f : (a : A) → B ⧸ I)) : (a : MvPolynomial A R) → B ⧸ I) x : B ⧸ I)
  ((aeval fun (i : A) ↦ (f : (a : A) → B ⧸ I) (P.val i) : (a : MvPolynomial A R) → B ⧸ I) x : B ⧸ I)
Tactic: rw [← Ideal.Quotient.algebraMap_eq, ← aeval_algebraMap_apply, P.algebraMap_eq,
      AlgHom.coe_toRingHom, comp_aeval_apply, ← Function.comp_assoc, Function.comp_surjInv,]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallySmooth R A
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : AlgHom.{u, v, u_1} R A (B ⧸ I)
P : Generators R A A := Generators.self R A
hP :
  Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
l : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g :
  A →ₐ[R]
    P.Ring ⧸
      HPow.hPow (α := Ideal P.Ring) (β := ℕ)
        (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2
hg : AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) g = AlgHom.id R A
σ : (b : B ⧸ I) → B := Function.surjInv (f := (⇑(algebraMap B (B ⧸ I)) : (a : B) → B ⧸ I)) ⋯
⊢ ∃ (a : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
have H : ∀ (x : P.Ring),
  Eq (α := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval (σ ∘ (⇑f : (a : A) → B ⧸ I)) : (a : MvPolynomial A R) → B) x) :
      B ⧸ I)
    ((f : (a : A) → B ⧸ I) ((algebraMap P.Ring A : (a : P.Ring) → A) x) : B ⧸ I)
Tactic: have H (x : P.Ring) : ↑(aeval (σ ∘ f) x) = f (algebraMap _ A x) := by
    rw [← Ideal.Quotient.algebraMap_eq, ← aeval_algebraMap_apply, P.algebraMap_eq,
      AlgHom.coe_toRingHom, comp_aeval_apply, ← Function.comp_assoc, Function.comp_surjInv,]
    simp [P]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallySmooth R A
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : AlgHom.{u, v, u_1} R A (B ⧸ I)
P : Generators R A A := Generators.self R A
hP :
  Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
l_1 : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l_1 ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g :
  A →ₐ[R]
    P.Ring ⧸
      HPow.hPow (α := Ideal P.Ring) (β := ℕ)
        (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2
hg : AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) g = AlgHom.id R A
σ : (b : B ⧸ I) → B := Function.surjInv (f := (⇑(algebraMap B (B ⧸ I)) : (a : B) → B ⧸ I)) ⋯
H :
  ∀ (x : P.Ring),
    Eq (α := B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval (σ ∘ (⇑f : (a : A) → B ⧸ I)) : (a : MvPolynomial A R) → B) x) :
        B ⧸ I)
      ((f : (a : A) → B ⧸ I) ((algebraMap P.Ring A : (a : P.Ring) → A) x) : B ⧸ I)
l : P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ
    (HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2)
    (aeval (σ ∘ (⇑f : (a : A) → B ⧸ I))) ⋯
⊢ f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) = AlgHom.comp (Ideal.Quotient.mkₐ R I) l
have refine : ∀ (i : A),
  Eq.{u_1 + 1} (α := B ⧸ I)
    ((AlgHom.comp (f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)))
            (Ideal.Quotient.mkₐ R
              (HPow.hPow (α := Ideal P.Ring) (β := ℕ)
                (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2)) :
          (a : MvPolynomial A R) → B ⧸ I)
        (X i) :
      B ⧸ I)
    ((AlgHom.comp (AlgHom.comp (Ideal.Quotient.mkₐ R I) l)
            (Ideal.Quotient.mkₐ R
              (HPow.hPow (α := Ideal P.Ring) (β := ℕ)
                (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2)) :
          (a : MvPolynomial A R) → B ⧸ I)
        (X i) :
      B ⧸ I)
Tactic: refine Ideal.Quotient.algHom_ext _ (MvPolynomial.algHom_ext fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallySmooth R A
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : AlgHom.{u, v, u_1} R A (B ⧸ I)
P : Generators R A A := Generators.self R A
hP :
  Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
l_1 : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l_1 ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g :
  A →ₐ[R]
    P.Ring ⧸
      HPow.hPow (α := Ideal P.Ring) (β := ℕ)
        (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2
hg : AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) g = AlgHom.id R A
σ : (b : B ⧸ I) → B := Function.surjInv (f := (⇑(algebraMap B (B ⧸ I)) : (a : B) → B ⧸ I)) ⋯
H :
  ∀ (x : P.Ring),
    Eq (α := B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval (σ ∘ (⇑f : (a : A) → B ⧸ I)) : (a : MvPolynomial A R) → B) x) :
        B ⧸ I)
      ((f : (a : A) → B ⧸ I) ((algebraMap P.Ring A : (a : P.Ring) → A) x) : B ⧸ I)
l : P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ
    (HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2)
    (aeval (σ ∘ (⇑f : (a : A) → B ⧸ I))) ⋯
i : A
⊢ Eq.{u_1 + 1} (α := B ⧸ I)
    ((AlgHom.comp (f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)))
            (Ideal.Quotient.mkₐ R
              (HPow.hPow (α := Ideal P.Ring) (β := ℕ)
                (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2)) :
          (a : MvPolynomial A R) → B ⧸ I)
        (X i) :
      B ⧸ I)
    ((AlgHom.comp (AlgHom.comp (Ideal.Quotient.mkₐ R I) l)
            (Ideal.Quotient.mkₐ R
              (HPow.hPow (α := Ideal P.Ring) (β := ℕ)
                (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2)) :
          (a : MvPolynomial A R) → B ⧸ I)
        (X i) :
      B ⧸ I)
have change : Eq (α := B ⧸ I) ((f : (a : A) → B ⧸ I) ((algebraMap P.Ring A : (a : P.Ring) → A) (X i)) : B ⧸ I)
  ((algebraMap B (B ⧸ I) : (a : B) → B ⧸ I) ((aeval (σ ∘ (⇑f : (a : A) → B ⧸ I)) : (a : MvPolynomial A R) → B) (X i)) :
    B ⧸ I)
Tactic: change f (algebraMap P.Ring A (.X i)) = algebraMap _ _ (MvPolynomial.aeval (σ ∘ f) (.X i))
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallySmooth R A
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : AlgHom.{u, v, u_1} R A (B ⧸ I)
P : Generators R A A := Generators.self R A
hP :
  Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
l_1 : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l_1 ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g :
  A →ₐ[R]
    P.Ring ⧸
      HPow.hPow (α := Ideal P.Ring) (β := ℕ)
        (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2
hg : AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) g = AlgHom.id R A
σ : (b : B ⧸ I) → B := Function.surjInv (f := (⇑(algebraMap B (B ⧸ I)) : (a : B) → B ⧸ I)) ⋯
H :
  ∀ (x : P.Ring),
    Eq (α := B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval (σ ∘ (⇑f : (a : A) → B ⧸ I)) : (a : MvPolynomial A R) → B) x) :
        B ⧸ I)
      ((f : (a : A) → B ⧸ I) ((algebraMap P.Ring A : (a : P.Ring) → A) x) : B ⧸ I)
l : P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ
    (HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2)
    (aeval (σ ∘ (⇑f : (a : A) → B ⧸ I))) ⋯
⊢ ∃ (a : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
have this : f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) = AlgHom.comp (Ideal.Quotient.mkₐ R I) l
Tactic: have : f.comp (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift =
      (Ideal.Quotient.mkₐ R _).comp l := by
    refine Ideal.Quotient.algHom_ext _ (MvPolynomial.algHom_ext fun i ↦ ?_)
    change f (algebraMap P.Ring A (.X i)) = algebraMap _ _ (MvPolynomial.aeval (σ ∘ f) (.X i))
    simpa using (Function.surjInv_eq _ _).symm