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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap ((swap y z) x) ((swap y z) y) = swap z x

Tactic:
swap_apply_left,

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap ((swap y z) x) z = swap z x
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
⊢ n = n - m + m

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: _n : ℕ
hn : _n ≠ 0
_x _y : ℤ
⊢ ↑_n ≠ 0

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b c : α
⊢ (a - a * b) * c = a * c - a * b * c

Tactic:
sub_mul

Goal state after:
α : Type u
inst✝ : NonAssocRing α
a b c : α
⊢ a * c - a * b * c = a * c - a * b * c
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
⊢ False

Tactic:
have h1 : m < t := Nat.mul_self_lt_mul_self_iff.1 hl

Goal state after:
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
⊢ False
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m : ℕ
⊢ (m + 1) % 2 = 0 ↔ m % 2 = 1

Tactic:
lia

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

Goal state before:
pp: m : ℕ
⊢ (m + 1) % 2 = 1 ↔ m % 2 = 0

Tactic:
lia

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

Goal state before:
pp: n : ℕ
⊢ ¬2 ∣ 2 * n + 1

Tactic:
lia

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

Goal state before:
pp: n : ℕ
⊢ 0 < n → ¬2 ∣ 2 * n - 1

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: i✝ : ℕ
a✝ : IsSquare (-↑i✝).sign ↔ 0 ≤ -↑i✝
⊢ -↑i✝ - 1 < 0

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
⊢ g.comp 0 = 0

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
ha : a = 0
⊢ SemiconjBy a⁻¹ x y ↔ SemiconjBy a y x

Tactic:
by simp only [ha, inv_zero, SemiconjBy.zero_left]

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u) a ↔ ↑u⁻¹ * (a * ↑u) = a

Tactic:
Units.inv_mul_eq_iff_eq_mul,

Goal state after:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u) a ↔ a * ↑u = ↑u * a
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
h : n < m
⊢ m ≠ 0

Tactic:
lia

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ 0 * a ^ 2 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * a ^ 2

Tactic:
zero_mul,

Goal state after:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ 0 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * a ^ 2
Module: Mathlib.Algebra.Ring.Parity

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

Tactic:
lia

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

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

Tactic:
lia

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

Goal state before:
pp: m : ℕ
⊢ m % 2 + (m + 1) % 2 = 1

Tactic:
lia

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

Goal state before:
pp: m : ℕ
⊢ (m + 1) % 2 + m % 2 = 1

Tactic:
lia

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ b < a⁻¹ * c ↔ a * b < c

Tactic:
by
  rw [← mul_lt_mul_iff_left a]
  simp

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
add_le_add_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
toIsOrderedAddMonoid : IsOrderedAddMonoid α := { add_le_add_left := add_le_add_left }
le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
a b c : α
h : a + b ≤ c + a
⊢ b ≤ c

Tactic:
add_comm _ a

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
add_le_add_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
toIsOrderedAddMonoid : IsOrderedAddMonoid α := { add_le_add_left := add_le_add_left }
le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
a b c : α
h : a + b ≤ a + c
⊢ b ≤ c
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ d * b + 0 * a = d * b

Tactic:
zero_mul,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ d * b + 0 = d * b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ d * a = 0 * b + d * a

Tactic:
zero_mul,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ d * a = 0 + d * a
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ d * b + 0 * a = d * b

Tactic:
zero_mul,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ d * b + 0 = d * b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ d * a = 0 * b + d * a

Tactic:
zero_mul,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ d * a = 0 + d * a
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ ↪ β₁
g : β₁ ↪ γ₁
⊢ (ea.embeddingCongr ec) (f.trans g) = ((ea.embeddingCongr eb) f).trans ((eb.embeddingCongr ec) g)

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosMono G₀
n : ℕ
hn : 0 < ↑n
⊢ n ≠ 0

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ a ^ 2 + 0 * b = a ^ 2

Tactic:
zero_mul,

Goal state after:
R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ a ^ 2 + 0 = a ^ 2
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a / c < b / c ↔ a < b

Tactic:
div_lt_iff₀ hc,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < b / c * c ↔ a < b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a / c < b / c ↔ a < b

Tactic:
rw [div_lt_iff₀ hc, div_mul_cancel₀ _ hc.ne']

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b / c < a ↔ b < c * a

Tactic:
div_lt_iff₀ hc,

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b < a * c ↔ b < c * a
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : α ≃o β
⊢ ofRelIsoLT e.toRelIsoLT = e

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : (fun x1 x2 ↦ x1 < x2) ≃r fun x1 x2 ↦ x1 < x2
⊢ (ofRelIsoLT e).toRelIsoLT = e

Tactic:
ext
  simp

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

Goal state after:
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:
rw [mul_inv]

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.Int

Goal state before:
pp: m x : ℤ
h1 : m ∣ x
h2 : ↑x.natAbs < m
h : ¬x = 0
this : m.natAbs ≤ x.natAbs
⊢ False

Tactic:
lia

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

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

Tactic:
lia

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 (max a a⁻¹) = max (f a) (f a)⁻¹

Tactic:
(OrderHomClass.mono f).map_max,

Goal state after:
α : 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 : α
⊢ max (f a) (f a⁻¹) = max (f a) (f a)⁻¹
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 cases n <;> simp [cast_add_one_pos]

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

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

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

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

Goal state after:
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:
· simp only [lowerBounds, and_imp, Set.mem_ofPred_eq]
    exact fun n hn_pos hn => Nat.le_of_dvd hn_pos hn

Goal state after:
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 : ¬0 ≤ b
⊢ b ≤ -1

Tactic:
lia

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

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

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

Tactic:
lia

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

Goal state before:
pp: case hbc
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := ⋯
b : ℤ := ⋯
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ a ≤ ↑q

Tactic:
lia

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

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

Tactic:
lia

Goal state after:
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 * q ≤ 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
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑p * ↑q + ↑q * 1 + (↑q * -1 + 1 * -1) = ↑p * ↑q - 1

Tactic:
lia

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

Goal state before:
pp: case neg.refine_1
α : 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
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ a = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n

Tactic:
refine (pow_one _).symm.trans ?_
    conv_lhs => rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]
    simp only [zpow_add₀ ha, zpow_add₀ hb, ← zpow_natCast, (hab.zpow_zpow₀ _ _).mul_zpow,
      ← zpow_mul, mul_comm (Nat.gcdB m n), mul_comm (Nat.gcdA m n)]
    simp only [zpow_mul, zpow_natCast, h]
    exact ((Commute.pow_pow (by aesop) _ _).zpow_zpow₀ _ _).symm

Goal state after:
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 * q ≤ 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
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑n - 1 < ↑n

Tactic:
lia

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

Goal state before:
pp: case neg.refine_2
α : 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
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ b = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m

Tactic:
refine (pow_one _).symm.trans ?_
    conv_lhs => rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]
    simp only [zpow_add₀ ha, zpow_add₀ hb, ← zpow_natCast, (hab.zpow_zpow₀ _ _).mul_zpow,
      ← zpow_mul, mul_comm (Nat.gcdB m n), mul_comm (Nat.gcdA m n)]
    simp only [zpow_mul, zpow_natCast, h]
    exact ((Commute.pow_pow (by aesop) _ _).zpow_zpow₀ _ _).symm

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Monoid α
n : ℕ
⊢ 0 ^ (n + 1) = 0 ^ n * 0

Tactic:
simp only [mul_zero]; rfl

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hc : AddLECancellable c
h₁ : b ≤ a
h₂ : c ≤ a
⊢ a - b < c ↔ a - c < b

Tactic:
rw [hb.tsub_lt_iff_left h₁, hc.tsub_lt_iff_right h₂]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
d : α
x : WithBot α
⊢ unbotD d x = d ↔ x = ↑d ∨ x = ⊥

Tactic:
simp [unbotD_eq_iff]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
⊢ (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr

Tactic:
by
  ext x
  simp

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
⊢ b < d

Tactic:
have ha : a ≠ 0 := ne_of_gt (lt_of_lt_of_le hc hh)
  rw [← inv_le_inv₀ ha.pos hc] at hh
  simpa [inv_mul_cancel_left₀ ha, inv_mul_cancel_left₀ hc.ne']
    using mul_lt_mul_of_le_of_lt_of_nonneg_of_pos hh h zero_le (inv_pos.2 hc)

Goal state after:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hlt : 0 < n
heq : n = 0
⊢ ¬P n

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hk : P (k + 1)
n : ℕ
hlt : k + 1 < n
hle : n ≤ k + 1
⊢ ¬P n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝² : Add α
inst✝¹ : Add β
inst✝ : Add γ
e₁ : α ≃+ β
e₂ : β ≃+ γ
⊢ (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr

Tactic:
by
  ext x
  simp

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ |a - ↑⌊a⌋₊| ≤ 1

Tactic:
by
  refine abs_le.mpr ⟨?_, ?_⟩
  · simpa using (floor_le ha).trans (le_add_of_nonneg_right zero_le_one)
  · simpa [add_comm] using (lt_floor_add_one a).le

Goal state after:
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : NeZero 2
a : K
⊢ a / 2 + a / 2 = a

Tactic:
rw [← add_div, add_self_div_two]

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: a b c d : ℤ
ha : a = 1 ∨ a = -1
hb : b = 1 ∨ b = -1
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
⊢ (fun x ↦ f x.1 x.2) '' (s ×ˢ t ∪ s' ×ˢ t) = (fun x ↦ f x.1 x.2) '' s ×ˢ t ∪ (fun x ↦ f x.1 x.2) '' s' ×ˢ t

Tactic:
image_union

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a ^ 2 < 1 ↔ |a| < 1

Tactic:
by
  simpa only [one_pow, abs_one] using sq_lt_sq (a := a) (b := 1)

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
wf : WellFounded r
inst✝ : Nonempty α
h : Relator.RightTotal r
a : α
ha : ∀ (x : α), x ∈ Set.univ → ¬r x a
b : α
hba : r b a
⊢ False

Tactic:
specialize ha b (Set.mem_univ b)

Goal state after:
α : Type u_1
r : α → α → Prop
wf : WellFounded r
inst✝ : Nonempty α
h : Relator.RightTotal r
a b : α
ha : ¬r b a
hba : r b a
⊢ False
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
wf : WellFounded (Function.swap r)
inst✝ : Nonempty α
h : Relator.LeftTotal r
a : α
ha : ∀ (x : α), x ∈ Set.univ → ¬Function.swap r x a
b : α
hab : r a b
⊢ False

Tactic:
specialize ha b (Set.mem_univ b)

Goal state after:
α : Type u_1
r : α → α → Prop
wf : WellFounded (Function.swap r)
inst✝ : Nonempty α
h : Relator.LeftTotal r
a b : α
ha : ¬Function.swap r b a
hab : r a b
⊢ False
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
f_inv : Nonempty α → β → α
hf : ∀ (h : Nonempty α), LeftInverse (f_inv h) f
⊢ ofLeftInverse f f_inv hf = ofInjective f ⋯

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
⊢ ofLeftInverse' f f_inv hf = ofInjective f ⋯

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a < b
⊢ Ioo a b = Ioc a b

Tactic:
Ioo_eq_empty h,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a < b
⊢ ∅ = Ioc a b
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : PartialOrder α
a b c : α
⊢ a = c ∧ b = c → Icc a b = {c}

Tactic:
· rintro ⟨rfl, rfl⟩
    exact Icc_self _

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a⁻¹ ≤ 0 ↔ a ≤ 0

Tactic:
grind [inv_lt_zero', le_iff_eq_or_lt]

Goal state after:
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
x : List α
m n : ℕ
⊢ take n (drop m x) ++ drop (m + n) x = drop m x

Tactic:
by rw [← drop_drop, take_append_drop]

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
h : a < b
⊢ a / 2 < b / 2

Tactic:
div_lt_div_iff_of_pos_right (zero_lt_two' α)

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
h : a < b
⊢ a < b
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l.insertIdx n b
⊢ a = b ∨ a ∈ l

Tactic:
cases Nat.lt_or_ge (length l) n with
  | inl hn =>
    rw [insertIdx_of_length_lt hn] at h
    exact .inr h
  | inr hn =>
    rwa [mem_insertIdx hn] at h

Goal state after:
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: α : Type u
β : Type v
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
⊢ n ≤ l.length

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:

Tactic:
2 * a * b
  _ = 2 * a * b * (ε * ε⁻¹) := by rw [mul_inv_cancel₀ hε.ne', mul_one]
  _ = (2 * (ε * a) * b) * ε⁻¹ := by simp_rw [mul_assoc, mul_comm ε, mul_assoc]
  _ ≤ ((ε * a) ^ 2 + b ^ 2) * ε⁻¹ := by gcongr; exact inv_nonneg.mpr hε.le
  _ = ε * a ^ 2 + ε⁻¹ * b ^ 2 := by
    rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
exact Or.inl hab

Goal state after: