awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.FinitePresentation
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

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σ⟩
-- Module: Mathlib.Algebra.Module.FinitePresentation
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

Tactic:
⟨Submodule.liftQ _ _ this ∘ₗ
    (LinearMap.quotKerEquivOfSurjective _ hπ).symm.toLinearMap, s₁ * s₀, ?_⟩

Premises used: LinearEquiv.symm, HMul.hMul, LinearMap.comp, LinearEquiv.toLinearMap, LinearMap.quotKerEquivOfSurjective, Exists.intro, Submodule.liftQ
-- Module: Mathlib.Algebra.Module.FinitePresentation
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
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
⊢ ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = s • g

Tactic:
refine ⟨Submodule.liftQ _ _ this ∘ₗ
    (LinearMap.quotKerEquivOfSurjective _ hπ).symm.toLinearMap, s₁ * s₀, ?_⟩
-- Module: Mathlib.Algebra.Module.FinitePresentation
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 :
  ∀ (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')
⊢ 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:
ext x
-- Module: Mathlib.Algebra.Module.FinitePresentation
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
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')
⊢ 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:
obtain ⟨x, rfl⟩ := hπ x

Premises used: rfl
-- Module: Mathlib.Algebra.Module.FinitePresentation
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
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')
⊢ 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:
rw [← LinearMap.comp_apply, ← LinearMap.comp_apply, mul_smul, LinearMap.smul_comp, ← hi,
    ← LinearMap.comp_smul, LinearMap.comp_assoc, LinearMap.comp_assoc]

Premises used: LinearMap.smul_comp, LinearMap.comp_assoc, LinearMap.comp_apply, LinearMap.comp_smul, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.FinitePresentation
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 : ↥σ →₀ 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:
simp
-- Module: Mathlib.Algebra.Module.FinitePresentation
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₂
⊢ ∀ (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)
-- Module: Mathlib.Algebra.Module.FinitePresentation
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)
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₂
⊢ ∃ (s : ↥S), s • g₁ = s • g₂

Tactic:
choose s hs using this
-- Module: Mathlib.Algebra.Module.FinitePresentation
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)
obtain : ∀ (σ : Finset M) (hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤), ∃ (s : ↥S), s • g₁ = s • g₂
⊢ ∃ (s : ↥S), s • g₁ = s • g₂

Tactic:
obtain ⟨σ, hσ⟩ := hM
-- Module: Mathlib.Algebra.Module.FinitePresentation
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)) ⊤
h₁ : σ.prod s • g₁ = σ.prod s • g₂
⊢ ∃ (s : ↥S), s • g₁ = s • g₂

Tactic:
use σ.prod s

Premises used: Finset.prod
-- Module: Mathlib.Algebra.Module.FinitePresentation
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)) ⊤
h₁ : (↑σ : Set M) ⊆ (↑(σ.prod s • g₁ - σ.prod s • g₂).ker : Set M)
⊢ σ.prod s • g₁ = σ.prod s • g₂

Tactic:
rw [← sub_eq_zero, ← LinearMap.ker_eq_top, ← top_le_iff, ← hσ, Submodule.span_le]

Premises used: LinearMap.ker_eq_top, sub_eq_zero, top_le_iff, Submodule.span_le
-- Module: Mathlib.Algebra.Module.FinitePresentation
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)) ⊤
x : M
hx : x ∈ (↑σ : Set M)
⊢ x ∈ (↑(σ.prod s • g₁ - σ.prod s • g₂).ker : Set M)

Tactic:
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]

Premises used: Finset.prod_erase_mul, LinearMap.smul_apply, sub_eq_zero, LinearMap.mem_ker, SetLike.mem_coe, LinearMap.sub_apply, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.FinitePresentation
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₂
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)
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)) ⊤) ⦃x : M⦄ (hx : x ∈ (↑σ : Set M)),
    x ∈ (↑(σ.prod s • g₁ - σ.prod s • g₂).ker : 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]

Premises used: LinearMap.ker_eq_top, LinearMap.smul_apply, sub_eq_zero, LinearMap.mem_ker, SetLike.mem_coe, top_le_iff, LinearMap.sub_apply, SemigroupAction.mul_smul, Submodule.span_le
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
N' : Type u_2
inst_8 : AddCommGroup N'
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
inst_11 : Module.Finite R M
inst_12 : Module.FinitePresentation R N
l : M →ₗ[R] N
hf :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) hf
obtain :
  ∀ (l' : N →ₗ[R] M) (s₀ : ↥S) (H : f ∘ₗ l' = s₀ • (↑e.symm : N' →ₗ[R] M') ∘ₗ g),
    ∃ r ∈ S,
      ∀ (t : R),
        r ∣ t →
          Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) N)
            (⇑((LocalizedModule.map (Submonoid.powers t) :
                      (a : M →ₗ[R] N) →
                        LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                          LocalizedModule (Submonoid.powers t) N)
                    l :
                  LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                    (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) N)) :
              (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) N)
⊢ ∃ r ∈ S,
    ∀ (t : R),
      r ∣ t →
        Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) N)
          (⇑((LocalizedModule.map (Submonoid.powers t) :
                    (a : M →ₗ[R] N) →
                      LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                        LocalizedModule (Submonoid.powers t) N)
                  l :
                LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                  (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) N)) :
            (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) N)

Tactic:
obtain ⟨l', s₀, H⟩ := Module.FinitePresentation.exists_lift_of_isLocalizedModule S f
    (e.symm.toLinearMap.comp g)

Premises used: LinearEquiv.symm, Module.FinitePresentation.exists_lift_of_isLocalizedModule, LinearMap.comp, LinearEquiv.toLinearMap