case nil
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Valid' (Option.map f a₁) nil (Option.map f a₂)
case nil
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Valid' (Option.map f a₁) (map f nil) (Option.map f a₂) ∧ size (map f nil) = size nil
simp [map]
case nil.h
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Bounded nil (Option.map f a₁) (Option.map f a₂)
case nil
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Valid' (Option.map f a₁) nil (Option.map f a₂)
apply valid'_nil
case nil.h.none
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₂ : WithTop α
h : Valid' none nil a₂
⊢ Bounded nil (Option.map f none) (Option.map f a₂)

case nil.h.some
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₂ : WithTop α
val✝ : α
h : Valid' (some val✝) nil a₂
⊢ Bounded nil (Option.map f (some val✝)) (Option.map f a₂)
case nil.h
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Bounded nil (Option.map f a₁) (Option.map f a₂)
cases a₁
case nil.h.some.none
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
val✝ : α
h : Valid' (some val✝) nil none
⊢ Bounded nil (Option.map f (some val✝)) (Option.map f none)

case nil.h.some.some
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
val✝¹ val✝ : α
h : Valid' (some val✝¹) nil (some val✝)
⊢ Bounded nil (Option.map f (some val✝¹)) (Option.map f (some val✝))
case nil.h.some
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₂ : WithTop α
val✝ : α
h : Valid' (some val✝) nil a₂
⊢ Bounded nil (Option.map f (some val✝)) (Option.map f a₂)
cases a₂
case nil.h.some.some
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
val✝¹ val✝ : α
h : Valid' (some val✝¹) nil (some val✝)
⊢ f val✝¹ < f val✝
case nil.h.some.some
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
val✝¹ val✝ : α
h : Valid' (some val✝¹) nil (some val✝)
⊢ Bounded nil (Option.map f (some val✝¹)) (Option.map f (some val✝))
simp [Bounded]
no goals
case nil.h.some.some
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
val✝¹ val✝ : α
h : Valid' (some val✝¹) nil (some val✝)
⊢ f val✝¹ < f val✝
exact f_strict_mono h.ord
no goals
case nil.h.none
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₂ : WithTop α
h : Valid' none nil a₂
⊢ Bounded nil (Option.map f none) (Option.map f a₂)
trivial
no goals
case nil.h.some.none
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
val✝ : α
h : Valid' (some val✝) nil none
⊢ Bounded nil (Option.map f (some val✝)) (Option.map f none)
trivial
case node
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ l✝ a₂ → Valid' (Option.map f a₁) (map f l✝) (Option.map f a₂) ∧ size (map f l✝) = size l✝
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ r✝ a₂ → Valid' (Option.map f a₁) (map f r✝) (Option.map f a₂) ∧ size (map f r✝) = size r✝
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_ih_l' : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝) ∧ size (map f l✝) = size l✝
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    size (map f (Ordnode.node size✝ l✝ x✝ r✝)) = size (Ordnode.node size✝ l✝ x✝ r✝)
case node
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ l✝ a₂ → Valid' (Option.map f a₁) (map f l✝) (Option.map f a₂) ∧ size (map f l✝) = size l✝
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ r✝ a₂ → Valid' (Option.map f a₁) (map f r✝) (Option.map f a₂) ∧ size (map f r✝) = size r✝
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    size (map f (Ordnode.node size✝ l✝ x✝ r✝)) = size (Ordnode.node size✝ l✝ x✝ r✝)
have t_ih_l' := t_ih_l h.left
case node
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ l✝ a₂ → Valid' (Option.map f a₁) (map f l✝) (Option.map f a₂) ∧ size (map f l✝) = size l✝
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ r✝ a₂ → Valid' (Option.map f a₁) (map f r✝) (Option.map f a₂) ∧ size (map f r✝) = size r✝
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_ih_l' : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝) ∧ size (map f l✝) = size l✝
t_ih_r' : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂) ∧ size (map f r✝) = size r✝
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    size (map f (Ordnode.node size✝ l✝ x✝ r✝)) = size (Ordnode.node size✝ l✝ x✝ r✝)
case node
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ l✝ a₂ → Valid' (Option.map f a₁) (map f l✝) (Option.map f a₂) ∧ size (map f l✝) = size l✝
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ r✝ a₂ → Valid' (Option.map f a₁) (map f r✝) (Option.map f a₂) ∧ size (map f r✝) = size r✝
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_ih_l' : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝) ∧ size (map f l✝) = size l✝
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    size (map f (Ordnode.node size✝ l✝ x✝ r✝)) = size (Ordnode.node size✝ l✝ x✝ r✝)
have t_ih_r' := t_ih_r h.right
case node
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_ih_l' : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝) ∧ size (map f l✝) = size l✝
t_ih_r' : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂) ∧ size (map f r✝) = size r✝
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    size (map f (Ordnode.node size✝ l✝ x✝ r✝)) = size (Ordnode.node size✝ l✝ x✝ r✝)
case node
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ l✝ a₂ → Valid' (Option.map f a₁) (map f l✝) (Option.map f a₂) ∧ size (map f l✝) = size l✝
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ r✝ a₂ → Valid' (Option.map f a₁) (map f r✝) (Option.map f a₂) ∧ size (map f r✝) = size r✝
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_ih_l' : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝) ∧ size (map f l✝) = size l✝
t_ih_r' : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂) ∧ size (map f r✝) = size r✝
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    size (map f (Ordnode.node size✝ l✝ x✝ r✝)) = size (Ordnode.node size✝ l✝ x✝ r✝)
clear t_ih_l t_ih_r
case node.intro
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_ih_r' : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂) ∧ size (map f r✝) = size r✝
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    size (map f (Ordnode.node size✝ l✝ x✝ r✝)) = size (Ordnode.node size✝ l✝ x✝ r✝)
case node
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_ih_l' : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝) ∧ size (map f l✝) = size l✝
t_ih_r' : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂) ∧ size (map f r✝) = size r✝
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    size (map f (Ordnode.node size✝ l✝ x✝ r✝)) = size (Ordnode.node size✝ l✝ x✝ r✝)
cases' t_ih_l' with t_l_valid t_l_size
case node.intro.intro
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    size (map f (Ordnode.node size✝ l✝ x✝ r✝)) = size (Ordnode.node size✝ l✝ x✝ r✝)
case node.intro
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_ih_r' : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂) ∧ size (map f r✝) = size r✝
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    size (map f (Ordnode.node size✝ l✝ x✝ r✝)) = size (Ordnode.node size✝ l✝ x✝ r✝)
cases' t_ih_r' with t_r_valid t_r_size
case node.intro.intro
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Valid' (Option.map f a₁) (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝)) (Option.map f a₂)
case node.intro.intro
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    size (map f (Ordnode.node size✝ l✝ x✝ r✝)) = size (Ordnode.node size✝ l✝ x✝ r✝)
simp [map]
case node.intro.intro.ord
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Bounded (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝)) (Option.map f a₁) (Option.map f a₂)

case node.intro.intro.sz
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Sized (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝))

case node.intro.intro.bal
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Balanced (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝))
case node.intro.intro
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Valid' (Option.map f a₁) (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝)) (Option.map f a₂)
constructor
no goals
case node.intro.intro.ord
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Bounded (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝)) (Option.map f a₁) (Option.map f a₂)
exact And.intro t_l_valid.ord t_r_valid.ord
case node.intro.intro.sz.left
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ size✝ = size (map f l✝) + size (map f r✝) + 1

case node.intro.intro.sz.right
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Sized (map f l✝) ∧ Sized (map f r✝)
case node.intro.intro.sz
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Sized (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝))
constructor
case node.intro.intro.sz.left
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ size✝ = size l✝ + size r✝ + 1
case node.intro.intro.sz.left
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ size✝ = size (map f l✝) + size (map f r✝) + 1
rw [t_l_size, t_r_size]
no goals
case node.intro.intro.sz.left
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ size✝ = size l✝ + size r✝ + 1
exact h.sz.1
case node.intro.intro.sz.right.left
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Sized (map f l✝)

case node.intro.intro.sz.right.right
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Sized (map f r✝)
case node.intro.intro.sz.right
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Sized (map f l✝) ∧ Sized (map f r✝)
constructor
no goals
case node.intro.intro.sz.right.left
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Sized (map f l✝)
exact t_l_valid.sz
no goals
case node.intro.intro.sz.right.right
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Sized (map f r✝)
exact t_r_valid.sz
case node.intro.intro.bal.left
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ BalancedSz (size (map f l✝)) (size (map f r✝))

case node.intro.intro.bal.right
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Balanced (map f l✝) ∧ Balanced (map f r✝)
case node.intro.intro.bal
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Balanced (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝))
constructor
case node.intro.intro.bal.left
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ BalancedSz (size l✝) (size r✝)
case node.intro.intro.bal.left
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ BalancedSz (size (map f l✝)) (size (map f r✝))
rw [t_l_size, t_r_size]
no goals
case node.intro.intro.bal.left
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ BalancedSz (size l✝) (size r✝)
exact h.bal.1
case node.intro.intro.bal.right.left
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Balanced (map f l✝)

case node.intro.intro.bal.right.right
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Balanced (map f r✝)
case node.intro.intro.bal.right
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Balanced (map f l✝) ∧ Balanced (map f r✝)
constructor
no goals
case node.intro.intro.bal.right.left
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Balanced (map f l✝)
exact t_l_valid.bal
no goals
case node.intro.intro.bal.right.right
α : Type u_2
inst✝¹ : Preorder α
β : Type u_1
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : size (map f l✝) = size l✝
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : size (map f r✝) = size r✝
⊢ Balanced (map f r✝)
exact t_r_valid.bal