ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<VAR>h : ¬Order.IsSuccLimit a<GOAL>a ∈ Set.range Order.succ
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>b : α<VAR>H : ∀ a < b, Order.succ a < b<GOAL>Order.IsSuccLimit b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<VAR>hb : Order.IsSuccLimit b<VAR>ha : a < b<GOAL>Order.succ a < b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<VAR>hb : Order.IsSuccLimit b<GOAL>Order.succ a < b ↔ a < b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>b : α<GOAL>Order.IsSuccLimit b ↔ ∀ a < b, Order.succ a < b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>b : α<VAR>C : α → Sort u_2<VAR>hs : (a : α) → ¬IsMax a → C (Order.succ a)<VAR>hl : (a : α) → Order.IsSuccLimit a → C a<VAR>hb : Order.IsSuccLimit b<GOAL>Order.isSuccLimitRecOn b hs hl = hl b hb
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>C : α → Sort u_2<VAR>hs : (a : α) → ¬IsMax a → C (Order.succ a)<VAR>hl : (a : α) → Order.IsSuccLimit a → C a<VAR>b : α<VAR>hb : ¬IsMax b<GOAL>Order.isSuccLimitRecOn (Order.succ b) hs hl = hs b hb
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<VAR>C : α → Sort u_2<VAR>WellFoundedLT α<VAR>H_succ : (a : α) → ¬IsMax a → C a → C (Order.succ a)<VAR>H_lim : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → C b) → C a<VAR>ha : ¬IsMax a<GOAL>SuccOrder.limitRecOn (Order.succ a) H_succ H_lim = H_succ a ha (SuccOrder.limitRecOn a H_succ H_lim)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<VAR>C : α → Sort u_2<VAR>WellFoundedLT α<VAR>H_succ : (a : α) → ¬IsMax a → C a → C (Order.succ a)<VAR>H_lim : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → C b) → C a<VAR>ha : Order.IsSuccLimit a<GOAL>SuccOrder.limitRecOn a H_succ H_lim = H_lim a ha fun x x_1 => SuccOrder.limitRecOn x H_succ H_lim
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>C : α → Sort u_2<VAR>NoMaxOrder α<VAR>hs : (a : α) → ¬IsMax a → C (Order.succ a)<VAR>hl : (a : α) → Order.IsSuccLimit a → C a<VAR>b : α<GOAL>Order.isSuccLimitRecOn (Order.succ b) hs hl = hs b ⋯
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<VAR>NoMaxOrder α<GOAL>Order.IsSuccLimit a ↔ ∀ (b : α), Order.succ b ≠ a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<VAR>NoMaxOrder α<GOAL>¬Order.IsSuccLimit a ↔ a ∈ Set.range Order.succ
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<VAR>IsSuccArchimedean α<VAR>h : Order.IsSuccLimit a<GOAL>IsMin a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<VAR>IsSuccArchimedean α<GOAL>Order.IsSuccLimit a ↔ IsMin a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<VAR>IsSuccArchimedean α<VAR>NoMinOrder α<GOAL>¬Order.IsSuccLimit a
<VAR>α : Type u_1<VAR>LT α<VAR>a : α<GOAL>¬Order.IsPredLimit a ↔ ∃ b, a ⋖ b
<VAR>α : Type u_1<VAR>LT α<VAR>DenselyOrdered α<VAR>a : α<GOAL>Order.IsPredLimit a
<VAR>α : Type u_1<VAR>LT α<VAR>a : α<GOAL>Order.IsSuccLimit (OrderDual.toDual a) ↔ Order.IsPredLimit a
<VAR>α : Type u_1<VAR>LT α<VAR>a : α<GOAL>Order.IsPredLimit (OrderDual.toDual a) ↔ Order.IsSuccLimit a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>IsMax a → Order.IsPredLimit a
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderTop α<GOAL>Order.IsPredLimit ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>PredOrder α<VAR>h : Order.IsPredLimit (Order.pred a)<GOAL>IsMin a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>PredOrder α<VAR>ha : ¬IsMin a<GOAL>¬Order.IsPredLimit (Order.pred a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>PredOrder α<VAR>NoMinOrder α<VAR>h : Order.IsPredLimit a<VAR>b : α<GOAL>Order.pred b ≠ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>NoMinOrder α<VAR>a : α<GOAL>¬Order.IsPredLimit (Order.pred a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>NoMinOrder α<VAR>h : Order.IsPredLimit a<GOAL>IsMax a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>NoMinOrder α<GOAL>Order.IsPredLimit a ↔ IsMax a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>NoMinOrder α<VAR>NoMaxOrder α<GOAL>¬Order.IsPredLimit a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<VAR>h : ∀ (b : α), Order.pred b ≠ a<GOAL>Order.IsPredLimit a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<GOAL>¬Order.IsPredLimit a ↔ ∃ b, ¬IsMin b ∧ Order.pred b = a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<VAR>h : ¬Order.IsPredLimit a<GOAL>a ∈ Set.range Order.pred
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>b : α<VAR>H : ∀ a > b, Order.pred a < b<GOAL>Order.IsPredLimit b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a b : α<VAR>h : Order.IsPredLimit a<GOAL>a < b → a < Order.pred b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a b : α<VAR>h : Order.IsPredLimit a<GOAL>a < Order.pred b ↔ a < b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<GOAL>Order.IsPredLimit a ↔ ∀ ⦃b : α⦄, a < b → a < Order.pred b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>b : α<VAR>C : α → Sort u_2<VAR>hs : (a : α) → ¬IsMin a → C (Order.pred a)<VAR>hl : (a : α) → Order.IsPredLimit a → C a<VAR>hb : Order.IsPredLimit b<GOAL>Order.isPredLimitRecOn b hs hl = hl b hb
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>C : α → Sort u_2<VAR>hs : (a : α) → ¬IsMin a → C (Order.pred a)<VAR>hl : (a : α) → Order.IsPredLimit a → C a<VAR>b : α<VAR>hb : ¬IsMin b<GOAL>Order.isPredLimitRecOn (Order.pred b) hs hl = hs b hb
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<VAR>C : α → Sort u_2<VAR>WellFoundedGT α<VAR>H_pred : (a : α) → ¬IsMin a → C a → C (Order.pred a)<VAR>H_lim : (a : α) → Order.IsPredLimit a → ((b : α) → b > a → C b) → C a<VAR>ha : ¬IsMin a<GOAL>PredOrder.limitRecOn (Order.pred a) H_pred H_lim = H_pred a ha (PredOrder.limitRecOn a H_pred H_lim)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<VAR>C : α → Sort u_2<VAR>WellFoundedGT α<VAR>H_pred : (a : α) → ¬IsMin a → C a → C (Order.pred a)<VAR>H_lim : (a : α) → Order.IsPredLimit a → ((b : α) → b > a → C b) → C a<VAR>ha : Order.IsPredLimit a<GOAL>PredOrder.limitRecOn a H_pred H_lim = H_lim a ha fun x x_1 => PredOrder.limitRecOn x H_pred H_lim
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>C : α → Sort u_2<VAR>NoMinOrder α<VAR>hs : (a : α) → ¬IsMin a → C (Order.pred a)<VAR>hl : (a : α) → Order.IsPredLimit a → C a<VAR>b : α<GOAL>Order.isPredLimitRecOn (Order.pred b) hs hl = hs b ⋯
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<VAR>IsPredArchimedean α<VAR>h : Order.IsPredLimit a<GOAL>IsMax a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<VAR>IsPredArchimedean α<GOAL>Order.IsPredLimit a ↔ IsMax a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<VAR>IsPredArchimedean α<VAR>NoMaxOrder α<GOAL>¬Order.IsPredLimit a
<VAR>α : Type u_1<VAR>SemilatticeSup α<GOAL>⇑UpperSet.iciSupHom = UpperSet.Ici
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>a : α<GOAL>UpperSet.iciSupHom a = UpperSet.Ici a
<VAR>α : Type u_1<VAR>CompleteLattice α<GOAL>⇑UpperSet.icisSupHom = UpperSet.Ici
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>a : α<GOAL>UpperSet.icisSupHom a = UpperSet.Ici a
<VAR>α : Type u_1<VAR>SemilatticeInf α<GOAL>⇑LowerSet.iicInfHom = LowerSet.Iic
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>a : α<GOAL>LowerSet.iicInfHom a = LowerSet.Iic a
<VAR>α : Type u_1<VAR>CompleteLattice α<GOAL>⇑LowerSet.iicsInfHom = LowerSet.Iic
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>a : α<GOAL>LowerSet.iicsInfHom a = LowerSet.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>LocallyFiniteOrderTop α<VAR>hs : s.Finite<GOAL>(↑(upperClosure s)).Finite
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>LocallyFiniteOrderBot α<VAR>hs : s.Finite<GOAL>(↑(lowerClosure s)).Finite
<VAR>α : Type u<VAR>x : α<VAR>S : Set (Set α)<GOAL>x ∈ ⋂₀ S ↔ ∀ (t : Set α), t ∈ S → x ∈ t
<VAR>α : Type u<VAR>x : α<VAR>S : Set (Set α)<GOAL>x ∈ ⋃₀ S ↔ ∃ t, t ∈ S ∧ x ∈ t
<VAR>α : Type u<VAR>ι : Sort v<VAR>x : α<VAR>s : ι → Set α<GOAL>x ∈ ⋃ i, s i ↔ ∃ i, x ∈ s i
<VAR>α : Type u<VAR>ι : Sort v<VAR>x : α<VAR>s : ι → Set α<GOAL>x ∈ ⋂ i, s i ↔ ∀ (i : ι), x ∈ s i
<VAR>α : Type u<VAR>S : Set (Set α)<GOAL>sSup S = ⋃₀ S
<VAR>α : Type u<VAR>S : Set (Set α)<GOAL>sInf S = ⋂₀ S
<VAR>α : Type u<VAR>ι : Sort v<VAR>s : ι → Set α<GOAL>iSup s = Set.iUnion s
<VAR>α : Type u<VAR>ι : Sort v<VAR>s : ι → Set α<GOAL>iInf s = Set.iInter s
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ⩿ b<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>a ⩿ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a = b<GOAL>a ⩿ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h1 : a ≤ b<VAR>h2 : b ≤ a<GOAL>a ⩿ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : AntisymmRel (fun x x_1 => x ≤ x_1) a b<GOAL>a ⩿ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>hab : a ⩿ b<GOAL>b ⩿ a ↔ b ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>hab : a ≤ b<VAR>h : ∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b<GOAL>a ⩿ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hab : AntisymmRel (fun x x_1 => x ≤ x_1) a b<VAR>hbc : b ⩿ c<GOAL>a ⩿ c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hab : AntisymmRel (fun x x_1 => x ≤ x_1) a b<GOAL>a ⩿ c ↔ b ⩿ c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hab : a ⩿ b<VAR>hbc : AntisymmRel (fun x x_1 => x ≤ x_1) b c<GOAL>a ⩿ c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hab : AntisymmRel (fun x x_1 => x ≤ x_1) a b<GOAL>c ⩿ a ↔ c ⩿ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>¬a ⩿ b ↔ ∃ c, a < c ∧ c < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ⩿ b<GOAL>Set.Ioo a b = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>a ⩿ b ↔ a ≤ b ∧ Set.Ioo a b = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hac : a ⩿ c<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<GOAL>b ⩿ c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hac : a ⩿ c<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<GOAL>a ⩿ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>f : α ↪o β<VAR>h : f a ⩿ f b<GOAL>a ⩿ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>f : α ↪o β<VAR>hab : a ⩿ b<VAR>h : (Set.range ⇑f).OrdConnected<GOAL>f a ⩿ f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>f : α ↪o β<VAR>h : (Set.range ⇑f).OrdConnected<GOAL>f a ⩿ f b ↔ a ⩿ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>E : Type u_3<VAR>EquivLike E α β<VAR>OrderIsoClass E α β<VAR>e : E<GOAL>e a ⩿ e b ↔ a ⩿ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>OrderDual.toDual b ⩿ OrderDual.toDual a ↔ a ⩿ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual a ⩿ OrderDual.ofDual b ↔ b ⩿ a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b c : α<VAR>h : a ⩿ b<VAR>h2 : a ≤ c<VAR>h3 : c ≤ b<GOAL>c = a ∨ c = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>a ⩿ b ↔ a ≤ b ∧ ∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b c : α<VAR>h : a ⩿ b<GOAL>a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ⩿ b<GOAL>Set.Icc a b = {a, b}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ⩿ b<GOAL>Set.Ico a b ⊆ {a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ⩿ b<GOAL>Set.Ioc a b ⊆ {b}
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>a b c : α<VAR>hac : a ⩿ c<VAR>hbc : b ⩿ c<VAR>hab : a ≠ b<GOAL>a ⊔ b = c
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>a b c : α<VAR>hca : c ⩿ a<VAR>hcb : c ⩿ b<VAR>hab : a ≠ b<GOAL>a ⊓ b = c
<VAR>α : Type u_1<VAR>LT α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>a < b
<VAR>α : Type u_1<VAR>LT α<VAR>a b : α<VAR>h : a < b<GOAL>¬a ⋖ b ↔ ∃ c, a < c ∧ c < b
<VAR>α : Type u_1<VAR>LT α<VAR>a b : α<VAR>DenselyOrdered α<GOAL>¬a ⋖ b
<VAR>α : Type u_1<VAR>LT α<GOAL>DenselyOrdered α ↔ ∀ (a b : α), ¬a ⋖ b
<VAR>α : Type u_1<VAR>LT α<VAR>a b : α<GOAL>OrderDual.toDual b ⋖ OrderDual.toDual a ↔ a ⋖ b
<VAR>α : Type u_1<VAR>LT α<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual a ⋖ OrderDual.ofDual b ↔ b ⋖ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>a ≠ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>b ≠ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>a ⩿ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ⩿ b<VAR>h2 : ¬b ≤ a<GOAL>a ⋖ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ⩿ b<VAR>h2 : a < b<GOAL>a ⋖ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hac : a ⋖ c<VAR>hab : a ≤ b<VAR>hbc : b < c<GOAL>b ⋖ c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hac : a ⋖ c<VAR>hab : a < b<VAR>hbc : b ≤ c<GOAL>a ⋖ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>h₁ : a < b<VAR>h₂ : b < c<GOAL>¬a ⋖ c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>a ⋖ b ↔ a ⩿ b ∧ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>a ⋖ b ↔ a ⩿ b ∧ ¬b ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>a ⩿ b ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hab : AntisymmRel (fun x x_1 => x ≤ x_1) a b<VAR>hbc : b ⋖ c<GOAL>a ⋖ c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hab : AntisymmRel (fun x x_1 => x ≤ x_1) a b<GOAL>a ⋖ c ↔ b ⋖ c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hab : a ⋖ b<VAR>hbc : AntisymmRel (fun x x_1 => x ≤ x_1) b c<GOAL>a ⋖ c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hab : AntisymmRel (fun x x_1 => x ≤ x_1) a b<GOAL>c ⋖ a ↔ c ⋖ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>Set.Ioo a b = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>a ⋖ b ↔ a < b ∧ Set.Ioo a b = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>f : α ↪o β<VAR>h : f a ⋖ f b<GOAL>a ⋖ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>f : α ↪o β<VAR>hab : a ⋖ b<VAR>h : (Set.range ⇑f).OrdConnected<GOAL>f a ⋖ f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>f : α ↪o β<VAR>h : (Set.range ⇑f).OrdConnected<GOAL>f a ⋖ f b ↔ a ⋖ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>E : Type u_3<VAR>EquivLike E α β<VAR>OrderIsoClass E α β<VAR>e : E<GOAL>e a ⋖ e b ↔ a ⋖ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>hab : a < b<VAR>h : ∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b<GOAL>a ⋖ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ⩿ b<VAR>h2 : a ≠ b<GOAL>a ⋖ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>a ⋖ b ↔ a ⩿ b ∧ a ≠ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>a ⩿ b ↔ a ⋖ b ∨ a = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>a ⩿ b ↔ a = b ∨ a ⋖ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b c : α<VAR>h : a ⋖ b<VAR>h2 : a ≤ c<VAR>h3 : c ≤ b<GOAL>c = a ∨ c = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>a ⋖ b ↔ a < b ∧ ∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>Set.Ico a b = {a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>Set.Ioc a b = {b}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>Set.Icc a b = {a, b}
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>Set.Ioi a = Set.Ici b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>Set.Iio b = Set.Iic a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>hab : a ⩿ b<VAR>hcb : c < b<GOAL>c ≤ a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>hab : a ⩿ b<VAR>hac : a < c<GOAL>b ≤ c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>hab : a ⋖ b<GOAL>c < b → c ≤ a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>hab : a ⋖ b<GOAL>a < c → b ≤ c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>ha : a ⋖ c<VAR>hb : b ⋖ c<GOAL>a = b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>hb : a ⋖ b<VAR>hc : a ⋖ c<GOAL>b = c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c x : α<VAR>hab : a ⋖ b<VAR>hbc : b ⋖ c<VAR>hax : a < x<VAR>hxc : x < c<GOAL>x = b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a < b<GOAL>∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y
<VAR>α : Type u_1<VAR>x : α<VAR>s : Set α<GOAL>s ⩿ insert x s
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<GOAL>s \ {a} ⩿ s
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>ha : a ∉ s<GOAL>s ⋖ insert a s
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>ha : a ∈ s<GOAL>s \ {a} ⋖ s
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⋖ t<GOAL>∃ a ∉ s, insert a s = t
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⋖ t<GOAL>∃ a ∈ t, t \ {a} = s
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>s ⋖ t ↔ ∃ a ∉ s, insert a s = t
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>s ⋖ t ↔ ∃ a ∈ t, t \ {a} = s
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>(fun x x_1 => x ⩿ x_1) = Relation.ReflGen fun x x_1 => x ⋖ x_1
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>(Relation.TransGen fun x x_1 => x ⩿ x_1) = Relation.ReflTransGen fun x x_1 => x ⋖ x_1
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>(Relation.ReflTransGen fun x x_1 => x ⩿ x_1) = Relation.ReflTransGen fun x x_1 => x ⋖ x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>x y : α × β<GOAL>x.swap ⩿ y.swap ↔ x ⩿ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>x y : α × β<GOAL>x.swap ⋖ y.swap ↔ x ⋖ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>x y : α × β<GOAL>x ⩿ y → x.1 = y.1 ∨ x.2 = y.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>x y : α × β<VAR>h : x ⩿ y<GOAL>x.1 ⩿ y.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>x y : α × β<VAR>h : x ⩿ y<GOAL>x.2 ⩿ y.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>a₁ a₂ : α<VAR>b : β<GOAL>(a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>a : α<VAR>b₁ b₂ : β<GOAL>(a, b₁) ⩿ (a, b₂) ↔ b₁ ⩿ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>a₁ a₂ : α<VAR>b : β<GOAL>(a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>a : α<VAR>b₁ b₂ : β<GOAL>(a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>(a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>(a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>x y : α × β<GOAL>x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>x y : α × β<GOAL>x ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>s : Set α<GOAL>upperBounds (⇑f '' s) = ⇑f '' upperBounds s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>s : Set α<GOAL>lowerBounds (⇑f '' s) = ⇑f '' lowerBounds s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>s : Set α<VAR>x : β<GOAL>IsLUB (⇑f '' s) x ↔ IsLUB s (f.symm x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>s : Set α<VAR>x : α<GOAL>IsLUB (⇑f '' s) (f x) ↔ IsLUB s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>s : Set α<VAR>x : β<GOAL>IsGLB (⇑f '' s) x ↔ IsGLB s (f.symm x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>s : Set α<VAR>x : α<GOAL>IsGLB (⇑f '' s) (f x) ↔ IsGLB s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>s : Set β<VAR>x : α<GOAL>IsLUB (⇑f ⁻¹' s) x ↔ IsLUB s (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>s : Set β<VAR>x : β<GOAL>IsLUB (⇑f ⁻¹' s) (f.symm x) ↔ IsLUB s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>s : Set β<VAR>x : α<GOAL>IsGLB (⇑f ⁻¹' s) x ↔ IsGLB s (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>s : Set β<VAR>x : β<GOAL>IsGLB (⇑f ⁻¹' s) (f.symm x) ↔ IsGLB s x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>NoMaxOrder α<VAR>nonem : Nonempty α<VAR>lo hi : Finset α<VAR>lo_lt_hi : ∀ x ∈ lo, ∀ y ∈ hi, x < y<GOAL>∃ m, (∀ x ∈ lo, x < m) ∧ ∀ y ∈ hi, m < y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>LinearOrder β<VAR>DenselyOrdered β<VAR>NoMinOrder β<VAR>NoMaxOrder β<VAR>Nonempty β<VAR>f : Order.PartialIso α β<VAR>a : α<GOAL>∃ b, ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>LinearOrder β<VAR>Countable α<VAR>DenselyOrdered β<VAR>Nontrivial β<GOAL>Nonempty (α ↪o β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>LinearOrder β<VAR>Countable α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>NoMaxOrder α<VAR>Nonempty α<VAR>Countable β<VAR>DenselyOrdered β<VAR>NoMinOrder β<VAR>NoMaxOrder β<VAR>Nonempty β<GOAL>Nonempty (α ≃o β)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>x₀ y₀ : α 0<VAR>x y : (i : Fin n) → α i.succ<VAR>s : {i : Fin n.succ} → α i → α i → Prop<GOAL>Pi.Lex (fun x x_1 => x < x_1) s (Fin.cons x₀ x) (Fin.cons y₀ y) ↔ s x₀ y₀ ∨ x₀ = y₀ ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i => s) x y
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>(i : Fin (n + 1)) → Preorder (α i)<VAR>i : Fin (n + 1)<VAR>x : α i<VAR>p : (j : Fin n) → α (i.succAbove j)<VAR>q₁ q₂ : (j : Fin (n + 1)) → α j<GOAL>i.insertNth x p ∈ Set.Icc q₁ q₂ ↔ x ∈ Set.Icc (q₁ i) (q₂ i) ∧ p ∈ Set.Icc (fun j => q₁ (i.succAbove j)) fun j => q₂ (i.succAbove j)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>(i : Fin (n + 1)) → Preorder (α i)<VAR>i : Fin (n + 1)<VAR>x : α i<VAR>q₁ q₂ : (j : Fin (n + 1)) → α j<VAR>hx : x ∈ Set.Icc (q₁ i) (q₂ i)<GOAL>i.insertNth x ⁻¹' Set.Icc q₁ q₂ = Set.Icc (fun j => q₁ (i.succAbove j)) fun j => q₂ (i.succAbove j)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>(i : Fin (n + 1)) → Preorder (α i)<VAR>i : Fin (n + 1)<VAR>x : α i<VAR>q₁ q₂ : (j : Fin (n + 1)) → α j<VAR>hx : x ∉ Set.Icc (q₁ i) (q₂ i)<GOAL>i.insertNth x ⁻¹' Set.Icc q₁ q₂ = ∅
<VAR>α : Type u_1<VAR>n : ℕ<VAR>r : α → α → Prop<VAR>IsTrans α r<VAR>f : Fin (n + 1) → α<VAR>a : α<GOAL>((fun x x_1 => x < x_1) ⇒ r) (Matrix.vecCons a f) (Matrix.vecCons a f) ↔ r a (f 0) ∧ ((fun x x_1 => x < x_1) ⇒ r) f f
<VAR>α : Type u_1<VAR>Preorder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>a : α<GOAL>StrictMono (Matrix.vecCons a f) ↔ a < f 0 ∧ StrictMono f
<VAR>α : Type u_1<VAR>Preorder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>a : α<GOAL>Monotone (Matrix.vecCons a f) ↔ a ≤ f 0 ∧ Monotone f
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Monotone ![a]
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>StrictMono ![a]
<VAR>α : Type u_1<VAR>Preorder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>a : α<GOAL>StrictAnti (Matrix.vecCons a f) ↔ f 0 < a ∧ StrictAnti f
<VAR>α : Type u_1<VAR>Preorder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>a : α<GOAL>Antitone (Matrix.vecCons a f) ↔ f 0 ≤ a ∧ Antitone f
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Antitone ![a]
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>StrictAnti ![a]
<VAR>α : Type u_1<VAR>Preorder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>a : α<VAR>hf : StrictMono f<VAR>ha : a < f 0<GOAL>StrictMono (Matrix.vecCons a f)
<VAR>α : Type u_1<VAR>Preorder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>a : α<VAR>hf : StrictAnti f<VAR>ha : f 0 < a<GOAL>StrictAnti (Matrix.vecCons a f)
<VAR>α : Type u_1<VAR>Preorder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>a : α<VAR>hf : Monotone f<VAR>ha : a ≤ f 0<GOAL>Monotone (Matrix.vecCons a f)
<VAR>α : Type u_1<VAR>Preorder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>a : α<VAR>hf : Antitone f<VAR>ha : f 0 ≤ a<GOAL>Antitone (Matrix.vecCons a f)
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>(finSuccAboveOrderIso p) i = ⟨p.succAbove i, ⋯⟩
<VAR>n : ℕ<VAR>x : { x // x ≠ Fin.last n }<GOAL>(finSuccAboveOrderIso (Fin.last n)).symm x = (↑x).castLT ⋯
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>h : p ≠ Fin.last n<VAR>x : { x // x ≠ p }<GOAL>(finSuccAboveEquiv p).symm x = (p.castLT ⋯).predAbove ↑x
<VAR>n m : ℕ<VAR>h : n ≤ m<VAR>i : { i // ↑i < n }<GOAL>(RelIso.symm (Fin.castLEOrderIso h)) i = ⟨↑↑i, ⋯⟩
<VAR>n m : ℕ<VAR>h : n ≤ m<VAR>i : Fin n<GOAL>(Fin.castLEOrderIso h) i = ⟨Fin.castLE h i, ⋯⟩