mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case zero.f
F : PFunctor.{uA, uB}
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ Agree' 0 (M.mk ⟨a✝, f✝⟩) (M.mk ⟨a✝, f✝⟩)

pp: case succ.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ Agree' (n✝ + 1) (M.mk ⟨a✝, f✝⟩) (M.mk ⟨a✝, f✝⟩)

Tactic:
<;>

Goal state after:
case zero.f
F : PFunctor.{uA, uB}
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ Agree' 0 (M.mk ⟨a✝, f✝⟩) (M.mk ⟨a✝, f✝⟩)

case succ.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ Agree' (n✝ + 1) (M.mk ⟨a✝, f✝⟩) (M.mk ⟨a✝, f✝⟩)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ M.mk ⟨a✝, f✝⟩ = M.mk ⟨?succ.f.a✝, ?succ.f.x⟩

pp: case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ M.mk ⟨a✝, f✝⟩ = M.mk ⟨?succ.f.a✝, ?succ.f.y⟩

pp: case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ ∀ (i : F.B ?succ.f.a✝), Agree' n✝ (?succ.f.x i) (?succ.f.y i)

pp: case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ F.A

pp: case succ.f.x
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ F.B ?succ.f.a✝ → F.M

pp: case succ.f.y
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ F.B ?succ.f.a✝ → F.M

Tactic:
<;>

Goal state after:
case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ M.mk ⟨a✝, f✝⟩ = M.mk ⟨?succ.f.a✝, ?succ.f.x⟩

case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ M.mk ⟨a✝, f✝⟩ = M.mk ⟨?succ.f.a✝, ?succ.f.y⟩

case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ ∀ (i : F.B ?succ.f.a✝), Agree' n✝ (?succ.f.x i) (?succ.f.y i)

case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ F.A

case succ.f.x
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ F.B ?succ.f.a✝ → F.M

case succ.f.y
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ F.B ?succ.f.a✝ → F.M
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mp
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
⊢ Agree (x.approx n) (y.approx (n + 1)) → Agree' n x y

pp: case mpr
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
⊢ Agree' n x y → Agree (x.approx n) (y.approx (n + 1))

Tactic:
<;>

Goal state after:
case mp
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
⊢ Agree (x.approx n) (y.approx (n + 1)) → Agree' n x y

case mpr
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
⊢ Agree' n x y → Agree (x.approx n) (y.approx (n + 1))
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
⊢ zero.div 0 = 0

pp: case pos
a✝ : PosNum
⊢ (pos a✝).div 0 = 0

pp: case neg
a✝ : PosNum
⊢ (neg a✝).div 0 = 0

Tactic:
<;>

Goal state after:
case zero
⊢ zero.div 0 = 0

case pos
a✝ : PosNum
⊢ (pos a✝).div 0 = 0

case neg
a✝ : PosNum
⊢ (neg a✝).div 0 = 0
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node.nil.node
α : Type u_1
x : α
ls : ℕ
lx : α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ node 3 (Ordnode.singleton x).dual lrx (Ordnode.singleton lx).dual =
    node 3 (Ordnode.singleton x) lrx (Ordnode.singleton lx)

pp: case nil.node.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
⊢ node 3 (Ordnode.singleton x).dual lx (node lls llr.dual llx lll.dual) =
    node 3 (Ordnode.singleton x) lx (node lls llr.dual llx lll.dual)

pp: case nil.node.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ (if lrs < ratio * lls then node (ls + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
      else
        node (ls + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
          (node (lrr.size + 1) lrr x nil)).dual =
    if lrs < ratio * lls then
      node (ls + 1) (node (lrs + 1) nil x (node lrs lrr.dual lrx lrl.dual)) lx (node lls llr.dual llx lll.dual)
    else
      node (ls + 1) (node (lrr.dual.size + 1) nil x lrr.dual) lrx
        (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))

Tactic:
<;>

Goal state after:
case nil.node.nil.node
α : Type u_1
x : α
ls : ℕ
lx : α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ node 3 (Ordnode.singleton x).dual lrx (Ordnode.singleton lx).dual =
    node 3 (Ordnode.singleton x) lrx (Ordnode.singleton lx)

case nil.node.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
⊢ node 3 (Ordnode.singleton x).dual lx (node lls llr.dual llx lll.dual) =
    node 3 (Ordnode.singleton x) lx (node lls llr.dual llx lll.dual)

case nil.node.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ (if lrs < ratio * lls then node (ls + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
      else
        node (ls + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
          (node (lrr.size + 1) lrr x nil)).dual =
    if lrs < ratio * lls then
      node (ls + 1) (node (lrs + 1) nil x (node lrs lrr.dual lrx lrl.dual)) lx (node lls llr.dual llx lll.dual)
    else
      node (ls + 1) (node (lrr.dual.size + 1) nil x lrr.dual) lrx
        (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case pos.h.a
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ M.mk ⟨a, x_f⟩ = M.mk ⟨a, ?pos.h.f✝⟩

pp: case pos.h.a
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ IsPath ps_tail (?pos.h.f✝ i)

pp: case pos.h.f
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ F.B a → F.M

Tactic:
<;>

Goal state after:
case pos.h.a
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ M.mk ⟨a, x_f⟩ = M.mk ⟨a, ?pos.h.f✝⟩

case pos.h.a
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ IsPath ps_tail (?pos.h.f✝ i)

case pos.h.f
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ F.B a → F.M
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
h : lrs < ratio * lls
⊢ (node (ls + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)).dual =
    node (ls + 1) (node (lrs + 1) nil x (node lrs lrr.dual lrx lrl.dual)) lx (node lls llr.dual llx lll.dual)

pp: case neg
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
h : ¬lrs < ratio * lls
⊢ (node (ls + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx (node (lrr.size + 1) lrr x nil)).dual =
    node (ls + 1) (node (lrr.dual.size + 1) nil x lrr.dual) lrx
      (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
h : lrs < ratio * lls
⊢ (node (ls + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)).dual =
    node (ls + 1) (node (lrs + 1) nil x (node lrs lrr.dual lrx lrl.dual)) lx (node lls llr.dual llx lll.dual)

case neg
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
h : ¬lrs < ratio * lls
⊢ (node (ls + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx (node (lrr.size + 1) lrr x nil)).dual =
    node (ls + 1) (node (lrr.dual.size + 1) nil x lrr.dual) lrx
      (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ
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)
x y z : F.M
hx : Agree' (n + 1) z x
hy : Agree' (n + 1) z y
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps x = iselect ps y
⊢ x.approx (n + 1 + 1) = y.approx (n + 1 + 1)

Tactic:
| succ n n_ih =>

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

Goal state before:
pp: case pos
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h✝ : ls > delta * rs
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
h : lrs < ratio * lls
⊢ (node (ls + rs + 1) (node lls lll llx llr) lx
        (node (rs + lrs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))).dual =
    node (rs + ls + 1) (node (rs + lrs + 1) (node rs rr.dual rx rl.dual) x (node lrs lrr.dual lrx lrl.dual)) lx
      (node lls llr.dual llx lll.dual)

pp: case neg
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h✝ : ls > delta * rs
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
h : ¬lrs < ratio * lls
⊢ (node (ls + rs + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
        (node (lrr.size + rs + 1) lrr x (node rs rl rx rr))).dual =
    node (rs + ls + 1) (node (rs + lrr.dual.size + 1) (node rs rr.dual rx rl.dual) x lrr.dual) lrx
      (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h✝ : ls > delta * rs
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
h : lrs < ratio * lls
⊢ (node (ls + rs + 1) (node lls lll llx llr) lx
        (node (rs + lrs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))).dual =
    node (rs + ls + 1) (node (rs + lrs + 1) (node rs rr.dual rx rl.dual) x (node lrs lrr.dual lrx lrl.dual)) lx
      (node lls llr.dual llx lll.dual)

case neg
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h✝ : ls > delta * rs
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
h : ¬lrs < ratio * lls
⊢ (node (ls + rs + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
        (node (lrr.size + rs + 1) lrr x (node rs rl rx rr))).dual =
    node (rs + ls + 1) (node (rs + lrr.dual.size + 1) (node rs rr.dual rx rl.dual) x lrr.dual) lrx
      (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
x y : P.M α
r : R x y
⊢ x = y

Tactic:
by
  obtain ⟨a₁, f₁⟩ := x
  obtain ⟨a₂, f₂⟩ := y
  dsimp [mp] at *
  have : a₁ = a₂ := by
    refine
      PFunctor.M.bisim (fun a₁ a₂ => ∃ x y, R x y ∧ x.1 = a₁ ∧ y.1 = a₂) ?_ _ _
        ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
    rintro _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
    rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h'⟩
    rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
    rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', _, rfl⟩
    rw [e₁', e₂']
    exact ⟨_, _, _, rfl, rfl, fun b => ⟨_, _, h' b, rfl, rfl⟩⟩
  subst this
  congr with (i p)
  induction p with (
    obtain ⟨a', f', f₁', f₂', e₁, e₂, h''⟩ := h _ _ r
    obtain ⟨g₁', e₁', rfl, rfl⟩ := M.bisim_lemma P e₁
    obtain ⟨g₂', e₂', e₃, rfl⟩ := M.bisim_lemma P e₂
    cases h'.symm.trans e₁'
    cases h'.symm.trans e₂')
  | root x a f h' i c =>
    exact congr_fun (congr_fun e₃ i) c
  | child x a f h' i c p IH =>
    exact IH _ _ (h'' _)

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx : P.B ax ⟹ α ::: P.M α
ay : P.A
fy : P.B ay ⟹ α ::: P.M α
h : (TypeVec.id ::: Quot.mk R) <$$> ⟨ax, fx⟩ = (TypeVec.id ::: Quot.mk R) <$$> ⟨ay, fy⟩
⊢ ∃ a f f₁ f₂, ⟨ax, fx⟩ = ⟨a, splitFun f f₁⟩ ∧ ⟨ay, fy⟩ = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)

Tactic:
rw [map_eq, map_eq] at h

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx : P.B ax ⟹ α ::: P.M α
ay : P.A
fy : P.B ay ⟹ α ::: P.M α
h : ⟨ax, (TypeVec.id ::: Quot.mk R) ⊚ fx⟩ = ⟨ay, (TypeVec.id ::: Quot.mk R) ⊚ fy⟩
⊢ ∃ a f f₁ f₂, ⟨ax, fx⟩ = ⟨a, splitFun f f₁⟩ ∧ ⟨ay, fy⟩ = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case inl
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
a' : F.A
i : F.B a'
hh : IsPath (⟨a', i⟩ :: ps) (M.mk ⟨a, f⟩)
⊢ a = a'

pp: case inr
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
a' : F.A
i : F.B a'
hh : IsPath (⟨a', i⟩ :: ps) (M.mk ⟨a, f'⟩)
⊢ a = a'

Tactic:
<;>

Goal state after:
case inl
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
a' : F.A
i : F.B a'
hh : IsPath (⟨a', i⟩ :: ps) (M.mk ⟨a, f⟩)
⊢ a = a'

case inr
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
a' : F.A
i : F.B a'
hh : IsPath (⟨a', i⟩ :: ps) (M.mk ⟨a, f'⟩)
⊢ a = a'
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case inl.refl
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩)
⊢ a = a

pp: case inr.refl
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
⊢ a = a

Tactic:
<;>

Goal state after:
case inl.refl
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩)
⊢ a = a

case inr.refl
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
⊢ a = a
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x : α
hm : nil.Sized
⊢ (l.rotateL x nil).size = l.size + nil.size + 1

pp: case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ (l.rotateL x (node size✝ l✝ x✝ r✝)).size = l.size + (node size✝ l✝ x✝ r✝).size + 1

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
l : Ordnode α
x : α
hm : nil.Sized
⊢ (l.rotateL x nil).size = l.size + nil.size + 1

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

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
h✝ : l✝.size < ratio * r✝.size
⊢ (l.node3L x l✝ x✝ r✝).size = l.size + (l✝.size + r✝.size + 1) + 1

pp: case neg
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
h✝ : ¬l✝.size < ratio * r✝.size
⊢ (l.node4L x l✝ x✝ r✝).size = l.size + (l✝.size + r✝.size + 1) + 1

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
h✝ : l✝.size < ratio * r✝.size
⊢ (l.node3L x l✝ x✝ r✝).size = l.size + (l✝.size + r✝.size + 1) + 1

case neg
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
h✝ : ¬l✝.size < ratio * r✝.size
⊢ (l.node4L x l✝ x✝ r✝).size = l.size + (l✝.size + r✝.size + 1) + 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
h✝ : l✝.size < ratio * r✝.size
⊢ l.size + l✝.size + r✝.size + 1 = l.size + (l✝.size + r✝.size + 1)

pp: case neg
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
h✝ : ¬l✝.size < ratio * r✝.size
⊢ l.size + l✝.size + r✝.size + 1 = l.size + (l✝.size + r✝.size + 1)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
h✝ : l✝.size < ratio * r✝.size
⊢ l.size + l✝.size + r✝.size + 1 = l.size + (l✝.size + r✝.size + 1)

case neg
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
h✝ : ¬l✝.size < ratio * r✝.size
⊢ l.size + l✝.size + r✝.size + 1 = l.size + (l✝.size + r✝.size + 1)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inl
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
H1 : BalancedSz l' r.size
⊢ r.size ≤ 3 * (l.size + 1)

pp: case inr
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
H1 : BalancedSz l.size r'
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
<;>

Goal state after:
case inl
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
H1 : BalancedSz l' r.size
⊢ r.size ≤ 3 * (l.size + 1)

case inr
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
H1 : BalancedSz l.size r'
⊢ r.size ≤ 3 * (l.size + 1)
Module: Mathlib.Data.Ordmap.Invariants

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

pp: case node
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ All P (l.node4L x (node size✝ l✝ x✝ r✝) y r) ↔ All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝) ∧ P y ∧ All P r

Tactic:
<;>

Goal state after:
case nil
α : 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

case node
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ All P (l.node4L x (node size✝ l✝ x✝ r✝) y r) ↔ All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝) ∧ P y ∧ All P r