Theorem: TypeFun.curriedAux_ofCurriedAux_involution (Qpf/Util/TypeFun.lean)

State before:
n : ℕ
F : CurriedTypeFun n
⊢ curriedAux (ofCurriedAux F) = F
Tactic:
cases n
State after:
case zero
F : CurriedTypeFun Nat.zero
⊢ curriedAux (ofCurriedAux F) = F

case succ
n✝ : ℕ
F : CurriedTypeFun (Nat.succ n✝)
⊢ curriedAux (ofCurriedAux F) = F

State before:
F : CurriedTypeFun Nat.zero
⊢ curriedAux (ofCurriedAux F) = F
Tactic:
case zero => simp [curriedAux, ofCurriedAux]
State after:
no goals

State before:
n : ℕ
F : CurriedTypeFun (Nat.succ n)
⊢ curriedAux (ofCurriedAux F) = F
Tactic:
case succ n => {
  induction n
  <;> simp [curriedAux, ofCurriedAux, Vec.append1]
  case succ _ ih => {
    funext a;
    apply @ih (F a);
  }
}
State after:
no goals

State before:
F : CurriedTypeFun Nat.zero
⊢ curriedAux (ofCurriedAux F) = F
Tactic:
simp [curriedAux, ofCurriedAux]
State after:
no goals

State before:
n : ℕ
F : CurriedTypeFun (Nat.succ n)
⊢ curriedAux (ofCurriedAux F) = F
Tactic:
induction n
<;> simp [curriedAux, ofCurriedAux, Vec.append1]
State after:
case succ
n✝ : ℕ
n_ih✝ : ∀ {F : CurriedTypeFun (Nat.succ n✝)}, curriedAux (ofCurriedAux F) = F
F : CurriedTypeFun (Nat.succ (Nat.succ n✝))
⊢ (fun a => curriedAux fun αs => ofCurriedAux (F (TypeVec.last (αs ::: a))) αs) = F

State before:
n✝ : ℕ
ih : ∀ {F : CurriedTypeFun (Nat.succ n✝)}, curriedAux (ofCurriedAux F) = F
F : CurriedTypeFun (Nat.succ (Nat.succ n✝))
⊢ (fun a => curriedAux fun αs => ofCurriedAux (F (TypeVec.last (αs ::: a))) αs) = F
Tactic:
case succ _ ih => {
  funext a;
  apply @ih (F a);
}
State after:
no goals

State before:
n✝ : ℕ
ih : ∀ {F : CurriedTypeFun (Nat.succ n✝)}, curriedAux (ofCurriedAux F) = F
F : CurriedTypeFun (Nat.succ (Nat.succ n✝))
⊢ (fun a => curriedAux fun αs => ofCurriedAux (F (TypeVec.last (αs ::: a))) αs) = F
Tactic:
funext a
State after:
case h
n✝ : ℕ
ih : ∀ {F : CurriedTypeFun (Nat.succ n✝)}, curriedAux (ofCurriedAux F) = F
F : CurriedTypeFun (Nat.succ (Nat.succ n✝))
a : Type u_1
⊢ (curriedAux fun αs => ofCurriedAux (F (TypeVec.last (αs ::: a))) αs) = F a

State before:
case h
n✝ : ℕ
ih : ∀ {F : CurriedTypeFun (Nat.succ n✝)}, curriedAux (ofCurriedAux F) = F
F : CurriedTypeFun (Nat.succ (Nat.succ n✝))
a : Type u_1
⊢ (curriedAux fun αs => ofCurriedAux (F (TypeVec.last (αs ::: a))) αs) = F a
Tactic:
apply @ih (F a)
State after:
no goals