awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (Ordnode.node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (Ordnode.node ls ll lx lr).Sized
H1 : (Ordnode.node ls ll lx lr).size = 0 → (Ordnode.node rs rl rx rr).size ≤ 1
H2 : ¬rs > delta * ls
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
                  Ordnode.node (ls + rs + 1) ll lx (Ordnode.node (rs + size_1 + 1) lr x (Ordnode.node rs rl rx rr))
                else
                  Ordnode.node (ls + rs + 1) (Ordnode.node (size + l.size + 1) ll lx l) x_2
                    (Ordnode.node (r.size + rs + 1) r x (Ordnode.node rs rl rx rr)))
              lr)
          ll
      else Ordnode.node (ls + rs + 1) (Ordnode.node ls ll lx lr) x (Ordnode.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
                  Ordnode.node (ls + rs + 1) ll lx (Ordnode.node (size_1 + rs + 1) lr x (Ordnode.node rs rl rx rr))
                else
                  Ordnode.node (ls + rs + 1) (Ordnode.node (size + l.size + 1) ll lx l) x_2
                    (Ordnode.node (r.size + rs + 1) r x (Ordnode.node rs rl rx rr)))
              lr)
          ll
      else Ordnode.node (ls + rs + 1) (Ordnode.node ls ll lx lr) x (Ordnode.node rs rl rx rr) :
      Ordnode α)
⊢ (Ordnode.node ls ll lx lr).balanceL x (Ordnode.node rs rl rx rr) =
    (Ordnode.node ls ll lx lr).balance x (Ordnode.node rs rl rx rr)

Tactic:
simp [balanceL, balance, H2]

Premises used: Ordnode.balanceL, Ordnode.balance
-- Module: Mathlib.Data.Ordmap.Invariants
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
h : 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:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Ordmap.Invariants
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
h : ¬delta * rs < ls
⊢ node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr) =
    node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
n m : ℕ
mp : Raised n m → n ≤ m ∧ m ≤ n + 1
mpr : n ≤ m ∧ m ≤ n + 1 → Raised n m
⊢ Raised n m ↔ n ≤ m ∧ m ≤ n + 1

Tactic:
constructor
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
m : ℕ
⊢ m ≤ m ∧ m ≤ m + 1

Tactic:
⟨le_rfl, Nat.le_succ _⟩

Premises used: le_rfl, Nat.le_succ, And.intro
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
m : ℕ
⊢ m ≤ m ∧ m ≤ m + 1

Tactic:
exact ⟨le_rfl, Nat.le_succ _⟩
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
n : ℕ
⊢ n ≤ n + 1 ∧ n + 1 ≤ n + 1

Tactic:
⟨Nat.le_succ _, le_rfl⟩

Premises used: le_rfl, Nat.le_succ, And.intro
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
n : ℕ
⊢ n ≤ n + 1 ∧ n + 1 ≤ n + 1

Tactic:
exact ⟨Nat.le_succ _, le_rfl⟩
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
n m : ℕ
h₁ : n ≤ m
h₂ : m ≤ n + 1
mpr : ∀ (h₁ : n ≤ n) (h₂ : n ≤ n + 1), Raised n n
mpr₁ : ∀ (h₁ : n < m), Raised n m
⊢ Raised n m

Tactic:
rcases eq_or_lt_of_le h₁ with (rfl | h₁)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
n : ℕ
h₁ : n ≤ n
h₂ : n ≤ n + 1
⊢ Raised n n

Tactic:
Or.inl rfl

Premises used: Ordnode.Raised, Or.inl, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
n : ℕ
h₁ : n ≤ n
h₂ : n ≤ n + 1
⊢ Raised n n

Tactic:
exact Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
n m : ℕ
h₁_1 : n ≤ m
h₂ : m ≤ n + 1
h₁ : n < m
⊢ Raised n m

Tactic:
Or.inr (le_antisymm h₂ h₁)

Premises used: Ordnode.Raised, le_antisymm, Or.inr
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
n m : ℕ
h₁_1 : n ≤ m
h₂ : m ≤ n + 1
h₁ : n < m
⊢ Raised n m

Tactic:
exact Or.inr (le_antisymm h₂ h₁)

Premises used: le_antisymm, Or.inr
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
n m : ℕ
H : Raised n m
⊢ n ≤ m

Tactic:
obtain ⟨H1, H2⟩ := raised_iff.1 H

Premises used: Ordnode.raised_iff, Iff.mp
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
n m : ℕ
H : Raised n m
H1 : n ≤ m
⊢ m ≤ n + 1

Tactic:
obtain ⟨H1, H2⟩ := raised_iff.1 H

Premises used: Ordnode.raised_iff, Iff.mp
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
rwa : m - n ≤ 1
rwa₁ rwa₂ rwa₃ rwa₄ : m ≤ n + 1
⊢ n.dist m ≤ 1

Tactic:
rwa [Nat.dist_eq_sub_of_le H1, tsub_le_iff_left]

Premises used: Nat.dist_eq_sub_of_le, tsub_le_iff_left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
n m : ℕ
H : Raised n m
rw : n.dist m ≤ 1
⊢ m.dist n ≤ 1

Tactic:
rw [Nat.dist_comm]

Premises used: Nat.dist_comm
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
n m : ℕ
H : Raised n m
⊢ n.dist m ≤ 1

Tactic:
H.dist_le

Premises used: Ordnode.Raised.dist_le
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
n m : ℕ
H : Raised n m
⊢ n.dist m ≤ 1

Tactic:
exact H.dist_le

Premises used: Ordnode.Raised.dist_le
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
k n m : ℕ
H : Raised n m
inl : Raised (k + m) (k + m)
inr : Raised (k + n) (k + (n + 1))
⊢ Raised (k + n) (k + m)

Tactic:
rcases H with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
k m : ℕ
⊢ Raised (k + m) (k + m)

Tactic:
Or.inl rfl

Premises used: Ordnode.Raised, Or.inl, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
k m : ℕ
⊢ Raised (k + m) (k + m)

Tactic:
exact Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
k n : ℕ
⊢ Raised (k + n) (k + (n + 1))

Tactic:
Or.inr rfl

Premises used: Ordnode.Raised, Or.inr, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
k n : ℕ
⊢ Raised (k + n) (k + (n + 1))

Tactic:
exact Or.inr rfl

Premises used: Or.inr, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
k n m : ℕ
H : Raised n m
rw : Raised (k + n) (k + m)
⊢ Raised (n + k) (m + k)

Tactic:
rw [add_comm, add_comm m]

Premises used: add_comm
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
k n m : ℕ
H : Raised n m
⊢ Raised (k + n) (k + m)

Tactic:
H.add_left _

Premises used: Ordnode.Raised.add_left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
k n m : ℕ
H : Raised n m
⊢ Raised (k + n) (k + m)

Tactic:
exact H.add_left _

Premises used: Ordnode.Raised.add_left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
H : Raised r₁.size r₂.size
generalize : ∀ (m : ℕ) (H : Raised r₁.size m), Raised (l.size + r₁.size + 1) (l.size + m + 1)
⊢ Raised (l.size + r₁.size + 1) (l.size + r₂.size + 1)

Tactic:
generalize size r₂ = m at H ⊢

Premises used: Ordnode.size
-- Module: Mathlib.Data.Ordmap.Invariants
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)
inr : Raised (l.size + r₁.size + 1) (l.size + (r₁.size + 1) + 1)
⊢ Raised (l.size + r₁.size + 1) (l.size + m + 1)

Tactic:
rcases H with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (l.size + r₁.size + 1) (l.size + r₁.size + 1)

Tactic:
Or.inl rfl

Premises used: Ordnode.Raised, Or.inl, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (l.size + r₁.size + 1) (l.size + r₁.size + 1)

Tactic:
exact Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (l.size + r₁.size + 1) (l.size + (r₁.size + 1) + 1)

Tactic:
Or.inr rfl

Premises used: Ordnode.Raised, Or.inr, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (l.size + r₁.size + 1) (l.size + (r₁.size + 1) + 1)

Tactic:
exact Or.inr rfl

Premises used: Or.inr, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
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
H2 : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
⊢ l.balanceL x r = l.balance' x r

Tactic:
rw [← balance_eq_balance' hl hr sl sr, balanceL_eq_balance sl sr]

Premises used: Ordnode.balance_eq_balance', Ordnode.balanceL_eq_balance
-- Module: Mathlib.Data.Ordmap.Invariants
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
⊢ (∃ (l' : ℕ), Raised l' 0 ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz 0 r'

Tactic:
rw [l0] at H
-- Module: Mathlib.Data.Ordmap.Invariants
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
H₁ : (∃ (l' : ℕ), Raised l' 0 ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz 0 r'
⊢ l.size = 0

Tactic:
rw [l0] at H
-- Module: Mathlib.Data.Ordmap.Invariants
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
H1₁ : ∀ (r' : ℕ) (e : Raised r.size r') (H : BalancedSz 0 r'), r.size ≤ 1
⊢ r.size ≤ 1

Tactic:
rcases H with (⟨_, ⟨⟨⟩⟩ | ⟨⟨⟩⟩, H⟩ | ⟨r', e, H⟩)
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l0 : l.size = 0
H : BalancedSz 0 r.size
⊢ r.size ≤ 1

Tactic:
balancedSz_zero.1 H.symm

Premises used: Ordnode.BalancedSz.symm, Ordnode.balancedSz_zero, Iff.mp
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l0 : l.size = 0
H : BalancedSz 0 r.size
⊢ r.size ≤ 1

Tactic:
exact balancedSz_zero.1 H.symm

Premises used: Ordnode.BalancedSz.symm, Ordnode.balancedSz_zero, Iff.mp
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l0 : l.size = 0
r' : ℕ
e : Raised r.size r'
H : BalancedSz 0 r'
⊢ r.size ≤ 1

Tactic:
le_trans (raised_iff.1 e).1 (balancedSz_zero.1 H.symm)

Premises used: Ordnode.raised_iff, Ordnode.BalancedSz.symm, Ordnode.balancedSz_zero, And.left, Iff.mp, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l0 : l.size = 0
r' : ℕ
e : Raised r.size r'
H : BalancedSz 0 r'
⊢ r.size ≤ 1

Tactic:
exact le_trans (raised_iff.1 e).1 (balancedSz_zero.1 H.symm)

Premises used: Ordnode.raised_iff, Ordnode.BalancedSz.symm, Ordnode.balancedSz_zero, And.left, Iff.mp, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
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
H2 : 1 ≤ r.size → r.size ≤ delta * l.size
⊢ 1 ≤ r.size → r.size ≤ delta * l.size

Tactic:
_
-- Module: Mathlib.Data.Ordmap.Invariants
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
H2₃ : ∀ (r' : ℕ) (e : Raised r.size r'), l.size ≤ delta * r' → ∀ (H₂ : r' ≤ delta * l.size), r.size ≤ delta * l.size
⊢ r.size ≤ delta * l.size

Tactic:
rcases H with (⟨l', e, H | ⟨_, H₂⟩⟩ | ⟨r', e, H | ⟨_, H₂⟩⟩)
-- Module: Mathlib.Data.Ordmap.Invariants
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
l' : ℕ
e : Raised l' l.size
H : l' + r.size ≤ 1
⊢ 0 < delta

Tactic:
decide
-- Module: Mathlib.Data.Ordmap.Invariants
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
l' : ℕ
e : Raised l' l.size
H : l' + r.size ≤ 1
⊢ r.size ≤ delta * l.size

Tactic:
exact le_trans (le_trans (Nat.le_add_left _ _) H) (mul_pos (by decide) l1 : (0 : ℕ) < _)

Premises used: Nat.le_add_left, mul_pos, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
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
l' : ℕ
e : Raised l' l.size
left : l' ≤ delta * r.size
H₂ : r.size ≤ delta * l'
⊢ r.size ≤ delta * l.size

Tactic:
le_trans H₂ (Nat.mul_le_mul_left _ (raised_iff.1 e).1)

Premises used: Ordnode.raised_iff, Nat.mul_le_mul_left, And.left, Iff.mp, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
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
l' : ℕ
e : Raised l' l.size
left : l' ≤ delta * r.size
H₂ : r.size ≤ delta * l'
⊢ r.size ≤ delta * l.size

Tactic:
exact le_trans H₂ (Nat.mul_le_mul_left _ (raised_iff.1 e).1)

Premises used: Ordnode.raised_iff, Nat.mul_le_mul_left, And.left, Iff.mp, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
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 ≤ r'

Tactic:
cases raised_iff.1 e

Premises used: Ordnode.raised_iff, Iff.mp
-- Module: Mathlib.Data.Ordmap.Invariants
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' ≤ r.size + 1

Tactic:
cases raised_iff.1 e

Premises used: Ordnode.raised_iff, Iff.mp
-- Module: Mathlib.Data.Ordmap.Invariants
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'
right : r' ≤ r.size + 1
⊢ r.size ≤ 3 * l.size

Tactic:
lia
-- Module: Mathlib.Data.Ordmap.Invariants
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'
left : l.size ≤ delta * r'
H₂ : r' ≤ delta * l.size
⊢ r.size ≤ delta * l.size

Tactic:
le_trans (raised_iff.1 e).1 H₂

Premises used: Ordnode.raised_iff, And.left, Iff.mp, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
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'
left : l.size ≤ delta * r'
H₂ : r' ≤ delta * l.size
⊢ r.size ≤ delta * l.size

Tactic:
exact le_trans (raised_iff.1 e).1 H₂

Premises used: Ordnode.raised_iff, And.left, Iff.mp, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
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'
rw : (∃ (l' : ℕ), Raised l' r.size ∧ BalancedSz l' l.size) ∨ ∃ (r' : ℕ), Raised l.size r' ∧ BalancedSz r.size r'
⊢ (∃ (l' : ℕ), Raised l' r.dual.size ∧ BalancedSz l' l.dual.size) ∨
    ∃ (r' : ℕ), Raised l.dual.size r' ∧ BalancedSz r.dual.size r'

Tactic:
rw [size_dual, size_dual]

Premises used: Ordnode.size_dual
-- Module: Mathlib.Data.Ordmap.Invariants
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.size ∧ BalancedSz l' l.size) ∨ ∃ (r' : ℕ), Raised l.size r' ∧ BalancedSz r.size r'

Tactic:
H.symm.imp (Exists.imp fun _ => And.imp_right BalancedSz.symm)
      (Exists.imp fun _ => And.imp_right BalancedSz.symm)

Premises used: Ordnode.BalancedSz.symm, Exists.imp, Or.symm, And.imp_right, Or.imp
-- Module: Mathlib.Data.Ordmap.Invariants
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.size ∧ BalancedSz l' l.size) ∨ ∃ (r' : ℕ), Raised l.size r' ∧ BalancedSz r.size r'

Tactic:
exact
    H.symm.imp (Exists.imp fun _ => And.imp_right BalancedSz.symm)
      (Exists.imp fun _ => And.imp_right BalancedSz.symm)

Premises used: Ordnode.BalancedSz.symm, Exists.imp, Or.symm, And.imp_right, Or.imp
-- Module: Mathlib.Data.Ordmap.Invariants
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
rw₁ rw₂ : l.size + r.size + 1 = l.size + r.size + 1
⊢ (l.balanceL x r).size = l.size + r.size + 1

Tactic:
rw [balanceL_eq_balance' hl hr sl sr H, size_balance' sl sr]

Premises used: Ordnode.balanceL_eq_balance', Ordnode.size_balance'
-- Module: Mathlib.Data.Ordmap.Invariants
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
rw₁ rw₂ : All P l ∧ P x ∧ All P r ↔ All P l ∧ P x ∧ All P r
⊢ All P (l.balanceL x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
rw [balanceL_eq_balance' hl hr sl sr H, all_balance']

Premises used: Ordnode.balanceL_eq_balance', Ordnode.all_balance'
-- Module: Mathlib.Data.Ordmap.Invariants
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
rw₄ rw₅ : l.balance' x r = l.balance' x r
⊢ l.balanceR 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]

Premises used: Ordnode.balance_sz_dual, Ordnode.balanceL_eq_balance', Ordnode.dual_balanceR, Ordnode.Balanced.dual, Ordnode.dual_balance', Ordnode.Sized.dual, Ordnode.balanceR, Ordnode.dual_dual
-- Module: Mathlib.Data.Ordmap.Invariants
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
rw₁ rw₂ : l.size + r.size + 1 = l.size + r.size + 1
⊢ (l.balanceR x r).size = l.size + r.size + 1

Tactic:
rw [balanceR_eq_balance' hl hr sl sr H, size_balance' sl sr]

Premises used: Ordnode.balanceR_eq_balance', Ordnode.size_balance'
-- Module: Mathlib.Data.Ordmap.Invariants
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'
rw : All P (l.balance' x r) ↔ All P l ∧ P x ∧ All P r
rw₁ rw₂ : All P l ∧ P x ∧ All P r ↔ All P l ∧ P x ∧ All P r
⊢ All P (l.balanceR x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
rw [balanceR_eq_balance' hl hr sl sr H, all_balance']

Premises used: Ordnode.balanceR_eq_balance', Ordnode.all_balance'
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : Bounded nil o₁ o₂
bot : ∀ (h : Bounded nil ⊥ o₂), Bounded (Ordnode.dual nil) o₂ ⊥
coe : ∀ (a : α) (h : Bounded nil (↑a : WithBot α) o₂), Bounded (Ordnode.dual nil) o₂ (↑a : WithBot α)
⊢ Bounded (Ordnode.dual nil) o₂ o₁

Tactic:
cases o₁
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
o₂ : WithTop α
h : Bounded nil ⊥ o₂
bot : ∀ (h : Bounded.{u_1} (α := α) nil ⊥ ⊤), Bounded.{u_1} (α := αᵒᵈ) (Ordnode.dual nil) ⊤ ⊥
bot₁ : ∀ (a : α) (h : Bounded nil ⊥ (↑a : WithTop α)), Bounded (Ordnode.dual nil) (↑a : WithTop α) ⊥
⊢ Bounded (Ordnode.dual nil) o₂ ⊥

Tactic:
cases o₂
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
o₂ : WithTop α
a : α
h : Bounded nil (↑a : WithBot α) o₂
coe : ∀ (h : Bounded nil (↑a : WithBot α) ⊤), Bounded (Ordnode.dual nil) ⊤ (↑a : WithBot α)
coe₁ :
  ∀ (a_1 : α) (h : Bounded nil (↑a : WithBot α) (↑a_1 : WithTop α)),
    Bounded (Ordnode.dual nil) (↑a_1 : WithTop α) (↑a : WithBot α)
⊢ Bounded (Ordnode.dual nil) o₂ (↑a : WithBot α)

Tactic:
cases o₂
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
h : Bounded.{u_1} (α := α) nil ⊥ ⊤
⊢ Bounded.{u_1} (α := αᵒᵈ) (Ordnode.dual nil) ⊤ ⊥

Tactic:
trivial
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
a : α
h : Bounded nil ⊥ (↑a : WithTop α)
⊢ Bounded (Ordnode.dual nil) (↑a : WithTop α) ⊥

Tactic:
trivial
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
a : α
h : Bounded nil (↑a : WithBot α) ⊤
⊢ Bounded (Ordnode.dual nil) ⊤ (↑a : WithBot α)

Tactic:
trivial
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
a a_1 : α
h : Bounded nil (↑a : WithBot α) (↑a_1 : WithTop α)
⊢ Bounded (Ordnode.dual nil) (↑a_1 : WithTop α) (↑a : WithBot α)

Tactic:
trivial