awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_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
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')
have h : HSMul.hSMul.{u_1, u_3, u_3} (α := ↥S) (∏ j ∈ σ.erase (↑j : M), (s ((g : (a : M) → N') j)).2)
    (HSMul.hSMul (β := N') (s ((g : (a : M) → N') (↑j : M))).2 ((g : (a : M) → N') (↑j : M) : N')) =
  HSMul.hSMul.{u_1, u_3, u_3} (α := ↥S) (β := N') (∏ j ∈ σ, (s ((g : (a : M) → N') j)).2)
    ((g : (a : M) → N') (↑j : M) : N')
Tactic: simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply,
      linearCombination_single, one_smul, LinearMap.map_smul_of_tower, ← hs, LinearMap.smul_apply,
      i, s₀, π]
-- 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
j : ↥σ
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := ↥S) (∏ j ∈ σ.erase (↑j : M), (s ((g : (a : M) → N') j)).2)
      (HSMul.hSMul (β := N') (s ((g : (a : M) → N') (↑j : M))).2 ((g : (a : M) → N') (↑j : M) : N')) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := ↥S) (β := N') (∏ j ∈ σ, (s ((g : (a : M) → N') j)).2)
      ((g : (a : M) → N') (↑j : M) : N')
have h : (↑j : M) ∈ σ
Tactic: rw [← mul_smul, Finset.prod_erase_mul]
-- 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π : 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
⊢ ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = s • g
have hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
Tactic: have hi : f ∘ₗ Finsupp.linearCombination R i = (s₀ • g) ∘ₗ π := by
    ext j
    simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply,
      linearCombination_single, one_smul, LinearMap.map_smul_of_tower, ← hs, LinearMap.smul_apply,
      i, s₀, π]
    rw [← mul_smul, Finset.prod_erase_mul]
    exact j.prop
-- 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
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
x : ↥τ
⊢ ∃ (s : ↥S), HSMul.hSMul (β := N) s ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = 0
have h : Eq.{u_1 + 1} (α := ↥S → Prop)
  (fun (s : ↥S) ↦ HSMul.hSMul (β := N) s ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = 0)
  fun (s : ↥S) ↦
  HSMul.hSMul (β := N) s ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = HSMul.hSMul (β := N) s 0
Tactic: convert_to ∃ s : S, s • (Finsupp.linearCombination R i x) = s • 0
-- 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
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
x : ↥τ
h :
  Eq.{u_1 + 1} (α := ↥S → Prop)
    (fun (s : ↥S) ↦ HSMul.hSMul (β := N) s ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = 0)
    fun (s : ↥S) ↦
    HSMul.hSMul (β := N) s ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = HSMul.hSMul (β := N) s 0
⊢ ∃ (s : ↥S), HSMul.hSMul (β := N) s ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = 0
have convert_to : ∃ (s : ↥S),
  HSMul.hSMul (β := N) s ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = HSMul.hSMul (β := N) s 0
Tactic: convert_to ∃ s : S, s • (Finsupp.linearCombination R i x) = s • 0
-- 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
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
x : ↥τ
⊢ ∃ (s : ↥S),
    HSMul.hSMul (β := N) s ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = HSMul.hSMul (β := N) s 0
have apply : Eq.{u_3 + 1} (α := N') ((f : (a : N) → N') ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) : N')
  ((f : (a : N) → N') 0 : N')
Tactic: apply IsLocalizedModule.exists_of_eq (S := S) (f := 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
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
x : ↥τ
⊢ Eq.{u_3 + 1} (α := N') ((f : (a : N) → N') ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) : N')
    ((f : (a : N) → N') 0 : N')
have rw : Eq.{u_3 + 1} (α := N') ((s₀ • g : (a : M) → N') ((π : (a : ↥σ →₀ R) → M) (↑x : ↥σ →₀ R) : M) : N') (0 : N')
Tactic: rw [← LinearMap.comp_apply, map_zero, hi, LinearMap.comp_apply]
-- 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
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
x : ↥τ
⊢ Eq.{u_3 + 1} (α := N') ((s₀ • g : (a : M) → N') ((π : (a : ↥σ →₀ R) → M) (↑x : ↥σ →₀ R) : M) : N') (0 : N')
have h : Eq.{u_2 + 1} (α := M) ((π : (a : ↥σ →₀ R) → M) (↑x : ↥σ →₀ R) : M) (0 : M)
Tactic: convert! map_zero (s₀ • g)
-- 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
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
x : ↥τ
⊢ Eq.{u_2 + 1} (α := M) ((π : (a : ↥σ →₀ R) → M) (↑x : ↥σ →₀ R) : M) (0 : M)
have h : Membership.mem (γ := Submodule R (Finsupp.{u_2, u_1} (↥σ) R)) (Submodule.span R (↑τ : Set (↥σ →₀ R))) (↑x : ↥σ →₀ R)
Tactic: rw [← LinearMap.mem_ker, ← 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π : 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
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
⊢ ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = s • g
have this : ∀ (x : ↥τ), ∃ (s : ↥S), HSMul.hSMul (β := N) s ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = 0
Tactic: have : ∀ x : τ, ∃ s : S, s • (Finsupp.linearCombination R i x) = 0 := by
    intro x
    convert_to ∃ s : S, s • (Finsupp.linearCombination R i x) = s • 0
    · simp only [smul_zero]
    apply IsLocalizedModule.exists_of_eq (S := S) (f := f)
    rw [← LinearMap.comp_apply, map_zero, hi, LinearMap.comp_apply]
    convert! map_zero (s₀ • g)
    rw [← LinearMap.mem_ker, ← hτ]
    exact Submodule.subset_span x.prop
-- 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
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
this :
  ∀ (x : ↥τ), ∃ (s : ↥S), HSMul.hSMul (β := N) s ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = 0
⊢ ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = s • g
have choose : ∀ (s' : (x : ↥τ) → ↥S)
  (hs' : ∀ (x : ↥τ), HSMul.hSMul (β := N) (s' x) ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = 0),
  ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = s • g
Tactic: choose s' hs' using this
Cleared hypotheses: this
-- 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
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
s' : (x : ↥τ) → ↥S
hs' : ∀ (x : ↥τ), HSMul.hSMul (β := N) (s' x) ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = 0
s₁ : ↥S := ∏ i : ↥τ, s' i
⊢ π.ker ≤ (HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)).ker
have rw : (↑τ : Set (↥σ →₀ R)) ⊆
  (↑(HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)).ker : Set (↥σ →₀ R))
Tactic: rw [← hτ, Submodule.span_le]
-- 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
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
s' : (x : ↥τ) → ↥S
hs' : ∀ (x : ↥τ), HSMul.hSMul (β := N) (s' x) ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = 0
s₁ : ↥S := ∏ i : ↥τ, s' i
x : Finsupp.{u_2, u_1} (↥σ) R
hxσ : x ∈ (↑τ : Set (↥σ →₀ R))
⊢ x ∈
    (↑(HSMul.hSMul (α := ↥S) (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) (∏ i : ↥τ, s' i) (linearCombination R i)).ker :
      Set (↥σ →₀ R))
have rw : HSMul.hSMul.{u_1, u_4, u_4} (α := ↥S)
    (∏ x ∈ Finset.erase Finset.univ (Subtype.mk (p := fun (x : Finsupp.{u_2, u_1} (↥σ) R) ↦ x ∈ τ) x hxσ), s' x)
    (HSMul.hSMul (β := N) (s' (Subtype.mk (p := fun (x : Finsupp.{u_2, u_1} (↥σ) R) ↦ x ∈ τ) x hxσ))
      ((linearCombination R i : (a : ↥σ →₀ R) → N) x : N)) =
  0
Tactic: rw [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.smul_apply,
      ← Finset.prod_erase_mul _ _ (Finset.mem_univ ⟨x, hxσ⟩), mul_smul]
-- 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
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
s' : (x : ↥τ) → ↥S
hs' : ∀ (x : ↥τ), HSMul.hSMul (β := N) (s' x) ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = 0
s₁ : ↥S := ∏ i : ↥τ, s' i
x : Finsupp.{u_2, u_1} (↥σ) R
hxσ : x ∈ (↑τ : Set (↥σ →₀ R))
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := ↥S)
      (∏ x ∈ Finset.erase Finset.univ (Subtype.mk (p := fun (x : Finsupp.{u_2, u_1} (↥σ) R) ↦ x ∈ τ) x hxσ), s' x)
      (HSMul.hSMul (β := N) (s' (Subtype.mk (p := fun (x : Finsupp.{u_2, u_1} (↥σ) R) ↦ x ∈ τ) x hxσ))
        ((linearCombination R i : (a : ↥σ →₀ R) → N) x : N)) =
    0
have h : HSMul.hSMul (β := N) (s' (Subtype.mk (p := fun (x : Finsupp.{u_2, u_1} (↥σ) R) ↦ x ∈ τ) x hxσ))
    ((linearCombination R i : (a : ↥σ →₀ R) → N) x : N) =
  0
Tactic: convert! smul_zero _