awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
⊢ f = f'
have suffices : f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient
Tactic: suffices f.comp solution.fromQuotient = f'.comp solution.fromQuotient by
    ext x
    obtain ⟨y, rfl⟩ := h.bijective.2 x
    exact DFunLike.congr_fun this y
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
⊢ f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient
have h₁ : ∀ (g : relations.G),
  Eq.{v' + 1} (α := N)
    ((f ∘ₗ solution.fromQuotient : (a : relations.Quotient) → N)
        ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) (Finsupp.single g 1) :
          relations.Quotient) :
      N)
    ((f' ∘ₗ solution.fromQuotient : (a : relations.Quotient) → N)
        ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) (Finsupp.single g 1) :
          relations.Quotient) :
      N)
Tactic: ext g
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (hypothesis)
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
e : M ≃ₗ[A] N
⊢ Function.Bijective (α := relations.Quotient) (β := N)
    (⇑(solution.postcomp (↑e : M →ₗ[A] N)).fromQuotient : (a : relations.Quotient) → N)
have this : (solution.postcomp (↑e : M →ₗ[A] N)).fromQuotient = (↑e : M →ₗ[A] N) ∘ₗ solution.fromQuotient
Tactic: have : (solution.postcomp e.toLinearMap).fromQuotient =
      e.toLinearMap.comp (solution.fromQuotient) := by aesop
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
e : M ≃ₗ[A] N
this : (solution.postcomp (↑e : M →ₗ[A] N)).fromQuotient = (↑e : M →ₗ[A] N) ∘ₗ solution.fromQuotient
⊢ Function.Bijective (α := relations.Quotient) (β := N)
    (⇑(solution.postcomp (↑e : M →ₗ[A] N)).fromQuotient : (a : relations.Quotient) → N)
have rw : Function.Bijective (α := relations.Quotient) (β := N)
  (Function.comp (β := M) (⇑e : (a : M) → N) (⇑solution.fromQuotient : (a : relations.Quotient) → M))
Tactic: rw [this, LinearMap.coe_comp, LinearEquiv.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
h : solution.IsPresentationCore
N : Type w''
x : AddCommGroup N
x_1 : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
⊢ f = f'
have h₁ : ∀ (x_2 : M), Eq.{w'' + 1} (α := N) ((f : (a : M) → N) x_2 : N) ((f' : (a : M) → N) x_2 : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (hypothesis)
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
h : solution.IsPresentationCore
N : Type w''
x_1 : AddCommGroup N
x_2 : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
x : M
⊢ Eq.{w'' + 1} (α := N) ((f : (a : M) → N) x : N) ((f' : (a : M) → N) x : N)
have this : Eq (α := relations.Solution (ULift.{w', w''} N))
  ((solution.postcomp f).postcomp (↑(LinearEquiv.symm ULift.moduleEquiv) : N →ₗ[A] ULift.{w', w''} N))
  ((solution.postcomp f').postcomp (↑(LinearEquiv.symm ULift.moduleEquiv) : N →ₗ[A] ULift.{w', w''} N))
Tactic: have := congr_postcomp h' ULift.moduleEquiv.{_, _, w'}.symm.toLinearMap
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
⊢ solution.IsPresentation ↔
    Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤ ∧
      solution.π.ker = Submodule.span A (Set.range relations.relation)
have rw : solution.IsPresentation ↔
  Function.Surjective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M) ∧
    Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M)
Tactic: rw [← injective_fromQuotient_iff_ker_π_eq_span,
    ← surjective_π_iff_span_eq_top, ← surjective_fromQuotient_iff_surjective_π, ]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
h₁ : Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ solution.IsPresentation
have rw : Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤ ∧
  solution.π.ker = Submodule.span A (Set.range relations.relation)
Tactic: rw [isPresentation_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Cokernel (goal)
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
⊢ Nonempty (pres₂.CokernelData f g₁)
have obtain : ∀ (s : M₂ → Finsupp.{w₂₀, u} pres₂.G A) (hs : Function.RightInverse s (⇑pres₂.π : (a : pres₂.G →₀ A) → M₂)),
  Nonempty (pres₂.CokernelData f g₁)
Tactic: obtain ⟨s, hs⟩ := pres₂.surjective_π.hasRightInverse
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Cokernel (goal)
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
x : (pres₂.cokernelRelations data).R
⊢ Eq.{v₂ + 1} (α := M₂ ⧸ f.range)
    ((Finsupp.linearCombination A fun (g : (pres₂.cokernelRelations data).G) ↦
            (f.range.mkQ : (a : M₂) → M₂ ⧸ f.range) (pres₂.var g) :
          (a : (pres₂.cokernelRelations data).G →₀ A) → M₂ ⧸ f.range)
        ((pres₂.cokernelRelations data).relation x) :
      M₂ ⧸ f.range)
    (0 : M₂ ⧸ f.range)
have erw : Eq (α := M₂ ⧸ f.range)
  ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range)
      ((Finsupp.linearCombination A pres₂.var : (a : (pres₂.cokernelRelations data).G →₀ A) → M₂)
        ((pres₂.cokernelRelations data).relation x)) :
    M₂ ⧸ f.range)
  (0 : M₂ ⧸ f.range)
Tactic: erw [← Finsupp.apply_linearCombination]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Cokernel (goal)
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
x : (pres₂.cokernelRelations data).R
⊢ Eq (α := M₂ ⧸ f.range)
    ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range)
        ((Finsupp.linearCombination A pres₂.var : (a : (pres₂.cokernelRelations data).G →₀ A) → M₂)
          ((pres₂.cokernelRelations data).relation x)) :
      M₂ ⧸ f.range)
    (0 : M₂ ⧸ f.range)
have inl : ∀ (r : pres₂.R),
  Eq (α := M₂ ⧸ f.range)
    ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range)
        ((Finsupp.linearCombination A pres₂.var : (a : (pres₂.cokernelRelations data).G →₀ A) → M₂)
          ((pres₂.cokernelRelations data).relation (Sum.inl r))) :
      M₂ ⧸ f.range)
    (0 : M₂ ⧸ f.range)
Tactic: obtain (r | i) := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Cokernel (goal)
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
x : (pres₂.cokernelRelations data).R
inl :
  ∀ (r : pres₂.R),
    Eq (α := M₂ ⧸ f.range)
      ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range)
          ((Finsupp.linearCombination A pres₂.var : (a : (pres₂.cokernelRelations data).G →₀ A) → M₂)
            ((pres₂.cokernelRelations data).relation (Sum.inl r))) :
        M₂ ⧸ f.range)
      (0 : M₂ ⧸ f.range)
⊢ Eq (α := M₂ ⧸ f.range)
    ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range)
        ((Finsupp.linearCombination A pres₂.var : (a : (pres₂.cokernelRelations data).G →₀ A) → M₂)
          ((pres₂.cokernelRelations data).relation x)) :
      M₂ ⧸ f.range)
    (0 : M₂ ⧸ f.range)
have inr : ∀ (i : ι),
  Eq (α := M₂ ⧸ f.range)
    ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range)
        ((Finsupp.linearCombination A pres₂.var : (a : (pres₂.cokernelRelations data).G →₀ A) → M₂)
          ((pres₂.cokernelRelations data).relation (Sum.inr i))) :
      M₂ ⧸ f.range)
    (0 : M₂ ⧸ f.range)
Tactic: obtain (r | i) := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Cokernel (goal)
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
r : pres₂.R
⊢ Eq (α := M₂ ⧸ f.range)
    ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range)
        ((Finsupp.linearCombination A pres₂.var : (a : (pres₂.cokernelRelations data).G →₀ A) → M₂)
          ((pres₂.cokernelRelations data).relation (Sum.inl r))) :
      M₂ ⧸ f.range)
    (0 : M₂ ⧸ f.range)
have inl : Eq (α := M₂ ⧸ f.range) ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range) 0) 0
Tactic: erw [pres₂.linearCombination_var_relation]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Cokernel (goal)
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
i : ι
⊢ Eq (α := M₂ ⧸ f.range)
    ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range)
        ((Finsupp.linearCombination A pres₂.var : (a : (pres₂.cokernelRelations data).G →₀ A) → M₂)
          ((pres₂.cokernelRelations data).relation (Sum.inr i))) :
      M₂ ⧸ f.range)
    (0 : M₂ ⧸ f.range)
have inr : Eq (α := M₂ ⧸ f.range) ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range) ((f : (a : M₁) → M₂) (g₁ i)) : M₂ ⧸ f.range)
  (0 : M₂ ⧸ f.range)
Tactic: erw [data.π_lift]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Cokernel (goal)
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
N : Type w
inst_7 : AddCommGroup N
inst_8 : Module A N
s : (pres₂.cokernelRelations data).Solution N
⊢ f.range ≤ LinearMap.ker.{u, u, v₂, w} (M₂ := N) (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ })
have rw : Set.range g₁ ⊆
  (⇑f : (a : M₁) → M₂) ⁻¹'
    (↑(LinearMap.ker.{u, u, v₂, w} (M₂ := N)
          (sorry.desc { var := s.var, linearCombination_var_relation := sorry : pres₂.Solution N })) :
      Set M₂)
Tactic: rw [LinearMap.range_eq_map, ← hg₁, Submodule.map_span, Submodule.span_le,
            Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Cokernel (goal)
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
N : Type w
inst_7 : AddCommGroup N
inst_8 : Module A N
s : (pres₂.cokernelRelations data).Solution N
i : ι
⊢ Membership.mem (γ := Set M₁)
    ((⇑f : (a : M₁) → M₂) ⁻¹'
      (↑(LinearMap.ker.{u, u, v₂, w} (M₂ := N)
            (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ : pres₂.Solution N })) :
        Set M₂))
    (g₁ i)
have rw : Eq.{w + 1} (α := N)
  ((Relations.Solution.π { var := s.var, linearCombination_var_relation := sorry } : (a : pres₂.G →₀ A) → N) (data.lift i) :
    N)
  (0 : N)
Tactic: rw [Set.mem_preimage, SetLike.mem_coe, LinearMap.mem_ker, ← data.π_lift,
            Relations.Solution.IsPresentation.π_desc_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Cokernel (goal)
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
N : Type w
inst_7 : AddCommGroup N
inst_8 : Module A N
f_1 f' : LinearMap.{u, u, v₂, w} (RingHom.id A) (M₂ ⧸ f.range) N
h : (pres₂.cokernelSolution data).postcomp f_1 = (pres₂.cokernelSolution data).postcomp f'
⊢ f_1 = f'
have h₁ : f_1 ∘ₗ f.range.mkQ = f' ∘ₗ f.range.mkQ
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Cokernel (goal)
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
N : Type w
inst_7 : AddCommGroup N
inst_8 : Module A N
f_1 f' : LinearMap.{u, u, v₂, w} (RingHom.id A) (M₂ ⧸ f.range) N
h : (pres₂.cokernelSolution data).postcomp f_1 = (pres₂.cokernelSolution data).postcomp f'
⊢ f_1 ∘ₗ f.range.mkQ = f' ∘ₗ f.range.mkQ
have h₁ : pres₂.postcomp (f_1 ∘ₗ f.range.mkQ) = pres₂.postcomp (f' ∘ₗ f.range.mkQ)
Tactic: apply pres₂.toIsPresentation.postcomp_injective
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Cokernel (goal)
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
N : Type w
inst_7 : AddCommGroup N
inst_8 : Module A N
f_1 f' : LinearMap.{u, u, v₂, w} (RingHom.id A) (M₂ ⧸ f.range) N
h : (pres₂.cokernelSolution data).postcomp f_1 = (pres₂.cokernelSolution data).postcomp f'
⊢ pres₂.postcomp (f_1 ∘ₗ f.range.mkQ) = pres₂.postcomp (f' ∘ₗ f.range.mkQ)
have h₁ : ∀ (g : pres₂.G), (pres₂.postcomp (f_1 ∘ₗ f.range.mkQ)).var g = (pres₂.postcomp (f' ∘ₗ f.range.mkQ)).var g
Tactic: ext g
-- 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.toKaehler ∘ₗ (↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace) =
    Finsupp.linearCombination S fun (g : ι) ↦ (D R S : (a : S) → Ω[S⁄R]) (pres.val g)
have h : ∀ (a : ι),
  Eq (α := Ω[S⁄R])
    (((pres.toExtension.toKaehler ∘ₗ
            (↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace)) ∘ₗ
          Finsupp.lsingle a :
        (a : S) → Ω[S⁄R])
      1)
    (((Finsupp.linearCombination S fun (g : ι) ↦ (D R S : (a : S) → Ω[S⁄R]) (pres.val g)) ∘ₗ Finsupp.lsingle a :
        (a : S) → Ω[S⁄R])
      1)
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 ι σ
φ : LinearMap (R := pres.Ring) (RingHom.id pres.Ring) (σ →₀ S) pres.toExtension.Cotangent :=
  { toFun := (⇑(hom₁ pres) : (a : σ →₀ S) → pres.toExtension.Cotangent), map_add' := ⋯, map_smul' := ⋯ }
⊢ Function.Surjective (α := σ →₀ S) (β := pres.toExtension.Cotangent)
    (⇑(hom₁ pres) : (a : σ →₀ S) → pres.toExtension.Cotangent)
have change : Function.Surjective (α := σ →₀ S) (β := pres.toExtension.Cotangent) (⇑φ : (a : σ →₀ S) → pres.toExtension.Cotangent)
Tactic: change Function.Surjective φ
-- 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' := ⋯ }
⊢ Function.Surjective (α := σ →₀ S) (β := pres.toExtension.Cotangent) (⇑φ : (a : σ →₀ S) → pres.toExtension.Cotangent)
have h₁ : Function.Surjective (α := ↥pres.toExtension.ker) (β := pres.toExtension.Cotangent)
  (⇑Extension.Cotangent.mk : (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
Tactic: have h₁ := Algebra.Extension.Cotangent.mk_surjective (P := pres.toExtension)
-- 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)
⊢ 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) ⋯))
    ⊤
have refine : Submodule.map (Submodule.subtype pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) sorry)) =
  Submodule.map (Submodule.subtype pres.ker) ⊤
Tactic: refine Submodule.map_injective_of_injective (f := Submodule.subtype pres.ker)
      Subtype.coe_injective ?_
-- 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)
⊢ Submodule.map (Submodule.subtype 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 (Submodule.subtype pres.ker) ⊤
have rw : Ideal.span
    (Set.image (α := ↥pres.ker) (Subtype.val (p := fun (x : pres.Ring) ↦ x ∈ pres.ker))
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) sorry)) =
  pres.ker
Tactic: rw [Submodule.map_top, Submodule.range_subtype, Submodule.map_span,
      Submodule.coe_subtype, Ideal.submodule_span_eq]
-- 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)
⊢ Ideal.span
      (Set.image (α := ↥pres.ker) (Subtype.val (p := fun (x : pres.Ring) ↦ x ∈ pres.ker))
        (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯)) =
    pres.ker
have simp : Eq (α := Submodule pres.Ring pres.Ring)
  (Ideal.span
    (Set.image (α := ↥pres.ker) (Subtype.val (p := fun (x : pres.Ring) ↦ x ∈ pres.ker))
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) sorry)))
  (Ideal.span (Set.range pres.relation))
Tactic: simp only [← pres.span_range_relation_eq_ker]
-- 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)
⊢ Eq (α := Submodule pres.Ring pres.Ring)
    (Ideal.span
      (Set.image (α := ↥pres.ker) (Subtype.val (p := fun (x : pres.Ring) ↦ x ∈ pres.ker))
        (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯)))
    (Ideal.span (Set.range pres.relation))
have e_s : Set.image (α := ↥pres.ker) (Subtype.val (p := fun (x : pres.Ring) ↦ x ∈ pres.ker))
    (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) sorry) =
  Set.range pres.relation
Tactic: congr