awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
rw :
  Eq.{u_3 + 1} (α := Submodule R N) (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : N) ↦ x ∈ s)))) ⊤
rw₁ : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
⊢ Eq.{u_3 + 1} (α := Submodule R N)
    (LinearMap.range (M := Finsupp.{u_3, u_1} (↥s) R) (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)))) ⊤
have rw₂ : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) (Submodule.span R (↑s : Set N))
Tactic: rw [range_linearCombination, Subtype.range_val, ← hs]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
⊢ l.ker.FG
have H : Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
  (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
Tactic: have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → N)) :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
⊢ ∃ (f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M), l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
have choose : ∀ (f : (b : N) → M) (hf : ∀ (b : N), (l : (a : M) → N) (f b) = b),
  ∃ (f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M), l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
Tactic: choose f hf using show _ from hl
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : (b : N) → M
hf : ∀ (b : N), (l : (a : M) → N) (f b) = b
⊢ Eq (α := Finsupp.{u_3, u_1} (↥s) R →ₗ[R] N) (l ∘ₗ linearCombination R fun (i : ↥s) ↦ f (↑i : N))
    (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)))
have h : ∀ (a : ↥s),
  Eq.{u_3 + 1} (α := N) (((l ∘ₗ linearCombination R fun (i : ↥s) ↦ f (↑i : N)) ∘ₗ lsingle a : (a : R) → N) 1 : N)
    ((linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)) ∘ₗ lsingle a : (a : R) → N) 1 : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
⊢ l.ker.FG
have obtain : ∀ (f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M) (hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))),
  l.ker.FG
Tactic: obtain ⟨f, hf⟩ : ∃ f : (s →₀ R) →ₗ[R] M, l ∘ₗ f = (Finsupp.linearCombination R Subtype.val) := by
    choose f hf using show _ from hl
    exact ⟨Finsupp.linearCombination R (fun i ↦ f i), by ext; simp [hf]⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
⊢ Submodule.map f.range.mkQ l.ker = ⊤
have rw : ⊤ ≤ Submodule.map f.range.mkQ l.ker
Tactic: rw [← top_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
x : M ⧸ f.range
⊢ x ∈ Submodule.map f.range.mkQ l.ker
have obtain : ∀ (x : M),
  Membership.mem (α := M ⧸ f.range) (Submodule.map f.range.mkQ l.ker)
    ((f.range.mkQ : (a : M) → M ⧸ f.range) x : M ⧸ f.range)
Tactic: obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
x : M
⊢ Membership.mem (α := M ⧸ f.range) (Submodule.map f.range.mkQ l.ker)
    ((f.range.mkQ : (a : M) → M ⧸ f.range) x : M ⧸ f.range)
have obtain : ∀ (y : Finsupp.{u_3, u_1} (↥s) R)
  (hy :
    Eq.{u_3 + 1} (α := N) ((linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)) : (a : ↥s →₀ R) → N) y : N)
      ((l : (a : M) → N) x : N)),
  Membership.mem (α := M ⧸ f.range) (Submodule.map f.range.mkQ l.ker)
    ((f.range.mkQ : (a : M) → M ⧸ f.range) x : M ⧸ f.range)
Tactic: obtain ⟨y, hy⟩ := H (l x)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
x : M
y : Finsupp.{u_3, u_1} (↥s) R
hy :
  Eq.{u_3 + 1} (α := N) ((linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)) : (a : ↥s →₀ R) → N) y : N)
    ((l : (a : M) → N) x : N)
⊢ Membership.mem (α := M ⧸ f.range) (Submodule.map f.range.mkQ l.ker)
    ((f.range.mkQ : (a : M) → M ⧸ f.range) x : M ⧸ f.range)
have hy₁ : Eq.{u_3 + 1} (α := N) ((l : (a : M) → N) (HSub.hSub (β := M) x ((f : (a : ↥s →₀ R) → M) y : M)) : N) (0 : N)
Tactic: rw [← hf, LinearMap.comp_apply, eq_comm, ← sub_eq_zero, ← map_sub] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
⊢ l.ker.FG
have this : Submodule.map f.range.mkQ l.ker = ⊤
Tactic: have : (LinearMap.ker l).map (LinearMap.range f).mkQ = ⊤ := by
    rw [← top_le_iff]
    rintro x -
    obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
    obtain ⟨y, hy⟩ := H (l x)
    rw [← hf, LinearMap.comp_apply, eq_comm, ← sub_eq_zero, ← map_sub] at hy
    exact ⟨_, hy, by simp⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
this : Submodule.map f.range.mkQ l.ker = ⊤
⊢ l.ker.FG
have hs1 : (Submodule.map f.range.mkQ l.ker).FG
Tactic: apply Submodule.fg_of_fg_map_of_fg_inf_ker (LinearMap.range f).mkQ
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
this : Submodule.map f.range.mkQ l.ker = ⊤
hs1 : (Submodule.map f.range.mkQ l.ker).FG
⊢ l.ker.FG
have hs2 : (l.ker ⊓ f.range.mkQ.ker).FG
Tactic: apply Submodule.fg_of_fg_map_of_fg_inf_ker (LinearMap.range f).mkQ
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
this : Submodule.map f.range.mkQ l.ker = ⊤
⊢ (Submodule.map f.range.mkQ l.ker).FG
have hs1 : Submodule.FG.{u_1, u_2} (R := R) (M := M ⧸ f.range) ⊤
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
this : Submodule.map f.range.mkQ l.ker = ⊤
⊢ (l.ker ⊓ f.range.mkQ.ker).FG
have hs2 : (Submodule.map f (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))).FG
Tactic: rw [Submodule.ker_mkQ, inf_comm, ← Submodule.map_comap_eq, ← LinearMap.ker_comp, hf]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
h : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
⊢ l.ker.FG
have obtain : ∀ (s : Finset N) (hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤)
  (hs' :
    Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
      (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))),
  l.ker.FG
Tactic: classical
  obtain ⟨s, hs, hs'⟩ := h
  have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → N)) :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])
  obtain ⟨f, hf⟩ : ∃ f : (s →₀ R) →ₗ[R] M, l ∘ₗ f = (Finsupp.linearCombination R Subtype.val) := by
    choose f hf using show _ from hl
    exact ⟨Finsupp.linearCombination R (fun i ↦ f i), by ext; simp [hf]⟩
  have : (LinearMap.ker l).map (LinearMap.range f).mkQ = ⊤ := by
    rw [← top_le_iff]
    rintro x -
    obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
    obtain ⟨y, hy⟩ := H (l x)
    rw [← hf, LinearMap.comp_apply, eq_comm, ← sub_eq_zero, ← map_sub] at hy
    exact ⟨_, hy, by simp⟩
  apply Submodule.fg_of_fg_map_of_fg_inf_ker (LinearMap.range f).mkQ
  · rw [this]
    exact Module.Finite.fg_top
  · rw [Submodule.ker_mkQ, inf_comm, ← Submodule.map_comap_eq, ← LinearMap.ker_comp, hf]
    exact hs'.map f
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
h : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
obtain :
  ∀ (s : Finset N) (hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))),
    l.ker.FG
⊢ l.ker.FG
have obtain₁ : ∀ (s : Finset N) (hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤)
  (hs' :
    Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
      (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)))))
  (H :
    Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
      (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)),
  l.ker.FG
Tactic: classical
  obtain ⟨s, hs, hs'⟩ := h
  have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → N)) :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])
  obtain ⟨f, hf⟩ : ∃ f : (s →₀ R) →ₗ[R] M, l ∘ₗ f = (Finsupp.linearCombination R Subtype.val) := by
    choose f hf using show _ from hl
    exact ⟨Finsupp.linearCombination R (fun i ↦ f i), by ext; simp [hf]⟩
  have : (LinearMap.ker l).map (LinearMap.range f).mkQ = ⊤ := by
    rw [← top_le_iff]
    rintro x -
    obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
    obtain ⟨y, hy⟩ := H (l x)
    rw [← hf, LinearMap.comp_apply, eq_comm, ← sub_eq_zero, ← map_sub] at hy
    exact ⟨_, hy, by simp⟩
  apply Submodule.fg_of_fg_map_of_fg_inf_ker (LinearMap.range f).mkQ
  · rw [this]
    exact Module.Finite.fg_top
  · rw [Submodule.ker_mkQ, inf_comm, ← Submodule.map_comap_eq, ← LinearMap.ker_comp, hf]
    exact hs'.map f
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
h : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
obtain :
  ∀ (s : Finset N) (hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))),
    l.ker.FG
obtain₁ :
  ∀ (s : Finset N) (hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)))))
    (H :
      Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
        (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)),
    l.ker.FG
⊢ l.ker.FG
have obtain₂ : ∀ (s : Finset N) (hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤)
  (hs' :
    Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
      (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)))))
  (H :
    Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
      (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N))
  (f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M) (hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))),
  l.ker.FG
Tactic: classical
  obtain ⟨s, hs, hs'⟩ := h
  have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → N)) :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])
  obtain ⟨f, hf⟩ : ∃ f : (s →₀ R) →ₗ[R] M, l ∘ₗ f = (Finsupp.linearCombination R Subtype.val) := by
    choose f hf using show _ from hl
    exact ⟨Finsupp.linearCombination R (fun i ↦ f i), by ext; simp [hf]⟩
  have : (LinearMap.ker l).map (LinearMap.range f).mkQ = ⊤ := by
    rw [← top_le_iff]
    rintro x -
    obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
    obtain ⟨y, hy⟩ := H (l x)
    rw [← hf, LinearMap.comp_apply, eq_comm, ← sub_eq_zero, ← map_sub] at hy
    exact ⟨_, hy, by simp⟩
  apply Submodule.fg_of_fg_map_of_fg_inf_ker (LinearMap.range f).mkQ
  · rw [this]
    exact Module.Finite.fg_top
  · rw [Submodule.ker_mkQ, inf_comm, ← Submodule.map_comap_eq, ← LinearMap.ker_comp, hf]
    exact hs'.map f
Cleared hypotheses: h