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₂
h_mem : x ∈ nil
⊢ size (erase x nil) = size nil - 1
contradiction
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₂ → x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r : ∀ {a₁ : WithBot α} {a₂ : WithTop α}, Valid' a₁ t_r a₂ → x ∈ t_r → size (erase x t_r) = size t_r - 1
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : x ∈ node size✝ t_l t_x t_r
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
⊢ size (erase x (node size✝ t_l t_x t_r)) = size (node size✝ t_l t_x t_r) - 1
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₂ → x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r : ∀ {a₁ : WithBot α} {a₂ : WithTop α}, Valid' a₁ t_r a₂ → x ∈ t_r → size (erase x t_r) = size t_r - 1
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : x ∈ node size✝ t_l t_x t_r
⊢ size (erase x (node size✝ t_l t_x t_r)) = size (node size✝ t_l t_x t_r) - 1
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₂ → x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r : ∀ {a₁ : WithBot α} {a₂ : WithTop α}, Valid' a₁ t_r a₂ → x ∈ t_r → size (erase x t_r) = size t_r - 1
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : x ∈ node size✝ t_l t_x t_r
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
⊢ size (erase x (node size✝ t_l t_x t_r)) = size (node size✝ t_l t_x t_r) - 1
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₂ → x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r : ∀ {a₁ : WithBot α} {a₂ : WithTop α}, Valid' a₁ t_r a₂ → x ∈ t_r → size (erase x t_r) = size t_r - 1
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : x ∈ node size✝ t_l t_x t_r
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
⊢ size (erase x (node size✝ t_l t_x t_r)) = size (node size✝ t_l t_x t_r) - 1
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₁ (node size✝ t_l t_x t_r) a₂
h_mem : x ∈ node size✝ t_l t_x t_r
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
⊢ size (erase x (node size✝ t_l t_x t_r)) = size (node size✝ t_l t_x t_r) - 1
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₂ → x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r : ∀ {a₁ : WithBot α} {a₂ : WithTop α}, Valid' a₁ t_r a₂ → x ∈ t_r → size (erase x t_r) = size t_r - 1
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : x ∈ node size✝ t_l t_x t_r
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
⊢ size (erase x (node size✝ t_l t_x t_r)) = size (node size✝ t_l t_x t_r) - 1
clear t_ih_l t_ih_r
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₁ (node size✝ t_l t_x t_r) a₂
h_mem :
  (match cmpLE x t_x with
    | Ordering.lt => mem x t_l
    | Ordering.eq => true
    | Ordering.gt => mem x t_r) =
    true
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
⊢ size (erase x (node size✝ t_l t_x t_r)) = size (node size✝ t_l t_x t_r) - 1
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₁ (node size✝ t_l t_x t_r) a₂
h_mem : x ∈ node size✝ t_l t_x t_r
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
⊢ size (erase x (node size✝ t_l t_x t_r)) = size (node size✝ t_l t_x t_r) - 1
dsimp only [Membership.mem, mem] at h_mem
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₁ (node size✝ t_l t_x t_r) a₂
h_mem :
  (match cmpLE x t_x with
    | Ordering.lt => mem x t_l
    | Ordering.eq => true
    | Ordering.gt => mem x t_r) =
    true
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
⊢ size
      (match cmpLE x t_x with
      | Ordering.lt => balanceR (erase x t_l) t_x t_r
      | Ordering.eq => glue t_l t_r
      | Ordering.gt => balanceL t_l t_x (erase x t_r)) =
    size (node size✝ t_l t_x t_r) - 1
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₁ (node size✝ t_l t_x t_r) a₂
h_mem :
  (match cmpLE x t_x with
    | Ordering.lt => mem x t_l
    | Ordering.eq => true
    | Ordering.gt => mem x t_r) =
    true
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
⊢ size (erase x (node size✝ t_l t_x t_r)) = size (node size✝ t_l t_x t_r) - 1
unfold 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 α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
⊢ (match cmpLE x t_x with
      | Ordering.lt => mem x t_l
      | Ordering.eq => true
      | Ordering.gt => mem x t_r) =
      true →
    size
        (match cmpLE x t_x with
        | Ordering.lt => balanceR (erase x t_l) t_x t_r
        | Ordering.eq => glue t_l t_r
        | Ordering.gt => balanceL t_l t_x (erase x t_r)) =
      size (node size✝ t_l t_x t_r) - 1
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₁ (node size✝ t_l t_x t_r) a₂
h_mem :
  (match cmpLE x t_x with
    | Ordering.lt => mem x t_l
    | Ordering.eq => true
    | Ordering.gt => mem x t_r) =
    true
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
⊢ size
      (match cmpLE x t_x with
      | Ordering.lt => balanceR (erase x t_l) t_x t_r
      | Ordering.eq => glue t_l t_r
      | Ordering.gt => balanceL t_l t_x (erase x t_r)) =
    size (node size✝ t_l t_x t_r) - 1
revert h_mem
case node.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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
h_mem : mem x t_l = true
⊢ size (balanceR (erase x t_l) t_x t_r) = size (node size✝ t_l t_x t_r) - 1

case node.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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
h_mem : true = true
⊢ size (glue t_l t_r) = size (node size✝ t_l t_x t_r) - 1

case node.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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
h_mem : mem x t_r = true
⊢ size (balanceL t_l t_x (erase x t_r)) = size (node size✝ t_l t_x t_r) - 1
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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
⊢ (match cmpLE x t_x with
      | Ordering.lt => mem x t_l
      | Ordering.eq => true
      | Ordering.gt => mem x t_r) =
      true →
    size
        (match cmpLE x t_x with
        | Ordering.lt => balanceR (erase x t_l) t_x t_r
        | Ordering.eq => glue t_l t_r
        | Ordering.gt => balanceL t_l t_x (erase x t_r)) =
      size (node size✝ t_l t_x t_r) - 1
cases cmpLE x t_x <;> intro h_mem <;> dsimp only at h_mem ⊢
case node.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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
⊢ size (balanceR (erase x t_l) t_x t_r) = size (node size✝ t_l t_x t_r) - 1
case node.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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
h_mem : mem x t_l = true
⊢ size (balanceR (erase x t_l) t_x t_r) = size (node size✝ t_l t_x t_r) - 1
have t_ih_l := t_ih_l' h_mem
case node.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
⊢ size (balanceR (erase x t_l) t_x t_r) = size (node size✝ t_l t_x t_r) - 1
case node.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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
⊢ size (balanceR (erase x t_l) t_x t_r) = size (node size✝ t_l t_x t_r) - 1
clear t_ih_l' t_ih_r'
case node.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_h : Valid' a₁ (erase x t_l) ↑t_x ∧ Raised (size (erase x t_l)) (size t_l)
⊢ size (balanceR (erase x t_l) t_x t_r) = size (node size✝ t_l t_x t_r) - 1
case node.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
⊢ size (balanceR (erase x t_l) t_x t_r) = size (node size✝ t_l t_x t_r) - 1
have t_l_h := Valid'.erase_aux x h.left
case node.lt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
⊢ size (balanceR (erase x t_l) t_x t_r) = size (node size✝ t_l t_x t_r) - 1
case node.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_h : Valid' a₁ (erase x t_l) ↑t_x ∧ Raised (size (erase x t_l)) (size t_l)
⊢ size (balanceR (erase x t_l) t_x t_r) = size (node size✝ t_l t_x t_r) - 1
cases' t_l_h with t_l_valid t_l_size
case node.lt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
⊢ size (erase x t_l) + size t_r + 1 = size (node size✝ t_l t_x t_r) - 1
case node.lt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
⊢ size (balanceR (erase x t_l) t_x t_r) = size (node size✝ t_l t_x t_r) - 1
rw [size_balanceR t_l_valid.bal h.right.bal t_l_valid.sz h.right.sz
    (Or.inl (Exists.intro t_l.size (And.intro t_l_size h.bal.1)))]
case node.lt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
⊢ size t_l - 1 + size t_r + 1 = size (node (size t_l + size t_r + 1) t_l t_x t_r) - 1
case node.lt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
⊢ size (erase x t_l) + size t_r + 1 = size (node size✝ t_l t_x t_r) - 1
rw [t_ih_l, h.sz.1]
case node.lt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
h_pos_t_l_size : 0 < size t_l
⊢ size t_l - 1 + size t_r + 1 = size (node (size t_l + size t_r + 1) t_l t_x t_r) - 1
case node.lt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
⊢ size t_l - 1 + size t_r + 1 = size (node (size t_l + size t_r + 1) t_l t_x t_r) - 1
have h_pos_t_l_size := pos_size_of_mem h.left.sz h_mem
case node.lt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
⊢ 0 < size t_l → size t_l - 1 + size t_r + 1 = size (node (size t_l + size t_r + 1) t_l t_x t_r) - 1
case node.lt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
h_pos_t_l_size : 0 < size t_l
⊢ size t_l - 1 + size t_r + 1 = size (node (size t_l + size t_r + 1) t_l t_x t_r) - 1
revert h_pos_t_l_size
case node.lt.intro.zero
α : 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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
h_pos_t_l_size : 0 < Nat.zero
⊢ Nat.zero - 1 + size t_r + 1 = size (node (Nat.zero + size t_r + 1) t_l t_x t_r) - 1

case node.lt.intro.succ
α : 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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size✝ : Raised (size (erase x t_l)) (size t_l)
t_l_size : ℕ
h_pos_t_l_size : 0 < Nat.succ t_l_size
⊢ Nat.succ t_l_size - 1 + size t_r + 1 = size (node (Nat.succ t_l_size + size t_r + 1) t_l t_x t_r) - 1
case node.lt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
⊢ 0 < size t_l → size t_l - 1 + size t_r + 1 = size (node (size t_l + size t_r + 1) t_l t_x t_r) - 1
cases' t_l.size with t_l_size <;> intro h_pos_t_l_size
no goals
case node.lt.intro.zero
α : 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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (size (erase x t_l)) (size t_l)
h_pos_t_l_size : 0 < Nat.zero
⊢ Nat.zero - 1 + size t_r + 1 = size (node (Nat.zero + size t_r + 1) t_l t_x t_r) - 1
cases h_pos_t_l_size
no goals
case node.lt.intro.succ
α : 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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : size (erase x t_l) = size t_l - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size✝ : Raised (size (erase x t_l)) (size t_l)
t_l_size : ℕ
h_pos_t_l_size : 0 < Nat.succ t_l_size
⊢ Nat.succ t_l_size - 1 + size t_r + 1 = size (node (Nat.succ t_l_size + size t_r + 1) t_l t_x t_r) - 1
simp [Nat.succ_add]
case node.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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
h_mem : true = true
⊢ size t_l + size t_r = size (node (size t_l + size t_r + 1) t_l t_x t_r) - 1
case node.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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
h_mem : true = true
⊢ size (glue t_l t_r) = size (node size✝ t_l t_x t_r) - 1
rw [(Valid'.glue h.left h.right h.bal.1).2, h.sz.1]
no goals
case node.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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
h_mem : true = true
⊢ size t_l + size t_r = size (node (size t_l + size t_r + 1) t_l t_x t_r) - 1
rfl
case node.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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
⊢ size (balanceL t_l t_x (erase x t_r)) = size (node size✝ t_l t_x t_r) - 1
case node.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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
h_mem : mem x t_r = true
⊢ size (balanceL t_l t_x (erase x t_r)) = size (node size✝ t_l t_x t_r) - 1
have t_ih_r := t_ih_r' h_mem
case node.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
⊢ size (balanceL t_l t_x (erase x t_r)) = size (node size✝ t_l t_x t_r) - 1
case node.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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → size (erase x t_l) = size t_l - 1
t_ih_r' : x ∈ t_r → size (erase x t_r) = size t_r - 1
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
⊢ size (balanceL t_l t_x (erase x t_r)) = size (node size✝ t_l t_x t_r) - 1
clear t_ih_l' t_ih_r'
case node.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_h : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (size (erase x t_r)) (size t_r)
⊢ size (balanceL t_l t_x (erase x t_r)) = size (node size✝ t_l t_x t_r) - 1
case node.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
⊢ size (balanceL t_l t_x (erase x t_r)) = size (node size✝ t_l t_x t_r) - 1
have t_r_h := Valid'.erase_aux x h.right
case node.gt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ size (balanceL t_l t_x (erase x t_r)) = size (node size✝ t_l t_x t_r) - 1
case node.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_h : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (size (erase x t_r)) (size t_r)
⊢ size (balanceL t_l t_x (erase x t_r)) = size (node size✝ t_l t_x t_r) - 1
cases' t_r_h with t_r_valid t_r_size
case node.gt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ size t_l + size (erase x t_r) + 1 = size (node size✝ t_l t_x t_r) - 1
case node.gt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ size (balanceL t_l t_x (erase x t_r)) = size (node size✝ t_l t_x t_r) - 1
rw [size_balanceL h.left.bal t_r_valid.bal h.left.sz t_r_valid.sz
    (Or.inr (Exists.intro t_r.size (And.intro t_r_size h.bal.1)))]
case node.gt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ size t_l + (size t_r - 1) + 1 = size (node (size t_l + size t_r + 1) t_l t_x t_r) - 1
case node.gt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ size t_l + size (erase x t_r) + 1 = size (node size✝ t_l t_x t_r) - 1
rw [t_ih_r, h.sz.1]
case node.gt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_pos_t_r_size : 0 < size t_r
⊢ size t_l + (size t_r - 1) + 1 = size (node (size t_l + size t_r + 1) t_l t_x t_r) - 1
case node.gt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ size t_l + (size t_r - 1) + 1 = size (node (size t_l + size t_r + 1) t_l t_x t_r) - 1
have h_pos_t_r_size := pos_size_of_mem h.right.sz h_mem
case node.gt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ 0 < size t_r → size t_l + (size t_r - 1) + 1 = size (node (size t_l + size t_r + 1) t_l t_x t_r) - 1
case node.gt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_pos_t_r_size : 0 < size t_r
⊢ size t_l + (size t_r - 1) + 1 = size (node (size t_l + size t_r + 1) t_l t_x t_r) - 1
revert h_pos_t_r_size
case node.gt.intro.zero
α : 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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_pos_t_r_size : 0 < Nat.zero
⊢ size t_l + (Nat.zero - 1) + 1 = size (node (size t_l + Nat.zero + 1) t_l t_x t_r) - 1

case node.gt.intro.succ
α : 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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size✝ : Raised (size (erase x t_r)) (size t_r)
t_r_size : ℕ
h_pos_t_r_size : 0 < Nat.succ t_r_size
⊢ size t_l + (Nat.succ t_r_size - 1) + 1 = size (node (size t_l + Nat.succ t_r_size + 1) t_l t_x t_r) - 1
case node.gt.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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
⊢ 0 < size t_r → size t_l + (size t_r - 1) + 1 = size (node (size t_l + size t_r + 1) t_l t_x t_r) - 1
cases' t_r.size with t_r_size <;> intro h_pos_t_r_size
no goals
case node.gt.intro.zero
α : 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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (size (erase x t_r)) (size t_r)
h_pos_t_r_size : 0 < Nat.zero
⊢ size t_l + (Nat.zero - 1) + 1 = size (node (size t_l + Nat.zero + 1) t_l t_x t_r) - 1
cases h_pos_t_r_size
no goals
case node.gt.intro.succ
α : 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₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : size (erase x t_r) = size t_r - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size✝ : Raised (size (erase x t_r)) (size t_r)
t_r_size : ℕ
h_pos_t_r_size : 0 < Nat.succ t_r_size
⊢ size t_l + (Nat.succ t_r_size - 1) + 1 = size (node (size t_l + Nat.succ t_r_size + 1) t_l t_x t_r) - 1
simp [Nat.succ_add, Nat.add_succ]