mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
f : κ → M
g : ι → κ
⊢ ∏ a ∈ s, f (g a) = ∏ b ∈ image g s, f b ^ #({a ∈ s | g a = b})

Tactic:
[

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
f : κ → M
g : ι → κ
⊢ ∏ a ∈ s, f (g a) = ∏ b ∈ image g s, f b ^ #({a ∈ s | g a = b})
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ : G
⊢ f ⁅g₁, g₂⁆ = ⁅f g₁, f g₂⁆

Tactic:
[

Goal state after:
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ : G
⊢ f ⁅g₁, g₂⁆ = ⁅f g₁, f g₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥
h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥
⊢ ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥
h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥
⊢ ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
a : G
h : a ∈ Group.conjugatesOfSet base
⊢ a ∈ base

Tactic:
[

Goal state after:
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
a : G
h : a ∈ Group.conjugatesOfSet base
⊢ a ∈ base
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'
⊢ map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆

Tactic:
[

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ 1 * x = x

Tactic:
[

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ 1 * x = x
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ x * 1 = x

Tactic:
rw [mul_def, one_def, lift_apply_of]
    induction x using FreeAbelianGroup.induction_on with
    | zero => rfl
    | of L => rw [lift_apply_of, mul_one]
    | neg L ih => rw [map_neg, ih]
    | add x1 x2 ih1 ih2 => rw [map_add, ih1, ih2]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 L1 : α
⊢ (lift ⇑f) (of L1 * of L2) = (lift ⇑f) (of L1) * (lift ⇑f) (of L2)

Tactic:
[

Goal state after:
case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 L1 : α
⊢ (lift ⇑f) (of L1 * of L2) = (lift ⇑f) (of L1) * (lift ⇑f) (of L2)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 L1 : α
ih : (lift ⇑f) (of L1 * of L2) = (lift ⇑f) (of L1) * (lift ⇑f) (of L2)
⊢ (lift ⇑f) (-of L1 * of L2) = (lift ⇑f) (-of L1) * (lift ⇑f) (of L2)

Tactic:
[

Goal state after:
case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 L1 : α
ih : (lift ⇑f) (of L1 * of L2) = (lift ⇑f) (of L1) * (lift ⇑f) (of L2)
⊢ (lift ⇑f) (-of L1 * of L2) = (lift ⇑f) (-of L1) * (lift ⇑f) (of L2)
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
⊢ f ((f.sec (x * y)).1 * ↑(f.sec y).2 * ↑(f.sec x).2) = f ((f.sec y).1 * ↑(f.sec (x * y)).2 * (f.sec x).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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : N
⊢ f ((f.sec (x * y)).1 * ↑(f.sec y).2 * ↑(f.sec x).2) = f ((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)).1 * ↑y) = f (x * ↑(f.sec (f.mk' x y)).2)

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
y : ↥S
⊢ f ((f.sec (f.mk' x y)).1 * ↑y) = f (x * ↑(f.sec (f.mk' x y)).2)
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f : α ≃*o β
a b : β
⊢ a ≤ b ↔ f.symm a ≤ f.symm b

Tactic:
by
    rw [← map_le_map_iff f]
    convert! Iff.rfl <;>
    exact f.toEquiv.apply_symm_apply _

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
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.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:
[

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: case refine_1
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ z * f ↑(a.2 * b.2) = f (a.1 * ↑b.2)

Tactic:
[

Goal state after:
case refine_1
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ z * f ↑(a.2 * b.2) = f (a.1 * ↑b.2)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ w * f ↑(a.2 * b.2) = f (↑a.2 * b.1)

Tactic:
[

Goal state after:
case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ w * f ↑(a.2 * b.2) = f (↑a.2 * b.1)
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 : M
hc : c ∈ ↑S
hc' : g c ∈ T
eq : g c * g z' = g c * g w'
⊢ z = w

Tactic:
[

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 * g z' = g c * g w'
⊢ z = w
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
z : N
x : M × ↥S
hx : z * f ↑x.2 = f x.1
v : P
hv : k v = x.1
w : P
hw : k w = ↑x.2
⊢ z * (f.toMonoidHom.comp k.toMonoidHom) w = (f.toMonoidHom.comp k.toMonoidHom) 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)
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
z : N
x : M × ↥S
hx : z * f ↑x.2 = f x.1
v : P
hv : k v = x.1
w : P
hw : k w = ↑x.2
⊢ z * (f.toMonoidHom.comp k.toMonoidHom) w = (f.toMonoidHom.comp k.toMonoidHom) v
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:
rw [← mul_one x]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
⊢ mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
⊢ mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
⊢ Injective ⇑f ↔ ∀ ⦃x : M⦄, x ∈ S → IsRegular x

Tactic:
[

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
⊢ Injective ⇑f ↔ ∀ ⦃x : M⦄, x ∈ S → IsRegular x
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : f m * n₁ * f (↑ms₁.2 * ↑ms₂.2) = f m * n₂ * f (↑ms₁.2 * ↑ms₂.2)
⊢ n₁ * f (↑ms₁.2 * ↑ms₂.2) = n₂ * f (↑ms₁.2 * ↑ms₂.2)

Tactic:
[

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : f m * n₁ * f (↑ms₁.2 * ↑ms₂.2) = f m * n₂ * f (↑ms₁.2 * ↑ms₂.2)
⊢ n₁ * f (↑ms₁.2 * ↑ms₂.2) = n₂ * f (↑ms₁.2 * ↑ms₂.2)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : f m * (f ms₁.1 * f ↑ms₂.2) = f m * (f ms₂.1 * f ↑ms₁.2)
⊢ f ms₁.1 * f ↑ms₂.2 = f ms₂.1 * f ↑ms₁.2

Tactic:
[

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : f m * (f ms₁.1 * f ↑ms₂.2) = f m * (f ms₂.1 * f ↑ms₁.2)
⊢ f ms₁.1 * f ↑ms₂.2 = f ms₂.1 * f ↑ms₁.2
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : ∃ c, ↑c * (m * (ms₁.1 * ↑ms₂.2)) = ↑c * (m * (ms₂.1 * ↑ms₁.2))
⊢ ∃ c, ↑c * (ms₁.1 * ↑ms₂.2) = ↑c * (ms₂.1 * ↑ms₁.2)

Tactic:
[

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : ∃ c, ↑c * (m * (ms₁.1 * ↑ms₂.2)) = ↑c * (m * (ms₂.1 * ↑ms₁.2))
⊢ ∃ c, ↑c * (ms₁.1 * ↑ms₂.2) = ↑c * (ms₂.1 * ↑ms₁.2)
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 α
⊢ a ^ 0 = 1

Tactic:
[

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
⊢ a ^ 0 = 1
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
inst✝ : IsCancelMul M
⊢ IsCancelMul N

Tactic:
[

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
inst✝ : IsCancelMul M
⊢ IsCancelMul N
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 α
⊢ a ^ (n + 1) = a ^ n * a

Tactic:
[

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n✝ n : ℕ
a : WithTop α
⊢ a ^ (n + 1) = a ^ n * a
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : MonoidWithZero α
inst✝² : NoZeroDivisors α
inst✝¹ : Nontrivial α
x : WithTop α
n : ℕ
inst✝ : Preorder α
⊢ x ^ n < ⊤ ↔ x < ⊤ ∨ n = 0

Tactic:
[

Goal state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : MonoidWithZero α
inst✝² : NoZeroDivisors α
inst✝¹ : Nontrivial α
x : WithTop α
n : ℕ
inst✝ : Preorder α
⊢ x ^ n < ⊤ ↔ x < ⊤ ∨ n = 0
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : CommMonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a b : WithTop α
⊢ a * b = b * a

Tactic:
[

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : CommMonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a b : WithTop α
⊢ a * b = b * a
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝⁷ : DecidableEq α
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : OrderBot α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : PosMulStrictMono α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
x✝ : n + 2 ≠ 0
x y : WithTop α
h : x < y
⊢ x ^ (n + 2) < y ^ (n + 2)

Tactic:
[

Goal state after:
α : Type u_1
inst✝⁷ : DecidableEq α
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : OrderBot α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : PosMulStrictMono α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
x✝ : n + 2 ≠ 0
x y : WithTop α
h : x < y
⊢ x ^ (n + 2) < y ^ (n + 2)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ⊥ ≤ b
⊢ ↑x * ⊥ ≤ ↑x * b

Tactic:
[

Goal state after:
case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ⊥ ≤ b
⊢ ↑x * ⊥ ≤ ↑x * b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ⊥ ≤ b
⊢ ⊥ * ↑x ≤ b * ↑x

Tactic:
[

Goal state after:
case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ⊥ ≤ b
⊢ ⊥ * ↑x ≤ b * ↑x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ↑x * ⊥ < ↑x * ↑a✝

Tactic:
[

Goal state after:
case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ↑x * ⊥ < ↑x * ↑a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ⊥ * ↑x < ↑a✝ * ↑x

Tactic:
[

Goal state after:
case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ⊥ * ↑x < ↑a✝ * ↑x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : α
x0 : 0 < ↑x
a✝ : α
h : ↑a✝ * ↑x ≤ ⊥ * ↑x
⊢ ↑a✝ ≤ ⊥

Tactic:
rw [bot_mul x0.ne.symm, ← coe_mul] at h
      exact absurd h (bot_lt_coe _).not_ge

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : ℕ
ih : ∀ (hmn : m ≤ Order.succ^[n] m), P (Order.succ^[n] m) hmn
hmn : m ≤ Order.succ^[n + 1] m
⊢ P (Order.succ^[n + 1] m) hmn

Tactic:
[

Goal state after:
case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : ℕ
ih : ∀ (hmn : m ≤ Order.succ^[n] m), P (Order.succ^[n] m) hmn
hmn : m ≤ Order.succ^[n + 1] m
⊢ P (Order.succ^[n + 1] m) hmn
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a✝ : α
ha : ∃ b, a✝ < b
x✝ : α
⊢ a✝ < x✝ ↔ (if h : (Ioi a✝).Nonempty then ⋯.min (Ioi a✝) h else a✝) ≤ x✝

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a✝ : α
ha : ∃ b, a✝ < b
x✝ : α
⊢ a✝ < x✝ ↔ (if h : (Ioi a✝).Nonempty then ⋯.min (Ioi a✝) h else a✝) ≤ x✝
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
h : IsSuccPrelimit a
⊢ NoMaxOrder ↑(Iio a)

Tactic:
by
  refine ⟨fun ⟨b, hb⟩ ↦ ?_⟩
  obtain ⟨c, hbc, hca⟩ := (not_covBy_iff hb).1 (h b)
  exact ⟨⟨c, hca⟩, hbc⟩

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : ¬b ≤ a
⊢ succ a ≤ succ b

Tactic:
· exact succ_le_of_lt ((h.lt_of_not_ge hba).trans_le <| le_succ b)

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
⊢ ¬IsSuccPrelimit a ↔ a ∈ range succ

Tactic:
[

Goal state after:
α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
⊢ ¬IsSuccPrelimit a ↔ a ∈ range succ
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccPrelimit c → c ≤ b
hc : IsSuccPrelimit (succ c)
this : succ c = c
⊢ succ c ≤ b

Tactic:
this

Goal state after:
α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccPrelimit c → c ≤ b
hc : IsSuccPrelimit c
this : succ c = c
⊢ c ≤ b
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hm : ∀ x ∈ S, x ≤ succ m
hn : n ∈ S
hm' : succ m ∉ S
⊢ ∃ x, IsGreatest S x

Tactic:
[

Goal state after:
case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hm : ∀ x ∈ S, x ≤ succ m
hn : n ∈ S
hm' : succ m ∉ S
⊢ ∃ x, IsGreatest S x
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
⊢ Icc a (succ b) = insert (succ b) (Icc a b)

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
⊢ Icc a (succ b) = insert (succ b) (Icc a b)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a < succ b
⊢ Ioc a (succ b) = insert (succ b) (Ioc a b)

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a < succ b
⊢ Ioc a (succ b) = insert (succ b) (Ioc a b)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a ≤ b
h₂ : ¬IsMax b
⊢ Ico a (succ b) = insert b (Ico a b)

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a ≤ b
h₂ : ¬IsMax b
⊢ Ico a (succ b) = insert b (Ico a b)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a < b
h₂ : ¬IsMax b
⊢ Ioo a (succ b) = insert b (Ioo a b)

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a < b
h₂ : ¬IsMax b
⊢ Ioo a (succ b) = insert b (Ioo a b)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ a < succ b ↔ a = b ∨ a < b

Tactic:
lt_succ_iff_eq_or_lt

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ a = b ∨ a < b ↔ a = b ∨ a < b