awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f
A : Type u_1
inst_8 : CommRing A
inst_9 : Algebra R A
inst_10 : Module.FinitePresentation R M
⊢ Module.FinitePresentation A (A ⊗[R] M)
have obtain : ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
  (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)),
  Module.FinitePresentation A (A ⊗[R] M)
Tactic: obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f_1 : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f_1
A : Type u_1
inst_8 : CommRing A
inst_9 : Algebra R A
inst_10 : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
⊢ Module.FinitePresentation A (A ⊗[R] M)
have inst : Module.FinitePresentation A (A ⊗[R] (Fin n → R))
Tactic: have inst := Module.finitePresentation_of_projective A (A ⊗[R] (Fin n → R))
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : AddCommGroup N'
inst_7 : Module R N'
S : Submonoid R
f_1 : N →ₗ[R] N'
inst_8 : IsLocalizedModule S f_1
A : Type u_1
inst_9 : CommRing A
inst_10 : Algebra R A
inst_11 : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
inst : Module.FinitePresentation A (A ⊗[R] (Fin n → R))
⊢ Module.FinitePresentation A (A ⊗[R] M)
have apply : Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.ker (LinearMap.baseChange A f))
Tactic: apply Module.finitePresentation_of_surjective (f.baseChange A)
    (LinearMap.lTensor_surjective A hf)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : AddCommGroup N'
inst_7 : Module R N'
S : Submonoid R
f_1 : N →ₗ[R] N'
inst_8 : IsLocalizedModule S f_1
A : Type u_1
inst_9 : CommRing A
inst_10 : Algebra R A
inst_11 : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
inst : Module.FinitePresentation A (A ⊗[R] (Fin n → R))
⊢ Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.ker (LinearMap.baseChange A f))
have this : Function.Exact (M := A ⊗[R] ↥f.ker) (N := A ⊗[R] (Fin n → R)) (P := A ⊗[R] M)
  (⇑(LinearMap.baseChange A f.ker.subtype) : (a : A ⊗[R] ↥f.ker) → A ⊗[R] (Fin n → R))
  (⇑(LinearMap.baseChange A f) : (a : A ⊗[R] (Fin n → R)) → A ⊗[R] M)
Tactic: have : Function.Exact ((LinearMap.ker f).subtype.baseChange A) (f.baseChange A) :=
    lTensor_exact A f.exact_subtype_ker_map hf
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : AddCommGroup N'
inst_7 : Module R N'
S : Submonoid R
f_1 : N →ₗ[R] N'
inst_8 : IsLocalizedModule S f_1
A : Type u_1
inst_9 : CommRing A
inst_10 : Algebra R A
inst_11 : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
inst : Module.FinitePresentation A (A ⊗[R] (Fin n → R))
this :
  Function.Exact (M := A ⊗[R] ↥f.ker) (N := A ⊗[R] (Fin n → R)) (P := A ⊗[R] M)
    (⇑(LinearMap.baseChange A f.ker.subtype) : (a : A ⊗[R] ↥f.ker) → A ⊗[R] (Fin n → R))
    (⇑(LinearMap.baseChange A f) : (a : A ⊗[R] (Fin n → R)) → A ⊗[R] M)
⊢ Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.ker (LinearMap.baseChange A f))
have this₁ : Eq (α := Submodule A (A ⊗[R] (Fin n → R))) (LinearMap.ker (LinearMap.baseChange A f))
  (LinearMap.range (LinearMap.baseChange A f.ker.subtype))
Tactic: rw [LinearMap.exact_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : AddCommGroup N'
inst_7 : Module R N'
S : Submonoid R
f_1 : N →ₗ[R] N'
inst_8 : IsLocalizedModule S f_1
A : Type u_1
inst_9 : CommRing A
inst_10 : Algebra R A
inst_11 : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
inst : Module.FinitePresentation A (A ⊗[R] (Fin n → R))
this :
  Eq (α := Submodule A (A ⊗[R] (Fin n → R))) (LinearMap.ker (LinearMap.baseChange A f))
    (LinearMap.range (LinearMap.baseChange A f.ker.subtype))
⊢ Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.ker (LinearMap.baseChange A f))
have rw : Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.range (LinearMap.baseChange A f.ker.subtype))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : AddCommGroup N'
inst_7 : Module R N'
S : Submonoid R
f_1 : N →ₗ[R] N'
inst_8 : IsLocalizedModule S f_1
A : Type u_1
inst_9 : CommRing A
inst_10 : Algebra R A
inst_11 : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
inst : Module.FinitePresentation A (A ⊗[R] (Fin n → R))
this :
  Eq (α := Submodule A (A ⊗[R] (Fin n → R))) (LinearMap.ker (LinearMap.baseChange A f))
    (LinearMap.range (LinearMap.baseChange A f.ker.subtype))
⊢ Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.range (LinearMap.baseChange A f.ker.subtype))
have this₁ : Module.Finite R ↥f.ker
Tactic: have : Module.Finite R (LinearMap.ker f) :=
    .of_fg (Module.FinitePresentation.fg_ker f hf)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f
A : Type u_1
inst_8 : CommRing A
inst_9 : Algebra R A
inst_10 : Module.FinitePresentation R M
⊢ Module.FinitePresentation A (A ⊗[R] M)
have obtain : ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
  (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)),
  Module.FinitePresentation A (A ⊗[R] M)
Tactic: classical
  obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
  have inst := Module.finitePresentation_of_projective A (A ⊗[R] (Fin n → R))
  apply Module.finitePresentation_of_surjective (f.baseChange A)
    (LinearMap.lTensor_surjective A hf)
  have : Function.Exact ((LinearMap.ker f).subtype.baseChange A) (f.baseChange A) :=
    lTensor_exact A f.exact_subtype_ker_map hf
  rw [LinearMap.exact_iff] at this
  rw [this]
  have : Module.Finite R (LinearMap.ker f) :=
    .of_fg (Module.FinitePresentation.fg_ker f hf)
  exact Submodule.fg_range _
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f
A : Type u_1
inst_8 : CommRing A
inst_9 : Algebra R A
inst_10 : Module.FinitePresentation R M
obtain :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)),
    Module.FinitePresentation A (A ⊗[R] M)
⊢ Module.FinitePresentation A (A ⊗[R] M)
have obtain₁ : ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
  (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
  (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R))), Module.FinitePresentation A (A ⊗[R] M)
Tactic: classical
  obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
  have inst := Module.finitePresentation_of_projective A (A ⊗[R] (Fin n → R))
  apply Module.finitePresentation_of_surjective (f.baseChange A)
    (LinearMap.lTensor_surjective A hf)
  have : Function.Exact ((LinearMap.ker f).subtype.baseChange A) (f.baseChange A) :=
    lTensor_exact A f.exact_subtype_ker_map hf
  rw [LinearMap.exact_iff] at this
  rw [this]
  have : Module.Finite R (LinearMap.ker f) :=
    .of_fg (Module.FinitePresentation.fg_ker f hf)
  exact Submodule.fg_range _
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f
A : Type u_1
inst_8 : CommRing A
inst_9 : Algebra R A
inst_10 : Module.FinitePresentation R M
obtain :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)),
    Module.FinitePresentation A (A ⊗[R] M)
obtain₁ :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
    (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R))), Module.FinitePresentation A (A ⊗[R] M)
⊢ Module.FinitePresentation A (A ⊗[R] M)
have obtain₂ : ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
  (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
  (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R))),
  Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.ker (LinearMap.baseChange A f))
Tactic: classical
  obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
  have inst := Module.finitePresentation_of_projective A (A ⊗[R] (Fin n → R))
  apply Module.finitePresentation_of_surjective (f.baseChange A)
    (LinearMap.lTensor_surjective A hf)
  have : Function.Exact ((LinearMap.ker f).subtype.baseChange A) (f.baseChange A) :=
    lTensor_exact A f.exact_subtype_ker_map hf
  rw [LinearMap.exact_iff] at this
  rw [this]
  have : Module.Finite R (LinearMap.ker f) :=
    .of_fg (Module.FinitePresentation.fg_ker f hf)
  exact Submodule.fg_range _
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f
A : Type u_1
inst_8 : CommRing A
inst_9 : Algebra R A
inst_10 : Module.FinitePresentation R M
obtain :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)),
    Module.FinitePresentation A (A ⊗[R] M)
obtain₁ :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
    (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R))), Module.FinitePresentation A (A ⊗[R] M)
obtain₂ :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
    (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R))),
    Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.ker (LinearMap.baseChange A f))
⊢ Module.FinitePresentation A (A ⊗[R] M)
have obtain₃ : ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
  (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
  (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R)))
  (this :
    Function.Exact (M := A ⊗[R] ↥f.ker) (N := A ⊗[R] (Fin n → R)) (P := A ⊗[R] M)
      (⇑(LinearMap.baseChange A f.ker.subtype) : (a : A ⊗[R] ↥f.ker) → A ⊗[R] (Fin n → R))
      (⇑(LinearMap.baseChange A f) : (a : A ⊗[R] (Fin n → R)) → A ⊗[R] M)),
  Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.ker (LinearMap.baseChange A f))
Tactic: classical
  obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
  have inst := Module.finitePresentation_of_projective A (A ⊗[R] (Fin n → R))
  apply Module.finitePresentation_of_surjective (f.baseChange A)
    (LinearMap.lTensor_surjective A hf)
  have : Function.Exact ((LinearMap.ker f).subtype.baseChange A) (f.baseChange A) :=
    lTensor_exact A f.exact_subtype_ker_map hf
  rw [LinearMap.exact_iff] at this
  rw [this]
  have : Module.Finite R (LinearMap.ker f) :=
    .of_fg (Module.FinitePresentation.fg_ker f hf)
  exact Submodule.fg_range _
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f
A : Type u_1
inst_8 : CommRing A
inst_9 : Algebra R A
inst_10 : Module.FinitePresentation R M
obtain :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)),
    Module.FinitePresentation A (A ⊗[R] M)
obtain₁ :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
    (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R))), Module.FinitePresentation A (A ⊗[R] M)
obtain₂ :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
    (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R))),
    Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.ker (LinearMap.baseChange A f))
obtain₃ :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
    (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R)))
    (this :
      Function.Exact (M := A ⊗[R] ↥f.ker) (N := A ⊗[R] (Fin n → R)) (P := A ⊗[R] M)
        (⇑(LinearMap.baseChange A f.ker.subtype) : (a : A ⊗[R] ↥f.ker) → A ⊗[R] (Fin n → R))
        (⇑(LinearMap.baseChange A f) : (a : A ⊗[R] (Fin n → R)) → A ⊗[R] M)),
    Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.ker (LinearMap.baseChange A f))
⊢ Module.FinitePresentation A (A ⊗[R] M)
have obtain₄ : ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
  (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
  (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R)))
  (this :
    Eq (α := Submodule A (A ⊗[R] (Fin n → R))) (LinearMap.ker (LinearMap.baseChange A f))
      (LinearMap.range (LinearMap.baseChange A f.ker.subtype))),
  Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.ker (LinearMap.baseChange A f))
Tactic: classical
  obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
  have inst := Module.finitePresentation_of_projective A (A ⊗[R] (Fin n → R))
  apply Module.finitePresentation_of_surjective (f.baseChange A)
    (LinearMap.lTensor_surjective A hf)
  have : Function.Exact ((LinearMap.ker f).subtype.baseChange A) (f.baseChange A) :=
    lTensor_exact A f.exact_subtype_ker_map hf
  rw [LinearMap.exact_iff] at this
  rw [this]
  have : Module.Finite R (LinearMap.ker f) :=
    .of_fg (Module.FinitePresentation.fg_ker f hf)
  exact Submodule.fg_range _
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f
h : FinitePresentation R M
g : M →ₗ[R] N'
⊢ ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = s • g
have obtain : ∀ (σ : Finset M) (hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤)
  (τ : Finset (Finsupp.{u_2, u_1} (↥σ) R))
  (hτ :
    Submodule.span R (↑τ : Set (↥σ →₀ R)) =
      LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ σ)))),
  ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = s • g
Tactic: obtain ⟨σ, hσ, τ, hτ⟩ := 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_4
N' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤
τ : Finset (Finsupp.{u_2, u_1} (↥σ) R)
hτ :
  Submodule.span R (↑τ : Set (↥σ →₀ R)) = LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ σ)))
π : Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ σ))
⊢ π.range = ⊤
have rw : Eq.{u_2 + 1} (α := Submodule R M) (Submodule.span R (Set.range (ι := ↥σ) (Subtype.val (p := fun (x : M) ↦ x ∈ σ)))) ⊤
Tactic: rw [range_linearCombination, Subtype.range_val, ← hσ]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤
τ : Finset (Finsupp.{u_2, u_1} (↥σ) R)
hτ :
  Submodule.span R (↑τ : Set (↥σ →₀ R)) = LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ σ)))
π : Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ σ))
rw :
  Eq.{u_2 + 1} (α := Submodule R M) (Submodule.span R (Set.range (ι := ↥σ) (Subtype.val (p := fun (x : M) ↦ x ∈ σ)))) ⊤
rw₁ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤
⊢ π.range = ⊤
have rw₂ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) (Submodule.span R (↑σ : Set M))
Tactic: rw [range_linearCombination, Subtype.range_val, ← hσ]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤
τ : Finset (Finsupp.{u_2, u_1} (↥σ) R)
hτ :
  Submodule.span R (↑τ : Set (↥σ →₀ R)) = LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ σ)))
π : Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ σ))
⊢ ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = s • g
have hπ : Function.Surjective (α := Finsupp.{u_2, u_1} (↥σ) R) (β := M) (⇑π : (a : ↥σ →₀ R) → M)
Tactic: have hπ : Function.Surjective π :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hσ])
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤
τ : Finset (Finsupp.{u_2, u_1} (↥σ) R)
hτ :
  Submodule.span R (↑τ : Set (↥σ →₀ R)) = LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ σ)))
π : Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ σ))
hπ : Function.Surjective (α := Finsupp.{u_2, u_1} (↥σ) R) (β := M) (⇑π : (a : ↥σ →₀ R) → M)
⊢ ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = s • g
have choose : ∀ (s : (y : N') → Prod.{u_4, u_1} N ↥S) (hs : ∀ (y : N'), (s y).2 • y = (f : (a : N) → N') (s y).1),
  ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = s • g
Tactic: choose s hs using IsLocalizedModule.surj S f
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤
τ : Finset (Finsupp.{u_2, u_1} (↥σ) R)
hτ :
  Submodule.span R (↑τ : Set (↥σ →₀ R)) = LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ σ)))
π : Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ σ))
hπ : Function.Surjective (α := Finsupp.{u_2, u_1} (↥σ) R) (β := M) (⇑π : (a : ↥σ →₀ R) → M)
s : (y : N') → Prod.{u_4, u_1} N ↥S
hs : ∀ (y : N'), (s y).2 • y = (f : (a : N) → N') (s y).1
i : ↥σ → N :=
  fun (x : ↥σ) ↦
    HSMul.hSMul.{u_1, u_4, u_4} (α := ↥S) (∏ j ∈ σ.erase (↑x : M), (s ((g : (a : M) → N') j)).2)
      (s ((g : (a : M) → N') (↑x : M))).1
s₀ : ↥S := ∏ j ∈ σ, (s ((g : (a : M) → N') j)).2
⊢ f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
have h : ∀ (j : ↥σ),
  Eq.{u_3 + 1} (α := N') (((f ∘ₗ linearCombination R i) ∘ₗ lsingle j : (a : R) → N') 1 : N')
    ((((s₀ • g) ∘ₗ π) ∘ₗ lsingle j : (a : R) → N') 1 : N')
Tactic: ext j