-- 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
⊢ ∀ (m : pres.Ring) (x : pres.rels →₀ S),
    { toFun := ⇑(hom₁ pres), map_add' := ⋯ }.toFun (m • x) =
      (RingHom.id pres.Ring) m • { toFun := ⇑(hom₁ pres), map_add' := ⋯ }.toFun x

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' := ⋯ }
⊢ Function.Surjective ⇑(hom₁ pres)

Tactic:
change Function.Surjective φ

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 ⇑φ

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, ⋯⟩) = ⊤
⊢ ∀ m ∈ Set.range fun r => ⟨pres.relation r, ⋯⟩, Extension.Cotangent.mk m ∈ LinearMap.range φ

Tactic:
rintro _ ⟨r, rfl⟩

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 ((fun r => ⟨pres.relation r, ⋯⟩) 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' := ⋯ }
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 φ

Tactic:
rw [Submodule.map_span_le]

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, ⋯⟩) = ⊤
⊢ ∀ m ∈ Set.range fun r => ⟨pres.relation r, ⋯⟩, Extension.Cotangent.mk m ∈ 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' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
h₂ : Submodule.span pres.Ring (Set.range fun r => ⟨pres.relation r, ⋯⟩) = ⊤
⊢ Function.Surjective ⇑φ

Tactic:
rw [← LinearMap.range_eq_top] at 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, ⋯⟩) = ⊤
⊢ 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' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
r : pres.rels
⊢ pres.relation r ∈ pres.ker

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
⊢ Submodule.map (Submodule.subtype pres.ker) (Submodule.span pres.Ring (Set.range fun r => ⟨pres.relation r, ⋯⟩)) =
    Submodule.map (Submodule.subtype pres.ker) ⊤

Tactic:
rw [Submodule.map_top, Submodule.range_subtype, Submodule.map_span,
  Submodule.coe_subtype, Ideal.submodule_span_eq]

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
⊢ Ideal.span (Subtype.val '' Set.range fun r => ⟨pres.relation r, ⋯⟩) = pres.ker

Proof state:
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

Tactic:
aesop

Result:
no goals

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 ((fun r => ⟨pres.relation r, ⋯⟩) r) ∈ LinearMap.range φ

Tactic:
simp only [LinearMap.mem_range]

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
⊢ ∃ y, φ y = 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
⊢ Ideal.span (Subtype.val '' Set.range fun r => ⟨pres.relation r, ⋯⟩) = pres.ker

Tactic:
simp only [← pres.span_range_relation_eq_ker]

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
⊢ Ideal.span (Subtype.val '' Set.range fun r => ⟨pres.relation r, ⋯⟩) = Ideal.span (Set.range pres.relation)