awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_balanceable :
  (∃ (l' : ℕ), Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size) ∨
    ∃ (r' : ℕ), Raised r' t_r.size ∧ BalancedSz (erase x t_l).size r'
⊢ Raised
    (Ordnode.size.{u_1} (α := α)
      (match (motive := Ordering → Ordnode α) Ordering.lt 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)))
    (t_l.size + t_r.size + 1)
have right : Raised ((erase x t_l).size + t_r.size + 1) (t_l.size + t_r.size + 1)
Tactic: rw [size_balanceR t_l_valid.bal h.right.bal t_l_valid.sz h.right.sz h_balanceable]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_balanceable :
  (∃ (l' : ℕ), Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size) ∨
    ∃ (r' : ℕ), Raised r' t_r.size ∧ BalancedSz (erase x t_l).size r'
⊢ Raised ((erase x t_l).size + t_r.size + 1) (t_l.size + t_r.size + 1)
have right : Raised ((erase x t_l).size + t_r.size) (t_l.size + t_r.size)
Tactic: apply Raised.add_right
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) Ordering.lt 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
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) Ordering.lt 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)))
      (t_l.size + t_r.size + 1)
have node : (∃ (l' : ℕ), Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size) ∨
  ∃ (r' : ℕ), Raised r' t_r.size ∧ BalancedSz (erase x t_l).size r'
Tactic: suffices h_balanceable : _ by
        constructor
        · exact Valid'.balanceR t_l_valid h.right h_balanceable
        · rw [size_balanceR t_l_valid.bal h.right.bal t_l_valid.sz h.right.sz h_balanceable]
          repeat apply Raised.add_right
          exact t_l_size
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ (∃ (l' : ℕ), Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size) ∨
    ∃ (r' : ℕ), Raised r' t_r.size ∧ BalancedSz (erase x t_l).size r'
have node : ∃ (l' : ℕ), Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size
Tactic: left
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ ∃ (l' : ℕ), Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size
have node : Raised (erase x t_l).size t_l.size ∧ BalancedSz t_l.size t_r.size
Tactic: exists t_l.size
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) 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))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) 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)))
      (t_l.size + t_r.size + 1)
have h_glue : Valid' a₁ (t_l.glue t_r) a₂ ∧ (t_l.glue t_r).size = t_l.size + t_r.size
Tactic: have h_glue := Valid'.glue h.left h.right h.bal.1
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_glue : Valid' a₁ (t_l.glue t_r) a₂ ∧ (t_l.glue t_r).size = t_l.size + t_r.size
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) 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))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) 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)))
      (t_l.size + t_r.size + 1)
have h_glue_valid : Valid' a₁ (t_l.glue t_r) a₂
Tactic: obtain ⟨h_glue_valid, h_glue_sized⟩ := h_glue
Cleared hypotheses: h_glue
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_glue : Valid' a₁ (t_l.glue t_r) a₂ ∧ (t_l.glue t_r).size = t_l.size + t_r.size
h_glue_valid : Valid' a₁ (t_l.glue t_r) a₂
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) 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))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) 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)))
      (t_l.size + t_r.size + 1)
have h_glue_sized : (t_l.glue t_r).size = t_l.size + t_r.size
Tactic: obtain ⟨h_glue_valid, h_glue_sized⟩ := h_glue
Cleared hypotheses: h_glue
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (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
node :
  Valid' a₁
    (match (motive := Ordering → Ordnode α) 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))
    a₂
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) 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))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) 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)))
      (t_l.size + t_r.size + 1)
have node₁ : Raised
  (Ordnode.size.{u_1} (α := α)
    (match (motive := Ordering → Ordnode α) 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)))
  (t_l.size + t_r.size + 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (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
    (Ordnode.size.{u_1} (α := α)
      (match (motive := Ordering → Ordnode α) 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)))
    (t_l.size + t_r.size + 1)
have node : t_l.size + t_r.size + 1 =
  Ordnode.size.{u_1} (α := α)
      (match (motive := Ordering → Ordnode α) 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)) +
    1
Tactic: right
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (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 =
    Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) 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)) +
      1
have node : t_l.size + t_r.size + 1 = t_l.size + t_r.size + 1
Tactic: rw [h_glue_sized]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_balanceable :
  (∃ (l' : ℕ), Raised l' t_l.size ∧ BalancedSz l' (erase x t_r).size) ∨
    ∃ (r' : ℕ), Raised (erase x t_r).size r' ∧ BalancedSz t_l.size r'
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) 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₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) 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)))
      (t_l.size + t_r.size + 1)
have left : Valid' a₁
  (match (motive := Ordering → Ordnode α) 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: constructor
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_balanceable :
  (∃ (l' : ℕ), Raised l' t_l.size ∧ BalancedSz l' (erase x t_r).size) ∨
    ∃ (r' : ℕ), Raised (erase x t_r).size r' ∧ BalancedSz t_l.size r'
left :
  Valid' a₁
    (match (motive := Ordering → Ordnode α) 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₂
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) 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₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) 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)))
      (t_l.size + t_r.size + 1)
have right : Raised
  (Ordnode.size.{u_1} (α := α)
    (match (motive := Ordering → Ordnode α) 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)))
  (t_l.size + t_r.size + 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_balanceable :
  (∃ (l' : ℕ), Raised l' t_l.size ∧ BalancedSz l' (erase x t_r).size) ∨
    ∃ (r' : ℕ), Raised (erase x t_r).size r' ∧ BalancedSz t_l.size r'
⊢ Raised
    (Ordnode.size.{u_1} (α := α)
      (match (motive := Ordering → Ordnode α) 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)))
    (t_l.size + t_r.size + 1)
have right : Raised (t_l.size + (erase x t_r).size + 1) (t_l.size + t_r.size + 1)
Tactic: rw [size_balanceL h.left.bal t_r_valid.bal h.left.sz t_r_valid.sz h_balanceable]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_balanceable :
  (∃ (l' : ℕ), Raised l' t_l.size ∧ BalancedSz l' (erase x t_r).size) ∨
    ∃ (r' : ℕ), Raised (erase x t_r).size r' ∧ BalancedSz t_l.size r'
⊢ Raised (t_l.size + (erase x t_r).size + 1) (t_l.size + t_r.size + 1)
have right : Raised (t_l.size + (erase x t_r).size) (t_l.size + t_r.size)
Tactic: apply Raised.add_right
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) 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₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) 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)))
      (t_l.size + t_r.size + 1)
have node : (∃ (l' : ℕ), Raised l' t_l.size ∧ BalancedSz l' (erase x t_r).size) ∨
  ∃ (r' : ℕ), Raised (erase x t_r).size r' ∧ BalancedSz t_l.size r'
Tactic: suffices h_balanceable : _ by
        constructor
        · exact Valid'.balanceL h.left t_r_valid h_balanceable
        · rw [size_balanceL h.left.bal t_r_valid.bal h.left.sz t_r_valid.sz h_balanceable]
          apply Raised.add_right
          apply Raised.add_left
          exact t_r_size
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ (∃ (l' : ℕ), Raised l' t_l.size ∧ BalancedSz l' (erase x t_r).size) ∨
    ∃ (r' : ℕ), Raised (erase x t_r).size r' ∧ BalancedSz t_l.size r'
have node : ∃ (r' : ℕ), Raised (erase x t_r).size r' ∧ BalancedSz t_l.size r'
Tactic: right
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
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 : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ ∃ (r' : ℕ), Raised (erase x t_r).size r' ∧ BalancedSz t_l.size r'
have node : Raised (erase x t_r).size t_r.size ∧ BalancedSz t_l.size t_r.size
Tactic: exists t_r.size
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
t : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ t a₂
⊢ Valid' a₁ (erase x t) a₂ ∧ Raised (erase x t).size t.size
have nil : ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ nil a₂),
  Valid' a₁ (erase x nil) a₂ ∧ Raised (erase x nil).size (size.{u_1} (α := α) nil)
Tactic: induction t generalizing a₁ a₂ with
  | nil =>
    simpa [erase, Raised]
  | node _ t_l t_x t_r t_ih_l t_ih_r =>
    simp only [erase, size_node]
    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
    obtain ⟨t_l_valid, t_l_size⟩ := t_ih_l'
    obtain ⟨t_r_valid, t_r_size⟩ := t_ih_r'
    cases cmpLE x t_x <;> rw [h.sz.1]
    · suffices h_balanceable : _ by
        constructor
        · exact Valid'.balanceR t_l_valid h.right h_balanceable
        · rw [size_balanceR t_l_valid.bal h.right.bal t_l_valid.sz h.right.sz h_balanceable]
          repeat apply Raised.add_right
          exact t_l_size
      left; exists t_l.size; exact And.intro t_l_size h.bal.1
    · have h_glue := Valid'.glue h.left h.right h.bal.1
      obtain ⟨h_glue_valid, h_glue_sized⟩ := h_glue
      constructor
      · exact h_glue_valid
      · right; rw [h_glue_sized]
    · suffices h_balanceable : _ by
        constructor
        · exact Valid'.balanceL h.left t_r_valid h_balanceable
        · rw [size_balanceL h.left.bal t_r_valid.bal h.left.sz t_r_valid.sz h_balanceable]
          apply Raised.add_right
          apply Raised.add_left
          exact t_r_size
      right; exists t_r.size; exact And.intro t_r_size h.bal.1
Cleared hypotheses: t, a₁, a₂, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
t : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ t a₂
nil :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ Ordnode.nil a₂),
    Valid' a₁ (erase x Ordnode.nil) a₂ ∧ Raised (erase x Ordnode.nil).size (size.{u_1} (α := α) Ordnode.nil)
⊢ Valid' a₁ (erase x t) a₂ ∧ Raised (erase x t).size t.size
have node : ∀ (size : ℕ) (t_l : Ordnode α) (t_x : α) (t_r : Ordnode α)
  (t_ih_l :
    ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : 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 α} (h : 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: induction t generalizing a₁ a₂ with
  | nil =>
    simpa [erase, Raised]
  | node _ t_l t_x t_r t_ih_l t_ih_r =>
    simp only [erase, size_node]
    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
    obtain ⟨t_l_valid, t_l_size⟩ := t_ih_l'
    obtain ⟨t_r_valid, t_r_size⟩ := t_ih_r'
    cases cmpLE x t_x <;> rw [h.sz.1]
    · suffices h_balanceable : _ by
        constructor
        · exact Valid'.balanceR t_l_valid h.right h_balanceable
        · rw [size_balanceR t_l_valid.bal h.right.bal t_l_valid.sz h.right.sz h_balanceable]
          repeat apply Raised.add_right
          exact t_l_size
      left; exists t_l.size; exact And.intro t_l_size h.bal.1
    · have h_glue := Valid'.glue h.left h.right h.bal.1
      obtain ⟨h_glue_valid, h_glue_sized⟩ := h_glue
      constructor
      · exact h_glue_valid
      · right; rw [h_glue_sized]
    · suffices h_balanceable : _ by
        constructor
        · exact Valid'.balanceL h.left t_r_valid h_balanceable
        · rw [size_balanceL h.left.bal t_r_valid.bal h.left.sz t_r_valid.sz h_balanceable]
          apply Raised.add_right
          apply Raised.add_left
          exact t_r_size
      right; exists t_r.size; exact And.intro t_r_size h.bal.1
Cleared hypotheses: t, a₁, a₂, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l : ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ t_l a₂) (h_mem : x ∈ t_l), (erase x t_l).size = t_l.size - 1
t_ih_r : ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ t_r a₂) (h_mem : x ∈ t_r), (erase x t_r).size = t_r.size - 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
⊢ (erase x (node size t_l t_x t_r)).size = (node size t_l t_x t_r).size - 1
have t_ih_l' : ∀ (h_mem : x ∈ t_l), (erase x t_l).size = t_l.size - 1
Tactic: have t_ih_l' := t_ih_l h.left