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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ (if ¬b ≤ a then b else a) = if a < b then b else a

Tactic:
;

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

Goal state before:
pp: α : Type u_2
toPreorder✝ : Preorder α
le_antisymm✝¹ le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
⊢ { toPreorder := toPreorder✝, le_antisymm := le_antisymm✝¹ } =
    { toPreorder := toPreorder✝, le_antisymm := le_antisymm✝ }

Tactic:
;

Goal state after:
α : Type u_2
toPreorder✝ : Preorder α
le_antisymm✝¹ le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
⊢ { toPreorder := toPreorder✝, le_antisymm := le_antisymm✝¹ } =
    { toPreorder := toPreorder✝, le_antisymm := le_antisymm✝ }
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A B : Preorder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y

Tactic:
;

Goal state after:
α : Type u_2
A B : Preorder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y

Tactic:
;

Goal state after:
α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
x y : α
⊢ x ≤ y ↔ x ≤ y

Tactic:
;

Goal state after:
α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
x y : α
⊢ x ≤ y ↔ x ≤ y
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A B : LinearOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y

Tactic:
;

Goal state after:
α : Type u_2
A B : LinearOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y
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:
;

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

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
x : α × β
⊢ x.swap.swap < (b, a).swap ↔ x < (a, b)
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:
;

Goal state after:
α : Type u_2
inst✝¹ : LT α
inst✝ : DenselyOrdered α
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PartialOrder α
a : α
ha : ∀ (a_1 : α), ⊥ ≤ a_1
b : α
hb : ∀ (a : α), ⊥ ≤ a
⊢ { bot := a, bot_le := ha } = { bot := b, bot_le := hb }

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝ : PartialOrder α
a : α
ha : ∀ (a_1 : α), ⊥ ≤ a_1
b : α
hb : ∀ (a : α), ⊥ ≤ a
⊢ { bot := a, bot_le := ha } = { bot := b, bot_le := hb }
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PartialOrder α
a : α
ha : ∀ (a_1 : α), ⊥ ≤ a_1
b : α
hb : ∀ (a : α), ⊥ ≤ a
⊢ a = b

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝ : PartialOrder α
a : α
ha : ∀ (a_1 : α), ⊥ ≤ a_1
b : α
hb : ∀ (a : α), ⊥ ≤ a
⊢ a = b
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PartialOrder α
toOrderTop✝¹ : OrderTop α
toOrderBot✝¹ : OrderBot α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
⊢ { toOrderTop := toOrderTop✝¹, toOrderBot := toOrderBot✝¹ } = { toOrderTop := toOrderTop✝, toOrderBot := toOrderBot✝ }

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝ : PartialOrder α
toOrderTop✝¹ : OrderTop α
toOrderBot✝¹ : OrderBot α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
⊢ { toOrderTop := toOrderTop✝¹, toOrderBot := toOrderBot✝¹ } = { toOrderTop := toOrderTop✝, toOrderBot := toOrderBot✝ }
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case succ.inl
b : ℕ
ha : 0 ≠ 1
⊢ 0 ≤ 0 ^ (b + 1)

Tactic:
;

Goal state after:
case succ.inl
b : ℕ
ha : 0 ≠ 1
⊢ 0 ≤ 0 ^ (b + 1)
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case succ.inr
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
ha1 : a > 1
⊢ a * (b + 1) ≤ a * a ^ b

Tactic:
;

Goal state after:
case succ.inr
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
ha1 : a > 1
⊢ a * (b + 1) ≤ a * a ^ b
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
⊢ leRec (motive := fun {n} mn ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) msn of_succ self =
    leRec (motive := fun {n} mn ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) mn (fun x x_1 ↦ of_succ x ⋯)
      (of_succ n ⋯ self)

Tactic:
;

Goal state after:
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
⊢ leRec (motive := fun {n} mn ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) msn of_succ self =
    leRec (motive := fun {n} mn ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) mn (fun x x_1 ↦ of_succ x ⋯)
      (of_succ n ⋯ self)
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) ⋯
⊢ leRec (motive := fun {n_1} mn ↦
      {motive : (m : ℕ) → m ≤ n_1 → Sort u_1} →
        ((k : ℕ) → (h : k < n_1) → motive (k + 1) h → motive k ⋯) → motive n_1 ⋯ → motive n mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) ⋯ of_succ self =
    of_succ n ⋯ self

Tactic:
;

Goal state after:
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) ⋯
⊢ leRec (motive := fun {n_1} mn ↦
      {motive : (m : ℕ) → m ≤ n_1 → Sort u_1} →
        ((k : ℕ) → (h : k < n_1) → motive (k + 1) h → motive k ⋯) → motive n_1 ⋯ → motive n mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) ⋯ of_succ self =
    of_succ n ⋯ self
Module: Mathlib.Data.Nat.Init

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

Tactic:
;

Goal state after:
n : ℕ
inst✝ : n.AtLeastTwo
this : 2 ≤ n
⊢ n - 1 ≠ 0
Module: Mathlib.Order.Compare

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

Tactic:
simp [cmpLE, *, Ordering.swap]

Goal state after:
Module: Mathlib.Order.Compare

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

Tactic:
simp [cmpLE, *, Ordering.swap]

Goal state after:
Module: Mathlib.Order.Compare

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

Tactic:
simp [cmpLE, *, Ordering.swap]

Goal state after:
Module: Mathlib.Order.Compare

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

Tactic:
simp [cmpLE, *, Ordering.swap]

Goal state after:
case neg
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsStrictOrder α r
x y : α
h : r x x
e : y = x
⊢ False

Tactic:
;

Goal state after:
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsStrictOrder α r
x y : α
h : r x x
e : y = x
⊢ False
Module: Mathlib.Order.BoundedOrder.Lattice

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ≤ ⊥ ∧ b ≤ ⊥ ↔ a = ⊥ ∧ b = ⊥
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:
;

Goal state after:
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₂
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderTop α
a b c : α
h : b ⊓ a ≤ c
hd : Codisjoint b c
⊢ a ⊓ b ≤ c

Tactic:
inf_comm

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderTop α
a b c : α
h : b ⊓ a ≤ c
hd : Codisjoint b c
⊢ b ⊓ a ≤ c
Module: Mathlib.Order.Monotone.Basic

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

Tactic:
;

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₂ ≤ f i
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a c : α
h : f a < f a ∧ f c < f a ∨ f a < f a ∧ f a < f c
⊢ False

Tactic:
;

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a c : α
h : f a < f a ∧ f c < f a ∨ f a < f a ∧ f a < f c
⊢ False
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
h : f a < f b ∧ f b < f b ∨ f b < f a ∧ f b < f b
⊢ False

Tactic:
;

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
h : f a < f b ∧ f b < f b ∨ f b < f a ∧ f b < f b
⊢ False
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case refl
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
⊢ r (f b) (f b.succ)

Tactic:
exact h _ hab

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

Goal state before:
pp: case zero
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + 1))

Tactic:
;

Goal state after:
case zero
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + 1))
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case succ
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑n.succ))
⊢ r (f a) (f (a + ↑(n + 1) + 1))

Tactic:
;

Goal state after:
case succ
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑n.succ))
⊢ r (f a) (f (a + ↑(n + 1) + 1))
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Min α
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
a b : α
hba : b ⊓ a = a
hab : a ⊓ b = b
⊢ b ⊓ a = b

Tactic:
inf_comm

Goal state after:
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Min α
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
a b : α
hba : b ⊓ a = a
hab : a ⊓ b = b
⊢ a ⊓ b = b
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Min α
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
a b : α
⊢ b ⊓ (a ⊓ b) = a ⊓ b

Tactic:
inf_comm,

Goal state after:
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Min α
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
a b : α
⊢ a ⊓ b ⊓ b = a ⊓ b
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s t : Set α
⊢ s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅

Tactic:
by
  simp only [← subset_empty_iff]
  exact union_subset_iff

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c x : α
⊢ (a ≤ x ∧ b ≤ x) ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x

Tactic:
;

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c x : α
⊢ (a ≤ x ∧ b ≤ x) ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u_1
s✝ t u : Set α
p : α → Prop
s : Set { a // p a }
a : { a // p a }
⊢ a ∈ (fun s ↦ {a | ↑a ∈ ↑s}) ((fun s ↦ ⟨{a | ∃ h, ⟨a, h⟩ ∈ s}, ⋯⟩) s) ↔ a ∈ s

Tactic:
;

Goal state after:
α : Type u_1
s✝ t u : Set α
p : α → Prop
s : Set { a // p a }
a : { a // p a }
⊢ a ∈ (fun s ↦ {a | ↑a ∈ ↑s}) ((fun s ↦ ⟨{a | ∃ h, ⟨a, h⟩ ∈ s}, ⋯⟩) s) ↔ a ∈ s
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u_1
s✝ t u : Set α
p : α → Prop
s : { s // ∀ (a : α), a ∈ s → p a }
x✝ : α
⊢ x✝ ∈ ↑((fun s ↦ ⟨{a | ∃ h, ⟨a, h⟩ ∈ s}, ⋯⟩) ((fun s ↦ {a | ↑a ∈ ↑s}) s)) ↔ x✝ ∈ ↑s

Tactic:
;

Goal state after:
α : Type u_1
s✝ t u : Set α
p : α → Prop
s : { s // ∀ (a : α), a ∈ s → p a }
x✝ : α
⊢ x✝ ∈ ↑((fun s ↦ ⟨{a | ∃ h, ⟨a, h⟩ ∈ s}, ⋯⟩) ((fun s ↦ {a | ↑a ∈ ↑s}) s)) ↔ x✝ ∈ ↑s
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c

Tactic:
;

Goal state after:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
N : ℕ
hc : f N ≤ c + 1
hN : c < f N
⊢ f N = c + 1

Tactic:
;

Goal state after:
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
N : ℕ
hc : f N ≤ c + 1
hN : c < f N
⊢ f N = c + 1
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
x y z w : α
⊢ ((x = z ∨ x = w) ∧ (y = z ∨ y = w)) ∧ (z = x ∨ z = y) ∧ (w = x ∨ w = y) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
;

Goal state after:
α : Type u_1
x y z w : α
⊢ ((x = z ∨ x = w) ∧ (y = z ∨ y = w)) ∧ (z = x ∨ z = y) ∧ (w = x ∨ w = y) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
Module: Mathlib.Order.Lattice

Goal state before:
pp: case e_sup
α : Type u_1
toPartialOrder✝ : PartialOrder α
sup✝¹ : α → α → α
le_sup_left✝¹ : ∀ (a b : α), a ≤ sup✝¹ a b
le_sup_right✝¹ : ∀ (a b : α), b ≤ sup✝¹ a b
sup_le✝¹ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝¹ a b ≤ c
sup✝ : α → α → α
le_sup_left✝ : ∀ (a b : α), a ≤ sup✝ a b
le_sup_right✝ : ∀ (a b : α), b ≤ sup✝ a b
sup_le✝ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝ a b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝¹ x✝ : α
⊢ sup✝¹ x✝¹ x✝ = sup✝ x✝¹ x✝

Tactic:
;

Goal state after:
case e_sup
α : Type u_1
toPartialOrder✝ : PartialOrder α
sup✝¹ : α → α → α
le_sup_left✝¹ : ∀ (a b : α), a ≤ sup✝¹ a b
le_sup_right✝¹ : ∀ (a b : α), b ≤ sup✝¹ a b
sup_le✝¹ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝¹ a b ≤ c
sup✝ : α → α → α
le_sup_left✝ : ∀ (a b : α), a ≤ sup✝ a b
le_sup_right✝ : ∀ (a b : α), b ≤ sup✝ a b
sup_le✝ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝ a b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝¹ x✝ : α
⊢ sup✝¹ x✝¹ x✝ = sup✝ x✝¹ x✝
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case h
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : f N = c + 1
⊢ ∀ (n : ℕ), n ≥ N → f n = c + 1

Tactic:
;

Goal state after:
case h
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : f N = c + 1
⊢ ∀ (n : ℕ), n ≥ N → f n = c + 1
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case h
f : ℕ → ℕ
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : f N = c + 1
n : ℕ
mono_f : f N ≤ f n
hn : n ≥ N
⊢ f n = c + 1

Tactic:
;

Goal state after:
case h
f : ℕ → ℕ
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : f N = c + 1
n : ℕ
mono_f : f N ≤ f n
hn : n ≥ N
⊢ f n = c + 1
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case h
f : ℕ → ℕ
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
N : ℕ
hN : f N = c + 1
n : ℕ
hc : f n ≤ c + 1
mono_f : f N ≤ f n
hn : n ≥ N
⊢ f n = c + 1

Tactic:
;

Goal state after:
case h
f : ℕ → ℕ
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
N : ℕ
hN : f N = c + 1
n : ℕ
hc : f n ≤ c + 1
mono_f : f N ≤ f n
hn : n ≥ N
⊢ f n = c + 1
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 : a ⊔ b = b
⊢ (a ⊔ b) ⊓ a = a

Tactic:
inf_comm,

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 : a ⊔ b = b
⊢ a ⊓ (a ⊔ b) = a
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
hs : s.Nonempty
⊢ ¬s = ∅

Tactic:
;

Goal state after:
α : Type u_1
s : Set α
a b : α
hs : s.Nonempty
⊢ ¬s = ∅
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: α : Type u
a : α
s : Set α
ha : a ∈ s
⊢ s.Subsingleton ∨ s.Nontrivial

Tactic:
;

Goal state after:
α : Type u
a : α
s : Set α
ha : a ∈ s
⊢ s.Subsingleton ∨ s.Nontrivial
Module: Mathlib.Order.GaloisConnection.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
⊢ (∀ (b : α) (a : β), u a ≤ b ↔ a ≤ l b) = ∀ (a : α) (b : β), b ≤ l a ↔ u b ≤ a

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
⊢ (∀ (b : α) (a : β), u a ≤ b ↔ a ≤ l b) = ∀ (a : α) (b : β), b ≤ l a ↔ u b ≤ a
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ⊓ b ≤ c ↔ b ⊓ a ≤ c

Tactic:
inf_comm

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ b ⊓ a ≤ c ↔ b ⊓ a ≤ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊓ (a ⇨ b) ≤ b

Tactic:
inf_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ (a ⇨ b) ⊓ a ≤ b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ (a ⇨ b) ⊓ a = b ⊓ a

Tactic:
inf_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊓ (a ⇨ b) = b ⊓ a
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊓ b = b ⊓ a

Tactic:
inf_comm

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ b ⊓ a = b ⊓ a
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ⊓ b ⇨ c = b ⊓ a ⇨ c

Tactic:
inf_comm

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ a ⇨ a ⊓ b = b

Tactic:
rw [himp_inf_distrib, himp_self, top_inf_eq, h.himp_eq_left]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ b ⊓ a ⊔ c ⊓ a ≤ b ⊓ a ⊔ c ⊓ a

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ b ⊓ a ⊔ c ⊓ a ≤ b ⊓ a ⊔ c ⊓ a
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ c ⊔ b

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ c ⊔ b
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α : Type u₀
x✝ : f α
⊢ (mapEquiv f (Equiv.refl α)) x✝ = (Equiv.refl (f α)) x✝

Tactic:
;

Goal state after:
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α : Type u₀
x✝ : f α
⊢ (mapEquiv f (Equiv.refl α)) x✝ = (Equiv.refl (f α)) x✝
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
inf_comm,

Goal state after:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y : α
⊢ x ⊓ y ⊓ x \ y = ⊥
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d : α
a b c : αᵒᵈ
⊢ a ≤ toDual (ofDual c \ ofDual b) ↔ a ⊓ b ≤ c

Tactic:
inf_comm

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d : α
a b c : αᵒᵈ
⊢ a ≤ toDual (ofDual c \ ofDual b) ↔ b ⊓ a ≤ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d : α
a b c : αᵒᵈ
⊢ a ≤ toDual (ofDual c \ ofDual b) ↔ b ⊓ a ≤ c

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d : α
a b c : αᵒᵈ
⊢ a ≤ toDual (ofDual c \ ofDual b) ↔ b ⊓ a ≤ c