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

Goal state before:
pp: case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ M.mk ⟨a✝, f✝⟩ = M.mk ⟨a✝, ?mp.succ.f.f.intro.y⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : PosNum
d : ZNum
⊢ subNatNat (↑d).natAbs (↑n.pred' % (↑d).natAbs + 1) = -(↑↑n.pred' + 1) % ↑d

Tactic:
rfl

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

Goal state before:
pp: case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ ∀ (i : F.B a✝), Agree' n✝ (f✝¹ i) (f✝ i)

Tactic:
rfl

Goal state after:
case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ ∀ (i : F.B a✝), Agree' n✝ (f✝¹ i) (f✝ i)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a b : ZNum
⊢ (↑a).natAbs.gcd (↑b).natAbs = (↑a).gcd ↑b

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : ZNum
⊢ ↑n % ↑m = 0 ↔ ↑n % ↑m = ↑0

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
x : P.last.M
i : Fin2 n
inst✝ : Inhabited (P.drop.B x.head i)
a : P.last.A := x.head
f : P.last.B x.head → P.last.M := x.children
a✝ : P.last.A
f✝ : P.last.B a✝ → P.last.M
⊢ x.dest = ⟨x.head, f⟩

Tactic:
rfl

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

Goal state before:
pp: case refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
h : x = corecShape P g₀ g₂ b
c : P.drop.B (g₀ b) i
⊢ g₀ b = g₀ b

Tactic:
rfl

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

Goal state before:
pp: case refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
h : x = corecShape P g₀ g₂ b
j : P.last.B (g₀ b)
c : Path P (((PFunctor.M.corec fun b ↦ ⟨g₀ b, g₂ b⟩) ∘ g₂ b) j) i
⊢ g₀ b = g₀ b

Tactic:
rfl

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

Goal state before:
pp: case refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
h : x = corecShape P g₀ g₂ b
j : P.last.B (g₀ b)
h₀ : g₀ b = g₀ b
c : Path P (((PFunctor.M.corec fun b ↦ ⟨g₀ b, g₂ b⟩) ∘ g₂ b) j) i
⊢ ((PFunctor.M.corec fun b ↦ ⟨g₀ b, g₂ b⟩) ∘ g₂ b) j = corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))

Tactic:
rfl

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

Goal state before:
pp: case refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
x : P.last.M
a₁ : P.A
f₁ : P.last.B a₁ → P.last.M
h₁ : x.dest = ⟨a₁, f₁⟩
f' : Path P x ⟹ α
h₂ : x.dest = ⟨a₁, f₁⟩
⊢ dest' P h₁ f' = dest' P h₂ f'

Tactic:
rfl

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

Goal state before:
pp: case cons.refl
F : PFunctor.{uA, uB}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
a✝ : IsPath xs (f i)
h : M.mk ⟨a, f⟩ = M.mk ⟨a, f⟩
⊢ a = a

Tactic:
rfl

Goal state after:
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)

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Goal state after:
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.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
| (TypeVec.id ::: corec P g) ⊚ splitFun (dropFun f) (lastFun f)

Tactic:
appendFun_comp_splitFun

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
| splitFun (TypeVec.id ⊚ dropFun f) (corec P g ∘ lastFun f)
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✝⟩

Tactic:
rfl

Goal state after:
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))
⊢ IsPath ps_tail (x_f i)

Tactic:
rfl

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))
⊢ IsPath ps_tail (x_f i)
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ splitFun (dropFun f)
      ((corec' P (fun b ↦ (g b).fst) (fun b ↦ dropFun (g b).snd) fun b ↦ lastFun (g b).snd) ∘ lastFun f) =
    splitFun (TypeVec.id ⊚ dropFun f) (corec P g ∘ lastFun f)

Tactic:
rfl

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

Goal state before:
pp: F : PFunctor.{uA, uB}
a : F.A
x : F.B a → F.M
i : F.B (M.mk ⟨a, x⟩).head
n : ℕ
⊢ ((M.mk ⟨a, x⟩).children i).approx n = (x (cast ⋯ i)).approx n

Tactic:
rfl

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

Goal state before:
pp: F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps : Path F
a : F.A
f : F.B a → F.M
i : F.B a
⊢ isubtree ps (f (cast ⋯ i)) = isubtree ps (f i)

Tactic:
rfl

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

Goal state before:
pp: case node.nil
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ (casesOn (id (node rs rl rx rr))
        (casesOn (id nil) (Ordnode.singleton x) fun ls ll lx lr ↦
          casesOn (id ll)
            (casesOn lr (node 2 nil x nil) fun size l lrx r ↦ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x))
            fun lls l x_1 r ↦
            casesOn (id lr) (node 3 ll lx (Ordnode.singleton x)) fun lrs lrl lrx lrr ↦
              if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
              else node (ls + 1) (node (lls + lrl.size + 1) ll lx lrl) lrx (node (lrr.size + 1) lrr x nil))
        fun rs_1 l x_1 r ↦
        casesOn (id nil) (node (rs_1 + 1) nil x (node rs rl rx rr)) fun ls ll lx lr ↦
          if ls > delta * rs_1 then
            casesOn (id ll) nil fun lls l x_2 r ↦
              casesOn (id lr) nil fun lrs lrl lrx lrr ↦
                if lrs < ratio * lls then node (ls + rs_1 + 1) ll lx (node (rs_1 + lrs + 1) lr x (node rs rl rx rr))
                else
                  node (ls + rs_1 + 1) (node (lls + lrl.size + 1) ll lx lrl) lrx
                    (node (lrr.size + rs_1 + 1) lrr x (node rs rl rx rr))
          else node (ls + rs_1 + 1) nil x (node rs rl rx rr)).dual =
    casesOn (id (node rs rl rx rr).dual)
      (casesOn (id nil.dual) (Ordnode.singleton x) fun rs rl rx rr ↦
        casesOn (id rr)
          (casesOn rl (node 2 nil x nil.dual) fun size l rlx r ↦
            node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx))
          fun rrs l x_1 r ↦
          casesOn (id rl) (node 3 (Ordnode.singleton x) rx rr) fun rls rll rlx rlr ↦
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
            else node (rs + 1) (node (rll.size + 1) nil x rll) rlx (node (rlr.size + rrs + 1) rlr rx rr))
      fun ls l x_1 r ↦
      casesOn (id nil.dual) (node (ls + 1) (node rs rl rx rr).dual x nil) fun rs_1 rl_1 rx_1 rr_1 ↦
        if rs_1 > delta * ls then
          casesOn (id rr_1) nil fun rrs l x_2 r ↦
            casesOn (id rl_1) nil fun rls rll rlx rlr ↦
              if rls < ratio * rrs then
                node (ls + rs_1 + 1) (node (ls + rls + 1) (node rs rl rx rr).dual x rl_1) rx_1 rr_1
              else
                node (ls + rs_1 + 1) (node (ls + rll.size + 1) (node rs rl rx rr).dual x rll) rlx
                  (node (rlr.size + rrs + 1) rlr rx_1 rr_1)
        else node (ls + rs_1 + 1) (node rs rl rx rr).dual x nil.dual

Tactic:
rfl

Goal state after:
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:
clear h₂

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₃⟩
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.Ordmap.Invariants

Goal state before:
pp: case pos.nil.nil
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
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) nil lx (node (rs + size_1 + 1) nil x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) nil lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            nil)
        nil).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 nil.dual) lx nil.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 nil.dual))
          nil.dual)
      nil.dual

Tactic:
rfl

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

Goal state before:
pp: case pos.nil.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h✝ : ls > delta * rs
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ (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) nil lx (node (rs + size_1 + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) nil lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            (node lrs lrl lrx lrr))
        nil).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 (node lrs lrl lrx lrr).dual) lx
                nil.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 nil.dual))
          (node lrs lrl lrx lrr).dual)
      nil.dual

Tactic:
rfl

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

Goal state before:
pp: case pos.node.nil
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h✝ : ls > delta * rs
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
⊢ (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) (node lls lll llx llr) lx (node (rs + size_1 + 1) nil x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) (node lls lll llx llr) lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            nil)
        (node lls lll llx llr)).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 nil.dual) lx
                (node lls lll llx llr).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 (node lls lll llx llr).dual))
          nil.dual)
      (node lls lll llx llr).dual

Tactic:
rfl

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

Goal state before:
pp: case pos.node.node
α : 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 α
⊢ (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) (node lls lll llx llr) lx
                  (node (rs + size_1 + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) (node lls lll llx llr) lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            (node lrs lrl lrx lrr))
        (node lls lll llx llr)).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 (node lrs lrl lrx lrr).dual) lx
                (node lls lll llx llr).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 (node lls lll llx llr).dual))
          (node lrs lrl lrx lrr).dual)
      (node lls lll llx llr).dual

Tactic:
rfl

Goal state after:
case pos.node.node
α : 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 α
⊢ (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) (node lls lll llx llr) lx
                  (node (rs + size_1 + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) (node lls lll llx llr) lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            (node lrs lrl lrx lrr))
        (node lls lll llx llr)).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 (node lrs lrl lrx lrr).dual) lx
                (node lls lll llx llr).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 (node lls lll llx llr).dual))
          (node lrs lrl lrx lrr).dual)
      (node lls lll llx llr).dual
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

Tactic:
rfl

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

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

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

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

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

Goal state before:
pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).size = l.size + r.size + 1

Tactic:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

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

Goal state before:
pp: α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
⊢ (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]

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.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:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
h : nil.Sized
h_mem : x ∈ nil
⊢ 0 < nil.size

pp: case node
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h : (node size✝ l✝ x✝ r✝).Sized
h_mem : x ∈ node size✝ l✝ x✝ r✝
⊢ 0 < (node size✝ l✝ x✝ r✝).size

Tactic:
· { contradiction }

Goal state after:
case node
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h : (node size✝ l✝ x✝ r✝).Sized
h_mem : x ∈ node size✝ l✝ x✝ r✝
⊢ 0 < (node size✝ l✝ x✝ r✝).size
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
⊢ nil.merge nil = nil

Tactic:
rfl

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

Goal state before:
pp: case node
α : Type u_1
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (node size✝ l✝ x✝ r✝).merge nil = node size✝ l✝ x✝ r✝

Tactic:
rfl

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

Goal state before:
pp: P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
⊢ ∀ (x y : P.M), R x y → x = y

Tactic:
introv h'

Goal state after:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
x y : P.M
h' : R x y
⊢ x = y
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
| ⟨(PFunctor.M.dest ⟨a, f⟩.fst).fst,
    (g ::: fun x ↦ g <$$> x) ⊚
      splitFun (pathDestLeft P ⋯ ⟨a, f⟩.snd) fun x ↦
        ⟨(PFunctor.M.dest ⟨a, f⟩.fst).snd x, pathDestRight P ⋯ ⟨a, f⟩.snd x⟩⟩

Tactic:
appendFun_comp_splitFun

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
| ⟨(PFunctor.M.dest ⟨a, f⟩.fst).fst,
    splitFun (g ⊚ pathDestLeft P ⋯ ⟨a, f⟩.snd)
      ((fun x ↦ g <$$> x) ∘ fun x ↦ ⟨(PFunctor.M.dest ⟨a, f⟩.fst).snd x, pathDestRight P ⋯ ⟨a, f⟩.snd x⟩)⟩