awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
⊢ 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) (h_1 : delta * rs < ls),
  Valid' o₁ (ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))) o₂ ∧
    (ll.balanceR 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: split_ifs with h h_1
-- 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)
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
pos₁ :
  ∀ (h : ¬delta * ls < rs) (h_1 : delta * rs < ls),
    Valid' o₁ (ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))) o₂ ∧
      (ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))).size =
        (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size
⊢ 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 neg : ∀ (h : ¬delta * ls < rs) (h_1 : ¬delta * rs < ls),
  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: split_ifs with h h_1
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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)
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
have v : Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) (↑rx : WithTop α)
Tactic: obtain ⟨v, e⟩ := IHrl (hl.of_lt hr.1.1.to_nil <| sep.imp fun x h => h.2.1) hr.left
      (sep.imp fun x h => h.1)
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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)
h : delta * ls < rs
v : Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) (↑rx : WithTop α)
⊢ 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
have e : ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size
Tactic: obtain ⟨v, e⟩ := IHrl (hl.of_lt hr.1.1.to_nil <| sep.imp fun x h => h.2.1) hr.left
      (sep.imp fun x h => h.1)
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
⊢ Valid' o₁ (ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))) o₂ ∧
    (ll.balanceR 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 v : Valid' (↑lx : WithBot α) (lr.merge (Ordnode.node rs rl rx rr)) o₂
Tactic: obtain ⟨v, e⟩ := IHlr hl.right (hr.of_gt hl.1.2.to_nil sep.2.1) sep.2.2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
v : Valid' (↑lx : WithBot α) (lr.merge (Ordnode.node rs rl rx rr)) o₂
⊢ Valid' o₁ (ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))) o₂ ∧
    (ll.balanceR 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 e : (lr.merge (Ordnode.node rs rl rx rr)).size = lr.size + (Ordnode.node rs rl rx rr).size
Tactic: obtain ⟨v, e⟩ := IHlr hl.right (hr.of_gt hl.1.2.to_nil sep.2.1) sep.2.2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
v : Valid' (↑lx : WithBot α) (lr.merge (Ordnode.node rs rl rx rr)) o₂
e : (lr.merge (Ordnode.node rs rl rx rr)).size = lr.size + (Ordnode.node rs rl rx rr).size
⊢ Valid' o₁ (ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))) o₂ ∧
    (ll.balanceR 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 this : ∀ (e : (lr.merge (Ordnode.node rs rl rx rr)).dual.size = rs + lr.dual.size),
  Valid' o₂ ((lr.merge (Ordnode.node rs rl rx rr)).dual.balanceL lx ll.dual) o₁ ∧
    ((lr.merge (Ordnode.node rs rl rx rr)).dual.balanceL lx ll.dual).size = rs + ls
Tactic: have := Valid'.merge_aux₁ hr.dual hl.dual h_1 v.dual
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
v : Valid' (↑lx : WithBot α) (lr.merge (Ordnode.node rs rl rx rr)) o₂
e : (lr.merge (Ordnode.node rs rl rx rr)).size = lr.size + (Ordnode.node rs rl rx rr).size
this :
  ∀ (e : (lr.merge (Ordnode.node rs rl rx rr)).dual.size = rs + lr.dual.size),
    Valid' o₂ ((lr.merge (Ordnode.node rs rl rx rr)).dual.balanceL lx ll.dual) o₁ ∧
      ((lr.merge (Ordnode.node rs rl rx rr)).dual.balanceL lx ll.dual).size = rs + ls
⊢ Valid' o₁ (ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))) o₂ ∧
    (ll.balanceR 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 this₁ : ∀ (e : (lr.merge (Ordnode.node rs rl rx rr)).size = lr.size + rs),
  Valid' o₁ (ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))) o₂ ∧
    (ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))).size = ls + rs
Tactic: rw [size_dual, add_comm, size_dual, ← dual_balanceR, ← Valid'.dual_iff, size_dual,
      add_comm rs] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
⊢ Valid' o₁ (insertWith f x (node sz l y r)) o₂ ∧ Raised (node sz l y r).size (insertWith f x (node sz l y r)).size
have rw : Valid' o₁
    (match (motive := Ordering → Ordnode α)
      if x ≤ y then if y ≤ x then Ordering.eq else Ordering.lt else Ordering.gt with
    | Ordering.lt => (insertWith f x l).balanceL y r
    | Ordering.eq => node sz l (f y) r
    | Ordering.gt => l.balanceR y (insertWith f x r))
    o₂ ∧
  Raised (node sz l y r).size
    (size.{u_1} (α := α)
      (match (motive := Ordering → Ordnode α)
        if x ≤ y then if y ≤ x then Ordering.eq else Ordering.lt else Ordering.gt with
      | Ordering.lt => (insertWith f x l).balanceL y r
      | Ordering.eq => node sz l (f y) r
      | Ordering.gt => l.balanceR y (insertWith f x r)))
Tactic: rw [insertWith, cmpLE]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
⊢ Valid' o₁
      (match (motive := Ordering → Ordnode α)
        if x ≤ y then if y ≤ x then Ordering.eq else Ordering.lt else Ordering.gt with
      | Ordering.lt => (insertWith f x l).balanceL y r
      | Ordering.eq => node sz l (f y) r
      | Ordering.gt => l.balanceR y (insertWith f x r))
      o₂ ∧
    Raised (node sz l y r).size
      (size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α)
          if x ≤ y then if y ≤ x then Ordering.eq else Ordering.lt else Ordering.gt with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r)))
have pos : ∀ (h_1 : x ≤ y) (h_2 : y ≤ x),
  Valid' o₁
      (match (motive := Ordering → Ordnode α) Ordering.eq with
      | Ordering.lt => (insertWith f x l).balanceL y r
      | Ordering.eq => node sz l (f y) r
      | Ordering.gt => l.balanceR y (insertWith f x r))
      o₂ ∧
    Raised (node sz l y r).size
      (size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) Ordering.eq with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r)))
Tactic: split_ifs with h_1 h_2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
pos :
  ∀ (h_1 : x ≤ y) (h_2 : y ≤ x),
    Valid' o₁
        (match (motive := Ordering → Ordnode α) Ordering.eq with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r))
        o₂ ∧
      Raised (node sz l y r).size
        (size.{u_1} (α := α)
          (match (motive := Ordering → Ordnode α) Ordering.eq with
          | Ordering.lt => (insertWith f x l).balanceL y r
          | Ordering.eq => node sz l (f y) r
          | Ordering.gt => l.balanceR y (insertWith f x r)))
⊢ Valid' o₁
      (match (motive := Ordering → Ordnode α)
        if x ≤ y then if y ≤ x then Ordering.eq else Ordering.lt else Ordering.gt with
      | Ordering.lt => (insertWith f x l).balanceL y r
      | Ordering.eq => node sz l (f y) r
      | Ordering.gt => l.balanceR y (insertWith f x r))
      o₂ ∧
    Raised (node sz l y r).size
      (size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α)
          if x ≤ y then if y ≤ x then Ordering.eq else Ordering.lt else Ordering.gt with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r)))
have neg : ∀ (h_1 : x ≤ y) (h_2 : ¬y ≤ x),
  Valid' o₁
      (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (insertWith f x l).balanceL y r
      | Ordering.eq => node sz l (f y) r
      | Ordering.gt => l.balanceR y (insertWith f x r))
      o₂ ∧
    Raised (node sz l y r).size
      (size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) Ordering.lt with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r)))
Tactic: split_ifs with h_1 h_2