awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
⊢ ∀ (r0 : r.size ≤ 1), BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + r.size + 1)
have node : ∀ (r0 : LE.le (α := ℕ) 0 1),
  BalancedSz 0 0 ∧ BalancedSz 0 0 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (HAdd.hAdd (α := ℕ) 0 0 + 1)
Tactic: rcases size r with (_ | _ | _)
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
node :
  ∀ (r0 : LE.le (α := ℕ) 0 1),
    BalancedSz 0 0 ∧ BalancedSz 0 0 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (HAdd.hAdd (α := ℕ) 0 0 + 1)
⊢ ∀ (r0 : r.size ≤ 1), BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + r.size + 1)
have node₁ : ∀ (r0 : HAdd.hAdd (α := ℕ) 0 1 ≤ 1),
  BalancedSz 0 0 ∧
    BalancedSz 0 (HAdd.hAdd (α := ℕ) 0 1) ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + HAdd.hAdd (α := ℕ) 0 1 + 1)
Tactic: rcases size r with (_ | _ | _)
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
node :
  ∀ (r0 : LE.le (α := ℕ) 0 1),
    BalancedSz 0 0 ∧ BalancedSz 0 0 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (HAdd.hAdd (α := ℕ) 0 0 + 1)
node₁ :
  ∀ (r0 : HAdd.hAdd (α := ℕ) 0 1 ≤ 1),
    BalancedSz 0 0 ∧
      BalancedSz 0 (HAdd.hAdd (α := ℕ) 0 1) ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + HAdd.hAdd (α := ℕ) 0 1 + 1)
⊢ ∀ (r0 : r.size ≤ 1), BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + r.size + 1)
have node₂ : ∀ (n : ℕ) (r0 : n + 1 + 1 ≤ 1),
  BalancedSz 0 0 ∧ BalancedSz 0 (n + 1 + 1) ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + (n + 1 + 1) + 1)
Tactic: rcases size r with (_ | _ | _)
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
⊢ ∀ (r0 : r.size ≤ 1), BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + r.size + 1)
have node : ∀ (r0 : LE.le (α := ℕ) 0 1),
  BalancedSz 0 0 ∧ BalancedSz 0 0 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (HAdd.hAdd (α := ℕ) 0 0 + 1)
Tactic: rcases size r with (_ | _ | _) <;>
      [decide; decide; (intro r0; unfold BalancedSz delta; lia)]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
node :
  ∀ (r0 : LE.le (α := ℕ) 0 1),
    BalancedSz 0 0 ∧ BalancedSz 0 0 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (HAdd.hAdd (α := ℕ) 0 0 + 1)
⊢ ∀ (r0 : r.size ≤ 1), BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + r.size + 1)
have node₁ : ∀ (r0 : HAdd.hAdd (α := ℕ) 0 1 ≤ 1),
  BalancedSz 0 0 ∧
    BalancedSz 0 (HAdd.hAdd (α := ℕ) 0 1) ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + HAdd.hAdd (α := ℕ) 0 1 + 1)
Tactic: rcases size r with (_ | _ | _) <;>
      [decide; decide; (intro r0; unfold BalancedSz delta; lia)]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
node :
  ∀ (r0 : LE.le (α := ℕ) 0 1),
    BalancedSz 0 0 ∧ BalancedSz 0 0 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (HAdd.hAdd (α := ℕ) 0 0 + 1)
node₁ :
  ∀ (r0 : HAdd.hAdd (α := ℕ) 0 1 ≤ 1),
    BalancedSz 0 0 ∧
      BalancedSz 0 (HAdd.hAdd (α := ℕ) 0 1) ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + HAdd.hAdd (α := ℕ) 0 1 + 1)
⊢ ∀ (r0 : r.size ≤ 1), BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + r.size + 1)
have node₂ : ∀ (n : ℕ) (r0 : n + 1 + 1 ≤ 1),
  BalancedSz 0 0 ∧ BalancedSz 0 (n + 1 + 1) ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + (n + 1 + 1) + 1)
Tactic: rcases size r with (_ | _ | _) <;>
      [decide; decide; (intro r0; unfold BalancedSz delta; lia)]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have node : ∀ (r0 : r.size = 0),
  BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Tactic: rcases Nat.eq_zero_or_pos (size r) with r0 | r0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size
node :
  ∀ (r0 : r.size = 0),
    BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have node₁ : ∀ (r0 : r.size > 0),
  BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Tactic: rcases Nat.eq_zero_or_pos (size r) with r0 | r0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size
r0 : r.size = 0
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have mr₃ : (Ordnode.node s ml z mr).size ≤ delta * 0
Tactic: rw [r0] at mr₂
Cleared hypotheses: mr₂, r0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size
r0 : r.size > 0
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have mr₃ : ratio * r.size ≤ ml.size + mr.size + 1
Tactic: rw [hm.2.size_eq] at lr₁ lr₂ mr₁ mr₂
Cleared hypotheses: mr₁, lr₁, lr₂, mr₂, r0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size
r0 : r.size > 0
mr₃ : ratio * r.size ≤ ml.size + mr.size + 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have lr₃ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
Tactic: rw [hm.2.size_eq] at lr₁ lr₂ mr₁ mr₂
Cleared hypotheses: mr₁, lr₁, lr₂, mr₂, r0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size
r0 : r.size > 0
mr₃ : ratio * r.size ≤ ml.size + mr.size + 1
lr₃ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have lr₄ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
Tactic: rw [hm.2.size_eq] at lr₁ lr₂ mr₁ mr₂
Cleared hypotheses: mr₁, lr₁, lr₂, mr₂, r0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size
r0 : r.size > 0
mr₃ : ratio * r.size ≤ ml.size + mr.size + 1
lr₃ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₄ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have mr₄ : ml.size + mr.size + 1 ≤ delta * r.size
Tactic: rw [hm.2.size_eq] at lr₁ lr₂ mr₁ mr₂
Cleared hypotheses: mr₁, lr₁, lr₂, mr₂, r0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have pos : ∀ (mm : ml.size + mr.size ≤ 1),
  BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Tactic: by_cases mm : size ml + size mr ≤ 1
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
pos :
  ∀ (mm : ml.size + mr.size ≤ 1),
    BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have neg : ∀ (mm : ¬ml.size + mr.size ≤ 1),
  BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Tactic: by_cases mm : size ml + size mr ≤ 1
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ml.size + mr.size ≤ 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have r1 : r.size = 1
Tactic: have r1 : r.size = 1 := by lia
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ml.size + mr.size ≤ 1
r1 : r.size = 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have l1 : l.size = 1
Tactic: have l1 : l.size = 1 := by lia
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ml.size + mr.size ≤ 1
r1 : r.size = 1
l1 : l.size = 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have lr₃ : 3 * l.size ≤ ml.size + mr.size + HAdd.hAdd (α := ℕ) 1 1
Tactic: rw [r1, add_assoc] at lr₁
Cleared hypotheses: lr₁, lr₂, mr₂, r0, mm, r1, l1
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + HAdd.hAdd (α := ℕ) 1 1
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ml.size + mr.size ≤ 1
r1 : r.size = 1
l1 : l.size = 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have pos : BalancedSz 1 ml.size ∧ BalancedSz mr.size 1 ∧ BalancedSz (1 + ml.size + 1) (mr.size + 1 + 1)
Tactic: rw [l1, r1]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + HAdd.hAdd (α := ℕ) 1 1
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ml.size + mr.size ≤ 1
r1 : r.size = 1
l1 : l.size = 1
⊢ BalancedSz 1 ml.size ∧ BalancedSz mr.size 1 ∧ BalancedSz (1 + ml.size + 1) (mr.size + 1 + 1)
have pos : ∀ (mm : ml.size + mr.size ≤ 1),
  BalancedSz 1 ml.size ∧ BalancedSz mr.size 1 ∧ BalancedSz (1 + ml.size + 1) (mr.size + 1 + 1)
Tactic: revert mm
Cleared hypotheses: mm
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + HAdd.hAdd (α := ℕ) 1 1
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
⊢ ∀ (mm : ml.size + mr.size ≤ 1),
    BalancedSz 1 ml.size ∧ BalancedSz mr.size 1 ∧ BalancedSz (1 + ml.size + 1) (mr.size + 1 + 1)
have pos : ∀ (mm : 0 + mr.size ≤ 1),
  BalancedSz 1 0 ∧ BalancedSz mr.size 1 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 1 0 + 1) (mr.size + 1 + 1)
Tactic: cases size ml
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + HAdd.hAdd (α := ℕ) 1 1
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
pos :
  ∀ (mm : 0 + mr.size ≤ 1),
    BalancedSz 1 0 ∧ BalancedSz mr.size 1 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 1 0 + 1) (mr.size + 1 + 1)
⊢ ∀ (mm : ml.size + mr.size ≤ 1),
    BalancedSz 1 ml.size ∧ BalancedSz mr.size 1 ∧ BalancedSz (1 + ml.size + 1) (mr.size + 1 + 1)
have pos₁ : ∀ (n : ℕ) (mm : n + 1 + mr.size ≤ 1),
  BalancedSz 1 (n + 1) ∧ BalancedSz mr.size 1 ∧ BalancedSz (1 + (n + 1) + 1) (mr.size + 1 + 1)
Tactic: cases size ml
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + HAdd.hAdd (α := ℕ) 1 1
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
⊢ ∀ (mm : 0 + mr.size ≤ 1),
    BalancedSz 1 0 ∧ BalancedSz mr.size 1 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 1 0 + 1) (mr.size + 1 + 1)
have pos : ∀ (mm : HAdd.hAdd (α := ℕ) 0 0 ≤ 1),
  BalancedSz 1 0 ∧ BalancedSz 0 1 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 1 0 + 1) (HAdd.hAdd (α := ℕ) 0 1 + 1)
Tactic: cases size mr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + HAdd.hAdd (α := ℕ) 1 1
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
pos :
  ∀ (mm : HAdd.hAdd (α := ℕ) 0 0 ≤ 1),
    BalancedSz 1 0 ∧ BalancedSz 0 1 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 1 0 + 1) (HAdd.hAdd (α := ℕ) 0 1 + 1)
⊢ ∀ (mm : 0 + mr.size ≤ 1),
    BalancedSz 1 0 ∧ BalancedSz mr.size 1 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 1 0 + 1) (mr.size + 1 + 1)
have pos₁ : ∀ (n : ℕ) (mm : 0 + (n + 1) ≤ 1),
  BalancedSz 1 0 ∧ BalancedSz (n + 1) 1 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 1 0 + 1) (n + 1 + 1 + 1)
Tactic: cases size mr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + HAdd.hAdd (α := ℕ) 1 1
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
n : ℕ
⊢ ∀ (mm : n + 1 + mr.size ≤ 1),
    BalancedSz 1 (n + 1) ∧ BalancedSz mr.size 1 ∧ BalancedSz (1 + (n + 1) + 1) (mr.size + 1 + 1)
have pos : ∀ (mm : n + 1 + 0 ≤ 1),
  BalancedSz 1 (n + 1) ∧ BalancedSz 0 1 ∧ BalancedSz (1 + (n + 1) + 1) (HAdd.hAdd (α := ℕ) 0 1 + 1)
Tactic: cases size mr