mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
ceil : α → ℤ
gc_ceil_coe : GaloisConnection ceil Int.cast
a : ℤ
z : α
⊢ ↑a ≤ z ↔ -z ≤ -↑a

Tactic:
neg_le_neg_iff

Goal state after:
F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
ceil : α → ℤ
gc_ceil_coe : GaloisConnection ceil Int.cast
a : ℤ
z : α
⊢ ↑a ≤ z ↔ ↑a ≤ z
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
x y : WithZero α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) x y ≤ x

Tactic:
cases x

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y : WithZero α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 y ≤ 0

case coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y : WithZero α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) y ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y : WithTop α
⊢ x ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) x y

Tactic:
cases x

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithTop α
⊢ ⊤ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ y

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithTop α
a✝ : α
⊢ ↑a✝ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) (↑a✝) y
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y : WithTop α
⊢ y ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) x y

Tactic:
cases x

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithTop α
⊢ y ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ y

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithTop α
a✝ : α
⊢ y ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) (↑a✝) y
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
x y : WithZero α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) x y ≤ y

Tactic:
cases x

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y : WithZero α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 y ≤ y

case coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y : WithZero α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) y ≤ y
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
x y z : WithZero α
⊢ x ≤ y → x ≤ z → x ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

Tactic:
cases x

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y z : WithZero α
⊢ 0 ≤ y → 0 ≤ z → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

case coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y z : WithZero α
a✝ : α
⊢ ↑a✝ ≤ y → ↑a✝ ≤ z → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y z : WithTop α
⊢ x ≤ z → y ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) x y ≤ z

Tactic:
cases x

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y z : WithTop α
⊢ ⊤ ≤ z → y ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ y ≤ z

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y z : WithTop α
a✝ : α
⊢ ↑a✝ ≤ z → y ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) (↑a✝) y ≤ z
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
cases x

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithZero α
⊢ 0 ≤ y ∨ y ≤ 0

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

Goal state before:
pp: x y : WithZero (Multiplicative ℤ)
hx : x ≠ 0
hy : y ≠ 0
z : WithZero (Multiplicative ℤ)
hz : z ≠ 0
hzx : z ≤ x
hzy : z ≤ y
⊢ ∃ k, exp (-↑k) < x ∧ exp (-↑k) < y

Tactic:
obtain ⟨k, hk⟩ := exists_exp_neg_natCast_lt hz

Goal state after:
x y : WithZero (Multiplicative ℤ)
hx : x ≠ 0
hy : y ≠ 0
z : WithZero (Multiplicative ℤ)
hz : z ≠ 0
hzx : z ≤ x
hzy : z ≤ y
k : ℕ
hk : exp (-↑k) < z
⊢ ∃ k, exp (-↑k) < x ∧ exp (-↑k) < y
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
⊢ x ≤ exp x.log

Tactic:
cases x

Goal state after:
case zero
G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
⊢ 0 ≤ exp (log 0)

case coe
G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
a✝ : Multiplicative G
⊢ ↑a✝ ≤ exp (↑a✝).log
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithZero α
a b : α
hx : x = 0 → a ≤ b
⊢ unzeroD a x ≤ b ↔ x ≤ ↑b

Tactic:
cases x

Goal state after:
case zero
α : Type u_1
inst✝ : LE α
a b : α
hx : 0 = 0 → a ≤ b
⊢ unzeroD a 0 ≤ b ↔ 0 ≤ ↑b

case coe
α : Type u_1
inst✝ : LE α
a b a✝ : α
hx : ↑a✝ = 0 → a ≤ b
⊢ unzeroD a ↑a✝ ≤ b ↔ ↑a✝ ≤ ↑b
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithZero α
a b : α
hx : x = 0 → a < b
⊢ unzeroD a x < b ↔ x < ↑b

Tactic:
cases x

Goal state after:
case zero
α : Type u_1
inst✝ : LT α
a b : α
hx : 0 = 0 → a < b
⊢ unzeroD a 0 < b ↔ 0 < ↑b

case coe
α : Type u_1
inst✝ : LT α
a b a✝ : α
hx : ↑a✝ = 0 → a < b
⊢ unzeroD a ↑a✝ < b ↔ ↑a✝ < ↑b
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : WithZero α
b : α
⊢ x ≤ ↑(unzeroD b x)

Tactic:
cases x

Goal state after:
case zero
α : Type u_1
inst✝ : Preorder α
b : α
⊢ 0 ≤ ↑(unzeroD b 0)

case coe
α : Type u_1
inst✝ : Preorder α
b a✝ : α
⊢ ↑a✝ ≤ ↑(unzeroD b ↑a✝)
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
x y z : WithBot α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
y z : WithBot α
⊢ (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ z

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
y z : WithBot α
a✝ : α
⊢ (↑a✝ ⊔ y) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ y ⊓ z
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
x y z : WithTop α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
cases x

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
y z : WithTop α
⊢ (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
y z : WithTop α
a✝ : α
⊢ (↑a✝ ⊔ y) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ y ⊓ z
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
n : ℕ
hn : n ≠ 0
a : R
⊢ ⌊a * ↑n⌋₊ / n = ⌊a⌋₊

Tactic:
rcases le_total a 0 with ha | ha
  · rw [floor_of_nonpos, floor_of_nonpos ha]
    · simp
    apply mul_nonpos_of_nonpos_of_nonneg ha n.cast_nonneg
  refine eq_of_forall_le_iff fun m ↦ ?_
  rw [le_div_iff_mul_le (zero_lt_of_ne_zero hn), le_floor_iff (mul_nonneg ha (cast_nonneg' n)),
    le_floor_iff ha, cast_mul, mul_le_mul_iff_of_pos_right (cast_pos'.mpr (zero_lt_of_ne_zero hn))]

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✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : WithBot α
⊢ x ≤ y ∨ y ≤ x

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithBot α
⊢ ⊥ ≤ y ∨ y ≤ ⊥

case 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
y : WithBot α
a✝ : α
⊢ ↑a✝ ≤ y ∨ y ≤ ↑a✝
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✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : WithTop α
⊢ x ≤ y ∨ y ≤ x

Tactic:
cases x

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithTop α
⊢ ⊤ ≤ y ∨ y ≤ ⊤

case 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
y : WithTop α
a✝ : α
⊢ ↑a✝ ≤ y ∨ y ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
⊢ DenselyOrdered (WithBot α) → DenselyOrdered α

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
⊢ DenselyOrdered α
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
⊢ DenselyOrdered α → DenselyOrdered (WithBot α)

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered α
⊢ DenselyOrdered (WithBot α)
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
⊢ DenselyOrdered (WithTop α) → DenselyOrdered α

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
⊢ DenselyOrdered α
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
⊢ DenselyOrdered α → DenselyOrdered (WithTop α)

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered α
⊢ DenselyOrdered (WithTop α)
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b✝ : α
x✝¹ x✝ : Invertible a
b : α
hba : b * a = 1
hab : a * b = 1
c : α
invOf_mul_self✝ : c * a = 1
hac : a * c = 1
⊢ { invOf := b, invOf_mul_self := hba, mul_invOf_self := hab } =
    { invOf := c, invOf_mul_self := invOf_mul_self✝, mul_invOf_self := hac }

Tactic:
by
    congr
    exact left_inv_eq_right_inv hba hac

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

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

Tactic:
← mul_left_inj_of_invertible (c := c),

Goal state after:
α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ a * ⅟c * c = b * c ↔ a = b * c
Module: Mathlib.Order.Directed

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.univ.pi d
b : (i : ι) → α i
hb : b ∈ Set.univ.pi d
f : (i : ι) → α i
hfd : ∀ (i : ι), f i ∈ d i
haf : ∀ (i : ι), r i (a i) (f i)
hbf : ∀ (i : ι), r i (b i) (f i)
⊢ ∃ z ∈ Set.univ.pi d, (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧ (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) b z

Tactic:
exact ⟨f, fun i _ => hfd i, haf, hbf⟩

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✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
x y : WithBot α
⊢ x < y ∨ x = y ∨ y < x

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
y : WithBot α
⊢ ⊥ < y ∨ ⊥ = y ∨ y < ⊥

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
y : WithBot α
a✝ : α
⊢ ↑a✝ < y ∨ ↑a✝ = y ∨ y < ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
x y : WithTop α
⊢ x < y ∨ x = y ∨ y < x

Tactic:
cases x

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
y : WithTop α
⊢ ⊤ < y ∨ ⊤ = y ∨ y < ⊤

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
y : WithTop α
a✝ : α
⊢ ↑a✝ < y ∨ ↑a✝ = y ∨ y < ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
x y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), x < ↑z → y ≤ ↑z) ↔ y ≤ x

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
inst✝² : LinearOrder α
y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ⊥ < ↑z → y ≤ ↑z) ↔ y ≤ ⊥

case coe
α : Type u_1
inst✝² : LinearOrder α
y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑a✝ < ↑z → y ≤ ↑z) ↔ y ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
x y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ↑z < x → ↑z ≤ y) ↔ x ≤ y

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
inst✝² : LinearOrder α
y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ↑z < ⊥ → ↑z ≤ y) ↔ ⊥ ≤ y

case coe
α : Type u_1
inst✝² : LinearOrder α
y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑z < ↑a✝ → ↑z ≤ y) ↔ ↑a✝ ≤ y
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithBot α
y : WithTop αᵒᵈ
⊢ WithBot.toDual x ≤ y ↔ WithTop.ofDual y ≤ x

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
inst✝ : LE α
y : WithTop αᵒᵈ
⊢ WithBot.toDual ⊥ ≤ y ↔ WithTop.ofDual y ≤ ⊥

case coe
α : Type u_1
inst✝ : LE α
y : WithTop αᵒᵈ
a✝ : α
⊢ WithBot.toDual ↑a✝ ≤ y ↔ WithTop.ofDual y ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithTop αᵒᵈ
y : WithBot α
⊢ x ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual x

Tactic:
cases x

Goal state after:
case top
α : Type u_1
inst✝ : LE α
y : WithBot α
⊢ ⊤ ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual ⊤

case coe
α : Type u_1
inst✝ : LE α
y : WithBot α
a✝ : αᵒᵈ
⊢ ↑a✝ ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x y : WithBot α
⊢ WithBot.toDual x ≤ WithBot.toDual y ↔ y ≤ x

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
inst✝ : LE α
y : WithBot α
⊢ WithBot.toDual ⊥ ≤ WithBot.toDual y ↔ y ≤ ⊥

case coe
α : Type u_1
inst✝ : LE α
y : WithBot α
a✝ : α
⊢ WithBot.toDual ↑a✝ ≤ WithBot.toDual y ↔ y ≤ ↑a✝
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
⊢ ⅟a - ⅟b = ⅟a * (b - a) * ⅟b

Tactic:
rw [mul_sub, invOf_mul_self, sub_mul, one_mul, mul_assoc, mul_invOf_self, mul_one]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithBot αᵒᵈ
y : WithTop α
⊢ WithBot.ofDual x ≤ y ↔ WithTop.toDual y ≤ x

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
inst✝ : LE α
y : WithTop α
⊢ WithBot.ofDual ⊥ ≤ y ↔ WithTop.toDual y ≤ ⊥

case coe
α : Type u_1
inst✝ : LE α
y : WithTop α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ ≤ y ↔ WithTop.toDual y ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithTop α
y : WithBot αᵒᵈ
⊢ x ≤ WithBot.ofDual y ↔ y ≤ WithTop.toDual x

Tactic:
cases x

Goal state after:
case top
α : Type u_1
inst✝ : LE α
y : WithBot αᵒᵈ
⊢ ⊤ ≤ WithBot.ofDual y ↔ y ≤ WithTop.toDual ⊤

case coe
α : Type u_1
inst✝ : LE α
y : WithBot αᵒᵈ
a✝ : α
⊢ ↑a✝ ≤ WithBot.ofDual y ↔ y ≤ WithTop.toDual ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x y : WithBot αᵒᵈ
⊢ WithBot.ofDual x ≤ WithBot.ofDual y ↔ y ≤ x

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
inst✝ : LE α
y : WithBot αᵒᵈ
⊢ WithBot.ofDual ⊥ ≤ WithBot.ofDual y ↔ y ≤ ⊥

case coe
α : Type u_1
inst✝ : LE α
y : WithBot αᵒᵈ
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ ≤ WithBot.ofDual y ↔ y ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithBot α
y : WithTop αᵒᵈ
⊢ WithBot.toDual x < y ↔ WithTop.ofDual y < x

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
inst✝ : LT α
y : WithTop αᵒᵈ
⊢ WithBot.toDual ⊥ < y ↔ WithTop.ofDual y < ⊥

case coe
α : Type u_1
inst✝ : LT α
y : WithTop αᵒᵈ
a✝ : α
⊢ WithBot.toDual ↑a✝ < y ↔ WithTop.ofDual y < ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithTop αᵒᵈ
y : WithBot α
⊢ x < WithBot.toDual y ↔ y < WithTop.ofDual x

Tactic:
cases x

Goal state after:
case top
α : Type u_1
inst✝ : LT α
y : WithBot α
⊢ ⊤ < WithBot.toDual y ↔ y < WithTop.ofDual ⊤

case coe
α : Type u_1
inst✝ : LT α
y : WithBot α
a✝ : αᵒᵈ
⊢ ↑a✝ < WithBot.toDual y ↔ y < WithTop.ofDual ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x y : WithBot α
⊢ WithBot.toDual x < WithBot.toDual y ↔ y < x

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
inst✝ : LT α
y : WithBot α
⊢ WithBot.toDual ⊥ < WithBot.toDual y ↔ y < ⊥

case coe
α : Type u_1
inst✝ : LT α
y : WithBot α
a✝ : α
⊢ WithBot.toDual ↑a✝ < WithBot.toDual y ↔ y < ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithBot αᵒᵈ
y : WithTop α
⊢ WithBot.ofDual x < y ↔ WithTop.toDual y < x

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
inst✝ : LT α
y : WithTop α
⊢ WithBot.ofDual ⊥ < y ↔ WithTop.toDual y < ⊥

case coe
α : Type u_1
inst✝ : LT α
y : WithTop α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ < y ↔ WithTop.toDual y < ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithTop α
y : WithBot αᵒᵈ
⊢ x < WithBot.ofDual y ↔ y < WithTop.toDual x

Tactic:
cases x

Goal state after:
case top
α : Type u_1
inst✝ : LT α
y : WithBot αᵒᵈ
⊢ ⊤ < WithBot.ofDual y ↔ y < WithTop.toDual ⊤

case coe
α : Type u_1
inst✝ : LT α
y : WithBot αᵒᵈ
a✝ : α
⊢ ↑a✝ < WithBot.ofDual y ↔ y < WithTop.toDual ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x y : WithBot αᵒᵈ
⊢ WithBot.ofDual x < WithBot.ofDual y ↔ y < x

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
inst✝ : LT α
y : WithBot αᵒᵈ
⊢ WithBot.ofDual ⊥ < WithBot.ofDual y ↔ y < ⊥

case coe
α : Type u_1
inst✝ : LT α
y : WithBot αᵒᵈ
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ < WithBot.ofDual y ↔ y < ↑a✝
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

Tactic:
have hb := h.mp ha

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ

Tactic:
have hb := h.mp ha

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
Module: Mathlib.Algebra.Field.Basic

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

Tactic:
mul_div_cancel_right₀ a two_ne_zero

Goal state after:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : NeZero 2
a : K
⊢ a = a
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: ⊢ -1 * -1 = 1

Tactic:
by decide

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
q : ℚ≥0
a : K
⊢ ↑q * f a = f ↑q * f a

Tactic:
nnratCast

Goal state after:
K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
q : ℚ≥0
a : K
⊢ ↑q * f a = ↑q * f a
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
⊢ MonotoneOn ψ s

Tactic:
by
  rintro x xs y ys l
  rcases le_total (ψ x) (ψ y) with (ψxy | ψyx)
  · exact ψxy
  · have := hφ (ψts ys) (ψts xs) ψyx
    rw [φψs.eq ys, φψs.eq xs] at this
    induction le_antisymm l this
    exact le_refl _

Goal state after:
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:
by
  simpa only [sq_abs] using sq_le_sq₀ (abs_nonneg a) (abs_nonneg b)

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 t' : Set β
⊢ image2 f (s ∩ s') (t ∪ t') ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
rw [image2_union_right]
  nth_grw 1 [inter_subset_left, inter_subset_right]

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

Goal state before:
pp: n : ℕ
hn : Odd n
hm : 2 ∣ n
⊢ ¬Odd 2

Tactic:
by decide

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
wf : WellFounded r
inst✝ : Nonempty α
⊢ ¬Relator.RightTotal r

Tactic:
intro h

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
wf : WellFounded (Function.swap r)
inst✝ : Nonempty α
⊢ ¬Relator.LeftTotal r

Tactic:
intro h

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ t \ s ∪ s ∩ t = t

Tactic:
union_comm,

Goal state after:
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ s ∩ t ∪ t \ s = t
Module: Mathlib.Order.Interval.Set.Basic

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

Tactic:
Ico_eq_empty h

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ {b} ∪ Ico a b = Icc a b

Tactic:
union_comm,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Ico a b ∪ {b} = Icc a b