mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c : α
h : b ≤ a * c⁻¹
⊢ b * c ≤ a

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c : α
h : b ≤ a * c⁻¹
⊢ b * c ≤ a
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 : a⁻¹ ≤ c⁻¹
ha : a ≠ 0
⊢ b < d

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : a⁻¹ ≤ c⁻¹
ha : a ≠ 0
⊢ b < d
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
x : α
hx : 0 < x
hx' : x < 1
⊢ Units.mk0 x ⋯ ≠ 1

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
x : α
hx : 0 < x
hx' : x < 1
⊢ ¬x = 1
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝¹ → a✝¹ ≤ a✝ → a✝² ≤ a✝

Tactic:
simpa using

Goal state after:
case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝¹ → a✝¹ ≤ a✝ → a✝² ≤ a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
y x : αˣ
h : ↑x < ↑y
hx : 0 < ↑x
z : αˣ
hz : x < z
hz' : z < y
⊢ ↑x < ↑z ∧ ↑z < ↑y

Tactic:
by simp [hz, hz']

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
a✝ : α
⊢ ∃ x, ¬a✝ < x

Tactic:
simpa using

Goal state after:
case coe
α : Type u_1
inst✝ : Preorder α
a✝ : α
⊢ ∃ x, ¬a✝ < x
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝ ≤ a✝¹ → a✝¹ = a✝

Tactic:
simpa using

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝ ≤ a✝¹ → a✝¹ = a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : Nonempty α
inst✝ : NoTopOrder α
a✝ : WithTop α
H : ∀ (a : α), ↑↑a ≤ ↑a✝
⊢ ↑a✝ = ⊤

Tactic:
simpa using

Goal state after:
case coe
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : Nonempty α
inst✝ : NoTopOrder α
a✝ : WithTop α
H : ∀ (a : α), ↑↑a ≤ ↑a✝
⊢ ∀ (b : α), ↑b ≤ a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝ → a✝¹ ≤ a✝ → a✝² ≤ a✝ ∧ a✝¹ ≤ a✝

Tactic:
simpa using

Goal state after:
case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝ → a✝¹ ≤ a✝ → a✝² ≤ a✝ ∧ a✝¹ ≤ a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝¹ → a✝² ≤ a✝ → a✝² ≤ a✝¹ ∧ a✝² ≤ a✝

Tactic:
simpa using

Goal state after:
case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝¹ → a✝² ≤ a✝ → a✝² ≤ a✝¹ ∧ a✝² ≤ a✝
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
n : ℕ
⊢ 0 ≤ ↑n

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
n : ℕ
⊢ 0 ≤ ↑n
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
⊢ 0 ≤ 1

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
⊢ 0 ≤ 1
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝ → a✝¹ ≤ a✝ → a✝² ≤ a✝ ∧ a✝¹ ≤ a✝

Tactic:
simpa using

Goal state after:
case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝ → a✝¹ ≤ a✝ → a✝² ≤ a✝ ∧ a✝¹ ≤ a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝¹ → a✝² ≤ a✝ → a✝² ≤ a✝¹ ∧ a✝² ≤ a✝

Tactic:
simpa using

Goal state after:
case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝¹ → a✝² ≤ a✝ → a✝² ≤ a✝¹ ∧ a✝² ≤ a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ ∨ a✝ ≤ a✝¹

Tactic:
simpa using

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ ∨ a✝ ≤ a✝¹
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
zero_le : ∀ (a : α), 0 ≤ a
this : AddLeftMono (WithZero α)
⊢ ∀ (a b : WithZero α), a ≤ b → ∀ (c : WithZero α), c + a ≤ c + b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
zero_le : ∀ (a : α), 0 ≤ a
this : AddLeftMono (WithZero α)
⊢ ∀ (a b : WithZero α), a ≤ b → ∀ (c : WithZero α), a + c ≤ b + c
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
⊢ a < ↑⌊a⌋₊ + 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
⊢ a < ↑⌊a⌋₊ + 1
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝² a✝¹ a✝ : α
⊢ (a✝² ⊔ a✝¹) ⊓ (a✝² ⊔ a✝) ≤ a✝² ⊔ a✝¹ ⊓ a✝

Tactic:
simpa using

Goal state after:
case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝² a✝¹ a✝ : α
⊢ (a✝² ⊔ a✝¹) ⊓ (a✝² ⊔ a✝) ≤ a✝² ⊔ a✝¹ ⊓ a✝
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Tactic:
by
  obtain ha | ha := le_total a 0
  · rw [floor_of_nonpos ha, floor_of_nonpos (tsub_nonpos_of_le (ha.trans n.cast_nonneg)), zero_tsub]
  rcases le_total a n with h | h
  · rw [floor_of_nonpos (tsub_nonpos_of_le h), eq_comm, tsub_eq_zero_iff_le]
    exact Nat.cast_le.1 ((Nat.floor_le ha).trans h)
  · rw [eq_tsub_iff_add_eq_of_le (le_floor h), ← floor_add_natCast _, tsub_add_cancel_of_le h]
    exact le_tsub_of_add_le_left ((add_zero _).trans_le h)

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ ∨ a✝ ≤ a✝¹

Tactic:
simpa using

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ ∨ a✝ ≤ a✝¹
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
⊢ ⌈a - 1⌉₊ = ⌈a⌉₊ - 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
⊢ ⌈a - 1⌉₊ = ⌈a⌉₊ - 1
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a b : α
hab : a < b
c : α
hc : ↑a < ↑c ∧ ↑c < ↑b
⊢ a < c ∧ c < b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a b : α
hab : a < b
c : α
hc : ↑a < ↑c ∧ ↑c < ↑b
⊢ a < c ∧ c < b
Module: Mathlib.Algebra.Order.Floor.Semiring

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

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ ↑⌊a⌋₊ ≤ a + 1
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case refine_2
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:
simpa using

Goal state after:
case refine_2
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ a ≤ ↑⌊a⌋₊ + 1
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered α
⊢ ∀ (a₁ a₂ : WithBot α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
simpa using

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered α
⊢ ∀ (x x_1 : α), x < x_1 → ∃ x_2, x < x_2 ∧ x_2 < x_1
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ -1 ≤ a - ↑⌈a⌉₊

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ ↑⌈a⌉₊ ≤ a + 1
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
h : a * c = b * c
⊢ a = b

Tactic:
simpa using

Goal state after:
α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
h : a * c = b * c
⊢ a = b
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
h : c * a = c * b
⊢ a = b

Tactic:
simpa using

Goal state after:
α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
h : c * a = c * b
⊢ a = b
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case refine_2
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:
simpa using

Goal state after:
case refine_2
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ a ≤ 1 + ↑⌈a⌉₊
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
a : R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
b : S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
⊢ 0 ≤ a ↔ 0 ≤ b

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
a : R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
b : S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
⊢ 0 ≤ a ↔ 0 ≤ b
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
a b : α
hab : a < b
c : α
hc : ↑a < ↑c ∧ ↑c < ↑b
⊢ a < c ∧ c < b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
a b : α
hab : a < b
c : α
hc : ↑a < ↑c ∧ ↑c < ↑b
⊢ a < c ∧ c < b
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered α
⊢ ∀ (a₁ a₂ : WithTop α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
simpa using

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered α
⊢ ∀ (x x_1 : α), x < x_1 → ∃ x_2, x < x_2 ∧ x_2 < x_1
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
h : -a = a * (⅟a * b + ⅟b * a)
⊢ -1 = ⅟a * b + ⅟b * a

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : Ring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
h : -a = a * (⅟a * b + ⅟b * a)
⊢ -1 = ⅟a * b + ⅟b * a
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: 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
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)

Tactic:
pow_succ' _ n,

Goal state after:
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
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a * (a + b) * (1 / b) = 1 / a + 1 / b

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ * (a + b) * b⁻¹ = a⁻¹ + b⁻¹
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h₁ : a ∣ b
h₂ : a ∣ c
⊢ a ∣ b - c

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h₁ : a ∣ b
h₂ : a ∣ c
⊢ a ∣ b - c
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ c
H : a ∣ b + c
⊢ a ∣ b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ c
H : a ∣ b + c
⊢ a ∣ b
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ c
⊢ a ∣ b - c ↔ a ∣ b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ c
⊢ a ∣ b - c ↔ a ∣ b
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
inst✝ : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ k ≠ 0

Tactic:
simpa using

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
⊢ ¬k = 0
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b : K
h : b ≠ 0
⊢ (b - a) / b = 1 - a / b

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
a b : K
h : b ≠ 0
⊢ (b - a) / b = b / b - a / b
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b : K
h : b ≠ 0
⊢ (a - b) / b = a / b - 1

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
a b : K
h : b ≠ 0
⊢ (a - b) / b = a / b - b / b
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a * (b - a) * (1 / b) = 1 / a - 1 / b

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ * (b - a) * b⁻¹ = a⁻¹ - b⁻¹
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inr
v : ℤ
h : -1 * v = -1
⊢ -1 = 1 ∧ v = -1 ∨ -1 = -1 ∧ v = 1

Tactic:
simpa using

Goal state after:
case inr
v : ℤ
h : -1 * v = -1
⊢ v = 1
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b - c / d = (a * d - b * c) / (b * d)

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b - c / d = (a * d - b * c) / (b * d)
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
a b c : K
hc : c ≠ 0
⊢ b - a / c = (b * c - a) / c

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : Field K
a b c : K
hc : c ≠ 0
⊢ b - a / c = (b * c - a) / c
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
a b c : K
hc : c ≠ 0
⊢ a / c - b = (a - c * b) / c

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : Field K
a b c : K
hc : c ≠ 0
⊢ a / c - b = (a - b * c) / c
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a : α
⊢ |a| ^ 2 = a ^ 2

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a : α
⊢ |a| * |a| = a * a
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
x : α
⊢ |x ^ 2| = x ^ 2

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
x : α
⊢ |x * x| = x * x
Module: Mathlib.Algebra.Order.Ring.Abs

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ |a| ≤ 1 ↔ a * a ≤ 1
Module: Mathlib.Algebra.Order.Ring.Abs

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ a ^ 2 < b ^ 2 ↔ |a| < |b|
Module: Mathlib.Algebra.Order.Ring.Abs

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b|
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:
simpa using

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a ^ 2 ≤ 1 ↔ |a| ≤ 1
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:
simpa using

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a ^ 2 < 1 ↔ |a| < 1
Module: Mathlib.Algebra.Order.Ring.Abs

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ 1 ≤ a ^ 2 ↔ 1 ≤ |a|
Module: Mathlib.Algebra.Order.Ring.Abs

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ 1 < a ^ 2 ↔ 1 < |a|
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n : ℕ
inst✝ : IsOrderedRing α
⊢ |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n

Tactic:
by
  induction n with | zero => simp [geomSum] | succ n ih => ?_
  refine (abs_add_le ..).trans ?_
  rw [abs_mul, abs_pow, Nat.cast_succ, add_one_mul]
  refine add_le_add ?_ (pow_le_pow_left₀ (abs_nonneg _) le_sup_right _)
  rw [pow_succ, ← mul_assoc, mul_comm |a|]
  gcongr
  exacts [abs_nonneg _, (abs_nonneg _).trans ih, le_sup_left]

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
n : ℕ
hb : b ≠ 0
he : Even n
this : a ^ n > -b ^ n
⊢ a ^ n = -b ^ n ↔ a = -b ∧ Odd n

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
n : ℕ
hb : b ≠ 0
he : Even n
this : a ^ n > -b ^ n
⊢ ¬a ^ n = -b ^ n
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
n : ℕ
⊢ a ^ n = -1 ↔ a = -1 ∧ Odd n

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
n : ℕ
⊢ a ^ n = -1 ↔ a = -1 ∧ Odd n
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictMono f
⊢ IsGreatest (f '' s) (f a) ↔ IsGreatest s a

Tactic:
by
  simp [IsGreatest, hf.injective.eq_iff, hf.mem_upperBounds_image]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
⊢ ⇑(prodAssoc α β γ) '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
⊢ ⇑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hg : Monotone g
⊢ BddAbove (range (g ∘ f))

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hg : Monotone g
⊢ BddAbove (g '' range f)
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
⊢ ⇑(prodAssoc α β γ) '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u

Tactic:
by
  simpa only [Equiv.image_eq_preimage_symm] using prod_assoc_symm_preimage

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
x : α
⊢ ¬Acc r x ↔ Nonempty { f // f 0 = x ∧ ∀ (n : ℕ), r (f (n + 1)) (f n) }

Tactic:
nonempty_subtype

Goal state after:
α : Sort u_1
r : α → α → Prop
x : α
⊢ ¬Acc r x ↔ ∃ a, a 0 = x ∧ ∀ (n : ℕ), r (a (n + 1)) (a n)
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 α
a : α
m : a ∈ s
⊢ e.symm ↑⟨e a, ⋯⟩ ∈ s

Tactic:
simpa using

Goal state after:
α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
a : α
m : a ∈ s
⊢ a ∈ s
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)
y : ↑(range f)
m : y ∈ s
⊢ ⟨f ↑⟨rangeSplitting f y, ⋯⟩, ⋯⟩ ∈ s

Tactic:
simpa using

Goal state after:
α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set ↑(range f)
y : ↑(range f)
m : y ∈ s
⊢ y ∈ s
Module: Mathlib.Algebra.Order.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : Invertible a
⊢ ⅟a < 0 ↔ a < 0

Tactic:
simp only [← not_le, invOf_nonneg]

Goal state after: