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

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

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

State before:
F : TypeFun Nat.zero
⊢ ofCurriedAux (curriedAux F) = F
Tactic:
case zero =>
  funext x;
  simp [curriedAux, ofCurriedAux, Matrix.vecEmpty]
  congr
  funext i
  contradiction
State after:
no goals

State before:
n : ℕ
F : TypeFun (Nat.succ n)
⊢ ofCurriedAux (curriedAux F) = F
Tactic:
case succ n => {
  induction n;
  case zero => {
    funext x;
    simp [curriedAux, ofCurriedAux];
    apply congrArg;
    funext i;
    cases i;
    . simp [Vec.append1, OfNat.ofNat]
    . contradiction
  }
  case succ _ ih => {
    funext x;
    simp [ofCurriedAux, curriedAux];
    let F' := fun α => F (α ::: x.last);
    have : F x = F' x.drop := by simp [F']
    rw [this]
    rw [@ih F']
  }
}
State after:
no goals

State before:
F : TypeFun Nat.zero
⊢ ofCurriedAux (curriedAux F) = F
Tactic:
funext x
State after:
case h
F : TypeFun Nat.zero
x : TypeVec.{u_1} Nat.zero
⊢ ofCurriedAux (curriedAux F) x = F x

State before:
case h
F : TypeFun Nat.zero
x : TypeVec.{u_1} Nat.zero
⊢ ofCurriedAux (curriedAux F) x = F x
Tactic:
simp [curriedAux, ofCurriedAux, Matrix.vecEmpty]
State after:
case h
F : TypeFun Nat.zero
x : TypeVec.{u_1} Nat.zero
⊢ F Vec.nil = F x

State before:
case h
F : TypeFun Nat.zero
x : TypeVec.{u_1} Nat.zero
⊢ F Vec.nil = F x
Tactic:
congr
State after:
case h.e_a
F : TypeFun Nat.zero
x : TypeVec.{u_1} Nat.zero
⊢ Vec.nil = x

State before:
case h.e_a
F : TypeFun Nat.zero
x : TypeVec.{u_1} Nat.zero
⊢ Vec.nil = x
Tactic:
funext i
State after:
case h.e_a.h
F : TypeFun Nat.zero
x : TypeVec.{u_1} Nat.zero
i : Fin2 0
⊢ Vec.nil i = x i

State before:
case h.e_a.h
F : TypeFun Nat.zero
x : TypeVec.{u_1} Nat.zero
i : Fin2 0
⊢ Vec.nil i = x i
Tactic:
contradiction
State after:
no goals

State before:
n : ℕ
F : TypeFun (Nat.succ n)
⊢ ofCurriedAux (curriedAux F) = F
Tactic:
induction n
State after:
case zero
F : TypeFun (Nat.succ Nat.zero)
⊢ ofCurriedAux (curriedAux F) = F

case succ
n✝ : ℕ
n_ih✝ : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
⊢ ofCurriedAux (curriedAux F) = F

State before:
F : TypeFun (Nat.succ Nat.zero)
⊢ ofCurriedAux (curriedAux F) = F
Tactic:
case zero => {
  funext x;
  simp [curriedAux, ofCurriedAux];
  apply congrArg;
  funext i;
  cases i;
  . simp [Vec.append1, OfNat.ofNat]
  . contradiction
}
State after:
no goals

State before:
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
⊢ ofCurriedAux (curriedAux F) = F
Tactic:
case succ _ ih => {
  funext x;
  simp [ofCurriedAux, curriedAux];
  let F' := fun α => F (α ::: x.last);
  have : F x = F' x.drop := by simp [F']
  rw [this]
  rw [@ih F']
}
State after:
no goals

State before:
F : TypeFun (Nat.succ Nat.zero)
⊢ ofCurriedAux (curriedAux F) = F
Tactic:
funext x
State after:
case h
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
⊢ ofCurriedAux (curriedAux F) x = F x

State before:
case h
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
⊢ ofCurriedAux (curriedAux F) x = F x
Tactic:
simp [curriedAux, ofCurriedAux]
State after:
case h
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
⊢ F (Vec.append1 Vec.nil (x 0)) = F x

State before:
case h
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
⊢ F (Vec.append1 Vec.nil (x 0)) = F x
Tactic:
apply congrArg
State after:
case h.h
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
⊢ Vec.append1 Vec.nil (x 0) = x

State before:
case h.h
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
⊢ Vec.append1 Vec.nil (x 0) = x
Tactic:
funext i
State after:
case h.h.h
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
i : Fin2 (Nat.succ 0)
⊢ Vec.append1 Vec.nil (x 0) i = x i

State before:
case h.h.h
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
i : Fin2 (Nat.succ 0)
⊢ Vec.append1 Vec.nil (x 0) i = x i
Tactic:
cases i
State after:
case h.h.h.fz
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
⊢ Vec.append1 Vec.nil (x 0) Fin2.fz = x Fin2.fz

case h.h.h.fs
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
a✝ : Fin2 0
⊢ Vec.append1 Vec.nil (x 0) (Fin2.fs a✝) = x (Fin2.fs a✝)

State before:
case h.h.h.fz
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
⊢ Vec.append1 Vec.nil (x 0) Fin2.fz = x Fin2.fz

case h.h.h.fs
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
a✝ : Fin2 0
⊢ Vec.append1 Vec.nil (x 0) (Fin2.fs a✝) = x (Fin2.fs a✝)
Tactic:
. simp [Vec.append1, OfNat.ofNat]
State after:
case h.h.h.fs
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
a✝ : Fin2 0
⊢ Vec.append1 Vec.nil (x 0) (Fin2.fs a✝) = x (Fin2.fs a✝)

State before:
case h.h.h.fs
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
a✝ : Fin2 0
⊢ Vec.append1 Vec.nil (x 0) (Fin2.fs a✝) = x (Fin2.fs a✝)
Tactic:
. contradiction
State after:
no goals

State before:
case h.h.h.fz
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
⊢ Vec.append1 Vec.nil (x 0) Fin2.fz = x Fin2.fz
Tactic:
simp [Vec.append1, OfNat.ofNat]
State after:
no goals

State before:
case h.h.h.fs
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
a✝ : Fin2 0
⊢ Vec.append1 Vec.nil (x 0) (Fin2.fs a✝) = x (Fin2.fs a✝)
Tactic:
contradiction
State after:
no goals

State before:
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
⊢ ofCurriedAux (curriedAux F) = F
Tactic:
funext x
State after:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
⊢ ofCurriedAux (curriedAux F) x = F x

State before:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
⊢ ofCurriedAux (curriedAux F) x = F x
Tactic:
simp [ofCurriedAux, curriedAux]
State after:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F x

State before:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F x
Tactic:
let F' := fun α => F (α ::: x.last)
State after:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
F' : TypeVec.{u_1} (n✝ + 1) → Type u_2 := fun α => F (α ::: TypeVec.last x)
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F x

State before:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
F' : TypeVec.{u_1} (n✝ + 1) → Type u_2 := fun α => F (α ::: TypeVec.last x)
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F x
Tactic:
have : F x = F' x.drop := by simp [F']
State after:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
F' : TypeVec.{u_1} (n✝ + 1) → Type u_2 := fun α => F (α ::: TypeVec.last x)
this : F x = F' (TypeVec.drop x)
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F x

State before:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
F' : TypeVec.{u_1} (n✝ + 1) → Type u_2 := fun α => F (α ::: TypeVec.last x)
this : F x = F' (TypeVec.drop x)
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F x
Tactic:
rw [this]
State after:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
F' : TypeVec.{u_1} (n✝ + 1) → Type u_2 := fun α => F (α ::: TypeVec.last x)
this : F x = F' (TypeVec.drop x)
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F' (TypeVec.drop x)

State before:
case h
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
F' : TypeVec.{u_1} (n✝ + 1) → Type u_2 := fun α => F (α ::: TypeVec.last x)
this : F x = F' (TypeVec.drop x)
⊢ ofCurriedAux (curriedAux fun αs => F (αs ::: TypeVec.last x)) (TypeVec.drop x) = F' (TypeVec.drop x)
Tactic:
rw [@ih F']
State after:
no goals

State before:
n✝ : ℕ
ih : ∀ {F : TypeFun (Nat.succ n✝)}, ofCurriedAux (curriedAux F) = F
F : TypeFun (Nat.succ (Nat.succ n✝))
x : TypeVec.{u_1} (Nat.succ (Nat.succ n✝))
F' : TypeVec.{u_1} (n✝ + 1) → Type u_2 := fun α => F (α ::: TypeVec.last x)
⊢ F x = F' (TypeVec.drop x)
Tactic:
simp [F']
State after:
no goals