-- Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean
@[ext]
lemma ext {M : ModuleCat B} {α β : KaehlerDifferential f ⟶ M}
    (h : ∀ (b : B), α (d b) = β (d b)) : α = β

Proof state:
case intro
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
y : ↑B
⊢ (_root_.KaehlerDifferential.D ↑A ↑B) y ∈ ↑(LinearMap.ker (ModuleCat.Hom.hom (α - β)))

Tactic:
rw [SetLike.mem_coe, LinearMap.mem_ker, ModuleCat.hom_sub, LinearMap.sub_apply, sub_eq_zero]

Result:
case intro
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
y : ↑B
⊢ (ModuleCat.Hom.hom α) ((_root_.KaehlerDifferential.D ↑A ↑B) y) =
    (ModuleCat.Hom.hom β) ((_root_.KaehlerDifferential.D ↑A ↑B) y)

Proof state:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
⊢ α = β

Tactic:
rw [← sub_eq_zero]

Result:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
⊢ α - β = 0

Proof state:
case hf
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
this : ModuleCat.Hom.hom (α - β) = 0
⊢ ModuleCat.Hom.hom (α - β) = ModuleCat.Hom.hom 0

Tactic:
exact this

Result:
no goals

Proof state:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
⊢ Set.range ⇑(_root_.KaehlerDifferential.D ↑A ↑B) ⊆ ↑(LinearMap.ker (ModuleCat.Hom.hom (α - β)))

Tactic:
rintro _ ⟨y, rfl⟩

Result:
case intro
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
y : ↑B
⊢ (_root_.KaehlerDifferential.D ↑A ↑B) y ∈ ↑(LinearMap.ker (ModuleCat.Hom.hom (α - β)))

Proof state:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
this : ModuleCat.Hom.hom (α - β) = 0
⊢ α - β = 0

Tactic:
ext : 1

Result:
case hf
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
this : ModuleCat.Hom.hom (α - β) = 0
⊢ ModuleCat.Hom.hom (α - β) = ModuleCat.Hom.hom 0

Proof state:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
this : ⊤ ≤ LinearMap.ker (ModuleCat.Hom.hom (α - β))
⊢ α - β = 0

Tactic:
rw [top_le_iff, LinearMap.ker_eq_top] at this

Result:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
this : ModuleCat.Hom.hom (α - β) = 0
⊢ α - β = 0

Proof state:
case intro
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
y : ↑B
⊢ (ModuleCat.Hom.hom α) ((_root_.KaehlerDifferential.D ↑A ↑B) y) =
    (ModuleCat.Hom.hom β) ((_root_.KaehlerDifferential.D ↑A ↑B) y)

Tactic:
apply h

Result:
no goals

Proof state:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
⊢ α - β = 0

Tactic:
have : ⊤ ≤ LinearMap.ker (α - β).hom := by
  rw [← KaehlerDifferential.span_range_derivation, Submodule.span_le]
  rintro _ ⟨y, rfl⟩
  rw [SetLike.mem_coe, LinearMap.mem_ker, ModuleCat.hom_sub, LinearMap.sub_apply, sub_eq_zero]
  apply h

Result:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
this : ⊤ ≤ LinearMap.ker (ModuleCat.Hom.hom (α - β))
⊢ α - β = 0

Proof state:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
⊢ ⊤ ≤ LinearMap.ker (ModuleCat.Hom.hom (α - β))

Tactic:
rw [← KaehlerDifferential.span_range_derivation, Submodule.span_le]

Result:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
⊢ Set.range ⇑(_root_.KaehlerDifferential.D ↑A ↑B) ⊆ ↑(LinearMap.ker (ModuleCat.Hom.hom (α - β)))