awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
hm : Sized.{u_1} (α := α) nil
⊢ (l.rotateL x nil).size = l.size + size.{u_1} (α := α) nil + 1

Tactic:
simp [Ordnode.rotateL]

Premises used: Ordnode.rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
hm : (Ordnode.node size l_1 x_1 r).Sized
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 + size + 1
⊢ (l.rotateL x (Ordnode.node size l_1 x_1 r)).size = l.size + (Ordnode.node size l_1 x_1 r).size + 1

Tactic:
simp [Ordnode.rotateL]

Premises used: Ordnode.rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
hm : (Ordnode.node size l_1 x_1 r).Sized
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
⊢ (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

Tactic:
simp only [hm.1]

Premises used: And.left
-- Module: Mathlib.Data.Ordmap.Invariants
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
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
⊢ (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:
split_ifs
-- Module: Mathlib.Data.Ordmap.Invariants
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
pos : l.size + l_1.size + r.size + 1 = l.size + (l_1.size + r.size + 1)
⊢ (l.node3L x l_1 x_1 r).size = l.size + (l_1.size + r.size + 1) + 1

Tactic:
simp [node3L_size, node4L_size hm.2.1]

Premises used: Ordnode.node4L_size, And.right, And.left, Ordnode.node3L_size
-- Module: Mathlib.Data.Ordmap.Invariants
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
neg : l.size + l_1.size + r.size + 1 = l.size + (l_1.size + r.size + 1)
⊢ (l.node4L x l_1 x_1 r).size = l.size + (l_1.size + r.size + 1) + 1

Tactic:
simp [node3L_size, node4L_size hm.2.1]

Premises used: Ordnode.node4L_size, And.right, And.left, Ordnode.node3L_size
-- Module: Mathlib.Data.Ordmap.Invariants
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.size + l_1.size + r.size + 1 = l.size + (l_1.size + r.size + 1)

Tactic:
abel
-- Module: Mathlib.Data.Ordmap.Invariants
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.size + l_1.size + r.size + 1 = l.size + (l_1.size + r.size + 1)

Tactic:
abel
-- Module: Mathlib.Data.Ordmap.Invariants
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
rw₅ rw₆ : r.size + l.size + 1 = r.size + l.size + 1
⊢ (l.rotateR x r).size = l.size + r.size + 1

Tactic:
rw [← size_dual, dual_rotateR, hl.dual.rotateL_size, size_dual, size_dual, add_comm (size l)]

Premises used: Ordnode.size_dual, Ordnode.Sized.rotateL_size, Ordnode.size, Ordnode.dual_rotateR, add_comm, Ordnode.Sized.dual
-- Module: Mathlib.Data.Ordmap.Invariants
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
neg : ¬l.size + r.size ≤ 1 → ¬r.size > delta * l.size → ¬l.size > delta * r.size → (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

Tactic:
split_ifs
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h : l.size + r.size ≤ 1
⊢ (l.node' x r).Sized

Tactic:
hl.node' hr

Premises used: Ordnode.Sized.node'
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h : l.size + r.size ≤ 1
⊢ (l.node' x r).Sized

Tactic:
exact hl.node' hr

Premises used: Ordnode.Sized.node'
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h : ¬l.size + r.size ≤ 1
h_1 : r.size > delta * l.size
⊢ (l.rotateL x r).Sized

Tactic:
hl.rotateL hr

Premises used: Ordnode.Sized.rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h : ¬l.size + r.size ≤ 1
h_1 : r.size > delta * l.size
⊢ (l.rotateL x r).Sized

Tactic:
exact hl.rotateL hr

Premises used: Ordnode.Sized.rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : l.size > delta * r.size
⊢ (l.rotateR x r).Sized

Tactic:
hl.rotateR hr

Premises used: Ordnode.Sized.rotateR
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : l.size > delta * r.size
⊢ (l.rotateR x r).Sized

Tactic:
exact hl.rotateR hr

Premises used: Ordnode.Sized.rotateR
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : ¬l.size > delta * r.size
⊢ (l.node' x r).Sized

Tactic:
hl.node' hr

Premises used: Ordnode.Sized.node'
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : ¬l.size > delta * r.size
⊢ (l.node' x r).Sized

Tactic:
exact hl.node' hr

Premises used: Ordnode.Sized.node'
-- Module: Mathlib.Data.Ordmap.Invariants
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
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
⊢ (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

Tactic:
split_ifs
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h : l.size + r.size ≤ 1
⊢ (l.node' x r).size = l.size + r.size + 1

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h : ¬l.size + r.size ≤ 1
h_1 : r.size > delta * l.size
⊢ (l.rotateL x r).size = l.size + r.size + 1

Tactic:
hr.rotateL_size

Premises used: Ordnode.Sized.rotateL_size
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h : ¬l.size + r.size ≤ 1
h_1 : r.size > delta * l.size
⊢ (l.rotateL x r).size = l.size + r.size + 1

Tactic:
exact hr.rotateL_size

Premises used: Ordnode.Sized.rotateL_size
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : l.size > delta * r.size
⊢ (l.rotateR x r).size = l.size + r.size + 1

Tactic:
hl.rotateR_size

Premises used: Ordnode.Sized.rotateR_size
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : l.size > delta * r.size
⊢ (l.rotateR x r).size = l.size + r.size + 1

Tactic:
exact hl.rotateR_size

Premises used: Ordnode.Sized.rotateR_size
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : ¬l.size > delta * r.size
⊢ (l.node' x r).size = l.size + r.size + 1

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
x : α
⊢ All P {x} ↔ P x

Tactic:
⟨fun h => h.2.1, fun h => ⟨⟨⟩, h, ⟨⟩⟩⟩

Premises used: And.right, And.left, And.intro, Iff.intro, True.intro
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
x : α
h : P x
⊢ P x

Tactic:
h
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
x : α
h : P x
⊢ P x

Tactic:
exact h
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (node size l x r) ↔ ∀ (x_1 : α), Emem x_1 (node size l x r) → P x_1

Tactic:
simp [All, Emem, all_iff_forall, Any, or_imp, forall_and]

Premises used: or_imp, Ordnode.Any, Ordnode.All, Ordnode.Emem, forall_and
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ Any P (node size l x r) ↔ ∃ (x_1 : α), Any (Eq x_1) (node size l x r) ∧ P x_1

Tactic:
simp [Any, any_iff_exists, or_and_right, exists_or]

Premises used: exists_or, Ordnode.Any, or_and_right
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
t : Ordnode α
⊢ Emem x t ↔ ∀ (P : α → Prop), All P t → P x

Tactic:
⟨fun h _ al => all_iff_forall.1 al _ h, fun H => H _ <| all_iff_forall.2 fun _ => id⟩

Premises used: Iff.mpr, id, Iff.intro, Ordnode.Emem, Iff.mp, Ordnode.all_iff_forall
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (l.node' x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
Iff.rfl

Premises used: Iff.rfl, Ordnode.All
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ All P (l.node3L x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r

Tactic:
simp [node3L, all_node', and_assoc]

Premises used: Ordnode.node3L, Ordnode.all_node', and_assoc
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ All P (l.node3R x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r

Tactic:
Iff.rfl

Premises used: Iff.rfl, Ordnode.All
-- Module: Mathlib.Data.Ordmap.Invariants
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
node :
  ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α),
    All P (l.node4L x (Ordnode.node size l_1 x_1 r_1) y r) ↔
      All P l ∧ P x ∧ All P (Ordnode.node size l_1 x_1 r_1) ∧ 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

Tactic:
cases m
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
⊢ All P (l.node4L x nil y r) ↔ All P l ∧ P x ∧ All P nil ∧ P y ∧ All P r

Tactic:
simp [node4L, all_node', All, all_node3L, and_assoc]

Premises used: Ordnode.all_node', Ordnode.All, and_assoc, Ordnode.node4L, Ordnode.all_node3L
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
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:
simp [node4L, all_node', All, all_node3L, and_assoc]

Premises used: Ordnode.all_node', Ordnode.All, and_assoc, Ordnode.node4L, Ordnode.all_node3L
-- Module: Mathlib.Data.Ordmap.Invariants
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
node :
  ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α),
    All P (l.node4R x (Ordnode.node size l_1 x_1 r_1) y r) ↔
      All P l ∧ P x ∧ All P (Ordnode.node size l_1 x_1 r_1) ∧ 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

Tactic:
cases m
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
⊢ All P (l.node4R x nil y r) ↔ All P l ∧ P x ∧ All P nil ∧ P y ∧ All P r

Tactic:
simp [node4R, all_node', All, all_node3R, and_assoc]

Premises used: Ordnode.all_node3R, Ordnode.all_node', Ordnode.All, and_assoc, Ordnode.node4R
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
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:
simp [node4R, all_node', All, all_node3R, and_assoc]

Premises used: Ordnode.all_node3R, Ordnode.all_node', Ordnode.All, and_assoc, Ordnode.node4R
-- Module: Mathlib.Data.Ordmap.Invariants
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
node :
  ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r : Ordnode α),
    All P (l.rotateL x (Ordnode.node size l_1 x_1 r)) ↔ All P l ∧ P x ∧ All P (Ordnode.node size l_1 x_1 r)
⊢ All P (l.rotateL x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
cases r
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
⊢ All P (l.rotateL x nil) ↔ All P l ∧ P x ∧ All P nil

Tactic:
simp [rotateL, all_node']

Premises used: Ordnode.all_node', Ordnode.rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
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))
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))
⊢ 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)

Tactic:
split_ifs
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
h : 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:
simp [all_node3L, all_node4L, All]

Premises used: Ordnode.all_node4L, Ordnode.All, Ordnode.all_node3L
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
h : ¬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:
simp [all_node3L, all_node4L, All]

Premises used: Ordnode.all_node4L, Ordnode.All, Ordnode.all_node3L
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
rw : All P r.dual ∧ P x ∧ All P l.dual ↔ All P l ∧ P x ∧ All P r
⊢ All P (l.rotateR x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
rw [← all_dual, dual_rotateR, all_rotateL]

Premises used: Ordnode.all_dual, Ordnode.dual_rotateR, Ordnode.all_rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P r.dual ∧ P x ∧ All P l.dual ↔ All P l ∧ P x ∧ All P r

Tactic:
simp [all_dual, and_comm, and_left_comm, and_assoc]

Premises used: Ordnode.all_dual, and_left_comm, and_comm, and_assoc
-- Module: Mathlib.Data.Ordmap.Invariants
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)
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)
⊢ 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

Tactic:
split_ifs
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h : l.size + r.size ≤ 1
⊢ All P (l.node' x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
simp [all_node', all_rotateL, all_rotateR]

Premises used: Ordnode.all_node', Ordnode.all_rotateL, Ordnode.all_rotateR
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : r.size > delta * l.size
⊢ All P (l.rotateL x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
simp [all_node', all_rotateL, all_rotateR]

Premises used: Ordnode.all_node', Ordnode.all_rotateL, Ordnode.all_rotateR
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : l.size > delta * r.size
⊢ All P (l.rotateR x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
simp [all_node', all_rotateL, all_rotateR]

Premises used: Ordnode.all_node', Ordnode.all_rotateL, Ordnode.all_rotateR
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : ¬l.size > delta * r.size
⊢ All P (l.node' x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
simp [all_node', all_rotateL, all_rotateR]

Premises used: Ordnode.all_node', Ordnode.all_rotateL, Ordnode.all_rotateR
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
r' : List α
rw : foldr List.cons l (x :: r.toList) ++ r' = (node size l x r).toList ++ r'
⊢ foldr List.cons (node size l x r) 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]

Premises used: List.append_assoc, List.cons_append, Ordnode.foldr
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
r' : List α
⊢ foldr List.cons l (x :: r.toList) ++ r' = (node size l x r).toList ++ r'

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List α) (toList nil) []

Tactic:
rfl

Premises used: Ordnode.toList, Ordnode.foldr, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
rw : l.toList ++ x :: foldr List.cons r [] = l.toList ++ x :: r.toList
⊢ (node s l x r).toList = l.toList ++ x :: r.toList

Tactic:
rw [toList, foldr, foldr_cons_eq_toList]

Premises used: Ordnode.foldr_cons_eq_toList, Ordnode.toList, Ordnode.foldr
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ l.toList ++ x :: foldr List.cons r [] = l.toList ++ x :: r.toList

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
t : Ordnode α
nil : Any (Eq x) Ordnode.nil ↔ Membership.mem (γ := List α) (toList Ordnode.nil) x
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) (Ordnode.node size l x_1 r) ↔ x ∈ (Ordnode.node size l x_1 r).toList)
⊢ Any (Eq x) t ↔ x ∈ t.toList

Tactic:
induction t
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
⊢ Any (Eq x) nil ↔ Membership.mem (γ := List α) (toList nil) x

Tactic:
simp [Any, *]

Premises used: Ordnode.Any
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
size : ℕ
l : Ordnode α
x_1 : α
r : Ordnode α
l_ih : Any (Eq x) l ↔ x ∈ l.toList
r_ih : 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:
simp [Any, *]

Premises used: Ordnode.Any
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
rw : l.realSize + (r.realSize + 1) = (node size l x r).realSize
⊢ (node size l x r).toList.length = (node size l x r).realSize

Tactic:
rw [toList_node, List.length_append, List.length_cons, length_toList' l,
        length_toList' r]

Premises used: List.length_cons, Ordnode.toList_node, List.length_append
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ l.realSize + (r.realSize + 1) = (node size l x r).realSize

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
t : Ordnode α
h : t.Sized
rw : t.realSize = t.size
rw₁ rw₂ : t.realSize = t.realSize
⊢ t.toList.length = t.size

Tactic:
rw [length_toList', size_eq_realSize h]

Premises used: Ordnode.size_eq_realSize, Ordnode.length_toList'
-- Module: Mathlib.Data.Ordmap.Invariants
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
rw₂ rw₃ : t₂.size = t₂.size
⊢ t₁.size = t₂.size

Tactic:
rw [← length_toList h₁, h, length_toList h₂]

Premises used: Ordnode.length_toList
-- Module: Mathlib.Data.Ordmap.Invariants
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
node :
  ∀ (size : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) (h : (Ordnode.node size l x_1 r).Sized)
    (h_mem : x ∈ Ordnode.node size l x_1 r), 0 < (Ordnode.node size l x_1 r).size
⊢ 0 < t.size

Tactic:
cases t
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : LE α
inst_1 : DecidableLE α
x : α
h : Sized.{u_1} (α := α) nil
h_mem : Membership.mem (γ := Ordnode α) nil x
⊢ 0 < size.{u_1} (α := α) nil

Tactic:
contradiction
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : LE α
inst_1 : DecidableLE α
x : α
h : Sized.{u_1} (α := α) nil
h_mem : Membership.mem (γ := Ordnode α) nil x
⊢ 0 < size.{u_1} (α := α) nil

Tactic:
{ contradiction }
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : LE α
inst_1 : DecidableLE α
x : α
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:
simp [h.1]

Premises used: And.left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : LE α
inst_1 : DecidableLE α
x : α
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:
{ simp [h.1] }

Premises used: And.left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
t : Ordnode α
x : α
rw : t.dual.dual.findMin' x = t.findMin' x
rw₁ rw₂ : t.findMin' x = t.findMin' x
⊢ findMax' x t.dual = t.findMin' x

Tactic:
rw [← findMin'_dual, dual_dual]

Premises used: Ordnode.findMin'_dual, Ordnode.dual_dual
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
t : Ordnode α
rw : t.dual.dual.findMin = t.findMin
rw₁ rw₂ : t.findMin = t.findMin
⊢ t.dual.findMax = t.findMin

Tactic:
rw [← findMin_dual, dual_dual]

Premises used: Ordnode.findMin_dual, Ordnode.dual_dual