-- Mathlib/Algebra/Module/Presentation/Differentials.lean
lemma surjective_hom₁ : Function.Surjective (hom₁ pres)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
⊢ Function.Surjective ⇑φ

Tactic:
have h₂ : Submodule.span pres.Ring
    (Set.range (fun r ↦ (⟨pres.relation r, by simp⟩ : pres.ker))) = ⊤ := by
  refine Submodule.map_injective_of_injective (f := Submodule.subtype pres.ker)
    Subtype.coe_injective ?_
  rw [Submodule.map_top, Submodule.range_subtype, Submodule.map_span,
    Submodule.coe_subtype, Ideal.submodule_span_eq]
  simp only [← pres.span_range_relation_eq_ker]
  congr
  aesop

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
h₂ : Submodule.span pres.Ring (Set.range fun r => ⟨pres.relation r, ⋯⟩) = ⊤
⊢ Function.Surjective ⇑φ

Proof state:
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : LinearMap.range Extension.Cotangent.mk = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r => ⟨pres.relation r, ⋯⟩) = ⊤
r : pres.rels
⊢ φ (Finsupp.single r 1) = Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩

Tactic:
simp only [LinearMap.coe_mk, AddHom.coe_mk, hom₁_single, φ]

Result:
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : LinearMap.range Extension.Cotangent.mk = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r => ⟨pres.relation r, ⋯⟩) = ⊤
r : pres.rels
⊢ Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩ = Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
⊢ Submodule.span pres.Ring (Set.range fun r => ⟨pres.relation r, ⋯⟩) = ⊤

Tactic:
refine Submodule.map_injective_of_injective (f := Submodule.subtype pres.ker)
  Subtype.coe_injective ?_

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
⊢ Submodule.map (Submodule.subtype pres.ker) (Submodule.span pres.Ring (Set.range fun r => ⟨pres.relation r, ⋯⟩)) =
    Submodule.map (Submodule.subtype pres.ker) ⊤

Proof state:
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : LinearMap.range Extension.Cotangent.mk = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r => ⟨pres.relation r, ⋯⟩) = ⊤
r : pres.rels
⊢ Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩ = Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
⊢ Function.Surjective ⇑(hom₁ pres)

Tactic:
let φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := hom₁ pres
    map_add' := by simp
    map_smul' := by simp }

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
⊢ Function.Surjective ⇑(hom₁ pres)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
⊢ ∀ (x y : pres.rels →₀ S), (hom₁ pres) (x + y) = (hom₁ pres) x + (hom₁ pres) y

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
⊢ Ideal.span (Subtype.val '' Set.range fun r => ⟨pres.relation r, ⋯⟩) = Ideal.span (Set.range pres.relation)

Tactic:
congr

Result:
case e_s
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
⊢ (Subtype.val '' Set.range fun r => ⟨pres.relation r, ⋯⟩) = Set.range pres.relation

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : LinearMap.range Extension.Cotangent.mk = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r => ⟨pres.relation r, ⋯⟩) = ⊤
⊢ LinearMap.range φ = ⊤

Tactic:
rw [← top_le_iff, ← h₁, LinearMap.range_eq_map, ← h₂]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : LinearMap.range Extension.Cotangent.mk = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r => ⟨pres.relation r, ⋯⟩) = ⊤
⊢ Submodule.map Extension.Cotangent.mk (Submodule.span pres.Ring (Set.range fun r => ⟨pres.relation r, ⋯⟩)) ≤
    LinearMap.range φ

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
⊢ Function.Surjective ⇑φ

Tactic:
have h₁ := Algebra.Extension.Cotangent.mk_surjective (P := pres.toExtension)

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
⊢ Function.Surjective ⇑φ

Proof state:
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : LinearMap.range Extension.Cotangent.mk = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r => ⟨pres.relation r, ⋯⟩) = ⊤
r : pres.rels
⊢ ∃ y, φ y = Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩

Tactic:
refine ⟨Finsupp.single r 1, ?_⟩

Result:
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
φ : (pres.rels →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
  { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : LinearMap.range Extension.Cotangent.mk = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r => ⟨pres.relation r, ⋯⟩) = ⊤
r : pres.rels
⊢ φ (Finsupp.single r 1) = Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩