mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ls > delta * rs
⊢ (rec nil
        (fun size l x_1 r l_ih r_ih ↦
          rec nil
            (fun size_1 l x_2 r l_ih r_ih ↦
              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).dual =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l x_2 r l_ih r_ih ↦
            if size_1 < ratio * size then
              node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx ll.dual
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx ll.dual))
          lr.dual)
      ll.dual

pp: case neg
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ¬ls > delta * rs
⊢ (node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)).dual =
    node (rs + ls + 1) (node rs rr.dual rx rl.dual) x (node ls lr.dual lx ll.dual)

Tactic:
;

Goal state after:
case pos
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ls > delta * rs
⊢ (rec nil
        (fun size l x_1 r l_ih r_ih ↦
          rec nil
            (fun size_1 l x_2 r l_ih r_ih ↦
              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).dual =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l x_2 r l_ih r_ih ↦
            if size_1 < ratio * size then
              node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx ll.dual
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx ll.dual))
          lr.dual)
      ll.dual

case neg
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ¬ls > delta * rs
⊢ (node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)).dual =
    node (rs + ls + 1) (node rs rr.dual rx rl.dual) x (node ls lr.dual lx ll.dual)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case neg
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ¬ls > delta * rs
⊢ (node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)).dual =
    node (rs + ls + 1) (node rs rr.dual rx rl.dual) x (node ls lr.dual lx ll.dual)

pp: case pos
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ls > delta * rs
⊢ (rec nil
        (fun size l x_1 r l_ih r_ih ↦
          rec nil
            (fun size_1 l x_2 r l_ih r_ih ↦
              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).dual =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l x_2 r l_ih r_ih ↦
            if size_1 < ratio * size then
              node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx ll.dual
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx ll.dual))
          lr.dual)
      ll.dual

Tactic:
;

Goal state after:
case neg
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ¬ls > delta * rs
⊢ (node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)).dual =
    node (rs + ls + 1) (node rs rr.dual rx rl.dual) x (node ls lr.dual lx ll.dual)

case pos
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ls > delta * rs
⊢ (rec nil
        (fun size l x_1 r l_ih r_ih ↦
          rec nil
            (fun size_1 l x_2 r l_ih r_ih ↦
              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).dual =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l x_2 r l_ih r_ih ↦
            if size_1 < ratio * size then
              node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx ll.dual
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx ll.dual))
          lr.dual)
      ll.dual
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f.f.refl.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
this : ⟨a✝⁷, x✝⟩ = ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)

Tactic:
;

Goal state after:
case succ.step.step.f.f.refl.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
this : ⟨a✝⁷, x✝⟩ = ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f.f.refl.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a✝ : F.A
f✝ : F.B a✝ → F.M
h₂ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₂⟩
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝, f✝⟩) = iselect ps (M.mk ⟨a, f₁⟩)
h₁ : M.mk ⟨a, f₁⟩ = M.mk ⟨a, f₁⟩
⊢ (CofixA.intro a✝ fun j ↦ (f✝ j).approx (n + 1)) = CofixA.intro a fun j ↦ (f₁ j).approx (n + 1)

Tactic:
;

Goal state after:
case succ.step.step.f.f.refl.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a✝ : F.A
f✝ : F.B a✝ → F.M
h₂ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₂⟩
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝, f✝⟩) = iselect ps (M.mk ⟨a, f₁⟩)
h₁ : M.mk ⟨a, f₁⟩ = M.mk ⟨a, f₁⟩
⊢ (CofixA.intro a✝ fun j ↦ (f✝ j).approx (n + 1)) = CofixA.intro a fun j ↦ (f₁ j).approx (n + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f.f.refl.refl.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
h₂ : M.mk ⟨a, f₂⟩ = M.mk ⟨a, f₂⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a, f₂⟩) = iselect ps (M.mk ⟨a, f₁⟩)
⊢ (CofixA.intro a fun j ↦ (f₂ j).approx (n + 1)) = CofixA.intro a fun j ↦ (f₁ j).approx (n + 1)

Tactic:
;

Goal state after:
case succ.step.step.f.f.refl.refl.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
h₂ : M.mk ⟨a, f₂⟩ = M.mk ⟨a, f₂⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a, f₂⟩) = iselect ps (M.mk ⟨a, f₁⟩)
⊢ (CofixA.intro a fun j ↦ (f₂ j).approx (n + 1)) = CofixA.intro a fun j ↦ (f₁ j).approx (n + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ ∀ (i : ℕ), x.approx i = y.approx i

Tactic:
;

Goal state after:
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ ∀ (i : ℕ), x.approx i = y.approx i
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (((match l with
            | nil => 0
            | node sz l x r => sz) +
            match m with
            | nil => 0
            | node sz l x r => sz) +
          1 +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      1 =
    (((match l with
          | nil => 0
          | node sz l x r => sz) +
          match m with
          | nil => 0
          | node sz l x r => sz) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      2

Tactic:
;

Goal state after:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (((match l with
            | nil => 0
            | node sz l x r => sz) +
            match m with
            | nil => 0
            | node sz l x r => sz) +
          1 +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      1 =
    (((match l with
          | nil => 0
          | node sz l x r => sz) +
          match m with
          | nil => 0
          | node sz l x r => sz) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      2
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (match l with
        | nil => 0
        | node sz l x r => sz) +
        (((match m with
            | nil => 0
            | node sz l x r => sz) +
            match r with
            | nil => 0
            | node sz l x r => sz) +
          1) +
      1 =
    (((match l with
          | nil => 0
          | node sz l x r => sz) +
          match m with
          | nil => 0
          | node sz l x r => sz) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      2

Tactic:
;

Goal state after:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (match l with
        | nil => 0
        | node sz l x r => sz) +
        (((match m with
            | nil => 0
            | node sz l x r => sz) +
            match r with
            | nil => 0
            | node sz l x r => sz) +
          1) +
      1 =
    (((match l with
          | nil => 0
          | node sz l x r => sz) +
          match m with
          | nil => 0
          | node sz l x r => sz) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      2
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ ¬r.dual.size + l.dual.size ≤ 1

Tactic:
rwa [size_dual, size_dual, add_comm]

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ ((match l with
          | nil => 0
          | node sz l x r => sz) +
          match l✝ with
          | nil => 0
          | node sz l x r => sz) +
        1 +
      (((match r✝ with
          | nil => 0
          | node sz l x r => sz) +
          match r with
          | nil => 0
          | node sz l x r => sz) +
        1) =
    ((match l with
          | nil => 0
          | node sz l x r => sz) +
          (((match l✝ with
              | nil => 0
              | node sz l x r => sz) +
              match r✝ with
              | nil => 0
              | node sz l x r => sz) +
            1) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      1

Tactic:
;

Goal state after:
case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ ((match l with
          | nil => 0
          | node sz l x r => sz) +
          match l✝ with
          | nil => 0
          | node sz l x r => sz) +
        1 +
      (((match r✝ with
          | nil => 0
          | node sz l x r => sz) +
          match r with
          | nil => 0
          | node sz l x r => sz) +
        1) =
    ((match l with
          | nil => 0
          | node sz l x r => sz) +
          (((match l✝ with
              | nil => 0
              | node sz l x r => sz) +
              match r✝ with
              | nil => 0
              | node sz l x r => sz) +
            1) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
h : t.dual.Sized
⊢ t.dual.dual.Sized

Tactic:
;

Goal state after:
α : Type u_1
t : Ordnode α
h : t.dual.Sized
⊢ t.dual.dual.Sized
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
hr : nil.Sized
⊢ (l.rotateL x nil).Sized

pp: case node
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
⊢ (l.rotateL x (node size✝ l✝ x✝ r✝)).Sized

Tactic:
;

Goal state after:
case nil
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
hr : nil.Sized
⊢ (l.rotateL x nil).Sized

case node
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
⊢ (l.rotateL x (node size✝ l✝ x✝ r✝)).Sized
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).Sized

Tactic:
;

Goal state after:
case node
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).Sized
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (l.rotateL x r).Sized

Tactic:
by
  cases r; · exact hl.node' hr
  rw [Ordnode.rotateL_node]; split_ifs
  · exact hl.node3L hr.2.1 hr.2.2
  · exact hl.node4L hr.2.1 hr.2.2

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (r.dual.rotateL x l.dual).Sized

Tactic:
;

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (r.dual.rotateL x l.dual).Sized
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ Valid' o₁
    (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)
    o₂

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ Valid' o₁
    (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)
    o₂
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : 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

Tactic:
;

Goal state after:
α : 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
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : 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

Tactic:
;

Goal state after:
α : 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
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case inr.inl
α : Type u_1
P : α → Prop
x : α
h : P x
⊢ P x

Tactic:
;

Goal state after:
case inr.inl
α : Type u_1
P : α → Prop
x : α
h : P x
⊢ P x
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : 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:
;

Goal state after:
α : 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
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ All P (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝) ↔
    All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝)

Tactic:
;

Goal state after:
case node
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ All P (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝) ↔
    All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : 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:
;

Goal state after:
α : 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
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : 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

Tactic:
;

Goal state after:
α : 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
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H : ∃ l' r', BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
⊢ Valid' o₁ (l.balance' x r) o₂

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H : ∃ l' r', BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
⊢ Valid' o₁ (l.balance' x r) o₂
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : 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:
;

Goal state after:
α : 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'
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ l.toList ++ x :: foldr List.cons r [] = l.toList ++ x :: r.toList

Tactic:
;

Goal state after:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ l.toList ++ x :: foldr List.cons r [] = l.toList ++ x :: r.toList
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
t : Ordnode α
⊢ Any (Eq x) t ↔ x ∈ t.toList

Tactic:
;

Goal state after:
α : Type u_1
x : α
t : Ordnode α
⊢ Any (Eq x) t ↔ x ∈ t.toList
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
⊢ l.realSize + (r.realSize + 1) = (node size✝ l x✝ r).realSize

Tactic:
;

Goal state after:
α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
⊢ l.realSize + (r.realSize + 1) = (node size✝ l x✝ r).realSize
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size = 0
⊢ 2 * 0 ≤ 9 * l.size + 5

Tactic:
;

Goal state after:
case inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size = 0
⊢ 2 * 0 ≤ 9 * l.size + 5