mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
n : ℕ
x✝ : 0 ≤ ↑n
⊢ 0 ≤ ↑↑n

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℕ
⊢ -↑n ≤ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
x✝ : { y // y ≠ ⊥ }
⊢ (fun x ↦ ⟨↑x, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨x, h⟩ => x.unbot h)
        x✝) =
    x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b x✝ : α
⊢ (fun x ↦
        match x with
        | ⟨x, h⟩ => x.unbot h)
      ((fun x ↦ ⟨↑x, ⋯⟩) x✝) =
    x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x y : WithBot α
⊢ ((∃ b, x = ⊥ ∧ y = ↑b) ∨ ∃ a b, a < b ∧ x = ↑a ∧ y = ↑b) ↔ (x = ⊥ ∧ ∃ b, y = ↑b) ∨ ∃ a b, a < b ∧ x = ↑a ∧ y = ↑b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
⊢ ⊥ ≤ ⊥ ↔ ⊥ = ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x y : WithBot α
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x.unbot hx ≤ y.unbot hy ↔ x ≤ y

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x y : WithBot α
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x.unbot hx < y.unbot hy ↔ x < y

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ ∀ (x : Additive αᵒᵈ), ⊤ + x = ⊤

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ ∀ (x : (Additive α)ᵒᵈ), ⊤ + x = ⊤

Tactic:
by simp

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

Goal state before:
pp: m✝ n✝ k : ℕ
p q : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
m : ℕ
IH : (y : ℕ) → y.lbp m → (∀ (n : ℕ), n < y → ¬p n) → { n // p n ∧ ∀ (m : ℕ), m < n → ¬p m }
al : ∀ (n : ℕ), n < m → ¬p n
pm : ¬p m
n : ℕ
h : n ≤ m
e : n = m
⊢ ¬p n

Tactic:
rw [e]; exact pm

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
y : αˣ
h : 0 < ↑y
z : αˣ
hz : 1 < z
⊢ 0 < ↑(y * z⁻¹)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝³ : Add α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : AddLeftReflectLE α
h : AddLECancellable ⊥
⊢ ⊥ + ↑(Classical.arbitrary α) ≤ ⊥ + ⊥

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
a : WithZero α
⊢ 0 ≤ a

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoBotOrder α
⊢ x = ⊥ ↔ ∀ (b : α), x ≤ ↑b

Tactic:
refine ⟨by simp +contextual, fun h ↦ (x.eq_bot_iff_forall_ne).2 fun y => ?_⟩

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoBotOrder α
h : ∀ (b : α), x ≤ ↑b
y : α
⊢ ↑y ≠ x
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
y : WithBot α
a b : α
hy : ↑b ≤ y
⊢ ↑b ≠ ⊥

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x✝ : WithZero α
⊢ 0 ≤ x✝

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableLE α
a : α
⊢ ¬↑a ≤ 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableLT α
x✝ : WithZero α
⊢ ¬x✝ < 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
⊢ 0 < ↑a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : WithZero α
hx : x ≠ 0
hy : y ≠ 0
⊢ min x y ≤ x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : WithZero α
hx : x ≠ 0
hy : y ≠ 0
⊢ min x y ≤ y

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Preorder G
a b : G
inst✝ : AddGroup G
x y : WithZero (Multiplicative G)
⊢ ∀ {a b : (WithZero (Multiplicative G))ˣ}, logEquiv a ≤ logEquiv b ↔ a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Set β
⊢ ∀ ⦃x y : β⦄, (r on f) x y → r (f x) (f y)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : DecidableLE α
x✝ : WithBot α
⊢ ⊥ ≤ x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝¹ : LE α
inst✝ : DecidableLE α
a : α
⊢ ¬↑a ≤ ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LT α
inst✝ : DecidableLT α
x✝ : WithBot α
⊢ ¬x✝ < ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝¹ : LT α
inst✝ : DecidableLT α
a : α
⊢ ⊥ < ↑a

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LT α
inst✝ : WellFoundedLT α
⊢ ∀ (y : WithBot α), y < ⊥ → Acc (fun x1 x2 ↦ x1 < x2) y

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝¹ : LT α
inst✝ : WellFoundedLT α
a x✝² : α
x✝¹ : ∀ (y : α), y < x✝² → Acc (fun x1 x2 ↦ x1 < x2) y
ih : ∀ (y : α), y < x✝² → Acc (fun x1 x2 ↦ x1 < x2) ↑y
x✝ : ⊥ < ↑x✝²
⊢ ∀ (y : WithBot α), y < ⊥ → Acc (fun x1 x2 ↦ x1 < x2) y

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a : α
inst✝ : Invertible a
⊢ a * ⅟a = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a : α
inst✝ : Invertible a
⊢ ⅟a * a = 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝¹ : GroupWithZero α
a : α
inst✝ : Invertible a
⊢ a * a⁻¹ = 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝¹ : GroupWithZero α
a : α
inst✝ : Invertible a
⊢ a⁻¹ * a = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝² : LE α
inst✝¹ : NoTopOrder α
inst✝ : Nonempty α
a : α
⊢ ¬↑a ≤ ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝² : LT α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
a : α
⊢ ⊥ < ↑a

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : Mul R
inst✝² : One R
inst✝¹ : HasDistribNeg R
a : R
inst✝ : Invertible a
⊢ -⅟a * -a = 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : Mul R
inst✝² : One R
inst✝¹ : HasDistribNeg R
a : R
inst✝ : Invertible a
⊢ -a * -⅟a = 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
inst✝² : HasDistribNeg R
a : R
inst✝¹ : Invertible a
inst✝ : Invertible (-a)
⊢ -a * -⅟a = 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ 1 = ⅟a * a + ⅟b * a + (⅟a + ⅟b) * b ↔ 1 = ⅟a * a + ⅟b * a + (⅟a * b + ⅟b * b)

Tactic:
add_mul

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ 1 = ⅟a * a + ⅟b * a + (⅟a * b + ⅟b * b) ↔ 1 = ⅟a * a + ⅟b * a + (⅟a * b + ⅟b * b)
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : Monoid M
inst✝³ : GroupWithZero G₀
inst✝² : FunLike F G₀ M₀
inst✝¹ : MonoidWithZeroHomClass F G₀ M₀
inst✝ : Nontrivial M₀
f : F
⊢ f 0 ≠ 1

Tactic:
by simp

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

Goal state before:
pp: case succ
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)

Tactic:
| succ k ih =>

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedRing R
inst✝ : ExistsAddOfLE R
n : ℕ
hn : Even n
a : R
⊢ 0 ≤ a ^ n

Tactic:
obtain ⟨k, rfl⟩ := hn

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedRing R
inst✝ : ExistsAddOfLE R
a : R
k : ℕ
⊢ 0 ≤ a ^ (k + k)
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) ^ 0 ≤ 2 ^ (0 - 1) * (a ^ 0 + b ^ 0)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) ^ 1 ≤ 2 ^ (1 - 1) * (a ^ 1 + b ^ 1)

Tactic:
by simp

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
⊢ (a + b) * c⁻¹ = a * c⁻¹ + b * c⁻¹

Tactic:
add_mul

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
G : Type u_4
inst✝ : LeftCancelSemigroup G
g x✝ : G
⊢ (fun x ↦
        match x with
        | ⟨val, h⟩ => Exists.choose h)
      ((fun a ↦ ⟨g * a, ⋯⟩) x✝) =
    x✝

Tactic:
by simp

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Even n
h₀ : n ≠ 0
⊢ 0 < a ^ n ↔ a ≠ 0

Tactic:
obtain ⟨k, rfl⟩ := hn

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
ha : a < 0
⊢ a ^ n < 0

Tactic:
obtain ⟨k, rfl⟩ := hn

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : ExistsAddOfLE R
ha : a < 0
k : ℕ
⊢ a ^ (2 * k + 1) < 0
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b c : K
⊢ a / c - b / c = (a - b) / c

Tactic:
by
  rw [sub_eq_add_neg, ← neg_div, ← add_div, sub_eq_add_neg]

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

Goal state before:
pp: case inr.inl
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : 0 < b
⊢ (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b

Tactic:
exact (hn.pow_nonpos ha).trans_lt (pow_pos hb _)

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
⊢ a ^ 0 = 1

Tactic:
by simp

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℤ
⊢ a ^ (-n) = (a ^ n)⁻¹

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_3
s : Set α
t : Set β
⊢ ∀ (x : α × β), x ∈ image2 Prod.mk s t ↔ x ∈ s ×ˢ t

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
t : Set β
⊢ ∀ (x : γ), x ∈ image2 f ∅ t ↔ x ∈ ∅

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
⊢ ∀ (x : γ), x ∈ image2 f s ∅ ↔ x ∈ ∅

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a : α
⊢ |a * a| = a * a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
a : α
⊢ 1 ≤ |a| + 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
t : Set β
a : α
x : γ
⊢ x ∈ image2 f {a} t ↔ x ∈ f a '' t

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
b : β
x : γ
⊢ x ∈ image2 f s {b} ↔ x ∈ (fun a ↦ f a b) '' s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
a : α
b : β
⊢ image2 f {a} {b} = {f a b}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
h : a ^ 2 ≤ b ^ 2
hb : 0 ≤ b
⊢ |a| ≤ b

Tactic:
by
  rwa [← abs_of_nonneg hb, ← sq_le_sq]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommRing α
a b : α
n✝ n : ℕ
ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = a ^ (n + 1 + 1) - b ^ (n + 1) * a + (a * b ^ (n + 1) - b * b ^ (n + 1))

Tactic:
← pow_succ',

Goal state after:
case succ
α : Type u_1
inst✝ : CommRing α
a b : α
n✝ n : ℕ
ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = a ^ (n + 1 + 1) - b ^ (n + 1) * a + (a * b ^ (n + 1) - b ^ (n + 1 + 1))
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
s : Set (α × β)
x : ↑s
⊢ (↑x).2 ∈ {y | ((↑x).1, y) ∈ s}

Tactic:
by simp

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

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
x : ↑s
⊢ e ↑x ∈ ⇑e '' s

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
a b : α
⊢ {a, b}.Nonempty

Tactic:
by simp

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

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
x : ↑s
⊢ (fun y ↦ ⟨e.symm ↑y, ⋯⟩) ((fun x ↦ ⟨e ↑x, ⋯⟩) x) = x

Tactic:
by simp

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

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
y : ↑(⇑e '' s)
⊢ (fun x ↦ ⟨e ↑x, ⋯⟩) ((fun y ↦ ⟨e.symm ↑y, ⋯⟩) y) = y

Tactic:
by simp

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
H : Disjoint s t
a : ↑s
⊢ ↑a ∈ s ∪ t

Tactic:
by simp

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
H : Disjoint s t
a : ↑t
⊢ ↑a ∈ s ∪ t

Tactic:
by simp

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
H : ¬a ∈ s
⊢ insert a s = s ∪ {a}

Tactic:
by simp

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

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set ↑(range f)
x : ↑(rangeSplitting f '' s)
⊢ f ↑x ∈ range f

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ ¬a ∈ Iio a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ a ∈ Iic a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ ¬a ∈ Ioo a b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ ¬a ∈ Ioc a b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ a ∈ Ico a b ↔ a < b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ a ∈ Icc a b ↔ a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Bounds.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : β
h : IsLUB (⇑f '' s) x
⊢ ∀ {x y : α}, f y ≤ f x ↔ y ≤ x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Bounds.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : β
h : IsLUB s (f.symm x)
⊢ ∀ {x y : β}, f.symm y ≤ f.symm x ↔ y ≤ x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
⊢ a ∈ Icc a a

Tactic:
by simp

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

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

Tactic:
by
  refine ⟨fun h => ?_, ?_⟩
  · have hab : a ≤ b := nonempty_Icc.1 (h.symm.subst <| singleton_nonempty c)
    exact
      ⟨eq_of_mem_singleton <| h ▸ left_mem_Icc.2 hab,
        eq_of_mem_singleton <| h ▸ right_mem_Icc.2 hab⟩
  · rintro ⟨rfl, rfl⟩
    exact Icc_self _

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ t.Nonempty

Tactic:
obtain h | h := directedOn_or_directedOn_of_union h

Goal state after:
case inl
α : Type u_1
inst✝ : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ t.Nonempty

case inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ t.Nonempty
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x : α
y : ↑(Iic x)
⊢ (fun y ↦ ⟨e.symm ↑y, ⋯⟩) ((fun y ↦ ⟨e ↑y, ⋯⟩) y) = y

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x : α
y : ↑(Iic (e x))
⊢ (fun y ↦ ⟨e ↑y, ⋯⟩) ((fun y ↦ ⟨e.symm ↑y, ⋯⟩) y) = y

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x : α
⊢ ∀ {a b : ↑(Iic x)},
    { toFun := fun y ↦ ⟨e ↑y, ⋯⟩, invFun := fun y ↦ ⟨e.symm ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun y ↦ ⟨e ↑y, ⋯⟩, invFun := fun y ↦ ⟨e.symm ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x : α
y : ↑(Ici x)
⊢ (fun y ↦ ⟨e.symm ↑y, ⋯⟩) ((fun y ↦ ⟨e ↑y, ⋯⟩) y) = y

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x : α
y : ↑(Ici (e x))
⊢ (fun y ↦ ⟨e ↑y, ⋯⟩) ((fun y ↦ ⟨e.symm ↑y, ⋯⟩) y) = y

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x : α
⊢ ∀ {a b : ↑(Ici x)},
    { toFun := fun y ↦ ⟨e ↑y, ⋯⟩, invFun := fun y ↦ ⟨e.symm ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun y ↦ ⟨e ↑y, ⋯⟩, invFun := fun y ↦ ⟨e.symm ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y✝ : α
y : ↑(Icc x y✝)
⊢ (fun z ↦ ⟨e.symm ↑z, ⋯⟩) ((fun z ↦ ⟨e ↑z, ⋯⟩) y) = y

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y✝ : α
y : ↑(Icc (e x) (e y✝))
⊢ (fun z ↦ ⟨e ↑z, ⋯⟩) ((fun z ↦ ⟨e.symm ↑z, ⋯⟩) y) = y

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y : α
⊢ ∀ {a b : ↑(Icc x y)},
    { toFun := fun z ↦ ⟨e ↑z, ⋯⟩, invFun := fun z ↦ ⟨e.symm ↑z, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun z ↦ ⟨e ↑z, ⋯⟩, invFun := fun z ↦ ⟨e.symm ↑z, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : BoundedOrder α
⊢ Icc ⊥ ⊤ = univ

Tactic:
by simp

Goal state after: