-- Mathlib/Algebra/Module/Presentation/Differentials.lean
lemma differentialsSolution_isPresentation :
    pres.differentialsSolution.IsPresentation

Proof state:
case right
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
⊢ LinearMap.ker pres.differentialsSolution.π = Submodule.span S (Set.range pres.differentialsRelations.relation)

Tactic:
rw [← Module.Relations.range_map]

Result:
case right
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
⊢ LinearMap.ker pres.differentialsSolution.π = LinearMap.range pres.differentialsRelations.map

Proof state:
case left
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
⊢ Function.Surjective ⇑(pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm)

Tactic:
exact Extension.toKaehler_surjective.comp pres.cotangentSpaceBasis.repr.symm.surjective

Result:
no goals

Proof state:
case right
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
⊢ LinearMap.ker pres.differentialsSolution.π = LinearMap.range pres.differentialsRelations.map

Tactic:
exact Function.Exact.linearMap_ker_eq
  ((LinearMap.exact_iff_of_surjective_of_bijective_of_injective
  _ _ _ _ (hom₁ pres)
  pres.cotangentSpaceBasis.repr.symm.toLinearMap .id
  (comm₁₂ pres) (by simpa using comm₂₃ pres) (surjective_hom₁ pres)
    (LinearEquiv.bijective _) (Equiv.refl _).injective).2
    pres.toExtension.exact_cotangentComplex_toKaehler)

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
⊢ Submodule.span S (Set.range pres.differentialsSolution.var) = ⊤ ∧
    LinearMap.ker pres.differentialsSolution.π = Submodule.span S (Set.range pres.differentialsRelations.relation)

Tactic:
constructor

Result:
case left
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
⊢ Submodule.span S (Set.range pres.differentialsSolution.var) = ⊤

case right
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
⊢ LinearMap.ker pres.differentialsSolution.π = Submodule.span S (Set.range pres.differentialsRelations.relation)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
⊢ pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm = LinearMap.id ∘ₗ pres.differentialsSolution.π

Tactic:
simpa using comm₂₃ pres

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.differentialsSolution.IsPresentation

Tactic:
rw [Module.Relations.Solution.isPresentation_iff]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
⊢ Submodule.span S (Set.range pres.differentialsSolution.var) = ⊤ ∧
    LinearMap.ker pres.differentialsSolution.π = Submodule.span S (Set.range pres.differentialsRelations.relation)

Proof state:
case left
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
⊢ Submodule.span S (Set.range pres.differentialsSolution.var) = ⊤

Tactic:
rw [← Module.Relations.Solution.surjective_π_iff_span_eq_top, ← comm₂₃]

Result:
case left
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
⊢ Function.Surjective ⇑(pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm)