awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
t_ih_l' : ∀ (h_mem : x ∈ t_l), (erase x t_l).size = t_l.size - 1
⊢ (erase x (node size t_l t_x t_r)).size = (node size t_l t_x t_r).size - 1
have t_ih_r' : ∀ (h_mem : x ∈ t_r), (erase x t_r).size = t_r.size - 1
Tactic: have t_ih_r' := t_ih_r h.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₁ (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
⊢ (erase x (node size t_l t_x t_r)).size = (node size t_l t_x t_r).size - 1
have 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)) =
  (node size t_l t_x t_r).size - 1
Tactic: unfold erase
-- 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₁ (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
⊢ 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)) =
    (node size t_l t_x t_r).size - 1
have 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)) =
    (node size t_l t_x t_r).size - 1
Tactic: revert h_mem
Cleared hypotheses: h_mem
-- 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₁ (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 :
      (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)) =
      (node size t_l t_x t_r).size - 1
have 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)) =
    (node size t_l t_x t_r).size - 1
Tactic: cases cmpLE x t_x
-- 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_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
⊢ ∀
    (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
have 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
Tactic: cases cmpLE x t_x
-- 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_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
⊢ ∀
    (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
have 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
Tactic: cases cmpLE x t_x
-- 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₁ (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).balanceR t_x t_r).size = (node size t_l t_x t_r).size - 1
have t_ih_l : (erase x t_l).size = t_l.size - 1
Tactic: have t_ih_l := t_ih_l' h_mem
-- 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₁ (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
have t_l_h : 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
-- 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₁ (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
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size t_l t_x t_r).size - 1
have t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
Tactic: obtain ⟨t_l_valid, t_l_size⟩ := t_l_h
Cleared hypotheses: t_l_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 α
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 α)
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size t_l t_x t_r).size - 1
have t_l_size : Raised (erase x t_l).size t_l.size
Tactic: obtain ⟨t_l_valid, t_l_size⟩ := t_l_h
Cleared hypotheses: t_l_h
-- 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₁ (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
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size t_l t_x t_r).size - 1
have node : (erase x t_l).size + t_r.size + 1 = (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)))]
-- 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₁ (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
⊢ (erase x t_l).size + t_r.size + 1 = (node size t_l t_x t_r).size - 1
have node : t_l.size - 1 + t_r.size + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
Tactic: rw [t_ih_l, h.sz.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₁ (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
⊢ t_l.size - 1 + t_r.size + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
have h_pos_t_l_size : 0 < t_l.size
Tactic: have h_pos_t_l_size := pos_size_of_mem h.left.sz h_mem
-- 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₁ (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
⊢ t_l.size - 1 + t_r.size + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
have node : ∀ (h_pos_t_l_size : 0 < t_l.size), t_l.size - 1 + t_r.size + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
Tactic: revert h_pos_t_l_size
Cleared hypotheses: h_pos_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₁ (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), t_l.size - 1 + t_r.size + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
have node : ∀ (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: rcases t_l.size with - | 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₂
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
⊢ ∀ (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
have 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
Tactic: rcases t_l.size with - | 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₁ (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
⊢ (t_l.glue t_r).size = (node size t_l t_x t_r).size - 1
have node : t_l.size + t_r.size = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
Tactic: rw [(Valid'.glue h.left h.right h.bal.1).2, h.sz.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₁ (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_r = true
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size t_l t_x t_r).size - 1
have t_ih_r : (erase x t_r).size = t_r.size - 1
Tactic: have t_ih_r := t_ih_r' h_mem
-- 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₁ (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_l.balanceL t_x (erase x t_r)).size = (node size t_l t_x t_r).size - 1
have t_r_h : Valid' (↑t_x : WithBot α) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
Tactic: have t_r_h := Valid'.erase_aux x h.right
-- 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₁ (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 : WithBot α) (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
have t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
Tactic: obtain ⟨t_r_valid, t_r_size⟩ := t_r_h
Cleared hypotheses: t_r_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 α
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 : WithBot α) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size t_l t_x t_r).size - 1
have t_r_size : Raised (erase x t_r).size t_r.size
Tactic: obtain ⟨t_r_valid, t_r_size⟩ := t_r_h
Cleared hypotheses: t_r_h
-- 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₁ (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 : WithBot α) (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
have node : t_l.size + (erase x t_r).size + 1 = (node size t_l t_x t_r).size - 1
Tactic: 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)))]
-- 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₁ (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 : WithBot α) (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
have node : 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: rw [t_ih_r, h.sz.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₁ (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 : WithBot α) (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
have h_pos_t_r_size : 0 < t_r.size
Tactic: have h_pos_t_r_size := pos_size_of_mem h.right.sz h_mem
-- 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₁ (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 : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_pos_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
have node : ∀ (h_pos_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: revert h_pos_t_r_size
Cleared hypotheses: h_pos_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₁ (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 : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ ∀ (h_pos_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
have node : ∀ (h_pos_t_r_size : LT.lt (α := ℕ) 0 0),
  t_l.size + HSub.hSub (α := ℕ) 0 1 + 1 = (node (t_l.size + 0 + 1) t_l t_x t_r).size - 1
Tactic: rcases t_r.size with - | 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₂
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 : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
node :
  ∀ (h_pos_t_r_size : LT.lt (α := ℕ) 0 0),
    t_l.size + HSub.hSub (α := ℕ) 0 1 + 1 = (Ordnode.node (t_l.size + 0 + 1) t_l t_x t_r).size - 1
⊢ ∀ (h_pos_t_r_size : 0 < t_r.size),
    t_l.size + (t_r.size - 1) + 1 = (Ordnode.node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
have node₁ : ∀ (t_r_size : ℕ) (h_pos_t_r_size : 0 < t_r_size + 1),
  t_l.size + (t_r_size + 1 - 1) + 1 = (Ordnode.node (t_l.size + (t_r_size + 1) + 1) t_l t_x t_r).size - 1
Tactic: rcases t_r.size with - | t_r_size