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) ∘ₗ π
x : ↥τ
rw : Eq.{u_3 + 1} (α := N') ((s₀ • g : (a : M) → N') ((π : (a : ↥σ →₀ R) → M) (↑x : ↥σ →₀ R) : M) : N') (0 : N')
⊢ 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:
rw [← LinearMap.comp_apply, map_zero, hi, LinearMap.comp_apply]

Premises used: LinearMap.comp_apply, map_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 : ↥τ
⊢ Eq.{u_3 + 1} (α := N') ((s₀ • g : (a : M) → N') 0 : N') (0 : N')

Tactic:
map_zero (s₀ • g)

Premises used: map_zero, HSMul.hSMul
-- 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_2 + 1} (α := M) ((π : (a : ↥σ →₀ R) → M) (↑x : ↥σ →₀ R) : M) (0 : M)
⊢ Eq.{u_3 + 1} (α := N') ((s₀ • g : (a : M) → N') ((π : (a : ↥σ →₀ R) → M) (↑x : ↥σ →₀ R) : M) : N') (0 : N')

Tactic:
convert! map_zero (s₀ • g)

Premises used: map_zero, HSMul.hSMul
-- 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 : Membership.mem (γ := Submodule R (Finsupp.{u_2, u_1} (↥σ) R)) (Submodule.span R (↑τ : Set (↥σ →₀ R))) (↑x : ↥σ →₀ R)
⊢ Eq.{u_2 + 1} (α := M) ((π : (a : ↥σ →₀ R) → M) (↑x : ↥σ →₀ R) : M) (0 : M)

Tactic:
rw [← LinearMap.mem_ker, ← hτ]

Premises used: LinearMap.mem_ker
-- 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 : ↥τ
⊢ Membership.mem (γ := Submodule R (Finsupp.{u_2, u_1} (↥σ) R)) (Submodule.span R (↑τ : Set (↥σ →₀ R))) (↑x : ↥σ →₀ R)

Tactic:
Submodule.subset_span x.prop

Premises used: Subtype.prop, Submodule.subset_span
-- 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 : ↥τ
⊢ Membership.mem (γ := Submodule R (Finsupp.{u_2, u_1} (↥σ) R)) (Submodule.span R (↑τ : Set (↥σ →₀ R))) (↑x : ↥σ →₀ R)

Tactic:
exact Submodule.subset_span x.prop

Premises used: Subtype.prop, Submodule.subset_span
-- 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 : ↥τ), ∃ (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
-- 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) ∘ₗ π
this :
  ∀ (x : ↥τ), ∃ (s : ↥S), HSMul.hSMul (β := N) s ((linearCombination R i : (a : ↥σ →₀ R) → N) (↑x : ↥σ →₀ R) : N) = 0
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
⊢ ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = 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_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
rw :
  (↑τ : Set (↥σ →₀ R)) ⊆
    (↑(HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)).ker : Set (↥σ →₀ R))
⊢ π.ker ≤ (HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)).ker

Tactic:
rw [← hτ, Submodule.span_le]

Premises used: Submodule.span_le
-- 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
x : Finsupp.{u_2, u_1} (↥σ) R
hxσ : x ∈ (↑τ : Set (↥σ →₀ R))
simp :
  x ∈
    (↑(HSMul.hSMul (α := ↥S) (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) (∏ i : ↥τ, s' i) (linearCombination R i)).ker :
      Set (↥σ →₀ R))
⊢ x ∈ (↑(HSMul.hSMul (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) s₁ (linearCombination R i)).ker : Set (↥σ →₀ R))

Tactic:
simp only [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
x : Finsupp.{u_2, u_1} (↥σ) R
hxσ : x ∈ (↑τ : Set (↥σ →₀ R))
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
⊢ x ∈
    (↑(HSMul.hSMul (α := ↥S) (β := Finsupp.{u_2, u_1} (↥σ) R →ₗ[R] N) (∏ i : ↥τ, s' i) (linearCombination R i)).ker :
      Set (↥σ →₀ R))

Tactic:
rw [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.smul_apply,
      ← Finset.prod_erase_mul _ _ (Finset.mem_univ ⟨x, hxσ⟩), mul_smul]

Premises used: Finset.mem_univ, Finset.prod_erase_mul, LinearMap.smul_apply, LinearMap.mem_ker, SetLike.mem_coe, 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
x : Finsupp.{u_2, u_1} (↥σ) R
hxσ : x ∈ (↑τ : Set (↥σ →₀ R))
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := ↥S) (β := N)
      (∏ x ∈ Finset.erase Finset.univ (Subtype.mk (p := fun (x : Finsupp.{u_2, u_1} (↥σ) R) ↦ x ∈ τ) x hxσ), s' x) 0 =
    0

Tactic:
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) ∘ₗ π
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))
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
⊢ 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:
convert! 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) ∘ₗ π
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 (β := 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:
hs' ⟨x, hxσ⟩

Premises used: Subtype.mk
-- 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
x : Finsupp.{u_2, u_1} (↥σ) R
hxσ : x ∈ (↑τ : Set (↥σ →₀ R))
⊢ 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:
exact hs' ⟨x, hxσ⟩

Premises used: Subtype.mk