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 : 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)))
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))))
⊢ (↑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:
refine (show Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker ≤ _ from ?_) hz
-- 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)))
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)))))
⊢ 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:
rw [Ideal.map_le_iff_le_comap]

Premises used: Ideal.map_le_iff_le_comap
-- 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)))
w : P.Ring
hw : w ∈ P.ker
h2 :
  Eq.{u₃ + 1} (α := T) ((algebraMap S T : (a : S) → T) ((aeval P.val : (a : MvPolynomial σ R) → S) w : S) : T) (0 : T)
⊢ 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))

Tactic:
simp only [ker_eq_ker_aeval_val, RingHom.mem_ker, Hom.algebraMap_toAlgHom]

Premises used: RingHom.mem_ker, Algebra.Generators.ker_eq_ker_aeval_val, Algebra.Generators.Hom.algebraMap_toAlgHom
-- 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)))
w : P.Ring
hw : w ∈ P.ker
h2 : Eq.{u₃ + 1} (α := T) ((algebraMap S T : (a : S) → T) 0 : T) (0 : T)
h2₁ h2₂ : Eq.{u₃ + 1} (α := T) 0 0
⊢ Eq.{u₃ + 1} (α := T) ((algebraMap S T : (a : S) → T) ((aeval P.val : (a : MvPolynomial σ R) → S) w : S) : T) (0 : T)

Tactic:
rw [aeval_val_eq_zero hw, map_zero]

Premises used: map_zero, 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 : 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 (α := 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)
          ((Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.toComp P)) :
              (a : P.toExtension.Ring) → (Q.comp P).toExtension.Ring)
            (↑(Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) w hw) : P.toExtension.Ring))
          ⋯) :
      Extension.Cotangent (toExtension (Q.comp P)))
    (((Extension.Cotangent.mk :
            LinearMap (R := Extension.Ring (toExtension (Q.comp P)))
              (RingHom.id (Extension.Ring (toExtension (Q.comp P)))) (↥(Extension.ker (toExtension (Q.comp P))))
              (Extension.Cotangent (toExtension (Q.comp P)))) :
          (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
        (Subtype.mk (p := fun (a : Generators.Ring (Q.comp P)) ↦
          Membership.mem (γ := Submodule (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P)))
            (Extension.ker (toExtension (Q.comp P))) a)
          ((Hom.toAlgHom (Q.toComp P) : (a : P.Ring) → (Q.comp P).Ring) w) ⋯) :
      Extension.Cotangent (toExtension (Q.comp P)))

Tactic:
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 σ
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)))
⊢ 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))))

Tactic:
apply (P.cotangentSpaceBasis.baseChange T).ext

Premises used: Algebra.Generators.cotangentSpaceBasis, Module.Basis.baseChange, Module.Basis.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 σ
i : σ
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)
⊢ 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 (Q.comp P).cotangentSpaceBasis.repr.injective

Premises used: Algebra.Generators.comp, Algebra.Generators.cotangentSpaceBasis, Module.Basis.repr, LinearEquiv.injective
-- 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 σ
i : σ
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)
⊢ 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:
ext j
-- 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 σ
i : σ
j : ι ⊕ σ
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)
⊢ 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:
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]

Premises used: Algebra.Generators.CotangentSpace.compEquiv, LinearMap.coe_inr, Algebra.Generators.toComp_val, Module.Basis.repr_linearCombination, MvPolynomial.pderiv_X, LinearEquiv.trans_apply, Module.Basis.baseChange_apply, LinearEquiv.symm_symm, one_smul, LinearMap.liftBaseChange_tmul, LinearMap.coe_comp, Algebra.Generators.repr_CotangentSpaceMap, Function.comp_apply, LinearEquiv.trans_symm, Module.Basis.repr_symm_apply, LinearEquiv.coe_coe