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

Proof state:
case left
α : 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₁ (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 (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_balanceable : ?m.312078
⊢ Valid' a₁
    (match Ordering.gt with
    | Ordering.lt => (erase x t_l).balanceR t_x t_r
    | Ordering.eq => t_l.glue t_r
    | Ordering.gt => t_l.balanceL t_x (erase x t_r))
    a₂

Tactic:
exact Valid'.balanceL h.left t_r_valid h_balanceable

Result:
no goals

Proof state:
case node
α : 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₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_ih_l' : Valid' a₁ (erase x t_l) ↑t_x ∧ Raised (erase x t_l).size t_l.size
t_ih_r' : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (match cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
      size✝

Tactic:
obtain ⟨t_l_valid, t_l_size⟩ := t_ih_l'

Result:
case node.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₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_ih_r' : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (match cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
      size✝

Proof state:
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 (erase x t_l).size t_l.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
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 (erase x (Ordnode.node size✝ t_l t_x t_r)).size (Ordnode.node size✝ t_l t_x t_r).size

Tactic:
simp only [erase, size_node]

Result:
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 (erase x t_l).size t_l.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
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 => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (match cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
      size✝

Proof state:
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 (erase x t_l).size t_l.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
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 (erase x t_l).size t_l.size
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (match cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
      size✝

Tactic:
have t_ih_r' := t_ih_r h.right

Result:
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
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 (erase x t_l).size t_l.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
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 (erase x t_l).size t_l.size
t_ih_r' : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (match cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
      size✝

Proof state:
case node.intro.intro.eq.intro.right
α : 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₁ (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 (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_glue_valid : Valid' a₁ (t_l.glue t_r) a₂
h_glue_sized : (t_l.glue t_r).size = t_l.size + t_r.size
⊢ Raised
    (match Ordering.eq with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
    (t_l.size + t_r.size + 1)

Tactic:
right

Result:
case node.intro.intro.eq.intro.right.h
α : 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₁ (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 (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_glue_valid : Valid' a₁ (t_l.glue t_r) a₂
h_glue_sized : (t_l.glue t_r).size = t_l.size + t_r.size
⊢ t_l.size + t_r.size + 1 =
    (match Ordering.eq with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size +
      1