-- Mathlib/Data/Ordmap/Ordset.lean
theorem size_erase_of_mem [DecidableRel (α := α) (· ≤ ·)] {x : α} {t a₁ a₂} (h : Valid' a₁ t a₂)
    (h_mem : x ∈ t) : size (erase x t) = size t - 1

Proof state:
case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
clear t_ih_l' t_ih_r'

Result:
case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 : (erase x t_l).size = t_l.size - 1
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size✝ t_l t_x t_r).size - 1

Proof state:
case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : mem x t_l = true
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
have t_ih_l := t_ih_l' h_mem

Result:
case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size✝ t_l t_x t_r).size - 1

Proof state:
case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 : (erase x t_r).size = t_r.size - 1
t_r_h : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
obtain ⟨t_r_valid, t_r_size⟩ := t_r_h

Result:
case node.gt.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size✝ t_l t_x t_r).size - 1

Proof state:
case node.gt.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ 0 < t_r.size → t_l.size + (t_r.size - 1) + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
rcases t_r.size with - | t_r_size <;> intro h_pos_t_r_size

Result:
case node.gt.intro.zero
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_pos_t_r_size : 0 < 0
⊢ t_l.size + (0 - 1) + 1 = (node (t_l.size + 0 + 1) t_l t_x t_r).size - 1

case node.gt.intro.succ
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size✝ : Raised (erase x t_r).size t_r.size
t_r_size : ℕ
h_pos_t_r_size : 0 < t_r_size + 1
⊢ t_l.size + (t_r_size + 1 - 1) + 1 = (node (t_l.size + (t_r_size + 1) + 1) t_l t_x t_r).size - 1

Proof state:
case node.gt.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ t_l.size + (erase x t_r).size + 1 = (node size✝ t_l t_x t_r).size - 1

Tactic:
rw [t_ih_r, h.sz.1]

Result:
case node.gt.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ t_l.size + (t_r.size - 1) + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Proof state:
case node.gt.intro.succ
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size✝ : Raised (erase x t_r).size t_r.size
t_r_size : ℕ
h_pos_t_r_size : 0 < t_r_size + 1
⊢ t_l.size + (t_r_size + 1 - 1) + 1 = (node (t_l.size + (t_r_size + 1) + 1) t_l t_x t_r).size - 1

Tactic:
simp [Nat.add_assoc]

Result:
no goals

Proof state:
case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : mem x t_r = true
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
have t_ih_r := t_ih_r' h_mem

Result:
case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size✝ t_l t_x t_r).size - 1

Proof state:
case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 : (erase x t_l).size = t_l.size - 1
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
have t_l_h := Valid'.erase_aux x h.left

Result:
case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 : (erase x t_l).size = t_l.size - 1
t_l_h : Valid' a₁ (erase x t_l) ↑t_x ∧ Raised (erase x t_l).size t_l.size
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size✝ t_l t_x t_r).size - 1