-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma CotangentSpace.compEquiv_symm_inr :
    (compEquiv Q P).symm.toLinearMap ∘ₗ
      LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) =
        (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom).liftBaseChange T

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ ∀ (i : P.vars),
    (↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
        ((Basis.baseChange T P.cotangentSpaceBasis) i) =
      (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
        ((Basis.baseChange T P.cotangentSpaceBasis) i)

Tactic:
intro i

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : P.vars
⊢ (↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
      ((Basis.baseChange T P.cotangentSpaceBasis) i) =
    (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
      ((Basis.baseChange T P.cotangentSpaceBasis) i)

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : P.vars
⊢ (↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
      ((Basis.baseChange T P.cotangentSpaceBasis) i) =
    (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
      ((Basis.baseChange T P.cotangentSpaceBasis) i)

Tactic:
apply (Q.comp P).cotangentSpaceBasis.repr.injective

Result:
case a
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : P.vars
⊢ (Q.comp P).cotangentSpaceBasis.repr
      ((↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
        ((Basis.baseChange T P.cotangentSpaceBasis) i)) =
    (Q.comp P).cotangentSpaceBasis.repr
      ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
        ((Basis.baseChange T P.cotangentSpaceBasis) i))

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ ↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) =
    LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)

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

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ ∀ (i : P.vars),
    (↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
        ((Basis.baseChange T P.cotangentSpaceBasis) i) =
      (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
        ((Basis.baseChange T P.cotangentSpaceBasis) i)

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ ↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) =
    LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)

Tactic:
classical
apply (P.cotangentSpaceBasis.baseChange T).ext
intro i
apply (Q.comp P).cotangentSpaceBasis.repr.injective
ext j
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]
obtain (j | j) := j <;>
  simp only [comp_vars, 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,
      RingHom.map_ite_one_zero, reduceCtorEq, ↓reduceIte]

Result:
no goals

Proof state:
case a.h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : P.vars
j : (Q.comp P).vars
⊢ ((Q.comp P).cotangentSpaceBasis.repr
        ((↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
          ((Basis.baseChange T P.cotangentSpaceBasis) i)))
      j =
    ((Q.comp P).cotangentSpaceBasis.repr
        ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
          ((Basis.baseChange T P.cotangentSpaceBasis) i)))
      j

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]

Result:
case a.h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : P.vars
j : (Q.comp P).vars
⊢ ((Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis)).repr (0, 1 ⊗ₜ[S] P.cotangentSpaceBasis i))
      j =
    (aeval (Q.comp P).val) (Pi.single j 1 (Sum.inr i))

Proof state:
case a.h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : P.vars
j : (Q.comp P).vars
⊢ ((Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis)).repr (0, 1 ⊗ₜ[S] P.cotangentSpaceBasis i))
      j =
    (aeval (Q.comp P).val) (Pi.single j 1 (Sum.inr i))

Tactic:
obtain (j | j) := j <;>
  simp only [comp_vars, 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,
      RingHom.map_ite_one_zero, reduceCtorEq, ↓reduceIte]

Result:
no goals