awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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))))
have h2 : Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker ≤
  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: refine (show Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker ≤ _ from ?_) hz
-- 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 : 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)))
⊢ Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker ≤
    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))))
have h2 : P.ker ≤
  Ideal.comap (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)))
    (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: rw [Ideal.map_le_iff_le_comap]
-- 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 : 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)))
w : P.Ring
hw : w ∈ P.ker
⊢ Membership.mem (α := Generators.Ring (Q.comp P)) (γ :=
    Submodule (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P)))
    (Extension.ker (toExtension (Q.comp P)) : Ideal (Extension.Ring (toExtension (Q.comp P))))
    ((Hom.toAlgHom (Q.toComp P) : (a : P.Ring) → (Q.comp P).Ring) w : Generators.Ring (Q.comp P))
have h2 : Eq.{u₃ + 1} (α := T) ((algebraMap S T : (a : S) → T) ((aeval P.val : (a : MvPolynomial σ R) → S) w : S) : T) (0 : T)
Tactic: simp only [ker_eq_ker_aeval_val, RingHom.mem_ker, Hom.algebraMap_toAlgHom]
-- 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 : 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)))
w : P.Ring
hw : w ∈ P.ker
⊢ Eq.{u₃ + 1} (α := T) ((algebraMap S T : (a : S) → T) ((aeval P.val : (a : MvPolynomial σ R) → S) w : S) : T) (0 : T)
have h2 : Eq.{u₃ + 1} (α := T) ((algebraMap S T : (a : S) → T) 0 : T) (0 : T)
Tactic: rw [aeval_val_eq_zero hw, 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 : 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)))
w : P.Ring
hw : w ∈ P.ker
h2 : Eq.{u₃ + 1} (α := T) ((algebraMap S T : (a : S) → T) 0 : T) (0 : T)
⊢ Eq.{u₃ + 1} (α := T) ((algebraMap S T : (a : S) → T) ((aeval P.val : (a : MvPolynomial σ R) → S) w : S) : T) (0 : T)
have h2₁ : Eq.{u₃ + 1} (α := T) 0 0
Tactic: rw [aeval_val_eq_zero hw, 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 σ
⊢ Eq (α := T ⊗[S] P.toExtension.CotangentSpace →ₗ[T] Extension.CotangentSpace (toExtension (Q.comp P)))
    ((↑(LinearEquiv.symm (compEquiv Q P)) :
        Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace →ₗ[T]
          (Q.comp P).toExtension.CotangentSpace) ∘ₗ
      LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
    (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))))
have apply : ∀ (i : σ),
  Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)))
    (((↑(LinearEquiv.symm (compEquiv Q P)) :
              Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace →ₗ[T]
                (Q.comp P).toExtension.CotangentSpace) ∘ₗ
            LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i) :
      Extension.CotangentSpace (toExtension (Q.comp P)))
    ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i) :
      Extension.CotangentSpace (toExtension (Q.comp P)))
Tactic: apply (P.cotangentSpaceBasis.baseChange T).ext
-- 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 σ
i : σ
⊢ Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)))
    (((↑(LinearEquiv.symm (compEquiv Q P)) :
              Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace →ₗ[T]
                (Q.comp P).toExtension.CotangentSpace) ∘ₗ
            LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i) :
      Extension.CotangentSpace (toExtension (Q.comp P)))
    ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i) :
      Extension.CotangentSpace (toExtension (Q.comp P)))
have a : Eq (α := ι ⊕ σ →₀ T)
  ((Basis.repr (cotangentSpaceBasis (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
      (((↑(LinearEquiv.symm (compEquiv Q P)) :
              Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace →ₗ[T]
                (Q.comp P).toExtension.CotangentSpace) ∘ₗ
            LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i)) :
    ι ⊕ σ →₀ T)
  ((Basis.repr (cotangentSpaceBasis (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
      ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i)) :
    ι ⊕ σ →₀ T)
Tactic: apply (Q.comp P).cotangentSpaceBasis.repr.injective
-- 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 σ
i : σ
⊢ Eq (α := ι ⊕ σ →₀ T)
    ((Basis.repr (cotangentSpaceBasis (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
        (((↑(LinearEquiv.symm (compEquiv Q P)) :
                Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace →ₗ[T]
                  (Q.comp P).toExtension.CotangentSpace) ∘ₗ
              LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) :
            (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
          ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i)) :
      ι ⊕ σ →₀ T)
    ((Basis.repr (cotangentSpaceBasis (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
        ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
            (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
          ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i)) :
      ι ⊕ σ →₀ T)
have a : ∀ (j : ι ⊕ σ),
  Eq.{u₃ + 1} (α := T)
    ((((Basis.repr (cotangentSpaceBasis (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
              (((↑(LinearEquiv.symm (compEquiv Q P)) :
                      Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace →ₗ[T]
                        (Q.comp P).toExtension.CotangentSpace) ∘ₗ
                    LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) :
                  (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
                ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i)) :
            ι ⊕ σ →₀ T) :
          (a : ι ⊕ σ) → T)
        j :
      T)
    ((((Basis.repr (cotangentSpaceBasis (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
              ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
                  (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
                ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i)) :
            ι ⊕ σ →₀ T) :
          (a : ι ⊕ σ) → T)
        j :
      T)
Tactic: ext j
-- 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 σ
i : σ
j : ι ⊕ σ
⊢ Eq.{u₃ + 1} (α := T)
    ((((Basis.repr (cotangentSpaceBasis (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
              (((↑(LinearEquiv.symm (compEquiv Q P)) :
                      Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace →ₗ[T]
                        (Q.comp P).toExtension.CotangentSpace) ∘ₗ
                    LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) :
                  (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
                ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i)) :
            ι ⊕ σ →₀ T) :
          (a : ι ⊕ σ) → T)
        j :
      T)
    ((((Basis.repr (cotangentSpaceBasis (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
              ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
                  (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
                ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i)) :
            ι ⊕ σ →₀ T) :
          (a : ι ⊕ σ) → T)
        j :
      T)
have a : Eq.{u₃ + 1} (α := T)
  ((((Basis.repr (Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis)) :
              (a : Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
            (0, 1 ⊗ₜ[S] (P.cotangentSpaceBasis : (a : σ) → P.toExtension.CotangentSpace) i) :
          ι ⊕ σ →₀ T) :
        (a : ι ⊕ σ) → T)
      j :
    T)
  ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι ⊕ σ) R) → T)
      (Pi.single (M := fun (x : ι ⊕ σ) ↦ MvPolynomial (ι ⊕ σ) R) j (1 : (fun (x : ι ⊕ σ) ↦ MvPolynomial (ι ⊕ σ) R) j)
          (Sum.inr i) :
        MvPolynomial (ι ⊕ σ) R) :
    T)
Tactic: simp only [compEquiv, LinearEquiv.trans_symm, LinearEquiv.symm_symm,
    Basis.baseChange_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, LinearMap.coe_inr,
    Function.comp_apply, LinearEquiv.trans_apply, Basis.repr_symm_apply, pderiv_X, toComp_val,
    Basis.repr_linearCombination, LinearMap.liftBaseChange_tmul, one_smul, repr_CotangentSpaceMap]
-- 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 σ
i : σ
j : ι ⊕ σ
⊢ Eq.{u₃ + 1} (α := T)
    ((((Basis.repr (Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis)) :
                (a : Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
              (0, 1 ⊗ₜ[S] (P.cotangentSpaceBasis : (a : σ) → P.toExtension.CotangentSpace) i) :
            ι ⊕ σ →₀ T) :
          (a : ι ⊕ σ) → T)
        j :
      T)
    ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι ⊕ σ) R) → T)
        (Pi.single (M := fun (x : ι ⊕ σ) ↦ MvPolynomial (ι ⊕ σ) R) j (1 : (fun (x : ι ⊕ σ) ↦ MvPolynomial (ι ⊕ σ) R) j)
            (Sum.inr i) :
          MvPolynomial (ι ⊕ σ) R) :
      T)
have a : ∀ (j : ι),
  Eq.{u₃ + 1} (α := T)
    ((((Basis.repr (Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis)) :
                (a : Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
              (0, 1 ⊗ₜ[S] (P.cotangentSpaceBasis : (a : σ) → P.toExtension.CotangentSpace) i) :
            ι ⊕ σ →₀ T) :
          (a : ι ⊕ σ) → T)
        (Sum.inl j) :
      T)
    ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι ⊕ σ) R) → T)
        (Pi.single (M := fun (x : ι ⊕ σ) ↦ MvPolynomial (ι ⊕ σ) R) (Sum.inl j)
            (1 : (fun (x : ι ⊕ σ) ↦ MvPolynomial (ι ⊕ σ) R) (Sum.inl j)) (Sum.inr i) :
          MvPolynomial (ι ⊕ σ) R) :
      T)
Tactic: obtain (j | j) := j
Cleared hypotheses: j