awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (l.node' x r) o₂
⊢ Valid' o₁ (l.node' x r).eraseMax (↑(findMax' x r) : WithTop α) ∧ (l.node' x r).size = (l.node' x r).eraseMax.size + 1
have nil : ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x nil) o₂),
  Valid' o₁ (l.node' x nil).eraseMax (↑(findMax' x nil) : WithTop α) ∧
    (l.node' x nil).size = (l.node' x nil).eraseMax.size + 1
Tactic: induction r generalizing l x o₁ with
  | nil => exact ⟨H.left, rfl⟩
  | node rs rl rx rr _ IHrr =>
    have := H.2.2.2.eq_node'; rw [this] at H ⊢
    rcases IHrr H.right with ⟨h, e⟩
    refine ⟨Valid'.balanceL H.left h (Or.inr ⟨_, Or.inr e, H.3.1⟩), ?_⟩
    rw [eraseMax, size_balanceL H.3.2.1 h.3 H.2.2.1 h.2 (Or.inr ⟨_, Or.inr e, H.3.1⟩)]
    rw [size_node, e]; rfl
Cleared hypotheses: l, x, r, o₁, H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (l.node' x r) o₂
nil :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x Ordnode.nil) o₂),
    Valid' o₁ (l.node' x Ordnode.nil).eraseMax (↑(findMax' x Ordnode.nil) : WithTop α) ∧
      (l.node' x Ordnode.nil).size = (l.node' x Ordnode.nil).eraseMax.size + 1
⊢ Valid' o₁ (l.node' x r).eraseMax (↑(findMax' x r) : WithTop α) ∧ (l.node' x r).size = (l.node' x r).eraseMax.size + 1
have node : ∀ (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α),
  (∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rl) o₂),
      Valid' o₁ (l.node' x rl).eraseMax (↑(findMax' x rl) : WithTop α) ∧
        (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1) →
    ∀
      (IHrr :
        ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rr) o₂),
          Valid' o₁ (l.node' x rr).eraseMax (↑(findMax' x rr) : WithTop α) ∧
            (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1)
      {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)) o₂),
      Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)).eraseMax (↑(findMax' x (Ordnode.node rs rl rx rr)) : WithTop α) ∧
        (l.node' x (Ordnode.node rs rl rx rr)).size = (l.node' x (Ordnode.node rs rl rx rr)).eraseMax.size + 1
Tactic: induction r generalizing l x o₁ with
  | nil => exact ⟨H.left, rfl⟩
  | node rs rl rx rr _ IHrr =>
    have := H.2.2.2.eq_node'; rw [this] at H ⊢
    rcases IHrr H.right with ⟨h, e⟩
    refine ⟨Valid'.balanceL H.left h (Or.inr ⟨_, Or.inr e, H.3.1⟩), ?_⟩
    rw [eraseMax, size_balanceL H.3.2.1 h.3 H.2.2.1 h.2 (Or.inr ⟨_, Or.inr e, H.3.1⟩)]
    rw [size_node, e]; rfl
Cleared hypotheses: l, x, r, o₁, H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
⊢ Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
have this : Valid' o₂ (r.dual.node' x l.dual).eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
  (r.dual.node' x l.dual).size = (r.dual.node' x l.dual).eraseMax.size + 1
Tactic: have := H.dual.eraseMax_aux
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
this :
  Valid' o₂ (r.dual.node' x l.dual).eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
    (r.dual.node' x l.dual).size = (r.dual.node' x l.dual).eraseMax.size + 1
⊢ Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
have rwa : ∀
  (this :
    Valid' o₂ (l.node' x r).dual.eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
      (l.node' x r).dual.size = (l.node' x r).dual.eraseMax.size + 1),
  Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
Tactic: rwa [← dual_node', size_dual, ← dual_eraseMin, size_dual, ← Valid'.dual_iff, findMax'_dual]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
this :
  Valid' o₂ (r.dual.node' x l.dual).eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
    (r.dual.node' x l.dual).size = (r.dual.node' x l.dual).eraseMax.size + 1
rwa :
  ∀
    (this :
      Valid' o₂ (l.node' x r).dual.eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).dual.size = (l.node' x r).dual.eraseMax.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
⊢ Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
have rwa₁ : ∀
  (this :
    Valid' o₂ (l.node' x r).dual.eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
      (l.node' x r).size = (l.node' x r).dual.eraseMax.size + 1),
  Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
Tactic: rwa [← dual_node', size_dual, ← dual_eraseMin, size_dual, ← Valid'.dual_iff, findMax'_dual]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
this :
  Valid' o₂ (r.dual.node' x l.dual).eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
    (r.dual.node' x l.dual).size = (r.dual.node' x l.dual).eraseMax.size + 1
rwa :
  ∀
    (this :
      Valid' o₂ (l.node' x r).dual.eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).dual.size = (l.node' x r).dual.eraseMax.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
rwa₁ :
  ∀
    (this :
      Valid' o₂ (l.node' x r).dual.eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).size = (l.node' x r).dual.eraseMax.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
⊢ Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
have rwa₂ : ∀
  (this :
    Valid' o₂ (l.node' x r).eraseMin.dual (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
      (l.node' x r).size = (l.node' x r).eraseMin.dual.size + 1),
  Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
Tactic: rwa [← dual_node', size_dual, ← dual_eraseMin, size_dual, ← Valid'.dual_iff, findMax'_dual]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
this :
  Valid' o₂ (r.dual.node' x l.dual).eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
    (r.dual.node' x l.dual).size = (r.dual.node' x l.dual).eraseMax.size + 1
rwa :
  ∀
    (this :
      Valid' o₂ (l.node' x r).dual.eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).dual.size = (l.node' x r).dual.eraseMax.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
rwa₁ :
  ∀
    (this :
      Valid' o₂ (l.node' x r).dual.eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).size = (l.node' x r).dual.eraseMax.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
rwa₂ :
  ∀
    (this :
      Valid' o₂ (l.node' x r).eraseMin.dual (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).size = (l.node' x r).eraseMin.dual.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
⊢ Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
have rwa₃ : ∀
  (this :
    Valid' o₂ (l.node' x r).eraseMin.dual (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1),
  Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
Tactic: rwa [← dual_node', size_dual, ← dual_eraseMin, size_dual, ← Valid'.dual_iff, findMax'_dual]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
this :
  Valid' o₂ (r.dual.node' x l.dual).eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
    (r.dual.node' x l.dual).size = (r.dual.node' x l.dual).eraseMax.size + 1
rwa :
  ∀
    (this :
      Valid' o₂ (l.node' x r).dual.eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).dual.size = (l.node' x r).dual.eraseMax.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
rwa₁ :
  ∀
    (this :
      Valid' o₂ (l.node' x r).dual.eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).size = (l.node' x r).dual.eraseMax.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
rwa₂ :
  ∀
    (this :
      Valid' o₂ (l.node' x r).eraseMin.dual (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).size = (l.node' x r).eraseMin.dual.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
rwa₃ :
  ∀
    (this :
      Valid' o₂ (l.node' x r).eraseMin.dual (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).size = (l.node' x r).eraseMin.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
⊢ Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
have rwa₄ : ∀
  (this :
    Valid' (↑(findMax' x l.dual) : WithTop αᵒᵈ) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1),
  Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
Tactic: rwa [← dual_node', size_dual, ← dual_eraseMin, size_dual, ← Valid'.dual_iff, findMax'_dual]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
this :
  Valid' o₂ (r.dual.node' x l.dual).eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
    (r.dual.node' x l.dual).size = (r.dual.node' x l.dual).eraseMax.size + 1
rwa :
  ∀
    (this :
      Valid' o₂ (l.node' x r).dual.eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).dual.size = (l.node' x r).dual.eraseMax.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
rwa₁ :
  ∀
    (this :
      Valid' o₂ (l.node' x r).dual.eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).size = (l.node' x r).dual.eraseMax.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
rwa₂ :
  ∀
    (this :
      Valid' o₂ (l.node' x r).eraseMin.dual (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).size = (l.node' x r).eraseMin.dual.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
rwa₃ :
  ∀
    (this :
      Valid' o₂ (l.node' x r).eraseMin.dual (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).size = (l.node' x r).eraseMin.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
rwa₄ :
  ∀
    (this :
      Valid' (↑(findMax' x l.dual) : WithTop αᵒᵈ) (l.node' x r).eraseMin o₂ ∧
        (l.node' x r).size = (l.node' x r).eraseMin.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
⊢ Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
have rwa₅ : ∀
  (this :
    Valid' (↑(l.findMin' x) : WithTop αᵒᵈ) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1),
  Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
Tactic: rwa [← dual_node', size_dual, ← dual_eraseMin, size_dual, ← Valid'.dual_iff, findMax'_dual]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node size l x r).Valid
⊢ (node size l x r).eraseMin.Valid
have rw : (l.node' x r).eraseMin.Valid
Tactic: rw [h.2.eq_node']
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
h : t.Valid
⊢ t.eraseMax.Valid
have rw : t.dual.eraseMin.Valid
Tactic: rw [Valid.dual_iff, dual_eraseMax]
-- 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
bal : BalancedSz l.size r.size
⊢ Valid' o₁ (l.glue r) o₂ ∧ (l.glue r).size = l.size + r.size
have nil : ∀ (hl : Valid' o₁ nil o₂) (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) nil)
  (bal : BalancedSz (size.{u_1} (α := α) nil) r.size),
  Valid' o₁ (glue nil r) o₂ ∧ (glue nil r).size = size.{u_1} (α := α) nil + r.size
Tactic: obtain - | ⟨ls, ll, lx, lr⟩ := l
Cleared hypotheses: l, hl, sep, bal
-- 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
bal : BalancedSz l.size r.size
nil :
  ∀ (hl : Valid' o₁ Ordnode.nil o₂) (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) Ordnode.nil)
    (bal : BalancedSz (size.{u_1} (α := α) Ordnode.nil) r.size),
    Valid' o₁ (glue Ordnode.nil r) o₂ ∧ (glue Ordnode.nil r).size = size.{u_1} (α := α) Ordnode.nil + r.size
⊢ Valid' o₁ (l.glue r) o₂ ∧ (l.glue r).size = l.size + r.size
have node : ∀ (ls : ℕ) (ll : Ordnode α) (lx : α) (lr : Ordnode α) (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂)
  (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) (Ordnode.node ls ll lx lr))
  (bal : BalancedSz (Ordnode.node ls ll lx lr).size r.size),
  Valid' o₁ ((Ordnode.node ls ll lx lr).glue r) o₂ ∧
    ((Ordnode.node ls ll lx lr).glue r).size = (Ordnode.node ls ll lx lr).size + r.size
Tactic: obtain - | ⟨ls, ll, lx, lr⟩ := l
Cleared hypotheses: l, hl, sep, bal
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hr : Valid' o₁ r o₂
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size r.size
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).glue r) o₂ ∧
    ((Ordnode.node ls ll lx lr).glue r).size = (Ordnode.node ls ll lx lr).size + r.size
have node : ∀ (hr : Valid' o₁ nil o₂) (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) nil) (Ordnode.node ls ll lx lr))
  (bal : BalancedSz (Ordnode.node ls ll lx lr).size (size.{u_1} (α := α) nil)),
  Valid' o₁ ((Ordnode.node ls ll lx lr).glue nil) o₂ ∧
    ((Ordnode.node ls ll lx lr).glue nil).size = (Ordnode.node ls ll lx lr).size + size.{u_1} (α := α) nil
Tactic: obtain - | ⟨rs, rl, rx, rr⟩ := r
Cleared hypotheses: r, hr, sep, bal
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hr : Valid' o₁ r o₂
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size r.size
node :
  ∀ (hr : Valid' o₁ nil o₂) (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) nil) (Ordnode.node ls ll lx lr))
    (bal : BalancedSz (Ordnode.node ls ll lx lr).size (size.{u_1} (α := α) nil)),
    Valid' o₁ ((Ordnode.node ls ll lx lr).glue nil) o₂ ∧
      ((Ordnode.node ls ll lx lr).glue nil).size = (Ordnode.node ls ll lx lr).size + size.{u_1} (α := α) nil
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).glue r) o₂ ∧
    ((Ordnode.node ls ll lx lr).glue r).size = (Ordnode.node ls ll lx lr).size + r.size
have node₁ : ∀ (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),
  Valid' o₁ ((Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr)) o₂ ∧
    ((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: obtain - | ⟨rs, rl, rx, rr⟩ := r
Cleared hypotheses: r, hr, sep, bal
-- 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
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr)) o₂ ∧
    ((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 node : Valid' o₁
    (if ls > rs then (ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)
    else (Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2)
    o₂ ∧
  (if ls > rs then (ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)
      else (Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2).size =
    ls + rs
Tactic: dsimp [glue]
-- 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
⊢ Valid' o₁
      (if ls > rs then (ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)
      else (Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2)
      o₂ ∧
    (if ls > rs then (ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)
        else (Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2).size =
      ls + rs
have pos : ls > rs →
  Valid' o₁ ((ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)) o₂ ∧
    ((ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)).size = ls + rs
Tactic: split_ifs
-- 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
pos :
  ls > rs →
    Valid' o₁ ((ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)) o₂ ∧
      ((ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)).size = ls + rs
⊢ Valid' o₁
      (if ls > rs then (ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)
      else (Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2)
      o₂ ∧
    (if ls > rs then (ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)
        else (Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2).size =
      ls + rs
have neg : ¬ls > rs →
  Valid' o₁ ((Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2) o₂ ∧
    ((Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2).size = ls + rs
Tactic: split_ifs
-- 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
⊢ Valid' o₁ ((ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)) o₂ ∧
    ((ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)).size = ls + rs
have pos : Valid' o₁
    (((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.balanceR
      ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr))
    o₂ ∧
  (((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.balanceR
        ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr)).size =
    ls + rs
Tactic: rw [splitMax_eq]
-- 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 α
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
⊢ Valid' o₁
      (((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.balanceR
        ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr))
      o₂ ∧
    (((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.balanceR
          ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2
          (Ordnode.node rs rl rx rr)).size =
      ls + rs
have v : Valid' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)
Tactic: obtain ⟨v, e⟩ := Valid'.eraseMax_aux hl