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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : a < b
h₂ : b < a
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : a < b
h₂ : ¬b < a
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

pp: case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : ¬a < b
h₂ : b < a
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : ¬a < b
h₂ : ¬b < a
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : a < b
h₂ : b < a
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : a < b
h₂ : ¬b < a
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : ¬a < b
h₂ : b < a
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : ¬a < b
h₂ : ¬b < a
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
⊢ ¬P x

Tactic:
intro hx'

Goal state after:
case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
hx' : P x
⊢ False
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case pos
p q : Prop
h : q
⊢ p ≤ q ∨ q ≤ p

pp: case neg
p q : Prop
h : ¬q
⊢ p ≤ q ∨ q ≤ p

Tactic:
<;>

Goal state after:
case pos
p q : Prop
h : q
⊢ p ≤ q ∨ q ≤ p

case neg
p q : Prop
h : ¬q
⊢ p ≤ q ∨ q ≤ p
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case pos
P Q : Prop
h✝ : P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

pp: case neg
P Q : Prop
h✝ : ¬P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Tactic:
<;>

Goal state after:
case pos
P Q : Prop
h✝ : P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

case neg
P Q : Prop
h✝ : ¬P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case pos
P Q : Prop
h✝¹ : P
h✝ : Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

pp: case neg
P Q : Prop
h✝¹ : P
h✝ : ¬Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

pp: case pos
P Q : Prop
h✝¹ : ¬P
h✝ : Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

pp: case neg
P Q : Prop
h✝¹ : ¬P
h✝ : ¬Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Tactic:
<;>

Goal state after:
case pos
P Q : Prop
h✝¹ : P
h✝ : Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

case neg
P Q : Prop
h✝¹ : P
h✝ : ¬Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

case pos
P Q : Prop
h✝¹ : ¬P
h✝ : Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

case neg
P Q : Prop
h✝¹ : ¬P
h✝ : ¬Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
Module: Mathlib.Order.PropInstances

Goal state before:
pp: P Q : Prop
⊢ IsCompl P Q ↔ ¬(P ↔ Q)

Tactic:
by
  rw [_root_.isCompl_iff, Prop.disjoint_iff, Prop.codisjoint_iff, not_iff]
  by_cases P <;> by_cases Q <;> simp [*]

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

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

pp: case refine_2
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c
⊢ b ≠ c

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c
⊢ a ≠ b

case refine_2
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c
⊢ b ≠ c
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: case pos
α : Type u
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
h✝ : p
⊢ x ∈ univ ↔ ∀ (h : ¬p), x ∈ t h

pp: case neg
α : Type u
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
h✝ : ¬p
⊢ x ∈ t h✝ ↔ ∀ (h : ¬p), x ∈ t h

Tactic:
<;>

Goal state after:
case pos
α : Type u
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
h✝ : p
⊢ x ∈ univ ↔ ∀ (h : ¬p), x ∈ t h

case neg
α : Type u
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
h✝ : ¬p
⊢ x ∈ t h✝ ↔ ∀ (h : ¬p), x ∈ t h
Module: Mathlib.Order.Lattice

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

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

Tactic:
<;>

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

case a
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ b ⊔ a ≤ a ⊔ b
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
s t✝ : Set α
a b : α
inst✝ : DecidableEq α
t : Set α
x : α
h : ¬x ∈ t
⊢ (fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) ((fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) none) = none

pp: case some
α : Type u_1
β : Type u_2
s t✝ : Set α
a b : α
inst✝ : DecidableEq α
t : Set α
x : α
h : ¬x ∈ t
y : { i // i ∈ t }
⊢ (fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) ((fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) (some y)) = some y

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
s t✝ : Set α
a b : α
inst✝ : DecidableEq α
t : Set α
x : α
h : ¬x ∈ t
⊢ (fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) ((fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) none) = none

case some
α : Type u_1
β : Type u_2
s t✝ : Set α
a b : α
inst✝ : DecidableEq α
t : Set α
x : α
h : ¬x ∈ t
y : { i // i ∈ t }
⊢ (fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) ((fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) (some y)) = some y
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl
ι : Type u_1
π : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
j : ι
a b : π j
⊢ update f j (a ⊔ b) j = (update f j a ⊔ update f j b) j

pp: case inr
ι : Type u_1
π : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
i : ι
a b : π i
j : ι
hji : j ≠ i
⊢ update f i (a ⊔ b) j = (update f i a ⊔ update f i b) j

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
π : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
j : ι
a b : π j
⊢ update f j (a ⊔ b) j = (update f j a ⊔ update f j b) j

case inr
ι : Type u_1
π : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
i : ι
a b : π i
j : ι
hji : j ≠ i
⊢ update f i (a ⊔ b) j = (update f i a ⊔ update f i b) j
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ f (max x y) = f x ⊔ f y

pp: case inr
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ f (max x y) = f x ⊔ f y

Tactic:
<;>

Goal state after:
case inl
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ f (max x y) = f x ⊔ f y

case inr
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ f (max x y) = f x ⊔ f y
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
this : f x ≤ f y
⊢ f (max x y) = f x ⊔ f y

pp: case inl.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ x ∈ s

pp: case inl.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ y ∈ s

pp: case inr.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
this : f y ≤ f x
⊢ f (max x y) = f x ⊔ f y

pp: case inr.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ y ∈ s

pp: case inr.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ x ∈ s

Tactic:
<;>

Goal state after:
case inl.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
this : f x ≤ f y
⊢ f (max x y) = f x ⊔ f y

case inl.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ x ∈ s

case inl.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ y ∈ s

case inr.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
this : f y ≤ f x
⊢ f (max x y) = f x ⊔ f y

case inr.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ y ∈ s

case inr.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ x ∈ s
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ f (max x y) = f x ⊓ f y

pp: case inr
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ f (max x y) = f x ⊓ f y

Tactic:
<;>

Goal state after:
case inl
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ f (max x y) = f x ⊓ f y

case inr
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ f (max x y) = f x ⊓ f y
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
this : f y ≤ f x
⊢ f (max x y) = f x ⊓ f y

pp: case inl.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ x ∈ s

pp: case inl.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ y ∈ s

pp: case inr.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
this : f x ≤ f y
⊢ f (max x y) = f x ⊓ f y

pp: case inr.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ y ∈ s

pp: case inr.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ x ∈ s

Tactic:
<;>

Goal state after:
case inl.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
this : f y ≤ f x
⊢ f (max x y) = f x ⊓ f y

case inl.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ x ∈ s

case inl.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ y ∈ s

case inr.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
this : f x ≤ f y
⊢ f (max x y) = f x ⊓ f y

case inr.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ y ∈ s

case inr.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ x ∈ s
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: case inl
α : Type u
s : Set α
h✝ : s = ∅
⊢ s.Subsingleton

pp: case inr
α : Type u
w✝ : α
⊢ {w✝}.Subsingleton

Tactic:
<;>

Goal state after:
case inl
α : Type u
s : Set α
h✝ : s = ∅
⊢ s.Subsingleton

case inr
α : Type u
w✝ : α
⊢ {w✝}.Subsingleton
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := ⋯
lt : LT α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := ⋯
lt : LT α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := ⋯
lt : LT α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := ⋯
lt : LT α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := e.le
lt : LT α := e.lt
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := e.le
lt : LT α := e.lt
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := e.le
lt : LT α := e.lt
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := e.le
lt : LT α := e.lt
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := e.preorder
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := e.preorder
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := e.preorder
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := e.preorder
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

pp: case min
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ (x y : α), e (x ⊓ y) = Min.min (e x) (e y)

pp: case max
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ (x y : α), e (x ⊔ y) = Max.max (e x) (e y)

pp: case compare
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ (x y : α), Ord.compare (e x) (e y) = Ord.compare x y

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case min
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ (x y : α), e (x ⊓ y) = Min.min (e x) (e y)

case max
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ (x y : α), e (x ⊔ y) = Max.max (e x) (e y)

case compare
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ (x y : α), Ord.compare (e x) (e y) = Ord.compare x y
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

pp: case min
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e (x✝ ⊓ y✝) = Min.min (e x✝) (e y✝)

pp: case max
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e (x✝ ⊔ y✝) = Max.max (e x✝) (e y✝)

pp: case compare
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ Ord.compare (e x✝) (e y✝) = Ord.compare x✝ y✝

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case min
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e (x✝ ⊓ y✝) = Min.min (e x✝) (e y✝)

case max
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e (x✝ ⊔ y✝) = Max.max (e x✝) (e y✝)

case compare
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ Ord.compare (e x✝) (e y✝) = Ord.compare x✝ y✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

pp: case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

pp: case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝