mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : CommSemiring Aₛ
inst✝³ : Algebra A Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R A Aₛ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
x : A
s : ↥S
⊢ mk' Aₛ x ⟨(algebraMap R A) ↑s, ⋯⟩ = IsLocalizedModule.mk' (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
x : R
s : ↥S
⊢ mk' A x s = IsLocalizedModule.mk' (Algebra.linearMap R A) x s

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
e : M ≅ X
⊢ X ◁ (η ≫ e.hom) ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom = (ρ_ X).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
e : M ≅ X
⊢ ((e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom) ▷ X ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom =
    (α_ X X X).hom ≫ X ◁ ((e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom) ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
⊢ 𝟙_ C ◁ 𝟙 (𝟙_ C) ≫ (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
⊢ (λ_ (𝟙_ C)).hom ▷ 𝟙_ C ≫ (λ_ (𝟙_ C)).hom = (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ≫ 𝟙_ C ◁ (λ_ (𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₁ h₂ : MonObj X
H : μ = μ
this : η = η
⊢ h₁ = h₂

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
a : R
b : S
hb : IsInteger R b
⊢ IsInteger R (a • b)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : S
⊢ ∃ b, IsInteger R (↑b • a)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₁ h₂ : MonObj X
H : μ = μ
⊢ h₁ = h₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
h : Z₁ ⟶ Z₂
⊢ (α_ X₁ Y₁ Z₁).hom ≫ (f ⊗ₘ g ⊗ₘ h) = ((f ⊗ₘ g) ⊗ₘ h) ≫ (α_ X₂ Y₂ Z₂).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
h : Z₁ ⟶ Z₂
⊢ (α_ X₁ Y₁ Z₁).inv ≫ ((f ⊗ₘ g) ⊗ₘ h) = (f ⊗ₘ g ⊗ₘ h) ≫ (α_ X₂ Y₂ Z₂).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
h : Z₁ ⟶ Z₂
gh : Y₂ ⊗ Z₂ ⟶ W
⊢ (α_ X₁ Y₁ Z₁).hom ≫ (f ⊗ₘ (g ⊗ₘ h) ≫ gh) = ((f ⊗ₘ g) ⊗ₘ h) ≫ (α_ X₂ Y₂ Z₂).hom ≫ (𝟙 X₂ ⊗ₘ gh)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
h : Z₁ ⟶ Z₂
fg : X₂ ⊗ Y₂ ⟶ W
⊢ (α_ X₁ Y₁ Z₁).inv ≫ ((f ⊗ₘ g) ≫ fg ⊗ₘ h) = (f ⊗ₘ g ⊗ₘ h) ≫ (α_ X₂ Y₂ Z₂).inv ≫ (fg ⊗ₘ 𝟙 Z₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
⊢ (λ_ M).hom = (η ⊗ₘ 𝟙 M) ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
⊢ (ρ_ M).hom = (𝟙 M ⊗ₘ η) ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X₁ : C
inst✝ : MonObj M
f : X₁ ⟶ M
⊢ (λ_ X₁).inv ≫ (η ⊗ₘ f) ≫ μ = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X₁ : C
inst✝ : MonObj M
f : X₁ ⟶ M
⊢ (ρ_ X₁).inv ≫ (f ⊗ₘ η) ≫ μ = f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
⊢ ∃ b, ∀ i ∈ s, IsInteger R (↑b • f i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
ι : Type u_4
inst✝ : Finite ι
f : ι → S
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X : C
inst✝ : MonObj M
f : X ⟶ M
⊢ (α_ X M M).hom ≫ (f ⊗ₘ μ) ≫ μ = ((f ⊗ₘ 𝟙 M) ≫ μ ⊗ₘ 𝟙 M) ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
hf : Injective f
⊢ Injective (integerMultiple M s f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X : C
inst✝ : MonObj M
f : X ⟶ M
⊢ (α_ M M X).inv ≫ (μ ⊗ₘ f) ≫ μ = (𝟙 M ⊗ₘ (𝟙 M ⊗ₘ f) ≫ μ) ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ⇑(algebraMap R S) '' ↑(finsetIntegerMultiple M s) = commonDenomOfFinset M s • ↑s

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
e : M ≅ X
⊢ IsMonHom e.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
M N O X : C
inst✝³ : MonObj M
inst✝² : MonObj N
inst✝¹ : MonObj O
f : M ≅ N
inst✝ : IsMonHom f.hom
⊢ η ≫ f.inv = η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
M N O X : C
inst✝³ : MonObj M
inst✝² : MonObj N
inst✝¹ : MonObj O
f : M ≅ N
inst✝ : IsMonHom f.hom
⊢ μ ≫ f.inv = (f.inv ⊗ₘ f.inv) ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
Z : C
f : Z ⟶ M
⊢ (η ⊗ₘ f) ≫ μ = (λ_ Z).hom ≫ f

Tactic:
rw [tensorHom_def'_assoc, one_mul, leftUnitor_naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
Z : C
f : Z ⟶ M
⊢ (η ⊗ₘ f) ≫ μ = (λ_ Z).hom ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
Z : C
f : Z ⟶ M
⊢ (f ⊗ₘ η) ≫ μ = (ρ_ Z).hom ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
⊢ M ◁ μ ≫ μ = (α_ M M M).inv ≫ μ ▷ M ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
⊢ ((λ_ (𝟙_ C)).inv ≫ ((λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η) ⊗ₘ η)) ≫ (α_ M N P).hom =
    (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
⊢ ((λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ₘ η)) ≫ (λ_ M).hom = η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
⊢ ((λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ 𝟙 (𝟙_ C))) ≫ (ρ_ M).hom = η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (η ▷ M ⊗ₘ η ▷ N) ≫ (μ ⊗ₘ μ)

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (λ_ (𝟙_ C)).inv ▷ (M ⊗ N)

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| tensorμ (𝟙_ C) (𝟙_ C) M N

Tactic:
rw [tensorHom_comp_tensorHom, one_mul, one_mul]

Goal state after:
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (λ_ M).hom ⊗ₘ (λ_ N).hom

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (λ_ (𝟙_ C)).inv ▷ (M ⊗ N)

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| tensorμ (𝟙_ C) (𝟙_ C) M N
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ ((λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)) ▷ (M ⊗ N) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ) = (λ_ (M ⊗ N)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (M ⊗ N) ◁ ((λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ) = (ρ_ (M ⊗ N)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (tensorμ M N M N ≫ (μ ⊗ₘ μ)) ▷ (M ⊗ N) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ) =
    (α_ (M ⊗ N) (M ⊗ N) (M ⊗ N)).hom ≫ (M ⊗ N) ◁ (tensorμ M N M N ≫ (μ ⊗ₘ μ)) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
v : Set M
hv : span R v = ⊤
x : Mₛ
x✝ : x ∈ ⊤
⊢ x ∈ span Rₛ (⇑f '' v)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
⊢ (tensorμ (M ⊗ N) P (M ⊗ N) P ≫ (tensorμ M N M N ≫ (μ ⊗ₘ μ) ⊗ₘ μ)) ≫ (α_ M N P).hom =
    ((α_ M N P).hom ⊗ₘ (α_ M N P).hom) ≫ tensorμ M (N ⊗ P) M (N ⊗ P) ≫ (μ ⊗ₘ tensorμ N P N P ≫ (μ ⊗ₘ μ))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
eq : ∑ i ∈ t, g₁ i • (⇑f ∘ v) i = ∑ i ∈ t, g₂ i • (⇑f ∘ v) i
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg : ∀ i ∈ t.disjSum t, (algebraMap R Rₛ) (fg i) = ↑a • Sum.elim g₁ g₂ i
⊢ g₁ i = g₂ i

Tactic:
simp_rw [Sum.forall, Finset.inl_mem_disjSum, Sum.elim_inl, Finset.inr_mem_disjSum, Sum.elim_inr,
    Subtype.forall'] at hfg

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
eq : ∑ i ∈ t, g₁ i • (⇑f ∘ v) i = ∑ i ∈ t, g₂ i • (⇑f ∘ v) i
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inl ↑x)) = ↑a • g₁ ↑x) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inr ↑x)) = ↑a • g₂ ↑x
⊢ g₁ i = g₂ i
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ (tensorμ (𝟙_ C) M (𝟙_ C) M ≫ ((λ_ (𝟙_ C)).hom ⊗ₘ μ)) ≫ (λ_ M).hom = ((λ_ M).hom ⊗ₘ (λ_ M).hom) ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ LinearIndependent Rₛ (⇑f ∘ v)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ (tensorμ M (𝟙_ C) M (𝟙_ C) ≫ (μ ⊗ₘ (λ_ (𝟙_ C)).hom)) ≫ (ρ_ M).hom = ((ρ_ M).hom ⊗ₘ (ρ_ M).hom) ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
h : ∀ (s : ↥S), IsRegular ↑s
⊢ Set.InjOn ⇑f ↑(span R (Set.range v))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝⁷ : CommSemiring R
S : Submonoid R
inst✝⁶ : CommSemiring Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : IsLocalization S Rₛ
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rₛ M
inst✝ : IsScalarTower R Rₛ M
ι : Type u_5
b : ι → M
hli : LinearIndependent R b
⊢ LinearIndependent Rₛ b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
⊢ η ≫ (f ⊗ₘ g) = η

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → Mₛ
hf : LinearIndependent R v
⊢ ∃ w, LinearIndependent R w

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
⊢ ⊤ ≤ span Rₛ (Set.range (⇑f ∘ ⇑b))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
i : ι
⊢ (ofIsLocalizedModule Rₛ S f b) i = f (b i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
m : M
i : ι
this : ↑R ↑(ofIsLocalizedModule Rₛ S f b).repr ∘ₗ f = Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ ↑b.repr
⊢ ((ofIsLocalizedModule Rₛ S f b).repr (f m)) i = (algebraMap R Rₛ) ((b.repr m) i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
⊢ μ ≫ (f ⊗ₘ g) = ((f ⊗ₘ g) ⊗ₘ f ⊗ₘ g) ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O X✝ : C
inst✝⁸ : MonObj M
inst✝⁷ : MonObj N
inst✝⁶ : MonObj O
inst✝⁵ : BraidedCategory C
X Y Z W : C
inst✝⁴ : MonObj X
inst✝³ : MonObj Y
inst✝² : MonObj Z
inst✝¹ : MonObj W
f : Y ⟶ Z
inst✝ : IsMonHom f
⊢ η ≫ X ◁ f = η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O X✝ : C
inst✝⁸ : MonObj M
inst✝⁷ : MonObj N
inst✝⁶ : MonObj O
inst✝⁵ : BraidedCategory C
X Y Z W : C
inst✝⁴ : MonObj X
inst✝³ : MonObj Y
inst✝² : MonObj Z
inst✝¹ : MonObj W
f : Y ⟶ Z
inst✝ : IsMonHom f
⊢ μ ≫ X ◁ f = (X ◁ f ⊗ₘ X ◁ f) ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
m : M
i : ι
⊢ ((ofIsLocalizedModule Rₛ S f b).repr (f m)) i = (algebraMap R Rₛ) ((b.repr m) i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O X✝ : C
inst✝⁸ : MonObj M
inst✝⁷ : MonObj N
inst✝⁶ : MonObj O
inst✝⁵ : BraidedCategory C
X Y Z W : C
inst✝⁴ : MonObj X
inst✝³ : MonObj Y
inst✝² : MonObj Z
inst✝¹ : MonObj W
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ η ≫ f ▷ Z = η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O X✝ : C
inst✝⁸ : MonObj M
inst✝⁷ : MonObj N
inst✝⁶ : MonObj O
inst✝⁵ : BraidedCategory C
X Y Z W : C
inst✝⁴ : MonObj X
inst✝³ : MonObj Y
inst✝² : MonObj Z
inst✝¹ : MonObj W
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ μ ≫ f ▷ Z = (f ▷ Z ⊗ₘ f ▷ Z) ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
⊢ span R (Set.range ⇑(ofIsLocalizedModule Rₛ S f b)) = span R (⇑f '' Set.range ⇑b)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
⊢ η ≫ (β_ X Y).hom = η

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
⊢ span R (⇑f '' Set.range ⇑b) = map f (span R (Set.range ⇑b))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
A✝ B✝ : Mon C
f : A✝ ⟶ B✝
e : IsIso ((forget C).map f)
⊢ f ≫ Hom.mk' (inv f.hom) ⋯ ⋯ = 𝟙 A✝ ∧ Hom.mk' (inv f.hom) ⋯ ⋯ ≫ f = 𝟙 B✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
A : Mon C
⊢ μ ≫ η = (η ⊗ₘ η) ≫ μ

Tactic:
by

Goal state after: