awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx rr).Balanced
sr : (node rs (node rls rll rlx rlr) rx rr).Sized
nil :
  ∀ (hr : ((node rls rll rlx rlr).node' rx Ordnode.nil).Balanced)
    (sr : (node rs (node rls rll rlx rlr) rx Ordnode.nil).Sized),
    balance Ordnode.nil x ((node rls rll rlx rlr).node' rx Ordnode.nil) =
      balance' Ordnode.nil x ((node rls rll rlx rlr).node' rx Ordnode.nil)
⊢ balance Ordnode.nil x ((node rls rll rlx rlr).node' rx rr) =
    balance' Ordnode.nil x ((node rls rll rlx rlr).node' rx rr)
have nil₁ : ∀ (rrs : ℕ) (rrl : Ordnode α) (rrx : α) (rrr : Ordnode α)
  (hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced)
  (sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized),
  balance Ordnode.nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)) =
    balance' Ordnode.nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
Tactic: obtain - | ⟨rrs, rrl, rrx, rrr⟩ := rr
Cleared hypotheses: rr, hr, sr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node' nil rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
⊢ balance nil x (node' nil rx (node rrs rrl rrx rrr)) = balance' nil x (node' nil rx (node rrs rrl rrx rrr))
have nil : node 3 (Ordnode.singleton x) rx (node rrs rrl rrx rrr) =
  if 0 + (0 + rrs + 1) ≤ 1 then node' nil x (node' nil rx (node rrs rrl rrx rrr))
  else rotateL nil x (node' nil rx (node rrs rrl rrx rrr))
Tactic: dsimp +instances [balance, balance']
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
⊢ balance nil x ((node rls rll rlx rlr).node' rx nil) = balance' nil x ((node rls rll rlx rlr).node' rx nil)
have nil : node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
  if 0 + (rls + 1) ≤ 1 then node' nil x ((node rls rll rlx rlr).node' rx nil)
  else rotateL nil x ((node rls rll rlx rlr).node' rx nil)
Tactic: dsimp +instances [balance, balance']
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
⊢ balance nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)) =
    balance' nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
have nil : (if rls < ratio * rrs then
    node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
  else
    node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
      (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))) =
  if 0 + (rls + rrs + 1) ≤ 1 then node' nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
  else rotateL nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
Tactic: dsimp +instances [balance, balance']
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node' nil rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
⊢ rrl.size = 0 ∧ rrr.size = 0
have this : (node rrs rrl rrx rrr).size ≤ 1
Tactic: have := balancedSz_zero.1 hr.1.symm
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node' nil rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
this : (node rrs rrl rrx rrr).size ≤ 1
⊢ rrl.size = 0 ∧ rrr.size = 0
have rwa : ∀ (this : rrs ≤ 1), rrl.size = 0 ∧ rrr.size = 0
Tactic: rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node' nil rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
this : (node rrs rrl rrx rrr).size ≤ 1
rwa : ∀ (this : rrs ≤ 1), rrl.size = 0 ∧ rrr.size = 0
⊢ rrl.size = 0 ∧ rrr.size = 0
have rwa₁ : ∀ (this : rrl.size + rrr.size + 1 ≤ 1), rrl.size = 0 ∧ rrr.size = 0
Tactic: rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node' nil rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
this : (node rrs rrl rrx rrr).size ≤ 1
rwa : ∀ (this : rrs ≤ 1), rrl.size = 0 ∧ rrr.size = 0
rwa₁ : ∀ (this : rrl.size + rrr.size + 1 ≤ 1), rrl.size = 0 ∧ rrr.size = 0
⊢ rrl.size = 0 ∧ rrr.size = 0
have rwa₂ : ∀ (this : rrl.size + rrr.size ≤ 0), rrl.size = 0 ∧ rrr.size = 0
Tactic: rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node' nil rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
this : (node rrs rrl rrx rrr).size ≤ 1
rwa : ∀ (this : rrs ≤ 1), rrl.size = 0 ∧ rrr.size = 0
rwa₁ : ∀ (this : rrl.size + rrr.size + 1 ≤ 1), rrl.size = 0 ∧ rrr.size = 0
rwa₂ : ∀ (this : rrl.size + rrr.size ≤ 0), rrl.size = 0 ∧ rrr.size = 0
⊢ rrl.size = 0 ∧ rrr.size = 0
have rwa₃ : ∀ (this : rrl.size + rrr.size = 0), rrl.size = 0 ∧ rrr.size = 0
Tactic: rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node' nil rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
this : (node rrs rrl rrx rrr).size ≤ 1
rwa : ∀ (this : rrs ≤ 1), rrl.size = 0 ∧ rrr.size = 0
rwa₁ : ∀ (this : rrl.size + rrr.size + 1 ≤ 1), rrl.size = 0 ∧ rrr.size = 0
rwa₂ : ∀ (this : rrl.size + rrr.size ≤ 0), rrl.size = 0 ∧ rrr.size = 0
rwa₃ : ∀ (this : rrl.size + rrr.size = 0), rrl.size = 0 ∧ rrr.size = 0
⊢ rrl.size = 0 ∧ rrr.size = 0
have rwa₄ : ∀ (this : rrl.size = 0 ∧ rrr.size = 0), rrl.size = 0 ∧ rrr.size = 0
Tactic: rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node' nil rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
⊢ node 3 (Ordnode.singleton x) rx (node rrs rrl rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' nil x (node' nil rx (node rrs rrl rrx rrr))
    else rotateL nil x (node' nil rx (node rrs rrl rrx rrr))
have this : rrl.size = 0 ∧ rrr.size = 0
Tactic: have : size rrl = 0 ∧ size rrr = 0 := by
          have := balancedSz_zero.1 hr.1.symm
          rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node' nil rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
this : rrl.size = 0 ∧ rrr.size = 0
⊢ node 3 (Ordnode.singleton x) rx (node rrs rrl rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' nil x (node' nil rx (node rrs rrl rrx rrr))
    else rotateL nil x (node' nil rx (node rrs rrl rrx rrr))
have nil : ∀ (hr : (node' nil rx (node rrs nil rrx rrr)).Balanced) (sr : (node rs nil rx (node rrs nil rrx rrr)).Sized)
  (this : size.{u_1} (α := α) nil = 0 ∧ rrr.size = 0),
  node 3 (Ordnode.singleton x) rx (node rrs nil rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' nil x (node' nil rx (node rrs nil rrx rrr))
    else rotateL nil x (node' nil rx (node rrs nil rrx rrr))
Tactic: cases sr.2.2.2.1.size_eq_zero.1 this.1
Cleared hypotheses: rrl, hr, sr, this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rrs : ℕ
rrx : α
rrr : Ordnode α
hr : (node' nil rx (node rrs nil rrx rrr)).Balanced
sr : (node rs nil rx (node rrs nil rrx rrr)).Sized
this : size.{u_1} (α := α) nil = 0 ∧ rrr.size = 0
⊢ node 3 (Ordnode.singleton x) rx (node rrs nil rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' nil x (node' nil rx (node rrs nil rrx rrr))
    else rotateL nil x (node' nil rx (node rrs nil rrx rrr))
have nil : ∀ (hr : (node' nil rx (node rrs nil rrx nil)).Balanced) (sr : (node rs nil rx (node rrs nil rrx nil)).Sized)
  (this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0),
  node 3 (Ordnode.singleton x) rx (node rrs nil rrx nil) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' nil x (node' nil rx (node rrs nil rrx nil))
    else rotateL nil x (node' nil rx (node rrs nil rrx nil))
Tactic: cases sr.2.2.2.2.size_eq_zero.1 this.2
Cleared hypotheses: rrr, hr, sr, this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rrs : ℕ
rrx : α
hr : (node' nil rx (node rrs nil rrx nil)).Balanced
sr : (node rs nil rx (node rrs nil rrx nil)).Sized
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
⊢ node 3 (Ordnode.singleton x) rx (node rrs nil rrx nil) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' nil x (node' nil rx (node rrs nil rrx nil))
    else rotateL nil x (node' nil rx (node rrs nil rrx nil))
have nil : ∀ (hr : (node' nil rx (node 1 nil rrx nil)).Balanced) (sr : (node rs nil rx (node 1 nil rrx nil)).Sized),
  node 3 (Ordnode.singleton x) rx (node 1 nil rrx nil) =
    if 0 + (HAdd.hAdd (α := ℕ) 0 1 + 1) ≤ 1 then node' nil x (node' nil rx (node 1 nil rrx nil))
    else rotateL nil x (node' nil rx (node 1 nil rrx nil))
Tactic: obtain rfl : rrs = 1 := sr.2.2.1
Cleared hypotheses: rrs, hr, sr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx rrx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hr : (node' nil rx (node 1 nil rrx nil)).Balanced
sr : (node rs nil rx (node 1 nil rrx nil)).Sized
⊢ node 3 (Ordnode.singleton x) rx (node 1 nil rrx nil) =
    if 0 + (HAdd.hAdd (α := ℕ) 0 1 + 1) ≤ 1 then node' nil x (node' nil rx (node 1 nil rrx nil))
    else rotateL nil x (node' nil rx (node 1 nil rrx nil))
have nil : node 3 (Ordnode.singleton x) rx (node 1 nil rrx nil) = node3L nil x nil rx (node 1 nil rrx nil)
Tactic: rw [if_neg, rotateL_node, if_pos]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx rrx : α
this : size.{u_1} (α := α) Ordnode.nil = 0 ∧ size.{u_1} (α := α) Ordnode.nil = 0
hr : (node' Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil)).Balanced
sr : (node rs Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil)).Sized
nil :
  node 3 (Ordnode.singleton x) rx (node 1 Ordnode.nil rrx Ordnode.nil) =
    node3L Ordnode.nil x Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil)
⊢ node 3 (Ordnode.singleton x) rx (node 1 Ordnode.nil rrx Ordnode.nil) =
    if 0 + (HAdd.hAdd (α := ℕ) 0 1 + 1) ≤ 1 then
      node' Ordnode.nil x (node' Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil))
    else rotateL Ordnode.nil x (node' Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil))
have nil₁ : size.{u_1} (α := α) Ordnode.nil < ratio * (node 1 Ordnode.nil rrx Ordnode.nil).size
Tactic: rw [if_neg, rotateL_node, if_pos]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx rrx : α
this : size.{u_1} (α := α) Ordnode.nil = 0 ∧ size.{u_1} (α := α) Ordnode.nil = 0
hr : (node' Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil)).Balanced
sr : (node rs Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil)).Sized
nil :
  node 3 (Ordnode.singleton x) rx (node 1 Ordnode.nil rrx Ordnode.nil) =
    node3L Ordnode.nil x Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil)
nil₁ : size.{u_1} (α := α) Ordnode.nil < ratio * (node 1 Ordnode.nil rrx Ordnode.nil).size
⊢ node 3 (Ordnode.singleton x) rx (node 1 Ordnode.nil rrx Ordnode.nil) =
    if 0 + (HAdd.hAdd (α := ℕ) 0 1 + 1) ≤ 1 then
      node' Ordnode.nil x (node' Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil))
    else rotateL Ordnode.nil x (node' Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil))
have nil₂ : ¬0 + (HAdd.hAdd (α := ℕ) 0 1 + 1) ≤ 1
Tactic: rw [if_neg, rotateL_node, if_pos]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
⊢ rll.size = 0 ∧ rlr.size = 0
have this : (node rls rll rlx rlr).size ≤ 1
Tactic: have := balancedSz_zero.1 hr.1
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
this : (node rls rll rlx rlr).size ≤ 1
⊢ rll.size = 0 ∧ rlr.size = 0
have rwa : ∀ (this : rls ≤ 1), rll.size = 0 ∧ rlr.size = 0
Tactic: rwa [size, sr.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
this : (node rls rll rlx rlr).size ≤ 1
rwa : ∀ (this : rls ≤ 1), rll.size = 0 ∧ rlr.size = 0
⊢ rll.size = 0 ∧ rlr.size = 0
have rwa₁ : ∀ (this : rll.size + rlr.size + 1 ≤ 1), rll.size = 0 ∧ rlr.size = 0
Tactic: rwa [size, sr.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
this : (node rls rll rlx rlr).size ≤ 1
rwa : ∀ (this : rls ≤ 1), rll.size = 0 ∧ rlr.size = 0
rwa₁ : ∀ (this : rll.size + rlr.size + 1 ≤ 1), rll.size = 0 ∧ rlr.size = 0
⊢ rll.size = 0 ∧ rlr.size = 0
have rwa₂ : ∀ (this : rll.size + rlr.size ≤ 0), rll.size = 0 ∧ rlr.size = 0
Tactic: rwa [size, sr.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
this : (node rls rll rlx rlr).size ≤ 1
rwa : ∀ (this : rls ≤ 1), rll.size = 0 ∧ rlr.size = 0
rwa₁ : ∀ (this : rll.size + rlr.size + 1 ≤ 1), rll.size = 0 ∧ rlr.size = 0
rwa₂ : ∀ (this : rll.size + rlr.size ≤ 0), rll.size = 0 ∧ rlr.size = 0
⊢ rll.size = 0 ∧ rlr.size = 0
have rwa₃ : ∀ (this : rll.size + rlr.size = 0), rll.size = 0 ∧ rlr.size = 0
Tactic: rwa [size, sr.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
this : (node rls rll rlx rlr).size ≤ 1
rwa : ∀ (this : rls ≤ 1), rll.size = 0 ∧ rlr.size = 0
rwa₁ : ∀ (this : rll.size + rlr.size + 1 ≤ 1), rll.size = 0 ∧ rlr.size = 0
rwa₂ : ∀ (this : rll.size + rlr.size ≤ 0), rll.size = 0 ∧ rlr.size = 0
rwa₃ : ∀ (this : rll.size + rlr.size = 0), rll.size = 0 ∧ rlr.size = 0
⊢ rll.size = 0 ∧ rlr.size = 0
have rwa₄ : ∀ (this : rll.size = 0 ∧ rlr.size = 0), rll.size = 0 ∧ rlr.size = 0
Tactic: rwa [size, sr.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' nil x ((node rls rll rlx rlr).node' rx nil)
    else rotateL nil x ((node rls rll rlx rlr).node' rx nil)
have this : rll.size = 0 ∧ rlr.size = 0
Tactic: have : size rll = 0 ∧ size rlr = 0 := by
          have := balancedSz_zero.1 hr.1
          rwa [size, sr.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
this : rll.size = 0 ∧ rlr.size = 0
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' nil x ((node rls rll rlx rlr).node' rx nil)
    else rotateL nil x ((node rls rll rlx rlr).node' rx nil)
have nil : ∀ (hr : ((node rls nil rlx rlr).node' rx nil).Balanced) (sr : (node rs (node rls nil rlx rlr) rx nil).Sized)
  (this : size.{u_1} (α := α) nil = 0 ∧ rlr.size = 0),
  node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' nil x ((node rls nil rlx rlr).node' rx nil)
    else rotateL nil x ((node rls nil rlx rlr).node' rx nil)
Tactic: cases sr.2.1.2.1.size_eq_zero.1 this.1
Cleared hypotheses: rll, hr, sr, this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rlx : α
rlr : Ordnode α
hr : ((node rls nil rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls nil rlx rlr) rx nil).Sized
this : size.{u_1} (α := α) nil = 0 ∧ rlr.size = 0
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' nil x ((node rls nil rlx rlr).node' rx nil)
    else rotateL nil x ((node rls nil rlx rlr).node' rx nil)
have nil : ∀ (hr : ((node rls nil rlx nil).node' rx nil).Balanced) (sr : (node rs (node rls nil rlx nil) rx nil).Sized)
  (this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0),
  node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' nil x ((node rls nil rlx nil).node' rx nil)
    else rotateL nil x ((node rls nil rlx nil).node' rx nil)
Tactic: cases sr.2.1.2.2.size_eq_zero.1 this.2
Cleared hypotheses: rlr, hr, sr, this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rlx : α
hr : ((node rls nil rlx nil).node' rx nil).Balanced
sr : (node rs (node rls nil rlx nil) rx nil).Sized
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' nil x ((node rls nil rlx nil).node' rx nil)
    else rotateL nil x ((node rls nil rlx nil).node' rx nil)
have nil : ∀ (hr : ((node 1 nil rlx nil).node' rx nil).Balanced) (sr : (node rs (node 1 nil rlx nil) rx nil).Sized),
  node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + HAdd.hAdd (α := ℕ) 1 1 ≤ 1 then node' nil x ((node 1 nil rlx nil).node' rx nil)
    else rotateL nil x ((node 1 nil rlx nil).node' rx nil)
Tactic: obtain rfl : rls = 1 := sr.2.1.1
Cleared hypotheses: rls, hr, sr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx rlx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hr : ((node 1 nil rlx nil).node' rx nil).Balanced
sr : (node rs (node 1 nil rlx nil) rx nil).Sized
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + HAdd.hAdd (α := ℕ) 1 1 ≤ 1 then node' nil x ((node 1 nil rlx nil).node' rx nil)
    else rotateL nil x ((node 1 nil rlx nil).node' rx nil)
have nil : node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) = node4L nil x (node 1 nil rlx nil) rx nil
Tactic: rw [if_neg, rotateL_node, if_neg]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx rlx : α
this : size.{u_1} (α := α) Ordnode.nil = 0 ∧ size.{u_1} (α := α) Ordnode.nil = 0
hr : ((node 1 Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil).Balanced
sr : (node rs (node 1 Ordnode.nil rlx Ordnode.nil) rx Ordnode.nil).Sized
nil :
  node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    node4L Ordnode.nil x (node 1 Ordnode.nil rlx Ordnode.nil) rx Ordnode.nil
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + HAdd.hAdd (α := ℕ) 1 1 ≤ 1 then
      node' Ordnode.nil x ((node 1 Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil)
    else rotateL Ordnode.nil x ((node 1 Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil)
have nil₁ : ¬(node 1 Ordnode.nil rlx Ordnode.nil).size < ratio * size.{u_1} (α := α) Ordnode.nil
Tactic: rw [if_neg, rotateL_node, if_neg]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx rlx : α
this : size.{u_1} (α := α) Ordnode.nil = 0 ∧ size.{u_1} (α := α) Ordnode.nil = 0
hr : ((node 1 Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil).Balanced
sr : (node rs (node 1 Ordnode.nil rlx Ordnode.nil) rx Ordnode.nil).Sized
nil :
  node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    node4L Ordnode.nil x (node 1 Ordnode.nil rlx Ordnode.nil) rx Ordnode.nil
nil₁ : ¬(node 1 Ordnode.nil rlx Ordnode.nil).size < ratio * size.{u_1} (α := α) Ordnode.nil
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + HAdd.hAdd (α := ℕ) 1 1 ≤ 1 then
      node' Ordnode.nil x ((node 1 Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil)
    else rotateL Ordnode.nil x ((node 1 Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil)
have nil₂ : ¬0 + HAdd.hAdd (α := ℕ) 1 1 ≤ 1
Tactic: rw [if_neg, rotateL_node, if_neg]