mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: n : Nat
⊢ bit (n.testBit 0) (n >>> 1) = n

Tactic:
simp

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

Goal state before:
pp: n : Nat
b : Bool
⊢ bit b n ≠ 0 ↔ n = 0 → b = true

Tactic:
simp

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

Goal state before:
pp: case false
x n : Nat
⊢ bit false x < 2 ^ (n + 1) ↔ x < 2 ^ n

Tactic:
simp

Goal state after:
case false
x n : Nat
⊢ 2 * x < 2 ^ (n + 1) ↔ x < 2 ^ n
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case true
x n : Nat
⊢ bit true x < 2 ^ (n + 1) ↔ x < 2 ^ n

Tactic:
simp

Goal state after:
case true
x n : Nat
⊢ 2 * x + 1 < 2 ^ (n + 1) ↔ x < 2 ^ n
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case succ.zero
n0 : ¬0 + 1 = 0
⊢ (if (0 + 1) >>> 1 = 0 then 0 else ((0 + 1) >>> 1).log2.succ) < if 0 + 1 = 0 then 0 else (0 + 1).log2.succ

Tactic:
simp

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

Goal state before:
pp: b : Bool
n : Nat
⊢ (bit b n).testBit 0 = b

Tactic:
simp

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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
⊢ 0 = 0 → true = true

Tactic:
simp

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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n = 0 → b = true
⊢ (if h : 0 = 0 → false = true then bit false 0 h zero
      else
        have this := ⋯;
        ⋯ ▸ zero) =
      zero ∨
    (n = 0 → b = true)

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowBinRec (n + 1) m = npowBinRec n m * m

Tactic:
rw [← npowBinRecAuto, ← npowRec_eq_npowBinRec]

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowRecAuto (n + 1) m = npowBinRec n m * m
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowRecAuto (n + 1) m = npowBinRec n m * m

Tactic:
rw [← npowBinRecAuto, ← npowRec_eq_npowBinRec]

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowRecAuto (n + 1) m = npowRecAuto n m * m
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ (0 + 1) = a * a ^ 0

Tactic:
simp

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

Goal state before:
pp: case zero
M : Type u_2
inst✝ : Monoid M
a b : M
⊢ (a * b) ^ 0 * a = a * (b * a) ^ 0

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 3 = a * (a * a)

Tactic:
rw [pow_succ', pow_two]

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: b : Prop
α : Sort u_2
i : Nonempty α
inst✝ : Subsingleton α
⊢ (∃! x, b) ↔ b

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: p q : Prop
⊢ (∃! x, q) ↔ p ∧ q

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α✝ : Sort u_1
α : Type u_2
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
⊢ ¬∃! x, x ∈ [] ∧ p x

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b : G
h : a * b = 1
⊢ b⁻¹ = a

Tactic:
rw [← inv_eq_of_mul_eq_one_right h, inv_inv]

Goal state after:
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
⊢ ¬Subsingleton α ↔ Nontrivial α

Tactic:
by
  rw [← not_nontrivial_iff_subsingleton, Classical.not_not]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β : Sort u
b : β
e : β = α
⊢ cast e b ≍ b

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
β : α → Sort u_3
⊢ (∀ (a : α) (a : β a), True) ↔ True

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
β : α → Sort u_3
γ : (a : α) → β a → Sort u_4
⊢ (∀ (a : α) (b : β a) (a : γ a b), True) ↔ True

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (a : α) (b : β), f a = b → p b) ↔ ∀ (a : α), p (f a)

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (a : α) (b : β), b = f a → p b) ↔ ∀ (a : α), p (f a)

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ ((a₁ == a₂) = true ↔ (b₁ == b₂) = true) ↔ (a₁ = a₂ ↔ b₁ = b₂)

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
inst1 inst2 : BEq α
inst✝¹ : LawfulBEq α
inst✝ : LawfulBEq α
x✝ y✝ : α
⊢ (x✝ == y✝) = (x✝ == y✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: case refine_1
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
x : A
⊢ default (f x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: case refine_2
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
x : B
⊢ f (default x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
⊢ False

Tactic:
cases hf (Set T) with | intro U hU =>
  let g : Set T → T := fun s ↦ ⟨U, cast hU.symm s⟩
  have hg : Injective g := by
    intro s t h
    suffices cast hU (g s).2 = cast hU (g t).2 by
      simp only [g, cast_cast, cast_eq] at this
      assumption
    · congr
  exact cantor_injective g hg

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst✝ : Nonempty γ
h : ∃ e, g = e ∘ f
x✝¹ x✝ : α
hf : f x✝¹ = f x✝
⊢ Classical.choose h (f x✝¹) = Classical.choose h (f x✝)

Tactic:
hf

Goal state after:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst✝ : Nonempty γ
h : ∃ e, g = e ∘ f
x✝¹ x✝ : α
hf : f x✝¹ = f x✝
⊢ Classical.choose h (f x✝) = Classical.choose h (f x✝)
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_1
p : α → Prop
a : α
h : p a
a' : α
h' : p a'
⊢ ⟨a, h⟩ = ⟨a', h'⟩ ↔ a = a'

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
β : Sort u_2
ra : α → α → Prop
rb : β → β → Prop
φ : Quot ra → Quot rb → Sort u_3
qa : Quot ra
qb : Quot rb
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ca : ∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂ → f a₁ b ≍ f a₂ b
cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂ → f a b₁ ≍ f a b₂
a₁ a₂ : α
pa : ra a₁ a₂
b : β
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
β : Sort u_2
ra : α → α → Prop
rb : β → β → Prop
φ : Quot ra → Quot rb → Sort u_3
qa : Quot ra
qb : Quot rb
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ca : ∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂ → f a₁ b ≍ f a₂ b
cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂ → f a b₁ ≍ f a b₂
a₁ a₂ : α
pa : ra a₁ a₂
b : β
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

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

Goal state before:
pp: α : Sort u_1
a b : α
⊢ (Equiv.cast ⋯) a = b ↔ a ≍ b

Tactic:
simp

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
p : Prop
⊢ (fun b ↦ b = true) ((fun p ↦ decide p) p) = p

Tactic:
simp

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
b : Bool
⊢ (fun p ↦ decide p) ((fun b ↦ b = true) b) = b

Tactic:
simp

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

Goal state before:
pp: α : Sort u
β✝ : Sort v
γ : Sort w
α₁ : Type u_1
α₂ : Type u_2
β : α₂ → Type ?u.16
e : α₁ ≃ α₂
x✝ : (a : α₁) × β (e a)
a : α₁
b : β (e a)
⊢ (fun a ↦ ⟨e.symm a.fst, ⋯ ▸ a.snd⟩) ((fun a ↦ ⟨e a.fst, a.snd⟩) ⟨a, b⟩) = ⟨a, b⟩

Tactic:
simp

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

Goal state before:
pp: α : Sort u
β✝ : Sort v
γ : Sort w
α₁ : Type u_1
α₂ : Type u_2
β : α₂ → Type ?u.16
e : α₁ ≃ α₂
x✝ : (a : α₂) × β a
a : α₂
b : β a
⊢ (fun a ↦ ⟨e a.fst, a.snd⟩) ((fun a ↦ ⟨e.symm a.fst, ⋯ ▸ a.snd⟩) ⟨a, b⟩) = ⟨a, b⟩

Tactic:
simp

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

Goal state before:
pp: α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
x✝¹ : α
x✝ : q (e x✝¹)
⊢ ∀ (a : α), q (e a) → a = x✝¹ ↔ q (e a) → e a = e x✝¹

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
⊢ ¬(x.isLeft = true ∧ x.isRight = true)

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (¬∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), ¬p fun t ↦ rec fa fb t) ↔
    ∃ fa fb, p fun t ↦ rec fa fb t

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u
β : Type v
a val✝ : α
⊢ inl val✝ = inl a ↔ ∃ h, (inl val✝).getLeft h = a

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u
β : Type v
a : α
val✝ : β
⊢ inr val✝ = inl a ↔ ∃ h, (inr val✝).getLeft h = a

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u
β : Type v
b : β
val✝ : α
⊢ inl val✝ = inr b ↔ ∃ h, (inl val✝).getRight h = b

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u
β : Type v
b val✝ : β
⊢ inr val✝ = inr b ↔ ∃ h, (inr val✝).getRight h = b

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : α
x : γ
⊢ x = Sum.elim (update f i x) g (inl i)

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : β
x : γ
⊢ x = Sum.elim f (update g i x) (inr i)

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
r : M
x : N
⊢ (r • x) ^ 0 = r ^ 0 • x ^ 0

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
d : δ
⊢ ∃ a, g a = d

Tactic:
obtain ⟨a | b, h⟩ := h (inr d)
        · cases h
        · exact ⟨b, inr_injective h⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
y : β
o : Option α
⊢ y ∈ Option.map f o ↔ ∃ x, x ∈ o ∧ f x = y

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
o : Option α
p : β → Prop
⊢ (∀ (y : β), y ∈ Option.map f o → p y) ↔ ∀ (x : α), x ∈ o → p (f x)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
o : Option α
p : β → Prop
⊢ (∃ y, y ∈ Option.map f o ∧ p y) ↔ ∃ x, x ∈ o ∧ p (f x)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
o o' : Option α
x : α
⊢ (o <|> o') = some x ↔ o = some x ∨ o = none ∧ o' = some x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
o o' : Option α
⊢ (o <|> o') = none ↔ o = none ∧ o' = none

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p₁ : α
p₂ : β
q₁ : α
q₂ : β
⊢ (p₁, p₂) = (q₁, q₂) ↔ (p₁, p₂).fst = (q₁, q₂).fst ∧ (p₁, p₂).snd = (q₁, q₂).snd

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
x : α
⊢ (a, b).fst = x ↔ (a, b) = (x, (a, b).snd)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b x : β
⊢ (a, b).snd = x ↔ (a, b) = ((a, b).fst, x)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
a₁ a₂ : α
ha : f a₁ = f a₂
⊢ a₁ = a₂

Tactic:
inhabit β

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
a₁ a₂ : α
ha : f a₁ = f a₂
inhabited_h : Inhabited β
⊢ a₁ = a₂
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
⊢ g₁ (g₂ d) = d

Tactic:
inhabit β

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
inhabited_h : Inhabited β
⊢ g₁ (g₂ d) = d
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α : Type u_1
a b : α
⊢ toDual a = toDual b ↔ a = b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α : Type u_1
a b : αᵒᵈ
⊢ ofDual a = ofDual b ↔ a = b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ max a b = if a < b then b else a

Tactic:
max_comm,

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ max b a = if a < b then b else a
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
⊢ Injective (@toPreorder α)

Tactic:
rintro ⟨⟩ ⟨⟩ ⟨⟩; congr

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.swap < (b, a).swap ↔ x < (a, b)

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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:
simp

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:
simp

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

Goal state before:
pp: case inr.inl
n : ℕ
h : 0 < n
⊢ n ∣ n - 0 ↔ 0 = 0 ∨ n ≤ 0

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: m n : ℕ
⊢ ¬0 = 1

Tactic:
simp

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

Goal state before:
pp: m n : ℕ
⊢ 1 < 2

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ univ.pi t ↔ ∀ (i : ι), f i ∈ t i

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x ≤ y ↔ x' ≤ y'

Tactic:
by
  rw [← not_lt, ← not_lt]
  apply not_congr
  apply lt_iff_lt_of_cmp_eq_cmp
  rwa [cmp_eq_cmp_symm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ≤ ⊥ ∧ b ≤ ⊥ ↔ a = ⊥ ∧ b = ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case mp
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
⊢ x ≤ f i → x ≤ g i → x ≤ ⊥

Tactic:
hf

Goal state after:
case mp
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
⊢ x ≤ g i → x ≤ ⊥
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case mpr
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : ∀ (i : ι), Disjoint (f i) (g i)
x : (i : ι) → α' i
⊢ x ≤ f → x ≤ g → x ≤ ⊥

Tactic:
hf

Goal state after:
case mpr
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : ∀ (i : ι), Disjoint (f i) (g i)
x : (i : ι) → α' i
hf : x ≤ f
⊢ x ≤ g → x ≤ ⊥
Module: Mathlib.Tactic.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst✝¹ : CanLift α β coeβα condβα
inst✝ : CanLift γ δ coeδγ condδγ
x : β
y : δ
hx : condβα (coeβα x, coeδγ y).fst
hy : condδγ (coeβα x, coeδγ y).snd
⊢ map coeβα coeδγ (x, y) = (coeβα x, coeδγ y)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this✝ : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot hbot
⊢ a ⊓ b = ⊥ ↔ ↑(a ⊓ b) = ↑⊥

Tactic:
exact Subtype.coe_inj.symm

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

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₂

Tactic:
exact h_mon h₂

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑a ≤ ↑b ↔ a ≤ b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑a < ↑b ↔ a < b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
⊢ ⟨⊥, ⋯⟩ = ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
⊢ ⟨⊤, ⋯⟩ = ⊤

Tactic:
simp

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

Goal state before:
pp: α : Type u
s : Set α
⊢ (s ⊆ univ ∧ ∃ a, ¬a ∈ s) ↔ ∃ x, x ∈ sᶜ

Tactic:
simp

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

Goal state before:
pp: α : Type u
s : Set α
⊢ (sᶜ ⊆ univ ∧ ∃ a, ¬a ∈ sᶜ) ↔ ∃ x, x ∈ s

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ⊔ b ≤ a ∧ a ≤ a ⊔ b ↔ b ≤ a

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ⊔ b ≤ b ∧ b ≤ a ⊔ b ↔ a ≤ b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a : α
⊢ a ⊔ a = a

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case a
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ⊔ b ≤ b ⊔ a

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case a
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ b ⊔ a ≤ a ⊔ b

Tactic:
simp

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

Goal state before:
pp: α : Type u
p : Prop
inst✝ : Decidable p
t : Set α
x : α
⊢ (∃ h, x ∈ t) ↔ p ∧ x ∈ t

Tactic:
simp

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

Goal state before:
pp: α : Type u
p : Prop
inst✝ : Decidable p
t : Set α
x : α
⊢ (∃ h, x ∈ t) ↔ ¬p ∧ x ∈ t

Tactic:
simp

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

Goal state before:
pp: α : Type u
s t : Set α
a b : α
⊢ ¬a ∈ ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ⊔ (a ⊔ b) = a ⊔ b

Tactic:
simp

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

Goal state before:
pp: α : Type u
s t : Set α
a b : α
⊢ a ∈ univ

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ⊔ b ⊔ b = a ⊔ b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
a b : α
⊢ {a} ⊆ {b} ↔ a = b

Tactic:
simp

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

Goal state before:
pp: case mpr
α : Type u_1
a : α
H : [a].Nodup
⊢ {x | x ∈ [a]} = {a}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ s ⊂ {x} ↔ s = ∅

Tactic:
rw [ssubset_iff_subset_ne, subset_singleton_iff_eq, or_and_right, and_not_self_iff, or_false,
    and_iff_left_iff_imp]

Goal state after:
α : Type u_1
s : Set α
x : α
⊢ s = ∅ → s ≠ {x}
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
a b : α
⊢ Disjoint {a} {b} ↔ a ≠ b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊓ (a ⊔ b) = a

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c) = a ⊓ b ⊔ a ⊓ c

Tactic:
sup_inf_left

Goal state after:
α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c) = (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c)
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: α : Type u
inst✝ : IsEmpty α
⊢ {∅} ⊆ univ

Tactic:
simp

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

Goal state before:
pp: α : Type u
x✝ : IsEmpty α
⊢ univ = {∅}

Tactic:
simp

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

Goal state before:
pp: α : Type u
h : univ = {∅}
⊢ univ ∈ univ

Tactic:
simp

Goal state after: