awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ∘ₗ π
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
⊢ ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = s • g
have this : π.ker ≤ (HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)).ker
Tactic: have : LinearMap.ker π ≤ LinearMap.ker (s₁ • Finsupp.linearCombination R i) := by
    rw [← hτ, Submodule.span_le]
    intro x hxσ
    simp only [s₁]
    rw [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.smul_apply,
      ← Finset.prod_erase_mul _ _ (Finset.mem_univ ⟨x, hxσ⟩), mul_smul]
    convert! smul_zero _
    exact hs' ⟨x, hxσ⟩
-- 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
this : π.ker ≤ (HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)).ker
⊢ ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = s • g
have refine : f ∘ₗ
    π.ker.liftQ (HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)) this ∘ₗ
      (↑(LinearEquiv.symm (π.quotKerEquivOfSurjective hπ)) : M →ₗ[R] (↥σ →₀ R) ⧸ π.ker) =
  (s₁ * s₀) • g
Tactic: refine ⟨Submodule.liftQ _ _ this ∘ₗ
    (LinearMap.quotKerEquivOfSurjective _ hπ).symm.toLinearMap, s₁ * 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
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
this : π.ker ≤ (HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)).ker
⊢ f ∘ₗ
      π.ker.liftQ (HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)) this ∘ₗ
        (↑(LinearEquiv.symm (π.quotKerEquivOfSurjective hπ)) : M →ₗ[R] (↥σ →₀ R) ⧸ π.ker) =
    (s₁ * s₀) • g
have h : ∀ (x : M),
  Eq.{u_3 + 1} (α := N')
    ((f ∘ₗ
            π.ker.liftQ (HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)) this ∘ₗ
              (↑(LinearEquiv.symm (π.quotKerEquivOfSurjective hπ)) : M →ₗ[R] (↥σ →₀ R) ⧸ π.ker) :
          (a : M) → N')
        x :
      N')
    (((s₁ * s₀) • g : (a : M) → N') x : N')
Tactic: ext x
-- 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
this : π.ker ≤ (HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)).ker
x : M
⊢ Eq.{u_3 + 1} (α := N')
    ((f ∘ₗ
            π.ker.liftQ (HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)) this ∘ₗ
              (↑(LinearEquiv.symm (π.quotKerEquivOfSurjective hπ)) : M →ₗ[R] (↥σ →₀ R) ⧸ π.ker) :
          (a : M) → N')
        x :
      N')
    (((s₁ * s₀) • g : (a : M) → N') x : N')
have h : ∀ (x : Finsupp.{u_2, u_1} (↥σ) R),
  Eq.{u_3 + 1} (α := N')
    ((f ∘ₗ
            π.ker.liftQ (HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)) this ∘ₗ
              (↑(LinearEquiv.symm (π.quotKerEquivOfSurjective hπ)) : M →ₗ[R] (↥σ →₀ R) ⧸ π.ker) :
          (a : M) → N')
        ((π : (a : ↥σ →₀ R) → M) x : M) :
      N')
    (((s₁ * s₀) • g : (a : M) → N') ((π : (a : ↥σ →₀ R) → M) x : M) : N')
Tactic: obtain ⟨x, rfl⟩ := hπ x
Cleared hypotheses: x
-- 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
this : π.ker ≤ (HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)).ker
x : Finsupp.{u_2, u_1} (↥σ) R
⊢ Eq.{u_3 + 1} (α := N')
    ((f ∘ₗ
            π.ker.liftQ (HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)) this ∘ₗ
              (↑(LinearEquiv.symm (π.quotKerEquivOfSurjective hπ)) : M →ₗ[R] (↥σ →₀ R) ⧸ π.ker) :
          (a : M) → N')
        ((π : (a : ↥σ →₀ R) → M) x : M) :
      N')
    (((s₁ * s₀) • g : (a : M) → N') ((π : (a : ↥σ →₀ R) → M) x : M) : N')
have h : Eq.{u_3 + 1} (α := N')
  ((f ∘ₗ
          π.ker.liftQ (HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)) this ∘ₗ
            (↑(LinearEquiv.symm (π.quotKerEquivOfSurjective hπ)) : M →ₗ[R] (↥σ →₀ R) ⧸ π.ker) ∘ₗ π :
        (a : ↥σ →₀ R) → N')
      x :
    N')
  ((f ∘ₗ HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i) : (a : ↥σ →₀ R) → N') x : N')
Tactic: rw [← LinearMap.comp_apply, ← LinearMap.comp_apply, mul_smul, LinearMap.smul_comp, ← hi,
    ← LinearMap.comp_smul, LinearMap.comp_assoc, LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
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
hM : Module.Finite R M
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
⊢ ∃ (s : ↥S), s • g₁ = s • g₂
have this : ∀ (x : M),
  ∃ (s : ↥S), HSMul.hSMul (β := N) s ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) s ((g₂ : (a : M) → N) x : N)
Tactic: have : ∀ x, ∃ s : S, s • g₁ x = s • g₂ x := fun x ↦
    IsLocalizedModule.exists_of_eq (S := S) (f := f) (LinearMap.congr_fun h x)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
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
hM : Module.Finite R M
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
this :
  ∀ (x : M),
    ∃ (s : ↥S), HSMul.hSMul (β := N) s ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) s ((g₂ : (a : M) → N) x : N)
⊢ ∃ (s : ↥S), s • g₁ = s • g₂
have choose : ∀ (s : (x : M) → ↥S)
  (hs :
    ∀ (x : M),
      HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N)),
  ∃ (s : ↥S), s • g₁ = 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_3
N' : Type u_4
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
hM : Module.Finite R M
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
s : (x : M) → ↥S
hs :
  ∀ (x : M),
    HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N)
⊢ ∃ (s : ↥S), s • g₁ = s • g₂
have obtain : ∀ (σ : Finset M) (hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤), ∃ (s : ↥S), s • g₁ = s • g₂
Tactic: obtain ⟨σ, hσ⟩ := hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
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₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
s : (x : M) → ↥S
hs :
  ∀ (x : M),
    HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N)
σ : Finset M
hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤
⊢ ∃ (s : ↥S), s • g₁ = s • g₂
have h₁ : σ.prod s • g₁ = σ.prod s • g₂
Tactic: use σ.prod s
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
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₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
s : (x : M) → ↥S
hs :
  ∀ (x : M),
    HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N)
σ : Finset M
hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤
⊢ σ.prod s • g₁ = σ.prod s • g₂
have h₁ : (↑σ : Set M) ⊆ (↑(σ.prod s • g₁ - σ.prod s • g₂).ker : Set M)
Tactic: rw [← sub_eq_zero, ← LinearMap.ker_eq_top, ← top_le_iff, ← 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_3
N' : Type u_4
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
hM : Module.Finite R M
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
⊢ ∃ (s : ↥S), s • g₁ = s • g₂
have have : ∀
  (this :
    ∀ (x : M),
      ∃ (s : ↥S),
        HSMul.hSMul (β := N) s ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) s ((g₂ : (a : M) → N) x : N)),
  ∃ (s : ↥S), s • g₁ = s • g₂
Tactic: classical
  have : ∀ x, ∃ s : S, s • g₁ x = s • g₂ x := fun x ↦
    IsLocalizedModule.exists_of_eq (S := S) (f := f) (LinearMap.congr_fun h x)
  choose s hs using this
  obtain ⟨σ, hσ⟩ := hM
  use σ.prod s
  rw [← sub_eq_zero, ← LinearMap.ker_eq_top, ← top_le_iff, ← hσ, Submodule.span_le]
  intro x hx
  simp only [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.sub_apply, LinearMap.smul_apply,
    sub_eq_zero, ← Finset.prod_erase_mul σ s hx, mul_smul, hs]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
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
hM : Module.Finite R M
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
have have₁ have₂ :
  ∀
    (this :
      ∀ (x : M),
        ∃ (s : ↥S),
          HSMul.hSMul (β := N) s ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) s ((g₂ : (a : M) → N) x : N)),
    ∃ (s : ↥S), s • g₁ = s • g₂
⊢ ∃ (s : ↥S), s • g₁ = s • g₂
have have₃ : ∀ (s : (x : M) → ↥S)
  (hs :
    ∀ (x : M),
      HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N)),
  ∃ (s : ↥S), s • g₁ = s • g₂
Tactic: classical
  have : ∀ x, ∃ s : S, s • g₁ x = s • g₂ x := fun x ↦
    IsLocalizedModule.exists_of_eq (S := S) (f := f) (LinearMap.congr_fun h x)
  choose s hs using this
  obtain ⟨σ, hσ⟩ := hM
  use σ.prod s
  rw [← sub_eq_zero, ← LinearMap.ker_eq_top, ← top_le_iff, ← hσ, Submodule.span_le]
  intro x hx
  simp only [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.sub_apply, LinearMap.smul_apply,
    sub_eq_zero, ← Finset.prod_erase_mul σ s hx, mul_smul, hs]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
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
hM : Module.Finite R M
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
have have₁ have₂ :
  ∀
    (this :
      ∀ (x : M),
        ∃ (s : ↥S),
          HSMul.hSMul (β := N) s ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) s ((g₂ : (a : M) → N) x : N)),
    ∃ (s : ↥S), s • g₁ = s • g₂
have₃ :
  ∀ (s : (x : M) → ↥S)
    (hs :
      ∀ (x : M),
        HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N)),
    ∃ (s : ↥S), s • g₁ = s • g₂
⊢ ∃ (s : ↥S), s • g₁ = s • g₂
have have₄ : ∀ (s : (x : M) → ↥S)
  (hs :
    ∀ (x : M),
      HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N))
  (σ : Finset M) (hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤), ∃ (s : ↥S), s • g₁ = s • g₂
Tactic: classical
  have : ∀ x, ∃ s : S, s • g₁ x = s • g₂ x := fun x ↦
    IsLocalizedModule.exists_of_eq (S := S) (f := f) (LinearMap.congr_fun h x)
  choose s hs using this
  obtain ⟨σ, hσ⟩ := hM
  use σ.prod s
  rw [← sub_eq_zero, ← LinearMap.ker_eq_top, ← top_le_iff, ← hσ, Submodule.span_le]
  intro x hx
  simp only [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.sub_apply, LinearMap.smul_apply,
    sub_eq_zero, ← Finset.prod_erase_mul σ s hx, mul_smul, hs]
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
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
hM : Module.Finite R M
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
have have₁ have₂ :
  ∀
    (this :
      ∀ (x : M),
        ∃ (s : ↥S),
          HSMul.hSMul (β := N) s ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) s ((g₂ : (a : M) → N) x : N)),
    ∃ (s : ↥S), s • g₁ = s • g₂
have₃ :
  ∀ (s : (x : M) → ↥S)
    (hs :
      ∀ (x : M),
        HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N)),
    ∃ (s : ↥S), s • g₁ = s • g₂
have₄ :
  ∀ (s : (x : M) → ↥S)
    (hs :
      ∀ (x : M),
        HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N))
    (σ : Finset M) (hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤), ∃ (s : ↥S), s • g₁ = s • g₂
⊢ ∃ (s : ↥S), s • g₁ = s • g₂
have h₁ : ∀ (s : (x : M) → ↥S)
  (hs :
    ∀ (x : M),
      HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N))
  (σ : Finset M) (hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤), σ.prod s • g₁ = σ.prod s • g₂
Tactic: classical
  have : ∀ x, ∃ s : S, s • g₁ x = s • g₂ x := fun x ↦
    IsLocalizedModule.exists_of_eq (S := S) (f := f) (LinearMap.congr_fun h x)
  choose s hs using this
  obtain ⟨σ, hσ⟩ := hM
  use σ.prod s
  rw [← sub_eq_zero, ← LinearMap.ker_eq_top, ← top_le_iff, ← hσ, Submodule.span_le]
  intro x hx
  simp only [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.sub_apply, LinearMap.smul_apply,
    sub_eq_zero, ← Finset.prod_erase_mul σ s hx, mul_smul, hs]
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
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
hM : Module.Finite R M
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
have have₁ have₂ :
  ∀
    (this :
      ∀ (x : M),
        ∃ (s : ↥S),
          HSMul.hSMul (β := N) s ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) s ((g₂ : (a : M) → N) x : N)),
    ∃ (s : ↥S), s • g₁ = s • g₂
have₃ :
  ∀ (s : (x : M) → ↥S)
    (hs :
      ∀ (x : M),
        HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N)),
    ∃ (s : ↥S), s • g₁ = s • g₂
have₄ :
  ∀ (s : (x : M) → ↥S)
    (hs :
      ∀ (x : M),
        HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N))
    (σ : Finset M) (hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤), ∃ (s : ↥S), s • g₁ = s • g₂
h₁ :
  ∀ (s : (x : M) → ↥S)
    (hs :
      ∀ (x : M),
        HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N))
    (σ : Finset M) (hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤), σ.prod s • g₁ = σ.prod s • g₂
⊢ ∃ (s : ↥S), s • g₁ = s • g₂
have h₂ : ∀ (s : (x : M) → ↥S)
  (hs :
    ∀ (x : M),
      HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N))
  (σ : Finset M) (hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤),
  (↑σ : Set M) ⊆ (↑(σ.prod s • g₁ - σ.prod s • g₂).ker : Set M)
Tactic: classical
  have : ∀ x, ∃ s : S, s • g₁ x = s • g₂ x := fun x ↦
    IsLocalizedModule.exists_of_eq (S := S) (f := f) (LinearMap.congr_fun h x)
  choose s hs using this
  obtain ⟨σ, hσ⟩ := hM
  use σ.prod s
  rw [← sub_eq_zero, ← LinearMap.ker_eq_top, ← top_le_iff, ← hσ, Submodule.span_le]
  intro x hx
  simp only [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.sub_apply, LinearMap.smul_apply,
    sub_eq_zero, ← Finset.prod_erase_mul σ s hx, mul_smul, hs]
Cleared hypotheses: hM