mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hab : a ≤ b
hbc : b ≤ c
⊢ b⁻¹ ≤ max |a|ₘ |c|ₘ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ |a / c|ₘ = |a / b * (b / c)|ₘ

Tactic:
by

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

Goal state before:
pp: 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
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ |a * b * c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊔ b) / (a ⊓ b) = |b / a|ₘ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
⊢ a = b → |a / b|ₘ ≤ 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |a|ₘ = a ↔ 1 ≤ a

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |a|ₘ = a⁻¹ ↔ a ≤ 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ max a 1 * max a⁻¹ 1 = |a|ₘ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
⊢ |a|.natAbs = a.natAbs

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
⊢ a.sign * |a| = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
⊢ a.sign * a = |a|

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊔ b) ^ 2 = a * b * |b / a|ₘ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
⊢ ↑a.natAbs ≤ a ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: i j : ℤ
⊢ 0 < (i - j).natAbs ↔ i ≠ j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
⊢ |a| < 1 ↔ a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
⊢ |a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: m x : ℤ
h1 : m ∣ x
h2 : |x| < m
⊢ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: m a b : ℕ
ha : a < m
hb : b < m
⊢ |↑b - ↑a| < ↑m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a b : ℤ
H1 : 0 ≤ a
H2✝ : a < |b|
n : ℕ
H2 : a < ↑-[n+1].natAbs
⊢ -(a / -[n+1]) = -0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a b : ℤ
H : b ≠ 0
⊢ a % b < |b|

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
n : ℕ
⊢ |a / ↑n| ≤ |a|

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) ^ 2 = a * b / |b / a|ₘ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / -↑n| ≤ |a|

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: z : ℤ
hz : z ≠ 0
⊢ |z.sign| = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
az : a = 0
⊢ a.sign = a / |a|

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
az : a = 0
⊢ a.sign = |a| / a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ |n| = 1 ↔ a ^ n = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ =
    (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c)))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.NeZero

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 1 ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.NeZero

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
h : NeZero ↑n
⊢ n ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a) * c / ((b ⊓ a) * c) = (b ⊔ a) / (b ⊓ a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a) / (b ⊓ a) = |a / b|ₘ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
h : |a|ₘ = b
⊢ a = b ∨ a = b⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
⊢ a = b ∨ a = b⁻¹ → |a|ₘ = |b|ₘ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
⊢ |a|ₘ = |b|ₘ ↔ a = b ∨ a = b⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
x✝ : Odd n
m : ℤ
hm : n = 2 * m + 1
⊢ n % 2 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Group α
inst✝⁵ : LinearOrder α
β : Type u_2
F : Type u_3
inst✝⁴ : Group β
inst✝³ : LinearOrder β
inst✝² : FunLike F α β
inst✝¹ : OrderHomClass F α β
inst✝ : MonoidHomClass F α β
f : F
a : α
⊢ f |a|ₘ = |f a|ₘ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
h : n % 2 = 1
⊢ n = 2 * (n / 2) + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
⊢ ¬Odd n ↔ n % 2 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: ⊢ ¬Odd 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
⊢ ¬Odd n ↔ Even n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
⊢ ¬Even n ↔ Odd n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
⊢ Even n ∨ Odd n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
⊢ ∃ k, n = 2 * k ∨ n = 2 * k + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
⊢ Xor (Even n) (Odd n)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: m n : ℤ
⊢ Even (m + n) ↔ (Odd m ↔ Odd n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
⊢ ¬Even (2 * n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: m n : ℤ
⊢ Even (m - n) ↔ (Odd m ↔ Odd n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: m n : ℤ
⊢ Odd (m * n) ↔ Odd m ∧ Odd n

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: m : ℤ
n : ℕ
⊢ Odd (m ^ n) ↔ Odd m ∨ n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: m : ℤ
n : ℕ
h : n ≠ 0
⊢ Odd (m ^ n) ↔ Odd m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: m n : ℤ
⊢ Odd (m + n) ↔ (Odd m ↔ Even n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: m n : ℤ
⊢ Odd (m + n) ↔ (Odd n ↔ Even m)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: m n : ℤ
h : Odd (m + n)
⊢ m ≠ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: m n : ℤ
⊢ Odd (m - n) ↔ (Odd m ↔ Even n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: m n : ℤ
⊢ Odd (m - n) ↔ (Odd n ↔ Even m)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
⊢ Even (n * (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
⊢ Even (n * (n - 1))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℕ
⊢ Odd ↑n ↔ Odd n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
⊢ Even n.natAbs ↔ Even n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
ha : a ≤ 1
hab : b ≤ a
⊢ |a|ₘ ≤ |b|ₘ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
⊢ Odd n.natAbs ↔ Odd n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: a b : ℤ
ha : Odd a
hb : Odd b
⊢ 4 ∣ a + b ∨ 4 ∣ a - b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
⊢ Odd n → 2 * (n / 2) + 1 = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a⁻¹ < b ∧ a < b ↔ b⁻¹ < a ∧ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
⊢ Odd n → n / 2 * 2 + 1 = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
⊢ Odd n → 1 + n / 2 * 2 = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
h : Odd n
⊢ 2 * (n / 2) = n - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: z : ℤ
⊢ Even z.sign ↔ z = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: z : ℤ
⊢ Odd z.sign ↔ z ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℕ
⊢ IsSquare ↑n ↔ IsSquare n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: b p : ℕ
w : 0 < b
⊢ ↑(b ^ p - 1) = ↑b ^ p - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: p : ℕ
⊢ 0 < 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Odd n
a : α
⊢ (-a) ^ n = -a ^ n

Tactic:
obtain ⟨k, rfl⟩ := h
  cases k with
  | ofNat k =>
    rw [Int.ofNat_eq_natCast]
    norm_cast
    simp [pow_add]
  | negSucc k =>
    simp_rw [Int.negSucc_eq, show 2 * -(↑k + 1) + (1 : ℤ) = - (1 + k*2) by grind, _root_.zpow_neg]
    norm_cast
    simp [pow_add]

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Odd n
a : α
⊢ (-a) ^ n = -a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Odd n
⊢ (-1) ^ n = -1

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_3
inst✝³ : (i : ι) → Group (α i)
f : (i : ι) → α i
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), MulLeftMono (α i)
inst✝ : ∀ (i : ι), MulRightMono (α i)
h : |f|ₘ = 1
i : ι
⊢ f i = 1 i

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_3
inst✝³ : (i : ι) → Group (α i)
f : (i : ι) → α i
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), MulLeftMono (α i)
inst✝ : ∀ (i : ι), MulRightMono (α i)
h : f = 1
i : ι
⊢ |f|ₘ i = 1 i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
n : ℕ
⊢ ↑n ≤ ↑(n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 0 < ↑n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 0 < ↑n ↔ 0 < n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ 1 < ↑n ↔ 1 < n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ 1 ≤ ↑n ↔ 1 ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑n < 1 ↔ n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑n ≤ 1 ↔ n ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑n ≤ 0 ↔ n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
⊢ 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
F : Type u_4
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : FunLike F R S
n : ℕ
inst✝¹ : NeZero ↑n
inst✝ : RingHomClass F R S
f : F
hf : Function.Injective ⇑f
h : ↑n = 0
⊢ f ↑n = f 0

Tactic:
by

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

Goal state before:
pp: s t : ℤ
r' : ℕ
s' t' : ℤ
⊢ xgcdAux 0 s t r' s' t' = (r', s', t')

Tactic:
by

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

Goal state before:
pp: r : ℕ
s t : ℤ
r' : ℕ
s' t' : ℤ
h : 0 < r
⊢ r.xgcdAux s t r' s' t' = (r' % r).xgcdAux (s' - ↑r' / ↑r * s) (t' - ↑r' / ↑r * t) r s t

Tactic:
by

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

Goal state before:
pp: s : ℕ
⊢ gcdA 0 s = 0

Tactic:
by

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

Goal state before:
pp: s : ℕ
⊢ gcdB 0 s = 1

Tactic:
by

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

Goal state before:
pp: s : ℕ
h : s ≠ 0
⊢ s.gcdA 0 = 1

Tactic:
by

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

Goal state before:
pp: s : ℕ
h : s ≠ 0
⊢ s.gcdB 0 = 0

Tactic:
by

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

Goal state before:
pp: x y : ℕ
⊢ ∀ (n : ℕ) (s t s' t' : ℤ), (xgcdAux 0 s t n s' t').1 = gcd 0 n

Tactic:
by

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

Goal state before:
pp: x✝ y✝ x y : ℕ
h : 0 < x
IH : ∀ (s t s' t' : ℤ), ((y % x).xgcdAux s t x s' t').1 = (y % x).gcd x
s t s' t' : ℤ
⊢ (x.xgcdAux s t y s' t').1 = x.gcd y

Tactic:
by

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

Goal state before:
pp: x y : ℕ
⊢ x.xgcdAux 1 0 y 0 1 = (x.gcd y, x.xgcd y)

Tactic:
by

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

Goal state before:
pp: x y : ℕ
⊢ x.xgcd y = (x.gcdA y, x.gcdB y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ {x | b < x ∧ x < a} = {x | x < a ∧ b < x}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ {x | b < x ∧ x ≤ a} = {x | x ≤ a ∧ b < x}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ {x | b ≤ x ∧ x < a} = {x | x < a ∧ b ≤ x}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ {x | b ≤ x ∧ x ≤ a} = {x | x ≤ a ∧ b ≤ x}

Tactic:
by

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

Goal state before:
pp: ⊢ OrderedSub ℕ

Tactic:
by

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

Goal state before:
pp: x y r r' : ℕ
⊢ ∀ {s t s' t' : ℤ}, x.P y (r, s, t) → x.P y (r', s', t') → x.P y (r.xgcdAux s t r' s' t')

Tactic:
by

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

Goal state before:
pp: x y : ℕ
⊢ x.P y (x, 1, 0)

Tactic:
by

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

Goal state before:
pp: x y : ℕ
⊢ x.P y (y, 0, 1)

Tactic:
by

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

Goal state before:
pp: x y : ℕ
⊢ ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: ⊢ IsCompl {n | Even n} {n | Odd n}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑n.natAbs = ↑|n|

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: m : ℤ
even : Even m
⊢ 0 < 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: m n : ℤ
even : Even (n - m)
⊢ m + 2 ≤ n ↔ m < n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: q n : ℕ
dvd : gcd 0 q ∣ n
le : pred 0 * q.pred ≤ n
b : ℕ
eq : n = q * b
⊢ 0 * 0 + b * q = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: n p : ℕ
dvd : (p + 1).gcd 0 ∣ n
le : (p + 1).pred * pred 0 ≤ n
a : ℕ
eq : n = (p.gcd 0 + 1).gcd 0 * a
⊢ a * (p + 1) + 0 * 0 = n

Tactic:
by

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

Goal state before:
pp: k n : ℕ
hk : n.gcd k < k
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k

Tactic:
by

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

Goal state before:
pp: k n : ℕ
hkn : n.Coprime k
hk : 1 < k
⊢ ∃ m, m < k ∧ n * m % k = 1

Tactic:
by

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

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

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

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

Tactic:
by

Goal state after: