awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
e_2 : ↥Q.toExtension.ker = ↥Q.ker
e_a :
  ∀ (i : σ),
    Eq (α := Q.toExtension.Ring)
      ((Extension.Hom.toAlgHom
              (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
                (Hom.toExtensionHom (Q.toComp P))) :
            (a : MvPolynomial σ R) → Q.toExtension.Ring)
          (X i) :
        Q.toExtension.Ring)
      ((AlgHom.comp (IsScalarTower.toAlgHom R S Q.toExtension.Ring) (IsScalarTower.toAlgHom R P.Ring S) :
            (a : MvPolynomial σ R) → Q.toExtension.Ring)
          (X i) :
        Q.toExtension.Ring)
⊢ Eq (α := P.toExtension.Ring →ₐ[R] Q.toExtension.Ring)
    (Extension.Hom.toAlgHom
      (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
        (Hom.toExtensionHom (Q.toComp P))))
    (AlgHom.comp (IsScalarTower.toAlgHom R S Q.toExtension.Ring) (IsScalarTower.toAlgHom R P.Ring S))

Tactic:
refine MvPolynomial.algHom_ext fun i ↦ ?_

Premises used: MvPolynomial.algHom_ext
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
e_2 : ↥Q.toExtension.ker = ↥Q.ker
i : σ
e_a :
  Eq (α := Q.Ring)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        ((Hom.toAlgHom (Q.toComp P) : (a : P.Ring) → (Q.comp P).Ring) (X i)) :
      Q.Ring)
    ((AlgHom.comp (IsScalarTower.toAlgHom R S Q.toExtension.Ring) (IsScalarTower.toAlgHom R P.Ring S) :
          (a : MvPolynomial σ R) → Q.toExtension.Ring)
        (X i) :
      Q.toExtension.Ring)
⊢ Eq (α := Q.toExtension.Ring)
    ((Extension.Hom.toAlgHom
            (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
              (Hom.toExtensionHom (Q.toComp P))) :
          (a : MvPolynomial σ R) → Q.toExtension.Ring)
        (X i) :
      Q.toExtension.Ring)
    ((AlgHom.comp (IsScalarTower.toAlgHom R S Q.toExtension.Ring) (IsScalarTower.toAlgHom R P.Ring S) :
          (a : MvPolynomial σ R) → Q.toExtension.Ring)
        (X i) :
      Q.toExtension.Ring)

Tactic:
change (Q.ofComp P).toAlgHom ((Q.toComp P).toAlgHom (X i)) = _

Premises used: Algebra.Generators.toComp, Algebra.Generators.Hom.toAlgHom, MvPolynomial.X, Algebra.Generators.ofComp, DFunLike.coe
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
e_2 : ↥Q.toExtension.ker = ↥Q.ker
i : σ
⊢ Eq (α := Q.Ring)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        ((Hom.toAlgHom (Q.toComp P) : (a : P.Ring) → (Q.comp P).Ring) (X i)) :
      Q.Ring)
    ((AlgHom.comp (IsScalarTower.toAlgHom R S Q.toExtension.Ring) (IsScalarTower.toAlgHom R P.Ring S) :
          (a : MvPolynomial σ R) → Q.toExtension.Ring)
        (X i) :
      Q.toExtension.Ring)

Tactic:
simp
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
e_2 : ↥Q.toExtension.ker = ↥Q.ker
⊢ Eq (α := Q.toExtension.Ring)
    ((AlgHom.comp (IsScalarTower.toAlgHom R S Q.toExtension.Ring) (IsScalarTower.toAlgHom R P.Ring S) :
          (a : P.Ring) → Q.toExtension.Ring)
        x :
      Q.toExtension.Ring)
    ((↑0 : Q.toExtension.Ring) : Q.toExtension.Ring)

Tactic:
simp [aeval_val_eq_zero hx]

Premises used: Algebra.Generators.aeval_val_eq_zero
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Extension.Cotangent (toExtension (Q.comp P))
hx :
  Eq (α := Q.toExtension.Cotangent)
    ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
        x :
      Q.toExtension.Cotangent)
    (0 : Q.toExtension.Cotangent)
h2 :
  ∀ (x : Generators.Ring (Q.comp P))
    (hx' :
      Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P))) x)
    (hx :
      Eq (α := Q.toExtension.Cotangent)
        ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
              (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
            ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
              (Subtype.mk (p := fun (x : Extension.Ring (toExtension (Q.comp P))) ↦
                Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P))))
                  (Extension.ker (toExtension (Q.comp P))) x)
                x hx')) :
          Q.toExtension.Cotangent)
        (0 : Q.toExtension.Cotangent)),
    Membership.mem (α := Extension.Cotangent (toExtension (Q.comp P))) (γ :=
      Submodule T (Extension.Cotangent (toExtension (Q.comp P))))
      (LinearMap.range (M := T ⊗[S] P.toExtension.Cotangent)
        (LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)))))
      ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Extension.Ring (toExtension (Q.comp P))) ↦
            Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P))))
              (Extension.ker (toExtension (Q.comp P))) x)
            x hx') :
        Extension.Cotangent (toExtension (Q.comp P)))
⊢ Membership.mem (γ := Submodule T (Extension.Cotangent (toExtension (Q.comp P))))
    (LinearMap.range (M := T ⊗[S] P.toExtension.Cotangent)
      (LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)))))
    x

Tactic:
obtain ⟨⟨x : (Q.comp P).Ring, hx'⟩, rfl⟩ := Extension.Cotangent.mk_surjective x

Premises used: Algebra.Generators.Ring, Algebra.Generators.comp, Algebra.Extension.Cotangent.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Generators.Ring (Q.comp P)
hx' : Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P))) x
hx :
  Eq (α := Q.toExtension.Cotangent)
    ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Extension.Ring (toExtension (Q.comp P))) ↦
            Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P))))
              (Extension.ker (toExtension (Q.comp P))) x)
            x hx')) :
      Q.toExtension.Cotangent)
    (0 : Q.toExtension.Cotangent)
⊢ Membership.mem (α := Q.Ring) (HPow.hPow (β := ℕ) Q.ker 2)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring)

Tactic:
simpa only [map_mk, val_mk, val_zero, Ideal.toCotangent_eq_zero] using congr(($hx).val)

Premises used: Algebra.Extension.Cotangent.val_mk, Ideal.toCotangent_eq_zero, Algebra.Extension.Cotangent.val_zero, Algebra.Extension.Cotangent.map_mk
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Generators.Ring (Q.comp P)
hx' : Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P))) x
hx :
  Eq (α := Q.toExtension.Cotangent)
    ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Extension.Ring (toExtension (Q.comp P))) ↦
            Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P))))
              (Extension.ker (toExtension (Q.comp P))) x)
            x hx')) :
      Q.toExtension.Cotangent)
    (0 : Q.toExtension.Cotangent)
⊢ Membership.mem (α := Q.Ring) (HPow.hPow (β := ℕ) Q.ker 2)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring)

Tactic:
replace hx : (Q.ofComp P).toAlgHom x ∈ Q.ker ^ 2 := by
      simpa only [map_mk, val_mk, val_zero, Ideal.toCotangent_eq_zero] using congr(($hx).val)
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Generators.Ring (Q.comp P)
hx' : Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P))) x
hx :
  Membership.mem (α := Q.Ring) (HPow.hPow (β := ℕ) Q.ker 2)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring)
⊢ ∃ x_1 ∈ HMul.hMul (α := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) (ker (Q.comp P)),
    Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x_1 : Q.Ring)
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring)

Tactic:
rw [pow_two, ← map_ofComp_ker (P := P), ← Ideal.map_mul, Ideal.mem_map_iff_of_surjective
      _ (toAlgHom_ofComp_surjective Q P)] at hx

Premises used: pow_two, Ideal.map_mul, Algebra.Generators.map_ofComp_ker, Algebra.Generators.toAlgHom_ofComp_surjective, Ideal.mem_map_iff_of_surjective
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Generators.Ring (Q.comp P)
hx' : Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P))) x
hx :
  ∃ x_1 ∈ HMul.hMul (α := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) (ker (Q.comp P)),
    Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x_1 : Q.Ring)
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring)
h2 :
  ∀ (y : Generators.Ring (Q.comp P))
    (hy : y ∈ HMul.hMul (α := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) (ker (Q.comp P)))
    (e :
      Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) y : Q.Ring)
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring)),
    Membership.mem (α := Extension.Cotangent (toExtension (Q.comp P))) (γ :=
      Submodule T (Extension.Cotangent (toExtension (Q.comp P))))
      (LinearMap.range (M := T ⊗[S] P.toExtension.Cotangent)
        (LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)))))
      ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Extension.Ring (toExtension (Q.comp P))) ↦
            Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P))))
              (Extension.ker (toExtension (Q.comp P))) x)
            x hx') :
        Extension.Cotangent (toExtension (Q.comp P)))
⊢ Membership.mem (α := Extension.Cotangent (toExtension (Q.comp P))) (γ :=
    Submodule T (Extension.Cotangent (toExtension (Q.comp P))))
    (LinearMap.range (M := T ⊗[S] P.toExtension.Cotangent)
      (LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)))))
    ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Extension.Ring (toExtension (Q.comp P))) ↦
          Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P)))
            x)
          x hx') :
      Extension.Cotangent (toExtension (Q.comp P)))

Tactic:
obtain ⟨y, hy, e⟩ := hx
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Generators.Ring (Q.comp P)
hx' : Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P))) x
y : Generators.Ring (Q.comp P)
hy : y ∈ HMul.hMul (α := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) (ker (Q.comp P))
e :
  Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) y : Q.Ring)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring)
⊢ Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker) (x - y)

Tactic:
rw [eq_comm, ← sub_eq_zero, ← map_sub, ← RingHom.mem_ker, ← map_toComp_ker] at e

Premises used: map_sub, sub_eq_zero, Algebra.Generators.map_toComp_ker, RingHom.mem_ker, eq_comm
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Generators.Ring (Q.comp P)
hx' : Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P))) x
y : Generators.Ring (Q.comp P)
hy : y ∈ HMul.hMul (α := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) (ker (Q.comp P))
e :
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker) (x - y)
h2 :
  Membership.mem (α := Extension.Cotangent (toExtension (Q.comp P))) (γ :=
    Submodule T (Extension.Cotangent (toExtension (Q.comp P))))
    (Submodule.span T
      (↑(LinearMap.range (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)))) :
        Set (Q.comp P).toExtension.Cotangent))
    ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Extension.Ring (toExtension (Q.comp P))) ↦
          Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P)))
            x)
          x hx') :
      Extension.Cotangent (toExtension (Q.comp P)))
⊢ Membership.mem (α := Extension.Cotangent (toExtension (Q.comp P))) (γ :=
    Submodule T (Extension.Cotangent (toExtension (Q.comp P))))
    (LinearMap.range (M := T ⊗[S] P.toExtension.Cotangent)
      (LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)))))
    ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Extension.Ring (toExtension (Q.comp P))) ↦
          Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P)))
            x)
          x hx') :
      Extension.Cotangent (toExtension (Q.comp P)))

Tactic:
rw [LinearMap.range_liftBaseChange]

Premises used: LinearMap.range_liftBaseChange
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Generators.Ring (Q.comp P)
hx' : Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P))) x
y : Generators.Ring (Q.comp P)
hy : y ∈ HMul.hMul (α := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) (ker (Q.comp P))
e :
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker) (x - y)
z : ↥(ker (Q.comp P)) :=
  Subtype.mk (p := fun (x : Generators.Ring (Q.comp P)) ↦
    Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x) (x - y) ⋯
⊢ Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    (↑z : (Q.comp P).Ring)

Tactic:
have hz : z.1 ∈ P.ker.map (Q.toComp P).toAlgHom.toRingHom := e
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Generators.Ring (Q.comp P)
hx' : Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P))) x
y : Generators.Ring (Q.comp P)
hy : y ∈ HMul.hMul (α := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) (ker (Q.comp P))
e :
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker) (x - y)
z : ↥(ker (Q.comp P)) :=
  Subtype.mk (p := fun (x : Generators.Ring (Q.comp P)) ↦
    Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x) (x - y) ⋯
hz :
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    (↑z : (Q.comp P).Ring)
⊢ Eq (α := Ideal.Cotangent (R := Extension.Ring (toExtension (Q.comp P))) (Extension.ker (toExtension (Q.comp P))))
    (Extension.Cotangent.val
      ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Extension.Ring (toExtension (Q.comp P))) ↦
          Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P)))
            x)
          x hx')))
    (Extension.Cotangent.val
      ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent) z))

Tactic:
simpa only [val_mk, Ideal.toCotangent_eq, sub_sub_cancel, pow_two, z]

Premises used: Ideal.toCotangent_eq, pow_two, Algebra.Extension.Cotangent.val_mk, sub_sub_cancel
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Generators.Ring (Q.comp P)
hx' : Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P))) x
y : Generators.Ring (Q.comp P)
hy : y ∈ HMul.hMul (α := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) (ker (Q.comp P))
e :
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker) (x - y)
z : ↥(ker (Q.comp P)) :=
  Subtype.mk (p := fun (x : Generators.Ring (Q.comp P)) ↦
    Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x) (x - y) ⋯
hz :
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    (↑z : (Q.comp P).Ring)
⊢ Eq (α := Extension.Cotangent (toExtension (Q.comp P)))
    ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Extension.Ring (toExtension (Q.comp P))) ↦
          Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P)))
            x)
          x hx') :
      Extension.Cotangent (toExtension (Q.comp P)))
    ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent) z :
      Extension.Cotangent (toExtension (Q.comp P)))

Tactic:
have : Extension.Cotangent.mk (P := (Q.comp P).toExtension) ⟨x, hx'⟩ =
      Extension.Cotangent.mk z := by
      ext; simpa only [val_mk, Ideal.toCotangent_eq, sub_sub_cancel, pow_two, z]
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Generators.Ring (Q.comp P)
hx' : Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P))) x
y : Generators.Ring (Q.comp P)
hy : y ∈ HMul.hMul (α := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) (ker (Q.comp P))
e :
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker) (x - y)
z : ↥(ker (Q.comp P)) :=
  Subtype.mk (p := fun (x : Generators.Ring (Q.comp P)) ↦
    Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x) (x - y) ⋯
hz :
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    (↑z : (Q.comp P).Ring)
this :
  Eq (α := Extension.Cotangent (toExtension (Q.comp P)))
    ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Extension.Ring (toExtension (Q.comp P))) ↦
          Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P)))
            x)
          x hx') :
      Extension.Cotangent (toExtension (Q.comp P)))
    ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent) z :
      Extension.Cotangent (toExtension (Q.comp P)))
⊢ (↑z : (Q.comp P).toExtension.Ring) ∈
    Submodule.map (Submodule.subtype (Extension.ker (toExtension (Q.comp P))))
      (Submodule.comap Extension.Cotangent.mk
        (Submodule.restrictScalars (Generators.Ring (Q.comp P))
          (Submodule.span T
            (↑(LinearMap.range (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)))) :
              Set (Q.comp P).toExtension.Cotangent))))

Tactic:
(show Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker ≤ _ from ?_) hz

Premises used: Set.Mem