awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.FinitePresentation
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
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)))
          ⋯)
        x)
f : M →ₗ[R]
  Finsupp.{u_3, u_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)))
        ⋯))
    R :=
  lmapDomain R R π ∘ₗ (↑b.repr : M →ₗ[R] Free.ChooseBasisIndex R M →₀ R)
⊢ (Submodule.map f l.ker).FG

Tactic:
hl'.map f

Premises used: Submodule.FG.map
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Projective R M
inst_4 : Module.Finite R M
⊢ FinitePresentation R M

Tactic:
have ⟨_n, _f, _g, surj, _, hfg⟩ := Finite.exists_comp_eq_id_of_projective R M
  Module.finitePresentation_of_free_of_surjective _ surj
    (LinearMap.ker_eq_range_of_comp_eq_id hfg ▸ .of_finite)

Premises used: Module.finitePresentation_of_free_of_surjective, Eq.rec, LinearMap.ker_eq_range_of_comp_eq_id, Module.Finite.exists_comp_eq_id_of_projective, _private.0.Module.finitePresentation_of_projective.match_1, Module.FinitePresentation, Submodule.FG.of_finite, Eq.symm
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type ?u.77863
N : Type ?u.78151
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Sort ?u.78426
inst_5 : Finite ι
⊢ Module.FinitePresentation R R

Tactic:
Module.finitePresentation_of_projective _ _

Premises used: Module.finitePresentation_of_projective
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type ?u.79077
N : Type ?u.79365
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_2
inst_5 : Finite ι
⊢ Module.FinitePresentation R (ι →₀ R)

Tactic:
Module.finitePresentation_of_projective _ _

Premises used: Module.finitePresentation_of_projective
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type ?u.80554
N : Type ?u.80842
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_2
inst_5 : Finite ι
⊢ Module.FinitePresentation R (ι → R)

Tactic:
Module.finitePresentation_of_projective _ _

Premises used: Module.finitePresentation_of_projective
-- Module: Mathlib.Algebra.Module.FinitePresentation
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

Tactic:
obtain ⟨s, hs, hs'⟩ := h
-- Module: Mathlib.Algebra.Module.FinitePresentation
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))))
obtain : ∀ (t : Finset M) (ht : Submodule.span R (↑t : Set M) = l.ker), FinitePresentation R N
⊢ FinitePresentation R N

Tactic:
obtain ⟨t, ht⟩ := hl'
-- Module: Mathlib.Algebra.Module.FinitePresentation
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
⊢ 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])
-- Module: Mathlib.Algebra.Module.FinitePresentation
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)
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))))
⊢ 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)
-- Module: Mathlib.Algebra.Module.FinitePresentation
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
⊢ (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M) '' σ '' (↑t : Set M) =
    (↑t : Set M)

Tactic:
simp only [Set.image_image, hσ, Set.image_id']

Premises used: Set.image_image, Set.image_id'
-- Module: Mathlib.Algebra.Module.FinitePresentation
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
⊢ (⇑(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']
-- Module: Mathlib.Algebra.Module.FinitePresentation
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)
rw :
  (Submodule.span R (↑(Finset.image σ t) : Set (↥s →₀ R)) ⊔
      LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))).FG
⊢ Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
    (LinearMap.ker (l ∘ₗ linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))

Tactic:
rw [LinearMap.ker_comp, ← ht, ← this, ← Submodule.map_span, Submodule.comap_map_eq,
    ← Finset.coe_image]

Premises used: Finset.coe_image, LinearMap.ker_comp, Submodule.map_span, Submodule.comap_map_eq
-- Module: Mathlib.Algebra.Module.FinitePresentation
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.span R (↑(Finset.image σ t) : Set (↥s →₀ R)) ⊔
      LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))).FG

Tactic:
Submodule.FG.sup ⟨_, rfl⟩ hs'

Premises used: Exists.intro, Submodule.FG.sup, rfl
-- Module: Mathlib.Algebra.Module.FinitePresentation
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.span R (↑(Finset.image σ t) : Set (↥s →₀ R)) ⊔
      LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))).FG

Tactic:
exact Submodule.FG.sup ⟨_, rfl⟩ hs'

Premises used: Exists.intro, Submodule.FG.sup, rfl
-- Module: Mathlib.Algebra.Module.FinitePresentation
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

Tactic:
obtain ⟨s, hs, hs'⟩ := h
-- Module: Mathlib.Algebra.Module.FinitePresentation
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)) ⊤
rw₂ rw₃ : Eq (α := Submodule R N) (Submodule.span R (↑s : Set 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)))) ⊤

Tactic:
rw [range_linearCombination, Subtype.range_val, ← hs]

Premises used: Subtype.range_val, Finsupp.range_linearCombination
-- Module: Mathlib.Algebra.Module.FinitePresentation
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))))
⊢ 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])
-- Module: Mathlib.Algebra.Module.FinitePresentation
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)
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))
⊢ ∃ (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
-- Module: Mathlib.Algebra.Module.FinitePresentation
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
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)
⊢ 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)))

Tactic:
ext
-- Module: Mathlib.Algebra.Module.FinitePresentation
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
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:
simp [hf]
-- Module: Mathlib.Algebra.Module.FinitePresentation
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
⊢ ∃ (f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M), l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))

Tactic:
exact ⟨Finsupp.linearCombination R (fun i ↦ f i), by ext; simp [hf]⟩
-- Module: Mathlib.Algebra.Module.FinitePresentation
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)
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
⊢ 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]⟩

Premises used: Membership.mem, Subtype, Finsupp.linearCombination, Subtype.val, Finsupp
-- Module: Mathlib.Algebra.Module.FinitePresentation
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))
rw : ⊤ ≤ Submodule.map f.range.mkQ l.ker
⊢ Submodule.map f.range.mkQ l.ker = ⊤

Tactic:
rw [← top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.Algebra.Module.FinitePresentation
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
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)
⊢ x ∈ Submodule.map f.range.mkQ l.ker

Tactic:
obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x

Premises used: Submodule.mkQ_surjective, rfl