ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a b : α<VAR>h : Order.pred a ≤ b<GOAL>Set.Icc (Order.pred a) b = insert (Order.pred a) (Set.Icc a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a b : α<VAR>h : Order.pred a < b<GOAL>Set.Ico (Order.pred a) b = insert (Order.pred a) (Set.Ico a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a b : α<VAR>NoMinOrder α<GOAL>Order.pred a = Order.pred b ↔ a = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>NoMinOrder α<GOAL>Function.Injective Order.pred
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a b : α<VAR>NoMinOrder α<GOAL>Order.pred a ≠ Order.pred b ↔ a ≠ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a b : α<VAR>NoMinOrder α<GOAL>Order.pred a < b ↔ a = b ∨ a < b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a b : α<VAR>NoMinOrder α<GOAL>Order.pred b = a ↔ a ⋖ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>NoMinOrder α<VAR>a : α<GOAL>Set.Ioi (Order.pred a) = insert a (Set.Ioi a)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a b : α<VAR>NoMinOrder α<VAR>h : a ≤ b<GOAL>Set.Ioc (Order.pred a) b = insert a (Set.Ioc a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a b : α<VAR>NoMinOrder α<VAR>h : a < b<GOAL>Set.Ioo (Order.pred a) b = insert a (Set.Ioo a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>OrderBot α<GOAL>Order.pred ⊥ = ⊥
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<VAR>OrderBot α<GOAL>a ≤ Order.pred a ↔ a = ⊥
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<VAR>OrderBot α<GOAL>Order.pred a < a ↔ a ≠ ⊥
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<VAR>OrderTop α<VAR>NoMinOrder α<GOAL>Order.pred ⊤ < a ↔ a = ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<VAR>OrderTop α<GOAL>Order.pred ⊤ ≤ a ↔ a = ⊤ ∨ a = Order.pred ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>OrderTop α<VAR>Nontrivial α<VAR>a : α<GOAL>Order.pred a < ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>OrderTop α<VAR>Nontrivial α<VAR>a : α<GOAL>Order.pred a ≠ ⊤
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>PredOrder α<VAR>a : α<GOAL>Order.pred a = ⨆ b, ⨆ (_ : b < a), b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>PredOrder α<VAR>a : α<GOAL>a ≤ Order.succ (Order.pred a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>PredOrder α<VAR>a : α<GOAL>Order.pred (Order.succ a) ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>PredOrder α<VAR>a b : α<GOAL>Order.pred a ≤ b ↔ a ≤ Order.succ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>PredOrder α<GOAL>GaloisConnection Order.pred Order.succ
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>PredOrder α<VAR>a : α<VAR>h : ¬IsMin a<GOAL>Order.succ (Order.pred a) = a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>PredOrder α<VAR>a : α<VAR>h : ¬IsMax a<GOAL>Order.pred (Order.succ a) = a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>PredOrder α<VAR>NoMinOrder α<VAR>a : α<GOAL>Order.succ (Order.pred a) = a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>PredOrder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>Order.pred (Order.succ a) = a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>PredOrder α<VAR>i : α<VAR>n : ℕ<VAR>hin : ¬IsMax (Order.succ^[n - 1] i)<GOAL>Order.pred^[n] (Order.succ^[n] i) = i
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>PredOrder α<VAR>i : α<VAR>n : ℕ<VAR>hin : ¬IsMin (Order.pred^[n - 1] i)<GOAL>Order.succ^[n] (Order.pred^[n] i) = i
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>PartialOrder α<VAR>OrderTop α<VAR>SuccOrder α<GOAL>Order.succ ↑⊤ = ⊤
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>PartialOrder α<VAR>OrderTop α<VAR>SuccOrder α<VAR>a : α<VAR>h : a ≠ ⊤<GOAL>Order.succ ↑a = ↑(Order.succ a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderTop α<VAR>PredOrder α<GOAL>Order.pred ⊤ = ↑⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderTop α<VAR>PredOrder α<VAR>a : α<GOAL>Order.pred ↑a = ↑(Order.pred a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderTop α<VAR>PredOrder α<VAR>a : WithTop α<VAR>ha : a ≠ ⊤<GOAL>Order.pred (a.untop ha) = (Order.pred a).untop ⋯
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoMaxOrder α<VAR>SuccOrder α<VAR>a : α<GOAL>Order.succ ↑a = ↑(Order.succ a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<VAR>SuccOrder α<GOAL>Order.succ ⊥ = ↑⊥
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<VAR>SuccOrder α<VAR>a : α<GOAL>Order.succ ↑a = ↑(Order.succ a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<VAR>SuccOrder α<VAR>a : WithBot α<VAR>ha : a ≠ ⊥<GOAL>Order.succ (a.unbot ha) = (Order.succ a).unbot ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>PartialOrder α<VAR>OrderBot α<VAR>PredOrder α<GOAL>Order.pred ↑⊥ = ⊥
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>PartialOrder α<VAR>OrderBot α<VAR>PredOrder α<VAR>a : α<VAR>h : a ≠ ⊥<GOAL>Order.pred ↑a = ↑(Order.pred a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoMinOrder α<VAR>PredOrder α<VAR>a : α<GOAL>Order.pred ↑a = ↑(Order.pred a)
<VAR>α : Type u_3<VAR>Preorder α<VAR>SuccOrder α<VAR>self : IsSuccArchimedean α<VAR>a b : α<VAR>h : a ≤ b<GOAL>∃ n, Order.succ^[n] a = b
<VAR>α : Type u_3<VAR>Preorder α<VAR>PredOrder α<VAR>self : IsPredArchimedean α<VAR>a b : α<VAR>h : a ≤ b<GOAL>∃ n, Order.pred^[n] b = a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>a b : α<VAR>h : a ≤ b<GOAL>∃ n, Order.succ^[n] a = b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>a b : α<GOAL>(∃ n, Order.succ^[n] a = b) ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>P : α → Prop<VAR>m : α<VAR>h0 : P m<VAR>h1 : ∀ (n : α), m ≤ n → P n → P (Order.succ n)<VAR>n : α<VAR>hmn : m ≤ n<GOAL>P n
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>p : α → Prop<VAR>hsucc : ∀ (a : α), p a ↔ p (Order.succ a)<VAR>a b : α<VAR>h : a ≤ b<GOAL>p a ↔ p b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>a b : α<VAR>h : a ≤ b<GOAL>∃ n, Order.pred^[n] b = a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>a b : α<GOAL>(∃ n, Order.pred^[n] b = a) ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>P : α → Prop<VAR>m : α<VAR>h0 : P m<VAR>h1 : ∀ n ≤ m, P n → P (Order.pred n)<VAR>n : α<VAR>hmn : n ≤ m<GOAL>P n
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>p : α → Prop<VAR>hsucc : ∀ (a : α), p a ↔ p (Order.pred a)<VAR>a b : α<VAR>h : a ≤ b<GOAL>p a ↔ p b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>SuccOrder α<VAR>a b : α<GOAL>Order.succ (max a b) = max (Order.succ a) (Order.succ b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>SuccOrder α<VAR>a b : α<GOAL>Order.succ (min a b) = min (Order.succ a) (Order.succ b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>a b : α<GOAL>(∃ n, Order.succ^[n] a = b) ∨ ∃ n, Order.succ^[n] b = a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>p : α → Prop<VAR>hsucc : ∀ (a : α), p a ↔ p (Order.succ a)<VAR>a b : α<GOAL>p a ↔ p b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>PredOrder α<VAR>a b : α<GOAL>Order.pred (max a b) = max (Order.pred a) (Order.pred b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>PredOrder α<VAR>a b : α<GOAL>Order.pred (min a b) = min (Order.pred a) (Order.pred b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>a b : α<GOAL>(∃ n, Order.pred^[n] b = a) ∨ ∃ n, Order.pred^[n] a = b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>p : α → Prop<VAR>hsucc : ∀ (a : α), p a ↔ p (Order.pred a)<VAR>a b : α<GOAL>p a ↔ p b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Nonempty α<VAR>Preorder β<VAR>f : α → β<VAR>NoMaxOrder α<VAR>SuccOrder β<VAR>IsSuccArchimedean β<VAR>hf : StrictMono f<GOAL>¬BddAbove (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Nonempty α<VAR>Preorder β<VAR>f : α → β<VAR>NoMinOrder α<VAR>PredOrder β<VAR>IsPredArchimedean β<VAR>hf : StrictMono f<GOAL>¬BddBelow (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Nonempty α<VAR>Preorder β<VAR>f : α → β<VAR>NoMinOrder α<VAR>SuccOrder β<VAR>IsSuccArchimedean β<VAR>hf : StrictAnti f<GOAL>¬BddAbove (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Nonempty α<VAR>Preorder β<VAR>f : α → β<VAR>NoMaxOrder α<VAR>PredOrder β<VAR>IsPredArchimedean β<VAR>hf : StrictAnti f<GOAL>¬BddBelow (Set.range f)
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>p : α → Prop<VAR>hbot : p ⊥<VAR>hsucc : ∀ (a : α), p a → p (Order.succ a)<VAR>a : α<GOAL>p a
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderTop α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>p : α → Prop<VAR>htop : p ⊤<VAR>hpred : ∀ (a : α), p a → p (Order.pred a)<VAR>a : α<GOAL>p a
<VAR>α : Type u_1<VAR>Nontrivial α<VAR>PartialOrder α<VAR>OrderBot α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>P : α → Prop<GOAL>(∀ (i : α), i ≠ ⊥ → P i) ↔ ∀ (i : α), P (SuccOrder.succ i)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>self : s.OrdConnected<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<GOAL>Set.Icc x y ⊆ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>h : s.OrdConnected<VAR>x : α<GOAL>x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.Icc x y ⊆ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>s.OrdConnected ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.Icc x y ⊆ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>s.OrdConnected ↔ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Set.Icc x y ⊆ s
<VAR>α : Type u_3<VAR>PartialOrder α<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Set.Ioo x y ⊆ s<GOAL>s.OrdConnected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set α<VAR>f : β → α<VAR>hs : s.OrdConnected<VAR>hf : Monotone f<GOAL>(f ⁻¹' s).OrdConnected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set α<VAR>f : β → α<VAR>hs : s.OrdConnected<VAR>hf : Antitone f<GOAL>(f ⁻¹' s).OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>hs : s.OrdConnected<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>Set.Icc x y ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>he : (Set.range ⇑e).OrdConnected<VAR>x y : α<GOAL>⇑e '' Set.Icc x y = Set.Icc (e x) (e y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>he : (Set.range ⇑e).OrdConnected<VAR>x y : α<GOAL>⇑e '' Set.Ico x y = Set.Ico (e x) (e y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>he : (Set.range ⇑e).OrdConnected<VAR>x y : α<GOAL>⇑e '' Set.Ioc x y = Set.Ioc (e x) (e y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>he : (Set.range ⇑e).OrdConnected<VAR>x y : α<GOAL>⇑e '' Set.Ioo x y = Set.Ioo (e x) (e y)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>s.OrdConnected<VAR>x y : ↑s<GOAL>Subtype.val '' Set.Icc x y = Set.Icc ↑x ↑y
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>s.OrdConnected<VAR>x y : ↑s<GOAL>Subtype.val '' Set.Ico x y = Set.Ico ↑x ↑y
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>s.OrdConnected<VAR>x y : ↑s<GOAL>Subtype.val '' Set.Ioc x y = Set.Ioc ↑x ↑y
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>s.OrdConnected<VAR>x y : ↑s<GOAL>Subtype.val '' Set.Ioo x y = Set.Ioo ↑x ↑y
<VAR>α : Type u_1<VAR>Preorder α<VAR>s t : Set α<VAR>hs : s.OrdConnected<VAR>ht : t.OrdConnected<GOAL>(s ∩ t).OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>hs : s.OrdConnected<GOAL>(⇑OrderDual.ofDual ⁻¹' s).OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>(⇑OrderDual.ofDual ⁻¹' s).OrdConnected ↔ s.OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>S : Set (Set α)<VAR>hS : ∀ s ∈ S, s.OrdConnected<GOAL>(⋂₀ S).OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>ι : Sort u_3<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), (s i).OrdConnected<GOAL>(⋂ i, s i).OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>s : (i : ι) → p i → Set α<VAR>hs : ∀ (i : ι) (hi : p i), (s i hi).OrdConnected<GOAL>(⋂ i, ⋂ (hi : p i), s i hi).OrdConnected
<VAR>ι : Type u_3<VAR>α : ι → Type u_4<VAR>(i : ι) → Preorder (α i)<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>h : ∀ i ∈ s, (t i).OrdConnected<GOAL>(s.pi t).OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>(Set.Ici a).OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>(Set.Iic a).OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>(Set.Ioi a).OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>(Set.Iio a).OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>(Set.Icc a b).OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>(Set.Ico a b).OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>(Set.Ioc a b).OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>(Set.Ioo a b).OrdConnected
<VAR>α : Type u_3<VAR>PartialOrder α<VAR>a : α<GOAL>{a}.OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<GOAL>∅.OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Set.univ.OrdConnected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>F : Type u_3<VAR>FunLike F α β<VAR>OrderHomClass F α β<VAR>f : F<VAR>s : Set β<VAR>hs : s.OrdConnected<GOAL>(⇑f ⁻¹' s).OrdConnected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>E : Type u_3<VAR>EquivLike E α β<VAR>OrderIsoClass E α β<VAR>e : E<VAR>s : Set α<VAR>hs : s.OrdConnected<GOAL>(⇑e '' s).OrdConnected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>E : Type u_3<VAR>EquivLike E α β<VAR>OrderIsoClass E α β<VAR>e : E<GOAL>(Set.range ⇑e).OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>s.OrdConnected<GOAL>(⇑OrderDual.ofDual ⁻¹' s).OrdConnected
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Set α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>s.OrdConnected
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Set α<VAR>x y : α<VAR>h : Set.Ioo x y ⊆ s<GOAL>(s ∩ Set.Icc x y).OrdConnected
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Set α<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>(s ∩ Set.Icc x y).OrdConnected ↔ Set.Ioo x y ⊆ s
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Set α<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>¬(s ∩ Set.Icc x y).OrdConnected ↔ ∃ z ∉ s, z ∈ Set.Ioo x y
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>[[a, b]].OrdConnected
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>(Ι a b).OrdConnected
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>hs : s.OrdConnected<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<GOAL>[[x, y]] ⊆ s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>hs : s.OrdConnected<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<GOAL>Ι x y ⊆ s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<GOAL>s.OrdConnected ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → [[x, y]] ⊆ s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x : α<VAR>h : ∀ y ∈ s, [[x, y]] ⊆ s<GOAL>s.OrdConnected
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → [[x, y]] ⊆ s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → [[y, x]] ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Function.Surjective f<VAR>a b : α<GOAL>Set.SurjOn f (Set.Ioo a b) (Set.Ioo (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Function.Surjective f<VAR>a b : α<GOAL>Set.SurjOn f (Set.Ico a b) (Set.Ico (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Function.Surjective f<VAR>a b : α<GOAL>Set.SurjOn f (Set.Ioc a b) (Set.Ioc (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Function.Surjective f<VAR>a b : α<VAR>hab : a ≤ b<GOAL>Set.SurjOn f (Set.Icc a b) (Set.Icc (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Function.Surjective f<VAR>a : α<GOAL>Set.SurjOn f (Set.Ioi a) (Set.Ioi (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Function.Surjective f<VAR>a : α<GOAL>Set.SurjOn f (Set.Iio a) (Set.Iio (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Function.Surjective f<VAR>a : α<GOAL>Set.SurjOn f (Set.Ici a) (Set.Ici (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Function.Surjective f<VAR>a : α<GOAL>Set.SurjOn f (Set.Iic a) (Set.Iic (f a))
<VAR>α : Type u_2<VAR>Lattice α<VAR>self : IsWeakUpperModularLattice α<VAR>a b : α<GOAL>a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b
<VAR>α : Type u_2<VAR>Lattice α<VAR>self : IsWeakLowerModularLattice α<VAR>a b : α<GOAL>a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a
<VAR>α : Type u_2<VAR>Lattice α<VAR>self : IsUpperModularLattice α<VAR>a b : α<GOAL>a ⊓ b ⋖ a → b ⋖ a ⊔ b
<VAR>α : Type u_2<VAR>Lattice α<VAR>self : IsLowerModularLattice α<VAR>a b : α<GOAL>a ⋖ a ⊔ b → a ⊓ b ⋖ b
<VAR>α : Type u_2<VAR>Lattice α<VAR>self : IsModularLattice α<VAR>x : α<VAR>y : α<VAR>z : α<GOAL>x ≤ z → (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsWeakUpperModularLattice α<VAR>a b : α<GOAL>a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsWeakUpperModularLattice α<VAR>a b : α<GOAL>a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsWeakLowerModularLattice α<VAR>a b : α<GOAL>a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsWeakLowerModularLattice α<VAR>a b : α<GOAL>a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsUpperModularLattice α<VAR>a b : α<GOAL>a ⊓ b ⋖ a → b ⋖ a ⊔ b
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsUpperModularLattice α<VAR>a b : α<GOAL>a ⊓ b ⋖ b → a ⋖ a ⊔ b
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsLowerModularLattice α<VAR>a b : α<GOAL>a ⋖ a ⊔ b → a ⊓ b ⋖ b
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsLowerModularLattice α<VAR>a b : α<GOAL>b ⋖ a ⊔ b → a ⊓ b ⋖ a
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>x : α<VAR>y : α<VAR>z : α<VAR>h : x ≤ z<GOAL>(x ⊔ y) ⊓ z = x ⊔ y ⊓ z
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>x y z : α<GOAL>x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>x : α<VAR>y : α<VAR>z : α<VAR>h : z ≤ x<GOAL>x ⊓ y ⊔ z = x ⊓ (y ⊔ z)
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>x y z : α<GOAL>(x ⊔ z) ⊓ (y ⊔ z) = (x ⊔ z) ⊓ y ⊔ z
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>x y z : α<VAR>hxy : x ≤ y<VAR>hinf : y ⊓ z ≤ x<VAR>hsup : y ≤ x ⊔ z<GOAL>x = y
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>x y z : α<VAR>hxy : x ≤ y<VAR>hinf : y ⊓ z ≤ x ⊓ z<VAR>hsup : y ⊔ z ≤ x ⊔ z<GOAL>x = y
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>x y z : α<VAR>hxy : x < y<VAR>hinf : y ⊓ z ≤ x ⊓ z<GOAL>x ⊔ z < y ⊔ z
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>x y z : α<VAR>hxy : x < y<VAR>hinf : y ⊔ z ≤ x ⊔ z<GOAL>x ⊓ z < y ⊓ z
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>PartialOrder β<VAR>Preorder γ<VAR>h₁ : WellFounded fun x x_1 => x < x_1<VAR>h₂ : WellFounded fun x x_1 => x < x_1<VAR>K : α<VAR>f₁ : β → α<VAR>f₂ : α → β<VAR>g₁ : γ → α<VAR>g₂ : α → γ<VAR>gci : GaloisCoinsertion f₁ f₂<VAR>gi : GaloisInsertion g₂ g₁<VAR>hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K<VAR>hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K<GOAL>WellFounded fun x x_1 => x < x_1
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder β<VAR>PartialOrder γ<VAR>h₁ : WellFounded fun x x_1 => x > x_1<VAR>h₂ : WellFounded fun x x_1 => x > x_1<VAR>K : α<VAR>f₁ : β → α<VAR>f₂ : α → β<VAR>g₁ : γ → α<VAR>g₂ : α → γ<VAR>gci : GaloisCoinsertion f₁ f₂<VAR>gi : GaloisInsertion g₂ g₁<VAR>hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K<VAR>hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K<GOAL>WellFounded fun x x_1 => x > x_1
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>a b : α<VAR>x : ↑(Set.Icc (a ⊓ b) a)<GOAL>↑((infIccOrderIsoIccSup a b) x) = ↑x ⊔ b
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>a b : α<VAR>x : ↑(Set.Icc b (a ⊔ b))<GOAL>↑((RelIso.symm (infIccOrderIsoIccSup a b)) x) = a ⊓ ↑x
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>a b : α<GOAL>StrictMonoOn (fun c => a ⊓ c) (Set.Icc b (a ⊔ b))
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>a b : α<GOAL>StrictMonoOn (fun c => c ⊔ b) (Set.Icc (a ⊓ b) a)
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>a b : α<VAR>c : ↑(Set.Ioo (a ⊓ b) a)<GOAL>↑((infIooOrderIsoIooSup a b) c) = ↑c ⊔ b
<VAR>α : Type u_1<VAR>Lattice α<VAR>IsModularLattice α<VAR>a b : α<VAR>c : ↑(Set.Ioo b (a ⊔ b))<GOAL>↑((RelIso.symm (infIooOrderIsoIooSup a b)) c) = a ⊓ ↑c
<VAR>α : Type u_1<VAR>Lattice α<GOAL>IsModularLattice α ↔ ∀ (x y z : α), x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z
<VAR>α : Type u_1<VAR>a b c : α<VAR>Lattice α<VAR>OrderBot α<VAR>IsModularLattice α<VAR>h : Disjoint a b<VAR>hsup : Disjoint (a ⊔ b) c<GOAL>Disjoint a (b ⊔ c)
<VAR>α : Type u_1<VAR>a b c : α<VAR>Lattice α<VAR>OrderBot α<VAR>IsModularLattice α<VAR>h : Disjoint b c<VAR>hsup : Disjoint a (b ⊔ c)<GOAL>Disjoint (a ⊔ b) c
<VAR>α : Type u_1<VAR>a b c : α<VAR>Lattice α<VAR>BoundedOrder α<VAR>IsModularLattice α<VAR>h : Disjoint a b<VAR>hcomp : IsCompl (a ⊔ b) c<GOAL>IsCompl a (b ⊔ c)
<VAR>α : Type u_1<VAR>a b c : α<VAR>Lattice α<VAR>BoundedOrder α<VAR>IsModularLattice α<VAR>h : Disjoint b c<VAR>hcomp : IsCompl a (b ⊔ c)<GOAL>IsCompl (a ⊔ b) c
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<VAR>IsModularLattice α<VAR>a b c : α<VAR>h₁ : IsCompl b c<VAR>h₂ : b ≤ a<GOAL>IsCompl ⟨a ⊓ b, ⋯⟩ ⟨a ⊓ c, ⋯⟩
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>i : ι<GOAL>IsGLB (Set.Ioi i) (LinearLocallyFiniteOrder.succFn i)
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>i : ι<GOAL>i ≤ LinearLocallyFiniteOrder.succFn i
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>i j k : ι<VAR>hij_lt : i < j<VAR>h : IsGLB (Set.Ioi i) k<GOAL>IsGLB (Set.Ioc i j) k
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>LocallyFiniteOrder ι<VAR>i : ι<VAR>hi : LinearLocallyFiniteOrder.succFn i ≤ i<GOAL>IsMax i
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>i j : ι<VAR>hij : i < j<GOAL>LinearLocallyFiniteOrder.succFn i ≤ j
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>j i : ι<VAR>hij : j < LinearLocallyFiniteOrder.succFn i<GOAL>j ≤ i
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 i : ι<VAR>hi : i0 ≤ i<GOAL>toZ i0 i = ↑(Nat.find ⋯)
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 i : ι<VAR>hi : i < i0<GOAL>toZ i0 i = -↑(Nat.find ⋯)
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 : ι<GOAL>toZ i0 i0 = 0
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 : ι<VAR>i : ι<VAR>hi : i0 ≤ i<GOAL>Order.succ^[(toZ i0 i).toNat] i0 = i
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 : ι<VAR>i : ι<VAR>hi : i < i0<GOAL>Order.pred^[(-toZ i0 i).toNat] i0 = i
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 i : ι<VAR>hi : i0 ≤ i<GOAL>0 ≤ toZ i0 i
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 i : ι<VAR>hi : i < i0<GOAL>toZ i0 i < 0
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 : ι<VAR>n : ℕ<GOAL>toZ i0 (Order.succ^[n] i0) ≤ ↑n
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 : ι<VAR>n : ℕ<GOAL>-↑n ≤ toZ i0 (Order.pred^[n] i0)
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 : ι<VAR>n : ℕ<VAR>hn : ¬IsMax (Order.succ^[n] i0)<GOAL>toZ i0 (Order.succ^[n] i0) = ↑n
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 : ι<VAR>n : ℕ<VAR>hn : ¬IsMin (Order.pred^[n] i0)<GOAL>toZ i0 (Order.pred^[n] i0) = -↑n