awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Ordset
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'
right : Raised (t_l.size + (erase x t_r).size + 1) (t_l.size + t_r.size + 1)
⊢ 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:
rw [size_balanceL h.left.bal t_r_valid.bal h.left.sz t_r_valid.sz h_balanceable]

Premises used: Ordnode.Valid'.bal, Ordnode.size_balanceL, Ordnode.Valid'.sz, Ordnode.Valid'.left
-- Module: Mathlib.Data.Ordmap.Ordset
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'
right : Raised (t_l.size + (erase x t_r).size) (t_l.size + t_r.size)
⊢ Raised (t_l.size + (erase x t_r).size + 1) (t_l.size + t_r.size + 1)

Tactic:
apply Raised.add_right

Premises used: Ordnode.Raised.add_right
-- Module: Mathlib.Data.Ordmap.Ordset
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'
right : Raised (erase x t_r).size t_r.size
⊢ Raised (t_l.size + (erase x t_r).size) (t_l.size + t_r.size)

Tactic:
apply Raised.add_left

Premises used: Ordnode.Raised.add_left
-- Module: Mathlib.Data.Ordmap.Ordset
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 (erase x t_r).size t_r.size

Tactic:
t_r_size
-- Module: Mathlib.Data.Ordmap.Ordset
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 (erase x t_r).size t_r.size

Tactic:
exact t_r_size
-- Module: Mathlib.Data.Ordmap.Ordset
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
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'
⊢ 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)

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
-- Module: Mathlib.Data.Ordmap.Ordset
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
node : ∃ (r' : ℕ), Raised (erase x t_r).size r' ∧ BalancedSz t_l.size r'
⊢ (∃ (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:
right
-- Module: Mathlib.Data.Ordmap.Ordset
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
node : Raised (erase x t_r).size t_r.size ∧ BalancedSz t_l.size t_r.size
⊢ ∃ (r' : ℕ), Raised (erase x t_r).size r' ∧ BalancedSz t_l.size r'

Tactic:
exists t_r.size

Premises used: Ordnode.size
-- Module: Mathlib.Data.Ordmap.Ordset
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
⊢ Raised (erase x t_r).size t_r.size ∧ BalancedSz t_l.size t_r.size

Tactic:
And.intro t_r_size h.bal.1

Premises used: Ordnode.Valid'.bal, And.left, And.intro
-- Module: Mathlib.Data.Ordmap.Ordset
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
⊢ Raised (erase x t_r).size t_r.size ∧ BalancedSz t_l.size t_r.size

Tactic:
exact And.intro t_r_size h.bal.1

Premises used: Ordnode.Valid'.bal, And.left, And.intro
-- Module: Mathlib.Data.Ordmap.Ordset
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)
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
⊢ Valid' a₁ (erase x t) a₂ ∧ Raised (erase x t).size t.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

Premises used: Ordnode.size_node, Ordnode.erase, Ordnode.Raised, Ordnode.nil, Ordnode.Valid'.node
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (erase x t).Valid

Tactic:
(Valid'.erase_aux x h).1

Premises used: Ordnode.Valid, And.left, Ordnode.Valid'.erase_aux
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
h_mem : Membership.mem (γ := Ordnode α) nil x
⊢ (erase x nil).size = size.{u_1} (α := α) nil - 1

Tactic:
contradiction
-- Module: Mathlib.Data.Ordmap.Ordset
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
⊢ ∀ (h_mem : x ∈ t_l), (erase x t_l).size = t_l.size - 1

Tactic:
have t_ih_l' := t_ih_l h.left
-- Module: Mathlib.Data.Ordmap.Ordset
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
t_ih_l' : ∀ (h_mem : x ∈ t_l), (erase x t_l).size = t_l.size - 1
⊢ ∀ (h_mem : x ∈ t_r), (erase x t_r).size = t_r.size - 1

Tactic:
have t_ih_r' := t_ih_r h.right
-- Module: Mathlib.Data.Ordmap.Ordset
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₂
h_mem :
  (match (motive := Ordering → Bool) cmpLE x t_x with
    | Ordering.lt => mem x t_l
    | Ordering.eq => true
    | Ordering.gt => mem x t_r) =
    true
t_ih_l' : ∀ (h_mem : x ∈ t_l), (erase x t_l).size = t_l.size - 1
t_ih_r' : ∀ (h_mem : x ∈ t_r), (erase x t_r).size = t_r.size - 1
node :
  Ordnode.size.{u_1} (α := α)
      (match (motive := Ordering → Ordnode α) 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)) =
    (Ordnode.node size t_l t_x t_r).size - 1
⊢ (erase x (Ordnode.node size t_l t_x t_r)).size = (Ordnode.node size t_l t_x t_r).size - 1

Tactic:
unfold erase

Premises used: Ordnode.erase
-- Module: Mathlib.Data.Ordmap.Ordset
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₂
h_mem :
  (match (motive := Ordering → Bool) cmpLE x t_x with
    | Ordering.lt => mem x t_l
    | Ordering.eq => true
    | Ordering.gt => mem x t_r) =
    true
t_ih_l' : ∀ (h_mem : x ∈ t_l), (erase x t_l).size = t_l.size - 1
t_ih_r' : ∀ (h_mem : x ∈ t_r), (erase x t_r).size = t_r.size - 1
node :
  ∀
    (h_mem :
      (match (motive := Ordering → Bool) cmpLE x t_x with
        | Ordering.lt => mem x t_l
        | Ordering.eq => true
        | Ordering.gt => mem x t_r) =
        true),
    Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) 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)) =
      (Ordnode.node size t_l t_x t_r).size - 1
⊢ Ordnode.size.{u_1} (α := α)
      (match (motive := Ordering → Ordnode α) 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)) =
    (Ordnode.node size t_l t_x t_r).size - 1

Tactic:
revert h_mem
-- Module: Mathlib.Data.Ordmap.Ordset
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_ih_l' : ∀ (h_mem : x ∈ t_l), (erase x t_l).size = t_l.size - 1
t_ih_r' : ∀ (h_mem : x ∈ t_r), (erase x t_r).size = t_r.size - 1
node :
  ∀
    (h_mem :
      (match (motive := Ordering → Bool) Ordering.lt with
        | Ordering.lt => mem x t_l
        | Ordering.eq => true
        | Ordering.gt => mem x t_r) =
        true),
    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)) =
      (Ordnode.node size t_l t_x t_r).size - 1
node₁ :
  ∀
    (h_mem :
      (match (motive := Ordering → Bool) Ordering.eq with
        | Ordering.lt => mem x t_l
        | Ordering.eq => true
        | Ordering.gt => mem x t_r) =
        true),
    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)) =
      (Ordnode.node size t_l t_x t_r).size - 1
node₂ :
  ∀
    (h_mem :
      (match (motive := Ordering → Bool) Ordering.gt with
        | Ordering.lt => mem x t_l
        | Ordering.eq => true
        | Ordering.gt => mem x t_r) =
        true),
    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)) =
      (Ordnode.node size t_l t_x t_r).size - 1
⊢ ∀
    (h_mem :
      (match (motive := Ordering → Bool) cmpLE x t_x with
        | Ordering.lt => mem x t_l
        | Ordering.eq => true
        | Ordering.gt => mem x t_r) =
        true),
    Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) 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)) =
      (Ordnode.node size t_l t_x t_r).size - 1

Tactic:
cases cmpLE x t_x

Premises used: cmpLE
-- Module: Mathlib.Data.Ordmap.Ordset
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₁ (node size t_l t_x t_r) a₂
t_ih_l' : ∀ (h_mem : x ∈ t_l), (erase x t_l).size = t_l.size - 1
t_ih_r' : ∀ (h_mem : x ∈ t_r), (erase x t_r).size = t_r.size - 1
h_mem : mem x t_l = true
⊢ (erase x t_l).size = t_l.size - 1

Tactic:
have t_ih_l := t_ih_l' h_mem
-- Module: Mathlib.Data.Ordmap.Ordset
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₁ (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
⊢ Valid' a₁ (erase x t_l) (↑t_x : WithTop α) ∧ Raised (erase x t_l).size t_l.size

Tactic:
have t_l_h := Valid'.erase_aux x h.left
-- Module: Mathlib.Data.Ordmap.Ordset
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₁ (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 : WithTop α) ∧ Raised (erase x t_l).size t_l.size
⊢ Valid' a₁ (erase x t_l) (↑t_x : WithTop α)

Tactic:
obtain ⟨t_l_valid, t_l_size⟩ := t_l_h
-- Module: Mathlib.Data.Ordmap.Ordset
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₁ (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 : WithTop α) ∧ Raised (erase x t_l).size t_l.size
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
⊢ Raised (erase x t_l).size t_l.size

Tactic:
obtain ⟨t_l_valid, t_l_size⟩ := t_l_h
-- Module: Mathlib.Data.Ordmap.Ordset
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₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
node : (erase x t_l).size + t_r.size + 1 = (Ordnode.node size t_l t_x t_r).size - 1
⊢ ((erase x t_l).balanceR t_x t_r).size = (Ordnode.node size t_l t_x t_r).size - 1

Tactic:
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)))]

Premises used: Ordnode.Valid'.bal, Ordnode.Valid'.sz, Ordnode.size_balanceR, Ordnode.size, Ordnode.Valid'.right, And.left, And.intro, Exists.intro, Or.inl
-- Module: Mathlib.Data.Ordmap.Ordset
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₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
node : t_l.size - 1 + t_r.size + 1 = (Ordnode.node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
⊢ (erase x t_l).size + t_r.size + 1 = (Ordnode.node size t_l t_x t_r).size - 1

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

Premises used: Ordnode.Valid'.sz, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
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₁ (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_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
⊢ 0 < t_l.size

Tactic:
have h_pos_t_l_size := pos_size_of_mem h.left.sz h_mem
-- Module: Mathlib.Data.Ordmap.Ordset
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₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
h_pos_t_l_size : 0 < t_l.size
node :
  ∀ (h_pos_t_l_size : 0 < t_l.size),
    t_l.size - 1 + t_r.size + 1 = (Ordnode.node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
⊢ t_l.size - 1 + t_r.size + 1 = (Ordnode.node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
revert h_pos_t_l_size
-- Module: Mathlib.Data.Ordmap.Ordset
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₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
node :
  ∀ (h_pos_t_l_size : LT.lt (α := ℕ) 0 0),
    HSub.hSub (α := ℕ) 0 1 + t_r.size + 1 = (Ordnode.node (0 + t_r.size + 1) t_l t_x t_r).size - 1
node₁ :
  ∀ (t_l_size : ℕ) (h_pos_t_l_size : 0 < t_l_size + 1),
    t_l_size + 1 - 1 + t_r.size + 1 = (Ordnode.node (t_l_size + 1 + t_r.size + 1) t_l t_x t_r).size - 1
⊢ ∀ (h_pos_t_l_size : 0 < t_l.size),
    t_l.size - 1 + t_r.size + 1 = (Ordnode.node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
rcases t_l.size with - | t_l_size

Premises used: Ordnode.size
-- Module: Mathlib.Data.Ordmap.Ordset
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₁ (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_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
h_pos_t_l_size : LT.lt (α := ℕ) 0 0
⊢ HSub.hSub (α := ℕ) 0 1 + t_r.size + 1 = (node (0 + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
cases h_pos_t_l_size
-- Module: Mathlib.Data.Ordmap.Ordset
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₁ (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_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size_1 : Raised (erase x t_l).size t_l.size
t_l_size : ℕ
h_pos_t_l_size : 0 < t_l_size + 1
⊢ t_l_size + 1 - 1 + t_r.size + 1 = (node (t_l_size + 1 + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
simp [Nat.add_right_comm]

Premises used: Nat.add_right_comm
-- Module: Mathlib.Data.Ordmap.Ordset
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_ih_l' : ∀ (h_mem : x ∈ t_l), (erase x t_l).size = t_l.size - 1
t_ih_r' : ∀ (h_mem : x ∈ t_r), (erase x t_r).size = t_r.size - 1
h_mem : true = true
node : t_l.size + t_r.size = (Ordnode.node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
⊢ (t_l.glue t_r).size = (Ordnode.node size t_l t_x t_r).size - 1

Tactic:
rw [(Valid'.glue h.left h.right h.bal.1).2, h.sz.1]

Premises used: Ordnode.Valid'.bal, Ordnode.Valid'.sz, Ordnode.Valid'.right, And.right, And.left, Ordnode.Valid'.glue, Ordnode.Valid'.left