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

Goal state before:
pp: case h.right
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ ↑sd * (rc * ↑sa * ↑s₁) = ↑sd * rc * (↑sa * ↑s₁)

Tactic:
mul_assoc,

Goal state after:
case h.right
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ ↑sd * (rc * (↑sa * ↑s₁)) = ↑sd * rc * (↑sa * ↑s₁)
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : ↑sb * ↑s₁ = rb * ↑s₁'
rc : R
sc : ↥S
hc : ↑sc * ↑s₁' = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rb = rd * ↑sc
⊢ ↑sd * ↑sb * ↑s₁ = rd * rc * ↑s₂

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : ↑sb * ↑s₁ = rb * ↑s₁'
rc : R
sc : ↥S
hc : ↑sc * ↑s₁' = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rb = rd * ↑sc
⊢ ↑sd * (↑sb * ↑s₁) = rd * rc * ↑s₂
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : ↑sb * ↑s₁ = rb * ↑s₁'
rc : R
sc : ↥S
hc : ↑sc * ↑s₁' = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rb = rd * ↑sc
⊢ rd * ↑sc * ↑s₁' = rd * rc * ↑s₂

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : ↑sb * ↑s₁ = rb * ↑s₁'
rc : R
sc : ↥S
hc : ↑sc * ↑s₁' = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rb = rd * ↑sc
⊢ rd * (↑sc * ↑s₁') = rd * rc * ↑s₂
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : ↑sb * ↑s₂ = rb * ↑s₁
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : ↑sc * ↑s₃ = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rc = rd * ↑sb
⊢ rd * rb * ↑s₁ = ↑sd * ↑sc * ↑s₃

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : ↑sb * ↑s₂ = rb * ↑s₁
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : ↑sc * ↑s₃ = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rc = rd * ↑sb
⊢ rd * (rb * ↑s₁) = ↑sd * ↑sc * ↑s₃
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : ↑sb * ↑s₂ = rb * ↑s₁
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : ↑sc * ↑s₃ = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rc = rd * ↑sb
⊢ ↑sd * rc * ↑s₂ = ↑sd * ↑sc * ↑s₃

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : ↑sb * ↑s₂ = rb * ↑s₁
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : ↑sc * ↑s₃ = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rc = rd * ↑sb
⊢ ↑sd * (rc * ↑s₂) = ↑sd * ↑sc * ↑s₃
Module: Mathlib.GroupTheory.MonoidLocalization.Divisibility

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m₁ m₂ : M
x✝ : f m₁ ∣ f m₂
n : N
eq : f m₂ = f m₁ * n
m : M
s : ↥S
hn : f (m₂ * ↑(m, s).2) = f (m₁ * (m, s).1)
s' : ↥S
hs' : ↑s' * (m₂ * ↑(m, s).2) = ↑s' * (m₁ * (m, s).1)
⊢ ↑s' * ↑s * m₂ = ↑s' * (m₁ * m)

Tactic:
mul_assoc,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m₁ m₂ : M
x✝ : f m₁ ∣ f m₂
n : N
eq : f m₂ = f m₁ * n
m : M
s : ↥S
hn : f (m₂ * ↑(m, s).2) = f (m₁ * (m, s).1)
s' : ↥S
hs' : ↑s' * (m₂ * ↑(m, s).2) = ↑s' * (m₁ * (m, s).1)
⊢ ↑s' * (↑s * m₂) = ↑s' * (m₁ * m)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r : X
s : ↥S
⊢ (0 /ₒ 1) • (r /ₒ s) = 0

Tactic:
oreDiv_smul_char 0 r 1 s 0 1 (by simp)

Goal state after:
case c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r : X
s : ↥S
⊢ 0 • r /ₒ (1 * 1) = 0
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
⊢ ↑sb * ra * ↑s₃ ∈ S

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
⊢ ↑sb * (ra * ↑s₃) ∈ S
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * (↑sa * r₂) = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra * r₃) = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((↑sc * ↑sb * (↑sa * r₂) + ↑sc * ↑sb * (ra * r₃)) /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) =
    (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))

Tactic:
mul_assoc,

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * (↑sa * r₂) = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra * r₃) = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((↑sc * (↑sb * (↑sa * r₂)) + ↑sc * ↑sb * (ra * r₃)) /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) =
    (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * (↑sa * r₂) = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra * r₃) = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((↑sc * (rb * ↑s₁) + ↑sc * ↑sb * (ra * r₃)) /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) =
    (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))

Tactic:
mul_assoc,

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * (↑sa * r₂) = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra * r₃) = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((↑sc * (rb * ↑s₁) + ↑sc * (↑sb * (ra * r₃))) /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) =
    (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * (f ↑s₃ * f r₁) + ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * (f r₃ * f r₂) =
    ↑(fS s₁)⁻¹ * f r₁ + ↑(fS s₂)⁻¹ * f r₂

Tactic:
mul_assoc,

Goal state after:
case c.c
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * (↑(fS s₃)⁻¹ * (f ↑s₃ * f r₁)) + ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * (f r₃ * f r₂) =
    ↑(fS s₁)⁻¹ * f r₁ + ↑(fS s₂)⁻¹ * f r₂
Module: Mathlib.RingTheory.Localization.Defs

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
x : R
y : ↥M
z : R
h : z * ↑y = x
⊢ (algebraMap R S) z * (algebraMap R S) ↑y = (algebraMap R S) x

Tactic:
rw [← h, map_mul]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ * w +
        ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ * ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y) * z₁ =
      z₂ ↔
    w +
        g ↑y *
          (↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ * ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y) * z₁) =
      g ↑y * z₂

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ * w +
        ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ * (↑((IsUnit.liftRight ((↑g).domRestrict M) h) y) * z₁) =
      z₂ ↔
    w +
        g ↑y *
          (↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ * (↑((IsUnit.liftRight ((↑g).domRestrict M) h) y) * z₁)) =
      g ↑y * z₂
Module: Mathlib.RingTheory.Localization.Defs

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
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 * ((toLocalizationMap M S).lift hg) y *
        g ↑((toLocalizationMap M S).sec x).2 +
      g ((toLocalizationMap M S).sec x).1 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 =
    g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 *
        (((toLocalizationMap M S).lift hg) y * g ↑((toLocalizationMap M S).sec x).2) +
      g ((toLocalizationMap M S).sec x).1 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 =
    g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1
Module: Mathlib.RingTheory.Localization.Defs

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
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ ((toLocalizationMap M S).lift hg) y * g ↑((toLocalizationMap M S).sec x).2 *
        ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 +
      g ((toLocalizationMap M S).sec x).1 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 =
    g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ ((toLocalizationMap M S).lift hg) y *
        (g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2) +
      g ((toLocalizationMap M S).sec x).1 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 =
    g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : y * (algebraMap R S) ↑(x, s).2 = (algebraMap R S) (x, s).1
u : Rˣ
hu : ↑u = ↑s
⊢ y * (algebraMap R S) ↑u * (algebraMap R S) ↑u⁻¹ = y

Tactic:
mul_assoc,

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : y * (algebraMap R S) ↑(x, s).2 = (algebraMap R S) (x, s).1
u : Rˣ
hu : ↑u = ↑s
⊢ y * ((algebraMap R S) ↑u * (algebraMap R S) ↑u⁻¹) = y
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ IsFractionRing R R ↔ Function.Surjective ⇑(algebraMap R K)

Tactic:
rw [self_iff_bijective K, Function.Bijective, and_iff_right (IsFractionRing.injective R K)]

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
c : R
hmc : c ∈ ↑M₁
hc : (algebraMap R S₂) (c * r) = (algebraMap R S₂) (c * s)
a : ↥M₂
ha : ↑a * (c * r) = ↑a * (c * s)
⊢ ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * x * (algebraMap R S₁) ↑d = ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * y * (algebraMap R S₁) ↑d

Tactic:
mul_assoc,

Goal state after:
case h
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
c : R
hmc : c ∈ ↑M₁
hc : (algebraMap R S₂) (c * r) = (algebraMap R S₂) (c * s)
a : ↥M₂
ha : ↑a * (c * r) = ↑a * (c * s)
⊢ ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * (x * (algebraMap R S₁) ↑d) = ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * y * (algebraMap R S₁) ↑d
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
c : R
hmc : c ∈ ↑M₁
hc : (algebraMap R S₂) (c * r) = (algebraMap R S₂) (c * s)
a : ↥M₂
ha : ↑a * (c * r) = ↑a * (c * s)
⊢ ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * (algebraMap R S₁) r = ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * y * (algebraMap R S₁) ↑d

Tactic:
mul_assoc,

Goal state after:
case h
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
c : R
hmc : c ∈ ↑M₁
hc : (algebraMap R S₂) (c * r) = (algebraMap R S₂) (c * s)
a : ↥M₂
ha : ↑a * (c * r) = ↑a * (c * s)
⊢ ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * (algebraMap R S₁) r = ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * (y * (algebraMap R S₁) ↑d)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
c : R
hmc : c ∈ ↑M₁
hc : (algebraMap R S₂) (c * r) = (algebraMap R S₂) (c * s)
a : ↥M₂
ha : ↑a * (c * r) = ↑a * (c * s)
⊢ (algebraMap R S₁) (↑a * r * ↑⟨c, hmc⟩) =
    ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * (algebraMap R S₁) s * (algebraMap R S₁) ↑⟨c, hmc⟩

Tactic:
mul_assoc,

Goal state after:
case h
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
c : R
hmc : c ∈ ↑M₁
hc : (algebraMap R S₂) (c * r) = (algebraMap R S₂) (c * s)
a : ↥M₂
ha : ↑a * (c * r) = ↑a * (c * s)
⊢ (algebraMap R S₁) (↑a * (r * ↑⟨c, hmc⟩)) =
    ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * (algebraMap R S₁) s * (algebraMap R S₁) ↑⟨c, hmc⟩
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ (algebraMap R Rₘ) (r * n * ↑⟨m, hm⟩) = (algebraMap R Rₘ) r

Tactic:
mul_assoc,

Goal state after:
R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ (algebraMap R Rₘ) (r * (n * ↑⟨m, hm⟩)) = (algebraMap R Rₘ) r
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - r⁻¹ • (b * a))
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)

Tactic:
simpa only [mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one, ← Units.smul_def,
    IsUnit.smul_sub_iff_sub_inv_smul, smul_mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
a : A
⊢ σ (star a) = star (σ a)

Tactic:
by
  ext
  simpa only [Set.mem_star, mem_iff, not_iff_not] using! star_mem_resolventSet_iff.symm

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R✝ : Type u_1
A✝ : Type u_2
B✝ : Type u_3
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : NonUnitalNonAssocSemiring A✝
inst✝¹⁵ : NonUnitalNonAssocSemiring B✝
inst✝¹⁴ : Module R✝ A✝
inst✝¹³ : Module R✝ B✝
inst✝¹² : SMulCommClass R✝ A✝ A✝
inst✝¹¹ : SMulCommClass R✝ B✝ B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ A✝
inst✝⁹ : IsScalarTower R✝ B✝ B✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
⊢ (LinearMap.liftBaseChange S ↑f) 1 = 1

Tactic:
by simp [Algebra.TensorProduct.one_def]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝²⁶ : CommSemiring R
inst✝²⁵ : CommSemiring S
inst✝²⁴ : Algebra R S
inst✝²³ : Semiring A
inst✝²² : Algebra R A
inst✝²¹ : Algebra S A
inst✝²⁰ : IsScalarTower R S A
inst✝¹⁹ : Semiring B
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : Semiring C
inst✝¹⁶ : Algebra R C
inst✝¹⁵ : Algebra S C
inst✝¹⁴ : IsScalarTower R S C
inst✝¹³ : Semiring D
inst✝¹² : Algebra R D
inst✝¹¹ : Semiring E
inst✝¹⁰ : Algebra R E
inst✝⁹ : Algebra S E
inst✝⁸ : IsScalarTower R S E
inst✝⁷ : Semiring F
inst✝⁶ : Algebra R F
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : Algebra T A
inst✝¹ : IsScalarTower R T A
inst✝ : IsScalarTower S T A
⊢ (AlgebraTensorModule.assoc R S T A C D) 1 = 1

Tactic:
by simp [Algebra.TensorProduct.one_def]

Goal state after: