English
If x is a member of t and t is valid, then size(erase x t) = size(t) − 1.
Русский
Если x принадлежит t и t валидно, то размер erase x t равен размеру t минус 1.
LaTeX
$$$\\forall x,\\ t,\\ h:\\mathrm{Valid}' a_1 t a_2,\\ h_mem:\\ x \\in t\\Rightarrow \\mathrm{size}(\\mathrm{erase} x t) = \\mathrm{size}(t) - 1$$$
Lean4
theorem size_erase_of_mem [DecidableLE α] {x : α} {t a₁ a₂} (h : Valid' a₁ t a₂) (h_mem : x ∈ t) :
size (erase x t) = size t - 1 := by
induction t generalizing a₁ a₂ with
| nil => contradiction
| node _ t_l t_x t_r t_ih_l t_ih_r =>
have t_ih_l' := t_ih_l h.left
have t_ih_r' := t_ih_r h.right
clear t_ih_l t_ih_r
dsimp only [Membership.mem, mem] at h_mem
unfold erase
revert h_mem; cases cmpLE x t_x <;> intro h_mem <;> dsimp only at h_mem ⊢
· have t_ih_l := t_ih_l' h_mem
clear t_ih_l' t_ih_r'
have t_l_h := Valid'.erase_aux x h.left
obtain ⟨t_l_valid, t_l_size⟩ := t_l_h
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)))]
rw [t_ih_l, h.sz.1]
have h_pos_t_l_size := pos_size_of_mem h.left.sz h_mem
revert h_pos_t_l_size; rcases t_l.size with - | t_l_size <;> intro h_pos_t_l_size
· cases h_pos_t_l_size
· simp [Nat.add_right_comm]
· rw [(Valid'.glue h.left h.right h.bal.1).2, h.sz.1]; rfl
· have t_ih_r := t_ih_r' h_mem
clear t_ih_l' t_ih_r'
have t_r_h := Valid'.erase_aux x h.right
obtain ⟨t_r_valid, t_r_size⟩ := t_r_h
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)))]
rw [t_ih_r, h.sz.1]
have h_pos_t_r_size := pos_size_of_mem h.right.sz h_mem
revert h_pos_t_r_size; rcases t_r.size with - | t_r_size <;> intro h_pos_t_r_size
· cases h_pos_t_r_size
· simp [Nat.add_assoc]
