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

Premises used: LinearMap.exact_iff
-- Module: Mathlib.Algebra.Module.FinitePresentation
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))
rw : Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.range (LinearMap.baseChange A f.ker.subtype))
⊢ Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.ker (LinearMap.baseChange A f))

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Module.FinitePresentation
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))
⊢ Module.Finite R ↥f.ker

Tactic:
have : Module.Finite R (LinearMap.ker f) :=
    .of_fg (Module.FinitePresentation.fg_ker f hf)
-- Module: Mathlib.Algebra.Module.FinitePresentation
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_1 :
  Eq (α := Submodule A (A ⊗[R] (Fin n → R))) (LinearMap.ker (LinearMap.baseChange A f))
    (LinearMap.range (LinearMap.baseChange A f.ker.subtype))
this : Module.Finite R ↥f.ker
⊢ Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.range (LinearMap.baseChange A f.ker.subtype))

Tactic:
Submodule.fg_range _

Premises used: Submodule.fg_range
-- Module: Mathlib.Algebra.Module.FinitePresentation
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_1 :
  Eq (α := Submodule A (A ⊗[R] (Fin n → R))) (LinearMap.ker (LinearMap.baseChange A f))
    (LinearMap.range (LinearMap.baseChange A f.ker.subtype))
this : Module.Finite R ↥f.ker
⊢ Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.range (LinearMap.baseChange A f.ker.subtype))

Tactic:
exact Submodule.fg_range _

Premises used: Submodule.fg_range
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : 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
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
inst_7 : Module A N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
h : IsBaseChange A f
inst_9 : Module.FinitePresentation R M
⊢ (↑h.equiv : A ⊗[R] M →ₗ[A] N).ker.FG

Tactic:
simpa using Submodule.fg_bot

Premises used: Submodule.fg_bot
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
N : Type ?u.284510
N' : Type ?u.284776
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_1 : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S_1 f
S : Submonoid R
inst_8 : Module.FinitePresentation R M
⊢ Module.FinitePresentation (Localization (M := R) S) (LocalizedModule S M)

Tactic:
FinitePresentation.of_isBaseChange (LocalizedModule.mkLinearMap S M)
    ((isLocalizedModule_iff_isBaseChange S _ _).mp inferInstance)

Premises used: isLocalizedModule_iff_isBaseChange, inferInstance, Iff.mp, LocalizedModule.mkLinearMap, FinitePresentation.of_isBaseChange
-- 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
h : FinitePresentation R M
g : M →ₗ[R] N'
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
⊢ ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = s • g

Tactic:
obtain ⟨σ, hσ, τ, hτ⟩ := h
-- 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 ∈ σ))
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)) ⊤
rw₂ rw₃ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) (Submodule.span R (↑σ : Set M))
⊢ π.range = ⊤

Tactic:
rw [range_linearCombination, Subtype.range_val, ← hσ]

Premises used: Subtype.range_val, Finsupp.range_linearCombination
-- 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 ∈ σ))
⊢ 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σ])
-- 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)
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
⊢ ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = s • g

Tactic:
choose s hs using IsLocalizedModule.surj S f

Premises used: IsLocalizedModule.surj
-- 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
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')
⊢ f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π

Tactic:
ext j
-- 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
j : ↥σ
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')
⊢ 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:
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₀, π]

Premises used: LinearMap.smul_apply, Finsupp.linearCombination_single, one_smul, LinearMap.coe_comp, Function.comp_apply, LinearMap.map_smul_of_tower, Finsupp.lsingle_apply
-- 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
j : ↥σ
h : (↑j : M) ∈ σ
⊢ 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:
rw [← mul_smul, Finset.prod_erase_mul]

Premises used: Finset.prod_erase_mul, 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
j : ↥σ
⊢ (↑j : M) ∈ σ

Tactic:
j.prop

Premises used: Subtype.prop
-- 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
j : ↥σ
⊢ (↑j : M) ∈ σ

Tactic:
exact j.prop

Premises used: Subtype.prop
-- 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
⊢ 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
-- 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) ∘ₗ π
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
convert_to :
  ∃ (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

Tactic:
convert_to ∃ s : S, s • (Finsupp.linearCombination R i x) = s • 0

Premises used: Finsupp.linearCombination, Subtype.val, DFunLike.coe
-- 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) ∘ₗ π
x : ↥τ
⊢ 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:
simp only [smul_zero]

Premises used: smul_zero
-- 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) ∘ₗ π
x : ↥τ
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')
⊢ ∃ (s : ↥S),
    HSMul.hSMul (β := N) s ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = HSMul.hSMul (β := N) s 0

Tactic:
apply IsLocalizedModule.exists_of_eq (S := S) (f := f)

Premises used: IsLocalizedModule.exists_of_eq