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

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

Tactic:
constructor

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

case mpr
M : Type u_1
inst✝ : Monoid M
⊢ (∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ) → FG M
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG ↔ P.FG

Tactic:
constructor

Goal state after:
case mp
G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG → P.FG

case mpr
G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG → P.FG
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ mk ⁻¹' mk '' s ↔ a ∈ ↑N * s

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ mk ⁻¹' mk '' s → a ∈ ↑N * s

case mpr
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ ↑N * s → a ∈ mk ⁻¹' mk '' s
Module: Mathlib.GroupTheory.Finiteness

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

Tactic:
constructor

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

case mpr
G : Type u_3
inst✝ : Group G
⊢ (∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ) → FG G
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✝³ : Monoid N
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
⊢ ⊤.FG

Tactic:
← Subgroup.top_prod_top

Goal state after:
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✝³ : Monoid N
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
⊢ (⊤.prod ⊤).FG
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✝³ : Monoid N
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
⊢ ⊤.FG

Tactic:
rw [← Subgroup.top_prod_top]
    exact ‹FG G›.out.prod ‹FG G'›.out

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
⊢ x ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x} ↔ x ∈ P

Tactic:
constructor

Goal state after:
case mp
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
⊢ x ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x} → x ∈ P

case mpr
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
⊢ x ∈ P → x ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
I : Finset κ
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
⊢ ∏ s ∈ image f I, g s = ∏ i ∈ I, g (f i)

Tactic:
rw [prod_image']
  exact fun n hnI => (prod_filter_of_pairwise_eq_one hnI hf).symm

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1

Tactic:
h1 _ (H₂.inv_mem hy) _ hz _ (H₁.inv_mem hx),

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * 1⁻¹ * y⁻¹ * x⁻¹ = 1
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ (∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅f g₁, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆) ∧
    ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆

Tactic:
constructor

Goal state after:
case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅f g₁, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆

case right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆ ∧
    map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
constructor

Goal state after:
case a.left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

case a.right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ∈ commutatorSet G

Tactic:
use h, g

Goal state after:
case h
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ ⁅↑h, g⁆ = g
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
p q : G
⊢ ↑p * ↑q = ↑q * ↑p

Tactic:
mul_comm'

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
p q : G
⊢ ↑q * ↑p = ↑q * ↑p
Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
f : M →* G
⊢ (fun f ↦ f.comp of) ((fun f ↦ (monoidOf ⊤).lift ⋯) f) = f

Tactic:
ext

Goal state after:
M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
f : M →* G
x✝ : M
⊢ ((fun f ↦ f.comp of) ((fun f ↦ (monoidOf ⊤).lift ⋯) f)) x✝ = f x✝
Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
f : GrothendieckGroup M →* G
⊢ (fun f ↦ (monoidOf ⊤).lift ⋯) ((fun f ↦ f.comp of) f) = f

Tactic:
ext

Goal state after:
M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
f : GrothendieckGroup M →* G
x✝ : Localization ⊤
⊢ ((fun f ↦ (monoidOf ⊤).lift ⋯) ((fun f ↦ f.comp of) f)) x✝ = f 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 : X
s s' : ↥S
⊢ ↑s' * ↑s ∈ S

Tactic:
norm_cast; apply SetLike.coe_mem

Goal state after:
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₁
hs₂ : ↑u * ↑s₂ = v * ↑s₁
s₁vS : v * ↑s₁ ∈ S
⊢ u * s₂ = ⟨v * ↑s₁, s₁vS⟩

Tactic:
ext

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₁
hs₂ : ↑u * ↑s₂ = v * ↑s₁
s₁vS : v * ↑s₁ ∈ S
⊢ ↑(u * s₂) = ↑⟨v * ↑s₁, s₁vS⟩
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →*o β
h : Monotone (↑↑f).toFun
⊢ { toMonoidHom := ↑f, monotone' := h } = f

Tactic:
ext

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →*o β
h : Monotone (↑↑f).toFun
a✝ : α
⊢ { toMonoidHom := ↑f, monotone' := h } a✝ = f a✝
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)
⊢ (f.lift hg).comp f.toMonoidHom = g

Tactic:
ext

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
⊢ f.lift ⋯ = j

Tactic:
ext

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.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)
j : N →* P
hj : ∀ (x : M), j (f x) = g x
⊢ f.lift hg = j

Tactic:
ext

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)
j : N →* P
hj : ∀ (x : M), j (f x) = g x
x✝ : N
⊢ (f.lift hg) x✝ = j x✝
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case h
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
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ (↑s₄ * ↑s₃) • v₀ • r₂ = (↑s₄ * r₃) • v • r₂ ∧ ↑s₄ * ↑s₃ * (↑u₀ * ↑s₁) = ↑s₄ * r₃ * (↑u * ↑s₁)

Tactic:
constructor

Goal state after:
case h.left
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₀)
⊢ (↑s₄ * ↑s₃) • v₀ • r₂ = (↑s₄ * r₃) • v • r₂

case h.right
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₀)
⊢ ↑s₄ * ↑s₃ * (↑u₀ * ↑s₁) = ↑s₄ * r₃ * (↑u * ↑s₁)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)) ↔ ∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2

Tactic:
constructor

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)) → ∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2

case mpr
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2) → ∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.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)
⊢ Surjective ⇑(f.lift hg) ↔ ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1

Tactic:
constructor

Goal state after:
case mp
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)
⊢ Surjective ⇑(f.lift hg) → ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1

case mpr
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)
⊢ (∀ (v : P), ∃ x, v * g ↑x.2 = g x.1) → Surjective ⇑(f.lift hg)
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
⊢ (fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ }) x✝) =
    x✝

Tactic:
ext

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.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)
⊢ Injective ⇑(f.lift hg) ↔ ∀ (x y : M), f x = f y ↔ g x = g y

Tactic:
constructor

Goal state after:
case mp
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)
⊢ Injective ⇑(f.lift hg) → ∀ (x y : M), f x = f y ↔ g x = g y

case mpr
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), f x = f y ↔ g x = g y) → Injective ⇑(f.lift hg)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mp
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 : Injective ⇑(f.lift hg)
x y : M
⊢ f x = f y ↔ g x = g y

Tactic:
constructor

Goal state after:
case mp.mp
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 : Injective ⇑(f.lift hg)
x y : M
⊢ f x = f y → g x = g y

case mp.mpr
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 : Injective ⇑(f.lift hg)
x y : M
⊢ g x = g y → f x = f y
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:
ext

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:
ext

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.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
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₁' • x /ₒ (s₁' * s) = r₂' • x /ₒ (s₂' * ⟨r₂ * ↑s, hs⟩)

Tactic:
rcases oreCondition (s₂' * r₂) (s₁') with ⟨r₃', s₃', h₃⟩

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
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₁' • x /ₒ (s₁' * s) = r₂' • x /ₒ (s₂' * ⟨r₂ * ↑s, hs⟩)
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
⊢ (k.map hl j).comp (f.map hy k) = f.map ⋯ j

Tactic:
by
  ext z
  change j _ * _ = j (l _) * _
  rw [mul_inv_left, ← mul_assoc, mul_inv_right]
  change j _ * j (l (g _)) = j (l _) * _
  rw [← map_mul j, ← map_mul j, ← l.map_mul, ← l.map_mul]
  refine k.comp_eq_of_eq hl j ?_
  rw [map_mul k, map_mul k, sec_spec', mul_assoc, map_mul_right]

Goal state after:
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:
ext

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: 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
or : Set.SurjOn ⇑g ↑S ↑T ∨ Injective ⇑k
hg : Injective ⇑g
z w : N
hizw : (f.map hy k) z = (f.map hy k) w
⊢ z = w

Tactic:
by
  set i := f.map hy k
  have ifkg (a : M) : i (f a) = k (g a) := f.map_eq hy a
  have ⟨z', w', x, hxz, hxw⟩ := surj₂ f z w
  have : k (g z') = k (g w') := by rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]
  obtain surj | inj := or
  · have ⟨⟨c, hc'⟩, eq⟩ := k.exists_of_eq this
    obtain ⟨c, hc, rfl⟩ := surj hc'
    simp_rw [← map_mul, hg.eq_iff] at eq
    rw [← (f.map_units x).mul_left_inj, hxz, hxw, f.eq_iff_exists]
    exact ⟨⟨c, hc⟩, eq⟩
  · apply (f.map_units x).mul_right_cancel
    rw [hxz, hxw, hg (inj this)]

Goal state after:
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
⊢ f.ofMulEquivOfLocalizations (MulEquiv.refl N) = f

Tactic:
ext

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.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
⊢ (f.ofMulEquivOfLocalizations (k.trans j)).toMonoidHom = j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMonoidHom

Tactic:
ext

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✝
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.mk' x₁ y₁ = f.mk' x₂ y₂
⊢ f ↑y₂ * f.mk' x₂ y₂ * f ↑y₁ = f ↑y₁ * f x₂

Tactic:
mk'_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
x₁ x₂ : M
y₁ y₂ : ↥S
H : f.mk' x₁ y₁ = f.mk' x₂ y₂
⊢ f x₂ * f ↑y₁ = f ↑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
⊢ f.ofMulEquivOfDom ⋯ = f

Tactic:
ext

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✝