mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ u ⊆ (powersetCard n.succ u).biUnion id

Tactic:
subset_iff

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ ∀ ⦃x : α⦄, x ∈ u → x ∈ (powersetCard n.succ u).biUnion id
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f ({x ∈ s | f x ∈ t}) = t
⊢ {x ∈ s | f x ∈ t} ⊆ s ∧ n = n

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
⊢ ↑(s.sup' H f) = s.sup (WithBot.some ∘ f)

Tactic:
rw [sup', WithBot.coe_unbot]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case singleton
α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
a✝ : ι
⊢ a ⊓ {a✝}.sup' ⋯ f = {a✝}.sup' ⋯ fun i ↦ a ⊓ f i

Tactic:
simp

Goal state after:
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case h₁
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
i : ι
⊢ (fun i ↦ f ⟨i, ⋯⟩) i ∈ range f

Tactic:
simp

Goal state after:
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case h₂
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
i : Subtype p
⊢ f i ∈ range fun i ↦ f ⟨i, ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝² : DecidableEq α
inst✝¹ : Fintype (PLift ι)
f : ι → Set α
inst✝ : (i : ι) → Fintype ↑(f i)
⊢ ∀ (x : α), (x ∈ Finset.univ.biUnion fun i ↦ (f i.down).toFinset) ↔ x ∈ ⋃ i, f i

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
inst✝¹ : DecidableEq α
ι : Type u_1
s : Set ι
inst✝ : Fintype ↑s
t : ι → Set α
H : (i : ι) → i ∈ s → Fintype ↑(t i)
this : (i : ↥s.toFinset) → Fintype ↑(t ↑i)
x : α
⊢ (x ∈ s.toFinset.attach.biUnion fun x ↦ (t ↑x).toFinset) ↔ x ∈ ⋃ x ∈ s, t x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
inst✝² : DecidableEq α
ι : Type u_1
s : Set ι
inst✝¹ : Fintype ↑s
t : ι → Set α
inst✝ : (i : ι) → Fintype ↑(t i)
⊢ ∀ (x : α), (x ∈ s.toFinset.biUnion fun x ↦ (t x).toFinset) ↔ x ∈ ⋃ x ∈ s, t x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : β → Set α
s : Set β
hs : s.PairwiseDisjoint f
⊢ (∀ (i : β), (⋃ (_ : i ∈ s), f i).Finite) ∧ {i | (⋃ (_ : i ∈ s), f i).Nonempty}.Finite ↔
    (∀ i ∈ s, (f i).Finite) ∧ {i | i ∈ s ∧ (f i).Nonempty}.Finite

Tactic:
simp

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

Goal state before:
pp: ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∉ s
⊢ ↑⊥ ≤ ↑(f j)

Tactic:
simp

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

Goal state before:
pp: case neg
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
i : ι
h : i ∉ s
⊢ ⨅ i ∈ s, ↑(f i) ≤ ↑(⨅ (_ : i ∈ s), f i)

Tactic:
simp [iInf_neg h]

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ (⋃ i ∈ a, s i).Infinite

Tactic:
by
  rw [biUnion_eq_iUnion]
  have _ := ha.to_subtype
  exact infinite_iUnion fun ⟨i,hi⟩ ⟨j,hj⟩ hij ↦ by simp [hs hi hj hij]

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
⊢ (fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩) ((fun a ↦ untopD ⊤ (map Subtype.val a)) ⊤) = ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a✝ b✝ : WithTop { a // a ≠ ⊤ }
a b : { a // a ≠ ⊤ }
⊢ { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩, left_inv := ⋯,
          right_inv := ⋯ }
        ↑a ≤
      { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ↑b ↔
    ↑a ≤ ↑b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a✝ b a : WithTop { a // a ≠ ⊤ }
⊢ { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩, left_inv := ⋯,
          right_inv := ⋯ }
        a ≤
      { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⊤ ↔
    a ≤ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
a✝ : WithTop (WithBot α)
⊢ (f.comp g).withTopWithBot a✝ = (f.withTopWithBot.comp g.withTopWithBot) a✝

Tactic:
simp

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

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ⊤ ∈ Ioi ↑a ↔ ⊤ ∈ some '' Ioi a ∪ {⊤}

Tactic:
simp

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

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
a a✝ : α
⊢ ↑a✝ ∈ Ioi ↑a ↔ ↑a✝ ∈ some '' Ioi a ∪ {⊤}

Tactic:
simp

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

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ⊤ ∈ Ici ↑a ↔ ⊤ ∈ some '' Ici a ∪ {⊤}

Tactic:
simp

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

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
a a✝ : α
⊢ ↑a✝ ∈ Ici ↑a ↔ ↑a✝ ∈ some '' Ici a ∪ {⊤}

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: case empty
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
hs : ↑∅ ⊆ ⋃ i, f i
⊢ ∃ i, ↑∅ ⊆ f i

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
s : Finset ι
h : s.Nonempty
h' : (image f s).Nonempty
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
s : Finset ι
h : s.Nonempty
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
s : Set ι
h : s.Nonempty
hs : s.Finite
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set ι
a : α
f : ι → α
h : s.Nonempty
hs : s.Finite
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun i j ↦ f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ i ∈ c, f i
⊢ ∃ i ∈ c, ↑s ⊆ f i

Tactic:
by
  rw [Set.biUnion_eq_iUnion] at hs
  have := hn.coe_sort
  simpa using (directed_comp.2 hc.directed_val).exists_mem_subset_of_finset_subset_biUnion hs

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this✝ : Nonempty ↑s
i : ι
h : i ∈ s
this : f i ∈ f '' s
⊢ g ↑⟨f i, this⟩ = g (f ↑⟨i, h⟩)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
b : ι
⊢ b ∈ {b}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: ι : Type u_5
s : Set ι
x : ι
hx : x ∈ s
⊢ ⟨x, ⋯⟩ ∈ {⟨x, hx⟩}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
a : α
s : α → β
⊢ ⨆ x ∈ {a}, s x = s a

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
o : Option α
f : α → β
⊢ ⨆ x ∈ o.toFinset, f x = ⨆ x ∈ o, f x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ ↑(∅.preimage f ⋯) = ↑∅

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype β
hf : InjOn f (f ⁻¹' ↑univ)
⊢ ↑(univ.preimage f hf) = ↑univ

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s t : Finset β
hs : InjOn f (f ⁻¹' ↑s)
ht : InjOn f (f ⁻¹' ↑t)
⊢ ↑((s ∩ t).preimage f ⋯) = ↑(s.preimage f hs ∩ t.preimage f ht)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s t : Finset β
hst : InjOn f (f ⁻¹' ↑(s ∪ t))
⊢ ↑((s ∪ t).preimage f hst) = ↑(s.preimage f ⋯ ∪ t.preimage f ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
s : Finset β
hfc : InjOn f (f ⁻¹' ↑sᶜ)
hf : InjOn f (f ⁻¹' ↑s)
⊢ ↑(sᶜ.preimage f hfc) = ↑(s.preimage f hf)ᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx : x.snd ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) (⋯ ▸ ⟨x.1, b⟩.snd)
⊢ (Embedding.sigmaMk ⟨x.1, b⟩.fst) x.snd = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
s : Finset (α ⊕ β)
x : α
⊢ x ∈ s.preimage Sum.inl ⋯ ↔ x ∈ s.toLeft

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ #(map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd)) = #(f (h ▸ a.snd) b.snd)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ #∅ = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
s : Finset (α ⊕ β)
x : β
⊢ x ∈ s.preimage Sum.inr ⋯ ↔ x ∈ s.toRight

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
e : α ≃ β
s : Finset β
b : ↥s
⊢ e.symm ↑b ∈ s.preimage ⇑e ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
e : α ≃ β
s : Finset β
x✝ : ↥(s.preimage ⇑e ⋯)
⊢ (fun b ↦ ⟨e.symm ↑b, ⋯⟩) ((fun a ↦ ⟨e ↑a, ⋯⟩) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
e : α ≃ β
s : Finset β
x✝ : ↥s
⊢ (fun a ↦ ⟨e ↑a, ⋯⟩) ((fun b ↦ ⟨e.symm ↑b, ⋯⟩) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s : Finset ι
i : ι
⊢ MaximalFor (fun x ↦ x ∈ {i}) f i

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n ↦ Nat.recOn n ⋯.choose fun x a ↦ ⋯.choose
hf : ∀ (n : ℕ), f n ∈ s
⊢ s.Infinite

Tactic:
exact infinite_of_injective_forall_mem
    (strictMono_nat_of_lt_succ fun n => (h _).choose_spec.2).injective hf

Goal state after:
Module: Mathlib.Order.Minimal

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: case inr
α : Type u_2
x✝ : α
inst✝ : Preorder α
x : α
h : {x}.Subsingleton
⊢ Minimal (fun x_1 ↦ x_1 ∈ {x}) x✝ ↔ x✝ ∈ {x}

Tactic:
simp

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
⊢ t = range (Subtype.val ∘ ⇑f)

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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:
simp

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.Ico a b)
x✝ : α
⊢ x✝ ∈ Ico a b ↔ x✝ ∈ Set.Ico a b

Tactic:
simp

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.Ioo a b)
x✝ : α
⊢ x✝ ∈ Ioo a b ↔ x✝ ∈ Set.Ioo a b

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : LocallyFiniteOrderTop α
inst✝² : One α
inst✝¹ : IsBotOneClass α
inst✝ : Fintype α
a✝ : α
⊢ a✝ ∈ Ici 1 ↔ a✝ ∈ univ

Tactic:
simp

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

Goal state before:
pp: a b : ℕ
⊢ a ∈ Ioc b (b + 1) ↔ a = b + 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x✝ : α
⊢ x✝ ∈ Finset.Icc a b ↔ x✝ ∈ Icc a b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x✝ : α
⊢ x✝ ∈ Finset.Ico a b ↔ x✝ ∈ Ico a b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x✝ : α
⊢ x✝ ∈ Finset.Ioo a b ↔ x✝ ∈ Ioo a b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ (⨆ (_ : 0 < n + 1), u 0) ⊔ ⨆ i, ⨆ (_ : i + 1 < n + 1), u (i + 1) = u 0 ⊔ ⨆ k, ⨆ (_ : k < n), u (k + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
f : ℕ → α
hf : StrictAnti f
n : ℕ
⊢ n < n + 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
⊢ ⊤ ∉ Finset.map Embedding.coeWithTop s

Tactic:
simp

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

Goal state before:
pp: case top.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
⊢ (⊤ ∈
      match ⊤, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ ⊤ ∧ ⊤ ≤ ⊤

Tactic:
simp

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

Goal state before:
pp: case top.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ ↑a✝ ∧ ↑a✝ ≤ ⊤

Tactic:
simp

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

Goal state before:
pp: case top.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ⊤, ↑a✝ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ ⊤ ∧ ⊤ ≤ ↑a✝

Tactic:
simp

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

Goal state before:
pp: case top.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ↑a✝¹ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ ↑a✝ ∧ ↑a✝ ≤ ↑a✝¹

Tactic:
simp

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

Goal state before:
pp: case coe.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ↑a✝, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝ ≤ ⊤ ∧ ⊤ ≤ ⊤

Tactic:
simp

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

Goal state before:
pp: case coe.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝¹, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝¹ ≤ ↑a✝ ∧ ↑a✝ ≤ ⊤

Tactic:
simp

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

Goal state before:
pp: case coe.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (⊤ ∈
      match ↑a✝¹, ↑a✝ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝¹ ≤ ⊤ ∧ ⊤ ≤ ↑a✝

Tactic:
simp

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

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝² a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝², ↑a✝¹ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝² ≤ ↑a✝ ∧ ↑a✝ ≤ ↑a✝¹

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case top.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ ↑a✝ ∧ ↑a✝ < ⊤

Tactic:
simp

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

Goal state before:
pp: case top.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ ⊤ ∧ ⊤ < ↑a✝

Tactic:
simp

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

Goal state before:
pp: case top.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ↑a✝¹ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ ↑a✝ ∧ ↑a✝ < ↑a✝¹

Tactic:
simp

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

Goal state before:
pp: case coe.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝ ≤ ⊤ ∧ ⊤ < ⊤

Tactic:
simp

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

Goal state before:
pp: case coe.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝¹, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝¹ ≤ ↑a✝ ∧ ↑a✝ < ⊤

Tactic:
simp

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

Goal state before:
pp: case coe.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (⊤ ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝¹ ≤ ⊤ ∧ ⊤ < ↑a✝

Tactic:
simp

Goal state after: