mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: case refine_2
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
e : Xᵒᵈ ≃o Y := { toEquiv := ofDual.trans ↑f, map_rel_iff' := ?refine_1 }
⊢ DenselyOrdered Xᵒᵈ ↔ DenselyOrdered Y

pp: case refine_1
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
⊢ ∀ {a b : Xᵒᵈ}, (ofDual.trans ↑f) a ≤ (ofDual.trans ↑f) b ↔ a ≤ b

Tactic:
·

Goal state after:
case refine_2
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
e : Xᵒᵈ ≃o Y := { toEquiv := ofDual.trans ↑f, map_rel_iff' := ?refine_1 }
⊢ DenselyOrdered Xᵒᵈ ↔ DenselyOrdered Y
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: case refine_1
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
⊢ ∀ {a b : Xᵒᵈ}, (ofDual.trans ↑f) a ≤ (ofDual.trans ↑f) b ↔ a ≤ b

Tactic:
·

Goal state after:
case refine_1
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
⊢ ∀ {a b : Xᵒᵈ}, (ofDual.trans ↑f) a ≤ (ofDual.trans ↑f) b ↔ a ≤ b
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: case left
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y

pp: case right
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z

Tactic:
·

Goal state after:
case left
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: case right
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z

Tactic:
·

Goal state after:
case right
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ |a ^ n|ₘ = |a|ₘ ^ n

pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : 1 ≤ a
⊢ |a ^ n|ₘ = |a|ₘ ^ n

Tactic:
·

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ |a ^ n|ₘ = |a|ₘ ^ n
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : 1 ≤ a
⊢ |a ^ n|ₘ = |a|ₘ ^ n

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : 1 ≤ a
⊢ |a ^ n|ₘ = |a|ₘ ^ n
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ n + 1 ≠ 0

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

pp: case inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

pp: case inr.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

pp: case inr.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
·

Goal state after:
case inl.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

pp: case inr.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

pp: case inr.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
·

Goal state after:
case inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inr.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

pp: case inr.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
·

Goal state after:
case inr.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inr.inl.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : a * b ≤ 1
⊢ b ≤ 1

pp: case inr.inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : 1 < a * b
⊢ b ≤ 1

Tactic:
·

Goal state after:
case inr.inl.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : a * b ≤ 1
⊢ b ≤ 1
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inr.inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : 1 < a * b
⊢ b ≤ 1

Tactic:
·

Goal state after:
case inr.inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : 1 < a * b
⊢ b ≤ 1
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ab : a ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ab : b ≤ a
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
·

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ab : a ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ab : b ≤ a
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ab : b ≤ a
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a * b ≤ |a|ₘ * |b|ₘ

pp: case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a * b)⁻¹ ≤ |a|ₘ * |b|ₘ

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a * b ≤ |a|ₘ * |b|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a * b)⁻¹ ≤ |a|ₘ * |b|ₘ

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a * b)⁻¹ ≤ |a|ₘ * |b|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case left
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ |a|ₘ / |b|ₘ ≤ |a / b|ₘ

pp: case right
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (|a|ₘ / |b|ₘ)⁻¹ ≤ |a / b|ₘ

Tactic:
·

Goal state after:
case left
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ |a|ₘ / |b|ₘ ≤ |a / b|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case right
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (|a|ₘ / |b|ₘ)⁻¹ ≤ |a / b|ₘ

Tactic:
·

Goal state after:
case right
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (|a|ₘ / |b|ₘ)⁻¹ ≤ |a / b|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ b = b / a * a

Tactic:
·

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ b = b / a * a
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : d ≤ b
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

Tactic:
·

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : d ≤ b
⊢ |b / d|ₘ ≤ max (c / d) (d / a)
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
⊢ |b / d|ₘ ≤ max (c / d) (d / a)
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : a < 1
⊢ 1 < |a|ₘ ↔ a ≠ 1

pp: case inr.inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
⊢ 1 < |1|ₘ ↔ 1 ≠ 1

pp: case inr.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : 1 < a
⊢ 1 < |a|ₘ ↔ a ≠ 1

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : a < 1
⊢ 1 < |a|ₘ ↔ a ≠ 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
⊢ 1 < |1|ₘ ↔ 1 ≠ 1

pp: case inr.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : 1 < a
⊢ 1 < |a|ₘ ↔ a ≠ 1

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
⊢ 1 < |1|ₘ ↔ 1 ≠ 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : 1 < a
⊢ 1 < |a|ₘ ↔ a ≠ 1

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : 1 < a
⊢ 1 < |a|ₘ ↔ a ≠ 1
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case inl
k : ℤ
⊢ ∃ k_1, Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)

Tactic:
·

Goal state after:
case inl
k : ℤ
⊢ ∃ k_1, Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case inr
k : ℤ
⊢ ∃ k_1, Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)

Tactic:
·

Goal state after:
case inr
k : ℤ
⊢ ∃ k_1, Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : 1 ≤ a
⊢ |a|ₘ⁻¹ ≤ a

pp: case inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : a ≤ 1
⊢ |a|ₘ⁻¹ ≤ a

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : 1 ≤ a
⊢ |a|ₘ⁻¹ ≤ a
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : a ≤ 1
⊢ |a|ₘ⁻¹ ≤ a

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : a ≤ 1
⊢ |a|ₘ⁻¹ ≤ a
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case mp
n : ℕ
x : ℤ
h : ↑n = x * x
⊢ IsSquare n

pp: case mpr
n x : ℕ
h : n = x * x
⊢ IsSquare ↑n

Tactic:
·

Goal state after:
case mp
n : ℕ
x : ℤ
h : ↑n = x * x
⊢ IsSquare n
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case mpr
n x : ℕ
h : n = x * x
⊢ IsSquare ↑n

Tactic:
·

Goal state after:
case mpr
n x : ℕ
h : n = x * x
⊢ IsSquare ↑n
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ max a b / min a b = |a / b|ₘ

pp: case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ max a b / min a b = |a / b|ₘ

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ max a b / min a b = |a / b|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ max a b / min a b = |a / b|ₘ

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ max a b / min a b = |a / b|ₘ
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case zero
q n : ℕ
dvd : gcd 0 q ∣ n
le : pred 0 * q.pred ≤ n
⊢ ∃ a b, a * 0 + b * q = n

pp: case succ
q n p : ℕ
dvd : (p + 1).gcd q ∣ n
le : (p + 1).pred * q.pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * q = n

Tactic:
·

Goal state after:
case zero
q n : ℕ
dvd : gcd 0 q ∣ n
le : pred 0 * q.pred ≤ n
⊢ ∃ a b, a * 0 + b * q = n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case refine_1
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ (n.gcdA k % ↑k).toNat < k

pp: case refine_2
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ↑(n * (n.gcdA k % ↑k).toNat % k) = ↑(↑n * n.gcdA k % ↑k).toNat

Tactic:
·

Goal state after:
case refine_1
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ (n.gcdA k % ↑k).toNat < k
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ.zero
n p : ℕ
dvd : (p + 1).gcd 0 ∣ n
le : (p + 1).pred * pred 0 ≤ n
⊢ ∃ a b, a * (p + 1) + b * 0 = n

pp: case succ.succ
n p q : ℕ
dvd : (p + 1).gcd (q + 1) ∣ n
le : (p + 1).pred * (q + 1).pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * (q + 1) = n

Tactic:
·

Goal state after:
case succ.zero
n p : ℕ
dvd : (p + 1).gcd 0 ∣ n
le : (p + 1).pred * pred 0 ≤ n
⊢ ∃ a b, a * (p + 1) + b * 0 = n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: k n r : ℕ
hkn : n.Coprime k
hk : k ≠ 0
⊢ k = 1 ∨ 1 < k

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case inl
n r : ℕ
hkn : n.Coprime 1
hk : 1 ≠ 0
⊢ ∃ m, m < 1 ∧ n * m % 1 = r % 1

pp: case inr
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
⊢ ∃ m, m < k ∧ n * m % k = r % k

Tactic:
·

Goal state after:
case inl
n r : ℕ
hkn : n.Coprime 1
hk : 1 ≠ 0
⊢ ∃ m, m < 1 ∧ n * m % 1 = r % 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ 0 < k

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case mp
a b : ℤ
n : ℕ
⊢ a.gcd b ∣ n → ∃ x y, ↑n = a * x + b * y

pp: case mpr
a b : ℤ
n : ℕ
⊢ (∃ x y, ↑n = a * x + b * y) → a.gcd b ∣ n

Tactic:
·

Goal state after:
case mp
a b : ℤ
n : ℕ
⊢ a.gcd b ∣ n → ∃ x y, ↑n = a * x + b * y
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case mp
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ a ≠ a * c → 1 < c

pp: case mpr
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ 1 < c → a ≠ a * c

Tactic:
·

Goal state after:
case mp
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ a ≠ a * c → 1 < c
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case mpr
a b : ℤ
n : ℕ
⊢ (∃ x y, ↑n = a * x + b * y) → a.gcd b ∣ n

Tactic:
·

Goal state after:
case mpr
a b : ℤ
n : ℕ
⊢ (∃ x y, ↑n = a * x + b * y) → a.gcd b ∣ n
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case mpr
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ 1 < c → a ≠ a * c

Tactic:
·

Goal state after:
case mpr
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ 1 < c → a ≠ a * c
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ ↑q.succ ≠ 0

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case inl
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : a ≤ b
⊢ min a (b * c) = min a (min a b * min a c)

pp: case inr
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
·

Goal state after:
case inl
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : a ≤ b
⊢ min a (b * c) = min a (min a b * min a c)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case left
a b : ℤ
ha : a ≠ 0
⊢ a.gcd b ∈ {n | 0 < n ∧ a.gcd b ∣ n}

pp: case right
a b : ℤ
ha : a ≠ 0
⊢ a.gcd b ∈ lowerBounds {n | 0 < n ∧ a.gcd b ∣ n}

Tactic:
·

Goal state after:
case left
a b : ℤ
ha : a ≠ 0
⊢ a.gcd b ∈ {n | 0 < n ∧ a.gcd b ∣ n}
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case inr
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
·

Goal state after:
case inr
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
⊢ min a (b * c) = min a (min a b * min a c)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case right
a b : ℤ
ha : a ≠ 0
⊢ a.gcd b ∈ lowerBounds {n | 0 < n ∧ a.gcd b ∣ n}

Tactic:
·

Goal state after:
case right
a b : ℤ
ha : a ≠ 0
⊢ a.gcd b ∈ lowerBounds {n | 0 < n ∧ a.gcd b ∣ n}
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case inr.inl
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : a ≤ c
⊢ min a (b * c) = min a (min a b * min a c)

pp: case inr.inr
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : c ≤ a
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
·

Goal state after:
case inr.inl
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : a ≤ c
⊢ min a (b * c) = min a (min a b * min a c)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case left
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ m = 1

pp: case right
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ n = 1

Tactic:
·

Goal state after:
case left
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ m = 1
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case inr.inr
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : c ≤ a
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
·

Goal state after:
case inr.inr
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : c ≤ a
⊢ min a (b * c) = min a (min a b * min a c)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case right
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ n = 1

Tactic:
·

Goal state after:
case right
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ n = 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case zero
M : Type u_1
inst✝ : Monoid M
a : M
n : ℕ
hn : a ^ n = 1
hm : a ^ 0 = 1
⊢ a ^ Nat.gcd 0 n = 1

pp: case succ
M : Type u_1
inst✝ : Monoid M
a : M
n : ℕ
hn : a ^ n = 1
m : ℕ
hm : a ^ (m + 1) = 1
⊢ a ^ (m + 1).gcd n = 1

Tactic:
·

Goal state after:
case zero
M : Type u_1
inst✝ : Monoid M
a : M
n : ℕ
hn : a ^ n = 1
hm : a ^ 0 = 1
⊢ a ^ Nat.gcd 0 n = 1
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
⊢ ↑q.succ ≠ 0

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝ : m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝ : ¬m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝ : m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m