awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H :
  (∃ (l' : ℕ),
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ (r' : ℕ),
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ ((Ordnode.node ls ll lx lr).balanceL (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).1
        (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2).size =
    ls + rs
have refine_3 : (Ordnode.node ls ll lx lr).size + (rl.node' rx rr).size = ls + (rl.size + rr.size + 1)
Tactic: rw [size_balanceL hl.3 v.3 hl.2 v.2 H, add_assoc, ← e, hr.2.1]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
⊢ Valid' o₁
      ((Ordnode.node ls ll lx lr).balanceL (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).1
        (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2)
      o₂ ∧
    ((Ordnode.node ls ll lx lr).balanceL (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).1
          (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2).size =
      ls + rs
have neg : (∃ (l' : ℕ),
    Raised l' (Ordnode.node ls ll lx lr).size ∧
      BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
  ∃ (r' : ℕ),
    Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
      BalancedSz (Ordnode.node ls ll lx lr).size r'
Tactic: suffices H : _ by
        refine ⟨Valid'.balanceL (hl.of_lt ?_ ?_) v H, ?_⟩
        · refine @findMin'_all (P := fun a : α => Bounded nil o₁ (a : WithBot α))
            _ rl rx (sep.2.1.1.imp ?_) hr.1.1.to_nil
          exact fun y h => hl.1.1.to_nil.mono_right (le_of_lt h)
        · exact
            @findMin'_all _ (fun a => All (· < a) (.node ls ll lx lr)) rl rx
              (all_iff_forall.2 fun x hx => sep.imp fun y hy => all_iff_forall.1 hy.1 _ hx)
              (sep.imp fun y hy => hy.2.1)
        · rw [size_balanceL hl.3 v.3 hl.2 v.2 H, add_assoc, ← e, hr.2.1]; rfl
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
⊢ (∃ (l' : ℕ),
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ (r' : ℕ),
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
have neg : BalancedSz (Ordnode.node ls ll lx lr).size (rl.node' rx rr).size
Tactic: refine Or.inr ⟨_, Or.inr e, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
⊢ BalancedSz (Ordnode.node ls ll lx lr).size (rl.node' rx rr).size
have neg : ∀ (bal : BalancedSz (Ordnode.node ls ll lx lr).size (rl.node' rx rr).size),
  ¬ls > rs →
    ∀ (v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂)
      (e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1),
      BalancedSz (Ordnode.node ls ll lx lr).size (rl.node' rx rr).size
Tactic: rwa [hr.2.eq_node'] at bal
Cleared hypotheses: bal, h, v, e
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * ls < rs
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ls + rl.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
have e₁ : t.size = ll.size + lr.size + 1 + rl.size
Tactic: rw [hl.2.1] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * ls < rs
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
have h₁ : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
Tactic: rw [hl.2.1, hr.2.1, delta] at h
Cleared hypotheses: h, v, e
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
have inl : ∀ (H : rl.size + rr.size ≤ 1), Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
Tactic: rcases hr.3.1 with (H | ⟨hr₁, hr₂⟩)
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
inl : ∀ (H : rl.size + rr.size ≤ 1), Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
have inr : ∀ (hr₁ : rl.size ≤ delta * rr.size) (hr₂ : rr.size ≤ delta * rl.size),
  Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
Tactic: rcases hr.3.1 with (H | ⟨hr₁, hr₂⟩)
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
have refine_1 : 2 * t.size ≤ 9 * rr.size + 5 ∨ t.size ≤ 3
Tactic: refine ⟨Valid'.balanceL_aux v hr.right H₁ H₂ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
refine_1 : 2 * t.size ≤ 9 * rr.size + 5 ∨ t.size ≤ 3
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
have refine_2 : (t.balanceL rx rr).size = ls + rs
Tactic: refine ⟨Valid'.balanceL_aux v hr.right H₁ H₂ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ 2 * t.size ≤ 9 * rr.size + 5 ∨ t.size ≤ 3
have refine_1 : 2 * (ll.size + lr.size + 1 + rl.size) ≤ 9 * rr.size + 5 ∨ ll.size + lr.size + 1 + rl.size ≤ 3
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ (t.balanceL rx rr).size = ls + rs
have refine_2 : ll.size + lr.size + 1 + rl.size + rr.size + 1 = ll.size + lr.size + 1 + (rl.size + rr.size + 1)
Tactic: rw [balanceL_eq_balance v.2 hr.2.2.2 H₁ H₂, balance_eq_balance' v.3 hr.3.2.2 v.2 hr.2.2.2,
          size_balance' v.2 hr.2.2.2, e, hl.2.1, hr.2.1]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
have suffices : t.size = 0 → rr.size ≤ 1
Tactic: suffices H₁ : _ by
      refine ⟨Valid'.balanceL_aux v hr.right H₁ H₂ ?_, ?_⟩
      · rw [e]; exact Or.inl (Valid'.merge_lemma h hr₁)
      · rw [balanceL_eq_balance v.2 hr.2.2.2 H₁ H₂, balance_eq_balance' v.3 hr.3.2.2 v.2 hr.2.2.2,
          size_balance' v.2 hr.2.2.2, e, hl.2.1, hr.2.1]
        abel
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
⊢ t.size = 0 → rr.size ≤ 1
have rw : ll.size + lr.size + rl.size + 1 = 0 → rr.size ≤ 1
Tactic: rw [e, add_right_comm]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
have inr : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
Tactic: suffices H₂ : _ by
    suffices H₁ : _ by
      refine ⟨Valid'.balanceL_aux v hr.right H₁ H₂ ?_, ?_⟩
      · rw [e]; exact Or.inl (Valid'.merge_lemma h hr₁)
      · rw [balanceL_eq_balance v.2 hr.2.2.2 H₁ H₂, balance_eq_balance' v.3 hr.3.2.2 v.2 hr.2.2.2,
          size_balance' v.2 hr.2.2.2, e, hl.2.1, hr.2.1]
        abel
    · rw [e, add_right_comm]; rintro ⟨⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
h_1 : 1 ≤ t.size
h_2 : 1 ≤ rr.size
⊢ rr.size ≤ delta * t.size
have inr : rr.size ≤ delta * (ll.size + lr.size + 1 + rl.size)
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l o₂
hr : Valid' o₁ r o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) l
⊢ Valid' o₁ (l.merge r) o₂ ∧ (l.merge r).size = l.size + r.size
have node : ∀ (ls : ℕ) (ll : Ordnode α) (lx : α) (lr : Ordnode α),
  (∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ ll o₂) (hr : Valid' o₁ r o₂)
      (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) ll),
      Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size) →
    ∀
      (IHlr :
        ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ lr o₂) (hr : Valid' o₁ r o₂)
          (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) lr),
          Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size)
      {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂)
      (hr : Valid' o₁ r o₂) (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) (Ordnode.node ls ll lx lr)),
      Valid' o₁ ((Ordnode.node ls ll lx lr).merge r) o₂ ∧
        ((Ordnode.node ls ll lx lr).merge r).size = (Ordnode.node ls ll lx lr).size + r.size
Tactic: induction l generalizing o₁ o₂ r with
  | nil => exact ⟨hr, (zero_add _).symm⟩
  | node ls ll lx lr _ IHlr => ?_
Cleared hypotheses: l, r, o₁, o₂, hl, hr, sep
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ ll o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) ll),
    Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ lr o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) lr),
    Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ r o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) (Ordnode.node ls ll lx lr)
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).merge r) o₂ ∧
    ((Ordnode.node ls ll lx lr).merge r).size = (Ordnode.node ls ll lx lr).size + r.size
have node : ∀ (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α)
  (IHrl :
    ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rl o₂)
      (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rl) (Ordnode.node ls ll lx lr)),
      Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) o₂ ∧
        ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size),
  (∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rr o₂)
      (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rr) (Ordnode.node ls ll lx lr)),
      Valid' o₁ ((Ordnode.node ls ll lx lr).merge rr) o₂ ∧
        ((Ordnode.node ls ll lx lr).merge rr).size = (Ordnode.node ls ll lx lr).size + rr.size) →
    ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂)
      (hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂)
      (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)),
      Valid' o₁ ((Ordnode.node ls ll lx lr).merge (Ordnode.node rs rl rx rr)) o₂ ∧
        ((Ordnode.node ls ll lx lr).merge (Ordnode.node rs rl rx rr)).size =
          (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size
Tactic: induction r generalizing o₁ o₂ with
  | nil => exact ⟨hl, rfl⟩
  | node rs rl rx rr IHrl _ => ?_
Cleared hypotheses: r, o₁, o₂, hl, hr, sep
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ ll o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) ll),
    Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ lr o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) lr),
    Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
IHrl :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rl o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rl) (Ordnode.node ls ll lx lr)),
    Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) o₂ ∧
      ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size
r_ih :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rr o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rr) (Ordnode.node ls ll lx lr)),
    Valid' o₁ ((Ordnode.node ls ll lx lr).merge rr) o₂ ∧
      ((Ordnode.node ls ll lx lr).merge rr).size = (Ordnode.node ls ll lx lr).size + rr.size
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).merge (Ordnode.node rs rl rx rr)) o₂ ∧
    ((Ordnode.node ls ll lx lr).merge (Ordnode.node rs rl rx rr)).size =
      (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size
have node : Valid' o₁
    (if delta * ls < rs then ((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr
    else
      if delta * rs < ls then ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))
      else (Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr))
    o₂ ∧
  (if delta * ls < rs then ((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr
      else
        if delta * rs < ls then ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))
        else (Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr)).size =
    (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size
Tactic: rw [merge_node]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ ll o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) ll),
    Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ lr o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) lr),
    Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
IHrl :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rl o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rl) (Ordnode.node ls ll lx lr)),
    Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) o₂ ∧
      ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size
r_ih :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rr o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rr) (Ordnode.node ls ll lx lr)),
    Valid' o₁ ((Ordnode.node ls ll lx lr).merge rr) o₂ ∧
      ((Ordnode.node ls ll lx lr).merge rr).size = (Ordnode.node ls ll lx lr).size + rr.size
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
⊢ Valid' o₁
      (if delta * ls < rs then ((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr
      else
        if delta * rs < ls then ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))
        else (Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr))
      o₂ ∧
    (if delta * ls < rs then ((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr
        else
          if delta * rs < ls then ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))
          else (Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr)).size =
      (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size
have pos : ∀ (h : delta * ls < rs),
  Valid' o₁ (((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr) o₂ ∧
    (((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr).size =
      (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size
Tactic: split_ifs with h h_1