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_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
⊢ Submodule.map l.ker.subtype f.range = Submodule.map l.ker.subtype ⊤
have a₇ : l.ker = l.ker
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]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
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
⊢ Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
have hf : 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
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.FG
have this : π.ker ≤ (l ∘ₗ π).ker
Tactic: have : LinearMap.ker π ≤ LinearMap.ker (l ∘ₗ π) :=
    Submodule.comap_mono (f := π) (bot_le (a := LinearMap.ker l))
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
⊢ π.ker.FG
have rw : (Submodule.map (l ∘ₗ π).ker.subtype f.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]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
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)
⊢ FinitePresentation R M
have hg : 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)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
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)
⊢ FinitePresentation R M
have this : Module.Finite R P
Tactic: have := Module.Finite.of_surjective g hg
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
⊢ FinitePresentation R M
have 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
Tactic: obtain ⟨e, rfl, rfl⟩ := ((Function.Exact.split_tfae' H).out 0 2 rfl rfl).mp
    ⟨hf, l, hl⟩
Cleared hypotheses: f, g, hl, hf, H, hg
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
have refine : (LinearMap.fst R M P ∘ₗ (↑e : N →ₗ[R] M × P)).ker.FG
Tactic: refine Module.finitePresentation_of_surjective (LinearMap.fst _ _ _ ∘ₗ e.toLinearMap)
    (Prod.fst_surjective.comp e.surjective) ?_
-- 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
ι : Sort ?u.225102
inst_5 : Finite ι
inst_6 : FinitePresentation R M
inst_7 : FinitePresentation R N
⊢ FinitePresentation R (M × N)
have hf : 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
-- 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
ι : 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))
have rw : FinitePresentation R ↥(LinearMap.range (LinearMap.inr R M N))
Tactic: rw [LinearMap.ker_fst]
-- 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
ι : 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 (M × N)
have this : 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)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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)
have refine_1 : ∀ {N : Type u_2} {N' : Type (max u_2 u_1)} [inst_10 : AddCommGroup N] [inst_11 : AddCommGroup N'] [inst_12 : Module R N]
  [inst_13 : Module R N'] (a : N ≃ₗ[R] N'),
  (fun (N : Type u_2) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N inst_10 inst_12 →
    (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N' inst_11 inst_13
Tactic: refine Module.pi_induction' (motive := fun N _ _ ↦ Module.FinitePresentation R N)
      (motive' := fun N _ _ ↦ Module.FinitePresentation R N) R ?_ ?_ ?_ ?_ M inferInstance
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 ι
refine_1 :
  ∀ {N : Type u_2} {N' : Type (max u_2 u_1)} [inst_10 : AddCommGroup N] [inst_11 : AddCommGroup N']
    [inst_12 : Module R N] [inst_13 : Module R N'] (a : N ≃ₗ[R] N'),
    (fun (N : Type u_2) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N inst_10 inst_12 →
      (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N' inst_11 inst_13
⊢ FinitePresentation R ((i : ι) → M i)
have refine_2 : ∀ {N N' : Type (max u_2 u_1)} [inst_10 : AddCommGroup N] [inst_11 : AddCommGroup N'] [inst_12 : Module R N]
  [inst_13 : Module R N'] (a : N ≃ₗ[R] N'),
  (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N inst_10 inst_12 →
    (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N' inst_11 inst_13
Tactic: refine Module.pi_induction' (motive := fun N _ _ ↦ Module.FinitePresentation R N)
      (motive' := fun N _ _ ↦ Module.FinitePresentation R N) R ?_ ?_ ?_ ?_ M inferInstance
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 ι
refine_1 :
  ∀ {N : Type u_2} {N' : Type (max u_2 u_1)} [inst_10 : AddCommGroup N] [inst_11 : AddCommGroup N']
    [inst_12 : Module R N] [inst_13 : Module R N'] (a : N ≃ₗ[R] N'),
    (fun (N : Type u_2) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N inst_10 inst_12 →
      (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N' inst_11 inst_13
refine_2 :
  ∀ {N N' : Type (max u_2 u_1)} [inst_10 : AddCommGroup N] [inst_11 : AddCommGroup N'] [inst_12 : Module R N]
    [inst_13 : Module R N'] (a : N ≃ₗ[R] N'),
    (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N inst_10 inst_12 →
      (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N' inst_11 inst_13
⊢ FinitePresentation R ((i : ι) → M i)
have refine_3 : (fun (N : Type u_2) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) PUnit.{u_2 + 1} PUnit.addCommGroup
  PUnit.module
Tactic: refine Module.pi_induction' (motive := fun N _ _ ↦ Module.FinitePresentation R N)
      (motive' := fun N _ _ ↦ Module.FinitePresentation R N) R ?_ ?_ ?_ ?_ M inferInstance
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 ι
refine_1 :
  ∀ {N : Type u_2} {N' : Type (max u_2 u_1)} [inst_10 : AddCommGroup N] [inst_11 : AddCommGroup N']
    [inst_12 : Module R N] [inst_13 : Module R N'] (a : N ≃ₗ[R] N'),
    (fun (N : Type u_2) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N inst_10 inst_12 →
      (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N' inst_11 inst_13
refine_2 :
  ∀ {N N' : Type (max u_2 u_1)} [inst_10 : AddCommGroup N] [inst_11 : AddCommGroup N'] [inst_12 : Module R N]
    [inst_13 : Module R N'] (a : N ≃ₗ[R] N'),
    (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N inst_10 inst_12 →
      (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N' inst_11 inst_13
refine_3 : FinitePresentation R PUnit.{u_2 + 1}
⊢ FinitePresentation R ((i : ι) → M i)
have refine_4 : ∀ {N : Type u_2} {N' : Type (max u_2 u_1)} [inst_10 : AddCommGroup N] [inst_11 : AddCommGroup N'] [inst_12 : Module R N]
  [inst_13 : Module R N'],
  (fun (N : Type u_2) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N inst_10 inst_12 →
    (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N' inst_11 inst_13 →
      (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) (N × N')
        Prod.instAddCommGroup Prod.instModule
Tactic: refine Module.pi_induction' (motive := fun N _ _ ↦ Module.FinitePresentation R N)
      (motive' := fun N _ _ ↦ Module.FinitePresentation R N) R ?_ ?_ ?_ ?_ M inferInstance
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
⊢ FinitePresentation R M
have obtain : ∀ (n : ℕ) (K : Submodule S (Fin n → S)) (e : M ≃ₗ[S] (Fin n → S) ⧸ K) (hK : K.FG), FinitePresentation R M
Tactic: obtain ⟨n, K, e, hK⟩ := Module.FinitePresentation.exists_fin S M
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (Fin n → S) M :=
  (↑R :
      {S M : Type u_1} →
        {M₂ : Type u_3} →
          [inst : Semiring R] →
            [inst_9 : Semiring S] →
              [inst_10 : AddCommMonoid M] →
                [inst_11 : AddCommMonoid M₂] →
                  [inst_12 : Module R M] →
                    [inst_13 : Module R M₂] →
                      [inst_14 : Module S M] →
                        [inst_15 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ)
⊢ FinitePresentation R M
have refine_1 : ∀ (m : M), ∃ (a : Fin n → S), (f : (a : Fin n → S) → M) a = m
Tactic: refine Module.finitePresentation_of_surjective f (fun m ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (Fin n → S) M :=
  (↑R :
      {S M : Type u_1} →
        {M₂ : Type u_3} →
          [inst : Semiring R] →
            [inst_9 : Semiring S] →
              [inst_10 : AddCommMonoid M] →
                [inst_11 : AddCommMonoid M₂] →
                  [inst_12 : Module R M] →
                    [inst_13 : Module R M₂] →
                      [inst_14 : Module S M] →
                        [inst_15 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ)
refine_1 : ∀ (m : M), ∃ (a : Fin n → S), (f : (a : Fin n → S) → M) a = m
⊢ FinitePresentation R M
have refine_2 : f.ker.FG
Tactic: refine Module.finitePresentation_of_surjective f (fun m ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (Fin n → S) M :=
  (↑R :
      {S M : Type u_1} →
        {M₂ : Type u_3} →
          [inst : Semiring R] →
            [inst_9 : Semiring S] →
              [inst_10 : AddCommMonoid M] →
                [inst_11 : AddCommMonoid M₂] →
                  [inst_12 : Module R M] →
                    [inst_13 : Module R M₂] →
                      [inst_14 : Module S M] →
                        [inst_15 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ)
m : M
⊢ ∃ (a : Fin n → S), (f : (a : Fin n → S) → M) a = m
have refine_1 : ∀ (a : Fin n → S)
  (ha :
    Eq (α := (Fin n → S) ⧸ K) ((K.mkQ : (a : Fin n → S) → (Fin n → S) ⧸ K) a : (Fin n → S) ⧸ K)
      ((e : (a : M) → (Fin n → S) ⧸ K) m : (Fin n → S) ⧸ K)),
  ∃ (a : Fin n → S), (f : (a : Fin n → S) → M) a = m
Tactic: obtain ⟨a, ha⟩ := K.mkQ_surjective (e m)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (Fin n → S) M :=
  (↑R :
      {S M : Type u_1} →
        {M₂ : Type u_3} →
          [inst : Semiring R] →
            [inst_9 : Semiring S] →
              [inst_10 : AddCommMonoid M] →
                [inst_11 : AddCommMonoid M₂] →
                  [inst_12 : Module R M] →
                    [inst_13 : Module R M₂] →
                      [inst_14 : Module S M] →
                        [inst_15 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ)
⊢ f.ker.FG
have this : Module.Finite S ↥(Submodule.restrictScalars R ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ).ker)
Tactic: have : Module.Finite S
        (Submodule.restrictScalars R (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ))) :=
      .of_fg <| show (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ)).FG by simpa
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (Fin n → S) M :=
  (↑R :
      {S M : Type u_1} →
        {M₂ : Type u_3} →
          [inst : Semiring R] →
            [inst_9 : Semiring S] →
              [inst_10 : AddCommMonoid M] →
                [inst_11 : AddCommMonoid M₂] →
                  [inst_12 : Module R M] →
                    [inst_13 : Module R M₂] →
                      [inst_14 : Module S M] →
                        [inst_15 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ)
this : Module.Finite S ↥(Submodule.restrictScalars R ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ).ker)
⊢ f.ker.FG
have refine_2 : Module.Finite.{u_2, u_1} R ↥(Submodule.restrictScalars R ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ).ker)
Tactic: simp only [f, LinearMap.ker_restrictScalars, ← Module.Finite.iff_fg]