-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
lemma H1Cotangent.map_eq (f g : Hom P P') : map f = map g

Proof state:
case h.e.e
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra 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'
P : Extension R S
f g : P.Hom P'
x : P.H1Cotangent
⊢ (↑((map f) x)).val = (↑((map g) x)).val

Tactic:
simp only [map_apply_coe]

Result:
case h.e.e
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra 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'
P : Extension R S
f g : P.Hom P'
x : P.H1Cotangent
⊢ ((Cotangent.map f) ↑x).val = ((Cotangent.map g) ↑x).val

Proof state:
case h.e.e
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra 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'
P : Extension R S
f g : P.Hom P'
x : P.H1Cotangent
⊢ ((Cotangent.map f) ↑x).val = ((Cotangent.map g) ↑x).val

Tactic:
rw [← sub_eq_zero, ← Cotangent.val_sub, ← LinearMap.sub_apply, Cotangent.map_sub_map]

Result:
case h.e.e
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra 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'
P : Extension R S
f g : P.Hom P'
x : P.H1Cotangent
⊢ ((f.sub g ∘ₗ P.cotangentComplex) ↑x).val = 0

Proof state:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra 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'
P : Extension R S
f g : P.Hom P'
⊢ map f = map g

Tactic:
ext x

Result:
case h.e.e
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra 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'
P : Extension R S
f g : P.Hom P'
x : P.H1Cotangent
⊢ (↑((map f) x)).val = (↑((map g) x)).val

Proof state:
case h.e.e
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra 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'
P : Extension R S
f g : P.Hom P'
x : P.H1Cotangent
⊢ ((f.sub g ∘ₗ P.cotangentComplex) ↑x).val = 0

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.map_coe_ker, map_zero,
  Cotangent.val_zero]

Result:
no goals