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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ sSup ∅ = sSup ∅

pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ ¬BddAbove univ

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ ¬BddAbove univ
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ x ∈ ∅, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ ∅, y ≤ x
this : t = ∅
⊢ sSup ∅ = sSup ∅

Tactic:
]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ (⨆ a, ↑a) ∆ a ≤ ⨆ a_1, ↑a_1 ∆ a

Tactic:
]

Goal state after:
α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ (⨆ a, ↑a) ∆ a ≤ ⨆ a_1, ↑a_1 ∆ a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup s ∆ sSup t ≤ ⨆ a ∈ s, ⨆ b ∈ t, a ∆ b

Tactic:
]

Goal state after:
α : Type u
inst✝ : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup s ∆ sSup t ≤ ⨆ a ∈ s, ⨆ b ∈ t, a ∆ b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
s_ne : s.Nonempty
hs : ∀ x ∈ s, ∃ y ∈ ∅, x ≤ y
ht : ∀ y ∈ ∅, ∃ x ∈ s, y ≤ x
this : s = ∅
⊢ sSup ∅ = sSup ∅

Tactic:
]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompleteAtomicBooleanAlgebra (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
x✝ : ι
⊢ (⨆ g, ⨅ a, f a (g a)) x✝ = (⨆ g, ⨅ a, f a (g a)) x✝

Tactic:
]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : Frame.MinimalAxioms β
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
a : α
s : Set α
⊢ ⨆ i ∈ s, f a ⊓ f i ≤ f (sSup (min a '' s))

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : Frame.MinimalAxioms β
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
a : α
s : Set α
⊢ ⨆ i ∈ s, f a ⊓ f i ≤ f (sSup (min a '' s))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ sSup (⋃ i, Iic (f i)) = ⨆ i, f i

Tactic:
apply csSup_eq_csSup_of_forall_exists_le

Goal state after:
case hs
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ∀ x ∈ ⋃ i, Iic (f i), ∃ y ∈ range fun i ↦ f i, x ≤ y

case ht
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ∀ y ∈ range fun i ↦ f i, ∃ x ∈ ⋃ i, Iic (f i), y ≤ x
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
⊢ IsLeast s (argminOn id s hs)

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
⊢ IsLeast s (argminOn id s hs)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
⊢ ⊥ ≤ sSup t

Tactic:
]

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
⊢ ⊥ ≤ sSup t
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
⊢ ⊤ ≤ c

Tactic:
]

Goal state after:
case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
⊢ ⊤ ≤ c
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
b : β
hb : b ∈ (fun a ↦ ↑a) ⁻¹' s
⊢ ↑a ≤ ↑b

Tactic:
]

Goal state after:
case neg.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
b : β
hb : b ∈ (fun a ↦ ↑a) ⁻¹' s
⊢ ↑a ≤ ↑b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hb : BddAbove s
⊢ ⨆ a ∈ s, ↑a = ⨆ a ∈ s, ↑a

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ico a b = Ico a b

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
h's : BddBelow s
⊢ ⨅ a ∈ s, ↑a = ⨅ a ∈ s, ↑a

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Icc a b = Icc a b

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioc a b = Ioc a b

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioo a b = Ioo a b

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
this : y = x
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
this : y = x
⊢ False
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
⊢ Icc a b = ⇑ofDual ⁻¹' Icc a b

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
⊢ Icc a b = ⇑ofDual ⁻¹' Icc a b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc (toDual b) (toDual a))
this : Icc a b = Icc (toDual b) (toDual a)
⊢ sInf (f '' Icc (toDual b) (toDual a)) = f b

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc (toDual b) (toDual a))
this : Icc a b = Icc (toDual b) (toDual a)
⊢ sInf (f '' Icc (toDual b) (toDual a)) = f b
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a b : α
h : a ≤ b
⊢ Icc a b = Icc a b

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a b : α
h : b ≤ a
⊢ Icc b a = Icc b a

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ [[b, a]]) b ↔ x ∈ (fun b ↦ [[b, a]]) c
⊢ b = c

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DistribLattice α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ [[b, a]]) b ↔ x ∈ (fun b ↦ [[b, a]]) c
⊢ b = c
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (min a b)) (f (max a b)))

pp: case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

pp: case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

pp: case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

pp: case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (min a b)) (f (max a b)))

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
h : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ¬Disjoint (f i) (f j) → i = j

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
h : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ¬Disjoint (f i) (f j) → i = j
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (max a b)) (f (min a b)))

pp: case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

pp: case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

pp: case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

pp: case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (max a b)) (f (min a b)))

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ b ∈ [[a, b]]
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ [[a, b]] = Icc (min a b) (max a b)

pp: case h₁
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ b ≤ b

pp: case h₂
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a ≤ a

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ [[a, b]] = Icc (min a b) (max a b)

case h₁
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ b ≤ b

case h₂
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a ≤ a
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : s.PairwiseDisjoint fun a ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
this : x.1 = y.1
⊢ (fun p ↦ f p.1 p.2) y = f y.1 y.2

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c x : α
⊢ x ∈ [[a, c]] → x ∈ [[a, b]] ∪ [[b, c]]

Tactic:
simp only [mem_uIcc, mem_union]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c x : α
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : s.PairwiseDisjoint fun a ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ (fun p ↦ f p.1 p.2) y ∈ f y.1 '' t

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : s.PairwiseDisjoint fun a ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ (fun p ↦ f p.1 p.2) y ∈ f y.1 '' t
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
this : x.2 = y.2
⊢ (fun p ↦ f p.1 p.2) y = (fun a ↦ f a y.2) y.1

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ (∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) → ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]

Tactic:
]

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ (∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) → ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ (fun p ↦ f p.1 p.2) y ∈ (fun a ↦ f a y.2) '' s

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ (fun p ↦ f p.1 p.2) y ∈ (fun a ↦ f a y.2) '' s
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b

Tactic:
]

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ⊆ f i
hfj : t ⊆ f j
ht : t.Nonempty
⊢ t.Nonempty

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ⊆ f i
hfj : t ⊆ f j
ht : t.Nonempty
⊢ t.Nonempty
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ Ι b a) b ↔ x ∈ (fun b ↦ Ι b a) c
⊢ b = c

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ Ι b a) b ↔ x ∈ (fun b ↦ Ι b a) c
⊢ b = c
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → Set α
h : ¬univ.Pairwise (Disjoint on f)
⊢ ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_4
f : ι → Set α
h : ¬univ.Pairwise (Disjoint on f)
⊢ ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬univ.Pairwise (Disjoint on f)
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬univ.Pairwise (Disjoint on f)
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ Ι a c = Ι a c

pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ b ∈ [[c, a]]

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ b ∈ [[c, a]]
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ b ∈ [[a, c]]

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ b ∈ [[a, c]]
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a✝ b c✝ a c : α
h : b ∈ Icc a c
hac : a ≤ c
⊢ Ι a b ∪ Ι b c = Ι a c

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a✝ b c✝ a c : α
h : b ∈ Icc a c
hac : a ≤ c
⊢ Ι a b ∪ Ι b c = Ι a c
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a✝ b c✝ a c : α
h : b ∈ Icc a c
hac : a ≤ c
⊢ Ioc a c = Ioc a c

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ Ioo a b = Ioo a b

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ Ioo b a = Ioo b a

Tactic:
]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
S T : A
⊢ S ≤ T ∧ S ≠ T ↔ S ≤ T ∧ S ≠ T

Tactic:
]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
S T : A
⊢ ↑S ⊂ ↑T ↔ S < T

Tactic:
rw [ssubset_iff_subset_ne, lt_iff_le_and_ne, coe_subset_coe, SetLike.coe_ne_coe]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
p q : A
⊢ (p ≤ q ∧ ∃ x, x ∈ q ∧ ¬x ∈ p) ↔ p ≤ q ∧ ∃ x, x ∈ q ∧ ¬x ∈ p

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
⊢ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Icc x y ⊆ s

Tactic:
]

Goal state after:
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
⊢ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Icc x y ⊆ s
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: case inr
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ insert x (insert y (Ioo x y)) ⊆ s

Tactic:
]

Goal state after:
case inr
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ insert x (insert y (Ioo x y)) ⊆ s
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ Icc (e x) (e y) = Icc (e x) (e y)

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ Ico (e x) (e y) = Ico (e x) (e y)

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ Ioc (e x) (e y) = Ioc (e x) (e y)

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ Ioo (e x) (e y) = Ioo (e x) (e y)

Tactic:
]

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
this : Std.Symm fun a b ↦ r a b ∨ r b a
⊢ ((s.Pairwise fun x y ↦ r x y ∨ r y x) ∧
      (t.Pairwise fun x y ↦ r x y ∨ r y x) ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a) ↔
    (s.Pairwise fun x y ↦ r x y ∨ r y x) ∧
      (t.Pairwise fun x y ↦ r x y ∨ r y x) ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a

Tactic:
]

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) (f '' univ)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) (f '' univ)
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
a : α
⊢ (Icc a a).OrdConnected

Tactic:
]

Goal state after:
α : Type u_3
inst✝ : PartialOrder α
a : α
⊢ (Icc a a).OrdConnected
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : s.OrdConnected
⊢ (⇑(↑e).symm ⁻¹' s).OrdConnected

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : s.OrdConnected
⊢ (⇑(↑e).symm ⁻¹' s).OrdConnected
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxChain r c
t : Set β
ht : IsChain s t
hf : ⇑e '' c ⊆ t
⊢ c = ⇑e.symm '' t

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxChain r c
t : Set β
ht : IsChain s t
hf : ⇑e '' c ⊆ t
⊢ c = ⇑e.symm '' t
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : ∃ x ∈ s, φ x = b
b' : β
hb' : ∃ x ∈ s, φ x = b'
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : ∃ x ∈ s, φ x = b
b' : β
hb' : ∃ x ∈ s, φ x = b'
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)
⊢ IsChain r (SuccChain r s)

Tactic:
]

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)
⊢ IsChain r (SuccChain r s)