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 : Free R M
inst_6 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M →
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯) :=
  fun (i : Free.ChooseBasisIndex R M) ↦
    Subtype.mk (p := fun (x : N) ↦
      Membership.mem (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)
        x)
      ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) ⋯
σ :
  (b :
      ↥(Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)) →
    Free.ChooseBasisIndex R M
hσ :
  ∀
    (b_1 :
      ↥(Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)),
    π (σ b_1) = b_1
hπ :
  Subtype.val (p := fun (x : N) ↦
        Membership.mem (γ := Finset N)
          (Set.Finite.toFinset (s :=
            Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
              (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
            ⋯)
          x) ∘
      π =
    Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)
hσ₁ : π ∘ σ = id
⊢ Function.comp (β := M) (⇑l : (a : M) → N) ((⇑b : (a : Free.ChooseBasisIndex R M) → M) ∘ σ) =
    Subtype.val (p := fun (x : N) ↦
      Membership.mem (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)
        x)
have h : ∀
  (i :
    ↥(Set.Finite.toFinset (s :=
        Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
          (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
        sorry)),
  Function.comp (β := M) (⇑l : (a : M) → N) ((⇑b : (a : Free.ChooseBasisIndex R M) → M) ∘ σ) i = (↑i : N)
Tactic: ext i
-- 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 : Free R M
inst_6 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M →
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯) :=
  fun (i : Free.ChooseBasisIndex R M) ↦
    Subtype.mk (p := fun (x : N) ↦
      Membership.mem (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)
        x)
      ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) ⋯
σ :
  (b :
      ↥(Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)) →
    Free.ChooseBasisIndex R M
hσ :
  ∀
    (b_1 :
      ↥(Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)),
    π (σ b_1) = b_1
hπ :
  Subtype.val (p := fun (x : N) ↦
        Membership.mem (γ := Finset N)
          (Set.Finite.toFinset (s :=
            Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
              (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
            ⋯)
          x) ∘
      π =
    Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)
hσ₁ : π ∘ σ = id
⊢ FinitePresentation R N
have hσ₂ : Function.comp (β := M) (⇑l : (a : M) → N) ((⇑b : (a : Free.ChooseBasisIndex R M) → M) ∘ σ) =
  Subtype.val (p := fun (x : N) ↦
    Membership.mem (γ := Finset N)
      (Set.Finite.toFinset (s :=
        Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
          (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
        sorry)
      x)
Tactic: have hσ₂ : l ∘ b ∘ σ = Subtype.val := by ext i; exact congr_arg Subtype.val (hσ i)
-- 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 : Free R M
inst_6 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
let let₁ let₂ let₃ : FinitePresentation R N
⊢ FinitePresentation R N
have let₄ : let b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M;
let π :
  Free.ChooseBasisIndex R M →
    ↥(Set.Finite.toFinset (s :=
        Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
          (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
        sorry) :=
  fun (i : Free.ChooseBasisIndex R M) ↦
  Subtype.mk (p := fun (x : N) ↦
    Membership.mem (γ := Finset N)
      (Set.Finite.toFinset (s :=
        Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
          (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
        sorry)
      x)
    ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) sorry;
∀ (this : Function.Surjective π), FinitePresentation R N
Tactic: classical
  let b := Module.Free.chooseBasis R M
  let π : Free.ChooseBasisIndex R M → (Set.finite_range (l ∘ b)).toFinset :=
    fun i ↦ ⟨l (b i), by simp⟩
  have : π.Surjective := fun ⟨x, hx⟩ ↦ by
    obtain ⟨y, rfl⟩ : ∃ a, l (b a) = x := by simpa using hx
    exact ⟨y, rfl⟩
  choose σ hσ using this
  have hπ : Subtype.val ∘ π = l ∘ b := rfl
  have hσ₁ : π ∘ σ = id := by ext i; exact congr_arg Subtype.val (hσ i)
  have hσ₂ : l ∘ b ∘ σ = Subtype.val := by ext i; exact congr_arg Subtype.val (hσ i)
  refine ⟨(Set.finite_range (l ∘ b)).toFinset,
    by simpa [Set.range_comp, LinearMap.range_eq_top], ?_⟩
  let f : M →ₗ[R] (Set.finite_range (l ∘ b)).toFinset →₀ R :=
    Finsupp.lmapDomain _ _ π ∘ₗ b.repr.toLinearMap
  convert! hl'.map f
  ext x; simp only [LinearMap.mem_ker, Submodule.mem_map]
  constructor
  · intro hx
    refine ⟨b.repr.symm (x.mapDomain σ), ?_, ?_⟩
    · simp [Finsupp.apply_linearCombination, hσ₂, hx]
    · simp only [f, LinearMap.comp_apply, b.repr.apply_symm_apply,
        LinearEquiv.coe_toLinearMap, Finsupp.lmapDomain_apply]
      rw [← Finsupp.mapDomain_comp, hσ₁, Finsupp.mapDomain_id]
  · rintro ⟨y, hy, rfl⟩
    simp [f, hπ, ← Finsupp.apply_linearCombination, hy]
-- 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
h : FinitePresentation R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
⊢ FinitePresentation R N
have obtain : ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
  (hs' :
    Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
      (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))),
  FinitePresentation R N
Tactic: obtain ⟨s, hs, hs'⟩ := h
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
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
⊢ FinitePresentation R N
have obtain : ∀ (t : Finset M) (ht : Submodule.span R (↑t : Set M) = l.ker), FinitePresentation R N
Tactic: obtain ⟨t, ht⟩ := hl'
Cleared hypotheses: hl'
-- 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
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
t : Finset M
ht : Submodule.span R (↑t : Set M) = l.ker
⊢ FinitePresentation R N
have H : Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := M)
  (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M)
Tactic: have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → M)) :=
    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
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
t : Finset M
ht : Submodule.span R (↑t : Set M) = l.ker
H :
  Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := M)
    (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M)
⊢ Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
    (LinearMap.ker (l ∘ₗ linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
have choose : ∀ (σ : (b : M) → Finsupp.{u_2, u_1} (↥s) R)
  (hσ : ∀ (b : M), (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) (σ b) = b),
  Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
    (LinearMap.ker (l ∘ₗ linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
Tactic: choose σ hσ using (show _ from H)
-- 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
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
t : Finset M
ht : Submodule.span R (↑t : Set M) = l.ker
H :
  Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := M)
    (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M)
σ : (b : M) → Finsupp.{u_2, u_1} (↥s) R
hσ : ∀ (b : M), (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) (σ b) = b
⊢ Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
    (LinearMap.ker (l ∘ₗ linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
have this : (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M) '' σ '' (↑t : Set M) =
  (↑t : Set M)
Tactic: have : Finsupp.linearCombination R Subtype.val '' σ '' t = t := by
    simp only [Set.image_image, hσ, Set.image_id']
-- 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
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
t : Finset M
ht : Submodule.span R (↑t : Set M) = l.ker
H :
  Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := M)
    (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M)
σ : (b : M) → Finsupp.{u_2, u_1} (↥s) R
hσ : ∀ (b : M), (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) (σ b) = b
this :
  (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M) '' σ '' (↑t : Set M) =
    (↑t : Set M)
⊢ Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
    (LinearMap.ker (l ∘ₗ linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
have rw : (Submodule.span R (↑(Finset.image σ t) : Set (↥s →₀ R)) ⊔
    LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))).FG
Tactic: rw [LinearMap.ker_comp, ← ht, ← this, ← Submodule.map_span, Submodule.comap_map_eq,
    ← Finset.coe_image]
-- 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
h : FinitePresentation R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
⊢ FinitePresentation R N
have obtain : ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
  (hs' :
    Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
      (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))),
  FinitePresentation R N
Tactic: classical
  obtain ⟨s, hs, hs'⟩ := h
  obtain ⟨t, ht⟩ := hl'
  have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → M)) :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])
  apply Module.finitePresentation_of_free_of_surjective (l ∘ₗ linearCombination R Subtype.val)
    (hl.comp H)
  choose σ hσ using (show _ from H)
  have : Finsupp.linearCombination R Subtype.val '' σ '' t = t := by
    simp only [Set.image_image, hσ, Set.image_id']
  rw [LinearMap.ker_comp, ← ht, ← this, ← Submodule.map_span, Submodule.comap_map_eq,
    ← Finset.coe_image]
  exact Submodule.FG.sup ⟨_, rfl⟩ hs'
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
h : FinitePresentation R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
obtain :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))),
    FinitePresentation R N
⊢ FinitePresentation R N
have obtain₁ : ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
  (hs' :
    Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
      (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))))
  (t : Finset M) (ht : Submodule.span R (↑t : Set M) = l.ker), FinitePresentation R N
Tactic: classical
  obtain ⟨s, hs, hs'⟩ := h
  obtain ⟨t, ht⟩ := hl'
  have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → M)) :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])
  apply Module.finitePresentation_of_free_of_surjective (l ∘ₗ linearCombination R Subtype.val)
    (hl.comp H)
  choose σ hσ using (show _ from H)
  have : Finsupp.linearCombination R Subtype.val '' σ '' t = t := by
    simp only [Set.image_image, hσ, Set.image_id']
  rw [LinearMap.ker_comp, ← ht, ← this, ← Submodule.map_span, Submodule.comap_map_eq,
    ← Finset.coe_image]
  exact Submodule.FG.sup ⟨_, rfl⟩ hs'
Cleared hypotheses: h, 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
h : FinitePresentation R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
obtain :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))),
    FinitePresentation R N
obtain₁ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))))
    (t : Finset M) (ht : Submodule.span R (↑t : Set M) = l.ker), FinitePresentation R N
⊢ FinitePresentation R N
have obtain₂ : ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
  (hs' :
    Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
      (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))))
  (t : Finset M) (ht : Submodule.span R (↑t : Set M) = l.ker)
  (H :
    Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := M)
      (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M)),
  FinitePresentation R N
Tactic: classical
  obtain ⟨s, hs, hs'⟩ := h
  obtain ⟨t, ht⟩ := hl'
  have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → M)) :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])
  apply Module.finitePresentation_of_free_of_surjective (l ∘ₗ linearCombination R Subtype.val)
    (hl.comp H)
  choose σ hσ using (show _ from H)
  have : Finsupp.linearCombination R Subtype.val '' σ '' t = t := by
    simp only [Set.image_image, hσ, Set.image_id']
  rw [LinearMap.ker_comp, ← ht, ← this, ← Submodule.map_span, Submodule.comap_map_eq,
    ← Finset.coe_image]
  exact Submodule.FG.sup ⟨_, rfl⟩ hs'
Cleared hypotheses: h, 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
h : FinitePresentation R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
obtain :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))),
    FinitePresentation R N
obtain₁ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))))
    (t : Finset M) (ht : Submodule.span R (↑t : Set M) = l.ker), FinitePresentation R N
obtain₂ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))))
    (t : Finset M) (ht : Submodule.span R (↑t : Set M) = l.ker)
    (H :
      Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := M)
        (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M)),
    FinitePresentation R N
⊢ FinitePresentation R N
have obtain₃ : ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
  (hs' :
    Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
      (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))))
  (t : Finset M) (ht : Submodule.span R (↑t : Set M) = l.ker)
  (H :
    Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := M)
      (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M)),
  Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
    (LinearMap.ker (l ∘ₗ linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
Tactic: classical
  obtain ⟨s, hs, hs'⟩ := h
  obtain ⟨t, ht⟩ := hl'
  have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → M)) :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])
  apply Module.finitePresentation_of_free_of_surjective (l ∘ₗ linearCombination R Subtype.val)
    (hl.comp H)
  choose σ hσ using (show _ from H)
  have : Finsupp.linearCombination R Subtype.val '' σ '' t = t := by
    simp only [Set.image_image, hσ, Set.image_id']
  rw [LinearMap.ker_comp, ← ht, ← this, ← Submodule.map_span, Submodule.comap_map_eq,
    ← Finset.coe_image]
  exact Submodule.FG.sup ⟨_, rfl⟩ hs'
Cleared hypotheses: h, 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
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: obtain ⟨s, hs, hs'⟩ := h
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
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))))
⊢ 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.{u_3 + 1} (α := Submodule R N) (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : N) ↦ x ∈ s)))) ⊤
Tactic: rw [range_linearCombination, Subtype.range_val, ← hs]