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

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

Tactic:
cases y

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

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

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

Tactic:
cases y

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

case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.toDual ⊥ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ ⊥
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
inst✝ : LE α
y : WithBot α
a✝ : α
⊢ WithBot.toDual ↑a✝ ≤ WithBot.toDual y ↔ y ≤ ↑a✝

Tactic:
cases y

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

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

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

Tactic:
cases y

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

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

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

Tactic:
cases y

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

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

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

Tactic:
cases y

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

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

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

Tactic:
cases y

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

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

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

Tactic:
cases y

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

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

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

Tactic:
cases y

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

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

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

Tactic:
cases y

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

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

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

Tactic:
cases y

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

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

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

Tactic:
cases y

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 ⊤
Module: Mathlib.Order.WithBot

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

Tactic:
cases y

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

Tactic:
cases y

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✝ < ⊥
Module: Mathlib.Order.WithBot

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

Tactic:
cases y

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

Tactic:
cases y

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✝ < ⊥
Module: Mathlib.Order.WithBot

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

Tactic:
cases y

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

Tactic:
cases y

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 ⊤
Module: Mathlib.Order.WithBot

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

Tactic:
cases y

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

Tactic:
cases y

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✝ < ⊥
Module: Mathlib.Order.WithBot

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

Tactic:
cases y

Goal state after:
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.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
n : ℕ
⊢ 2 ^ n * (a ^ (n + 1 + 1) + b ^ (n + 1 + 1) + (b ^ (n + 1) * a + a ^ (n + 1) * b)) =
    2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))

Tactic:
add_comm (_ * a)

Goal state after:
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
n : ℕ
⊢ 2 ^ n * (a ^ (n + 1 + 1) + b ^ (n + 1 + 1) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) =
    2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))
Module: Mathlib.Algebra.Group.Int.Units

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

Tactic:
obtain rfl | rfl := isUnit_eq_one_or (IsUnit.mul_iff.mp (Int.isUnit_iff.mpr (Or.inr h))).1

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

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

Goal state before:
pp: u v : ℤ
⊢ u * v = -1 ↔ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1

Tactic:
refine ⟨eq_one_or_neg_one_of_mul_eq_neg_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩ <;>
    obtain ⟨rfl, rfl⟩ := H <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hf : Injective2 f
⊢ f a b ∈ image2 f s t → a ∈ s ∧ b ∈ t

Tactic:
rintro ⟨a', ha', b', hb', h⟩
    rcases hf h with ⟨rfl, rfl⟩
    exact ⟨ha', hb'⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
hf : Injective2 f
⊢ image2 f s (t ∩ t') = image2 f s t ∩ image2 f s t'

Tactic:
simp_rw [← image_uncurry_prod, prod_inter, image_inter hf.uncurry]

Goal state after:
Module: Mathlib.Order.BoundedOrder.Monotone

Goal state before:
pp: α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : Preorder β
inst✝ : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ f a ≤ p

Tactic:
rw [h_bot]

Goal state after:
α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : Preorder β
inst✝ : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ ⊥ ≤ p
Module: Mathlib.Order.Interval.Set.Basic

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

Tactic:
by
  contrapose!; exact nonempty_Icc

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝² : Ring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
⊢ 0 < e

Tactic:
have pos_n : (0 < (n : A)) := Int.cast_pos (n := n) |>.2 (of_decide_eq_true h)

Goal state after:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝² : Ring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
pos_n : 0 < ↑n
⊢ 0 < e
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
hb : 0 < b
⊢ a ≤ 1 / b ↔ b ≤ 1 / a

Tactic:
by
  simpa using le_inv_comm₀ ha hb

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ n)⁻¹ ≤ (a ^ m)⁻¹

Tactic:
by
  convert one_div_pow_le_one_div_pow_of_le a1 mn <;> simp

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

Goal state before:
pp: α : Type u
x y : List α
n : ℕ
⊢ take n x = take n (x ++ y) ↔ y = [] ∨ n ≤ x.length

Tactic:
by
  rw [Eq.comm]; apply take_eq_left_iff

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ zpow' a ↑n = a ^ n

Tactic:
by
  rw [zpow'_of_ne_zero_right]
  · simp
  exact_mod_cast hn

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : Ring M
x₁ x₂ X₁ X₂ Y y a : M
h₁ : x₁ = a * X₁
h₂ : x₂ = a * X₂
H_atom : X₁ - X₂ = Y
hy : a * Y = y
⊢ x₁ - x₂ = y

Tactic:
by
  subst h₁ h₂ H_atom hy
  simp [mul_sub]

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
n : ℕ
l : List α
ha : a ∈ l
⊢ a ∈ take n l ↔ idxOf a l < n

Tactic:
l.take_prefix n |>.mem_iff_idxOf_lt_length

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
n : ℕ
l : List α
ha : a ∈ l
⊢ idxOf a l < (take n l).length ↔ idxOf a l < n
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
h : ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1)
⊢ (map (fun k ↦ f (k + 1) / f k) (range n)).prod⁻¹ = (f n / f 0)⁻¹

Tactic:
prod_inv,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
h : ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1)
⊢ (map (fun x ↦ x⁻¹) (map (fun k ↦ f (k + 1) / f k) (range n))).prod = (f n / f 0)⁻¹
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
this : (fun x ↦ a == x) = fun x ↦ f a == f x
⊢ map f (l.erase a) = (map f l).erase (f a)

Tactic:
rw [erase_eq_eraseP, erase_eq_eraseP, eraseP_map, this]

Goal state after:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
this : (fun x ↦ a == x) = fun x ↦ f a == f x
⊢ map f (eraseP (fun x ↦ f a == f x) l) = map f (eraseP ((fun x ↦ f a == x) ∘ f) l)
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑p.num / ↑p.den = ↑q.num / ↑q.den

Tactic:
div_eq_div_iff

Goal state after:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑p.num * ↑q.den = ↑q.num * ↑p.den

case hb
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑p.den ≠ 0

case hd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑q.den ≠ 0
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q * r = s
⊢ ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
    (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den

Tactic:
rw [h, mul_comm, ← Rat.eq_iff_mul_eq_mul, ← divInt_eq_div]

Goal state after:
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
⊢ ∀ (a b c : PUnit), a ≤ b ⇨ c ↔ min a b ≤ c

Tactic:
by intros; trivial

Goal state after:
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
⊢ ∀ (a : PUnit), a ⇨ ⊥ = aᶜ

Tactic:
by intros; trivial

Goal state after:
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
⊢ ∀ (a b c : PUnit), a \ b ≤ c ↔ a ≤ max b c

Tactic:
by intros; trivial

Goal state after:
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
⊢ ∀ (a : PUnit), ⊤ \ a = ￢a

Tactic:
by intros; trivial

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
s : ι → α
⊢ ⊥ < ⨆ i, s i ↔ ∃ i, ⊥ < s i

Tactic:
by simp [bot_lt_iff_ne_bot]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
s : ι → Set (Set α)
⊢ ⋂₀ ⋃ i, s i = ⋂ i, ⋂₀ s i

Tactic:
by
  simp only [sInter_eq_biInter, biInter_iUnion]

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderTop α
a : α
x y : ↑(Ici a)
⊢ IsCompl x y ↔ ↑x ⊓ ↑y = a ∧ Codisjoint ↑x ↑y

Tactic:
rw [_root_.isCompl_iff, Ici.disjoint_iff, Ici.codisjoint_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
e : α ↪o β
x y : α
⊢ ⇑e ⁻¹' uIcc (e x) (e y) = uIcc x y

Tactic:
by
  cases le_total x y <;> simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
e : α ↪o β
x y : α
⊢ ⇑e ⁻¹' uIoc (e x) (e y) = uIoc x y

Tactic:
by
  cases le_total x y <;> simp [*]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
⊢ CompleteBooleanAlgebra α

Tactic:
by
  let completeLattice := e.completeLattice
  let booleanAlgebra := e.booleanAlgebra
  apply e.injective.completeBooleanAlgebra <;> intros <;> first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ Ι b a) b ↔ x ∈ (fun b ↦ Ι b a) c
ha : b ≤ a
hb : b ≤ c
hc : b < c
⊢ False

Tactic:
simpa [ha, and_iff_right hc, ← @not_le _ _ _ a, iff_not_self, -not_le] using h c

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ Ico (e x) (e y) ∩ range ⇑e = Ico (e x) (e y)

Tactic:
inter_eq_left.2 <| Ico_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ Ico (e x) (e y) = Ico (e x) (e y)
Module: Mathlib.Tactic.NormNum.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
⊢ IsNat |a| na

Tactic:
pa.out,

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
⊢ IsNat |↑na| na
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ ↑r % ↑b' = ↑r

Tactic:
Int.emod_eq_of_lt

Goal state after:
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ ↑r = ↑r

case H1
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ 0 ≤ ↑r

case H2
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ ↑r < ↑b'
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h✝ : (fun x ↦ ↑x) (num✝¹ * ↑db) < (fun x ↦ ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ↑(num✝¹ * ↑db) * ⅟↑db * ⅟↑da < ⅟↑db * ((fun x ↦ ↑x) (num✝ * ↑da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
simp only [Int.cast_mul, Int.cast_natCast, mul_invOf_cancel_right'] at h

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h✝ : (fun x ↦ ↑x) (num✝¹ * ↑db) < (fun x ↦ ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ↑num✝¹ * ⅟↑da < ⅟↑db * ↑num✝
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁻¹ * a ⊔ a ⊔ (a⁻¹ ⊔ 1) = |a|ₘ

Tactic:
inv_mul_cancel,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ⊔ a ⊔ (a⁻¹ ⊔ 1) = |a|ₘ
Module: Mathlib.Data.Int.Cast.Field

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
m n : ℤ
n_dvd : n ∣ m
hn : ↑n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
rcases n_dvd with ⟨k, rfl⟩
  have : n ≠ 0 := by rintro rfl; simp at hn
  rw [Int.mul_ediv_cancel_left _ this, mul_comm n, Int.cast_mul, mul_div_cancel_right₀ _ hn]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial (k + 1)

Tactic:
by
    rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, Nat.mul_left_comm]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(n + 1))⁻¹.num / ↑(↑(n + 1))⁻¹.den = (↑(n + 1))⁻¹

Tactic:
inv_natCast_num,

Goal state after:
case succ
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(n + 1)).sign / ↑(↑(n + 1))⁻¹.den = (↑(n + 1))⁻¹
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ ⌈a + ↑n⌉ = ⌈a⌉ + ↑n

Tactic:
by
  rw [← Int.cast_natCast, ceil_add_intCast]

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
⊢ ⌈0⌉ = 0

Tactic:
by rw [← cast_zero, ceil_intCast]

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

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
⊢ f (x + Int.negSucc n • a) = f x + Int.negSucc n • b

Tactic:
by simp [← sub_eq_add_neg]

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

Goal state before:
pp: case pos
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ ∃ n, y ^ n < x

Tactic:
use 1

Goal state after:
case h
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ y ^ 1 < x
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num
⊢ (q_inv - ↑⌊q_inv⌋).num < q.num

Tactic:
by
    simp only [gt_iff_lt, q_inv]
    field_simp
    simp [q_inv, this]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g : G
p₁ p₂ : P
⊢ g • p₁ = (g * (p₁ /ₛ p₂)) • p₂

Tactic:
mul_smul,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g : G
p₁ p₂ : P
⊢ g • p₁ = g • (p₁ /ₛ p₂) • p₂
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p₃ : P
⊢ ((p₁ /ₛ p₂) * (p₂ /ₛ p₃)) • p₃ = (p₁ /ₛ p₃) • p₃

Tactic:
mul_smul,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₂) • (p₂ /ₛ p₃) • p₃ = (p₁ /ₛ p₃) • p₃