case nil
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Valid' a₁ nil a₂
case nil
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Valid' a₁ (erase x nil) a₂ ∧ Raised (size (erase x nil)) (size nil)
simp [erase, Raised]
no goals
case nil
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Valid' a₁ nil a₂
exact h
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_l a₂ → Valid' a₁ (erase x t_l) a₂ ∧ Raised (size (erase x t_l)) (size t_l)
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (size (erase x t_r)) (size t_r)
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match cmpLE x t_x with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      size✝
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_l a₂ → Valid' a₁ (erase x t_l) a₂ ∧ Raised (size (erase x t_l)) (size t_l)
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (size (erase x t_r)) (size t_r)
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
⊢ Valid' a₁ (erase x (Ordnode.node size✝ t_l t_x t_r)) a₂ ∧
    Raised (size (erase x (Ordnode.node size✝ t_l t_x t_r))) (size (Ordnode.node size✝ t_l t_x t_r))
simp [erase]
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_l a₂ → Valid' a₁ (erase x t_l) a₂ ∧ Raised (size (erase x t_l)) (size t_l)
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (size (erase x t_r)) (size t_r)
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_ih_l' : Valid' a₁ (erase x t_l) ↑t_x ∧ Raised (size (erase x t_l)) (size t_l)
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match cmpLE x t_x with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      size✝
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_l a₂ → Valid' a₁ (erase x t_l) a₂ ∧ Raised (size (erase x t_l)) (size t_l)
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (size (erase x t_r)) (size t_r)
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match cmpLE x t_x with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      size✝
have t_ih_l' := t_ih_l h.left
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_l a₂ → Valid' a₁ (erase x t_l) a₂ ∧ Raised (size (erase x t_l)) (size t_l)
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (size (erase x t_r)) (size t_r)
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_ih_l' : Valid' a₁ (erase x t_l) ↑t_x ∧ Raised (size (erase x t_l)) (size t_l)
t_ih_r' : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (size (erase x t_r)) (size t_r)
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match cmpLE x t_x with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      size✝
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_l a₂ → Valid' a₁ (erase x t_l) a₂ ∧ Raised (size (erase x t_l)) (size t_l)
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (size (erase x t_r)) (size t_r)
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_ih_l' : Valid' a₁ (erase x t_l) ↑t_x ∧ Raised (size (erase x t_l)) (size t_l)
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match cmpLE x t_x with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      size✝
have t_ih_r' := t_ih_r h.right
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_ih_l' : Valid' a₁ (erase x t_l) ↑t_x ∧ Raised (size (erase x t_l)) (size t_l)
t_ih_r' : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (size (erase x t_r)) (size t_r)
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match cmpLE x t_x with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      size✝
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_l a₂ → Valid' a₁ (erase x t_l) a₂ ∧ Raised (size (erase x t_l)) (size t_l)
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (size (erase x t_r)) (size t_r)
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_ih_l' : Valid' a₁ (erase x t_l) ↑t_x ∧ Raised (size (erase x t_l)) (size t_l)
t_ih_r' : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (size (erase x t_r)) (size t_r)
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match cmpLE x t_x with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      size✝
clear t_ih_l t_ih_r
case node.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_ih_r' : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (size (erase x t_r)) (size t_r)
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match cmpLE x t_x with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      size✝
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_ih_l' : Valid' a₁ (erase x t_l) ↑t_x ∧ Raised (size (erase x t_l)) (size t_l)
t_ih_r' : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (size (erase x t_r)) (size t_r)
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match cmpLE x t_x with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      size✝
cases' t_ih_l' with t_l_valid t_l_size
case node.intro.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match cmpLE x t_x with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      size✝
case node.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_ih_r' : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (size (erase x t_r)) (size t_r)
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match cmpLE x t_x with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      size✝
cases' t_ih_r' with t_r_valid t_r_size
case node.intro.intro.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ Valid' a₁
      (match Ordering.lt with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match Ordering.lt with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      (size t_l + size t_r + 1)

case node.intro.intro.eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ Valid' a₁
      (match Ordering.eq with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match Ordering.eq with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      (size t_l + size t_r + 1)

case node.intro.intro.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ Valid' a₁
      (match Ordering.gt with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match Ordering.gt with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      (size t_l + size t_r + 1)
case node.intro.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match cmpLE x t_x with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      size✝
cases cmpLE x t_x <;> rw [h.sz.1]
case node.intro.intro.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable : ?m.383765
⊢ Valid' a₁
      (match Ordering.lt with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match Ordering.lt with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      (size t_l + size t_r + 1)

case h_balanceable
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ ?m.383765
case node.intro.intro.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ Valid' a₁
      (match Ordering.lt with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match Ordering.lt with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      (size t_l + size t_r + 1)
suffices h_balanceable
case node.intro.intro.lt.left
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable : ?m.383765
⊢ Valid' a₁
    (match Ordering.lt with
    | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
    | Ordering.eq => Ordnode.glue t_l t_r
    | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
    a₂

case node.intro.intro.lt.right
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable : ?m.383765
⊢ Raised
    (size
      (match Ordering.lt with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
    (size t_l + size t_r + 1)

case h_balanceable
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ ?m.383765
case node.intro.intro.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable : ?m.383765
⊢ Valid' a₁
      (match Ordering.lt with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match Ordering.lt with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      (size t_l + size t_r + 1)

case h_balanceable
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ ?m.383765
constructor
no goals
case node.intro.intro.lt.left
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable : ?m.383765
⊢ Valid' a₁
    (match Ordering.lt with
    | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
    | Ordering.eq => Ordnode.glue t_l t_r
    | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
    a₂
exact Valid'.balanceR t_l_valid h.right h_balanceable
case node.intro.intro.lt.right
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable :
  (∃ l', Raised (size (erase x t_l)) l' ∧ BalancedSz l' (size t_r)) ∨
    ∃ r', Raised r' (size t_r) ∧ BalancedSz (size (erase x t_l)) r'
⊢ Raised (size (erase x t_l) + size t_r + 1) (size t_l + size t_r + 1)
case node.intro.intro.lt.right
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable :
  (∃ l', Raised (size (erase x t_l)) l' ∧ BalancedSz l' (size t_r)) ∨
    ∃ r', Raised r' (size t_r) ∧ BalancedSz (size (erase x t_l)) r'
⊢ Raised
    (size
      (match Ordering.lt with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
    (size t_l + size t_r + 1)
rw [size_balanceR t_l_valid.bal h.right.bal t_l_valid.sz h.right.sz h_balanceable]
case node.intro.intro.lt.right.H.H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable :
  (∃ l', Raised (size (erase x t_l)) l' ∧ BalancedSz l' (size t_r)) ∨
    ∃ r', Raised r' (size t_r) ∧ BalancedSz (size (erase x t_l)) r'
⊢ Raised (size (erase x t_l)) (size t_l)
case node.intro.intro.lt.right
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable :
  (∃ l', Raised (size (erase x t_l)) l' ∧ BalancedSz l' (size t_r)) ∨
    ∃ r', Raised r' (size t_r) ∧ BalancedSz (size (erase x t_l)) r'
⊢ Raised (size (erase x t_l) + size t_r + 1) (size t_l + size t_r + 1)
repeat apply Raised.add_right
no goals
case node.intro.intro.lt.right.H.H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable :
  (∃ l', Raised (size (erase x t_l)) l' ∧ BalancedSz l' (size t_r)) ∨
    ∃ r', Raised r' (size t_r) ∧ BalancedSz (size (erase x t_l)) r'
⊢ Raised (size (erase x t_l)) (size t_l)
exact t_l_size
case node.intro.intro.lt.right.H.H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable :
  (∃ l', Raised (size (erase x t_l)) l' ∧ BalancedSz l' (size t_r)) ∨
    ∃ r', Raised r' (size t_r) ∧ BalancedSz (size (erase x t_l)) r'
⊢ Raised (size (erase x t_l)) (size t_l)
case node.intro.intro.lt.right.H.H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable :
  (∃ l', Raised (size (erase x t_l)) l' ∧ BalancedSz l' (size t_r)) ∨
    ∃ r', Raised r' (size t_r) ∧ BalancedSz (size (erase x t_l)) r'
⊢ Raised (size (erase x t_l)) (size t_l)
apply Raised.add_right
case h_balanceable.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ ∃ l', Raised (size (erase x t_l)) l' ∧ BalancedSz l' (size t_r)
case h_balanceable
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ (∃ l', Raised (size (erase x t_l)) l' ∧ BalancedSz l' (size t_r)) ∨
    ∃ r', Raised r' (size t_r) ∧ BalancedSz (size (erase x t_l)) r'
left
case h_balanceable.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ Raised (size (erase x t_l)) (size t_l) ∧ BalancedSz (size t_l) (size t_r)
case h_balanceable.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ ∃ l', Raised (size (erase x t_l)) l' ∧ BalancedSz l' (size t_r)
exists t_l.size
no goals
case h_balanceable.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ Raised (size (erase x t_l)) (size t_l) ∧ BalancedSz (size t_l) (size t_r)
exact And.intro t_l_size h.bal.1
case node.intro.intro.eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_glue : Valid' a₁ (Ordnode.glue t_l t_r) a₂ ∧ size (Ordnode.glue t_l t_r) = size t_l + size t_r
⊢ Valid' a₁
      (match Ordering.eq with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match Ordering.eq with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      (size t_l + size t_r + 1)
case node.intro.intro.eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ Valid' a₁
      (match Ordering.eq with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match Ordering.eq with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      (size t_l + size t_r + 1)
have h_glue := Valid'.glue h.left h.right h.bal.1
case node.intro.intro.eq.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_glue_valid : Valid' a₁ (Ordnode.glue t_l t_r) a₂
h_glue_sized : size (Ordnode.glue t_l t_r) = size t_l + size t_r
⊢ Valid' a₁
      (match Ordering.eq with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match Ordering.eq with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      (size t_l + size t_r + 1)
case node.intro.intro.eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_glue : Valid' a₁ (Ordnode.glue t_l t_r) a₂ ∧ size (Ordnode.glue t_l t_r) = size t_l + size t_r
⊢ Valid' a₁
      (match Ordering.eq with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match Ordering.eq with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      (size t_l + size t_r + 1)
cases' h_glue with h_glue_valid h_glue_sized
case node.intro.intro.eq.intro.left
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_glue_valid : Valid' a₁ (Ordnode.glue t_l t_r) a₂
h_glue_sized : size (Ordnode.glue t_l t_r) = size t_l + size t_r
⊢ Valid' a₁
    (match Ordering.eq with
    | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
    | Ordering.eq => Ordnode.glue t_l t_r
    | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
    a₂

case node.intro.intro.eq.intro.right
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_glue_valid : Valid' a₁ (Ordnode.glue t_l t_r) a₂
h_glue_sized : size (Ordnode.glue t_l t_r) = size t_l + size t_r
⊢ Raised
    (size
      (match Ordering.eq with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
    (size t_l + size t_r + 1)
case node.intro.intro.eq.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_glue_valid : Valid' a₁ (Ordnode.glue t_l t_r) a₂
h_glue_sized : size (Ordnode.glue t_l t_r) = size t_l + size t_r
⊢ Valid' a₁
      (match Ordering.eq with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match Ordering.eq with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      (size t_l + size t_r + 1)
constructor
no goals
case node.intro.intro.eq.intro.left
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_glue_valid : Valid' a₁ (Ordnode.glue t_l t_r) a₂
h_glue_sized : size (Ordnode.glue t_l t_r) = size t_l + size t_r
⊢ Valid' a₁
    (match Ordering.eq with
    | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
    | Ordering.eq => Ordnode.glue t_l t_r
    | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
    a₂
exact h_glue_valid
case node.intro.intro.eq.intro.right.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_glue_valid : Valid' a₁ (Ordnode.glue t_l t_r) a₂
h_glue_sized : size (Ordnode.glue t_l t_r) = size t_l + size t_r
⊢ size t_l + size t_r + 1 =
    size
        (match Ordering.eq with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)) +
      1
case node.intro.intro.eq.intro.right
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_glue_valid : Valid' a₁ (Ordnode.glue t_l t_r) a₂
h_glue_sized : size (Ordnode.glue t_l t_r) = size t_l + size t_r
⊢ Raised
    (size
      (match Ordering.eq with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
    (size t_l + size t_r + 1)
right
no goals
case node.intro.intro.eq.intro.right.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_glue_valid : Valid' a₁ (Ordnode.glue t_l t_r) a₂
h_glue_sized : size (Ordnode.glue t_l t_r) = size t_l + size t_r
⊢ size t_l + size t_r + 1 =
    size
        (match Ordering.eq with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)) +
      1
rw [h_glue_sized]
case node.intro.intro.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable : ?m.384378
⊢ Valid' a₁
      (match Ordering.gt with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match Ordering.gt with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      (size t_l + size t_r + 1)

case h_balanceable
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ ?m.384378
case node.intro.intro.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ Valid' a₁
      (match Ordering.gt with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match Ordering.gt with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      (size t_l + size t_r + 1)
suffices h_balanceable
case node.intro.intro.gt.left
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable : ?m.384378
⊢ Valid' a₁
    (match Ordering.gt with
    | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
    | Ordering.eq => Ordnode.glue t_l t_r
    | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
    a₂

case node.intro.intro.gt.right
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable : ?m.384378
⊢ Raised
    (size
      (match Ordering.gt with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
    (size t_l + size t_r + 1)

case h_balanceable
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ ?m.384378
case node.intro.intro.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable : ?m.384378
⊢ Valid' a₁
      (match Ordering.gt with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
      a₂ ∧
    Raised
      (size
        (match Ordering.gt with
        | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
        | Ordering.eq => Ordnode.glue t_l t_r
        | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
      (size t_l + size t_r + 1)

case h_balanceable
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ ?m.384378
constructor
no goals
case node.intro.intro.gt.left
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable : ?m.384378
⊢ Valid' a₁
    (match Ordering.gt with
    | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
    | Ordering.eq => Ordnode.glue t_l t_r
    | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r))
    a₂
exact Valid'.balanceL h.left t_r_valid h_balanceable
case node.intro.intro.gt.right
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable :
  (∃ l', Raised l' (size t_l) ∧ BalancedSz l' (size (erase x t_r))) ∨
    ∃ r', Raised (size (erase x t_r)) r' ∧ BalancedSz (size t_l) r'
⊢ Raised (size t_l + size (erase x t_r) + 1) (size t_l + size t_r + 1)
case node.intro.intro.gt.right
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable :
  (∃ l', Raised l' (size t_l) ∧ BalancedSz l' (size (erase x t_r))) ∨
    ∃ r', Raised (size (erase x t_r)) r' ∧ BalancedSz (size t_l) r'
⊢ Raised
    (size
      (match Ordering.gt with
      | Ordering.lt => Ordnode.balanceR (erase x t_l) t_x t_r
      | Ordering.eq => Ordnode.glue t_l t_r
      | Ordering.gt => Ordnode.balanceL t_l t_x (erase x t_r)))
    (size t_l + size t_r + 1)
rw [size_balanceL h.left.bal t_r_valid.bal h.left.sz t_r_valid.sz h_balanceable]
case node.intro.intro.gt.right.H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable :
  (∃ l', Raised l' (size t_l) ∧ BalancedSz l' (size (erase x t_r))) ∨
    ∃ r', Raised (size (erase x t_r)) r' ∧ BalancedSz (size t_l) r'
⊢ Raised (size t_l + size (erase x t_r)) (size t_l + size t_r)
case node.intro.intro.gt.right
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable :
  (∃ l', Raised l' (size t_l) ∧ BalancedSz l' (size (erase x t_r))) ∨
    ∃ r', Raised (size (erase x t_r)) r' ∧ BalancedSz (size t_l) r'
⊢ Raised (size t_l + size (erase x t_r) + 1) (size t_l + size t_r + 1)
apply Raised.add_right
case node.intro.intro.gt.right.H.H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable :
  (∃ l', Raised l' (size t_l) ∧ BalancedSz l' (size (erase x t_r))) ∨
    ∃ r', Raised (size (erase x t_r)) r' ∧ BalancedSz (size t_l) r'
⊢ Raised (size (erase x t_r)) (size t_r)
case node.intro.intro.gt.right.H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable :
  (∃ l', Raised l' (size t_l) ∧ BalancedSz l' (size (erase x t_r))) ∨
    ∃ r', Raised (size (erase x t_r)) r' ∧ BalancedSz (size t_l) r'
⊢ Raised (size t_l + size (erase x t_r)) (size t_l + size t_r)
apply Raised.add_left
no goals
case node.intro.intro.gt.right.H.H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_balanceable :
  (∃ l', Raised l' (size t_l) ∧ BalancedSz l' (size (erase x t_r))) ∨
    ∃ r', Raised (size (erase x t_r)) r' ∧ BalancedSz (size t_l) r'
⊢ Raised (size (erase x t_r)) (size t_r)
exact t_r_size
case h_balanceable.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ ∃ r', Raised (size (erase x t_r)) r' ∧ BalancedSz (size t_l) r'
case h_balanceable
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ (∃ l', Raised l' (size t_l) ∧ BalancedSz l' (size (erase x t_r))) ∨
    ∃ r', Raised (size (erase x t_r)) r' ∧ BalancedSz (size t_l) r'
right
case h_balanceable.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ Raised (size (erase x t_r)) (size t_r) ∧ BalancedSz (size t_l) (size t_r)
case h_balanceable.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ ∃ r', Raised (size (erase x t_r)) r' ∧ BalancedSz (size t_l) r'
exists t_r.size
no goals
case h_balanceable.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ Raised (size (erase x t_r)) (size t_r) ∧ BalancedSz (size t_l) (size t_r)
exact And.intro t_r_size h.bal.1