awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
sl : Sized.{u_1} (α := α) nil
H1 : size.{u_1} (α := α) nil = 0 → (node rs rl rx rr).size ≤ 1
H2 :
  1 ≤ size.{u_1} (α := α) nil → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * size.{u_1} (α := α) nil
this : rl.size = 0 ∧ rr.size = 0
⊢ balanceL nil x (node rs rl rx rr) = balance nil x (node rs rl rx rr)
have node : ∀ (sr : (node rs nil rx rr).Sized) (H1 : size.{u_1} (α := α) nil = 0 → (node rs nil rx rr).size ≤ 1)
  (H2 :
    1 ≤ size.{u_1} (α := α) nil →
      1 ≤ (node rs nil rx rr).size → (node rs nil rx rr).size ≤ delta * size.{u_1} (α := α) nil)
  (this : size.{u_1} (α := α) nil = 0 ∧ rr.size = 0),
  balanceL nil x (node rs nil rx rr) = balance nil x (node rs nil rx rr)
Tactic: cases sr.2.1.size_eq_zero.1 this.1
Cleared hypotheses: rl, sr, H1, H2, this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
rs : ℕ
rx : α
rr : Ordnode α
sl : Sized.{u_1} (α := α) nil
sr : (node rs nil rx rr).Sized
H1 : size.{u_1} (α := α) nil = 0 → (node rs nil rx rr).size ≤ 1
H2 :
  1 ≤ size.{u_1} (α := α) nil →
    1 ≤ (node rs nil rx rr).size → (node rs nil rx rr).size ≤ delta * size.{u_1} (α := α) nil
this : size.{u_1} (α := α) nil = 0 ∧ rr.size = 0
⊢ balanceL nil x (node rs nil rx rr) = balance nil x (node rs nil rx rr)
have node : ∀ (sr : (node rs nil rx nil).Sized) (H1 : size.{u_1} (α := α) nil = 0 → (node rs nil rx nil).size ≤ 1)
  (H2 :
    1 ≤ size.{u_1} (α := α) nil →
      1 ≤ (node rs nil rx nil).size → (node rs nil rx nil).size ≤ delta * size.{u_1} (α := α) nil)
  (this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0),
  balanceL nil x (node rs nil rx nil) = balance nil x (node rs nil rx nil)
Tactic: cases sr.2.2.size_eq_zero.1 this.2
Cleared hypotheses: rr, sr, H1, H2, this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
rs : ℕ
rx : α
sl : Sized.{u_1} (α := α) nil
sr : (node rs nil rx nil).Sized
H1 : size.{u_1} (α := α) nil = 0 → (node rs nil rx nil).size ≤ 1
H2 :
  1 ≤ size.{u_1} (α := α) nil →
    1 ≤ (node rs nil rx nil).size → (node rs nil rx nil).size ≤ delta * size.{u_1} (α := α) nil
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
⊢ balanceL nil x (node rs nil rx nil) = balance nil x (node rs nil rx nil)
have node : balanceL nil x (node' nil rx nil) = balance nil x (node' nil rx nil)
Tactic: rw [sr.eq_node']
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 :
  1 ≤ (node ls ll lx lr).size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * (node ls ll lx lr).size
⊢ (node ls ll lx lr).balanceL x (node rs rl rx rr) = (node ls ll lx lr).balance x (node rs rl rx rr)
have H2₁ : ¬rs > delta * ls
Tactic: replace H2 : ¬rs > delta * ls := not_lt_of_ge (H2 sl.pos sr.pos)
Cleared hypotheses: H2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 : ¬rs > delta * ls
⊢ (node ls ll lx lr).balanceL x (node rs rl rx rr) = (node ls ll lx lr).balance x (node rs rl rx rr)
have node : Eq (α := Ordnode α)
  (if delta * rs < ls 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) :
    Ordnode α)
  (if delta * rs < ls 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 (size_1 + rs + 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) :
    Ordnode α)
Tactic: simp [balanceL, balance, H2]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 : ¬rs > delta * ls
⊢ Eq (α := Ordnode α)
    (if delta * rs < ls 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) :
      Ordnode α)
    (if delta * rs < ls 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 (size_1 + rs + 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) :
      Ordnode α)
have pos : delta * rs < ls →
  Eq (α := Ordnode α)
    (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 :
      Ordnode α)
    (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 (size_1 + rs + 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 :
      Ordnode α)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
n m : ℕ
⊢ Raised n m ↔ n ≤ m ∧ m ≤ n + 1
have mp : Raised n m → n ≤ m ∧ m ≤ n + 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
n m : ℕ
mp : Raised n m → n ≤ m ∧ m ≤ n + 1
⊢ Raised n m ↔ n ≤ m ∧ m ≤ n + 1
have mpr : n ≤ m ∧ m ≤ n + 1 → Raised n m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
n m : ℕ
h₁ : n ≤ m
h₂ : m ≤ n + 1
⊢ Raised n m
have mpr : ∀ (h₁ : n ≤ n) (h₂ : n ≤ n + 1), Raised n n
Tactic: rcases eq_or_lt_of_le h₁ with (rfl | h₁)
Cleared hypotheses: m, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
n m : ℕ
h₁ : n ≤ m
h₂ : m ≤ n + 1
mpr : ∀ (h₁ : n ≤ n) (h₂ : n ≤ n + 1), Raised n n
⊢ Raised n m
have mpr₁ : ∀ (h₁ : n < m), Raised n m
Tactic: rcases eq_or_lt_of_le h₁ with (rfl | h₁)
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
Goal:
n m : ℕ
H : Raised n m
⊢ n.dist m ≤ 1
have H1 : n ≤ m
Tactic: obtain ⟨H1, H2⟩ := raised_iff.1 H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
Goal:
n m : ℕ
H : Raised n m
H1 : n ≤ m
⊢ n.dist m ≤ 1
have H2 : m ≤ n + 1
Tactic: obtain ⟨H1, H2⟩ := raised_iff.1 H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
⊢ n.dist m ≤ 1
have rwa : m - n ≤ 1
Tactic: rwa [Nat.dist_eq_sub_of_le H1, tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
n m : ℕ
H : Raised n m
⊢ m.dist n ≤ 1
have rw : n.dist m ≤ 1
Tactic: rw [Nat.dist_comm]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
k n m : ℕ
H : Raised n m
⊢ Raised (k + n) (k + m)
have inl : Raised (k + m) (k + m)
Tactic: rcases H with (rfl | rfl)
Cleared hypotheses: n, H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
k n m : ℕ
H : Raised n m
inl : Raised (k + m) (k + m)
⊢ Raised (k + n) (k + m)
have inr : Raised (k + n) (k + (n + 1))
Tactic: rcases H with (rfl | rfl)
Cleared hypotheses: m, H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
k n m : ℕ
H : Raised n m
⊢ Raised (n + k) (m + k)
have rw : Raised (k + n) (k + m)
Tactic: rw [add_comm, add_comm m]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
H : Raised r₁.size r₂.size
⊢ Raised (l.size + r₁.size + 1) (l.size + r₂.size + 1)
have generalize : ∀ (m : ℕ) (H : Raised r₁.size m), Raised (l.size + r₁.size + 1) (l.size + m + 1)
Tactic: generalize size r₂ = m at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
m : ℕ
H : Raised r₁.size m
⊢ Raised (l.size + r₁.size + 1) (l.size + m + 1)
have inl : Raised (l.size + r₁.size + 1) (l.size + r₁.size + 1)
Tactic: rcases H with (rfl | rfl)
Cleared hypotheses: m, H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
m : ℕ
H : Raised r₁.size m
inl : Raised (l.size + r₁.size + 1) (l.size + r₁.size + 1)
⊢ Raised (l.size + r₁.size + 1) (l.size + m + 1)
have inr : Raised (l.size + r₁.size + 1) (l.size + (r₁.size + 1) + 1)
Tactic: rcases H with (rfl | rfl)
Cleared hypotheses: m, H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
⊢ l.balanceL x r = l.balance' x r
have H1 : l.size = 0 → r.size ≤ 1
Tactic: rw [← balance_eq_balance' hl hr sl sr, balanceL_eq_balance sl sr]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
H1 : l.size = 0 → r.size ≤ 1
⊢ l.balanceL x r = l.balance' x r
have H2 : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
Tactic: rw [← balance_eq_balance' hl hr sl sr, balanceL_eq_balance sl sr]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
l0 : l.size = 0
⊢ r.size ≤ 1
have H₁ : (∃ (l' : ℕ), Raised l' 0 ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz 0 r'
Tactic: rw [l0] at H
Cleared hypotheses: H, l0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l' 0 ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz 0 r'
l0 : l.size = 0
⊢ r.size ≤ 1
have H1 : ∀ (H : BalancedSz 0 r.size), r.size ≤ 1
Tactic: rcases H with (⟨_, ⟨⟨⟩⟩ | ⟨⟨⟩⟩, H⟩ | ⟨r', e, H⟩)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l' 0 ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz 0 r'
l0 : l.size = 0
H1 : ∀ (H : BalancedSz 0 r.size), r.size ≤ 1
⊢ r.size ≤ 1
have H1₁ : ∀ (r' : ℕ) (e : Raised r.size r') (H : BalancedSz 0 r'), r.size ≤ 1
Tactic: rcases H with (⟨_, ⟨⟨⟩⟩ | ⟨⟨⟩⟩, H⟩ | ⟨r', e, H⟩)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
l1 : 1 ≤ l.size
h : 1 ≤ r.size
⊢ r.size ≤ delta * l.size
have H2 : ∀ (l' : ℕ) (e : Raised l' l.size) (H : l' + r.size ≤ 1), r.size ≤ delta * l.size
Tactic: rcases H with (⟨l', e, H | ⟨_, H₂⟩⟩ | ⟨r', e, H | ⟨_, H₂⟩⟩)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
l1 : 1 ≤ l.size
h : 1 ≤ r.size
H2 : ∀ (l' : ℕ) (e : Raised l' l.size) (H : l' + r.size ≤ 1), r.size ≤ delta * l.size
⊢ r.size ≤ delta * l.size
have H2₁ : ∀ (l' : ℕ) (e : Raised l' l.size), l' ≤ delta * r.size → ∀ (H₂ : r.size ≤ delta * l'), r.size ≤ delta * l.size
Tactic: rcases H with (⟨l', e, H | ⟨_, H₂⟩⟩ | ⟨r', e, H | ⟨_, H₂⟩⟩)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
l1 : 1 ≤ l.size
h : 1 ≤ r.size
H2 : ∀ (l' : ℕ) (e : Raised l' l.size) (H : l' + r.size ≤ 1), r.size ≤ delta * l.size
H2₁ : ∀ (l' : ℕ) (e : Raised l' l.size), l' ≤ delta * r.size → ∀ (H₂ : r.size ≤ delta * l'), r.size ≤ delta * l.size
⊢ r.size ≤ delta * l.size
have H2₂ : ∀ (r' : ℕ) (e : Raised r.size r') (H : l.size + r' ≤ 1), r.size ≤ delta * l.size
Tactic: rcases H with (⟨l', e, H | ⟨_, H₂⟩⟩ | ⟨r', e, H | ⟨_, H₂⟩⟩)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
l1 : 1 ≤ l.size
h : 1 ≤ r.size
H2 : ∀ (l' : ℕ) (e : Raised l' l.size) (H : l' + r.size ≤ 1), r.size ≤ delta * l.size
H2₁ : ∀ (l' : ℕ) (e : Raised l' l.size), l' ≤ delta * r.size → ∀ (H₂ : r.size ≤ delta * l'), r.size ≤ delta * l.size
H2₂ : ∀ (r' : ℕ) (e : Raised r.size r') (H : l.size + r' ≤ 1), r.size ≤ delta * l.size
⊢ r.size ≤ delta * l.size
have H2₃ : ∀ (r' : ℕ) (e : Raised r.size r'), l.size ≤ delta * r' → ∀ (H₂ : r' ≤ delta * l.size), r.size ≤ delta * l.size
Tactic: rcases H with (⟨l', e, H | ⟨_, H₂⟩⟩ | ⟨r', e, H | ⟨_, H₂⟩⟩)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
h : 1 ≤ r.size
r' : ℕ
e : Raised r.size r'
H : l.size + r' ≤ 1
⊢ r.size ≤ delta * l.size
have left : r.size ≤ r'
Tactic: cases raised_iff.1 e
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
h : 1 ≤ r.size
r' : ℕ
e : Raised r.size r'
H : l.size + r' ≤ 1
left : r.size ≤ r'
⊢ r.size ≤ delta * l.size
have right : r' ≤ r.size + 1
Tactic: cases raised_iff.1 e
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l r : Ordnode α
H : (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r' r.size ∧ BalancedSz l.size r'
⊢ (∃ (l' : ℕ), Raised l' r.dual.size ∧ BalancedSz l' l.dual.size) ∨
    ∃ (r' : ℕ), Raised l.dual.size r' ∧ BalancedSz r.dual.size r'
have rw : (∃ (l' : ℕ), Raised l' r.size ∧ BalancedSz l' l.size) ∨ ∃ (r' : ℕ), Raised l.size r' ∧ BalancedSz r.size r'
Tactic: rw [size_dual, size_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
⊢ (l.balanceL x r).size = l.size + r.size + 1
have rw : (l.balance' x r).size = l.size + r.size + 1
Tactic: rw [balanceL_eq_balance' hl hr sl sr H, size_balance' sl sr]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
rw : (l.balance' x r).size = l.size + r.size + 1
⊢ (l.balanceL x r).size = l.size + r.size + 1
have rw₁ : l.size + r.size + 1 = l.size + r.size + 1
Tactic: rw [balanceL_eq_balance' hl hr sl sr H, size_balance' sl sr]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
⊢ All P (l.balanceL x r) ↔ All P l ∧ P x ∧ All P r
have rw : All P (l.balance' x r) ↔ All P l ∧ P x ∧ All P r
Tactic: rw [balanceL_eq_balance' hl hr sl sr H, all_balance']
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
rw : All P (l.balance' x r) ↔ All P l ∧ P x ∧ All P r
⊢ All P (l.balanceL x r) ↔ All P l ∧ P x ∧ All P r
have rw₁ : All P l ∧ P x ∧ All P r ↔ All P l ∧ P x ∧ All P r
Tactic: rw [balanceL_eq_balance' hl hr sl sr H, all_balance']
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r' r.size ∧ BalancedSz l.size r'
⊢ l.balanceR x r = l.balance' x r
have rw : (l.balanceR x r).dual.dual = l.balance' x r
Tactic: rw [← dual_dual (balanceR l x r), dual_balanceR,
    balanceL_eq_balance' hr.dual hl.dual sr.dual sl.dual (balance_sz_dual H), ← dual_balance',
    dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r' r.size ∧ BalancedSz l.size r'
rw : (l.balanceR x r).dual.dual = l.balance' x r
⊢ l.balanceR x r = l.balance' x r
have rw₁ : (r.dual.balanceL x l.dual).dual = l.balance' x r
Tactic: rw [← dual_dual (balanceR l x r), dual_balanceR,
    balanceL_eq_balance' hr.dual hl.dual sr.dual sl.dual (balance_sz_dual H), ← dual_balance',
    dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r' r.size ∧ BalancedSz l.size r'
rw : (l.balanceR x r).dual.dual = l.balance' x r
rw₁ : (r.dual.balanceL x l.dual).dual = l.balance' x r
⊢ l.balanceR x r = l.balance' x r
have rw₂ : (r.dual.balance' x l.dual).dual = l.balance' x r
Tactic: rw [← dual_dual (balanceR l x r), dual_balanceR,
    balanceL_eq_balance' hr.dual hl.dual sr.dual sl.dual (balance_sz_dual H), ← dual_balance',
    dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r' r.size ∧ BalancedSz l.size r'
rw : (l.balanceR x r).dual.dual = l.balance' x r
rw₁ : (r.dual.balanceL x l.dual).dual = l.balance' x r
rw₂ : (r.dual.balance' x l.dual).dual = l.balance' x r
⊢ l.balanceR x r = l.balance' x r
have rw₃ : (l.balance' x r).dual.dual = l.balance' x r
Tactic: rw [← dual_dual (balanceR l x r), dual_balanceR,
    balanceL_eq_balance' hr.dual hl.dual sr.dual sl.dual (balance_sz_dual H), ← dual_balance',
    dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r' r.size ∧ BalancedSz l.size r'
rw : (l.balanceR x r).dual.dual = l.balance' x r
rw₁ : (r.dual.balanceL x l.dual).dual = l.balance' x r
rw₂ : (r.dual.balance' x l.dual).dual = l.balance' x r
rw₃ : (l.balance' x r).dual.dual = l.balance' x r
⊢ l.balanceR x r = l.balance' x r
have rw₄ : l.balance' x r = l.balance' x r
Tactic: rw [← dual_dual (balanceR l x r), dual_balanceR,
    balanceL_eq_balance' hr.dual hl.dual sr.dual sl.dual (balance_sz_dual H), ← dual_balance',
    dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r' r.size ∧ BalancedSz l.size r'
⊢ (l.balanceR x r).size = l.size + r.size + 1
have rw : (l.balance' x r).size = l.size + r.size + 1
Tactic: rw [balanceR_eq_balance' hl hr sl sr H, size_balance' sl sr]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r' r.size ∧ BalancedSz l.size r'
rw : (l.balance' x r).size = l.size + r.size + 1
⊢ (l.balanceR x r).size = l.size + r.size + 1
have rw₁ : l.size + r.size + 1 = l.size + r.size + 1
Tactic: rw [balanceR_eq_balance' hl hr sl sr H, size_balance' sl sr]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r' r.size ∧ BalancedSz l.size r'
⊢ All P (l.balanceR x r) ↔ All P l ∧ P x ∧ All P r
have rw : All P (l.balance' x r) ↔ All P l ∧ P x ∧ All P r
Tactic: rw [balanceR_eq_balance' hl hr sl sr H, all_balance']