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

Goal state before:
pp: α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ ¬f a = f b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
⊢ compare (f a) (f b) = compareOfLessAndEq a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
x : α × β
⊢ x.swap < (b, a) ↔ x < (a, b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
⊢ x < y ↔ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
h₁ : a₁ < a₂
h₂ : b₁ ≤ b₂
⊢ (a₁, b₁) < (a₂, b₂)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
h₁ : a₁ ≤ a₂
h₂ : b₁ < b₂
⊢ (a₁, b₁) < (a₂, b₂)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LT α
inst✝ : DenselyOrdered α
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ a, a < a₂ ∧ a₁ < a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ a i < update a i c i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ update a i c i < b i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b

Tactic:
by

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

Goal state before:
pp: ⊢ ¬true = false

Tactic:
by

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

Goal state before:
pp: ⊢ ¬false = true

Tactic:
by

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

Goal state before:
pp: b : Bool
⊢ (¬b = true) = (b = false)

Tactic:
by

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

Goal state before:
pp: b : Bool
⊢ (¬b = false) = (b = true)

Tactic:
by

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

Goal state before:
pp: a b : Bool
⊢ ((a && b) = true) = (a = true ∧ b = true)

Tactic:
by

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

Goal state before:
pp: a b : Bool
⊢ ((a || b) = true) = (a = true ∨ b = true)

Tactic:
by

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

Goal state before:
pp: a : Bool
⊢ ((!a) = true) = (a = false)

Tactic:
by

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

Goal state before:
pp: a b : Bool
⊢ ((a && b) = false) = (a = false ∨ b = false)

Tactic:
by

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

Goal state before:
pp: a b : Bool
⊢ ((a || b) = false) = (a = false ∧ b = false)

Tactic:
by

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

Goal state before:
pp: a : Bool
⊢ ((!a) = false) = (a = true)

Tactic:
by

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

Goal state before:
pp: ⊢ (false = true) = False

Tactic:
by

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

Goal state before:
pp: ⊢ (true = true) = True

Tactic:
by

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

Goal state before:
pp: p : Prop
d : Decidable p
⊢ decide p = true ↔ p

Tactic:
by

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

Goal state before:
pp: b : Bool
⊢ ¬b = true ↔ b = false

Tactic:
by

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

Goal state before:
pp: a b : Bool
⊢ (a ^^ b) = true ↔ Xor (a = true) (b = true)

Tactic:
by

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

Goal state before:
pp: b : Bool
⊢ b = false ∨ b = true

Tactic:
by

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

Goal state before:
pp: a b : Bool
H : a = true
⊢ (a || b) = true

Tactic:
by

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

Goal state before:
pp: a b : Bool
H : b = true
⊢ (a || b) = true

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {a b : Bool}, (a && b) = true → a = true

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {a b : Bool}, a = true → b = true → (a && b) = true

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Push

Goal state before:
pp: p q : Prop
⊢ ¬p ∧ q ∨ ¬¬p ∧ ¬q ↔ p ∧ ¬q ∨ ¬p ∧ q

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {a b : Bool}, (a && b) = true → b = true

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {a b : Bool}, a = !b ↔ a ≠ b

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {a b : Bool}, (!a) = b ↔ a ≠ b

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (b : Bool), (!b) ≠ b

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (b : Bool), b ≠ !b

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b : Bool), a = b ∨ a = !b

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {b : Bool}, (!b) = true ↔ ¬b = true

Tactic:
by

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

Goal state before:
pp: a : Bool
⊢ (!a) = false → a = true

Tactic:
by

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

Goal state before:
pp: a : Bool
⊢ (!a) = true → a = false

Tactic:
by

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

Goal state before:
pp: ⊢ bne = xor

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {x y : Bool}, (x ^^ y) = true ↔ x ≠ y

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a : Bool), a ≤ a

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b c : Bool), a ≤ b → b ≤ c → a ≤ c

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b : Bool), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b : Bool), a ≤ b → b ≤ a → a = b

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b : Bool), a ≤ b ∨ b ≤ a

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b : Bool), min a b = if a ≤ b then a else b

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b : Bool), max a b = if a ≤ b then b else a

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {x y : Bool}, x < y ↔ x = false ∧ y = true

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {x y : Bool}, x ≤ y ↔ x = true → y = true

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x y : Bool), (x && y) ≤ x

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x y : Bool), (x && y) ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Pairwise

Goal state before:
pp: n : ℕ
R : Fin n.succ → Fin n.succ → Prop
inst✝ : Std.Symm R
⊢ Pairwise R ↔ (∀ (j : Fin n), R 0 j.succ) ∧ Pairwise fun i j ↦ R i.succ j.succ

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {x y z : Bool}, x ≤ y → x ≤ z → x ≤ (y && z)

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x y : Bool), x ≤ (x || y)

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x y : Bool), y ≤ (x || y)

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {x y z : Bool}, x ≤ z → y ≤ z → (x || y) ≤ z

Tactic:
by

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

Goal state before:
pp: b : Bool
⊢ (b.toNat == 0) = !b

Tactic:
by

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

Goal state before:
pp: b : Bool
⊢ (b.toNat != 0) = b

Tactic:
by

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

Goal state before:
pp: b : Bool
⊢ (b.toNat == 1) = b

Tactic:
by

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

Goal state before:
pp: b : Bool
⊢ (b.toNat != 1) = !b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
⊢ x = y ∨ y = z ∨ x = z

Tactic:
by

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

Goal state before:
pp: n m : Nat
h : n ≤ m
⊢ ofNat n ≤ ofNat m

Tactic:
by

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

Goal state before:
pp: b₀ b₁ : Bool
h : b₀ ≤ b₁
⊢ b₀.toNat ≤ b₁.toNat

Tactic:
by

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

Goal state before:
pp: b : Bool
⊢ ofNat b.toNat = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
π : ι → Type u_4
α : Type u_5
inst✝ : Subsingleton α
x✝¹ x✝ : α
⊢ False ↔ True ∧ ¬True

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
f : Bool → α
H : f false ≠ f true
x y : Bool
⊢ f x = f y → x = y

Tactic:
by

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

Goal state before:
pp: f : Bool → Bool
x : Bool
⊢ f (f (f x)) = f x

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : LE α
⊢ OrderTop α ⊕' NoTopOrder α

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Top α
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
ha : ∀ (h : p), a h ≠ ⊤
hb : ∀ (h : ¬p), b h ≠ ⊤
⊢ (if h : p then a h else b h) ≠ ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ a < ⊤ ↔ ¬⊤ ≤ a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ ¬IsMax a ↔ a < ⊤

Tactic:
rw [not_isMax_iff]

Goal state after:
α : Type u
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ (∃ b, a < b) ↔ a < ⊤
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ ¬IsMax a ↔ a < ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
hA : PartialOrder α
A : OrderTop α
hB : PartialOrder α
B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PartialOrder α
⊢ ∀ (a b : OrderBot α), a = b

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PartialOrder α
⊢ ∀ (a b : BoundedOrder α), a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Bot γ
x : α → β
⊢ ⊥ ∘ x = ⊥

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Unique α
⊢ ∀ (a : α), a ≤ default

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Unique α
⊢ ∀ (a : α), default ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ 0 ≤ a * b → 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : LE α
inst✝² : Top α
inst✝¹ : LE β
inst✝ : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ f ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u
p : α → Prop
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : OrderBot (Subtype p)
hbot : p ⊥
x : { x // p x }
⊢ ↑x = ⊥ ↔ x = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
⊢ a / (c * b) = a / c / b

Tactic:
← Nat.div_div_eq_div_mul

Goal state after:
a b c : ℕ
⊢ a / c / b = a / c / b
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: a b c : ℕ
⊢ a / b / c = a / c / b

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ Injective fun a ↦ a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
by

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

Goal state before:
pp: a : ℕ
ha : 2 ≤ a
⊢ Injective fun x ↦ a ^ x

Tactic:
by

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

Goal state before:
pp: x a : ℕ
hx : x ≠ 0
ha : a ≠ 0
⊢ x ^ (a - 1) = x ^ a / x

Tactic:
by

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

Goal state before:
pp: C : ℕ → Sort u_1
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
⊢ Injective (leRecOn hnm fun {k} ↦ next)

Tactic:
by

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

Goal state before:
pp: C : ℕ → Sort u_1
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
⊢ Surjective (leRecOn hnm fun {k} ↦ next)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
by

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

Goal state before:
pp: n m : ℕ
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n

Tactic:
by

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

Goal state before:
pp: a : ℕ
ha : a ≠ 1
b : ℕ
⊢ a * b ≤ a ^ b

Tactic:
by

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

Goal state before:
pp: k : ℕ
hk : k > 0
hk0 : 0 < 2 * k ^ 2
⊢ 2 * k ^ 2 + 2 * k ^ 2 = (2 * k) ^ 2

Tactic:
by

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

Goal state before:
pp: k : ℕ
hk : k > 0
hk0 : 0 < 2 * k ^ 2
⊢ 2 ≠ 1

Tactic:
by

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

Goal state before:
pp: k : ℕ
⊢ 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)

Tactic:
by

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

Goal state before:
pp: ⊢ 2 ≤ 0 ↔ 0 ≠ 0 ∧ 0 ≠ 1

Tactic:
by

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

Goal state before:
pp: ⊢ 2 ≤ 1 ↔ 1 ≠ 0 ∧ 1 ≠ 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ 2 ≤ n + 2 ↔ n + 2 ≠ 0 ∧ n + 2 ≠ 1

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ ¬2 * n % 2 = (2 * m + 1) % 2

Tactic:
by

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

Goal state before:
pp: n m : ℕ
⊢ m ≤ n / 2 ↔ ↑m * 2 ≤ ↑n

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
⊢ 2 * (n / 2) = n - 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec refl le_succ_of_le ⋯ = refl

Tactic:
by

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

Goal state before:
pp: m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
⊢ leRec refl le_succ_of_le h2 = le_succ_of_le h1 (leRec refl le_succ_of_le h1)

Tactic:
by

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

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec refl le_succ_of_le ⋯ = le_succ_of_le ⋯ refl

Tactic:
by

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

Goal state before:
pp: n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
hmk : m ≤ k
⊢ leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) hmk

Tactic:
by

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

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
m : ℕ
h1 : n ≤ m
h2 : n + 1 ≤ m
⊢ leRec (le_succ_of_le ⋯ refl) (fun x h ih ↦ le_succ_of_le ⋯ ih) h2 = leRec refl le_succ_of_le h1

Tactic:
by

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

Goal state before:
pp: a b c d e m✝ n✝ k : ℕ
p : ℕ → Prop
n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
m : ℕ
mn : m ≤ n
⊢ motive m mn

Tactic:
by

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

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
⊢ decreasingInduction of_succ self ⋯ = self

Tactic:
by

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

Goal state before:
pp: m n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
mn : m ≤ n
msn : m ≤ n + 1
⊢ decreasingInduction of_succ self msn = decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (of_succ n ⋯ self) mn

Tactic:
by

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

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
⊢ decreasingInduction of_succ self ⋯ = of_succ n ⋯ self

Tactic:
by

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

Goal state before:
pp: m n k : ℕ
motive : (m : ℕ) → m ≤ k → Sort u_1
hmn : m ≤ n
hnk : n ≤ k
of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯
self : motive k ⋯
⊢ decreasingInduction of_succ self ⋯ =
    decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn

Tactic:
by

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

Goal state before:
pp: m n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
smn : m + 1 ≤ n
mn : m ≤ n
⊢ decreasingInduction of_succ self mn = of_succ m smn (decreasingInduction of_succ self smn)

Tactic:
by

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

Goal state before:
pp: a b c d e m n k : ℕ
p : ℕ → Prop
P : ℕ → Sort u_1
h : (k : ℕ) → k < n → m ≤ k → P (k + 1) → P k
mn : m ≤ n
hP : P n
⊢ P m

Tactic:
by

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

Goal state before:
pp: P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ a + 1 = b ∨ a + 1 < b

Tactic:
by

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

Goal state before:
pp: P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ P (a + 1) (b + 1)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ¬2 ∣ 2 * n + 1

Tactic:
by

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

Goal state before:
pp: m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ m ∣ n ↔ n✝ ∣ n

Tactic:
by

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

Goal state before:
pp: m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ n ∣ m ↔ n ∣ n✝

Tactic:
by

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

Goal state before:
pp: a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ (∀ (x : ℕ), x < hi - lo → P (lo + x)) ↔ ∀ (x : ℕ), lo ≤ x → x < hi → P x

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : n.AtLeastTwo
⊢ n - 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
⊢ (cmpLE x y).swap = cmpLE y x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
⊢ cmpLE x y = cmp x y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : α
o : Ordering
⊢ o.swap.Compares a b ↔ o.Compares b a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: o o' : Ordering
⊢ o.swap = o' ↔ o = o'.swap

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h✝ : eq.Compares a b
h : eq = lt
⊢ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h✝ : gt.Compares a b
h : gt = lt
⊢ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x✝² x✝¹ : α
h✝ : eq.Compares x✝² x✝¹
x✝ : x✝¹ ≤ x✝²
h : eq = lt
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x✝² x✝¹ : α
h✝ : gt.Compares x✝² x✝¹
x✝ : x✝¹ ≤ x✝²
h : gt = lt
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h✝ : lt.Compares a b
h : lt = eq
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h✝ : gt.Compares a b
h : gt = eq
⊢ a = b

Tactic:
by

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

Goal state before:
pp: α : Type u
ι : Sort u_1
f : ι → α
⊢ Function.Injective (rangeFactorization f) ↔ Function.Injective f

Tactic:
by

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

Goal state before:
pp: α : Type u
ι : Sort u_1
f : ι → α
⊢ Function.Bijective (rangeFactorization f) ↔ Function.Injective f

Tactic:
by

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

Goal state before:
pp: ι : Sort u_2
α : Type u_3
f : ι → α
a b : ι
⊢ rangeFactorization f a = rangeFactorization f b ↔ f a = f b

Tactic:
by

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

Goal state before:
pp: ι : Sort u_2
α : Type u_3
f : ι → α
a : ι
b : ↑(range f)
⊢ rangeFactorization f a = b ↔ f a = ↑b

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ f ∘ rangeSplitting f = Subtype.val

Tactic:
by

Goal state after: