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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictAntiOn g (f '' ofPred Q)
h : MinimalFor Q (g ∘ f) i
⊢ MaximalFor Q f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
P : ι → Prop
f : ι → α
hP : ∃ i, P i
⊢ ∃ i, MinimalFor P f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
P : α → Prop
a : α
ha : P a
⊢ ∃ b, b ≤ a ∧ Minimal P b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : α → Prop
x y : α
inst✝ : PartialOrder α
hy : P y
hP : ∀ ⦃x : α⦄, P x → y ≤ x
⊢ x = y → Minimal P x

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
t : Set β
f : α → β
inst✝ : Infinite α
hf : ∀ (a : α), f a ∈ t
ht : t.Finite
⊢ ∃ a b, a < b ∧ f a = f b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
⊢ Minimal P x ↔ Minimal Q x

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
a : α
ha : Maximal (fun x ↦ x ∈ s) a
this : IsTop a
⊢ {a}.Subsingleton ∧ IsCofinal {a}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → t ⊆ s → P s
hs : P s
h : ¬Minimal P s
⊢ ∃ x, x ∈ s ∧ P (s \ {x})

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ (x : α), ¬x ∈ s → ¬P (insert x s)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
⊢ f = g → Set.range ⇑f = Set.range ⇑g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
hs : P s
h : ¬Maximal P s
⊢ ∃ x, ¬x ∈ s ∧ P (insert x s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
x : α
s : Set α
inst✝ : Preorder α
h : s.Subsingleton
⊢ Minimal (fun x ↦ x ∈ s) x ↔ x ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
h : Set.range ⇑f = Set.range ⇑g
ef : ↑Set.univ ≃o ↑(⇑f '' Set.univ) := StrictMonoOn.orderIso (⇑f) Set.univ ⋯
eg : ↑Set.univ ≃o ↑(⇑g '' Set.univ) := StrictMonoOn.orderIso (⇑g) Set.univ ⋯
⊢ ⇑f '' Set.univ = ⇑g '' Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun x ↦ x ∈ s) x
⊢ Minimal (fun x ↦ x ∈ f '' s) (f x)

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
h : Set.range ⇑f = Set.range ⇑g
ef : ↑Set.univ ≃o ↑(⇑f '' Set.univ) := StrictMonoOn.orderIso (⇑f) Set.univ ⋯
eg : ↑Set.univ ≃o ↑(⇑g '' Set.univ) := StrictMonoOn.orderIso (⇑g) Set.univ ⋯
⊢ ∀ {a b : ↑(⇑f '' Set.univ)}, (Equiv.setCongr ⋯) a ≤ (Equiv.setCongr ⋯) b ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
h : Set.range ⇑f = Set.range ⇑g
ef : ↑Set.univ ≃o ↑(⇑f '' Set.univ) := StrictMonoOn.orderIso (⇑f) Set.univ ⋯
eg : ↑Set.univ ≃o ↑(⇑g '' Set.univ) := StrictMonoOn.orderIso (⇑g) Set.univ ⋯
i : ↑(⇑f '' Set.univ) ≃o ↑(⇑g '' Set.univ) :=
  let __spread.0 := Equiv.setCongr ⋯;
  { toEquiv := __spread.0, map_rel_iff' := ⋯ }
⊢ (ef.trans i).trans eg.symm = OrderIso.refl ↑Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
a : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
⊢ Minimal (fun x ↦ x ∈ f '' s) (f a) ↔ Minimal (fun x ↦ x ∈ s) a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
⊢ f '' {x | Minimal P x} = {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ↪o β
hx : Minimal (fun x ↦ x ∈ s) x
⊢ ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
⊢ Set.range ⇑f = Set.range ⇑g ↔ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
a : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ↪o β
ha : a ∈ s
⊢ ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α →o β
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ f = g → Set.range ⇑f = Set.range ⇑g

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α →o β
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
h : Set.range ⇑f = Set.range ⇑g
x✝ : α
⊢ Set.range ⇑(OrderEmbedding.ofStrictMono ⇑f ⋯) = Set.range ⇑(OrderEmbedding.ofStrictMono ⇑g ⋯)

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α →o β
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ Set.range ⇑f = Set.range ⇑g ↔ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
⊢ Minimal (fun x ↦ x ∈ t ∩ range ⇑f) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝¹ : LinearOrder α
inst✝ : Finite α
f : α →o α
hf : Function.Injective ⇑f
⊢ Set.range ⇑f = Set.range ⇑id

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
ht : t ⊆ range ⇑f
⊢ Minimal (fun x ↦ x ∈ t) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ↪o β
⊢ ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ↪o β
t : Set β
hts : t ⊆ ⇑f '' s
⊢ x ∈ s ∩ ⇑f ⁻¹' {y | Minimal (fun x ↦ x ∈ t) y} ↔ Minimal (fun x ↦ x ∈ s ∩ ⇑f ⁻¹' t) x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
⊢ ∀ ⦃x y : α⦄, ?m.25 x → ?m.25 y → (f x ≤ f y ↔ x ≤ y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
⊢ ⇑f '' {x | Minimal P x} = {x | Minimal (fun x ↦ P (f.symm x)) x}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
f : ↑s ≃o ↑t
hx : Minimal (fun x ↦ x ∈ s) x
⊢ Minimal (fun x ↦ x ∈ t) ↑(f ⟨x, ⋯⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ico a b ↔ a ≤ x ∧ x < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioc a b ↔ a < x ∧ x ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioo a b ↔ a < x ∧ x < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ici a ↔ a ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ioi a ↔ a < x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ Iic b ↔ x ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ Iio b ↔ x < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc a b = 0 ↔ ¬a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ico a b = 0 ↔ ¬a < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ioc a b = 0 ↔ ¬a < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DenselyOrdered α
⊢ Ioo a b = 0 ↔ ¬a < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Ico a a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Ioc a a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Ioo a a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hca : c ≤ a
⊢ filter (fun x ↦ x < c) (Ico a b) = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hbc : b ≤ c
⊢ filter (fun x ↦ x < c) (Ico a b) = Ico a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hcb : c ≤ b
⊢ filter (fun x ↦ x < c) (Ico a b) = Ico a c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ c ≤ x
hca : c ≤ a
⊢ filter (fun x ↦ c ≤ x) (Ico a b) = Ico a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ b ≤ x
⊢ filter (fun x ↦ b ≤ x) (Ico a b) = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ c ≤ x
hac : a ≤ c
⊢ filter (fun x ↦ c ≤ x) (Ico a b) = Ico c b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Icc a a = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ b ::ₘ Ico a b = Icc a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ a ::ₘ Ioo a b = Ico a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h : b ≤ c
a✝ : α
hab : a✝ ∈ Ico a b
hbc : a✝ ∈ Ico c d
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ x ≤ a
hab : a < b
⊢ filter (fun x ↦ x ≤ a) (Ico a b) = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ico a b + Ico b c = Ico a c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ filter (fun x ↦ x < c) (Ico a b) = Ico a (min b c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ filter (fun x ↦ c ≤ x) (Ico a b) = Ico (max a c) b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a b - Ico a c = Ico (max a c) b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a b - Ico c b = Ico a (min b c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
finsetIcc finsetIco finsetIoc finsetIoo : α → α → Finset α
finset_mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ x ≤ a ∧ b ≤ x
finset_mem_Ico : ∀ (a b x : α), x ∈ finsetIco a b ↔ x ≤ a ∧ b < x
finset_mem_Ioc : ∀ (a b x : α), x ∈ finsetIoc a b ↔ x < a ∧ b ≤ x
finset_mem_Ioo : ∀ (a b x : α), x ∈ finsetIoo a b ↔ x < a ∧ b < x
⊢ ∀ (a b x : α), x ∈ swap finsetIcc a b ↔ a ≤ x ∧ x ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
finsetIcc finsetIco finsetIoc finsetIoo : α → α → Finset α
finset_mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ x ≤ a ∧ b ≤ x
finset_mem_Ico : ∀ (a b x : α), x ∈ finsetIco a b ↔ x ≤ a ∧ b < x
finset_mem_Ioc : ∀ (a b x : α), x ∈ finsetIoc a b ↔ x < a ∧ b ≤ x
finset_mem_Ioo : ∀ (a b x : α), x ∈ finsetIoo a b ↔ x < a ∧ b < x
⊢ ∀ (a b x : α), x ∈ swap finsetIoc a b ↔ a ≤ x ∧ x < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
finsetIcc finsetIco finsetIoc finsetIoo : α → α → Finset α
finset_mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ x ≤ a ∧ b ≤ x
finset_mem_Ico : ∀ (a b x : α), x ∈ finsetIco a b ↔ x ≤ a ∧ b < x
finset_mem_Ioc : ∀ (a b x : α), x ∈ finsetIoc a b ↔ x < a ∧ b ≤ x
finset_mem_Ioo : ∀ (a b x : α), x ∈ finsetIoo a b ↔ x < a ∧ b < x
⊢ ∀ (a b x : α), x ∈ swap finsetIco a b ↔ a < x ∧ x ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
finsetIcc finsetIco finsetIoc finsetIoo : α → α → Finset α
finset_mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ x ≤ a ∧ b ≤ x
finset_mem_Ico : ∀ (a b x : α), x ∈ finsetIco a b ↔ x ≤ a ∧ b < x
finset_mem_Ioc : ∀ (a b x : α), x ∈ finsetIoc a b ↔ x < a ∧ b ≤ x
finset_mem_Ioo : ∀ (a b x : α), x ∈ finsetIoo a b ↔ x < a ∧ b < x
⊢ ∀ (a b x : α), x ∈ swap finsetIoo a b ↔ a < x ∧ x < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | ¬b ≤ x} ↔ a ≤ x ∧ x < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ { val := ↑(List.range' a (b + 1 - a)), nodup := ⋯ } ↔ a ≤ x ∧ x ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ { val := ↑(List.range' a (b - a)), nodup := ⋯ } ↔ a ≤ x ∧ x < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | ¬x ≤ a} ↔ a < x ∧ x ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ { val := ↑(List.range' (a + 1) (b - a)), nodup := ⋯ } ↔ a < x ∧ x ≤ b

Tactic:
by

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

Goal state before:
pp: s : Set ℕ
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅

Tactic:
by

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

Goal state before:
pp: ⊢ sInf ∅ = 0

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℕ
⊢ iInf f = 0

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
h : IsEmpty ι
⊢ ⨅ x, 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ { val := ↑(List.range' (a + 1) (b - a - 1)), nodup := ⋯ } ↔ a < x ∧ x < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | ¬x ≤ a ∧ ¬b ≤ x} ↔ a < x ∧ x < b

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
h : Nonempty ι
⊢ (0 ∈ range fun x ↦ 0) ∨ (range fun x ↦ 0) = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b c : ℕ
⊢ Unique ↥(Iic 0)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a : ℕ
⊢ Iio a = range a

Tactic:
by

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

Goal state before:
pp: s : Set ℕ
h : s.Nonempty
⊢ sInf s ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | x ≠ b} ↔ a ≤ x ∧ x < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a : ℕ
⊢ Ico 0 a = range a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ range n = Icc 0 (n - 1)

Tactic:
by

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

Goal state before:
pp: s : Set ℕ
m : ℕ
hm : m < sInf s
⊢ m ∉ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: n : ℕ
⊢ range (n + 1) = Icc 0 n

Tactic:
by

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

Goal state before:
pp: s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ sInf s ≤ m

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | a ≠ x} ↔ a < x ∧ x ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: n : ℕ
⊢ range (n + 1) = Iic n

Tactic:
by

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

Goal state before:
pp: s : Set ℕ
h : 0 < sInf s
⊢ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | a ≠ x ∧ x ≠ b} ↔ a < x ∧ x < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b : ℕ
⊢ max a b + 1 - min a b = (↑b - ↑a).natAbs + 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
⊢ x ∈ {x ∈ finsetIci a | ¬x ≤ a} ↔ a < x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: b : ℕ
⊢ #(Iic b) = b + 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
⊢ x ∈ {x ∈ finsetIci a | a ≠ x} ↔ a < x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Icc a b ↔ x ≤ b ∧ a ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ico a b ↔ x < b ∧ a ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioc a b ↔ x ≤ b ∧ a < x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: b : ℕ
⊢ #(Iio b) = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioo a b ↔ x < b ∧ a < x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a : ℕ
⊢ Ico a (a + 1) = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Set.Icc a b)
x✝ : α
⊢ x✝ ∈ Icc a b ↔ x✝ ∈ Set.Icc a b

Tactic:
by

Goal state after: