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

Goal state before:
pp: n : Nat
⊢ bit (decide (n % 2 = 1)) (n >>> 1) = n

Tactic:
simp only [bit, shiftRight_one]

Goal state after:
n : Nat
⊢ (bif decide (n % 2 = 1) then 2 * (n / 2) + 1 else 2 * (n / 2)) = n
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:
by 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:
by simp

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * a * b⁻¹ * (b * x * b⁻¹) = b * y * b⁻¹ * (b * a * b⁻¹) ↔ a * x = y * a

Tactic:
simp only [← mul_assoc, inv_mul_cancel_right]

Goal state after:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * a * x * b⁻¹ = b * y * a * b⁻¹ ↔ a * x = y * a
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:
by simp

Goal state after:
Module: Mathlib.Logic.ExistsUnique

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Logic.ExistsUnique

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

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

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b : M
reg : IsRightRegular a
eq : b * a = 1
⊢ (fun x ↦ x * a) (a * b) = (fun x ↦ x * a) 1

Tactic:
simp [mul_assoc, eq]

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b : M
reg : IsRightRegular a
eq : b * a = 1
⊢ (fun x ↦ x * a) (a * b) = (fun x ↦ x * a) 1

Tactic:
by simp [mul_assoc, eq]

Goal state after:
Module: Mathlib.Logic.Basic

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

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

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
⊢ x = y

Tactic:
rcases em (p x) with (hx | hx)

Goal state after:
case inl
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : p x
⊢ x = y

case inr
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : ¬p x
⊢ x = y
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
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
s : Set T
⊢ ∀ ⦃a₂ : Set T⦄, g s = g a₂ → s = a₂

Tactic:
t

Goal state after:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
s t : Set T
⊢ g s = g t → s = t
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Sort u_6
f : α → β
g : β → Option α
h : β → γ
i : γ → Option β
hf : IsPartialInv f g
hh : IsPartialInv h i
a : α
b : γ
⊢ (fun x ↦ (i x).bind g) b = some a ↔ (h ∘ f) a = b

Tactic:
simp [Option.bind_eq_some_iff, hh _, hf _]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
b : β
hr : rβ b (f a)
⊢ Acc rβ b

Tactic:
obtain ⟨a', hr', rfl⟩ := fib hr

Goal state after:
case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
a' : α
hr' : rα a' a
hr : rβ (f a') (f a)
⊢ Acc rβ (f a')
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:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.Associative gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x₁ x₂ x₃ : α
⊢ f (ga (ga x₁ x₂) x₃) = f (ga x₁ (ga x₂ x₃))

Tactic:
by simp only [h.eq, Std.Associative.assoc (op := gb)]

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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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
n : ℕ
⊢ (r * r ^ n) • (x * x ^ n) = r ^ (n + 1) • x ^ (n + 1)

Tactic:
← pow_succ',

Goal state after:
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
n : ℕ
⊢ r ^ (n + 1) • (x * x ^ n) = r ^ (n + 1) • x ^ (n + 1)
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:
by 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:
by 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:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
x : Option α
f : α → β
⊢ Option.map f x = some b ↔ ∃ a, x = some a ∧ f a = b

Tactic:
map_eq_some_iff

Goal state after:
α : Type u_1
β : Type u_2
b : β
x : Option α
f : α → β
⊢ (∃ a, x = some a ∧ f a = b) ↔ ∃ a, x = some a ∧ f a = b
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:
by simp

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

Goal state before:
pp: α : Type u_5
β : Type u_6
a : α
⊢ Function.Injective (mk a)

Tactic:
by
  intro b₁ b₂ h
  simpa only [true_and, Prod.mk_inj, eq_self_iff_true] using h

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

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ∀ {x y : α}, compare x y = Ordering.lt ↔ x < y

Tactic:
simp [compare_lt_iff_lt]

Goal state after:
Module: Mathlib.Order.OrderDual

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.OrderDual

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

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

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

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

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

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint (a ⊓ b) c ↔ Disjoint a (b ⊓ c)

Tactic:
grind [disjoint_iff_inf_le]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint a (b ⊓ c) ↔ Disjoint b (a ⊓ c)

Tactic:
grind [disjoint_iff_inf_le]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint (a ⊓ b) c ↔ Disjoint (a ⊓ c) b

Tactic:
grind [disjoint_iff_inf_le]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
x y : α
h₁ : x ⊓ y ≤ ⊥
h₂ : ⊤ ≤ x ⊔ y
⊢ Disjoint x y

Tactic:
grind [disjoint_iff_inf_le]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ y ⊓ (x' ⊓ y') = ⊥

Tactic:
h'.inf_eq_bot,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ y ⊓ ⊥ = ⊥
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
x : α
h : IsCompl x ⊥
⊢ x ⊔ ⊥ = ⊤

Tactic:
h.sup_eq_top

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
x : α
h : IsCompl x ⊥
⊢ ⊤ = ⊤
Module: Mathlib.Order.Disjoint

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

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

Goal state after:
Module: Mathlib.Order.Disjoint

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Disjoint

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Monotone f
n a : ℤ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False

Tactic:
exact (hf.reflect_lt h1).not_ge (Int.le_of_lt_add_one <| hf.reflect_lt h2)

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

Goal state after:
Module: Mathlib.Order.Lattice

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

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

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

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

Tactic:
by simp

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

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
x y z w : α
⊢ {x, y} = {z, w} ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
by
  simp [subset_antisymm_iff, insert_subset_iff]; aesop

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : b ⊓ a = a
⊢ b ⊔ b ⊓ a = b

Tactic:
sup_inf_self

Goal state after:
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : b ⊓ a = a
⊢ b = b
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
b : α
⊢ b ⊔ b ⊓ (b ⊔ b) = b

Tactic:
sup_inf_self

Goal state after:
α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
b : α
⊢ b = b
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
b : α
⊢ b ⊓ b = b ⊓ (b ⊔ b ⊓ b)

Tactic:
sup_inf_self

Goal state after:
α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
b : α
⊢ b ⊓ b = b ⊓ b
Module: Mathlib.Order.Lattice

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
sup_inf_self

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

Goal state before:
pp: α : Type u
s : Set α
p : Set α → Prop
hs : s.Subsingleton
he : p ∅
h₁ : ∀ (x : α), p {x}
⊢ p s

Tactic:
by
  rcases hs.eq_empty_or_singleton with (rfl | ⟨x, rfl⟩)
  exacts [he, h₁ _]

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

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

Tactic:
by simp

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

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Defs

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
⊢ ∀ (x y z : PUnit), min (max x y) (max x z) ≤ max x (min y z)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y \ x ⊔ x = y \ x ⊔ (x ⊔ x ⊓ y)

Tactic:
sup_inf_self

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y \ x ⊔ x = y \ x ⊔ x
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
x : α
⊢ x ∈ s ∧ ¬x ∈ t ↔ x ∈ s ∩ tᶜ

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
x : α
⊢ e.optionCongr (some x) = some (e x)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ s \ {a} ⊂ s ↔ a ∈ s

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
a b : α
hab : a ≠ b
⊢ {a, b} \ {a} = {b}

Tactic:
rw [insert_sdiff_of_mem _ (mem_singleton a), sdiff_singleton_eq_self (by simpa)]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ (optionSubtypeNe a).symm a = none

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : α → Type u_4
a₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
⊢ ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ b₁ ≍ b₂

Tactic:
by simp

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ x ⊓ y \ x ⊓ y \ z ⊔ y \ x ⊓ (y \ z ⊓ (y ⊓ z)) = ⊥

Tactic:
by simp

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y))) = x

Tactic:
by simp

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

Goal state before:
pp: α : Sort u_1
α₁✝ : Sort u_2
α₂✝ : Sort u_3
β : Sort u_4
β₁✝ : Sort u_5
β₂✝ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type ?u.23
α₂ : Type ?u.25
β₁ : Type ?u.22
β₂ : Type ?u.24
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
x : α₁ ⊕ β₁
⊢ Sum.map (⇑ea.symm) (⇑eb.symm) (Sum.map (⇑ea) (⇑eb) x) = x

Tactic:
by simp

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

Goal state before:
pp: α : Sort u_1
α₁✝ : Sort u_2
α₂✝ : Sort u_3
β : Sort u_4
β₁✝ : Sort u_5
β₂✝ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type ?u.23
α₂ : Type ?u.25
β₁ : Type ?u.22
β₂ : Type ?u.24
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
x : α₂ ⊕ β₂
⊢ Sum.map (⇑ea) (⇑eb) (Sum.map (⇑ea.symm) (⇑eb.symm) x) = x

Tactic:
by simp

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ (x \ y) = x ⊓ y

Tactic:
sdiff_sdiff_right,

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ x ⊔ x ⊓ x ⊓ y = x ⊓ y