awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
hm : (node size l_1 x_1 r).Sized
⊢ (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).size = l.size + size + 1
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).size =
  l.size + (l_1.size + r.size + 1) + 1
Tactic: simp only [hm.1]
-- 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 α
hm : (node size l_1 x_1 r).Sized
⊢ (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).size =
    l.size + (l_1.size + r.size + 1) + 1
have pos : l_1.size < ratio * r.size → (l.node3L x l_1 x_1 r).size = l.size + (l_1.size + r.size + 1) + 1
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 α
hm : (node size l_1 x_1 r).Sized
pos : l_1.size < ratio * r.size → (l.node3L x l_1 x_1 r).size = l.size + (l_1.size + r.size + 1) + 1
⊢ (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).size =
    l.size + (l_1.size + r.size + 1) + 1
have neg : ¬l_1.size < ratio * r.size → (l.node4L x l_1 x_1 r).size = l.size + (l_1.size + r.size + 1) + 1
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 α
hm : (node size l_1 x_1 r).Sized
h : l_1.size < ratio * r.size
⊢ (l.node3L x l_1 x_1 r).size = l.size + (l_1.size + r.size + 1) + 1
have pos : l.size + l_1.size + r.size + 1 = l.size + (l_1.size + r.size + 1)
Tactic: simp [node3L_size, node4L_size hm.2.1]
-- 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 α
hm : (node size l_1 x_1 r).Sized
h : ¬l_1.size < ratio * r.size
⊢ (l.node4L x l_1 x_1 r).size = l.size + (l_1.size + r.size + 1) + 1
have neg : l.size + l_1.size + r.size + 1 = l.size + (l_1.size + r.size + 1)
Tactic: simp [node3L_size, node4L_size hm.2.1]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
⊢ (l.rotateR x r).size = l.size + r.size + 1
have rw : (l.rotateR x r).dual.size = l.size + r.size + 1
Tactic: rw [← size_dual, dual_rotateR, hl.dual.rotateL_size, size_dual, size_dual, add_comm (size l)]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
rw : (l.rotateR x r).dual.size = l.size + r.size + 1
⊢ (l.rotateR x r).size = l.size + r.size + 1
have rw₁ : (r.dual.rotateL x l.dual).size = l.size + r.size + 1
Tactic: rw [← size_dual, dual_rotateR, hl.dual.rotateL_size, size_dual, size_dual, add_comm (size l)]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
rw : (l.rotateR x r).dual.size = l.size + r.size + 1
rw₁ : (r.dual.rotateL x l.dual).size = l.size + r.size + 1
⊢ (l.rotateR x r).size = l.size + r.size + 1
have rw₂ : r.dual.size + l.dual.size + 1 = l.size + r.size + 1
Tactic: rw [← size_dual, dual_rotateR, hl.dual.rotateL_size, size_dual, size_dual, add_comm (size l)]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
rw : (l.rotateR x r).dual.size = l.size + r.size + 1
rw₁ : (r.dual.rotateL x l.dual).size = l.size + r.size + 1
rw₂ : r.dual.size + l.dual.size + 1 = l.size + r.size + 1
⊢ (l.rotateR x r).size = l.size + r.size + 1
have rw₃ : r.size + l.dual.size + 1 = l.size + r.size + 1
Tactic: rw [← size_dual, dual_rotateR, hl.dual.rotateL_size, size_dual, size_dual, add_comm (size l)]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
rw : (l.rotateR x r).dual.size = l.size + r.size + 1
rw₁ : (r.dual.rotateL x l.dual).size = l.size + r.size + 1
rw₂ : r.dual.size + l.dual.size + 1 = l.size + r.size + 1
rw₃ : r.size + l.dual.size + 1 = l.size + r.size + 1
⊢ (l.rotateR x r).size = l.size + r.size + 1
have rw₄ : r.size + l.size + 1 = l.size + r.size + 1
Tactic: rw [← size_dual, dual_rotateR, hl.dual.rotateL_size, size_dual, size_dual, add_comm (size l)]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
rw : (l.rotateR x r).dual.size = l.size + r.size + 1
rw₁ : (r.dual.rotateL x l.dual).size = l.size + r.size + 1
rw₂ : r.dual.size + l.dual.size + 1 = l.size + r.size + 1
rw₃ : r.size + l.dual.size + 1 = l.size + r.size + 1
rw₄ : r.size + l.size + 1 = l.size + r.size + 1
⊢ (l.rotateR x r).size = l.size + r.size + 1
have rw₅ : r.size + l.size + 1 = r.size + l.size + 1
Tactic: rw [← size_dual, dual_rotateR, hl.dual.rotateL_size, size_dual, size_dual, add_comm (size l)]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (if l.size + r.size ≤ 1 then l.node' x r
    else
      if r.size > delta * l.size then l.rotateL x r
      else if l.size > delta * r.size then l.rotateR x r else l.node' x r).Sized
have pos : l.size + r.size ≤ 1 → (l.node' x r).Sized
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
pos : l.size + r.size ≤ 1 → (l.node' x r).Sized
⊢ (if l.size + r.size ≤ 1 then l.node' x r
    else
      if r.size > delta * l.size then l.rotateL x r
      else if l.size > delta * r.size then l.rotateR x r else l.node' x r).Sized
have pos₁ : ¬l.size + r.size ≤ 1 → r.size > delta * l.size → (l.rotateL x r).Sized
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
pos : l.size + r.size ≤ 1 → (l.node' x r).Sized
pos₁ : ¬l.size + r.size ≤ 1 → r.size > delta * l.size → (l.rotateL x r).Sized
⊢ (if l.size + r.size ≤ 1 then l.node' x r
    else
      if r.size > delta * l.size then l.rotateL x r
      else if l.size > delta * r.size then l.rotateR x r else l.node' x r).Sized
have pos₂ : ¬l.size + r.size ≤ 1 → ¬r.size > delta * l.size → l.size > delta * r.size → (l.rotateR x r).Sized
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
pos : l.size + r.size ≤ 1 → (l.node' x r).Sized
pos₁ : ¬l.size + r.size ≤ 1 → r.size > delta * l.size → (l.rotateL x r).Sized
pos₂ : ¬l.size + r.size ≤ 1 → ¬r.size > delta * l.size → l.size > delta * r.size → (l.rotateR x r).Sized
⊢ (if l.size + r.size ≤ 1 then l.node' x r
    else
      if r.size > delta * l.size then l.rotateL x r
      else if l.size > delta * r.size then l.rotateR x r else l.node' x r).Sized
have neg : ¬l.size + r.size ≤ 1 → ¬r.size > delta * l.size → ¬l.size > delta * r.size → (l.node' x r).Sized
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if r.size > delta * l.size then l.rotateL x r
        else if l.size > delta * r.size then l.rotateR x r else l.node' x r).size =
    l.size + r.size + 1
have pos : l.size + r.size ≤ 1 → (l.node' x r).size = l.size + r.size + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
pos : l.size + r.size ≤ 1 → (l.node' x r).size = l.size + r.size + 1
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if r.size > delta * l.size then l.rotateL x r
        else if l.size > delta * r.size then l.rotateR x r else l.node' x r).size =
    l.size + r.size + 1
have pos₁ : ¬l.size + r.size ≤ 1 → r.size > delta * l.size → (l.rotateL x r).size = l.size + r.size + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
pos : l.size + r.size ≤ 1 → (l.node' x r).size = l.size + r.size + 1
pos₁ : ¬l.size + r.size ≤ 1 → r.size > delta * l.size → (l.rotateL x r).size = l.size + r.size + 1
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if r.size > delta * l.size then l.rotateL x r
        else if l.size > delta * r.size then l.rotateR x r else l.node' x r).size =
    l.size + r.size + 1
have pos₂ : ¬l.size + r.size ≤ 1 → ¬r.size > delta * l.size → l.size > delta * r.size → (l.rotateR x r).size = l.size + r.size + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
pos : l.size + r.size ≤ 1 → (l.node' x r).size = l.size + r.size + 1
pos₁ : ¬l.size + r.size ≤ 1 → r.size > delta * l.size → (l.rotateL x r).size = l.size + r.size + 1
pos₂ :
  ¬l.size + r.size ≤ 1 → ¬r.size > delta * l.size → l.size > delta * r.size → (l.rotateR x r).size = l.size + r.size + 1
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if r.size > delta * l.size then l.rotateL x r
        else if l.size > delta * r.size then l.rotateR x r else l.node' x r).size =
    l.size + r.size + 1
have neg : ¬l.size + r.size ≤ 1 → ¬r.size > delta * l.size → ¬l.size > delta * r.size → (l.node' x r).size = l.size + r.size + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ All P (l.node4L x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r
have nil : All P (l.node4L x nil y r) ↔ All P l ∧ P x ∧ All P nil ∧ P y ∧ All P r
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
nil : All P (l.node4L x Ordnode.nil y r) ↔ All P l ∧ P x ∧ All P Ordnode.nil ∧ P y ∧ All P r
⊢ All P (l.node4L x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r
have node : ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α),
  All P (l.node4L x (node size l_1 x_1 r_1) y r) ↔ All P l ∧ P x ∧ All P (node size l_1 x_1 r_1) ∧ P y ∧ All P r
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ All P (l.node4R x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r
have nil : All P (l.node4R x nil y r) ↔ All P l ∧ P x ∧ All P nil ∧ P y ∧ All P r
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
nil : All P (l.node4R x Ordnode.nil y r) ↔ All P l ∧ P x ∧ All P Ordnode.nil ∧ P y ∧ All P r
⊢ All P (l.node4R x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r
have node : ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α),
  All P (l.node4R x (node size l_1 x_1 r_1) y r) ↔ All P l ∧ P x ∧ All P (node size l_1 x_1 r_1) ∧ P y ∧ All P r
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (l.rotateL x r) ↔ All P l ∧ P x ∧ All P r
have nil : All P (l.rotateL x nil) ↔ All P l ∧ P x ∧ All P nil
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
nil : All P (l.rotateL x Ordnode.nil) ↔ All P l ∧ P x ∧ All P Ordnode.nil
⊢ All P (l.rotateL x r) ↔ All P l ∧ P x ∧ All P r
have node : ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r : Ordnode α),
  All P (l.rotateL x (node size l_1 x_1 r)) ↔ All P l ∧ P x ∧ All P (node size l_1 x_1 r)
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
⊢ All P (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) ↔
    All P l ∧ P x ∧ All P (node size l_1 x_1 r)
have pos : l_1.size < ratio * r.size → (All P (l.node3L x l_1 x_1 r) ↔ All P l ∧ P x ∧ All P (node size l_1 x_1 r))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
pos : l_1.size < ratio * r.size → (All P (l.node3L x l_1 x_1 r) ↔ All P l ∧ P x ∧ All P (node size l_1 x_1 r))
⊢ All P (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) ↔
    All P l ∧ P x ∧ All P (node size l_1 x_1 r)
have neg : ¬l_1.size < ratio * r.size → (All P (l.node4L x l_1 x_1 r) ↔ All P l ∧ P x ∧ All P (node size l_1 x_1 r))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (l.rotateR x r) ↔ All P l ∧ P x ∧ All P r
have rw : All P r.dual ∧ P x ∧ All P l.dual ↔ All P l ∧ P x ∧ All P r
Tactic: rw [← all_dual, dual_rotateR, all_rotateL]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P
      (if l.size + r.size ≤ 1 then l.node' x r
      else
        if r.size > delta * l.size then l.rotateL x r
        else if l.size > delta * r.size then l.rotateR x r else l.node' x r) ↔
    All P l ∧ P x ∧ All P r
have pos : l.size + r.size ≤ 1 → (All P (l.node' x r) ↔ All P l ∧ P x ∧ All P r)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
pos : l.size + r.size ≤ 1 → (All P (l.node' x r) ↔ All P l ∧ P x ∧ All P r)
⊢ All P
      (if l.size + r.size ≤ 1 then l.node' x r
      else
        if r.size > delta * l.size then l.rotateL x r
        else if l.size > delta * r.size then l.rotateR x r else l.node' x r) ↔
    All P l ∧ P x ∧ All P r
have pos₁ : ¬l.size + r.size ≤ 1 → r.size > delta * l.size → (All P (l.rotateL x r) ↔ All P l ∧ P x ∧ All P r)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
pos : l.size + r.size ≤ 1 → (All P (l.node' x r) ↔ All P l ∧ P x ∧ All P r)
pos₁ : ¬l.size + r.size ≤ 1 → r.size > delta * l.size → (All P (l.rotateL x r) ↔ All P l ∧ P x ∧ All P r)
⊢ All P
      (if l.size + r.size ≤ 1 then l.node' x r
      else
        if r.size > delta * l.size then l.rotateL x r
        else if l.size > delta * r.size then l.rotateR x r else l.node' x r) ↔
    All P l ∧ P x ∧ All P r
have pos₂ : ¬l.size + r.size ≤ 1 →
  ¬r.size > delta * l.size → l.size > delta * r.size → (All P (l.rotateR x r) ↔ All P l ∧ P x ∧ All P r)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
pos : l.size + r.size ≤ 1 → (All P (l.node' x r) ↔ All P l ∧ P x ∧ All P r)
pos₁ : ¬l.size + r.size ≤ 1 → r.size > delta * l.size → (All P (l.rotateL x r) ↔ All P l ∧ P x ∧ All P r)
pos₂ :
  ¬l.size + r.size ≤ 1 →
    ¬r.size > delta * l.size → l.size > delta * r.size → (All P (l.rotateR x r) ↔ All P l ∧ P x ∧ All P r)
⊢ All P
      (if l.size + r.size ≤ 1 then l.node' x r
      else
        if r.size > delta * l.size then l.rotateL x r
        else if l.size > delta * r.size then l.rotateR x r else l.node' x r) ↔
    All P l ∧ P x ∧ All P r
have neg : ¬l.size + r.size ≤ 1 →
  ¬r.size > delta * l.size → ¬l.size > delta * r.size → (All P (l.node' x r) ↔ All P l ∧ P x ∧ All P r)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
r' : List α
⊢ foldr List.cons (node size l x r) r' = (node size l x r).toList ++ r'
have rw : foldr List.cons l (x :: r.toList) ++ r' = (node size l x r).toList ++ r'
Tactic: rw [foldr, foldr_cons_eq_toList l, foldr_cons_eq_toList r, ← List.cons_append,
        ← List.append_assoc, ← foldr_cons_eq_toList l]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ (node s l x r).toList = l.toList ++ x :: r.toList
have rw : l.toList ++ x :: foldr List.cons r [] = l.toList ++ x :: r.toList
Tactic: rw [toList, foldr, foldr_cons_eq_toList]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
t : Ordnode α
⊢ Any (Eq x) t ↔ x ∈ t.toList
have nil : Any (Eq x) nil ↔ Membership.mem (γ := List α) (toList nil) x
Tactic: induction t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
t : Ordnode α
nil : Any (Eq x) Ordnode.nil ↔ Membership.mem (γ := List α) (toList Ordnode.nil) x
⊢ Any (Eq x) t ↔ x ∈ t.toList
have node : ∀ (size : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α),
  (Any (Eq x) l ↔ x ∈ l.toList) →
    (Any (Eq x) r ↔ x ∈ r.toList) → (Any (Eq x) (node size l x_1 r) ↔ x ∈ (node size l x_1 r).toList)
Tactic: induction t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ (node size l x r).toList.length = (node size l x r).realSize
have rw : l.realSize + (r.realSize + 1) = (node size l x r).realSize
Tactic: rw [toList_node, List.length_append, List.length_cons, length_toList' l,
        length_toList' r]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
h : t.Sized
⊢ t.toList.length = t.size
have rw : t.realSize = t.size
Tactic: rw [length_toList', size_eq_realSize h]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
h : t.Sized
rw : t.realSize = t.size
⊢ t.toList.length = t.size
have rw₁ : t.realSize = t.realSize
Tactic: rw [length_toList', size_eq_realSize h]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t₁ t₂ : Ordnode α
h₁ : t₁.Sized
h₂ : t₂.Sized
h : t₁.toList = t₂.toList
⊢ t₁.size = t₂.size
have rw : t₁.toList.length = t₂.size
Tactic: rw [← length_toList h₁, h, length_toList h₂]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t₁ t₂ : Ordnode α
h₁ : t₁.Sized
h₂ : t₂.Sized
h : t₁.toList = t₂.toList
rw : t₁.toList.length = t₂.size
⊢ t₁.size = t₂.size
have rw₁ : t₂.toList.length = t₂.size
Tactic: rw [← length_toList h₁, h, length_toList h₂]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t₁ t₂ : Ordnode α
h₁ : t₁.Sized
h₂ : t₂.Sized
h : t₁.toList = t₂.toList
rw : t₁.toList.length = t₂.size
rw₁ : t₂.toList.length = t₂.size
⊢ t₁.size = t₂.size
have rw₂ : t₂.size = t₂.size
Tactic: rw [← length_toList h₁, h, length_toList h₂]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : DecidableLE α
x : α
t : Ordnode α
h : t.Sized
h_mem : x ∈ t
⊢ 0 < t.size
have nil : ∀ (h : Sized.{u_1} (α := α) nil) (h_mem : Membership.mem (γ := Ordnode α) nil x), 0 < size.{u_1} (α := α) nil
Tactic: cases t
Cleared hypotheses: t, h, h_mem
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : DecidableLE α
x : α
t : Ordnode α
h : t.Sized
h_mem : x ∈ t
nil :
  ∀ (h : Sized.{u_1} (α := α) Ordnode.nil) (h_mem : Membership.mem (γ := Ordnode α) Ordnode.nil x),
    0 < size.{u_1} (α := α) Ordnode.nil
⊢ 0 < t.size
have node : ∀ (size : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) (h : (node size l x_1 r).Sized) (h_mem : x ∈ node size l x_1 r),
  0 < (node size l x_1 r).size
Tactic: cases t
Cleared hypotheses: t, h, h_mem
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
x : α
⊢ findMax' x t.dual = t.findMin' x
have rw : t.dual.dual.findMin' x = t.findMin' x
Tactic: rw [← findMin'_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
x : α
rw : t.dual.dual.findMin' x = t.findMin' x
⊢ findMax' x t.dual = t.findMin' x
have rw₁ : t.findMin' x = t.findMin' x
Tactic: rw [← findMin'_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
⊢ t.dual.findMax = t.findMin
have rw : t.dual.dual.findMin = t.findMin
Tactic: rw [← findMin_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
rw : t.dual.dual.findMin = t.findMin
⊢ t.dual.findMax = t.findMin
have rw₁ : t.findMin = t.findMin
Tactic: rw [← findMin_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
size sz : ℕ
l' : Ordnode α
y : α
r' : Ordnode α
x : α
r : Ordnode α
⊢ (node size (node sz l' y r') x r).eraseMin.dual = (node size (node sz l' y r') x r).dual.eraseMax
have rw : ((node sz l' y r').eraseMin.balanceR x r).dual = (node size (node sz l' y r') x r).dual.eraseMax
Tactic: rw [eraseMin, dual_balanceR, dual_eraseMin (node sz l' y r'), dual, dual, dual, eraseMax]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
size sz : ℕ
l' : Ordnode α
y : α
r' : Ordnode α
x : α
r : Ordnode α
rw : ((node sz l' y r').eraseMin.balanceR x r).dual = (node size (node sz l' y r') x r).dual.eraseMax
⊢ (node size (node sz l' y r') x r).eraseMin.dual = (node size (node sz l' y r') x r).dual.eraseMax
have rw₁ : r.dual.balanceL x (node sz l' y r').eraseMin.dual = (node size (node sz l' y r') x r).dual.eraseMax
Tactic: rw [eraseMin, dual_balanceR, dual_eraseMin (node sz l' y r'), dual, dual, dual, eraseMax]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
size sz : ℕ
l' : Ordnode α
y : α
r' : Ordnode α
x : α
r : Ordnode α
rw : ((node sz l' y r').eraseMin.balanceR x r).dual = (node size (node sz l' y r') x r).dual.eraseMax
rw₁ : r.dual.balanceL x (node sz l' y r').eraseMin.dual = (node size (node sz l' y r') x r).dual.eraseMax
⊢ (node size (node sz l' y r') x r).eraseMin.dual = (node size (node sz l' y r') x r).dual.eraseMax
have rw₂ : r.dual.balanceL x (node sz l' y r').dual.eraseMax = (node size (node sz l' y r') x r).dual.eraseMax
Tactic: rw [eraseMin, dual_balanceR, dual_eraseMin (node sz l' y r'), dual, dual, dual, eraseMax]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
size sz : ℕ
l' : Ordnode α
y : α
r' : Ordnode α
x : α
r : Ordnode α
rw : ((node sz l' y r').eraseMin.balanceR x r).dual = (node size (node sz l' y r') x r).dual.eraseMax
rw₁ : r.dual.balanceL x (node sz l' y r').eraseMin.dual = (node size (node sz l' y r') x r).dual.eraseMax
rw₂ : r.dual.balanceL x (node sz l' y r').dual.eraseMax = (node size (node sz l' y r') x r).dual.eraseMax
⊢ (node size (node sz l' y r') x r).eraseMin.dual = (node size (node sz l' y r') x r).dual.eraseMax
have rw₃ : r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax = (node size (node sz l' y r') x r).dual.eraseMax
Tactic: rw [eraseMin, dual_balanceR, dual_eraseMin (node sz l' y r'), dual, dual, dual, eraseMax]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
size sz : ℕ
l' : Ordnode α
y : α
r' : Ordnode α
x : α
r : Ordnode α
rw : ((node sz l' y r').eraseMin.balanceR x r).dual = (node size (node sz l' y r') x r).dual.eraseMax
rw₁ : r.dual.balanceL x (node sz l' y r').eraseMin.dual = (node size (node sz l' y r') x r).dual.eraseMax
rw₂ : r.dual.balanceL x (node sz l' y r').dual.eraseMax = (node size (node sz l' y r') x r).dual.eraseMax
rw₃ : r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax = (node size (node sz l' y r') x r).dual.eraseMax
⊢ (node size (node sz l' y r') x r).eraseMin.dual = (node size (node sz l' y r') x r).dual.eraseMax
have rw₄ : r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax = (node size r.dual x (node sz l' y r').dual).eraseMax
Tactic: rw [eraseMin, dual_balanceR, dual_eraseMin (node sz l' y r'), dual, dual, dual, eraseMax]