mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.bot
α : Type u_1
inst✝ : LT α
⊢ ⊤ < WithBot.toDual ⊥ ↔ ⊥ < WithTop.ofDual ⊤

pp: case top.coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ⊤ < WithBot.toDual ↑a✝ ↔ ↑a✝ < WithTop.ofDual ⊤

pp: case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ ↑a✝ < WithBot.toDual ⊥ ↔ ⊥ < WithTop.ofDual ↑a✝

pp: case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ : αᵒᵈ
a✝ : α
⊢ ↑a✝¹ < WithBot.toDual ↑a✝ ↔ ↑a✝ < WithTop.ofDual ↑a✝¹

Tactic:
<;>

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

case top.coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ⊤ < WithBot.toDual ↑a✝ ↔ ↑a✝ < WithTop.ofDual ⊤

case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ ↑a✝ < WithBot.toDual ⊥ ↔ ⊥ < WithTop.ofDual ↑a✝

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

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

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

Tactic:
<;>

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: case bot.bot
α : Type u_1
inst✝ : LT α
⊢ WithBot.toDual ⊥ < WithBot.toDual ⊥ ↔ ⊥ < ⊥

pp: case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ WithBot.toDual ⊥ < WithBot.toDual ↑a✝ ↔ ↑a✝ < ⊥

pp: case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ WithBot.toDual ↑a✝ < WithBot.toDual ⊥ ↔ ⊥ < ↑a✝

pp: case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ a✝ : α
⊢ WithBot.toDual ↑a✝¹ < WithBot.toDual ↑a✝ ↔ ↑a✝ < ↑a✝¹

Tactic:
<;>

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

case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ WithBot.toDual ⊥ < WithBot.toDual ↑a✝ ↔ ↑a✝ < ⊥

case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ WithBot.toDual ↑a✝ < WithBot.toDual ⊥ ↔ ⊥ < ↑a✝

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

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

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

Tactic:
<;>

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: case bot.top
α : Type u_1
inst✝ : LT α
⊢ WithBot.ofDual ⊥ < ⊤ ↔ WithTop.toDual ⊤ < ⊥

pp: case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ WithBot.ofDual ⊥ < ↑a✝ ↔ WithTop.toDual ↑a✝ < ⊥

pp: case coe.top
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ < ⊤ ↔ WithTop.toDual ⊤ < ↑a✝

pp: case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ : αᵒᵈ
a✝ : α
⊢ WithBot.ofDual ↑a✝¹ < ↑a✝ ↔ WithTop.toDual ↑a✝ < ↑a✝¹

Tactic:
<;>

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

case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ WithBot.ofDual ⊥ < ↑a✝ ↔ WithTop.toDual ↑a✝ < ⊥

case coe.top
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ < ⊤ ↔ WithTop.toDual ⊤ < ↑a✝

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

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

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

Tactic:
<;>

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: case top.bot
α : Type u_1
inst✝ : LT α
⊢ ⊤ < WithBot.ofDual ⊥ ↔ ⊥ < WithTop.toDual ⊤

pp: case top.coe
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ ⊤ < WithBot.ofDual ↑a✝ ↔ ↑a✝ < WithTop.toDual ⊤

pp: case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ↑a✝ < WithBot.ofDual ⊥ ↔ ⊥ < WithTop.toDual ↑a✝

pp: case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ : α
a✝ : αᵒᵈ
⊢ ↑a✝¹ < WithBot.ofDual ↑a✝ ↔ ↑a✝ < WithTop.toDual ↑a✝¹

Tactic:
<;>

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

case top.coe
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ ⊤ < WithBot.ofDual ↑a✝ ↔ ↑a✝ < WithTop.toDual ⊤

case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ↑a✝ < WithBot.ofDual ⊥ ↔ ⊥ < WithTop.toDual ↑a✝

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

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

pp: case coe
α : Type u_1
inst✝ : LT α
y : WithBot αᵒᵈ
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ < WithBot.ofDual y ↔ y < ↑a✝

Tactic:
<;>

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.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝ : LT α
⊢ WithBot.ofDual ⊥ < WithBot.ofDual ⊥ ↔ ⊥ < ⊥

pp: case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ⊥ < WithBot.ofDual ↑a✝ ↔ ↑a✝ < ⊥

pp: case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ < WithBot.ofDual ⊥ ↔ ⊥ < ↑a✝

pp: case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝¹ < WithBot.ofDual ↑a✝ ↔ ↑a✝ < ↑a✝¹

Tactic:
<;>

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

case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ⊥ < WithBot.ofDual ↑a✝ ↔ ↑a✝ < ⊥

case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ < WithBot.ofDual ⊥ ↔ ⊥ < ↑a✝

case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝¹ < WithBot.ofDual ↑a✝ ↔ ↑a✝ < ↑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
inst✝ : Invertible (a + b)
h : ⅟(a + b) = ⅟a + ⅟b
h' : -1 = ⅟a * b + ⅟b * a
h_a_binv_a : -(b + a) = a * ⅟b * a
h_b_ainv_b : -(a + b) = b * ⅟a * b
⊢ a * ⅟b * a = b * ⅟a * b

Tactic:
← h_a_binv_a,

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
h : ⅟(a + b) = ⅟a + ⅟b
h' : -1 = ⅟a * b + ⅟b * a
h_a_binv_a : -(b + a) = a * ⅟b * a
h_b_ainv_b : -(a + b) = b * ⅟a * b
⊢ -(b + a) = b * ⅟a * b
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 + y) * (x ^ n + y ^ n) ≤ (x + y) ^ (n + 1)

Tactic:
rw [pow_succ' _ n]
        gcongr; exact ih (Nat.succ_ne_zero k)

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

Goal state before:
pp: case hab
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ≤ a + b

pp: case hab
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ b ≤ a + b

Tactic:
<;>

Goal state after:
case hab
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ≤ a + b

case hab
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ 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:
by
  simpa only [← sub_eq_add_neg] using h₁.add h₂.neg_right

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

Goal state before:
pp: case inl
v : ℤ
hv : IsUnit v
hu : IsUnit 1
⊢ 1 ≠ v ↔ 1 = -v

pp: case inr
v : ℤ
hv : IsUnit v
hu : IsUnit (-1)
⊢ -1 ≠ v ↔ -1 = -v

Tactic:
<;>

Goal state after:
case inl
v : ℤ
hv : IsUnit v
hu : IsUnit 1
⊢ 1 ≠ v ↔ 1 = -v

case inr
v : ℤ
hv : IsUnit v
hu : IsUnit (-1)
⊢ -1 ≠ v ↔ -1 = -v
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inl.inl
hu hv : IsUnit 1
⊢ 1 ≠ 1 ↔ 1 = -1

pp: case inl.inr
hu : IsUnit 1
hv : IsUnit (-1)
⊢ 1 ≠ -1 ↔ 1 = - -1

pp: case inr.inl
hu : IsUnit (-1)
hv : IsUnit 1
⊢ -1 ≠ 1 ↔ -1 = -1

pp: case inr.inr
hu hv : IsUnit (-1)
⊢ -1 ≠ -1 ↔ -1 = - -1

Tactic:
<;>

Goal state after:
case inl.inl
hu hv : IsUnit 1
⊢ 1 ≠ 1 ↔ 1 = -1

case inl.inr
hu : IsUnit 1
hv : IsUnit (-1)
⊢ 1 ≠ -1 ↔ 1 = - -1

case inr.inl
hu : IsUnit (-1)
hv : IsUnit 1
⊢ -1 ≠ 1 ↔ -1 = -1

case inr.inr
hu hv : IsUnit (-1)
⊢ -1 ≠ -1 ↔ -1 = - -1
Module: Mathlib.Algebra.Group.Int.Units

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

pp: case inr
v : ℤ
h : -1 * v = 1
h' : v * -1 = 1
⊢ -1 = 1 ∧ v = 1 ∨ -1 = -1 ∧ v = -1

Tactic:
<;>

Goal state after:
case inl
v : ℤ
h : 1 * v = 1
h' : v * 1 = 1
⊢ 1 = 1 ∧ v = 1 ∨ 1 = -1 ∧ v = -1

case inr
v : ℤ
h : -1 * v = 1
h' : v * -1 = 1
⊢ -1 = 1 ∧ v = 1 ∨ -1 = -1 ∧ v = -1
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inl.inl
h h' : 1 * 1 = 1
⊢ 1 = 1 ∧ 1 = 1 ∨ 1 = -1 ∧ 1 = -1

pp: case inl.inr
h : 1 * -1 = 1
h' : -1 * 1 = 1
⊢ 1 = 1 ∧ -1 = 1 ∨ 1 = -1 ∧ -1 = -1

pp: case inr.inl
h : -1 * 1 = 1
h' : 1 * -1 = 1
⊢ -1 = 1 ∧ 1 = 1 ∨ -1 = -1 ∧ 1 = -1

pp: case inr.inr
h h' : -1 * -1 = 1
⊢ -1 = 1 ∧ -1 = 1 ∨ -1 = -1 ∧ -1 = -1

Tactic:
<;>

Goal state after:
case inl.inl
h h' : 1 * 1 = 1
⊢ 1 = 1 ∧ 1 = 1 ∨ 1 = -1 ∧ 1 = -1

case inl.inr
h : 1 * -1 = 1
h' : -1 * 1 = 1
⊢ 1 = 1 ∧ -1 = 1 ∨ 1 = -1 ∧ -1 = -1

case inr.inl
h : -1 * 1 = 1
h' : 1 * -1 = 1
⊢ -1 = 1 ∧ 1 = 1 ∨ -1 = -1 ∧ 1 = -1

case inr.inr
h h' : -1 * -1 = 1
⊢ -1 = 1 ∧ -1 = 1 ∨ -1 = -1 ∧ -1 = -1
Module: Mathlib.Algebra.Group.Int.Units

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

pp: case refine_2
u v : ℤ
h : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
H : u = -1 ∧ v = -1
⊢ u * v = 1

Tactic:
<;>

Goal state after:
case refine_1
u v : ℤ
h : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
H : u = 1 ∧ v = 1
⊢ u * v = 1

case refine_2
u v : ℤ
h : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
H : u = -1 ∧ v = -1
⊢ u * v = 1
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case refine_1
h : 1 = 1 ∧ 1 = 1 ∨ 1 = -1 ∧ 1 = -1
⊢ 1 * 1 = 1

pp: case refine_2
h : -1 = 1 ∧ -1 = 1 ∨ -1 = -1 ∧ -1 = -1
⊢ -1 * -1 = 1

Tactic:
<;>

Goal state after:
case refine_1
h : 1 = 1 ∧ 1 = 1 ∨ 1 = -1 ∧ 1 = -1
⊢ 1 * 1 = 1

case refine_2
h : -1 = 1 ∧ -1 = 1 ∨ -1 = -1 ∧ -1 = -1
⊢ -1 * -1 = 1
Module: Mathlib.Algebra.Group.Int.Units

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

pp: case refine_2
u v : ℤ
h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
H : u = -1 ∧ v = 1
⊢ u * v = -1

Tactic:
<;>

Goal state after:
case refine_1
u v : ℤ
h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
H : u = 1 ∧ v = -1
⊢ u * v = -1

case refine_2
u v : ℤ
h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
H : u = -1 ∧ v = 1
⊢ u * v = -1
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case refine_1
h : 1 = 1 ∧ -1 = -1 ∨ 1 = -1 ∧ -1 = 1
⊢ 1 * -1 = -1

pp: case refine_2
h : -1 = 1 ∧ 1 = -1 ∨ -1 = -1 ∧ 1 = 1
⊢ -1 * 1 = -1

Tactic:
<;>

Goal state after:
case refine_1
h : 1 = 1 ∧ -1 = -1 ∨ 1 = -1 ∧ -1 = 1
⊢ 1 * -1 = -1

case refine_2
h : -1 = 1 ∧ 1 = -1 ∨ -1 = -1 ∧ 1 = 1
⊢ -1 * 1 = -1
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
⊢ f ↑q = f (↑q.num / ↑q.den)

Tactic:
by rw [nnratCast, NNRat.cast_def, div, natCast, natCast]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Ring α
a : α
h : |a| = a
⊢ Odd |a| ↔ Odd a

pp: case inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Ring α
a : α
h : |a| = -a
⊢ Odd |a| ↔ Odd a

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Ring α
a : α
h : |a| = a
⊢ Odd |a| ↔ Odd a

case inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Ring α
a : α
h : |a| = -a
⊢ Odd |a| ↔ Odd a
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : a ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

pp: case inr
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : 0 ≤ a
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : a ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

case inr
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : 0 ≤ a
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : a ≤ 0
hb : b ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

pp: case inl.inr
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

pp: case inr.inl
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

pp: case inr.inr
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : a ≤ 0
hb : b ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

case inl.inr
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

case inr.inl
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

case inr.inr
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a : ℤˣ
h✝ : a = 1
⊢ |↑↑a| = 1

pp: case inr
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a : ℤˣ
h✝ : a = -1
⊢ |↑↑a| = 1

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a : ℤˣ
h✝ : a = 1
⊢ |↑↑a| = 1

case inr
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a : ℤˣ
h✝ : a = -1
⊢ |↑↑a| = 1
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f t s ∪ image2 f s t ⊆ image2 f s t

Tactic:
image2_comm hf,

Goal state after:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f s t ∪ image2 f s t ⊆ image2 f s t
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a b : α
h : |a| = a
⊢ |a| ∣ b ↔ a ∣ b

pp: case inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a b : α
h : |a| = -a
⊢ |a| ∣ b ↔ a ∣ b

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a b : α
h : |a| = a
⊢ |a| ∣ b ↔ a ∣ b

case inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a b : α
h : |a| = -a
⊢ |a| ∣ b ↔ a ∣ b
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a b : α
h : |b| = b
⊢ a ∣ |b| ↔ a ∣ b

pp: case inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a b : α
h : |b| = -b
⊢ a ∣ |b| ↔ a ∣ b

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a b : α
h : |b| = b
⊢ a ∣ |b| ↔ a ∣ b

case inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a b : α
h : |b| = -b
⊢ a ∣ |b| ↔ a ∣ b
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inl
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
⊢ a ^ 0 = b ^ 0 ↔ 0 = 0 ∨ a = b ∨ a = -b ∧ Even 0

pp: case inr
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
n : ℕ
hn : n ≠ 0
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Tactic:
<;>

Goal state after:
case inl
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
⊢ a ^ 0 = b ^ 0 ↔ 0 = 0 ∨ a = b ∨ a = -b ∧ Even 0

case inr
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
n : ℕ
hn : n ≠ 0
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: case inl
α : Type u_1
a b c : α
inst✝ : Preorder α
h₂ : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) b c
h : a ≤ b
⊢ SymmGen (fun x1 x2 ↦ x1 ≤ x2) a c

pp: case inr
α : Type u_1
a b c : α
inst✝ : Preorder α
h₂ : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) b c
h : b ≤ a
⊢ SymmGen (fun x1 x2 ↦ x1 ≤ x2) a c

Tactic:
· exact (h.trans h₂.le).symmGen

Goal state after:
case inr
α : Type u_1
a b c : α
inst✝ : Preorder α
h₂ : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) b c
h : b ≤ a
⊢ SymmGen (fun x1 x2 ↦ x1 ≤ x2) a c
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: case pos
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x✝ : ↑(s ∪ t)
x : α
h' : x ∈ s ∪ t
h : p x
⊢ (fun o ↦
        match o with
        | Sum.inl x => ⟨↑x, ⋯⟩
        | Sum.inr x => ⟨↑x, ⋯⟩)
      ((fun x ↦ if hp : p ↑x then Sum.inl ⟨↑x, ⋯⟩ else Sum.inr ⟨↑x, ⋯⟩) ⟨x, h'⟩) =
    ⟨x, h'⟩

pp: case neg
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x✝ : ↑(s ∪ t)
x : α
h' : x ∈ s ∪ t
h : ¬p x
⊢ (fun o ↦
        match o with
        | Sum.inl x => ⟨↑x, ⋯⟩
        | Sum.inr x => ⟨↑x, ⋯⟩)
      ((fun x ↦ if hp : p ↑x then Sum.inl ⟨↑x, ⋯⟩ else Sum.inr ⟨↑x, ⋯⟩) ⟨x, h'⟩) =
    ⟨x, h'⟩

Tactic:
<;>

Goal state after:
case pos
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x✝ : ↑(s ∪ t)
x : α
h' : x ∈ s ∪ t
h : p x
⊢ (fun o ↦
        match o with
        | Sum.inl x => ⟨↑x, ⋯⟩
        | Sum.inr x => ⟨↑x, ⋯⟩)
      ((fun x ↦ if hp : p ↑x then Sum.inl ⟨↑x, ⋯⟩ else Sum.inr ⟨↑x, ⋯⟩) ⟨x, h'⟩) =
    ⟨x, h'⟩

case neg
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x✝ : ↑(s ∪ t)
x : α
h' : x ∈ s ∪ t
h : ¬p x
⊢ (fun o ↦
        match o with
        | Sum.inl x => ⟨↑x, ⋯⟩
        | Sum.inr x => ⟨↑x, ⋯⟩)
      ((fun x ↦ if hp : p ↑x then Sum.inl ⟨↑x, ⋯⟩ else Sum.inr ⟨↑x, ⋯⟩) ⟨x, h'⟩) =
    ⟨x, h'⟩
Module: Mathlib.Order.WellFounded

Goal state before:
pp: case inr.inr
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : f c = g a
this : c < a
⊢ f a = g a

Tactic:
IH c this

Goal state after:
case inr.inr
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : g c = g a
this : c < a
⊢ f a = g a
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: case pos
α : Type u_3
β : α → Type u_4
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : p i
⊢ (piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔ (∀ (b : p i), f ⟨i, b⟩ ∈ s i) ∧ ∀ (b : ¬p i), g ⟨i, b⟩ ∈ s i

pp: case neg
α : Type u_3
β : α → Type u_4
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : ¬p i
⊢ (piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔ (∀ (b : p i), f ⟨i, b⟩ ∈ s i) ∧ ∀ (b : ¬p i), g ⟨i, b⟩ ∈ s i

Tactic:
<;>

Goal state after:
case pos
α : Type u_3
β : α → Type u_4
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : p i
⊢ (piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔ (∀ (b : p i), f ⟨i, b⟩ ∈ s i) ∧ ∀ (b : ¬p i), g ⟨i, b⟩ ∈ s i

case neg
α : Type u_3
β : α → Type u_4
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : ¬p i
⊢ (piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔ (∀ (b : p i), f ⟨i, b⟩ ∈ s i) ∧ ∀ (b : ¬p i), g ⟨i, b⟩ ∈ s i
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

pp: case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case refine_2.inl
α : Type u_1
inst✝ : Preorder α
s t : Set α
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hts : IsCofinalFor t s
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨x', hx', hxx'⟩ := hts.union_right hx
      obtain ⟨y', hy', hyy'⟩ := hts.union_right hy
      obtain ⟨z, hz, hx'z, hy'z⟩ := hs x' hx' y' hy'
      exact ⟨z, .inl hz, hxx'.trans hx'z, hyy'.trans hy'z⟩

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

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : IsCofinalFor s t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨x', hx', hxx'⟩ := hst.union_left hx
      obtain ⟨y', hy', hyy'⟩ := hst.union_left hy
      obtain ⟨z, hz, hx'z, hy'z⟩ := ht x' hx' y' hy'
      exact ⟨z, .inr hz, hxx'.trans hx'z, hyy'.trans hy'z⟩

Goal state after: