awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
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
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:
simpa using congr($hg x)
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
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)
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
⊢ ∃ (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

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, Algebra.FormallySmooth.exists_adicCompletionEvalOneₐ_comp_eq, Ideal.quotientKerAlgEquivOfSurjective
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
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)
h : (AdicCompletion.kerProj hf).comp g = AlgHom.id R A
⊢ ∃ (g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion (ker f) S)), (AdicCompletion.kerProj hf).comp g = AlgHom.id R A

Tactic:
use g
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
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)
h :
  ∀ (x : A),
    Eq (α := A) (((AdicCompletion.kerProj hf).comp g : (a : A) → A) x : A) ((AlgHom.id R A : (a : A) → A) x : A)
⊢ (AdicCompletion.kerProj hf).comp g = AlgHom.id R A

Tactic:
ext x
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
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)
x : A
⊢ Eq (α := A) (((AdicCompletion.kerProj hf).comp g : (a : A) → A) x : A) ((AlgHom.id R A : (a : A) → A) x : A)

Tactic:
simpa using congr(Ideal.quotientKerAlgEquivOfSurjective hf ($hg x))
-- Module: Mathlib.RingTheory.Smooth.Basic
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
rw : Subsingleton ↥P.toExtension.cotangentComplex.ker
⊢ Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)

Tactic:
rw [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot]

Premises used: Submodule.subsingleton_iff_eq_bot, LinearMap.ker_eq_bot
-- Module: Mathlib.RingTheory.Smooth.Basic
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
⊢ Subsingleton ↥P.toExtension.cotangentComplex.ker

Tactic:
FormallySmooth.subsingleton_h1Cotangent

Premises used: Set.Mem, Algebra.Extension.H1Cotangent, Algebra.FormallySmooth.subsingleton_h1Cotangent
-- Module: Mathlib.RingTheory.Smooth.Basic
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
⊢ Subsingleton ↥P.toExtension.cotangentComplex.ker

Tactic:
exact FormallySmooth.subsingleton_h1Cotangent

Premises used: Algebra.FormallySmooth.subsingleton_h1Cotangent
-- Module: Mathlib.RingTheory.Smooth.Basic
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)

Tactic:
have hP : Function.Injective P.toExtension.cotangentComplex := by
    rw [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot]
    exact FormallySmooth.subsingleton_h1Cotangent
-- Module: Mathlib.RingTheory.Smooth.Basic
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)
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
⊢ ∃ (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

Premises used: Algebra.Extension.subsingleton_h1Cotangent, Function.Exact.split_tfae', List.TFAE.out, And.right, Algebra.Extension.toKaehler_surjective, And.intro, Algebra.FormallySmooth.subsingleton_h1Cotangent, Iff.mp, Module.projective_lifting_property, Algebra.Generators.toExtension, OfNat.ofNat, Algebra.Extension.exact_cotangentComplex_toKaehler, rfl
-- Module: Mathlib.RingTheory.Smooth.Basic
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
⊢ ∀ (x y : P.toExtension.Cotangent), (x + y).val = x.val + y.val

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.Basic
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
⊢ ∀ (m : P.Ring) (x : P.toExtension.Cotangent),
    AddHom.toFun
        { toFun := Cotangent.val, map_add' := ⋯ :
          P.toExtension.Cotangent →ₙ+ Ideal.Cotangent (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) }
        (m • x) =
      HSMul.hSMul (α := P.Ring) ((RingHom.id P.Ring : (a : P.Ring) → P.Ring) m : P.Ring)
        (AddHom.toFun
          { toFun := Cotangent.val, map_add' := ⋯ :
            P.toExtension.Cotangent →ₙ+ Ideal.Cotangent (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) }
          x)

Tactic:
simpa using Cotangent.val_smul' (P := P.toExtension)

Premises used: Algebra.Extension.Cotangent.val_smul'
-- Module: Mathlib.RingTheory.Smooth.Basic
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
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
⊢ ∃ (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)⟩

Premises used: LinearMap.restrictScalars, Algebra.Generators.algebraMap_surjective, LinearMap.ext, congrArg, id, Algebra.Extension.Ring, Subtype.mk, LinearMap.comp, LinearMap.mk, AddHom.mk, Algebra.Generators.toExtension, DFunLike.coe, retractionKerCotangentToTensorEquivSection
-- Module: Mathlib.RingTheory.Smooth.Basic
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
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)
⊢ 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:
rw [← Ideal.Quotient.algebraMap_eq, ← aeval_algebraMap_apply, P.algebraMap_eq,
      AlgHom.coe_toRingHom, comp_aeval_apply, ← Function.comp_assoc, Function.comp_surjInv,]

Premises used: AlgHom.coe_toRingHom, Ideal.Quotient.algebraMap_eq, Algebra.Generators.algebraMap_eq, MvPolynomial.aeval_algebraMap_apply, MvPolynomial.comp_aeval_apply, Function.comp_surjInv, Function.comp_assoc
-- Module: Mathlib.RingTheory.Smooth.Basic
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.{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:
simp [P]
-- Module: Mathlib.RingTheory.Smooth.Basic
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)

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]
-- Module: Mathlib.RingTheory.Smooth.Basic
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)) ⋯
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)
x : P.Ring
hx : Membership.mem (γ := Submodule P.Ring P.Ring) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) x
⊢ Membership.mem (γ := Submodule P.Ring P.Ring)
    (Ideal.comap (F := MvPolynomial A R →+* B) (AlgHom.toRingHom (aeval (σ ∘ (⇑f : (a : A) → B ⧸ I)))) I) x

Tactic:
simp_all [← Ideal.Quotient.eq_zero_iff_mem (I := I), -map_aeval]

Premises used: MvPolynomial.map_aeval, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Smooth.Basic
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

Tactic:
Ideal.Quotient.algHom_ext _ (MvPolynomial.algHom_ext fun i ↦ ?_)

Premises used: MvPolynomial.algHom_ext, Ideal.Quotient.algHom_ext
-- Module: Mathlib.RingTheory.Smooth.Basic
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))) ⋯
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)
⊢ f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) = AlgHom.comp (Ideal.Quotient.mkₐ R I) l

Tactic:
refine Ideal.Quotient.algHom_ext _ (MvPolynomial.algHom_ext fun i ↦ ?_)

Premises used: Ideal.Quotient.algHom_ext