mathlib-initiative/mathlib-tactics huggingface dataset:
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
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * ↑s₁ ∈ S
hs₂ : u * s₂ = ⟨v * ↑s₁, s₁vS⟩
⊢ P (u • r₂) (u * s₂) = P (↑u • r₂) ⟨↑u * ↑s₂, ⋯⟩

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
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * ↑s₁ ∈ S
hs₂ : u * s₂ = ⟨v * ↑s₁, s₁vS⟩
⊢ P (u • r₂) (u * s₂) = P (↑u • r₂) ⟨↑u * ↑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)
x : M
v : P
y : ↥S
⊢ g x * ↑((IsUnit.liftRight (g.domRestrict S) hg) y)⁻¹ = v ↔ g x = g ↑y * v

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)
x : M
v : P
y : ↥S
⊢ g x * ↑((IsUnit.liftRight (g.domRestrict S) hg) y)⁻¹ = v ↔ g x = g ↑y * v
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
P : Type u_3
inst✝ : CommMonoid P
a b c : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑c.2 * b.1) = ↑t₂ * (↑b.2 * c.1)
⊢ ↑t₂ * ↑c.2 * (↑t₁ * (↑a.2 * b.1)) = ↑t₁ * ↑a.2 * (↑t₂ * (↑c.2 * b.1))

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
a b c : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑c.2 * b.1) = ↑t₂ * (↑b.2 * c.1)
⊢ ↑t₂ * ↑c.2 * (↑t₁ * (↑a.2 * b.1)) = ↑t₁ * ↑a.2 * (↑t₂ * (↑c.2 * b.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
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
r₁ : X
t₁ : R
s₁ : ↥S
ht₁ : t₁ * ↑s₁ ∈ S
x : OreLocalization S X
⊢ liftExpand (P r₁ s₁) ⋯ x = liftExpand (P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩) ⋯ x

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
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
r₁ : X
t₁ : R
s₁ : ↥S
ht₁ : t₁ * ↑s₁ ∈ S
x : OreLocalization S X
⊢ liftExpand (P r₁ s₁) ⋯ x = liftExpand (P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩) ⋯ x
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g₁ : α ≃*o β
f : β ≃*o γ
hf : Injective ⇑f
⊢ g₁.trans f = g₁.trans f

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g₁ : α ≃*o β
f : β ≃*o γ
hf : Injective ⇑f
⊢ g₁.trans f = g₁.trans f
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
r₁ : X
t₁ : R
s₁ : ↥S
ht₁ : t₁ * ↑s₁ ∈ S
r₂ : X
s₂ : ↥S
⊢ P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (1 • r₂) ⟨1 * ↑s₂, ⋯⟩ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ r₂ s₂

Tactic:
;

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
r₁ : X
t₁ : R
s₁ : ↥S
ht₁ : t₁ * ↑s₁ ∈ S
r₂ : X
s₂ : ↥S
⊢ P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (1 • r₂) ⟨1 * ↑s₂, ⋯⟩ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ r₂ s₂
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
P : Type u_3
inst✝ : CommMonoid P
a b c : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑c.2 * b.1) = ↑t₂ * (↑b.2 * c.1)
⊢ ↑t₁ * ↑a.2 * (↑t₂ * (↑b.2 * c.1)) = ↑t₂ * ↑t₁ * ↑b.2 * (↑a.2 * c.1)

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
a b c : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑c.2 * b.1) = ↑t₂ * (↑b.2 * c.1)
⊢ ↑t₁ * ↑a.2 * (↑t₂ * (↑b.2 * c.1)) = ↑t₂ * ↑t₁ * ↑b.2 * (↑a.2 * c.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_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
h₀ : ↑(oreDenom r₁ s₂) * r₁ = oreNum r₁ s₂ * ↑s₂
⊢ oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁) = v • r₂ /ₒ (u * s₁)

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
h₀ : ↑(oreDenom r₁ s₂) * r₁ = oreNum r₁ s₂ * ↑s₂
⊢ oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁) = v • r₂ /ₒ (u * s₁)
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_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
h₀ : ↑(oreDenom r₁ s₂) * r₁ = v₀ * ↑s₂
⊢ v₀ • r₂ /ₒ (oreDenom r₁ s₂ * s₁) = v • r₂ /ₒ (u * s₁)

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
h₀ : ↑(oreDenom r₁ s₂) * r₁ = v₀ * ↑s₂
⊢ v₀ • r₂ /ₒ (oreDenom r₁ s₂ * s₁) = v • r₂ /ₒ (u * 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)
x : M
⊢ g (f.sec (f x)).1 = g (↑(f.sec (f x)).2 * x)

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)
x : M
⊢ g (f.sec (f x)).1 = g (↑(f.sec (f x)).2 * x)
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
P : Type u_3
inst✝ : CommMonoid P
a b c d : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑d.2 * c.1) = ↑t₂ * (↑c.2 * d.1)
⊢ ↑t₂ * (↑c.2 * d.1) * (↑t₁ * (↑a.2 * b.1)) = ↑t₂ * ↑t₁ * (↑a.2 * ↑c.2 * (b.1 * d.1))

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
a b c d : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑d.2 * c.1) = ↑t₂ * (↑c.2 * d.1)
⊢ ↑t₂ * (↑c.2 * d.1) * (↑t₁ * (↑a.2 * b.1)) = ↑t₂ * ↑t₁ * (↑a.2 * ↑c.2 * (b.1 * d.1))
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)
x✝ : M
⊢ ((f.lift hg).comp f.toMonoidHom) x✝ = g x✝

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)
x✝ : M
⊢ ((f.lift hg).comp f.toMonoidHom) x✝ = g 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
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
j : N →* P
x✝ : N
⊢ (f.lift ⋯) x✝ = j x✝

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
j : N →* P
x✝ : N
⊢ (f.lift ⋯) x✝ = j x✝
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_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := ⋯
u₀ : ↥S := ⋯
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ v • r₂ /ₒ (u * s₁) = v₀ • r₂ /ₒ (u₀ * s₁)

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := ⋯
u₀ : ↥S := ⋯
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ v • r₂ /ₒ (u * s₁) = v₀ • r₂ /ₒ (u₀ * s₁)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case mk
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
p : Localization S → Sort u
f : (a : M) → (b : ↥S) → p (mk a b)
H : ∀ {a c : M} {b d : ↥S} (h : (r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d
x : Localization S
z : M × ↥S
fst✝ : M
snd✝ : ↥S
h : (OreLocalization.oreEqv S M) (fst✝, snd✝) z
⊢ ⋯ ▸ f (fst✝, snd✝).1 (fst✝, snd✝).2 = f z.1 z.2

Tactic:
;

Goal state after:
case mk
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
p : Localization S → Sort u
f : (a : M) → (b : ↥S) → p (mk a b)
H : ∀ {a c : M} {b d : ↥S} (h : (r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d
x : Localization S
z : M × ↥S
fst✝ : M
snd✝ : ↥S
h : (OreLocalization.oreEqv S M) (fst✝, snd✝) z
⊢ ⋯ ▸ f (fst✝, snd✝).1 (fst✝, snd✝).2 = f z.1 z.2
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
p : Localization S → Sort u
f : (a : M) → (b : ↥S) → p (mk a b)
H : ∀ {a c : M} {b d : ↥S} (h : (r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d
x : Localization S
fst✝¹ : M
snd✝¹ : ↥S
fst✝ : M
snd✝ : ↥S
h : (OreLocalization.oreEqv S M) (fst✝¹, snd✝¹) (fst✝, snd✝)
⊢ ⋯ ▸ f (fst✝¹, snd✝¹).1 (fst✝¹, snd✝¹).2 = f (fst✝, snd✝).1 (fst✝, snd✝).2

Tactic:
;

Goal state after:
case mk.mk
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
p : Localization S → Sort u
f : (a : M) → (b : ↥S) → p (mk a b)
H : ∀ {a c : M} {b d : ↥S} (h : (r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d
x : Localization S
fst✝¹ : M
snd✝¹ : ↥S
fst✝ : M
snd✝ : ↥S
h : (OreLocalization.oreEqv S M) (fst✝¹, snd✝¹) (fst✝, snd✝)
⊢ ⋯ ▸ f (fst✝¹, snd✝¹).1 (fst✝¹, snd✝¹).2 = f (fst✝, snd✝).1 (fst✝, snd✝).2
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : G ≃*o H
a✝ : G
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ }) x✝))
      a✝ =
    x✝ a✝

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : G ≃*o H
a✝ : G
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ }) x✝))
      a✝ =
    x✝ a✝
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : WithZero G ≃*o WithZero H
x : WithZero G
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ }) x✝))
      x =
    x✝ x

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : WithZero G ≃*o WithZero H
x : WithZero G
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ }) x✝))
      x =
    x✝ x
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case mk
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
b✝ : Localization S
x : M
y : ↥S
⊢ ∃ a, mkHom a = Quot.mk ⇑(OreLocalization.oreEqv S M) (x, y)

Tactic:
;

Goal state after:
case mk
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
b✝ : Localization S
x : M
y : ↥S
⊢ ∃ a, mkHom a = Quot.mk ⇑(OreLocalization.oreEqv S M) (x, y)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ c • (a /ₒ b) = c • a /ₒ b

Tactic:
← OreLocalization.smul_one_oreDiv_one_smul,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ (c • 1 /ₒ 1) • (a /ₒ b) = c • a /ₒ b
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case mk
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
g : S.LocalizationMap N
toMulHom✝ : M →ₙ* N
isLocalizationMap✝ : S.IsLocalizationMap toMulHom✝.toFun
⊢ { toMulHom := toMulHom✝, isLocalizationMap := isLocalizationMap✝ }.toMonoidHom = g.toMonoidHom →
    { toMulHom := toMulHom✝, isLocalizationMap := isLocalizationMap✝ } = g

Tactic:
;

Goal state after:
case mk
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
g : S.LocalizationMap N
toMulHom✝ : M →ₙ* N
isLocalizationMap✝ : S.IsLocalizationMap toMulHom✝.toFun
⊢ { toMulHom := toMulHom✝, isLocalizationMap := isLocalizationMap✝ }.toMonoidHom = g.toMonoidHom →
    { toMulHom := toMulHom✝, isLocalizationMap := isLocalizationMap✝ } = g
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case mk.e'_6
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
g : S.LocalizationMap N
toMulHom✝ : M →ₙ* N
isLocalizationMap✝ : S.IsLocalizationMap toMulHom✝.toFun
eq : { toMulHom := toMulHom✝, isLocalizationMap := isLocalizationMap✝ }.toMonoidHom = g.toMonoidHom
⊢ toMulHom✝ = g.toMulHom

Tactic:
;

Goal state after:
case mk.e'_6
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
g : S.LocalizationMap N
toMulHom✝ : M →ₙ* N
isLocalizationMap✝ : S.IsLocalizationMap toMulHom✝.toFun
eq : { toMulHom := toMulHom✝, isLocalizationMap := isLocalizationMap✝ }.toMonoidHom = g.toMonoidHom
⊢ toMulHom✝ = g.toMulHom
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case mk.e'_6
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
g : S.LocalizationMap N
toMulHom✝ : M →ₙ* N
isLocalizationMap✝ : S.IsLocalizationMap toMulHom✝.toFun
eq : { toMulHom := toMulHom✝, isLocalizationMap := isLocalizationMap✝ }.toMonoidHom = g.toMonoidHom
x✝ : M
⊢ toMulHom✝ x✝ = g.toMulHom x✝

Tactic:
;

Goal state after:
case mk.e'_6
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
g : S.LocalizationMap N
toMulHom✝ : M →ₙ* N
isLocalizationMap✝ : S.IsLocalizationMap toMulHom✝.toFun
eq : { toMulHom := toMulHom✝, isLocalizationMap := isLocalizationMap✝ }.toMonoidHom = g.toMonoidHom
x✝ : M
⊢ toMulHom✝ x✝ = g.toMulHom x✝
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this✝ : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ ↑(s₄' * (s₃' * (s₁' * s))) = ↑⟨↑s₄' * (r₃' * (↑s₂' * ↑s)), ⋯⟩

Tactic:
;

Goal state after:
case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this✝ : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ ↑(s₄' * (s₃' * (s₁' * s))) = ↑⟨↑s₄' * (r₃' * (↑s₂' * ↑s)), ⋯⟩
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
z : N
⊢ f (f.sec z).1 = z * f ↑(f.sec z).2

Tactic:
sec_spec

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z : N
⊢ f (f.sec z).1 = f (f.sec z).1
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ ↑⟨↑s₄' * (r₃' * (↑s₁' * ↑s)), ⋯⟩ = ↑(s₄' * (s₃' * (s₂' * ⟨r₂ * ↑s, hs⟩)))

Tactic:
;

Goal state after:
case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ ↑⟨↑s₄' * (r₃' * (↑s₁' * ↑s)), ⋯⟩ = ↑(s₄' * (s₃' * (s₂' * ⟨r₂ * ↑s, hs⟩)))
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case inl
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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
this : k (g z') = k (g w')
surj : Set.SurjOn ⇑g ↑S ↑T
c : P
hc' : c ∈ T
eq : ↑⟨c, hc'⟩ * g z' = ↑⟨c, hc'⟩ * g w'
⊢ z = w

Tactic:
obtain ⟨c, hc, rfl⟩ := surj hc'

Goal state after:
case inl
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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
this : k (g z') = k (g w')
surj : Set.SurjOn ⇑g ↑S ↑T
c : M
hc : c ∈ ↑S
hc' : g c ∈ T
eq : ↑⟨g c, hc'⟩ * g z' = ↑⟨g c, hc'⟩ * g w'
⊢ z = w
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
z : N
⊢ f ↑(f.sec z).2 * z = f.toMonoidHom ↑(f.sec z).2 * z

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
z : N
⊢ f ↑(f.sec z).2 * z = f.toMonoidHom ↑(f.sec z).2 * z
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
x : M
y : ↥S
⊢ f ↑y * f x = f.toMonoidHom ↑y * 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
y : ↥S
⊢ f ↑y * f x = f.toMonoidHom ↑y * 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
⊢ (f.ofMulEquivOfLocalizations (MulEquiv.refl N)) 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.ofMulEquivOfLocalizations (MulEquiv.refl N)) x✝ = f x✝
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₁)
⊢ (r₁ /ₒ s₁ * (r₂ /ₒ 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₁)
⊢ (r₁ /ₒ s₁ * (r₂ /ₒ 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
Q : Type u_4
inst✝ : CommMonoid Q
k : N ≃* P
j : P ≃* Q
x✝ : M
⊢ (f.ofMulEquivOfLocalizations (k.trans j)).toMonoidHom x✝ =
    (j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMonoidHom) x✝

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
Q : Type u_4
inst✝ : CommMonoid Q
k : N ≃* P
j : P ≃* Q
x✝ : M
⊢ (f.ofMulEquivOfLocalizations (k.trans j)).toMonoidHom x✝ =
    (j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMonoidHom) x✝