mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r a * ↑b ^ N) = (↑a * ↑b) ^ N'✝ a b * (r b * ↑a ^ N)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
a b : ↑↑s
⊢ ((↑a * ↑b) ^ (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) * (r a * ↑b ^ N) =
    ((↑a * ↑b) ^ (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) * (r b * ↑a ^ N)

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r a * ↑b ^ N) = (↑a * ↑b) ^ N'✝ a b * (r b * ↑a ^ N)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
a b : ↑↑s
⊢ ((↑a * ↑b) ^ (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) * (r a * ↑b ^ N) =
    ((↑a * ↑b) ^ (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) * (r b * ↑a ^ N)
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
hi : I.IsLocal
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {x}
hpq : p + q = 1
r : R
hr : q = x * r
⊢ -p ∈ I

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
hi : I.IsLocal
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {x}
hpq : p + q = 1
r : R
hr : q = x * r
⊢ -p ∈ I
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : TwoSidedIdeal R
x✝ : R
⊢ x✝ ∈ asIdeal I.jacobson ↔ x✝ ∈ (asIdeal I).jacobson

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
I : TwoSidedIdeal R
x✝ : R
⊢ x✝ ∈ asIdeal I.jacobson ↔ x✝ ∈ (asIdeal I).jacobson
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S)
tfae_2_to_4 : ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalHom f
x✝¹ : IsLocalHom f
x✝ : R
⊢ x✝ ∈ Ideal.comap f (maximalIdeal S) ↔ x✝ ∈ maximalIdeal R

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S)
tfae_2_to_4 : ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalHom f
x✝¹ : IsLocalHom f
x✝ : R
⊢ x✝ ∈ Ideal.comap f (maximalIdeal S) ↔ x✝ ∈ maximalIdeal R
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
J : Ideal R
hJ : J ≠ ⊤
M : Ideal R
hM1 : M.IsMaximal
hM2 : J ≤ M
⊢ J ≤ maximalIdeal R

Tactic:
rwa [← eq_maximalIdeal hM1]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
x : R
⊢ x ∉ maximalIdeal R ↔ IsUnit x

Tactic:
simp only [mem_maximalIdeal, mem_nonunits_iff, not_not]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ IsUnit ↑a

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ IsUnit ↑a
Module: Mathlib.Algebra.Category.Ring.Instances

Goal state before:
pp: α : Type u_1
commRing✝ : CommRing α
M : Submonoid ↑(CommRingCat.of α)
⊢ Epi (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of α)) (Localization M)))

Tactic:
exact IsLocalization.epi M _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ ((Functor.const J).obj (F.1 i)).obj i = F.obj i

Tactic:
;

Goal state after:
case refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ ((Functor.const J).obj (F.1 i)).obj i = F.obj i
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: case refine_3
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ₛ
x✝¹ x✝ : A
⊢ ((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ →
      ∃ c, c • x✝¹ = c • x✝) ↔
    (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝

Tactic:
;

Goal state after:
case refine_3
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ₛ
x✝¹ x✝ : A
⊢ ((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ →
      ∃ c, c • x✝¹ = c • x✝) ↔
    (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: case refine_3
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ₛ
x✝¹ x✝ : A
⊢ ((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ →
      ∃ a, ∃ (b : a ∈ S), ⟨a, b⟩ • x✝¹ = ⟨a, b⟩ • x✝) ↔
    (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ a, ∃ (_ : a ∈ Submonoid.map (algebraMap R A) S), a * x✝¹ = a * x✝

Tactic:
;

Goal state after:
case refine_3
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ₛ
x✝¹ x✝ : A
⊢ ((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ →
      ∃ a, ∃ (b : a ∈ S), ⟨a, b⟩ • x✝¹ = ⟨a, b⟩ • x✝) ↔
    (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ a, ∃ (_ : a ∈ Submonoid.map (algebraMap R A) S), a * x✝¹ = a * x✝
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₂ : MonObj X
one✝ : 𝟙_ C ⟶ X
mul✝ : X ⊗ X ⟶ X
one_mul✝ : one✝ ▷ X ≫ mul✝ = (λ_ X).hom
mul_one✝ : X ◁ one✝ ≫ mul✝ = (ρ_ X).hom
mul_assoc✝ : mul✝ ▷ X ≫ mul✝ = (α_ X X X).hom ≫ X ◁ mul✝ ≫ mul✝
H : μ = μ
this : η = η
⊢ { one := one✝, mul := mul✝, one_mul := one_mul✝, mul_one := mul_one✝, mul_assoc := mul_assoc✝ } = h₂

Tactic:
;

Goal state after:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₂ : MonObj X
one✝ : 𝟙_ C ⟶ X
mul✝ : X ⊗ X ⟶ X
one_mul✝ : one✝ ▷ X ≫ mul✝ = (λ_ X).hom
mul_one✝ : X ◁ one✝ ≫ mul✝ = (ρ_ X).hom
mul_assoc✝ : mul✝ ▷ X ≫ mul✝ = (α_ X X X).hom ≫ X ◁ mul✝ ≫ mul✝
H : μ = μ
this : η = η
⊢ { one := one✝, mul := mul✝, one_mul := one_mul✝, mul_one := mul_one✝, mul_assoc := mul_assoc✝ } = h₂
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
one✝¹ : 𝟙_ C ⟶ X
mul✝¹ : X ⊗ X ⟶ X
one_mul✝¹ : one✝¹ ▷ X ≫ mul✝¹ = (λ_ X).hom
mul_one✝¹ : X ◁ one✝¹ ≫ mul✝¹ = (ρ_ X).hom
mul_assoc✝¹ : mul✝¹ ▷ X ≫ mul✝¹ = (α_ X X X).hom ≫ X ◁ mul✝¹ ≫ mul✝¹
one✝ : 𝟙_ C ⟶ X
mul✝ : X ⊗ X ⟶ X
one_mul✝ : one✝ ▷ X ≫ mul✝ = (λ_ X).hom
mul_one✝ : X ◁ one✝ ≫ mul✝ = (ρ_ X).hom
mul_assoc✝ : mul✝ ▷ X ≫ mul✝ = (α_ X X X).hom ≫ X ◁ mul✝ ≫ mul✝
H : μ = μ
this : η = η
⊢ { one := one✝¹, mul := mul✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, mul_assoc := mul_assoc✝¹ } =
    { one := one✝, mul := mul✝, one_mul := one_mul✝, mul_one := mul_one✝, mul_assoc := mul_assoc✝ }

Tactic:
;

Goal state after:
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
one✝¹ : 𝟙_ C ⟶ X
mul✝¹ : X ⊗ X ⟶ X
one_mul✝¹ : one✝¹ ▷ X ≫ mul✝¹ = (λ_ X).hom
mul_one✝¹ : X ◁ one✝¹ ≫ mul✝¹ = (ρ_ X).hom
mul_assoc✝¹ : mul✝¹ ▷ X ≫ mul✝¹ = (α_ X X X).hom ≫ X ◁ mul✝¹ ≫ mul✝¹
one✝ : 𝟙_ C ⟶ X
mul✝ : X ⊗ X ⟶ X
one_mul✝ : one✝ ▷ X ≫ mul✝ = (λ_ X).hom
mul_one✝ : X ◁ one✝ ≫ mul✝ = (ρ_ X).hom
mul_assoc✝ : mul✝ ▷ X ≫ mul✝ = (α_ X X X).hom ≫ X ◁ mul✝ ≫ mul✝
H : μ = μ
this : η = η
⊢ { one := one✝¹, mul := mul✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, mul_assoc := mul_assoc✝¹ } =
    { one := one✝, mul := mul✝, one_mul := one_mul✝, mul_one := mul_one✝, mul_assoc := mul_assoc✝ }
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
one✝ : 𝟙_ C ⟶ X
mul✝ : X ⊗ X ⟶ X
one_mul✝¹ : one✝ ▷ X ≫ mul✝ = (λ_ X).hom
mul_one✝¹ : X ◁ one✝ ≫ mul✝ = (ρ_ X).hom
mul_assoc✝¹ : mul✝ ▷ X ≫ mul✝ = (α_ X X X).hom ≫ X ◁ mul✝ ≫ mul✝
mul_assoc✝ : μ ▷ X ≫ μ = (α_ X X X).hom ≫ X ◁ μ ≫ μ
one_mul✝ : η ▷ X ≫ μ = (λ_ X).hom
mul_one✝ : X ◁ η ≫ μ = (ρ_ X).hom
⊢ { one := one✝, mul := mul✝, one_mul := one_mul✝¹, mul_one := mul_one✝¹, mul_assoc := mul_assoc✝¹ } =
    { one := η, mul := μ, one_mul := one_mul✝, mul_one := mul_one✝, mul_assoc := mul_assoc✝ }

Tactic:
;

Goal state after:
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
one✝ : 𝟙_ C ⟶ X
mul✝ : X ⊗ X ⟶ X
one_mul✝¹ : one✝ ▷ X ≫ mul✝ = (λ_ X).hom
mul_one✝¹ : X ◁ one✝ ≫ mul✝ = (ρ_ X).hom
mul_assoc✝¹ : mul✝ ▷ X ≫ mul✝ = (α_ X X X).hom ≫ X ◁ mul✝ ≫ mul✝
mul_assoc✝ : μ ▷ X ≫ μ = (α_ X X X).hom ≫ X ◁ μ ≫ μ
one_mul✝ : η ▷ X ≫ μ = (λ_ X).hom
mul_one✝ : X ◁ η ≫ μ = (ρ_ X).hom
⊢ { one := one✝, mul := mul✝, one_mul := one_mul✝¹, mul_one := mul_one✝¹, mul_assoc := mul_assoc✝¹ } =
    { one := η, mul := μ, one_mul := one_mul✝, mul_one := mul_one✝, mul_assoc := mul_assoc✝ }
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 : μ = μ
⊢ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η) ≫ μ = η

Tactic:
· simp [tensorHom_def']

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
this : MonObj X := MonObj.ofIso e
⊢ IsMonHom e.hom

Tactic:
;

Goal state after:
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
this : MonObj X := MonObj.ofIso e
⊢ IsMonHom e.hom
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: case e_6
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
w✝¹ w✝ : ι →₀ R
eq : f ((Finsupp.linearCombination R v) w✝¹) = f ((Finsupp.linearCombination R v) w✝)
⊢ w✝¹ = w✝

Tactic:
;

Goal state after:
case e_6
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
w✝¹ w✝ : ι →₀ R
eq : f ((Finsupp.linearCombination R v) w✝¹) = f ((Finsupp.linearCombination R v) w✝)
⊢ w✝¹ = w✝
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
⊢ Set.range ⇑(ofIsLocalizedModule Rₛ S f b) = ⇑f '' Set.range ⇑b

Tactic:
;

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
b : Basis ι R M
⊢ Set.range ⇑(ofIsLocalizedModule Rₛ S f b) = ⇑f '' Set.range ⇑b
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
x✝ : Mₛ
⊢ x✝ ∈ Set.range ⇑(ofIsLocalizedModule Rₛ S f b) ↔ x✝ ∈ ⇑f '' Set.range ⇑b

Tactic:
;

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
b : Basis ι R M
x✝ : Mₛ
⊢ x✝ ∈ Set.range ⇑(ofIsLocalizedModule Rₛ S f b) ↔ x✝ ∈ ⇑f '' Set.range ⇑b
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₁✝ X₂✝ Y₂✝ : Mon C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ f✝ ⊗ₘ g✝ = f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝

Tactic:
;

Goal state after:
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₁✝ X₂✝ Y₂✝ : Mon C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ f✝ ⊗ₘ g✝ = f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
x✝ y✝ : M →ₗ[R] N
⊢ extendScalarsOfIsLocalization S A (x✝ + y✝) =
    extendScalarsOfIsLocalization S A x✝ + extendScalarsOfIsLocalization S A y✝

Tactic:
;

Goal state after:
R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
x✝ y✝ : M →ₗ[R] N
⊢ extendScalarsOfIsLocalization S A (x✝ + y✝) =
    extendScalarsOfIsLocalization S A x✝ + extendScalarsOfIsLocalization S A y✝
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₁✝ X₂✝ Y₂✝ : Mon C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ (f✝ ⊗ₘ g✝).hom = (f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝).hom

Tactic:
;

Goal state after:
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₁✝ X₂✝ Y₂✝ : Mon C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ (f✝ ⊗ₘ g✝).hom = (f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝).hom
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
x✝¹ y✝ : M →ₗ[R] N
x✝ : M
⊢ (extendScalarsOfIsLocalization S A (x✝¹ + y✝)) x✝ =
    (extendScalarsOfIsLocalization S A x✝¹ + extendScalarsOfIsLocalization S A y✝) x✝

Tactic:
;

Goal state after:
R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
x✝¹ y✝ : M →ₗ[R] N
x✝ : M
⊢ (extendScalarsOfIsLocalization S A (x✝¹ + y✝)) x✝ =
    (extendScalarsOfIsLocalization S A x✝¹ + extendScalarsOfIsLocalization S A y✝) x✝
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
m✝ : A
x✝ : M →ₗ[R] N
⊢ extendScalarsOfIsLocalization S A (m✝ • x✝) = (RingHom.id A) m✝ • extendScalarsOfIsLocalization S A x✝

Tactic:
;

Goal state after:
R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
m✝ : A
x✝ : M →ₗ[R] N
⊢ extendScalarsOfIsLocalization S A (m✝ • x✝) = (RingHom.id A) m✝ • extendScalarsOfIsLocalization S A x✝
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
m✝ : A
x✝¹ : M →ₗ[R] N
x✝ : M
⊢ (extendScalarsOfIsLocalization S A (m✝ • x✝¹)) x✝ = ((RingHom.id A) m✝ • extendScalarsOfIsLocalization S A x✝¹) x✝

Tactic:
;

Goal state after:
R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
m✝ : A
x✝¹ : M →ₗ[R] N
x✝ : M
⊢ (extendScalarsOfIsLocalization S A (m✝ • x✝¹)) x✝ = ((RingHom.id A) m✝ • extendScalarsOfIsLocalization S A x✝¹) x✝
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
x✝ : M →ₗ[R] N
⊢ ↑R (extendScalarsOfIsLocalization S A x✝) = x✝

Tactic:
;

Goal state after:
R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
x✝ : M →ₗ[R] N
⊢ ↑R (extendScalarsOfIsLocalization S A x✝) = x✝
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
x✝¹ : M →ₗ[R] N
x✝ : M
⊢ (↑R (extendScalarsOfIsLocalization S A x✝¹)) x✝ = x✝¹ x✝

Tactic:
;

Goal state after:
R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
x✝¹ : M →ₗ[R] N
x✝ : M
⊢ (↑R (extendScalarsOfIsLocalization S A x✝¹)) x✝ = x✝¹ x✝
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
x✝ : M →ₗ[A] N
⊢ extendScalarsOfIsLocalization S A (↑R x✝) = x✝

Tactic:
;

Goal state after:
R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
x✝ : M →ₗ[A] N
⊢ extendScalarsOfIsLocalization S A (↑R x✝) = x✝