ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>SupSet α<VAR>SupSet β<VAR>f : ι → α × β<GOAL>(iSup f).1 = ⨆ i, (f i).1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>SupSet α<VAR>SupSet β<VAR>f : ι → α × β<GOAL>(iSup f).2 = ⨆ i, (f i).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>SupSet α<VAR>SupSet β<VAR>f : ι → α × β<GOAL>(iSup f).swap = ⨆ i, (f i).swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>SupSet α<VAR>SupSet β<VAR>f : ι → α<VAR>g : ι → β<GOAL>⨆ i, (f i, g i) = (⨆ i, f i, ⨆ i, g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>InfSet α<VAR>InfSet β<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>sInf (s ×ˢ t) = (sInf s, sInf t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SupSet α<VAR>SupSet β<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>sSup (s ×ˢ t) = (sSup s, sSup t)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>a : α<VAR>s : Set α<GOAL>a ⊔ sInf s ≤ ⨅ b ∈ s, a ⊔ b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>a : α<VAR>s : Set α<GOAL>⨆ b ∈ s, a ⊓ b ≤ a ⊓ sSup s
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>a : α<VAR>s : Set α<GOAL>sInf s ⊔ a ≤ ⨅ b ∈ s, b ⊔ a
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>a : α<VAR>s : Set α<GOAL>⨆ b ∈ s, b ⊓ a ≤ sSup s ⊓ a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f g : ι → α<GOAL>⨆ i, f i ⊓ g i ≤ (⨆ i, f i) ⊓ ⨆ i, g i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f g : ι → α<GOAL>(⨅ i, f i) ⊔ ⨅ i, g i ≤ ⨅ i, f i ⊔ g i
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>a : Set α<VAR>b : α<VAR>d : Disjoint (sSup a) b<VAR>i : α<VAR>hi : i ∈ a<GOAL>Disjoint i b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>a : Set α<VAR>b : α<VAR>d : Disjoint b (sSup a)<VAR>i : α<VAR>hi : i ∈ a<GOAL>Disjoint b i
<VAR>α : Type u_1<VAR>SupSet α<VAR>s : Set (ULift.{v, u_1} α)<GOAL>(sSup s).down = sSup (ULift.up ⁻¹' s)
<VAR>α : Type u_1<VAR>SupSet α<VAR>s : Set α<GOAL>{ down := sSup s } = sSup (ULift.down ⁻¹' s)
<VAR>α : Type u_1<VAR>InfSet α<VAR>s : Set (ULift.{v, u_1} α)<GOAL>(sInf s).down = sInf (ULift.up ⁻¹' s)
<VAR>α : Type u_1<VAR>InfSet α<VAR>s : Set α<GOAL>{ down := sInf s } = sInf (ULift.down ⁻¹' s)
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>SupSet α<VAR>f : ι → ULift.{v, u_1} α<GOAL>(⨆ i, f i).down = ⨆ i, (f i).down
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>SupSet α<VAR>f : ι → α<GOAL>{ down := ⨆ i, f i } = ⨆ i, { down := f i }
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>InfSet α<VAR>f : ι → ULift.{v, u_1} α<GOAL>(⨅ i, f i).down = ⨅ i, (f i).down
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>InfSet α<VAR>f : ι → α<GOAL>{ down := ⨅ i, f i } = ⨅ i, { down := f i }
<VAR>α : Sort u<VAR>s : Setoid α<GOAL>Quotient.mk' = Quotient.mk s
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>a : α<VAR>h : IsCoatom a<GOAL>Order.radical α ≤ a
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>β : Type u_2<VAR>CompleteLattice β<VAR>f : α ≃o β<GOAL>f (Order.radical α) = Order.radical β
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>IsCoatomic α<VAR>a : α<VAR>h : a ⊔ Order.radical α = ⊤<GOAL>a = ⊤
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>a b : α<VAR>J : Order.Ideal α<GOAL>b ∈ J ⊔ Order.Ideal.principal a ↔ ∃ j ∈ J, b ≤ j ⊔ a
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>F : Order.PFilter α<VAR>I : Order.Ideal α<VAR>hFI : Disjoint ↑F ↑I<GOAL>∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>f : ℕ → α<VAR>H : ∀ (n : ℕ), r (f n) (f (n + 1))<GOAL>⇑(RelEmbedding.natLT f H) = f
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>f : ℕ → α<VAR>H : ∀ (n : ℕ), r (f (n + 1)) (f n)<GOAL>⇑(RelEmbedding.natGT f H) = f
<VAR>α : Type u_1<VAR>a : α<VAR>r : α → α → Prop<VAR>h : ¬Acc r a<GOAL>∃ b, ¬Acc r b ∧ r b a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>x : α<GOAL>Acc r x ↔ IsEmpty { f // x ∈ Set.range ⇑f }
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>f : (fun x x_1 => x > x_1) ↪r r<VAR>k : ℕ<GOAL>¬Acc r (f k)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<GOAL>WellFounded r ↔ IsEmpty ((fun x x_1 => x > x_1) ↪r r)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>f : (fun x x_1 => x > x_1) ↪r r<GOAL>¬WellFounded r
<VAR>s : Set ℕ<VAR>Infinite ↑s<VAR>DecidablePred fun x => x ∈ s<GOAL>⇑(Nat.orderEmbeddingOfSet s) = Subtype.val ∘ Nat.Subtype.ofNat s
<VAR>s : Set ℕ<VAR>Infinite ↑s<VAR>DecidablePred fun x => x ∈ s<VAR>n : ℕ<GOAL>(Nat.orderEmbeddingOfSet s) n = ↑(Nat.Subtype.ofNat s n)
<VAR>s : Set ℕ<VAR>Infinite ↑s<VAR>dP : DecidablePred fun x => x ∈ s<VAR>n : ℕ<GOAL>(Nat.Subtype.orderIsoOfNat s) n = Nat.Subtype.ofNat s n
<VAR>s : Set ℕ<VAR>Infinite ↑s<VAR>DecidablePred fun x => x ∈ s<GOAL>Set.range ⇑(Nat.orderEmbeddingOfSet s) = s
<VAR>α : Type u_1<VAR>s t : Set α<VAR>e : ℕ → α<VAR>he : ∀ (n : ℕ), e n ∈ s ∪ t<GOAL>∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : ℕ → α<GOAL>∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsTrans α r<VAR>f : ℕ → α<GOAL>∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
<VAR>α : Type u_1<VAR>Preorder α<GOAL>(WellFounded fun x x_1 => x > x_1) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>(WellFounded fun x x_1 => x > x_1) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>h : WellFounded fun x x_1 => x > x_1<VAR>a : ℕ →o α<GOAL>iSup ⇑a = monotonicSequenceLimit a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : Thunk α<VAR>ε : Type u_3<VAR>self : Estimator a ε<VAR>e : ε<GOAL>EstimatorData.bound a e ≤ a.get
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : Thunk α<VAR>ε : Type u_3<VAR>self : Estimator a ε<VAR>e : ε<GOAL>match EstimatorData.improve a e with
| some e' => EstimatorData.bound a e < EstimatorData.bound a e'
<VAR>α : Type u_1<VAR>ε : Type u_2<VAR>Preorder α<VAR>a : Thunk α<VAR>p : α → Bool<VAR>Estimator a ε<VAR>WellFoundedGT ↑(Set.range (EstimatorData.bound a))<VAR>e : ε<VAR>r : Bool<GOAL>match Estimator.improveUntilAux a p e r with
| Except.ok e' => p (EstimatorData.bound a e') = true
<VAR>α : Type u_1<VAR>ε : Type u_2<VAR>Preorder α<VAR>a : Thunk α<VAR>p : α → Bool<VAR>Estimator a ε<VAR>WellFoundedGT ↑(Set.range (EstimatorData.bound a))<VAR>e : ε<GOAL>match Estimator.improveUntil a p e with
<VAR>α : Type u_1<VAR>Add α<VAR>a b : Thunk α<VAR>εa : Type u_3<VAR>εb : Type u_4<VAR>EstimatorData a εa<VAR>EstimatorData b εb<VAR>e : εa × εb<GOAL>EstimatorData.improve (a + b) e = match EstimatorData.improve a e.1 with | some e' => some (e', e.2) | none => match EstimatorData.improve b e.2 with | some e' => some (e.1, e') | none => none
<VAR>α : Type u_1<VAR>Add α<VAR>a b : Thunk α<VAR>εa : Type u_3<VAR>εb : Type u_4<VAR>EstimatorData a εa<VAR>EstimatorData b εb<VAR>e : εa × εb<GOAL>EstimatorData.bound (a + b) e = EstimatorData.bound a e.1 + EstimatorData.bound b e.2
<VAR>α : Type u<VAR>r : α → α → Prop<GOAL>Equivalence (EqvGen r)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<VAR>H : Quot.mk r a = Quot.mk r b<GOAL>EqvGen r a b
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<VAR>H : EqvGen r a b<GOAL>Quot.mk r a = Quot.mk r b
<VAR>p : Prop → Prop<VAR>h1 : p True<VAR>h2 : p False<VAR>a : Prop<GOAL>p a
<VAR>a : Prop<VAR>p : Prop → Prop<VAR>h1 : p True<VAR>h2 : p False<GOAL>p a
<VAR>a : Prop<GOAL>a = False ∨ a = True
<VAR>α : Type u_1<VAR>Preorder α<VAR>self : LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ LocallyFiniteOrder.finsetIcc a b ↔ a ≤ x ∧ x ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>self : LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ LocallyFiniteOrder.finsetIoc a b ↔ a < x ∧ x ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>self : LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ LocallyFiniteOrder.finsetIoo a b ↔ a < x ∧ x < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>self : LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ LocallyFiniteOrder.finsetIco a b ↔ a ≤ x ∧ x < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>self : LocallyFiniteOrderTop α<VAR>a x : α<GOAL>x ∈ LocallyFiniteOrderTop.finsetIci a ↔ a ≤ x
<VAR>α : Type u_1<VAR>Preorder α<VAR>self : LocallyFiniteOrderTop α<VAR>a x : α<GOAL>x ∈ LocallyFiniteOrderTop.finsetIoi a ↔ a < x
<VAR>α : Type u_1<VAR>Preorder α<VAR>self : LocallyFiniteOrderBot α<VAR>a x : α<GOAL>x ∈ LocallyFiniteOrderBot.finsetIio a ↔ x < a
<VAR>α : Type u_1<VAR>Preorder α<VAR>self : LocallyFiniteOrderBot α<VAR>a x : α<GOAL>x ∈ LocallyFiniteOrderBot.finsetIic a ↔ x ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ Finset.Icc a b ↔ a ≤ x ∧ x ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ Finset.Ico a b ↔ a ≤ x ∧ x < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ Finset.Ioc a b ↔ a < x ∧ x ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ Finset.Ioo a b ↔ a < x ∧ x < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>↑(Finset.Icc a b) = Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>↑(Finset.Ico a b) = Set.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>↑(Finset.Ioc a b) = Set.Ioc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>↑(Finset.Ioo a b) = Set.Ioo a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a x : α<GOAL>x ∈ Finset.Ici a ↔ a ≤ x
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a x : α<GOAL>x ∈ Finset.Ioi a ↔ a < x
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a : α<GOAL>↑(Finset.Ici a) = Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a : α<GOAL>↑(Finset.Ioi a) = Set.Ioi a
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>a x : α<GOAL>x ∈ Finset.Iic a ↔ x ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>a x : α<GOAL>x ∈ Finset.Iio a ↔ x < a
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>a : α<GOAL>↑(Finset.Iic a) = Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>a : α<GOAL>↑(Finset.Iio a) = Set.Iio a
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>OrderTop α<VAR>a : α<GOAL>Finset.Ici a = Finset.Icc a ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>OrderTop α<VAR>a : α<GOAL>Finset.Ioi a = Finset.Ioc a ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<VAR>LocallyFiniteOrder α<GOAL>Finset.Iic = Finset.Icc ⊥
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<VAR>LocallyFiniteOrder α<GOAL>Finset.Iio = Finset.Ico ⊥
<VAR>α : Type u_1<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ Finset.uIcc a b ↔ a ⊓ b ≤ x ∧ x ≤ a ⊔ b
<VAR>α : Type u_1<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>↑(Finset.uIcc a b) = Set.uIcc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Set.Icc a b).Finite
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Set.Ico a b).Finite
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Set.Ioc a b).Finite
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Set.Ioo a b).Finite
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a : α<GOAL>(Set.Ici a).Finite
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a : α<GOAL>(Set.Ioi a).Finite
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>b : α<GOAL>(Set.Iic b).Finite
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>b : α<GOAL>(Set.Iio b).Finite
<VAR>α : Type u_1<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Set.uIcc a b).Finite
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Icc (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.Icc b a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ico (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioc b a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ioc (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ico b a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ioo (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioo b a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : αᵒᵈ<GOAL>Finset.Icc (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Icc b a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : αᵒᵈ<GOAL>Finset.Ico (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ioc b a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : αᵒᵈ<GOAL>Finset.Ioc (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ico b a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : αᵒᵈ<GOAL>Finset.Ioo (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ioo b a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a : α<GOAL>Finset.Iic (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ici a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a : α<GOAL>Finset.Iio (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioi a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a : αᵒᵈ<GOAL>Finset.Ici (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Iic a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a : αᵒᵈ<GOAL>Finset.Ioi (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Iio a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>a : α<GOAL>Finset.Ici (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Iic a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>a : α<GOAL>Finset.Ioi (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Iio a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>a : αᵒᵈ<GOAL>Finset.Iic (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ici a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>a : αᵒᵈ<GOAL>Finset.Iio (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ioi a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>p q : α × β<GOAL>Finset.Icc p q = Finset.Icc p.1 q.1 ×ˢ Finset.Icc p.2 q.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>Finset.Icc (a₁, b₁) (a₂, b₂) = Finset.Icc a₁ a₂ ×ˢ Finset.Icc b₁ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>p q : α × β<GOAL>(Finset.Icc p q).card = (Finset.Icc p.1 q.1).card * (Finset.Icc p.2 q.2).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Lattice α<VAR>Lattice β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>p q : α × β<GOAL>Finset.uIcc p q = Finset.uIcc p.1 q.1 ×ˢ Finset.uIcc p.2 q.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Lattice α<VAR>Lattice β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>Finset.uIcc (a₁, b₁) (a₂, b₂) = Finset.uIcc a₁ a₂ ×ˢ Finset.uIcc b₁ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Lattice α<VAR>Lattice β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>p q : α × β<GOAL>(Finset.uIcc p q).card = (Finset.uIcc p.1 q.1).card * (Finset.uIcc p.2 q.2).card
<VAR>α : Type u_1<VAR>x : α<VAR>p : α → Prop<GOAL>(∃ a, p a ∧ ↑a = ↑x) ↔ p x
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>LocallyFiniteOrder α<VAR>a : α<GOAL>Finset.Icc ↑a ⊤ = Finset.insertNone (Finset.Ici a)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Icc ↑a ↑b = Finset.map Function.Embedding.some (Finset.Icc a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>LocallyFiniteOrder α<VAR>a : α<GOAL>Finset.Ico ↑a ⊤ = Finset.map Function.Embedding.some (Finset.Ici a)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ico ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ico a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>LocallyFiniteOrder α<VAR>a : α<GOAL>Finset.Ioc ↑a ⊤ = Finset.insertNone (Finset.Ioi a)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ioc ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ioc a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>LocallyFiniteOrder α<VAR>a : α<GOAL>Finset.Ioo ↑a ⊤ = Finset.map Function.Embedding.some (Finset.Ioi a)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ioo ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ioo a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>LocallyFiniteOrder α<VAR>b : α<GOAL>Finset.Icc ⊥ ↑b = Finset.insertNone (Finset.Iic b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Icc ↑a ↑b = Finset.map Function.Embedding.some (Finset.Icc a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>LocallyFiniteOrder α<VAR>b : α<GOAL>Finset.Ico ⊥ ↑b = Finset.insertNone (Finset.Iio b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ico ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ico a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>LocallyFiniteOrder α<VAR>b : α<GOAL>Finset.Ioc ⊥ ↑b = Finset.map Function.Embedding.some (Finset.Iic b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ioc ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ioc a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>LocallyFiniteOrder α<VAR>b : α<GOAL>Finset.Ioo ⊥ ↑b = Finset.map Function.Embedding.some (Finset.Iio b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ioo ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ioo a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrder α<VAR>a b : Subtype p<GOAL>Finset.Icc a b = Finset.subtype p (Finset.Icc ↑a ↑b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrder α<VAR>a b : Subtype p<GOAL>Finset.Ico a b = Finset.subtype p (Finset.Ico ↑a ↑b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrder α<VAR>a b : Subtype p<GOAL>Finset.Ioc a b = Finset.subtype p (Finset.Ioc ↑a ↑b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrder α<VAR>a b : Subtype p<GOAL>Finset.Ioo a b = Finset.subtype p (Finset.Ioo ↑a ↑b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<GOAL>Finset.map (Function.Embedding.subtype p) (Finset.Icc a b) = Finset.Icc ↑a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<GOAL>Finset.map (Function.Embedding.subtype p) (Finset.Ico a b) = Finset.Ico ↑a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<GOAL>Finset.map (Function.Embedding.subtype p) (Finset.Ioc a b) = Finset.Ioc ↑a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<GOAL>Finset.map (Function.Embedding.subtype p) (Finset.Ioo a b) = Finset.Ioo ↑a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrderTop α<VAR>a : Subtype p<GOAL>Finset.Ici a = Finset.subtype p (Finset.Ici ↑a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrderTop α<VAR>a : Subtype p<GOAL>Finset.Ioi a = Finset.subtype p (Finset.Ioi ↑a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrderTop α<VAR>a : Subtype p<VAR>hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x<GOAL>Finset.map (Function.Embedding.subtype p) (Finset.Ici a) = Finset.Ici ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrderTop α<VAR>a : Subtype p<VAR>hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x<GOAL>Finset.map (Function.Embedding.subtype p) (Finset.Ioi a) = Finset.Ioi ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrderBot α<VAR>a : Subtype p<GOAL>Finset.Iic a = Finset.subtype p (Finset.Iic ↑a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrderBot α<VAR>a : Subtype p<GOAL>Finset.Iio a = Finset.subtype p (Finset.Iio ↑a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrderBot α<VAR>a : Subtype p<VAR>hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x<GOAL>Finset.map (Function.Embedding.subtype p) (Finset.Iic a) = Finset.Iic ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>LocallyFiniteOrderBot α<VAR>a : Subtype p<VAR>hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x<GOAL>Finset.map (Function.Embedding.subtype p) (Finset.Iio a) = Finset.Iio ↑a
<VAR>α : Type u_3<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>s : Set α<VAR>h₀ : BddBelow s<VAR>h₁ : BddAbove s<GOAL>s.Finite
<VAR>α : Type u_3<VAR>s : Set α<VAR>SemilatticeSup α<VAR>LocallyFiniteOrder α<VAR>OrderBot α<GOAL>s.Finite ↔ BddAbove s
<VAR>α : Type u_3<VAR>s : Set α<VAR>SemilatticeInf α<VAR>LocallyFiniteOrder α<VAR>OrderTop α<GOAL>s.Finite ↔ BddBelow s
<VAR>α : Type u_3<VAR>s : Set α<VAR>Nonempty α<VAR>Lattice α<VAR>LocallyFiniteOrder α<GOAL>s.Finite ↔ BddBelow s ∧ BddAbove s
<VAR>α : Type u_3<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>Fintype ↑(Set.Icc a b)<GOAL>(Set.Icc a b).toFinset = Finset.Icc a b
<VAR>α : Type u_3<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>Fintype ↑(Set.Ico a b)<GOAL>(Set.Ico a b).toFinset = Finset.Ico a b
<VAR>α : Type u_3<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>Fintype ↑(Set.Ioc a b)<GOAL>(Set.Ioc a b).toFinset = Finset.Ioc a b
<VAR>α : Type u_3<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>Fintype ↑(Set.Ioo a b)<GOAL>(Set.Ioo a b).toFinset = Finset.Ioo a b
<VAR>α : Type u_3<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a : α<VAR>Fintype ↑(Set.Ici a)<GOAL>(Set.Ici a).toFinset = Finset.Ici a
<VAR>α : Type u_3<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a : α<VAR>Fintype ↑(Set.Ioi a)<GOAL>(Set.Ioi a).toFinset = Finset.Ioi a
<VAR>α : Type u_3<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>a : α<VAR>Fintype ↑(Set.Iic a)<GOAL>(Set.Iic a).toFinset = Finset.Iic a
<VAR>α : Type u_3<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>a : α<VAR>Fintype ↑(Set.Iio a)<GOAL>(Set.Iio a).toFinset = Finset.Iio a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>min a b = if a ≤ b then a else b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>max a b = if a ≤ b then b else a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>min a b ≤ a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>min a b ≤ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : c ≤ a<VAR>h₂ : c ≤ b<GOAL>c ≤ min a b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>a ≤ max a b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>b ≤ max a b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a ≤ c<VAR>h₂ : b ≤ c<GOAL>max a b ≤ c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : c ≤ a<VAR>h₂ : c ≤ b<VAR>h₃ : ∀ {d : α}, d ≤ a → d ≤ b → d ≤ c<GOAL>c = min a b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>min a b = min b a