awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_7 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
π : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
H : Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := M) (⇑π : (a : ↥s →₀ R) → M)
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
rw : f.range = ⊤
⊢ Function.Surjective (α := ↥(l ∘ₗ π).ker) (β := ↥l.ker) (⇑f : (a : ↥(l ∘ₗ π).ker) → ↥l.ker)

Tactic:
rw [← LinearMap.range_eq_top]

Premises used: LinearMap.range_eq_top
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_7 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
π : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
H : Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := M) (⇑π : (a : ↥s →₀ R) → M)
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
a : Submodule.map l.ker.subtype f.range = Submodule.map l.ker.subtype ⊤
⊢ f.range = ⊤

Tactic:
apply Submodule.map_injective_of_injective (Submodule.injective_subtype _)

Premises used: Submodule.injective_subtype, Submodule.map_injective_of_injective
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_7 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
π : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
H : Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := M) (⇑π : (a : ↥s →₀ R) → M)
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
a : Submodule.map l.ker.subtype f.range = l.ker.subtype.range
a₁ : Submodule.map l.ker.subtype f.range = l.ker
a₂ : (l.ker.subtype ∘ₗ f).range = l.ker
a₃ : (π ∘ₗ (l ∘ₗ π).ker.subtype).range = l.ker
a₄ : Submodule.map π (l ∘ₗ π).ker.subtype.range = l.ker
a₅ : Submodule.map π (l ∘ₗ π).ker = l.ker
a₆ : Submodule.map π (Submodule.comap π l.ker) = l.ker
a₇ a₈ : l.ker = l.ker
⊢ Submodule.map l.ker.subtype f.range = Submodule.map l.ker.subtype ⊤

Tactic:
rw [Submodule.map_top, Submodule.range_subtype, ← LinearMap.range_comp, ← e,
      LinearMap.range_comp, Submodule.range_subtype, LinearMap.ker_comp,
      Submodule.map_comap_eq_of_surjective H]

Premises used: Submodule.map_top, LinearMap.range_comp, LinearMap.ker_comp, Submodule.map_comap_eq_of_surjective, Submodule.range_subtype
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_7 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
π : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
H : Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := M) (⇑π : (a : ↥s →₀ R) → M)
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
⊢ Function.Surjective (α := ↥(l ∘ₗ π).ker) (β := ↥l.ker) (⇑f : (a : ↥(l ∘ₗ π).ker) → ↥l.ker)

Tactic:
have hf : Function.Surjective f := by
    rw [← LinearMap.range_eq_top]
    apply Submodule.map_injective_of_injective (Submodule.injective_subtype _)
    rw [Submodule.map_top, Submodule.range_subtype, ← LinearMap.range_comp, ← e,
      LinearMap.range_comp, Submodule.range_subtype, LinearMap.ker_comp,
      Submodule.map_comap_eq_of_surjective H]
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_7 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
π : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
H : Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := M) (⇑π : (a : ↥s →₀ R) → M)
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
hf : Function.Surjective (α := ↥(l ∘ₗ π).ker) (β := ↥l.ker) (⇑f : (a : ↥(l ∘ₗ π).ker) → ↥l.ker)
change : π.ker.FG
⊢ Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))

Tactic:
change (LinearMap.ker π).FG

Premises used: LinearMap.ker, Submodule.FG
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_7 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
π : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
H : Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := M) (⇑π : (a : ↥s →₀ R) → M)
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
hf : Function.Surjective (α := ↥(l ∘ₗ π).ker) (β := ↥l.ker) (⇑f : (a : ↥(l ∘ₗ π).ker) → ↥l.ker)
⊢ π.ker ≤ (l ∘ₗ π).ker

Tactic:
have : LinearMap.ker π ≤ LinearMap.ker (l ∘ₗ π) :=
    Submodule.comap_mono (f := π) (bot_le (a := LinearMap.ker l))
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_7 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
π : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
H : Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := M) (⇑π : (a : ↥s →₀ R) → M)
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
hf : Function.Surjective (α := ↥(l ∘ₗ π).ker) (β := ↥l.ker) (⇑f : (a : ↥(l ∘ₗ π).ker) → ↥l.ker)
this : π.ker ≤ (l ∘ₗ π).ker
rw : (Submodule.map (l ∘ₗ π).ker.subtype f.ker).FG
⊢ π.ker.FG

Tactic:
rw [← inf_eq_right.mpr this, ← Submodule.range_subtype (LinearMap.ker _),
    ← Submodule.map_comap_eq, ← LinearMap.ker_comp, e, LinearMap.ker_comp f,
    LinearMap.ker_eq_bot.mpr (Submodule.injective_subtype (LinearMap.ker l)), Submodule.comap_bot]

Premises used: Iff.mpr, Submodule.map_comap_eq, LinearMap.ker_eq_bot, LinearMap.ker, LinearMap.ker_comp, Submodule.injective_subtype, inf_eq_right, Submodule.range_subtype, Submodule.comap_bot
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_7 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
π : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
H : Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := M) (⇑π : (a : ↥s →₀ R) → M)
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
hf : Function.Surjective (α := ↥(l ∘ₗ π).ker) (β := ↥l.ker) (⇑f : (a : ↥(l ∘ₗ π).ker) → ↥l.ker)
this : π.ker ≤ (l ∘ₗ π).ker
⊢ (Submodule.map (l ∘ₗ π).ker.subtype f.ker).FG

Tactic:
(Module.FinitePresentation.fg_ker f hf).map (Submodule.subtype _)

Premises used: Submodule.FG.map, Submodule.subtype
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_4
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
P : Type u_1
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : FinitePresentation R N
f : M →ₗ[R] N
g : N →ₗ[R] P
l : P →ₗ[R] N
hl : g ∘ₗ l = LinearMap.id
hf : Function.Injective.{u_4 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
H : Function.Exact.{u_4, u_3, u_1} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
⊢ Function.Surjective.{u_3 + 1, u_1 + 1} (α := N) (β := P) (⇑g : (a : N) → P)

Tactic:
have hg : Function.Surjective g := Function.LeftInverse.surjective (DFunLike.congr_fun hl)
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_4
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
P : Type u_1
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : FinitePresentation R N
f : M →ₗ[R] N
g : N →ₗ[R] P
l : P →ₗ[R] N
hl : g ∘ₗ l = LinearMap.id
hf : Function.Injective.{u_4 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
H : Function.Exact.{u_4, u_3, u_1} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Function.Surjective.{u_3 + 1, u_1 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
⊢ Module.Finite R P

Tactic:
have := Module.Finite.of_surjective g hg
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_4
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
P : Type u_1
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : FinitePresentation R N
f : M →ₗ[R] N
g : N →ₗ[R] P
l : P →ₗ[R] N
hl : g ∘ₗ l = LinearMap.id
hf : Function.Injective.{u_4 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
H : Function.Exact.{u_4, u_3, u_1} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Function.Surjective.{u_3 + 1, u_1 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
this : Module.Finite R P
obtain :
  ∀ (e : N ≃ₗ[R] M × P)
    (hf :
      Function.Injective.{u_4 + 1, u_3 + 1} (α := M) (β := N)
        (⇑((↑e.symm : M × P →ₗ[R] N) ∘ₗ LinearMap.inl R M P) : (a : M) → N))
    (hl : (LinearMap.snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) ∘ₗ l = LinearMap.id)
    (hg :
      Function.Surjective.{u_3 + 1, u_1 + 1} (α := N) (β := P)
        (⇑(LinearMap.snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P))
    (H :
      Function.Exact.{u_4, u_3, u_1} (M := M) (N := N) (P := P)
        (⇑((↑e.symm : M × P →ₗ[R] N) ∘ₗ LinearMap.inl R M P) : (a : M) → N)
        (⇑(LinearMap.snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P)),
    FinitePresentation R M
⊢ FinitePresentation R M

Tactic:
obtain ⟨e, rfl, rfl⟩ := ((Function.Exact.split_tfae' H).out 0 2 rfl rfl).mp
    ⟨hf, l, hl⟩

Premises used: Function.Exact.split_tfae', List.TFAE.out, And.intro, Exists.intro, Iff.mp, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_4
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
P : Type u_1
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : FinitePresentation R N
l : P →ₗ[R] N
this : Module.Finite R P
e : N ≃ₗ[R] M × P
hf :
  Function.Injective.{u_4 + 1, u_3 + 1} (α := M) (β := N)
    (⇑((↑e.symm : M × P →ₗ[R] N) ∘ₗ LinearMap.inl R M P) : (a : M) → N)
hl : (LinearMap.snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) ∘ₗ l = LinearMap.id
hg :
  Function.Surjective.{u_3 + 1, u_1 + 1} (α := N) (β := P)
    (⇑(LinearMap.snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P)
H :
  Function.Exact.{u_4, u_3, u_1} (M := M) (N := N) (P := P)
    (⇑((↑e.symm : M × P →ₗ[R] N) ∘ₗ LinearMap.inl R M P) : (a : M) → N)
    (⇑(LinearMap.snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P)
⊢ FinitePresentation R M

Tactic:
Module.finitePresentation_of_surjective (LinearMap.fst _ _ _ ∘ₗ e.toLinearMap)
    (Prod.fst_surjective.comp e.surjective) ?_

Premises used: LinearMap.fst, Prod.fst_surjective, LinearEquiv.surjective, Module.finitePresentation_of_surjective, LinearMap.comp, LinearEquiv.toLinearMap, Function.Surjective.comp
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_4
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
P : Type u_1
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : FinitePresentation R N
l : P →ₗ[R] N
this : Module.Finite R P
e : N ≃ₗ[R] M × P
hf :
  Function.Injective.{u_4 + 1, u_3 + 1} (α := M) (β := N)
    (⇑((↑e.symm : M × P →ₗ[R] N) ∘ₗ LinearMap.inl R M P) : (a : M) → N)
hl : (LinearMap.snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) ∘ₗ l = LinearMap.id
hg :
  Function.Surjective.{u_3 + 1, u_1 + 1} (α := N) (β := P)
    (⇑(LinearMap.snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P)
H :
  Function.Exact.{u_4, u_3, u_1} (M := M) (N := N) (P := P)
    (⇑((↑e.symm : M × P →ₗ[R] N) ∘ₗ LinearMap.inl R M P) : (a : M) → N)
    (⇑(LinearMap.snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P)
refine : (LinearMap.fst R M P ∘ₗ (↑e : N →ₗ[R] M × P)).ker.FG
⊢ FinitePresentation R M

Tactic:
refine Module.finitePresentation_of_surjective (LinearMap.fst _ _ _ ∘ₗ e.toLinearMap)
    (Prod.fst_surjective.comp e.surjective) ?_

Premises used: LinearMap.fst, Prod.fst_surjective, LinearEquiv.surjective, Module.finitePresentation_of_surjective, LinearMap.comp, LinearEquiv.toLinearMap, Function.Surjective.comp
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_4
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
P : Type u_1
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : FinitePresentation R N
l : P →ₗ[R] N
this : Module.Finite R P
e : N ≃ₗ[R] M × P
hf :
  Function.Injective.{u_4 + 1, u_3 + 1} (α := M) (β := N)
    (⇑((↑e.symm : M × P →ₗ[R] N) ∘ₗ LinearMap.inl R M P) : (a : M) → N)
hl : (LinearMap.snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) ∘ₗ l = LinearMap.id
hg :
  Function.Surjective.{u_3 + 1, u_1 + 1} (α := N) (β := P)
    (⇑(LinearMap.snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P)
H :
  Function.Exact.{u_4, u_3, u_1} (M := M) (N := N) (P := P)
    (⇑((↑e.symm : M × P →ₗ[R] N) ∘ₗ LinearMap.inl R M P) : (a : M) → N)
    (⇑(LinearMap.snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P)
⊢ ((↑e.symm : M × P →ₗ[R] N) ∘ₗ LinearMap.inr R M P).range.FG

Tactic:
Submodule.fg_range _

Premises used: Submodule.fg_range
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_4
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
P : Type u_1
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : FinitePresentation R N
l : P →ₗ[R] N
this : Module.Finite R P
e : N ≃ₗ[R] M × P
hf :
  Function.Injective.{u_4 + 1, u_3 + 1} (α := M) (β := N)
    (⇑((↑e.symm : M × P →ₗ[R] N) ∘ₗ LinearMap.inl R M P) : (a : M) → N)
hl : (LinearMap.snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) ∘ₗ l = LinearMap.id
hg :
  Function.Surjective.{u_3 + 1, u_1 + 1} (α := N) (β := P)
    (⇑(LinearMap.snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P)
H :
  Function.Exact.{u_4, u_3, u_1} (M := M) (N := N) (P := P)
    (⇑((↑e.symm : M × P →ₗ[R] N) ∘ₗ LinearMap.inl R M P) : (a : M) → N)
    (⇑(LinearMap.snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P)
⊢ ((↑e.symm : M × P →ₗ[R] N) ∘ₗ LinearMap.inr R M P).range.FG

Tactic:
exact Submodule.fg_range _

Premises used: Submodule.fg_range
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_4
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
P : Type u_1
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : FinitePresentation R N
inst_8 : Projective R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective.{u_4 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_1 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
H : Function.Exact.{u_4, u_3, u_1} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
⊢ FinitePresentation R M

Tactic:
have ⟨l, hl⟩ := Module.projective_lifting_property g .id hg
  Module.finitePresentation_of_split_exact f g l hl hf H

Premises used: LinearMap.id, _private.0.Module.finitePresentation_of_projective_of_exact.match_1, Module.finitePresentation_of_split_exact, Module.FinitePresentation, Module.projective_lifting_property
-- 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
e : M ≃ₗ[R] N
inst_5 : FinitePresentation R M
⊢ FinitePresentation R N

Tactic:
simp [← Module.FinitePresentation.fg_ker_iff e.toLinearMap e.surjective, Submodule.fg_bot]

Premises used: LinearEquiv.surjective, LinearEquiv.toLinearMap, Module.FinitePresentation.fg_ker_iff, Submodule.fg_bot
-- 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
e : M ≃ₗ[R] N
⊢ Module.FinitePresentation R M ↔ Module.FinitePresentation R N

Tactic:
⟨fun _ ↦ .of_equiv e, fun _ ↦ .of_equiv e.symm⟩

Premises used: LinearEquiv.symm, Module.FinitePresentation.of_equiv, Iff.intro
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_1
N : Type ?u.221690
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Sort ?u.221965
inst_5 : Finite ι
inst_6 : Subsingleton M
⊢ FinitePresentation R M

Tactic:
.of_equiv (default : (Fin 0 → R) ≃ₗ[R] M)

Premises used: Inhabited.default, Module.FinitePresentation.of_equiv
-- 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
ι : Sort ?u.225102
inst_5 : Finite ι
inst_6 : FinitePresentation R M
inst_7 : FinitePresentation R N
⊢ Function.Surjective (α := M × N) (β := M) (⇑(LinearMap.fst R M N) : (a : M × N) → M)

Tactic:
have hf : Function.Surjective (LinearMap.fst R M N) := LinearMap.fst_surjective
-- 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
ι : Sort ?u.225102
inst_5 : Finite ι
inst_6 : FinitePresentation R M
inst_7 : FinitePresentation R N
hf : Function.Surjective (α := M × N) (β := M) (⇑(LinearMap.fst R M N) : (a : M × N) → M)
rw : FinitePresentation R ↥(LinearMap.range (LinearMap.inr R M N))
⊢ FinitePresentation R ↥(LinearMap.ker (LinearMap.fst R M N))

Tactic:
rw [LinearMap.ker_fst]

Premises used: LinearMap.ker_fst
-- 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
ι : Sort ?u.225102
inst_5 : Finite ι
inst_6 : FinitePresentation R M
inst_7 : FinitePresentation R N
hf : Function.Surjective (α := M × N) (β := M) (⇑(LinearMap.fst R M N) : (a : M × N) → M)
⊢ FinitePresentation R ↥(LinearMap.range (LinearMap.inr R M N))

Tactic:
.of_equiv (LinearEquiv.ofInjective (LinearMap.inr R M N) LinearMap.inr_injective)

Premises used: LinearMap.inr_injective, Module.FinitePresentation.of_equiv, LinearEquiv.ofInjective, LinearMap.inr
-- 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
ι : Sort ?u.225102
inst_5 : Finite ι
inst_6 : FinitePresentation R M
inst_7 : FinitePresentation R N
hf : Function.Surjective (α := M × N) (β := M) (⇑(LinearMap.fst R M N) : (a : M × N) → M)
⊢ FinitePresentation R ↥(LinearMap.range (LinearMap.inr R M N))

Tactic:
exact .of_equiv (LinearEquiv.ofInjective (LinearMap.inr R M N) LinearMap.inr_injective)
-- 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
ι : Sort ?u.225102
inst_5 : Finite ι
inst_6 : FinitePresentation R M
inst_7 : FinitePresentation R N
hf : Function.Surjective (α := M × N) (β := M) (⇑(LinearMap.fst R M N) : (a : M × N) → M)
⊢ FinitePresentation R ↥(LinearMap.ker (LinearMap.fst R M N))

Tactic:
have : FinitePresentation R ↥(LinearMap.ker (LinearMap.fst R M N)) := by
    rw [LinearMap.ker_fst]
    exact .of_equiv (LinearEquiv.ofInjective (LinearMap.inr R M N) LinearMap.inr_injective)
-- 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
ι : Sort ?u.225102
inst_5 : Finite ι
inst_6 : FinitePresentation R M
inst_7 : FinitePresentation R N
hf : Function.Surjective (α := M × N) (β := M) (⇑(LinearMap.fst R M N) : (a : M × N) → M)
this : FinitePresentation R ↥(LinearMap.ker (LinearMap.fst R M N))
⊢ FinitePresentation R (M × N)

Tactic:
apply Module.finitePresentation_of_ker (.fst R M N) hf

Premises used: LinearMap.fst, Module.finitePresentation_of_ker
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M_1 : Type ?u.229890
N : Type ?u.230178
inst : Ring R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
ι_1 : Sort ?u.230453
inst_5 : Finite ι_1
ι : Type u_1
M : ι → Type u_2
inst_6 : (i : ι) → AddCommGroup (M i)
inst_7 : (i : ι) → Module.{u_3, u_2} R (M i)
inst_8 : ∀ (i : ι), FinitePresentation.{u_3, u_2} R (M i)
inst_9 : Finite ι
⊢ FinitePresentation R ((i : ι) → M i)

Tactic:
Module.pi_induction' (motive := fun N _ _ ↦ Module.FinitePresentation R N)
      (motive' := fun N _ _ ↦ Module.FinitePresentation R N) R ?_ ?_ ?_ ?_ M inferInstance

Premises used: inferInstance, Module.FinitePresentation, Module.pi_induction'