Theorem: MvQPF.Arrow.box_unbox_id (Qpf/PFunctor/Multivariate/Constructions/Arrow.lean)

State before:
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
⊢ box (unbox f) = f
Tactic:
simp[box, unbox]
State after:
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
⊢ { fst := (),
      snd := fun x =>
        match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) x with
        | Fin2.fz =>
          match f with
          | { fst := fst, snd := f } => f Fin2.fz } =
    f

State before:
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
⊢ { fst := (),
      snd := fun x =>
        match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) x with
        | Fin2.fz =>
          match f with
          | { fst := fst, snd := f } => f Fin2.fz } =
    f
Tactic:
apply congrArg
State after:
case h
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
⊢ (fun x =>
      match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) x with
      | Fin2.fz =>
        match f with
        | { fst := fst, snd := f } => f Fin2.fz) =
    f.snd

State before:
case h
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
⊢ (fun x =>
      match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) x with
      | Fin2.fz =>
        match f with
        | { fst := fst, snd := f } => f Fin2.fz) =
    f.snd
Tactic:
funext i
State after:
case h.h
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
i : Fin2 1
⊢ (match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) i with
    | Fin2.fz =>
      match f with
      | { fst := fst, snd := f } => f Fin2.fz) =
    f.snd i

State before:
case h.h
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
i : Fin2 1
⊢ (match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) i with
    | Fin2.fz =>
      match f with
      | { fst := fst, snd := f } => f Fin2.fz) =
    f.snd i
Tactic:
fin_cases i
State after:
case h.h.head
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
⊢ (match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) Fin2.fz with
    | Fin2.fz =>
      match f with
      | { fst := fst, snd := f } => f Fin2.fz) =
    f.snd Fin2.fz

State before:
case h.h.head
α : Type
Γ : TypeVec.{0} 1
f : QpfArrow' α Γ
⊢ (match (motive := (x : Fin2 1) → (ArrowPFunctor α).B () x → Γ x) Fin2.fz with
    | Fin2.fz =>
      match f with
      | { fst := fst, snd := f } => f Fin2.fz) =
    f.snd Fin2.fz
Tactic:
rfl
State after:
no goals