awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
h : ¬l + r₂ ≤ 1
H : l + r₁ ≤ 1
inl : ∀ (h₁ : r₁ ≤ 0) (h₂ : l + 0 ≤ 1 ∨ 0 ≤ delta * l) (h : ¬l + 0 ≤ 1), l ≤ delta * 0
⊢ l ≤ delta * r₂
have inl₁ : ∀ (n : ℕ) (h₁ : r₁ ≤ n + 1) (h₂ : l + (n + 1) ≤ 1 ∨ n + 1 ≤ delta * l) (h : ¬l + (n + 1) ≤ 1), l ≤ delta * (n + 1)
Tactic: cases r₂
Cleared hypotheses: r₂, h₁, h₂, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
h : ¬l + r₂ ≤ 1
⊢ l ≤ delta * r₂
have inl : ∀ (H : l + r₁ ≤ 1), l ≤ delta * r₂
Tactic: cases H with
  | inl H =>
    cases r₂
    · cases h (le_trans (Nat.add_le_add_left (Nat.zero_le _) _) H)
    · exact le_trans (le_trans (Nat.le_add_right _ _) H) (Nat.le_add_left 1 _)
  | inr H =>
    exact le_trans H.1 (Nat.mul_le_mul_left _ h₁)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
h : ¬l + r₂ ≤ 1
inl : ∀ (H : l + r₁ ≤ 1), l ≤ delta * r₂
⊢ l ≤ delta * r₂
have inr : ∀ (H : l ≤ delta * r₁ ∧ r₁ ≤ delta * l), l ≤ delta * r₂
Tactic: cases H with
  | inl H =>
    cases r₂
    · cases h (le_trans (Nat.add_le_add_left (Nat.zero_le _) _) H)
    · exact le_trans (le_trans (Nat.le_add_right _ _) H) (Nat.le_add_left 1 _)
  | inr H =>
    exact le_trans H.1 (Nat.mul_le_mul_left _ h₁)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
⊢ BalancedSz r.dual.size l.dual.size
have rw : BalancedSz r.size l.size
Tactic: rw [size_dual, size_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node4L x m y r).dual = r.dual.node4R y m.dual x l.dual
have nil : (l.node4L x nil y r).dual = r.dual.node4R y (dual nil) x l.dual
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
nil : (l.node4L x Ordnode.nil y r).dual = r.dual.node4R y (dual Ordnode.nil) x l.dual
⊢ (l.node4L x m y r).dual = r.dual.node4R y m.dual x l.dual
have node : ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α),
  (l.node4L x (node size l_1 x_1 r_1) y r).dual = r.dual.node4R y (node size l_1 x_1 r_1).dual x l.dual
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node4R x m y r).dual = r.dual.node4L y m.dual x l.dual
have nil : (l.node4R x nil y r).dual = r.dual.node4L y (dual nil) x l.dual
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
nil : (l.node4R x Ordnode.nil y r).dual = r.dual.node4L y (dual Ordnode.nil) x l.dual
⊢ (l.node4R x m y r).dual = r.dual.node4L y m.dual x l.dual
have node : ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α),
  (l.node4R x (node size l_1 x_1 r_1) y r).dual = r.dual.node4L y (node size l_1 x_1 r_1).dual x l.dual
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.rotateL x r).dual = r.dual.rotateR x l.dual
have nil : (l.rotateL x nil).dual = rotateR (dual nil) x l.dual
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
nil : (l.rotateL x Ordnode.nil).dual = rotateR (dual Ordnode.nil) x l.dual
⊢ (l.rotateL x r).dual = r.dual.rotateR x l.dual
have node : ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r : Ordnode α),
  (l.rotateL x (node size l_1 x_1 r)).dual = (node size l_1 x_1 r).dual.rotateR x l.dual
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
⊢ (l.rotateL x (node size l_1 x_1 r)).dual = (node size l_1 x_1 r).dual.rotateR x l.dual
have node : (if l_1.size < ratio * r.size then l.node3L x l_1 x_1 r else l.node4L x l_1 x_1 r).dual =
  if l_1.size < ratio * r.size then r.dual.node3R x_1 l_1.dual x l.dual else r.dual.node4R x_1 l_1.dual x l.dual
Tactic: simp [rotateL, rotateR]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
⊢ (if l_1.size < ratio * r.size then l.node3L x l_1 x_1 r else l.node4L x l_1 x_1 r).dual =
    if l_1.size < ratio * r.size then r.dual.node3R x_1 l_1.dual x l.dual else r.dual.node4R x_1 l_1.dual x l.dual
have pos : l_1.size < ratio * r.size → (l.node3L x l_1 x_1 r).dual = r.dual.node3R x_1 l_1.dual x l.dual
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
pos : l_1.size < ratio * r.size → (l.node3L x l_1 x_1 r).dual = r.dual.node3R x_1 l_1.dual x l.dual
⊢ (if l_1.size < ratio * r.size then l.node3L x l_1 x_1 r else l.node4L x l_1 x_1 r).dual =
    if l_1.size < ratio * r.size then r.dual.node3R x_1 l_1.dual x l.dual else r.dual.node4R x_1 l_1.dual x l.dual
have neg : ¬l_1.size < ratio * r.size → (l.node4L x l_1 x_1 r).dual = r.dual.node4R x_1 l_1.dual x l.dual
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.rotateR x r).dual = r.dual.rotateL x l.dual
have rw : (l.rotateR x r).dual = (r.dual.rotateL x l.dual).dual.dual
Tactic: rw [← dual_dual (rotateL _ _ _), dual_rotateL, dual_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rw : (l.rotateR x r).dual = (r.dual.rotateL x l.dual).dual.dual
⊢ (l.rotateR x r).dual = r.dual.rotateL x l.dual
have rw₁ : (l.rotateR x r).dual = (l.dual.dual.rotateR x r.dual.dual).dual
Tactic: rw [← dual_dual (rotateL _ _ _), dual_rotateL, dual_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rw : (l.rotateR x r).dual = (r.dual.rotateL x l.dual).dual.dual
rw₁ : (l.rotateR x r).dual = (l.dual.dual.rotateR x r.dual.dual).dual
⊢ (l.rotateR x r).dual = r.dual.rotateL x l.dual
have rw₂ : (l.rotateR x r).dual = (l.rotateR x r.dual.dual).dual
Tactic: rw [← dual_dual (rotateL _ _ _), dual_rotateL, dual_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rw : (l.rotateR x r).dual = (r.dual.rotateL x l.dual).dual.dual
rw₁ : (l.rotateR x r).dual = (l.dual.dual.rotateR x r.dual.dual).dual
rw₂ : (l.rotateR x r).dual = (l.rotateR x r.dual.dual).dual
⊢ (l.rotateR x r).dual = r.dual.rotateL x l.dual
have rw₃ : (l.rotateR x r).dual = (l.rotateR x r).dual
Tactic: rw [← dual_dual (rotateL _ _ _), dual_rotateL, dual_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.balance' x r).dual = r.dual.balance' x l.dual
have simp : (if l.size + r.size ≤ 1 then l.node' x r
    else
      if delta * l.size < r.size then l.rotateL x r
      else if delta * r.size < l.size then l.rotateR x r else l.node' x r).dual =
  if l.size + r.size ≤ 1 then r.dual.node' x l.dual
  else
    if delta * r.size < l.size then r.dual.rotateL x l.dual
    else if delta * l.size < r.size then r.dual.rotateR x l.dual else r.dual.node' x l.dual
Tactic: simp [balance', add_comm]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if delta * l.size < r.size then l.rotateL x r
        else if delta * r.size < l.size then l.rotateR x r else l.node' x r).dual =
    if l.size + r.size ≤ 1 then r.dual.node' x l.dual
    else
      if delta * r.size < l.size then r.dual.rotateL x l.dual
      else if delta * l.size < r.size then r.dual.rotateR x l.dual else r.dual.node' x l.dual
have pos : ∀ (h : l.size + r.size ≤ 1), (l.node' x r).dual = r.dual.node' x l.dual
Tactic: split_ifs with h h_1 h_2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
pos : ∀ (h : l.size + r.size ≤ 1), (l.node' x r).dual = r.dual.node' x l.dual
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if delta * l.size < r.size then l.rotateL x r
        else if delta * r.size < l.size then l.rotateR x r else l.node' x r).dual =
    if l.size + r.size ≤ 1 then r.dual.node' x l.dual
    else
      if delta * r.size < l.size then r.dual.rotateL x l.dual
      else if delta * l.size < r.size then r.dual.rotateR x l.dual else r.dual.node' x l.dual
have pos₁ : ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : delta * l.size < r.size) (h_2 : delta * r.size < l.size),
  (l.rotateL x r).dual = r.dual.rotateL x l.dual
Tactic: split_ifs with h h_1 h_2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
pos : ∀ (h : l.size + r.size ≤ 1), (l.node' x r).dual = r.dual.node' x l.dual
pos₁ :
  ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : delta * l.size < r.size) (h_2 : delta * r.size < l.size),
    (l.rotateL x r).dual = r.dual.rotateL x l.dual
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if delta * l.size < r.size then l.rotateL x r
        else if delta * r.size < l.size then l.rotateR x r else l.node' x r).dual =
    if l.size + r.size ≤ 1 then r.dual.node' x l.dual
    else
      if delta * r.size < l.size then r.dual.rotateL x l.dual
      else if delta * l.size < r.size then r.dual.rotateR x l.dual else r.dual.node' x l.dual
have neg : ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : delta * l.size < r.size) (h_2 : ¬delta * r.size < l.size),
  (l.rotateL x r).dual = r.dual.rotateR x l.dual
Tactic: split_ifs with h h_1 h_2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
pos : ∀ (h : l.size + r.size ≤ 1), (l.node' x r).dual = r.dual.node' x l.dual
pos₁ :
  ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : delta * l.size < r.size) (h_2 : delta * r.size < l.size),
    (l.rotateL x r).dual = r.dual.rotateL x l.dual
neg :
  ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : delta * l.size < r.size) (h_2 : ¬delta * r.size < l.size),
    (l.rotateL x r).dual = r.dual.rotateR x l.dual
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if delta * l.size < r.size then l.rotateL x r
        else if delta * r.size < l.size then l.rotateR x r else l.node' x r).dual =
    if l.size + r.size ≤ 1 then r.dual.node' x l.dual
    else
      if delta * r.size < l.size then r.dual.rotateL x l.dual
      else if delta * l.size < r.size then r.dual.rotateR x l.dual else r.dual.node' x l.dual
have pos₂ : ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : ¬delta * l.size < r.size),
  delta * r.size < l.size → (l.rotateR x r).dual = r.dual.rotateL x l.dual
Tactic: split_ifs with h h_1 h_2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
pos : ∀ (h : l.size + r.size ≤ 1), (l.node' x r).dual = r.dual.node' x l.dual
pos₁ :
  ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : delta * l.size < r.size) (h_2 : delta * r.size < l.size),
    (l.rotateL x r).dual = r.dual.rotateL x l.dual
neg :
  ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : delta * l.size < r.size) (h_2 : ¬delta * r.size < l.size),
    (l.rotateL x r).dual = r.dual.rotateR x l.dual
pos₂ :
  ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : ¬delta * l.size < r.size),
    delta * r.size < l.size → (l.rotateR x r).dual = r.dual.rotateL x l.dual
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if delta * l.size < r.size then l.rotateL x r
        else if delta * r.size < l.size then l.rotateR x r else l.node' x r).dual =
    if l.size + r.size ≤ 1 then r.dual.node' x l.dual
    else
      if delta * r.size < l.size then r.dual.rotateL x l.dual
      else if delta * l.size < r.size then r.dual.rotateR x l.dual else r.dual.node' x l.dual
have neg₁ : ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : ¬delta * l.size < r.size),
  ¬delta * r.size < l.size → (l.node' x r).dual = r.dual.node' x l.dual
Tactic: split_ifs with h h_1 h_2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : delta * l.size < r.size
h_2 : delta * r.size < l.size
⊢ (l.rotateL x r).dual = r.dual.rotateL x l.dual
have pos : r.dual.rotateR x l.dual = r.dual.rotateL x l.dual
Tactic: simp [dual_rotateL, dual_rotateR, add_comm]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ (if lrs < ratio * lls then node (ls + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
      else
        node (ls + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
          (node (lrr.size + 1) lrr x nil)).dual =
    if lrs < ratio * lls then
      node (ls + 1) (node (lrs + 1) nil x (node lrs lrr.dual lrx lrl.dual)) lx (node lls llr.dual llx lll.dual)
    else
      node (ls + 1) (node (lrr.dual.size + 1) nil x lrr.dual) lrx
        (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))
have pos : ∀ (h : lrs < ratio * lls),
  (node (ls + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)).dual =
    node (ls + 1) (node (lrs + 1) nil x (node lrs lrr.dual lrx lrl.dual)) lx (node lls llr.dual llx lll.dual)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
pos :
  ∀ (h : lrs < ratio * lls),
    (node (ls + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)).dual =
      node (ls + 1) (node (lrs + 1) nil x (node lrs lrr.dual lrx lrl.dual)) lx (node lls llr.dual llx lll.dual)
⊢ (if lrs < ratio * lls then node (ls + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
      else
        node (ls + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
          (node (lrr.size + 1) lrr x nil)).dual =
    if lrs < ratio * lls then
      node (ls + 1) (node (lrs + 1) nil x (node lrs lrr.dual lrx lrl.dual)) lx (node lls llr.dual llx lll.dual)
    else
      node (ls + 1) (node (lrr.dual.size + 1) nil x lrr.dual) lrx
        (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))
have neg : ∀ (h : ¬lrs < ratio * lls),
  (node (ls + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx (node (lrr.size + 1) lrr x nil)).dual =
    node (ls + 1) (node (lrr.dual.size + 1) nil x lrr.dual) lrx
      (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (if ls > delta * rs then
        rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
          (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
            rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
              (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
                if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (rs + size_1 + 1) lr x (node rs rl rx rr))
                else
                  node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                    (node (r.size + rs + 1) r x (node rs rl rx rr)))
              lr)
          ll
      else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)))
    (if ls > delta * rs then
      rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
        (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
          rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
            (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
              if size_1 < ratio * size then
                node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx ll.dual
              else
                node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                  (node (r.size + size + 1) r lx ll.dual))
            lr.dual)
        ll.dual
    else node (rs + ls + 1) (node rs rr.dual rx rl.dual) x (node ls lr.dual lx ll.dual))
have pos : ls > delta * rs →
  Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
        (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
          rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
            (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
              if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (rs + size_1 + 1) lr x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        ll))
    (rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
      (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
        rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
          (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
            if size_1 < ratio * size then
              node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx ll.dual
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx ll.dual))
          lr.dual)
      ll.dual)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h : ls > delta * rs
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
        (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
          rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
            (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
              if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (rs + size_1 + 1) lr x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        ll))
    (rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
      (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
        rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
          (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
            if size_1 < ratio * size then
              node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx ll.dual
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx ll.dual))
          lr.dual)
      ll.dual)
have pos : Eq.{u_1 + 1} (α := Ordnode α)
  (dual
    (rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
      (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
        rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
          (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
            if size_1 < ratio * size then node (ls + rs + 1) nil lx (node (rs + size_1 + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) nil lx l) x_2
                (node (r.size + rs + 1) r x (node rs rl rx rr)))
          lr)
      nil))
  (rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
    (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
      rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
        (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
          if size_1 < ratio * size then
            node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx (dual nil)
          else
            node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
              (node (r.size + size + 1) r lx (dual nil)))
        lr.dual)
    (dual nil))
Tactic: obtain - | ⟨lls, lll, llx, llr⟩ := ll
Cleared hypotheses: ll
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
lr : Ordnode α
h : ls > delta * rs
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
        (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
          rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
            (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
              if size_1 < ratio * size then node (ls + rs + 1) nil lx (node (rs + size_1 + 1) lr x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) nil lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        nil))
    (rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
      (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
        rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
          (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
            if size_1 < ratio * size then
              node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx (dual nil)
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx (dual nil)))
          lr.dual)
      (dual nil))
have pos : Eq.{u_1 + 1} (α := Ordnode α)
  (dual
    (rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
      (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
        rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
          (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
            if size_1 < ratio * size then node (ls + rs + 1) nil lx (node (rs + size_1 + 1) nil x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) nil lx l) x_2
                (node (r.size + rs + 1) r x (node rs rl rx rr)))
          nil)
      nil))
  (rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
    (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
      rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
        (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
          if size_1 < ratio * size then
            node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x (dual nil)) lx (dual nil)
          else
            node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
              (node (r.size + size + 1) r lx (dual nil)))
        (dual nil))
    (dual nil))
Tactic: obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr
Cleared hypotheses: lr