Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝²⁰ : CommRing R'
inst✝¹⁹ : CommRing S'
inst✝¹⁸ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁷ : Algebra R R'
inst✝¹⁶ : Algebra S S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹⁰ : Algebra R R''
inst✝⁹ : Algebra S S''
inst✝⁸ : Algebra R S''
inst✝⁷ : IsScalarTower R R'' S''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
this✝³ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
this✝² : IsScalarTower P.Ring S S'
this✝¹ : Algebra P.Ring P'.Ring := f.toAlgHom.toAlgebra
this✝ : IsScalarTower P.Ring P'.Ring S'
this : IsScalarTower R P.Ring S'
⊢ (↑R Cotangent.mk ∘ₗ f.subToKer g) 1 = 0

pp: case refine_2
R : Type u
S : Type v
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝²⁰ : CommRing R'
inst✝¹⁹ : CommRing S'
inst✝¹⁸ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁷ : Algebra R R'
inst✝¹⁶ : Algebra S S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹⁰ : Algebra R R''
inst✝⁹ : Algebra S S''
inst✝⁸ : Algebra R S''
inst✝⁷ : IsScalarTower R R'' S''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
this✝³ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
this✝² : IsScalarTower P.Ring S S'
this✝¹ : Algebra P.Ring P'.Ring := f.toAlgHom.toAlgebra
this✝ : IsScalarTower P.Ring P'.Ring S'
this : IsScalarTower R P.Ring S'
⊢ ∀ (a b : P.Ring),
    (↑R Cotangent.mk ∘ₗ f.subToKer g) (a * b) =
      a • (↑R Cotangent.mk ∘ₗ f.subToKer g) b + b • (↑R Cotangent.mk ∘ₗ f.subToKer g) a

Tactic:
· ext
    simp [Ideal.toCotangent_eq_zero]

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝²⁰ : CommRing R'
inst✝¹⁹ : CommRing S'
inst✝¹⁸ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁷ : Algebra R R'
inst✝¹⁶ : Algebra S S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹⁰ : Algebra R R''
inst✝⁹ : Algebra S S''
inst✝⁸ : Algebra R S''
inst✝⁷ : IsScalarTower R R'' S''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
this✝³ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
this✝² : IsScalarTower P.Ring S S'
this✝¹ : Algebra P.Ring P'.Ring := f.toAlgHom.toAlgebra
this✝ : IsScalarTower P.Ring P'.Ring S'
this : IsScalarTower R P.Ring S'
⊢ ∀ (a b : P.Ring),
    (↑R Cotangent.mk ∘ₗ f.subToKer g) (a * b) =
      a • (↑R Cotangent.mk ∘ₗ f.subToKer g) b + b • (↑R Cotangent.mk ∘ₗ f.subToKer g) a