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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
⊢ s.Finite

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : Finite α
inst✝ : Std.Refl r
⊢ WellQuasiOrdered r

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
⊢ WellQuasiOrdered r ↔ ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
⊢ WellQuasiOrdered fun a b ↦ r a.1 b.1 ∧ s a.2 b.2

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a b x : WithTop α
⊢ (x ∈
      match a, b with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    a < x ∧ x ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ a ∈ Ico a b ↔ a < b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ b ∈ Ioc a b ↔ a < b

Tactic:
by

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

Goal state before:
pp: P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ P n

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ioc a₁ b₁ ⊆ Ioc a₂ b₂

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ioo a₁ b₁ ⊆ Ioo a₂ b₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝¹ : Fintype ι
this✝ : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
this : ∀ (s : Finset ι) (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ WellQuasiOrdered fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
by

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

Goal state before:
pp: P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
⊢ P n

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : a₁ < a₂
⊢ Ico a₂ b ⊆ Ioo a₁ b

Tactic:
by

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

Goal state before:
pp: P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n : ℕ
⊢ P n

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Ioc a b₁ ⊆ Ioo a b₂

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
k : ℕ
hk : 1 < k
P : M → Prop
hmul : ∀ (x y : M), P x → P (x * y) ∨ P (y * x)
hpow : ∀ (x : M), P (x ^ k) → P x
n : ℕ
ih : ∀ (x : M), P (x ^ (n + 1)) → P x
x : M
hx : P (x ^ n)
h : P (x ^ n * x)
⊢ P (x ^ (n + 1))

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
k : ℕ
hk : 1 < k
P : M → Prop
hmul : ∀ (x y : M), P x → P (x * y) ∨ P (y * x)
hpow : ∀ (x : M), P (x ^ k) → P x
n : ℕ
ih : ∀ (x : M), P (x ^ (n + 1)) → P x
x : M
hx : P (x ^ n)
h : P (x * x ^ n)
⊢ P (x ^ (n + 1))

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Icc a b₁ ⊆ Ico a b₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
⊢ ∀ {a b : { x // x ∈ s }},
    r ({ toFun := Subtype.val, inj' := ⋯ } a) ({ toFun := Subtype.val, inj' := ⋯ } b) ∧
        { toFun := Subtype.val, inj' := ⋯ } a ∈ s ∧ { toFun := Subtype.val, inj' := ⋯ } b ∈ s ↔
      Subrel r (fun x ↦ x ∈ s) a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
⊢ s.WellFoundedOn r ↔ WellFounded fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
⊢ univ.WellFoundedOn r ↔ WellFounded r

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ico a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
⊢ (range f).WellFoundedOn r ↔ WellFounded (r on f)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ioc a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
s : Set β
⊢ (f '' s).WellFoundedOn r ↔ s.WellFoundedOn (r on f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a b x : WithTop α
⊢ (x ∈
      match a, b with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    a < x ∧ x < b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ico a b ⊆ Icc a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α), x ∈ map f.symm.toEmbedding (Icc (f a) (f b)) ↔ a ≤ x ∧ x ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
⊢ P x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α), x ∈ map f.symm.toEmbedding (Ico (f a) (f b)) ↔ a ≤ x ∧ x < b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Icc a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α), x ∈ map f.symm.toEmbedding (Ioc (f a) (f b)) ↔ a < x ∧ x ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r r' : α → α → Prop
s t : Set α
h : t.WellFoundedOn r'
hle : r ≤ r'
hst : s ⊆ t
⊢ s.WellFoundedOn r

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α), x ∈ map f.symm.toEmbedding (Ioo (f a) (f b)) ↔ a < x ∧ x < b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrderTop β
f : α ≃o β
⊢ ∀ (a x : α), x ∈ map f.symm.toEmbedding (Ici (f a)) ↔ a ≤ x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrderTop β
f : α ≃o β
⊢ ∀ (a x : α), x ∈ map f.symm.toEmbedding (Ioi (f a)) ↔ a < x

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
⊢ WellQuasiOrdered fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Icc ↑a ↑b) ↔ a ≤ x ∧ x ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
⊢ WellQuasiOrdered r ↔ WellQuasiOrdered s

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_6
r : α → α → Prop
a : α
⊢ Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Ico ↑a ↑b) ↔ a ≤ x ∧ x < b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r
tfae_2_to_3 : {b | ReflTransGen r b a}.WellFoundedOn r → {b | TransGen r b a}.WellFoundedOn r
⊢ {b | TransGen r b a}.WellFoundedOn r → Acc r a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Ioc ↑a ↑b) ↔ a < x ∧ x ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
h : WellQuasiOrdered r
f : r →r s
hf : Function.Surjective ⇑f
seq : ℕ → β
w✝¹ w✝ : ℕ
hle : w✝¹ < w✝
hr : r ((Function.surjInv hf ∘ seq) w✝¹) ((Function.surjInv hf ∘ seq) w✝)
⊢ s (seq w✝¹) (seq w✝)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
h : WellQuasiOrdered r
f : r →r s
hf : Function.Surjective ⇑f
⊢ WellQuasiOrdered s

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_6
r : α → α → Prop
a : α
⊢ [Acc r a, {b | ReflTransGen r b a}.WellFoundedOn r, {b | TransGen r b a}.WellFoundedOn r].TFAE

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Ioo ↑a ↑b) ↔ a < x ∧ x < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : LE α
inst✝ : LE β
f : α ≃o β
⊢ WellQuasiOrderedLE α ↔ WellQuasiOrderedLE β

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a x : Subtype p
⊢ x ∈ Finset.subtype p (Ici ↑a) ↔ a ≤ x

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a x : Subtype p
⊢ x ∈ Finset.subtype p (Ioi ↑a) ↔ a < x

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a b : α
⊢ ¬a < b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b c : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidablePred fun x ↦ x < c
hcb : c ≤ b
⊢ {x ∈ Ico a b | x < c} = Ico a c

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Preorder α
inst✝ : WellQuasiOrderedLE α
⊢ WellFoundedLT α

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Preorder α
inst✝ : WellQuasiOrderedLE α
⊢ WellFoundedLT α

Tactic:
by
  rw [WellFoundedLT, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]
  refine ⟨fun f ↦ ?_⟩
  obtain ⟨a, b, h, hf⟩ := wellQuasiOrdered_le f
  exact (f.map_rel_iff.2 h).not_ge hf

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

Goal state before:
pp: α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ c ≤ x
hac : a ≤ c
⊢ {x ∈ Ico a b | c ≤ x} = Ico c b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Icc a b) = Icc ↑a ↑b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a < j ∧ j < b
⊢ {j | a < j ∧ j < b} = Ioo a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
⊢ WellFounded fun a b ↦ r a b ∧ ¬r b a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a < j ∧ j ≤ b
⊢ {j | a < j ∧ j ≤ b} = Ioc a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ s.WellFoundedOn r ↔ ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a ≤ j ∧ j < b
⊢ {j | a ≤ j ∧ j < b} = Ico a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Ico a b) = Ico ↑a ↑b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a ≤ j ∧ j ≤ b
⊢ {j | a ≤ j ∧ j ≤ b} = Icc a b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Ioi a = ∅ ↔ IsMax a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ (Ioi a).Nonempty ↔ ¬IsMax a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : OrderBot α
inst✝ : Fintype α
⊢ Ici ⊥ = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Ici a ⊆ Ici b ↔ b ≤ a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Ici a ⊂ Ici b ↔ b < a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
h : a ≤ b
⊢ Ioi b ⊆ Ioi a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
h : a < b
⊢ Ioi b ⊂ Ioi a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Icc a b ⊆ Ici a

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : s.WellFoundedOn r
ht : t.WellFoundedOn r
⊢ (s ∪ t).WellFoundedOn r

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Ico a b ⊆ Ici a

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : LT α
⊢ univ.IsWF ↔ WellFoundedLT α

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Ioi a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Ioi a

Tactic:
by
  simpa [← coe_subset] using Set.Ioc_subset_Ioi_self

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
⊢ ∀ (x : α), x ∈ univ

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ioi a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ (Iio a).Nonempty ↔ ¬IsMin a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderTop α
inst✝ : Fintype α
⊢ Iic ⊤ = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Ioc a b) = Ioc ↑a ↑b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ Iic a ⊆ Iic b ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ Iic a ⊂ Iic b ↔ a < b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h : a ≤ b
⊢ Iio a ⊆ Iio b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h : a < b
⊢ Iio a ⊂ Iio b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
β : Type u_3
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : α → β
hf : Monotone f
x✝ : α
h : x✝ ∈ Iic a
⊢ x✝ ≤ a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
β : Type u_3
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : α → β
hf : Monotone f
⊢ a ∈ Iic a

Tactic:
by

Goal state after: