awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ Eq (α := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B))
    (Submodule.restrictScalars A (LinearMap.ker (M₂ := Ω[B⁄R]) (mapBaseChange R A B)))
have h₁ : ∀ (x : B ⊗[A] Ω[A⁄R]),
  Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R])) (LinearMap.range (kerCotangentToTensor R A B)) x ↔
    Membership.mem (γ := Submodule A (B ⊗[A] Ω[A⁄R]))
      (Submodule.restrictScalars A (LinearMap.ker (M₂ := Ω[B⁄R]) (mapBaseChange R A B))) x
Tactic: classical
  ext x
  constructor
  · rintro ⟨x, rfl⟩
    obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x
    simp only [kerCotangentToTensor_toCotangent, Submodule.restrictScalars_mem, LinearMap.mem_ker,
      mapBaseChange_tmul, map_D, RingHom.mem_ker.mp x.2, map_zero, smul_zero]
  · intro hx
    obtain ⟨x, rfl⟩ := LinearMap.rTensor_surjective Ω[A⁄R] (g := Algebra.linearMap A B) h x
    obtain ⟨x, rfl⟩ := (TensorProduct.lid _ _).symm.surjective x
    replace hx : x ∈ LinearMap.ker (KaehlerDifferential.map R R A B) := by simpa using hx
    rw [KaehlerDifferential.ker_map_of_surjective R A B h] at hx
    obtain ⟨x, hx, rfl⟩ := hx
    simp only [TensorProduct.lid_symm_apply, LinearMap.rTensor_tmul,
      Algebra.linearMap_apply, map_one]
    rw [← Finsupp.sum_single x, Finsupp.sum, ← Finset.sum_fiberwise_of_maps_to
      (fun _ ↦ Finset.mem_image_of_mem (algebraMap A B))]
    simp only [map_sum (s := x.support.image (algebraMap A B)),
      TensorProduct.tmul_sum]
    apply sum_mem
    intro c _
    simp only [LinearMap.mem_range]
    simp only [map_sum, Finsupp.linearCombination_single]
    have : ∑ i ∈ x.support with algebraMap A B i = c, x i ∈ RingHom.ker (algebraMap A B) := by
      simpa [Finsupp.mapDomain, Finsupp.sum, Finsupp.finsetSum_apply, RingHom.mem_ker,
        Finsupp.single_apply, ← Finset.sum_filter] using DFunLike.congr_fun hx c
    obtain ⟨a, ha⟩ := h c
    use ∑ i ∈ {i ∈ x.support | algebraMap A B i = c}.attach, x i • Ideal.toCotangent _ ⟨i - a, ?_⟩
    · simp only [map_sum, LinearMapClass.map_smul, kerCotangentToTensor_toCotangent, map_sub]
      simp_rw [← TensorProduct.tmul_smul]
      -- TODO: was `simp [kerCotangentToTensor_toCotangent, RingHom.mem_ker.mp x.2]` and very slow
      -- (https://github.com/leanprover-community/mathlib4/issues/19751)
      simp only [smul_sub, TensorProduct.tmul_sub, Finset.sum_sub_distrib, ← TensorProduct.tmul_sum,
        ← Finset.sum_smul, Finset.sum_attach, sub_eq_self,
        Finset.sum_attach (f := fun i ↦ x i • KaehlerDifferential.D R A i)]
      rw [← TensorProduct.smul_tmul, ← Algebra.algebraMap_eq_smul_one, RingHom.mem_ker.mp this,
        TensorProduct.zero_tmul]
    · have : x i ≠ 0 ∧ algebraMap A B i = c := by
        convert! i.prop
        simp_rw [Finset.mem_filter, Finsupp.mem_support_iff]
      simp [RingHom.mem_ker, ha, this.2]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ Function.Surjective (α := B ⊗[A] Ω[A⁄R]) (β := Ω[B⁄R]) (⇑(mapBaseChange R A B) : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R])
have this : Subsingleton.{u_3 + 1} Ω[B⁄A]
Tactic: have := subsingleton_of_surjective A B h
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
this : Subsingleton.{u_3 + 1} Ω[B⁄A]
⊢ Function.Surjective (α := B ⊗[A] Ω[A⁄R]) (β := Ω[B⁄R]) (⇑(mapBaseChange R A B) : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R])
have rw : LE.le (α := Submodule B Ω[B⁄R]) ⊤ (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
Tactic: rw [← LinearMap.range_eq_top, range_mapBaseChange, ← top_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
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 : Q.toExtension.Cotangent
⊢ ∃ (a : Extension.Cotangent (toExtension (Q.comp P))),
    (Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
        a =
      x
have obtain : ∀ (x : Q.toExtension.Ring) (hx : x ∈ Q.toExtension.ker),
  ∃ (a : Extension.Cotangent (toExtension (Q.comp P))),
    Eq (α := Q.toExtension.Cotangent)
      ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
            (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
          a :
        Q.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker) x hx) :
        Q.toExtension.Cotangent)
Tactic: obtain ⟨⟨x, hx⟩, rfl⟩ := Extension.Cotangent.mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (hypothesis)
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 : Q.toExtension.Ring
hx : x ∈ Q.toExtension.ker
⊢ ∃ (a : Extension.Cotangent (toExtension (Q.comp P))),
    Eq (α := Q.toExtension.Cotangent)
      ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
            (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
          a :
        Q.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker) x hx) :
        Q.toExtension.Cotangent)
have this : x ∈ Q.ker
Tactic: have : x ∈ Q.ker := hx
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (hypothesis)
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 : Q.toExtension.Ring
hx : x ∈ Q.toExtension.ker
this : x ∈ Q.ker
⊢ ∃ (a : Extension.Cotangent (toExtension (Q.comp P))),
    Eq (α := Q.toExtension.Cotangent)
      ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
            (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
          a :
        Q.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker) x hx) :
        Q.toExtension.Cotangent)
have this₁ : ∃ (x_1 : Generators.Ring (Q.comp P)),
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x_1 ∧
    (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x_1 = x
Tactic: rw [← map_ofComp_ker Q P, Ideal.mem_map_iff_of_surjective
    _ (toAlgHom_ofComp_surjective Q P)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
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 : Q.toExtension.Ring
hx : x ∈ Q.toExtension.ker
this :
  ∃ (x_1 : Generators.Ring (Q.comp P)),
    Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x_1 ∧
      (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x_1 = x
⊢ ∃ (a : Extension.Cotangent (toExtension (Q.comp P))),
    Eq (α := Q.toExtension.Cotangent)
      ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
            (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
          a :
        Q.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker) x hx) :
        Q.toExtension.Cotangent)
have obtain : ∀ (x : Generators.Ring (Q.comp P)) (hx' : Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x)
  (hx :
    Membership.mem (α := Q.toExtension.Ring) Q.toExtension.ker
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring)),
  ∃ (a : Extension.Cotangent (toExtension (Q.comp P))),
    Eq (α := Q.toExtension.Cotangent)
      ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
            (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
          a :
        Q.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker)
            ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x) hx) :
        Q.toExtension.Cotangent)
Tactic: obtain ⟨x, hx', rfl⟩ := this
Cleared hypotheses: x, hx, this
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
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 σ
⊢ Function.Exact (M := T ⊗[S] P.toExtension.Cotangent) (N := Extension.Cotangent (toExtension (Q.comp P))) (P :=
    Q.toExtension.Cotangent)
    (⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)))) :
      (a : T ⊗[S] P.toExtension.Cotangent) → (Q.comp P).toExtension.Cotangent)
    (⇑(Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P))) :
      (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
have h1 : Eq (α := T ⊗[S] P.toExtension.Cotangent →ₗ[T] Q.toExtension.Cotangent)
  (Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) ∘ₗ
    LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P))))
  0
Tactic: apply LinearMap.exact_of_comp_of_mem_range
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
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 σ
h1 :
  Eq (α := T ⊗[S] P.toExtension.Cotangent →ₗ[T] Q.toExtension.Cotangent)
    (Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) ∘ₗ
      LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P))))
    0
⊢ Function.Exact (M := T ⊗[S] P.toExtension.Cotangent) (N := Extension.Cotangent (toExtension (Q.comp P))) (P :=
    Q.toExtension.Cotangent)
    (⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)))) :
      (a : T ⊗[S] P.toExtension.Cotangent) → (Q.comp P).toExtension.Cotangent)
    (⇑(Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P))) :
      (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
have h2 : ∀ (x : Extension.Cotangent (toExtension (Q.comp P))),
  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) →
    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: apply LinearMap.exact_of_comp_of_mem_range
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
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 σ
⊢ Eq (α := T ⊗[S] P.toExtension.Cotangent →ₗ[T] Q.toExtension.Cotangent)
    (Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) ∘ₗ
      LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P))))
    0
have h1 : Eq (α := P.toExtension.Cotangent →ₗ[S] Q.toExtension.Cotangent)
  (Extension.Cotangent.map
    (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
      (Hom.toExtensionHom (Q.toComp P))))
  0
Tactic: rw [LinearMap.liftBaseChange_comp, ← Extension.Cotangent.map_comp,
      EmbeddingLike.map_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
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 σ
⊢ Eq (α := P.toExtension.Cotangent →ₗ[S] Q.toExtension.Cotangent)
    (Extension.Cotangent.map
      (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
        (Hom.toExtensionHom (Q.toComp P))))
    0
have h1 : ∀ (x : P.toExtension.Cotangent),
  Eq (α := Q.toExtension.ker.Cotangent)
    (Extension.Cotangent.val
      ((Extension.Cotangent.map
            (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
              (Hom.toExtensionHom (Q.toComp P))) :
          (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent)
        x))
    (Extension.Cotangent.val ((0 : (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent) x))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
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.Cotangent
⊢ Eq (α := Q.toExtension.ker.Cotangent)
    (Extension.Cotangent.val
      ((Extension.Cotangent.map
            (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
              (Hom.toExtensionHom (Q.toComp P))) :
          (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent)
        x))
    (Extension.Cotangent.val ((0 : (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent) x))
have h1 : ∀ (x : P.toExtension.Ring) (hx : x ∈ P.toExtension.ker),
  Eq (α := Q.toExtension.ker.Cotangent)
    (Extension.Cotangent.val
      ((Extension.Cotangent.map
            (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
              (Hom.toExtensionHom (Q.toComp P))) :
          (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) x hx))))
    (Extension.Cotangent.val
      ((0 : (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) x hx))))
Tactic: obtain ⟨⟨x, hx⟩, rfl⟩ := Extension.Cotangent.mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
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
⊢ Eq (α := Q.toExtension.ker.Cotangent)
    (Extension.Cotangent.val
      ((Extension.Cotangent.map
            (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
              (Hom.toExtensionHom (Q.toComp P))) :
          (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) x hx))))
    (Extension.Cotangent.val
      ((0 : (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) x hx))))
have h1 : Eq (α := Q.toExtension.ker.Cotangent)
  ((Q.toExtension.ker.toCotangent : (a : ↥Q.toExtension.ker) → Q.toExtension.ker.Cotangent)
      (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker)
        ((Extension.Hom.toAlgHom
              (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
                (Hom.toExtensionHom (Q.toComp P))) :
            (a : P.toExtension.Ring) → Q.toExtension.Ring)
          x)
        sorry) :
    Q.toExtension.ker.Cotangent)
  (0 : Q.toExtension.ker.Cotangent)
Tactic: simp only [map_mk, val_mk, LinearMap.zero_apply, val_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
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
⊢ Eq (α := Q.toExtension.ker.Cotangent)
    ((Q.toExtension.ker.toCotangent : (a : ↥Q.toExtension.ker) → Q.toExtension.ker.Cotangent)
        (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker)
          ((Extension.Hom.toAlgHom
                (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
                  (Hom.toExtensionHom (Q.toComp P))) :
              (a : P.toExtension.Ring) → Q.toExtension.Ring)
            x)
          ⋯) :
      Q.toExtension.ker.Cotangent)
    (0 : Q.toExtension.ker.Cotangent)
have h : ↥Q.toExtension.ker = ↥Q.ker →
  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 : P.toExtension.Ring) → Q.toExtension.Ring)
        x :
      Q.toExtension.Ring)
    ((↑0 : Q.toExtension.Ring) : Q.toExtension.Ring)
Tactic: convert! Q.ker.toCotangent.map_zero
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
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)
    ((Extension.Hom.toAlgHom
            (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
              (Hom.toExtensionHom (Q.toComp P))) :
          (a : P.toExtension.Ring) → Q.toExtension.Ring)
        x :
      Q.toExtension.Ring)
    ((↑0 : Q.toExtension.Ring) : Q.toExtension.Ring)
have trans : 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 : P.toExtension.Ring) → Q.toExtension.Ring)
      x :
    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)
Tactic: trans ((IsScalarTower.toAlgHom R _ _).comp (IsScalarTower.toAlgHom R P.Ring S)) x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
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
trans :
  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 : P.toExtension.Ring) → Q.toExtension.Ring)
        x :
      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)
⊢ 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 : P.toExtension.Ring) → Q.toExtension.Ring)
        x :
      Q.toExtension.Ring)
    ((↑0 : Q.toExtension.Ring) : Q.toExtension.Ring)
have trans₁ : 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: trans ((IsScalarTower.toAlgHom R _ _).comp (IsScalarTower.toAlgHom R P.Ring S)) x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
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)
    ((Extension.Hom.toAlgHom
            (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
              (Hom.toExtensionHom (Q.toComp P))) :
          (a : P.toExtension.Ring) → Q.toExtension.Ring)
        x :
      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)
have e_a : 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: congr