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

Goal state before:
pp: case mk
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
L : List (α × Bool)
⊢ (map g) ((map f) (Quot.mk Red.Step L)) = (map (g ∘ f)) (Quot.mk Red.Step L)

Tactic:
simp [Function.comp_def]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ x ∈ s, p x
⊢ ∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ s, f x

Tactic:
rw [prod_subtype_eq_prod_filter, filter_true_of_mem]

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ x ∈ s, p x
⊢ ∀ x ∈ s, p x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ ∏ i, f i = ∏ i, g i

Tactic:
← prod_subset s.toFinset.subset_univ (by simpa),

Goal state after:
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ ∏ x ∈ s.toFinset, f x = ∏ i, g i
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mp
M : Type u_1
inst✝ : Monoid M
⊢ (∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ) → ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ

Tactic:
intro ⟨S, hS, φ, hφ⟩

Goal state after:
case mp
M : Type u_1
inst✝ : Monoid M
S : Set M
hS : S.Finite
φ : FreeMonoid ↑S →* M
hφ : Function.Surjective ⇑φ
⊢ ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr.refine_1
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ closure ↑S ≤ P

Tactic:
rw [Subgroup.closure_le, ← Subgroup.coe_toSubmonoid, ← hS]

Goal state after:
case mpr.refine_1
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(Submonoid.closure ↑S)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : Monoid M
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
⊢ FG G

Tactic:
cases nonempty_fintype G

Goal state after:
case intro
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
val✝ : Fintype G
⊢ FG G
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mp
G : Type u_3
inst✝ : Group G
⊢ (∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ) → ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ

Tactic:
intro ⟨S, hS, φ, hφ⟩

Goal state after:
case mp
G : Type u_3
inst✝ : Group G
S : Set G
hS : S.Finite
φ : FreeGroup ↑S →* G
hφ : Function.Surjective ⇑φ
⊢ ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂

Tactic:
mul_assoc,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ f a * ((∏ a ∈ s.erase a, f a) * b₁) = (f a * ∏ a ∈ s.erase a, f a) * b₂
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ s.erase a, f a) * b₁ * f a = (f a * ∏ a ∈ s.erase a, f a) * b₂

Tactic:
mul_assoc,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ s.erase a, f a) * (b₁ * f a) = (f a * ∏ a ∈ s.erase a, f a) * b₂
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
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
⊢ r₃ * v * ↑s = r₃ * ↑u * ↑s'

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
⊢ r₃ * (v * ↑s) = r₃ * ↑u * ↑s'
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ r' * ↑u * ↑s₂ = r' * (v * ↑s₁)

Tactic:
mul_assoc,

Goal state after:
case refine_2.refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ r' * (↑u * ↑s₂) = r' * (v * ↑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 y : M
h : f x = f y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ ↑((IsUnit.liftRight (g.domRestrict S) hg) c)⁻¹ * g ↑c * g x = g y

Tactic:
mul_assoc,

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 y : M
h : f x = f y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ ↑((IsUnit.liftRight (g.domRestrict S) hg) c)⁻¹ * (g ↑c * g x) = g 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
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : N
⊢ g (f.sec (x * y)).1 * g ↑(f.sec y).2 * g ↑(f.sec x).2 = g (f.sec y).1 * g ↑(f.sec (x * y)).2 * g (f.sec x).1

Tactic:
← g.map_mul

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 y : N
⊢ g ((f.sec (x * y)).1 * ↑(f.sec y).2) * g ↑(f.sec x).2 = g (f.sec y).1 * g ↑(f.sec (x * y)).2 * g (f.sec x).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 y : N
⊢ g ((f.sec (x * y)).1 * ↑(f.sec y).2) * g ↑(f.sec x).2 = g (f.sec y).1 * g ↑(f.sec (x * y)).2 * g (f.sec x).1

Tactic:
← g.map_mul

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 y : N
⊢ g ((f.sec (x * y)).1 * ↑(f.sec y).2 * ↑(f.sec x).2) = g (f.sec y).1 * g ↑(f.sec (x * y)).2 * g (f.sec x).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 y : N
⊢ g ((f.sec (x * y)).1 * ↑(f.sec y).2 * ↑(f.sec x).2) = g (f.sec y).1 * g ↑(f.sec (x * y)).2 * g (f.sec x).1

Tactic:
← g.map_mul

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 y : N
⊢ g ((f.sec (x * y)).1 * ↑(f.sec y).2 * ↑(f.sec x).2) = g ((f.sec y).1 * ↑(f.sec (x * y)).2) * g (f.sec x).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 y : N
⊢ g ((f.sec (x * y)).1 * ↑(f.sec y).2 * ↑(f.sec x).2) = g ((f.sec y).1 * ↑(f.sec (x * y)).2) * g (f.sec x).1

Tactic:
← g.map_mul

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 y : N
⊢ g ((f.sec (x * y)).1 * ↑(f.sec y).2 * ↑(f.sec x).2) = g ((f.sec y).1 * ↑(f.sec (x * y)).2 * (f.sec x).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 y : N
⊢ g ((f.sec (x * y)).1 * ↑(f.sec y).2 * ↑(f.sec x).2) = g ((f.sec y).1 * ↑(f.sec (x * y)).2 * (f.sec x).1)

Tactic:
← g.map_mul

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 y : N
⊢ g ((f.sec (x * y)).1 * ↑(f.sec y).2 * ↑(f.sec x).2) = g ((f.sec y).1 * ↑(f.sec (x * y)).2 * (f.sec x).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
y : ↥S
⊢ f ↑(f.sec (f.mk' x y)).2 * f.mk' x y * f ↑y = f x * f ↑(f.sec (f.mk' x y)).2

Tactic:
mul_assoc,

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
y : ↥S
⊢ f ↑(f.sec (f.mk' x y)).2 * (f.mk' x y * f ↑y) = f x * f ↑(f.sec (f.mk' x y)).2
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)
z : N
⊢ g (f.sec z).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec z).2)⁻¹ * g ↑(f.sec z).2 = g (f.sec z).1

Tactic:
mul_assoc,

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)
z : N
⊢ g (f.sec z).1 * (↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec z).2)⁻¹ * g ↑(f.sec z).2) = g (f.sec z).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
⊢ g (f.sec (f x)).1 = g ↑(f.sec (f x)).2 * g x

Tactic:
← g.map_mul

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.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₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
⊢ r₃ * v * ↑s₂ = r₃ * (↑u * r₁)

Tactic:
mul_assoc,

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₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
⊢ r₃ * (v * ↑s₂) = r₃ * (↑u * r₁)
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₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
⊢ ↑s₃ * (↑u₀ * r₁) = ↑s₃ * v₀ * ↑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✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
⊢ ↑s₃ * (↑u₀ * r₁) = ↑s₃ * (v₀ * ↑s₂)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}
x✝² x✝¹ : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
x✝ : (r' S) (p, q) (x, y)
t : ↥S
ht : ↑t * (↑y * p) = ↑t * (↑q * x)
⊢ (↑t * ↑y * p, t * y * q) = (↑t * ↑q * x, t * q * y)

Tactic:
mul_assoc,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}
x✝² x✝¹ : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
x✝ : (r' S) (p, q) (x, y)
t : ↥S
ht : ↑t * (↑y * p) = ↑t * (↑q * x)
⊢ (↑t * (↑y * p), t * (y * q)) = (↑t * (↑q * x), t * (q * y))
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
e : u * (↑y.2 * x.1) = u * (↑x.2 * y.1)
⊢ u * ↑x.2 * y.1 = u * ↑y.2 * x.1

Tactic:
mul_assoc,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
e : u * (↑y.2 * x.1) = u * (↑x.2 * y.1)
⊢ u * (↑x.2 * y.1) = u * ↑y.2 * x.1
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
e : u * (↑y.2 * x.1) = u * (↑x.2 * y.1)
⊢ u * (↑x.2 * y.1) = u * ↑y.2 * x.1

Tactic:
mul_assoc,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
e : u * (↑y.2 * x.1) = u * (↑x.2 * y.1)
⊢ u * (↑x.2 * y.1) = u * (↑y.2 * x.1)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * ↑y.2 = v * ↑x.2
⊢ u * y.1 * ↑x.2 = u * (↑x.2 * y.1)

Tactic:
mul_assoc,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * ↑y.2 = v * ↑x.2
⊢ u * (y.1 * ↑x.2) = u * (↑x.2 * y.1)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case h
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)
H : Surjective ⇑(f.lift hg)
v : P
z : N
hz : (f.lift hg) z = v
x : M × ↥S
hx : z * f ↑x.2 = f x.1
⊢ g x.1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) x.2)⁻¹ * g ↑x.2 = g x.1

Tactic:
mul_assoc,

Goal state after:
case h
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)
H : Surjective ⇑(f.lift hg)
v : P
z : N
hz : (f.lift hg) z = v
x : M × ↥S
hx : z * f ↑x.2 = f x.1
⊢ g x.1 * (↑((IsUnit.liftRight (g.domRestrict S) hg) x.2)⁻¹ * g ↑x.2) = g x.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
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₂'
⊢ ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'

Tactic:
mul_assoc,

Goal state after:
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₂'
⊢ ↑s₃' * (r₁' * ↑s') = r₃' * r₂' * r₂ * ↑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.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₂'
⊢ r₃' * ↑s₂' * r = r₃' * r₂' * r₂ * ↑s'

Tactic:
mul_assoc,

Goal state after:
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₂'
⊢ r₃' * (↑s₂' * r) = r₃' * r₂' * r₂ * ↑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.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₂)
⊢ ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S

Tactic:
mul_assoc,

Goal state after:
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₂)
⊢ ↑s₄' * (r₃' * (↑s₂' * ↑s)) ∈ 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.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₁'
⊢ ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂

Tactic:
mul_assoc,

Goal state after:
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₁'
⊢ ↑s₃' * (r₂' * ↑s₂) = r₃' * r₁' * ↑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.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₁'
⊢ r₃' * ↑s₁' * r₁ = r₃' * r₁' * ↑s₂

Tactic:
mul_assoc,

Goal state after:
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₁'
⊢ r₃' * (↑s₁' * r₁) = r₃' * 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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ k ↑(k.sec ((f.map hy k) z)).2 * (f.map hy k) z * k (g ↑(f.sec z).2) =
    k ↑(k.sec ((f.map hy k) z)).2 * k (g (f.sec z).1)

Tactic:
mul_assoc,

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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ k ↑(k.sec ((f.map hy k) z)).2 * ((f.map hy k) z * k (g ↑(f.sec z).2)) =
    k ↑(k.sec ((f.map hy k) z)).2 * k (g (f.sec z).1)
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 : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f x₁ * ↑((IsUnit.liftRight (f.domRestrict S) h) y₁)⁻¹ * f ↑y₂ = f x₂ ↔ f (x₁ * ↑y₂) = f (x₂ * ↑y₁)

Tactic:
mul_assoc,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f x₁ * (↑((IsUnit.liftRight (f.domRestrict S) h) y₁)⁻¹ * f ↑y₂) = f x₂ ↔ f (x₁ * ↑y₂) = f (x₂ * ↑y₁)
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 x * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y)⁻¹ * f ↑y = f x

Tactic:
mul_assoc,

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 x * (↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y)⁻¹ * f ↑y) = f 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
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f (↑y₂ * x₁) = f (↑y₁ * x₂)
⊢ f x₁ = f x₂ * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y₂)⁻¹ * f ↑y₁

Tactic:
mul_assoc,

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₁ x₂ : M
y₁ y₂ : ↥S
H : f (↑y₂ * x₁) = f (↑y₁ * x₂)
⊢ f x₁ = f x₂ * (↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y₂)⁻¹ * f ↑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 * ↑sb * r₂ = rc * rb * ↑s₃

Tactic:
mul_assoc,

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 * (↑sb * r₂) = rc * rb * ↑s₃