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

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • (r₃ /ₒ s₃)

Tactic:
;

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • (r₃ /ₒ s₃)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
hb' : (r₂ /ₒ s₂) • (r₃ /ₒ s₃) = rb • r₃ /ₒ (sb * s₂)
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • (r₃ /ₒ s₃)

Tactic:
;

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
hb' : (r₂ /ₒ s₂) • (r₃ /ₒ s₃) = rb • r₃ /ₒ (sb * s₂)
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • (r₃ /ₒ s₃)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
d : P
hc : k (d * x) = k (d * y)
hd : k d = ↑c
⊢ ↑⟨d, ⋯⟩ * x = ↑⟨d, ⋯⟩ * y

Tactic:
;

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
d : P
hc : k (d * x) = k (d * y)
hd : k d = ↑c
⊢ ↑⟨d, ⋯⟩ * x = ↑⟨d, ⋯⟩ * y
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
hb' : (r₂ /ₒ s₂) • (r₃ /ₒ s₃) = rb • r₃ /ₒ (sb * s₂)
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))

Tactic:
;

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
hb' : (r₂ /ₒ s₂) • (r₃ /ₒ s₃) = rb • r₃ /ₒ (sb * s₂)
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x✝ : M
⊢ (f.ofMulEquivOfDom ⋯) x✝ = f x✝

Tactic:
;

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x✝ : M
⊢ (f.ofMulEquivOfDom ⋯) x✝ = f x✝
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f) ((monoidOf S).mk' x y) = f.mk' x y

Tactic:
;

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f) ((monoidOf S).mk' x y) = f.mk' x y
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f).symm (f.mk' x y) = (monoidOf S).mk' x y

Tactic:
;

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f).symm (f.mk' x y) = (monoidOf S).mk' x y
Module: Mathlib.GroupTheory.OreLocalization.Basic

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

pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑sc * (ra * r₂) = rc * rb * ↑s₃

Tactic:
;

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ (rc * rb) • r₃ /ₒ (sc * (sa * s₁)) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))

case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑sc * (ra * r₂) = rc * rb * ↑s₃
Module: Mathlib.Algebra.Order.Hom.Ring

Goal state before:
pp: case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
g : α →+*o β
toRingHom✝ : α →+* β
monotone'✝ : Monotone (↑↑toRingHom✝).toFun
h :
  (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝, monotone' := monotone'✝ } =
    (fun f ↦ (↑↑f.toRingHom).toFun) g
⊢ { toRingHom := toRingHom✝, monotone' := monotone'✝ } = g

Tactic:
;

Goal state after:
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
g : α →+*o β
toRingHom✝ : α →+* β
monotone'✝ : Monotone (↑↑toRingHom✝).toFun
h :
  (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝, monotone' := monotone'✝ } =
    (fun f ↦ (↑↑f.toRingHom).toFun) g
⊢ { toRingHom := toRingHom✝, monotone' := monotone'✝ } = g
Module: Mathlib.Algebra.Order.Hom.Ring

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
toRingHom✝¹ : α →+* β
monotone'✝¹ : Monotone (↑↑toRingHom✝¹).toFun
toRingHom✝ : α →+* β
monotone'✝ : Monotone (↑↑toRingHom✝).toFun
h :
  (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝¹, monotone' := monotone'✝¹ } =
    (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝, monotone' := monotone'✝ }
⊢ { toRingHom := toRingHom✝¹, monotone' := monotone'✝¹ } = { toRingHom := toRingHom✝, monotone' := monotone'✝ }

Tactic:
;

Goal state after:
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
toRingHom✝¹ : α →+* β
monotone'✝¹ : Monotone (↑↑toRingHom✝¹).toFun
toRingHom✝ : α →+* β
monotone'✝ : Monotone (↑↑toRingHom✝).toFun
h :
  (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝¹, monotone' := monotone'✝¹ } =
    (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝, monotone' := monotone'✝ }
⊢ { toRingHom := toRingHom✝¹, monotone' := monotone'✝¹ } = { toRingHom := toRingHom✝, monotone' := monotone'✝ }
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
y : ↥S
⊢ f ↑y = f.toMonoidHom ↑y

Tactic:
;

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
y : ↥S
⊢ f ↑y = f.toMonoidHom ↑y
Module: Mathlib.GroupTheory.OreLocalization.Basic

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

Tactic:
;

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂)) = rc • rb • r₃ /ₒ (sc * sa * s₁)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
| mk x 1

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
| mk x 1
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
| mk x (1 * 1)

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
| mk x (1 * 1)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
⊢ ↑(fS 1)⁻¹ * f 1 = 1

Tactic:
;

Goal state after:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
⊢ ↑(fS 1)⁻¹ * f 1 = 1
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁) * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₂ /ₒ s₂)

Tactic:
;

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁) * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₂ /ₒ s₂)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
⊢ (if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) a b) = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
⊢ (if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) a b) = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
⊢ ⊤ = Option.bind ⊤ fun a ↦ Option.some (a * b)

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
⊢ ⊤ = Option.bind ⊤ fun a ↦ Option.some (a * b)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : α
ha : a ≠ 0
⊢ ⊤ = Option.bind ⊤ fun b ↦ Option.some (a * b)

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : α
ha : a ≠ 0
⊢ ⊤ = Option.bind ⊤ fun b ↦ Option.some (a * b)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : a = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

Tactic:
;

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : a = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : ¬b = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

Tactic:
;

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : ¬b = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (ra * r₂ /ₒ (sa * s₁)) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁) * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₂ /ₒ s₂)

Tactic:
;

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (ra * r₂ /ₒ (sa * s₁)) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁) * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₂ /ₒ s₂)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : ¬b = 0
ha : ¬⊤ = 0
⊢ untopD 0 (⊤ * b) = untopD 0 ⊤ * untopD 0 b

pp: case neg.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : ¬b = 0
a✝ : α
ha : ¬↑a✝ = 0
⊢ untopD 0 (↑a✝ * b) = untopD 0 ↑a✝ * untopD 0 b

Tactic:
;

Goal state after:
case neg.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : ¬b = 0
ha : ¬⊤ = 0
⊢ untopD 0 (⊤ * b) = untopD 0 ⊤ * untopD 0 b

case neg.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : ¬b = 0
a✝ : α
ha : ¬↑a✝ = 0
⊢ untopD 0 (↑a✝ * b) = untopD 0 ↑a✝ * untopD 0 b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.coe.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊤ = 0
⊢ untopD 0 (↑a✝ * ⊤) = untopD 0 ↑a✝ * untopD 0 ⊤

pp: case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ untopD 0 (↑a✝¹ * ↑a✝) = untopD 0 ↑a✝¹ * untopD 0 ↑a✝

Tactic:
;

Goal state after:
case neg.coe.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊤ = 0
⊢ untopD 0 (↑a✝ * ⊤) = untopD 0 ↑a✝ * untopD 0 ⊤

case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ untopD 0 (↑a✝¹ * ↑a✝) = untopD 0 ↑a✝¹ * untopD 0 ↑a✝
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
x : OreLocalization S R
⊢ φ x = (universalMulHom f fS hf) x

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
x : OreLocalization S R
⊢ φ x = (universalMulHom f fS hf) x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
b c : WithTop α
⊢ 0 * b * c = 0 * (b * c)

pp: case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
⊢ a * b * c = a * (b * c)

Tactic:
;

Goal state after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
b c : WithTop α
⊢ 0 * b * c = 0 * (b * c)

case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
⊢ a * b * c = a * (b * c)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a c : WithTop α
ha : a ≠ 0
⊢ a * 0 * c = a * (0 * c)

pp: case inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b * c = a * (b * c)

Tactic:
;

Goal state after:
case inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a c : WithTop α
ha : a ≠ 0
⊢ a * 0 * c = a * (0 * c)

case inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b * c = a * (b * c)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b : WithTop α
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b * 0 = a * (b * 0)

pp: case inr.inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a * b * c = a * (b * c)

Tactic:
;

Goal state after:
case inr.inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b : WithTop α
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b * 0 = a * (b * 0)

case inr.inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a * b * c = a * (b * c)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
⊢ (match a, 0 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    1

Tactic:
;

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
⊢ (match a, 0 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    1
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n✝ n : ℕ
a : WithTop α
⊢ (match a, n + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match a, n with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      a

Tactic:
;

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n✝ n : ℕ
a : WithTop α
⊢ (match a, n + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match a, n with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      a
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
r : R
m : R'
x : OreLocalization S X
⊢ ((r • m) • 1 /ₒ 1) • x = (r • 1 /ₒ 1) • (m • 1 /ₒ 1) • x

Tactic:
← mul_smul,

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
r : R
m : R'
x : OreLocalization S X
⊢ ((r • m) • 1 /ₒ 1) • x = (r • 1 /ₒ 1 * (m • 1 /ₒ 1)) • x
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
r : R
m : OreLocalization S M
x : OreLocalization S X
⊢ ((r • 1 /ₒ 1) • m) • x = (r • 1 /ₒ 1) • m • x

Tactic:
← mul_smul,

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
r : R
m : OreLocalization S M
x : OreLocalization S X
⊢ ((r • 1 /ₒ 1) • m) • x = (r • 1 /ₒ 1 * m) • x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : CommMonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a b : WithTop α
⊢ (if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) a b) =
    if b = 0 ∨ a = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) b a

Tactic:
;

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : CommMonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a b : WithTop α
⊢ (if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) a b) =
    if b = 0 ∨ a = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) b a