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 σ
i : σ
j : ι ⊕ σ
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)
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.inr j) :
        T)
      ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι ⊕ σ) R) → T)
          (Pi.single (M := fun (x : ι ⊕ σ) ↦ MvPolynomial (ι ⊕ σ) R) (Sum.inr j)
              (1 : (fun (x : ι ⊕ σ) ↦ MvPolynomial (ι ⊕ σ) R) (Sum.inr j)) (Sum.inr i) :
            MvPolynomial (ι ⊕ σ) R) :
        T)
⊢ 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:
obtain (j | j) := 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 : ι
⊢ 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:
simp only [Basis.prod_repr_inr, Basis.baseChange_repr_tmul,
      Basis.repr_self, Basis.prod_repr_inl, map_zero, Finsupp.coe_zero,
      Pi.zero_apply, ne_eq, not_false_eq_true, Pi.single_eq_of_ne, Pi.single_apply,
      Finsupp.single_apply, ite_smul, one_smul, zero_smul, Sum.inr.injEq,
      MonoidWithZeroHom.map_ite_one_zero, reduceCtorEq]

Premises used: reduceCtorEq, Module.Basis.prod_repr_inl, Sum.inr.injEq, Pi.single_apply, Pi.zero_apply, map_zero, Pi.single_eq_of_ne, ne_eq, one_smul, zero_smul, MonoidWithZeroHom.map_ite_one_zero, Module.Basis.baseChange_repr_tmul, Finsupp.single_apply, ite_smul, Module.Basis.prod_repr_inr, not_false_eq_true, Module.Basis.repr_self, Finsupp.coe_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 σ
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)
        (Sum.inr j) :
      T)
    ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι ⊕ σ) R) → T)
        (Pi.single (M := fun (x : ι ⊕ σ) ↦ MvPolynomial (ι ⊕ σ) R) (Sum.inr j)
            (1 : (fun (x : ι ⊕ σ) ↦ MvPolynomial (ι ⊕ σ) R) (Sum.inr j)) (Sum.inr i) :
          MvPolynomial (ι ⊕ σ) R) :
      T)

Tactic:
simp only [Basis.prod_repr_inr, Basis.baseChange_repr_tmul,
      Basis.repr_self, Basis.prod_repr_inl, map_zero, Finsupp.coe_zero,
      Pi.zero_apply, ne_eq, not_false_eq_true, Pi.single_eq_of_ne, Pi.single_apply,
      Finsupp.single_apply, ite_smul, one_smul, zero_smul, Sum.inr.injEq,
      MonoidWithZeroHom.map_ite_one_zero, reduceCtorEq]

Premises used: reduceCtorEq, Module.Basis.prod_repr_inl, Sum.inr.injEq, Pi.single_apply, Pi.zero_apply, map_zero, Pi.single_eq_of_ne, ne_eq, one_smul, zero_smul, MonoidWithZeroHom.map_ite_one_zero, Module.Basis.baseChange_repr_tmul, Finsupp.single_apply, ite_smul, Module.Basis.prod_repr_inr, not_false_eq_true, Module.Basis.repr_self, Finsupp.coe_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 : T ⊗[S] P.toExtension.CotangentSpace
⊢ Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)))
    ((LinearEquiv.symm (compEquiv Q P) :
          (a : Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) →
            (Q.comp P).toExtension.CotangentSpace)
        (0, x) :
      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)
        x :
      Extension.CotangentSpace (toExtension (Q.comp P)))

Tactic:
DFunLike.congr_fun (compEquiv_symm_inr Q P) x

Premises used: DFunLike.congr_fun, Algebra.Generators.CotangentSpace.compEquiv_symm_inr, Function.prod
-- 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 (α := Q.toExtension.CotangentSpace)
      ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
              (↑(compEquiv Q P) :
                (Q.comp P).toExtension.CotangentSpace →ₗ[T]
                  Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) :
            (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
          ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i) :
        Q.toExtension.CotangentSpace)
      ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) :
            (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
          ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i) :
        Q.toExtension.CotangentSpace)
⊢ Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)) →ₗ[T] Q.toExtension.CotangentSpace)
    (LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
      (↑(compEquiv Q P) :
        (Q.comp P).toExtension.CotangentSpace →ₗ[T] Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace))
    (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)))

Tactic:
apply (Q.comp P).cotangentSpaceBasis.ext

Premises used: Algebra.Generators.comp, Algebra.Generators.cotangentSpaceBasis, 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)
    ((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
        ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
              (↑(compEquiv Q P) :
                (Q.comp P).toExtension.CotangentSpace →ₗ[T]
                  Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) :
            (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
          ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i)) :
      ι →₀ T)
    ((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
        ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) :
            (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
          ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i)) :
      ι →₀ T)
⊢ Eq (α := Q.toExtension.CotangentSpace)
    ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
            (↑(compEquiv Q P) :
              (Q.comp P).toExtension.CotangentSpace →ₗ[T]
                Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) :
          (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
        ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i) :
      Q.toExtension.CotangentSpace)
    ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
        ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i) :
      Q.toExtension.CotangentSpace)

Tactic:
apply Q.cotangentSpaceBasis.repr.injective

Premises used: 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)
      ((((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
                ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
                      (↑(compEquiv Q P) :
                        (Q.comp P).toExtension.CotangentSpace →ₗ[T]
                          Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) :
                    (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
                  ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i)) :
              ι →₀ T) :
            (a : ι) → T)
          j :
        T)
      ((((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
                ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) :
                    (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
                  ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i)) :
              ι →₀ T) :
            (a : ι) → T)
          j :
        T)
⊢ Eq (α := ι →₀ T)
    ((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
        ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
              (↑(compEquiv Q P) :
                (Q.comp P).toExtension.CotangentSpace →ₗ[T]
                  Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) :
            (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
          ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i)) :
      ι →₀ T)
    ((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
        ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) :
            (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
          ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp 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)
    (((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
            ((LinearEquiv.symm (Basis.repr (Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis))) :
                  (a : ι ⊕ σ →₀ T) → Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
                (Finsupp.single i 1)).1 :
          (a : ι) → T)
        j :
      T)
    ((aeval Q.val : (a : MvPolynomial ι S) → T)
        ((pderiv j : (a : MvPolynomial ι S) → MvPolynomial ι S)
            (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι S) ∘ P.val) i) :
          MvPolynomial ι S) :
      T)
⊢ Eq.{u₃ + 1} (α := T)
    ((((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
              ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
                    (↑(compEquiv Q P) :
                      (Q.comp P).toExtension.CotangentSpace →ₗ[T]
                        Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) :
                  (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
                ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i)) :
            ι →₀ T) :
          (a : ι) → T)
        j :
      T)
    ((((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
              ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) :
                  (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
                ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i)) :
            ι →₀ T) :
          (a : ι) → T)
        j :
      T)

Tactic:
simp only [compEquiv, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ofComp_val,
    LinearEquiv.trans_apply, Basis.repr_self, LinearMap.fst_apply, repr_CotangentSpaceMap]

Premises used: Algebra.Generators.CotangentSpace.compEquiv, Algebra.Generators.ofComp_val, LinearEquiv.trans_apply, LinearMap.fst_apply, LinearMap.coe_comp, Algebra.Generators.repr_CotangentSpaceMap, Function.comp_apply, Module.Basis.repr_self, LinearEquiv.coe_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 σ
i : ι ⊕ σ
j : ι
a :
  ∀ (i : ι),
    Eq.{u₃ + 1} (α := T)
      (((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
              ((LinearEquiv.symm (Basis.repr (Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis))) :
                    (a : ι ⊕ σ →₀ T) → Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
                  (Finsupp.single (Sum.inl i) 1)).1 :
            (a : ι) → T)
          j :
        T)
      ((aeval Q.val : (a : MvPolynomial ι S) → T)
          ((pderiv j : (a : MvPolynomial ι S) → MvPolynomial ι S)
              (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι S) ∘ P.val) (Sum.inl i)) :
            MvPolynomial ι S) :
        T)
a₁ :
  ∀ (i : σ),
    Eq.{u₃ + 1} (α := T)
      (((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
              ((LinearEquiv.symm (Basis.repr (Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis))) :
                    (a : ι ⊕ σ →₀ T) → Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
                  (Finsupp.single (Sum.inr i) 1)).1 :
            (a : ι) → T)
          j :
        T)
      ((aeval Q.val : (a : MvPolynomial ι S) → T)
          ((pderiv j : (a : MvPolynomial ι S) → MvPolynomial ι S)
              (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι S) ∘ P.val) (Sum.inr i)) :
            MvPolynomial ι S) :
        T)
⊢ Eq.{u₃ + 1} (α := T)
    (((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
            ((LinearEquiv.symm (Basis.repr (Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis))) :
                  (a : ι ⊕ σ →₀ T) → Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
                (Finsupp.single i 1)).1 :
          (a : ι) → T)
        j :
      T)
    ((aeval Q.val : (a : MvPolynomial ι S) → T)
        ((pderiv j : (a : MvPolynomial ι S) → MvPolynomial ι S)
            (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι S) ∘ P.val) i) :
          MvPolynomial ι S) :
      T)

Tactic:
obtain (i | i) := i
-- 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 σ
j i : ι
⊢ Eq.{u₃ + 1} (α := T)
    (((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
            ((LinearEquiv.symm (Basis.repr (Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis))) :
                  (a : ι ⊕ σ →₀ T) → Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
                (Finsupp.single (Sum.inl i) 1)).1 :
          (a : ι) → T)
        j :
      T)
    ((aeval Q.val : (a : MvPolynomial ι S) → T)
        ((pderiv j : (a : MvPolynomial ι S) → MvPolynomial ι S)
            (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι S) ∘ P.val) (Sum.inl i)) :
          MvPolynomial ι S) :
      T)

Tactic:
simp only [Basis.repr_symm_apply, Finsupp.linearCombination_single, Basis.prod_apply,
      LinearMap.coe_inl, LinearMap.coe_inr, Sum.elim_inl, Function.comp_apply, one_smul,
      Basis.repr_self, Finsupp.single_apply, pderiv_X, Pi.single_apply,
      Sum.elim_inr, Function.comp_apply, Basis.baseChange_apply, one_smul,
      MonoidWithZeroHom.map_ite_one_zero, map_zero, Finsupp.coe_zero, Pi.zero_apply, derivation_C]

Premises used: LinearMap.coe_inr, Pi.single_apply, MvPolynomial.pderiv_X, Pi.zero_apply, map_zero, Module.Basis.prod_apply, Module.Basis.baseChange_apply, MvPolynomial.derivation_C, Finsupp.linearCombination_single, one_smul, Sum.elim_inr, LinearMap.coe_inl, MonoidWithZeroHom.map_ite_one_zero, Sum.elim_inl, Finsupp.single_apply, Function.comp_apply, Module.Basis.repr_symm_apply, Module.Basis.repr_self, Finsupp.coe_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 σ
j : ι
i : σ
⊢ Eq.{u₃ + 1} (α := T)
    (((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
            ((LinearEquiv.symm (Basis.repr (Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis))) :
                  (a : ι ⊕ σ →₀ T) → Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
                (Finsupp.single (Sum.inr i) 1)).1 :
          (a : ι) → T)
        j :
      T)
    ((aeval Q.val : (a : MvPolynomial ι S) → T)
        ((pderiv j : (a : MvPolynomial ι S) → MvPolynomial ι S)
            (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι S) ∘ P.val) (Sum.inr i)) :
          MvPolynomial ι S) :
      T)

Tactic:
simp only [Basis.repr_symm_apply, Finsupp.linearCombination_single, Basis.prod_apply,
      LinearMap.coe_inl, LinearMap.coe_inr, Sum.elim_inl, Function.comp_apply, one_smul,
      Basis.repr_self, Finsupp.single_apply, pderiv_X, Pi.single_apply,
      Sum.elim_inr, Function.comp_apply, Basis.baseChange_apply, one_smul,
      MonoidWithZeroHom.map_ite_one_zero, map_zero, Finsupp.coe_zero, Pi.zero_apply, derivation_C]

Premises used: LinearMap.coe_inr, Pi.single_apply, MvPolynomial.pderiv_X, Pi.zero_apply, map_zero, Module.Basis.prod_apply, Module.Basis.baseChange_apply, MvPolynomial.derivation_C, Finsupp.linearCombination_single, one_smul, Sum.elim_inr, LinearMap.coe_inl, MonoidWithZeroHom.map_ite_one_zero, Sum.elim_inl, Finsupp.single_apply, Function.comp_apply, Module.Basis.repr_symm_apply, Module.Basis.repr_self, Finsupp.coe_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.CotangentSpace (toExtension (Q.comp P))
⊢ Eq (α := Q.toExtension.CotangentSpace)
    (((compEquiv Q P :
            (a : (Q.comp P).toExtension.CotangentSpace) →
              Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
          x).1 :
      Q.toExtension.CotangentSpace)
    ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
        x :
      Q.toExtension.CotangentSpace)

Tactic:
DFunLike.congr_fun (fst_compEquiv Q P) x

Premises used: DFunLike.congr_fun, Algebra.Generators.CotangentSpace.fst_compEquiv
-- 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 σ
rw :
  Function.Injective (α := T ⊗[S] P.toExtension.CotangentSpace) (β := 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)
⊢ Function.Injective (α := T ⊗[S] P.toExtension.CotangentSpace) (β := 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)

Tactic:
rw [← compEquiv_symm_inr]

Premises used: Algebra.Generators.CotangentSpace.compEquiv_symm_inr