awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (hypothesis)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
φ : LinearMap (R := pres.Ring) (RingHom.id pres.Ring) (σ →₀ S) pres.toExtension.Cotangent :=
  { toFun := (⇑(hom₁ pres) : (a : σ →₀ S) → pres.toExtension.Cotangent), map_add' := ⋯, map_smul' := ⋯ }
h₁ :
  Function.Surjective (α := ↥pres.toExtension.ker) (β := pres.toExtension.Cotangent)
    (⇑Extension.Cotangent.mk : (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
⊢ Function.Surjective (α := σ →₀ S) (β := pres.toExtension.Cotangent) (⇑φ : (a : σ →₀ S) → pres.toExtension.Cotangent)
have h₂ : Eq (α := Submodule pres.Ring ↥pres.ker)
  (Submodule.span pres.Ring
    (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) sorry))
  ⊤
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
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
φ : LinearMap (R := pres.Ring) (RingHom.id pres.Ring) (σ →₀ S) pres.toExtension.Cotangent :=
  { toFun := (⇑(hom₁ pres) : (a : σ →₀ S) → pres.toExtension.Cotangent), map_add' := ⋯, map_smul' := ⋯ }
h₁ :
  Function.Surjective (α := ↥pres.toExtension.ker) (β := pres.toExtension.Cotangent)
    (⇑Extension.Cotangent.mk : (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
h₂ :
  Eq (α := Submodule pres.Ring ↥pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
    ⊤
⊢ Function.Surjective (α := σ →₀ S) (β := pres.toExtension.Cotangent) (⇑φ : (a : σ →₀ S) → pres.toExtension.Cotangent)
have rw : ∀ (h₁ : Eq (α := Submodule pres.toExtension.Ring pres.toExtension.Cotangent) (LinearMap.range Extension.Cotangent.mk) ⊤)
  (h₂ :
    Eq (α := Submodule pres.Ring ↥pres.ker)
      (Submodule.span pres.Ring
        (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) sorry))
      ⊤),
  φ.range = ⊤
Tactic: rw [← LinearMap.range_eq_top] at h₁ ⊢
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
φ : LinearMap (R := pres.Ring) (RingHom.id pres.Ring) (σ →₀ S) pres.toExtension.Cotangent :=
  { toFun := (⇑(hom₁ pres) : (a : σ →₀ S) → pres.toExtension.Cotangent), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Eq (α := Submodule pres.toExtension.Ring pres.toExtension.Cotangent) (LinearMap.range Extension.Cotangent.mk) ⊤
h₂ :
  Eq (α := Submodule pres.Ring ↥pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
    ⊤
⊢ φ.range = ⊤
have rw : Submodule.map Extension.Cotangent.mk
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) sorry)) ≤
  φ.range
Tactic: rw [← top_le_iff, ← h₁, LinearMap.range_eq_map, ← h₂]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
φ : LinearMap (R := pres.Ring) (RingHom.id pres.Ring) (σ →₀ S) pres.toExtension.Cotangent :=
  { toFun := (⇑(hom₁ pres) : (a : σ →₀ S) → pres.toExtension.Cotangent), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Eq (α := Submodule pres.toExtension.Ring pres.toExtension.Cotangent) (LinearMap.range Extension.Cotangent.mk) ⊤
h₂ :
  Eq (α := Submodule pres.Ring ↥pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
    ⊤
⊢ Submodule.map (R := pres.Ring) (M := ↥pres.toExtension.ker) (σ₁₂ := RingHom.id pres.Ring) Extension.Cotangent.mk
      (Submodule.span pres.Ring
        (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯)) ≤
    φ.range
have rw : ∀ (m : ↥pres.toExtension.ker),
  Membership.mem (γ := Set ↥pres.toExtension.ker)
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) sorry) m →
    Membership.mem (α := pres.toExtension.Cotangent) φ.range
      (((Extension.Cotangent.mk :
              LinearMap (R := pres.toExtension.Ring) (RingHom.id pres.toExtension.Ring) (↥pres.toExtension.ker)
                pres.toExtension.Cotangent) :
            (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
          m :
        pres.toExtension.Cotangent)
Tactic: rw [Submodule.map_span_le]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
φ : LinearMap (R := pres.Ring) (RingHom.id pres.Ring) (σ →₀ S) pres.toExtension.Cotangent :=
  { toFun := (⇑(hom₁ pres) : (a : σ →₀ S) → pres.toExtension.Cotangent), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Eq (α := Submodule pres.toExtension.Ring pres.toExtension.Cotangent) (LinearMap.range Extension.Cotangent.mk) ⊤
h₂ :
  Eq (α := Submodule pres.Ring ↥pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
    ⊤
r : σ
⊢ ∃ (y : σ →₀ S),
    Eq (α := pres.toExtension.Cotangent)
      ((φ : (a : σ →₀ S) → pres.toExtension.Cotangent) y : pres.toExtension.Cotangent)
      (((Extension.Cotangent.mk :
              LinearMap (R := pres.toExtension.Ring) (RingHom.id pres.toExtension.Ring) (↥pres.toExtension.ker)
                pres.toExtension.Cotangent) :
            (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯) :
        pres.toExtension.Cotangent)
have refine : Eq (α := pres.toExtension.Cotangent)
  ((φ : (a : σ →₀ S) → pres.toExtension.Cotangent) (Finsupp.single r 1) : pres.toExtension.Cotangent)
  (((Extension.Cotangent.mk :
          LinearMap (R := pres.toExtension.Ring) (RingHom.id pres.toExtension.Ring) (↥pres.toExtension.ker)
            pres.toExtension.Cotangent) :
        (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
      (Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) sorry) :
    pres.toExtension.Cotangent)
Tactic: refine ⟨Finsupp.single r 1, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
φ : LinearMap (R := pres.Ring) (RingHom.id pres.Ring) (σ →₀ S) pres.toExtension.Cotangent :=
  { toFun := (⇑(hom₁ pres) : (a : σ →₀ S) → pres.toExtension.Cotangent), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Eq (α := Submodule pres.toExtension.Ring pres.toExtension.Cotangent) (LinearMap.range Extension.Cotangent.mk) ⊤
h₂ :
  Eq (α := Submodule pres.Ring ↥pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
    ⊤
r : σ
⊢ Eq (α := pres.toExtension.Cotangent)
    ((φ : (a : σ →₀ S) → pres.toExtension.Cotangent) (Finsupp.single r 1) : pres.toExtension.Cotangent)
    (((Extension.Cotangent.mk :
            LinearMap (R := pres.toExtension.Ring) (RingHom.id pres.toExtension.Ring) (↥pres.toExtension.ker)
              pres.toExtension.Cotangent) :
          (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯) :
      pres.toExtension.Cotangent)
have simp : Eq (α := pres.toExtension.Cotangent)
  ((Extension.Cotangent.mk : (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
      (Subtype.mk (p := fun (x : pres.toExtension.Ring) ↦ x ∈ pres.toExtension.ker) (pres.relation r) sorry) :
    pres.toExtension.Cotangent)
  (((Extension.Cotangent.mk :
          LinearMap (R := pres.toExtension.Ring) (RingHom.id pres.toExtension.Ring) (↥pres.toExtension.ker)
            pres.toExtension.Cotangent) :
        (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
      (Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) sorry) :
    pres.toExtension.Cotangent)
Tactic: simp only [LinearMap.coe_mk, AddHom.coe_mk, hom₁_single, φ]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
r : σ
⊢ Eq (α := pres.toExtension.CotangentSpace)
    ((pres.toExtension.cotangentComplex : (a : pres.toExtension.Cotangent) → pres.toExtension.CotangentSpace)
        ((hom₁ pres : (a : σ →₀ S) → pres.toExtension.Cotangent) (Finsupp.single r 1)) :
      pres.toExtension.CotangentSpace)
    ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
        (pres.differentialsRelations.relation r) :
      pres.toExtension.CotangentSpace)
have simp : Eq (α := pres.toExtension.CotangentSpace)
  (1 ⊗ₜ[pres.toExtension.Ring]
      (D R pres.toExtension.Ring : (a : pres.toExtension.Ring) → Ω[pres.toExtension.Ring⁄R]) (pres.relation r) :
    TensorProduct pres.toExtension.Ring S Ω[pres.toExtension.Ring⁄R])
  ((Finsupp.linearCombination S (⇑pres.cotangentSpaceBasis : (a : ι) → pres.toExtension.CotangentSpace) :
        (a : ι →₀ S) → pres.toExtension.CotangentSpace)
      (Finsupp.mapRange (⇑(algebraMap pres.Ring S) : (a : pres.Ring) → S) sorry
        ((Basis.repr (mvPolynomialBasis R ι) : (a : Ω[MvPolynomial ι R⁄R]) → ι →₀ MvPolynomial ι R)
          ((D R (MvPolynomial ι R) : (a : MvPolynomial ι R) → Ω[MvPolynomial ι R⁄R]) (pres.relation r)))) :
    pres.toExtension.CotangentSpace)
Tactic: simp only [hom₁, Finsupp.linearCombination_single, one_smul, differentialsRelations,
    Basis.repr_symm_apply, Extension.cotangentComplex_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
r : σ
⊢ Eq (α := ι →₀ S)
    ((pres.cotangentSpaceBasis.repr : (a : pres.toExtension.CotangentSpace) → ι →₀ S)
        (1 ⊗ₜ[pres.toExtension.Ring]
          (D R pres.toExtension.Ring : (a : pres.toExtension.Ring) → Ω[pres.toExtension.Ring⁄R]) (pres.relation r)) :
      ι →₀ S)
    ((pres.cotangentSpaceBasis.repr : (a : pres.toExtension.CotangentSpace) → ι →₀ S)
        ((Finsupp.linearCombination S (⇑pres.cotangentSpaceBasis : (a : ι) → pres.toExtension.CotangentSpace) :
            (a : ι →₀ S) → pres.toExtension.CotangentSpace)
          (Finsupp.mapRange (⇑(algebraMap pres.Ring S) : (a : pres.Ring) → S) ⋯
            ((Basis.repr (mvPolynomialBasis R ι) : (a : Ω[MvPolynomial ι R⁄R]) → ι →₀ MvPolynomial ι R)
              ((D R (MvPolynomial ι R) : (a : MvPolynomial ι R) → Ω[MvPolynomial ι R⁄R]) (pres.relation r))))) :
      ι →₀ S)
have h : ∀ (a : ι),
  Eq.{v + 1} (α := S)
    ((((pres.cotangentSpaceBasis.repr : (a : pres.toExtension.CotangentSpace) → ι →₀ S)
              (1 ⊗ₜ[pres.toExtension.Ring]
                (D R pres.toExtension.Ring : (a : pres.toExtension.Ring) → Ω[pres.toExtension.Ring⁄R])
                  (pres.relation r)) :
            ι →₀ S) :
          (a : ι) → S)
        a :
      S)
    ((((pres.cotangentSpaceBasis.repr : (a : pres.toExtension.CotangentSpace) → ι →₀ S)
              ((Finsupp.linearCombination S (⇑pres.cotangentSpaceBasis : (a : ι) → pres.toExtension.CotangentSpace) :
                  (a : ι →₀ S) → pres.toExtension.CotangentSpace)
                (Finsupp.mapRange (⇑(algebraMap pres.Ring S) : (a : pres.Ring) → S) sorry
                  ((Basis.repr (mvPolynomialBasis R ι) : (a : Ω[MvPolynomial ι R⁄R]) → ι →₀ MvPolynomial ι R)
                    ((D R (MvPolynomial ι R) : (a : MvPolynomial ι R) → Ω[MvPolynomial ι R⁄R]) (pres.relation r))))) :
            ι →₀ S) :
          (a : ι) → S)
        a :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
⊢ pres.toExtension.cotangentComplex ∘ₗ hom₁ pres =
    (↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace) ∘ₗ
      pres.differentialsRelations.map
have h : ∀ (r : σ),
  Eq (α := pres.toExtension.CotangentSpace)
    (((pres.toExtension.cotangentComplex ∘ₗ hom₁ pres) ∘ₗ Finsupp.lsingle r : (a : S) → pres.toExtension.CotangentSpace)
      1)
    ((((↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace) ∘ₗ
            pres.differentialsRelations.map) ∘ₗ
          Finsupp.lsingle r :
        (a : S) → pres.toExtension.CotangentSpace)
      1)
Tactic: ext r
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (hypothesis)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
r : σ
⊢ Eq (α := pres.toExtension.CotangentSpace)
    (((pres.toExtension.cotangentComplex ∘ₗ hom₁ pres) ∘ₗ Finsupp.lsingle r : (a : S) → pres.toExtension.CotangentSpace)
      1)
    ((((↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace) ∘ₗ
            pres.differentialsRelations.map) ∘ₗ
          Finsupp.lsingle r :
        (a : S) → pres.toExtension.CotangentSpace)
      1)
have this : ∀ (r : pres.differentialsRelations.R),
  (pres.differentialsRelations.map : (a : pres.differentialsRelations.R →₀ S) → pres.differentialsRelations.G →₀ S)
      (Finsupp.single r 1) =
    pres.differentialsRelations.relation r
Tactic: have := (differentialsRelations pres).map_single
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
r : σ
this :
  ∀ (r : pres.differentialsRelations.R),
    (pres.differentialsRelations.map : (a : pres.differentialsRelations.R →₀ S) → pres.differentialsRelations.G →₀ S)
        (Finsupp.single r 1) =
      pres.differentialsRelations.relation r
⊢ Eq (α := pres.toExtension.CotangentSpace)
    (((pres.toExtension.cotangentComplex ∘ₗ hom₁ pres) ∘ₗ Finsupp.lsingle r : (a : S) → pres.toExtension.CotangentSpace)
      1)
    ((((↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace) ∘ₗ
            pres.differentialsRelations.map) ∘ₗ
          Finsupp.lsingle r :
        (a : S) → pres.toExtension.CotangentSpace)
      1)
have h : Eq (α := pres.toExtension.CotangentSpace)
  ((pres.toExtension.cotangentComplex : (a : pres.toExtension.Cotangent) → pres.toExtension.CotangentSpace)
      ((hom₁ pres : (a : σ →₀ S) → pres.toExtension.Cotangent) (Finsupp.single r 1)) :
    pres.toExtension.CotangentSpace)
  ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
      ((pres.differentialsRelations.map : (a : σ →₀ S) → ι →₀ S) (Finsupp.single r 1)) :
    pres.toExtension.CotangentSpace)
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
r : σ
this :
  ∀ (r : σ),
    (pres.differentialsRelations.map : (a : σ →₀ S) → ι →₀ S) (Finsupp.single r 1) =
      pres.differentialsRelations.relation r
⊢ Eq (α := pres.toExtension.CotangentSpace)
    ((pres.toExtension.cotangentComplex : (a : pres.toExtension.Cotangent) → pres.toExtension.CotangentSpace)
        ((hom₁ pres : (a : σ →₀ S) → pres.toExtension.Cotangent) (Finsupp.single r 1)) :
      pres.toExtension.CotangentSpace)
    ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
        ((pres.differentialsRelations.map : (a : σ →₀ S) → ι →₀ S) (Finsupp.single r 1)) :
      pres.toExtension.CotangentSpace)
have h : Eq (α := pres.toExtension.CotangentSpace)
  ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
      (pres.differentialsRelations.relation r) :
    pres.toExtension.CotangentSpace)
  ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
      ((pres.differentialsRelations.map : (a : σ →₀ S) → ι →₀ S) (Finsupp.single r 1)) :
    pres.toExtension.CotangentSpace)
Tactic: rw [comm₁₂_single, this]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
r : σ
this :
  ∀ (r : σ),
    (pres.differentialsRelations.map : (a : σ →₀ S) → ι →₀ S) (Finsupp.single r 1) =
      pres.differentialsRelations.relation r
h :
  Eq (α := pres.toExtension.CotangentSpace)
    ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
        (pres.differentialsRelations.relation r) :
      pres.toExtension.CotangentSpace)
    ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
        ((pres.differentialsRelations.map : (a : σ →₀ S) → ι →₀ S) (Finsupp.single r 1)) :
      pres.toExtension.CotangentSpace)
⊢ Eq (α := pres.toExtension.CotangentSpace)
    ((pres.toExtension.cotangentComplex : (a : pres.toExtension.Cotangent) → pres.toExtension.CotangentSpace)
        ((hom₁ pres : (a : σ →₀ S) → pres.toExtension.Cotangent) (Finsupp.single r 1)) :
      pres.toExtension.CotangentSpace)
    ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
        ((pres.differentialsRelations.map : (a : σ →₀ S) → ι →₀ S) (Finsupp.single r 1)) :
      pres.toExtension.CotangentSpace)
have h₁ : Eq (α := pres.toExtension.CotangentSpace)
  ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
      (pres.differentialsRelations.relation r) :
    pres.toExtension.CotangentSpace)
  ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
      (pres.differentialsRelations.relation r) :
    pres.toExtension.CotangentSpace)
Tactic: rw [comm₁₂_single, this]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
r : pres.differentialsRelations.R
⊢ Eq.{v + 1} (α := Ω[S⁄R])
    ((Finsupp.linearCombination S fun (g : pres.differentialsRelations.G) ↦ (D R S : (a : S) → Ω[S⁄R]) (pres.val g) :
          (a : pres.differentialsRelations.G →₀ S) → Ω[S⁄R])
        (pres.differentialsRelations.relation r) :
      Ω[S⁄R])
    (0 : Ω[S⁄R])
have simp : Eq.{v + 1} (α := Ω[S⁄R])
  ((pres.toExtension.toKaehler : (a : pres.toExtension.CotangentSpace) → Ω[S⁄R])
      ((pres.toExtension.cotangentComplex : (a : pres.toExtension.Cotangent) → pres.toExtension.CotangentSpace)
        ((hom₁ pres : (a : σ →₀ S) → pres.toExtension.Cotangent) (Finsupp.single r 1))) :
    Ω[S⁄R])
  (0 : Ω[S⁄R])
Tactic: simp only [differentialsRelations_G, LinearMap.coe_comp, LinearEquiv.coe_coe,
      Function.comp_apply, ← comm₂₃', ← comm₁₂_single]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
⊢ Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range pres.differentialsSolution.var)) ⊤ ∧
    pres.differentialsSolution.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)
have left : Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range pres.differentialsSolution.var)) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
left : Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range pres.differentialsSolution.var)) ⊤
⊢ Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range pres.differentialsSolution.var)) ⊤ ∧
    pres.differentialsSolution.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)
have right : pres.differentialsSolution.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
⊢ Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range pres.differentialsSolution.var)) ⊤
have left : Function.Surjective (α := Finsupp.{w, v} pres.differentialsRelations.G S) (β := Ω[S⁄R])
  (⇑(pres.toExtension.toKaehler ∘ₗ
        (↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace)) :
    (a : pres.differentialsRelations.G →₀ S) → Ω[S⁄R])
Tactic: rw [← Module.Relations.Solution.surjective_π_iff_span_eq_top, ← comm₂₃]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Differentials (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
⊢ pres.differentialsSolution.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)
have right : pres.differentialsSolution.π.ker = pres.differentialsRelations.map.range
Tactic: rw [← Module.Relations.range_map]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.DirectSum (goal)
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
relations : ι → Relations.{w₀, w₁, u} A
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
N : Type v
inst_4 : AddCommGroup N
inst_5 : Module A N
s : (directSum relations).Solution N
i : ι
r : (relations i).R
⊢ Eq.{v + 1} (α := N)
    ((Finsupp.linearCombination A fun (g : (relations i).G) ↦
            s.var (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g) :
          (a : (relations i).G →₀ A) → N)
        ((relations i).relation r) :
      N)
    (0 : N)
have rw : Eq.{v + 1} (α := N)
  ((Finsupp.linearCombination A fun (g : (relations i).G) ↦ s.var (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g) :
        (a : (relations i).G →₀ A) → N)
      ((relations i).relation r) :
    N)
  ((Finsupp.linearCombination A s.var : (a : (directSum relations).G →₀ A) → N)
      ((directSum relations).relation (Sigma.mk (β := fun (i : ι) ↦ (relations i).R) i r)) :
    N)
Tactic: rw [← s.linearCombination_var_relation ⟨i, r⟩]