ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Balanced<VAR>hr : r.Balanced<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>H : (∃ l', Ordnode.Raised l' l.size ∧ Ordnode.BalancedSz l' r.size) ∨ ∃ r', Ordnode.Raised r.size r' ∧ Ordnode.BalancedSz l.size r'<GOAL>(l.balanceL x r).size = l.size + r.size + 1
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Balanced<VAR>hr : r.Balanced<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>H : (∃ l', Ordnode.Raised l' l.size ∧ Ordnode.BalancedSz l' r.size) ∨ ∃ r', Ordnode.Raised r.size r' ∧ Ordnode.BalancedSz l.size r'<GOAL>Ordnode.All P (l.balanceL x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Balanced<VAR>hr : r.Balanced<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>H : (∃ l', Ordnode.Raised l.size l' ∧ Ordnode.BalancedSz l' r.size) ∨ ∃ r', Ordnode.Raised r' r.size ∧ Ordnode.BalancedSz l.size r'<GOAL>l.balanceR x r = l.balance' x r
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Balanced<VAR>hr : r.Balanced<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>H : (∃ l', Ordnode.Raised l.size l' ∧ Ordnode.BalancedSz l' r.size) ∨ ∃ r', Ordnode.Raised r' r.size ∧ Ordnode.BalancedSz l.size r'<GOAL>(l.balanceR x r).size = l.size + r.size + 1
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Balanced<VAR>hr : r.Balanced<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>H : (∃ l', Ordnode.Raised l.size l' ∧ Ordnode.BalancedSz l' r.size) ∨ ∃ r', Ordnode.Raised r' r.size ∧ Ordnode.BalancedSz l.size r'<GOAL>Ordnode.All P (l.balanceR x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<GOAL>t.Bounded o₁ o₂ → t.dual.Bounded o₂ o₁
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<GOAL>t.Bounded o₁ o₂ ↔ t.dual.Bounded o₂ o₁
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<GOAL>t.Bounded o₁ o₂ → t.Bounded ⊥ o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<GOAL>t.Bounded o₁ o₂ → t.Bounded o₁ ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>h : t.Bounded o₁ o₂<GOAL>t.Bounded ⊥ ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>x y : α<VAR>xy : x ≤ y<VAR>t : Ordnode α<VAR>o : WithTop α<GOAL>t.Bounded (↑y) o → t.Bounded (↑x) o
<VAR>α : Type u_1<VAR>Preorder α<VAR>x y : α<VAR>xy : x ≤ y<VAR>t : Ordnode α<VAR>o : WithBot α<GOAL>t.Bounded o ↑x → t.Bounded o ↑y
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>x y : α<GOAL>t.Bounded ↑x ↑y → x < y
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<GOAL>t.Bounded o₁ o₂ → Ordnode.nil.Bounded o₁ o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>t₁ t₂ : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<GOAL>t₁.Bounded o₁ ↑x → t₂.Bounded (↑x) o₂ → t₂.Bounded o₁ o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>t₁ t₂ : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<GOAL>t₁.Bounded o₁ ↑x → t₂.Bounded (↑x) o₂ → t₁.Bounded o₁ o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>o : WithBot α<VAR>x : α<GOAL>t.Bounded o ↑x → Ordnode.All (fun x_1 => x_1 < x) t
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>o : WithTop α<VAR>x : α<GOAL>t.Bounded (↑x) o → Ordnode.All (fun x_1 => x_1 > x) t
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>x : α<GOAL>t.Bounded o₁ o₂ → Ordnode.nil.Bounded o₁ ↑x → Ordnode.All (fun x_1 => x_1 < x) t → t.Bounded o₁ ↑x
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>x : α<GOAL>t.Bounded o₁ o₂ → Ordnode.nil.Bounded (↑x) o₂ → Ordnode.All (fun x_1 => x_1 > x) t → t.Bounded (↑x) o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>t₁ t₂ : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>x : α<VAR>h₁ : t₁.Bounded o₁ ↑x<VAR>h₂ : t₂.Bounded (↑x) o₂<GOAL>Ordnode.All (fun y => Ordnode.All (fun z => y < z) t₂) t₁
<VAR>α : Type u_1<VAR>Preorder α<VAR>lo : WithBot α<VAR>t : Ordnode α<VAR>hi : WithTop α<VAR>self : Ordnode.Valid' lo t hi<GOAL>t.Bounded lo hi
<VAR>α : Type u_1<VAR>Preorder α<VAR>lo : WithBot α<VAR>t : Ordnode α<VAR>hi : WithTop α<VAR>self : Ordnode.Valid' lo t hi<GOAL>t.Balanced
<VAR>α : Type u_1<VAR>Preorder α<VAR>lo : WithBot α<VAR>t : Ordnode α<VAR>hi : WithTop α<VAR>self : Ordnode.Valid' lo t hi<GOAL>t.Sized
<VAR>α : Type u_1<VAR>Preorder α<VAR>x y : α<VAR>xy : x ≤ y<VAR>t : Ordnode α<VAR>o : WithTop α<VAR>h : Ordnode.Valid' (↑y) t o<GOAL>Ordnode.Valid' (↑x) t o
<VAR>α : Type u_1<VAR>Preorder α<VAR>x y : α<VAR>xy : x ≤ y<VAR>t : Ordnode α<VAR>o : WithBot α<VAR>h : Ordnode.Valid' o t ↑x<GOAL>Ordnode.Valid' o t ↑y
<VAR>α : Type u_1<VAR>Preorder α<VAR>t₁ t₂ : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>h : t₁.Bounded o₁ ↑x<VAR>H : Ordnode.Valid' (↑x) t₂ o₂<GOAL>Ordnode.Valid' o₁ t₂ o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>t₁ t₂ : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>H : Ordnode.Valid' o₁ t₁ ↑x<VAR>h : t₂.Bounded (↑x) o₂<GOAL>Ordnode.Valid' o₁ t₁ o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>H : Ordnode.Valid' o₁ t o₂<VAR>h₁ : Ordnode.nil.Bounded o₁ ↑x<VAR>h₂ : Ordnode.All (fun x_1 => x_1 < x) t<GOAL>Ordnode.Valid' o₁ t ↑x
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>H : Ordnode.Valid' o₁ t o₂<VAR>h₁ : Ordnode.nil.Bounded (↑x) o₂<VAR>h₂ : Ordnode.All (fun x_1 => x_1 > x) t<GOAL>Ordnode.Valid' (↑x) t o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>h : Ordnode.Valid' o₁ t o₂<GOAL>t.Valid
<VAR>α : Type u_1<VAR>Preorder α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>h : Ordnode.nil.Bounded o₁ o₂<GOAL>Ordnode.Valid' o₁ Ordnode.nil o₂
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Ordnode.nil.Valid
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l ↑x<VAR>hr : Ordnode.Valid' (↑x) r o₂<VAR>H : Ordnode.BalancedSz l.size r.size<VAR>hs : s = l.size + r.size + 1<GOAL>Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<GOAL>Ordnode.Valid' o₁ t o₂ → Ordnode.Valid' o₂ t.dual o₁
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<GOAL>Ordnode.Valid' o₁ t o₂ ↔ Ordnode.Valid' o₂ t.dual o₁
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<GOAL>t.Valid → t.dual.Valid
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<GOAL>t.Valid ↔ t.dual.Valid
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>H : Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂<GOAL>Ordnode.Valid' o₁ l ↑x
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>H : Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂<GOAL>Ordnode.Valid' (↑x) r o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>H : (Ordnode.node s l x r).Valid<GOAL>l.Valid
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>H : (Ordnode.node s l x r).Valid<GOAL>r.Valid
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>H : (Ordnode.node s l x r).Valid<GOAL>(Ordnode.node s l x r).size = l.size + r.size + 1
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l ↑x<VAR>hr : Ordnode.Valid' (↑x) r o₂<VAR>H : Ordnode.BalancedSz l.size r.size<GOAL>Ordnode.Valid' o₁ (l.node' x r) o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>h₁ : Ordnode.nil.Bounded o₁ ↑x<VAR>h₂ : Ordnode.nil.Bounded (↑x) o₂<GOAL>Ordnode.Valid' o₁ {x} o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>x : α<GOAL>{x}.Valid
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l ↑x<VAR>hm : Ordnode.Valid' (↑x) m ↑y<VAR>hr : Ordnode.Valid' (↑y) r o₂<VAR>H1 : Ordnode.BalancedSz l.size m.size<VAR>H2 : Ordnode.BalancedSz (l.size + m.size + 1) r.size<GOAL>Ordnode.Valid' o₁ (l.node3L x m y r) o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l ↑x<VAR>hm : Ordnode.Valid' (↑x) m ↑y<VAR>hr : Ordnode.Valid' (↑y) r o₂<VAR>H1 : Ordnode.BalancedSz l.size (m.size + r.size + 1)<VAR>H2 : Ordnode.BalancedSz m.size r.size<GOAL>Ordnode.Valid' o₁ (l.node3R x m y r) o₂
<VAR>a b c d : ℕ<VAR>lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9<VAR>mr₂ : b + c + 1 ≤ 3 * d<VAR>mm₁ : b ≤ 3 * c<GOAL>b < 3 * a + 1
<VAR>b c d : ℕ<VAR>mr₂ : b + c + 1 ≤ 3 * d<GOAL>c ≤ 3 * d
<VAR>b c d : ℕ<VAR>mr₁ : 2 * d ≤ b + c + 1<VAR>mm₁ : b ≤ 3 * c<GOAL>d ≤ 3 * c
<VAR>a b c d : ℕ<VAR>lr₁ : 3 * a ≤ b + c + 1 + d<VAR>mr₂ : b + c + 1 ≤ 3 * d<VAR>mm₁ : b ≤ 3 * c<GOAL>a + b + 1 ≤ 3 * (c + d + 1)
<VAR>a b c d : ℕ<VAR>lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9<VAR>mr₁ : 2 * d ≤ b + c + 1<VAR>mm₂ : c ≤ 3 * b<GOAL>c + d + 1 ≤ 3 * (a + b + 1)
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l ↑x<VAR>hm : Ordnode.Valid' (↑x) m ↑y<VAR>hr : Ordnode.Valid' (↑y) r o₂<VAR>Hm : 0 < m.size<VAR>H : l.size = 0 ∧ m.size = 1 ∧ r.size ≤ 1 ∨ 0 < l.size ∧ Ordnode.ratio * r.size ≤ m.size ∧ Ordnode.delta * l.size ≤ m.size + r.size ∧ 3 * (m.size + r.size) ≤ 16 * l.size + 9 ∧ m.size ≤ Ordnode.delta * r.size<GOAL>Ordnode.Valid' o₁ (l.node4L x m y r) o₂
<VAR>a b c : ℕ<VAR>H2 : 3 * a ≤ b + c<VAR>hb₂ : c ≤ 3 * b<GOAL>a ≤ 3 * b
<VAR>a b c : ℕ<VAR>H3 : 2 * (b + c) ≤ 9 * a + 3<VAR>h : b < 2 * c<GOAL>b < 3 * a + 1
<VAR>a b c : ℕ<VAR>H2 : 3 * a ≤ b + c<VAR>h : b < 2 * c<GOAL>a + b < 3 * c
<VAR>a b : ℕ<VAR>H3 : 2 * b ≤ 9 * a + 3<GOAL>3 * b ≤ 16 * a + 9
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l ↑x<VAR>hr : Ordnode.Valid' (↑x) r o₂<VAR>H1 : ¬l.size + r.size ≤ 1<VAR>H2 : Ordnode.delta * l.size < r.size<VAR>H3 : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3<GOAL>Ordnode.Valid' o₁ (l.rotateL x r) o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l ↑x<VAR>hr : Ordnode.Valid' (↑x) r o₂<VAR>H1 : ¬l.size + r.size ≤ 1<VAR>H2 : Ordnode.delta * r.size < l.size<VAR>H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<GOAL>Ordnode.Valid' o₁ (l.rotateR x r) o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l ↑x<VAR>hr : Ordnode.Valid' (↑x) r o₂<VAR>H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3<VAR>H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<GOAL>Ordnode.Valid' o₁ (l.balance' x r) o₂
<VAR>α : Type u_2<VAR>l : Ordnode α<VAR>l' : ℕ<VAR>r : Ordnode α<VAR>r' : ℕ<VAR>H1 : Ordnode.BalancedSz l' r'<VAR>H2 : l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l'<GOAL>2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l ↑x<VAR>hr : Ordnode.Valid' (↑x) r o₂<VAR>H : ∃ l' r', Ordnode.BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')<GOAL>Ordnode.Valid' o₁ (l.balance' x r) o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l ↑x<VAR>hr : Ordnode.Valid' (↑x) r o₂<VAR>H : ∃ l' r', Ordnode.BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')<GOAL>Ordnode.Valid' o₁ (l.balance x r) o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l ↑x<VAR>hr : Ordnode.Valid' (↑x) r o₂<VAR>H₁ : l.size = 0 → r.size ≤ 1<VAR>H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ Ordnode.delta * l.size<VAR>H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<GOAL>Ordnode.Valid' o₁ (l.balanceL x r) o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l ↑x<VAR>hr : Ordnode.Valid' (↑x) r o₂<VAR>H : (∃ l', Ordnode.Raised l' l.size ∧ Ordnode.BalancedSz l' r.size) ∨ ∃ r', Ordnode.Raised r.size r' ∧ Ordnode.BalancedSz l.size r'<GOAL>Ordnode.Valid' o₁ (l.balanceL x r) o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l ↑x<VAR>hr : Ordnode.Valid' (↑x) r o₂<VAR>H₁ : r.size = 0 → l.size ≤ 1<VAR>H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ Ordnode.delta * r.size<VAR>H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3<GOAL>Ordnode.Valid' o₁ (l.balanceR x r) o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l ↑x<VAR>hr : Ordnode.Valid' (↑x) r o₂<VAR>H : (∃ l', Ordnode.Raised l.size l' ∧ Ordnode.BalancedSz l' r.size) ∨ ∃ r', Ordnode.Raised r' r.size ∧ Ordnode.BalancedSz l.size r'<GOAL>Ordnode.Valid' o₁ (l.balanceR x r) o₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>H : Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂<GOAL>Ordnode.Valid' o₁ (l.node' x r).eraseMax ↑(Ordnode.findMax' x r) ∧ (l.node' x r).size = (l.node' x r).eraseMax.size + 1
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>H : Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂<GOAL>Ordnode.Valid' (↑(l.findMin' x)) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<GOAL>t.Valid → t.eraseMin.Valid
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Ordnode α<VAR>h : t.Valid<GOAL>t.eraseMax.Valid
<VAR>α : Type u_1<VAR>Preorder α<VAR>l r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l o₂<VAR>hr : Ordnode.Valid' o₁ r o₂<VAR>sep : Ordnode.All (fun x => Ordnode.All (fun y => x < y) r) l<VAR>bal : Ordnode.BalancedSz l.size r.size<GOAL>Ordnode.Valid' o₁ (l.glue r) o₂ ∧ (l.glue r).size = l.size + r.size
<VAR>α : Type u_1<VAR>Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l ↑x<VAR>hr : Ordnode.Valid' (↑x) r o₂<GOAL>Ordnode.BalancedSz l.size r.size → Ordnode.Valid' o₁ (l.glue r) o₂ ∧ (l.glue r).size = l.size + r.size
<VAR>a b c : ℕ<VAR>h₁ : 3 * a < b + c + 1<VAR>h₂ : b ≤ 3 * c<GOAL>2 * (a + b) ≤ 9 * c + 5
<VAR>α : Type u_1<VAR>Preorder α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>ls : ℕ<VAR>ll : Ordnode α<VAR>lx : α<VAR>lr : Ordnode α<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr t : Ordnode α<VAR>hl : Ordnode.Valid' o₁ (Ordnode.node ls ll lx lr) o₂<VAR>hr : Ordnode.Valid' o₁ (Ordnode.node rs rl rx rr) o₂<VAR>h : Ordnode.delta * ls < rs<VAR>v : Ordnode.Valid' o₁ t ↑rx<VAR>e : t.size = ls + rl.size<GOAL>Ordnode.Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
<VAR>α : Type u_1<VAR>Preorder α<VAR>l r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Ordnode.Valid' o₁ l o₂<VAR>hr : Ordnode.Valid' o₁ r o₂<VAR>sep : Ordnode.All (fun x => Ordnode.All (fun y => x < y) r) l<GOAL>Ordnode.Valid' o₁ (l.merge r) o₂ ∧ (l.merge r).size = l.size + r.size
<VAR>α : Type u_1<VAR>Preorder α<VAR>l r : Ordnode α<VAR>hl : l.Valid<VAR>hr : r.Valid<VAR>sep : Ordnode.All (fun x => Ordnode.All (fun y => x < y) r) l<GOAL>(l.merge r).Valid
<VAR>α : Type u_1<VAR>Preorder α<VAR>IsTotal α fun x x_1 => x ≤ x_1<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>f : α → α<VAR>x : α<VAR>hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<GOAL>Ordnode.Valid' o₁ t o₂ → Ordnode.nil.Bounded o₁ ↑x → Ordnode.nil.Bounded (↑x) o₂ → Ordnode.Valid' o₁ (Ordnode.insertWith f x t) o₂ ∧ Ordnode.Raised t.size (Ordnode.insertWith f x t).size
<VAR>α : Type u_1<VAR>Preorder α<VAR>IsTotal α fun x x_1 => x ≤ x_1<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>f : α → α<VAR>x : α<VAR>hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x<VAR>t : Ordnode α<VAR>h : t.Valid<GOAL>(Ordnode.insertWith f x t).Valid
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>t : Ordnode α<GOAL>Ordnode.insert x t = Ordnode.insertWith (fun x_1 => x) x t
<VAR>α : Type u_1<VAR>Preorder α<VAR>IsTotal α fun x x_1 => x ≤ x_1<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>t : Ordnode α<VAR>h : t.Valid<GOAL>(Ordnode.insert x t).Valid
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>t : Ordnode α<GOAL>Ordnode.insert' x t = Ordnode.insertWith id x t
<VAR>α : Type u_1<VAR>Preorder α<VAR>IsTotal α fun x x_1 => x ≤ x_1<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>t : Ordnode α<VAR>h : t.Valid<GOAL>(Ordnode.insert' x t).Valid
<VAR>α : Type u_1<VAR>Preorder α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>f_strict_mono : StrictMono f<VAR>t : Ordnode α<VAR>a₁ : WithBot α<VAR>a₂ : WithTop α<VAR>h : Ordnode.Valid' a₁ t a₂<GOAL>Ordnode.Valid' (Option.map f a₁) (Ordnode.map f t) (Option.map f a₂) ∧ (Ordnode.map f t).size = t.size
<VAR>α : Type u_1<VAR>Preorder α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>f_strict_mono : StrictMono f<VAR>t : Ordnode α<VAR>h : t.Valid<GOAL>(Ordnode.map f t).Valid
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>t : Ordnode α<VAR>a₁ : WithBot α<VAR>a₂ : WithTop α<VAR>h : Ordnode.Valid' a₁ t a₂<GOAL>Ordnode.Valid' a₁ (Ordnode.erase x t) a₂ ∧ Ordnode.Raised (Ordnode.erase x t).size t.size
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>t : Ordnode α<VAR>h : t.Valid<GOAL>(Ordnode.erase x t).Valid
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>t : Ordnode α<VAR>a₁ : WithBot α<VAR>a₂ : WithTop α<VAR>h : Ordnode.Valid' a₁ t a₂<VAR>h_mem : x ∈ t<GOAL>(Ordnode.erase x t).size = t.size - 1
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Ordset α<GOAL>s = ∅ ↔ (↑s).empty = true
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>t : Ordset α<VAR>h_mem : x ∈ t<GOAL>0 < t.size
<VAR>abv : ℚ → ℚ<VAR>IsAbsoluteValue abv<VAR>q : ℚ<GOAL>CauSeq.Completion.ofRat q = ↑q
<VAR>x y : ℝ<GOAL>x = y ↔ x.cauchy = y.cauchy
<VAR>x y : ℝ<GOAL>x.cauchy = y.cauchy → x = y
<GOAL>∀ (x x_1 : ℝ), Real.add x x_1 = match x, x_1 with | { cauchy := a }, { cauchy := b } => { cauchy := a + b }
<GOAL>∀ (x : ℝ), Real.neg x = match x with | { cauchy := a } => { cauchy := -a }
<GOAL>∀ (x x_1 : ℝ), Real.mul x x_1 = match x, x_1 with | { cauchy := a }, { cauchy := b } => { cauchy := a * b }
<GOAL>∀ (x : ℝ), Real.inv' x = match x with | { cauchy := a } => { cauchy := a⁻¹ }
<VAR>a b : CauSeq.Completion.Cauchy abs<GOAL>{ cauchy := a + b } = { cauchy := a } + { cauchy := b }
<VAR>a : CauSeq.Completion.Cauchy abs<GOAL>{ cauchy := -a } = -{ cauchy := a }
<VAR>a b : CauSeq.Completion.Cauchy abs<GOAL>{ cauchy := a - b } = { cauchy := a } - { cauchy := b }
<VAR>a b : CauSeq.Completion.Cauchy abs<GOAL>{ cauchy := a * b } = { cauchy := a } * { cauchy := b }
<VAR>f : CauSeq.Completion.Cauchy abs<GOAL>{ cauchy := f⁻¹ } = { cauchy := f }⁻¹
<VAR>a b : ℝ<GOAL>(a + b).cauchy = a.cauchy + b.cauchy
<VAR>a : ℝ<GOAL>(-a).cauchy = -a.cauchy
<VAR>a b : ℝ<GOAL>(a * b).cauchy = a.cauchy * b.cauchy
<VAR>a b : ℝ<GOAL>(a - b).cauchy = a.cauchy - b.cauchy
<VAR>f : ℝ<GOAL>f⁻¹.cauchy = f.cauchy⁻¹
<VAR>n : ℕ<GOAL>{ cauchy := ↑n } = ↑n
<VAR>z : ℤ<GOAL>{ cauchy := ↑z } = ↑z
<VAR>q : ℚ≥0<GOAL>{ cauchy := ↑q } = ↑q
<VAR>q : ℚ<GOAL>{ cauchy := ↑q } = ↑q
<VAR>n : ℕ<GOAL>(↑n).cauchy = ↑n
<VAR>z : ℤ<GOAL>(↑z).cauchy = ↑z
<VAR>q : ℚ≥0<GOAL>(↑q).cauchy = ↑q
<VAR>q : ℚ<GOAL>(↑q).cauchy = ↑q
<VAR>cauchy : CauSeq.Completion.Cauchy abs<GOAL>(Real.ringEquivCauchy.symm cauchy).cauchy = cauchy
<VAR>self : ℝ<GOAL>Real.ringEquivCauchy self = self.cauchy
<VAR>f g : CauSeq ℚ abs<GOAL>Real.mk f = Real.mk g ↔ f ≈ g
<GOAL>∀ (x x_1 : ℝ), Real.lt x x_1 = match x, x_1 with | { cauchy := x }, { cauchy := y } => Quotient.liftOn₂ x y (fun x x_2 => x < x_2) Real.definition.proof_1✝
<VAR>f g : CauSeq ℚ abs<GOAL>{ cauchy := ⟦f⟧ } < { cauchy := ⟦g⟧ } ↔ f < g
<VAR>f g : CauSeq ℚ abs<GOAL>Real.mk f < Real.mk g ↔ f < g
<VAR>f g : CauSeq ℚ abs<GOAL>Real.mk (f + g) = Real.mk f + Real.mk g
<VAR>f g : CauSeq ℚ abs<GOAL>Real.mk (f * g) = Real.mk f * Real.mk g
<VAR>f : CauSeq ℚ abs<GOAL>Real.mk (-f) = -Real.mk f
<VAR>f : CauSeq ℚ abs<GOAL>0 < Real.mk f ↔ f.Pos
<VAR>x y : ℝ<GOAL>Real.le x y = (x < y ∨ x = y)
<VAR>x y : ℝ<GOAL>x ≤ y ↔ x < y ∨ x = y
<VAR>f g : CauSeq ℚ abs<GOAL>Real.mk f ≤ Real.mk g ↔ f ≤ g
<VAR>C : ℝ → Prop<VAR>x : ℝ<VAR>h : ∀ (y : CauSeq ℚ abs), C (Real.mk y)<GOAL>C x
<VAR>a b : ℝ<VAR>c : ℝ<GOAL>c + a < c + b ↔ a < b
<VAR>x y : ℚ<GOAL>↑x < ↑y ↔ x < y
<VAR>a b : ℝ<GOAL>0 < a → 0 < b → 0 < a * b
<GOAL>∀ (x x_1 : ℝ), Real.sup x x_1 = match x, x_1 with | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x x_2 => x ⊔ x_2) ⋯ x y }
<VAR>a b : CauSeq ℚ abs<GOAL>{ cauchy := ⟦a ⊔ b⟧ } = { cauchy := ⟦a⟧ } ⊔ { cauchy := ⟦b⟧ }
<VAR>a b : CauSeq ℚ abs<GOAL>Real.mk (a ⊔ b) = Real.mk a ⊔ Real.mk b
<GOAL>∀ (x x_1 : ℝ), Real.inf x x_1 = match x, x_1 with | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x x_2 => x ⊓ x_2) ⋯ x y }
<VAR>a b : CauSeq ℚ abs<GOAL>{ cauchy := ⟦a ⊓ b⟧ } = { cauchy := ⟦a⟧ } ⊓ { cauchy := ⟦b⟧ }
<VAR>a b : CauSeq ℚ abs<GOAL>Real.mk (a ⊓ b) = Real.mk a ⊓ Real.mk b
<VAR>f g : CauSeq.Completion.Cauchy abs<GOAL>{ cauchy := f / g } = { cauchy := f } / { cauchy := g }
<VAR>x : ℝ<VAR>f : CauSeq ℚ abs<GOAL>(∃ i, ∀ j ≥ i, x ≤ ↑(↑f j)) → x ≤ Real.mk f
<VAR>f : CauSeq ℚ abs<VAR>x : ℝ<VAR>h : ∃ i, ∀ j ≥ i, ↑(↑f j) ≤ x<GOAL>Real.mk f ≤ x
<VAR>f : CauSeq ℚ abs<VAR>x ε : ℝ<VAR>H : ∃ i, ∀ j ≥ i, |↑(↑f j) - x| ≤ ε<GOAL>|Real.mk f - x| ≤ ε
<VAR>n : ℕ<GOAL>2 ^ (n + 1) * √(2 - Real.sqrtTwoAddSeries 0 n) < π
<VAR>n : ℕ<GOAL>π < 2 ^ (n + 1) * √(2 - Real.sqrtTwoAddSeries 0 n) + 1 / 4 ^ n
<VAR>c d : ℕ<VAR>a b n : ℕ<VAR>z : ℝ<VAR>hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b<GOAL>(↑a / ↑b).sqrtTwoAddSeries (n + 1) ≤ z
<VAR>a b : ℕ<VAR>c d n : ℕ<VAR>z : ℝ<VAR>hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2<GOAL>z ≤ (↑c / ↑d).sqrtTwoAddSeries (n + 1)
<GOAL>Filter.Tendsto (fun k => ∑ i ∈ Finset.range k, (-1) ^ i / (2 * ↑i + 1)) Filter.atTop (nhds (Real.pi / 4))
<VAR>n : ℝ≥0<GOAL>↑n = ↑n
<VAR>n m : ℝ≥0<GOAL>↑n = ↑m → n = m
<VAR>n m : ℝ≥0<GOAL>n = m ↔ ↑n = ↑m
<VAR>x y : ℝ≥0<GOAL>↑x ≠ ↑y ↔ x ≠ y
<VAR>p : ℝ≥0 → Prop<GOAL>(∀ (x : ℝ≥0), p x) ↔ ∀ (x : ℝ) (hx : 0 ≤ x), p ⟨x, hx⟩
<VAR>p : ℝ≥0 → Prop<GOAL>(∃ x, p x) ↔ ∃ x, ∃ (hx : 0 ≤ x), p ⟨x, hx⟩
<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>↑r.toNNReal = r
<VAR>r : ℝ<GOAL>r ≤ ↑r.toNNReal
<VAR>r : ℝ≥0<GOAL>0 ≤ ↑r
<VAR>a : ℝ<VAR>ha : 0 ≤ a<GOAL>↑⟨a, ha⟩ = a
<VAR>r₁ r₂ : ℝ≥0<GOAL>↑r₁ = ↑r₂ ↔ r₁ = r₂
<VAR>r₁ r₂ : ℝ≥0<GOAL>↑(r₁ + r₂) = ↑r₁ + ↑r₂
<VAR>r₁ r₂ : ℝ≥0<GOAL>↑(r₁ * r₂) = ↑r₁ * ↑r₂
<VAR>r : ℝ≥0<GOAL>↑r⁻¹ = (↑r)⁻¹
<VAR>r₁ r₂ : ℝ≥0<GOAL>↑(r₁ / r₂) = ↑r₁ / ↑r₂
<VAR>r₁ r₂ : ℝ≥0<VAR>h : r₂ ≤ r₁<GOAL>↑(r₁ - r₂) = ↑r₁ - ↑r₂
<GOAL>⇑NNReal.toRealHom = NNReal.toReal
<VAR>M : Type u_1<VAR>MulAction ℝ M<VAR>c : ℝ≥0<VAR>x : M<GOAL>c • x = ↑c • x
<VAR>α : Type u_1<VAR>s : Set α<VAR>f : α → ℝ≥0<VAR>a : α<GOAL>↑(s.indicator f a) = s.indicator (fun x => ↑(f x)) a
<VAR>r : ℝ≥0<VAR>n : ℕ<GOAL>↑(r ^ n) = ↑r ^ n
<VAR>r : ℝ≥0<VAR>n : ℤ<GOAL>↑(r ^ n) = ↑r ^ n
<VAR>l : List ℝ≥0<GOAL>↑l.sum = (List.map NNReal.toReal l).sum
<VAR>l : List ℝ≥0<GOAL>↑l.prod = (List.map NNReal.toReal l).prod
<VAR>s : Multiset ℝ≥0<GOAL>↑s.sum = (Multiset.map NNReal.toReal s).sum
<VAR>s : Multiset ℝ≥0<GOAL>↑s.prod = (Multiset.map NNReal.toReal s).prod