-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
lemma CotangentSpace.map_sub_map (f g : Hom P P') :
    CotangentSpace.map f - CotangentSpace.map g =
      P'.cotangentComplex.restrictScalars S ∘ₗ (f.sub g)

Proof state:
case h.tmul.intro.zero
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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : S
⊢ (CotangentSpace.map f - CotangentSpace.map g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo 0) =
    (↑S P'.cotangentComplex ∘ₗ f.sub g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo 0)

Tactic:
simp only [map_zero, tmul_zero, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
Function.comp_apply]

Result:
no goals

Proof state:
case h.tmul.intro.tmul
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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : S
x✝ y✝ : P.Ring
⊢ (CotangentSpace.map f - CotangentSpace.map g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ ⊗ₜ[R] y✝)) =
    (↑S P'.cotangentComplex ∘ₗ f.sub g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ ⊗ₜ[R] y✝))

Tactic:
simp only [Derivation.tensorProductTo_tmul, tmul_smul, smul_tmul', LinearMap.sub_apply,
  map_tmul, Hom.toAlgHom_apply, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
  Function.comp_apply, Hom.sub_tmul, LinearMap.map_smul_of_tower, cotangentComplex_mk,
  Hom.subToKer_apply_coe, map_sub, ← algebraMap_eq_smul_one, tmul_sub, smul_sub]

Result:
no goals

Proof state:
case h.tmul.intro
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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : S
y : P.Ring ⊗[R] P.Ring
⊢ (CotangentSpace.map f - CotangentSpace.map g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo y) =
    (↑S P'.cotangentComplex ∘ₗ f.sub g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo y)

Tactic:
induction y with
| zero => simp only [map_zero, tmul_zero, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
    Function.comp_apply]
| add => simp only [map_add, tmul_add, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
  Function.comp_apply, *]
| tmul =>
  simp only [Derivation.tensorProductTo_tmul, tmul_smul, smul_tmul', LinearMap.sub_apply,
    map_tmul, Hom.toAlgHom_apply, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
    Function.comp_apply, Hom.sub_tmul, LinearMap.map_smul_of_tower, cotangentComplex_mk,
    Hom.subToKer_apply_coe, map_sub, ← algebraMap_eq_smul_one, tmul_sub, smul_sub]

Result:
no goals

Proof state:
case h.tmul
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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : S
y : Ω[P.Ring⁄R]
⊢ (CotangentSpace.map f - CotangentSpace.map g) (x ⊗ₜ[P.Ring] y) = (↑S P'.cotangentComplex ∘ₗ f.sub g) (x ⊗ₜ[P.Ring] y)

Tactic:
obtain ⟨y, rfl⟩ := KaehlerDifferential.tensorProductTo_surjective _ _ y

Result:
case h.tmul.intro
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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : S
y : P.Ring ⊗[R] P.Ring
⊢ (CotangentSpace.map f - CotangentSpace.map g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo y) =
    (↑S P'.cotangentComplex ∘ₗ f.sub g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo y)

Proof state:
case h.zero
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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
⊢ (CotangentSpace.map f - CotangentSpace.map g) 0 = (↑S P'.cotangentComplex ∘ₗ f.sub g) 0

Tactic:
simp only [map_zero, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply]

Result:
no goals

Proof state:
case h.tmul.intro.add
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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : S
x✝ y✝ : P.Ring ⊗[R] P.Ring
a✝¹ :
  (CotangentSpace.map f - CotangentSpace.map g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo x✝) =
    (↑S P'.cotangentComplex ∘ₗ f.sub g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo x✝)
a✝ :
  (CotangentSpace.map f - CotangentSpace.map g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo y✝) =
    (↑S P'.cotangentComplex ∘ₗ f.sub g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo y✝)
⊢ (CotangentSpace.map f - CotangentSpace.map g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ + y✝)) =
    (↑S P'.cotangentComplex ∘ₗ f.sub g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ + y✝))

Tactic:
simp only [map_add, tmul_add, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
Function.comp_apply, *]

Result:
no goals

Proof state:
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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
⊢ CotangentSpace.map f - CotangentSpace.map g = ↑S P'.cotangentComplex ∘ₗ f.sub g

Tactic:
ext x

Result:
case h
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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : P.CotangentSpace
⊢ (CotangentSpace.map f - CotangentSpace.map g) x = (↑S P'.cotangentComplex ∘ₗ f.sub g) x