internlm/Lean-Github huggingface dataset:
Theorem: Vec.ofList_toList_iso
Proof state before:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n} (i : Fin2 (List.length (toList v))), HEq (ofList (toList v) i) (v (cast ⋯ i))
v : Vec α (Nat.succ n)
i : Fin2 (Nat.add (List.length (toList (drop v))) 0)
⊢ Fin2 n = Fin2 (Nat.add (List.length (toList (drop v))) 0)
Tactic:
apply congrArg
Proof state after:
case h
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n} (i : Fin2 (List.length (toList v))), HEq (ofList (toList v) i) (v (cast ⋯ i))
v : Vec α (Nat.succ n)
i : Fin2 (Nat.add (List.length (toList (drop v))) 0)
⊢ n = Nat.add (List.length (toList (drop v))) 0
Theorem: Vec.ofList_toList_iso
Proof state before:
case h
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n} (i : Fin2 (List.length (toList v))), HEq (ofList (toList v) i) (v (cast ⋯ i))
v : Vec α (Nat.succ n)
i : Fin2 (Nat.add (List.length (toList (drop v))) 0)
⊢ n = Nat.add (List.length (toList (drop v))) 0
Tactic:
simp
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso
Proof state before:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n} (i : Fin2 (List.length (toList v))), HEq (ofList (toList v) i) (v (cast ⋯ i))
v : Vec α (Nat.succ n)
i : Fin2 (Nat.add (List.length (toList (drop v))) 0)
⊢ Fin2 n → Fin2 (Nat.succ n) = Fin2 (Nat.succ (List.length (toList (drop v))))
Tactic:
intro _
Proof state after:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n} (i : Fin2 (List.length (toList v))), HEq (ofList (toList v) i) (v (cast ⋯ i))
v : Vec α (Nat.succ n)
i : Fin2 (Nat.add (List.length (toList (drop v))) 0)
a✝ : Fin2 n
⊢ Fin2 (Nat.succ n) = Fin2 (Nat.succ (List.length (toList (drop v))))
Theorem: Vec.ofList_toList_iso
Proof state before:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n} (i : Fin2 (List.length (toList v))), HEq (ofList (toList v) i) (v (cast ⋯ i))
v : Vec α (Nat.succ n)
i : Fin2 (Nat.add (List.length (toList (drop v))) 0)
a✝ : Fin2 n
⊢ Fin2 (Nat.succ n) = Fin2 (Nat.succ (List.length (toList (drop v))))
Tactic:
apply congrArg
Proof state after:
case h
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n} (i : Fin2 (List.length (toList v))), HEq (ofList (toList v) i) (v (cast ⋯ i))
v : Vec α (Nat.succ n)
i : Fin2 (Nat.add (List.length (toList (drop v))) 0)
a✝ : Fin2 n
⊢ Nat.succ n = Nat.succ (List.length (toList (drop v)))
Theorem: Vec.ofList_toList_iso
Proof state before:
case h
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n} (i : Fin2 (List.length (toList v))), HEq (ofList (toList v) i) (v (cast ⋯ i))
v : Vec α (Nat.succ n)
i : Fin2 (Nat.add (List.length (toList (drop v))) 0)
a✝ : Fin2 n
⊢ Nat.succ n = Nat.succ (List.length (toList (drop v)))
Tactic:
simp
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso
Proof state before:
case H₂.H₁.H₃
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n} (i : Fin2 (List.length (toList v))), HEq (ofList (toList v) i) (v (cast ⋯ i))
v : Vec α (Nat.succ n)
i : Fin2 (Nat.add (List.length (toList (drop v))) 0)
⊢ ℕ = ℕ
Tactic:
try solve | intros; rfl
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso
Proof state before:
case H₂.H₁.H₃
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n} (i : Fin2 (List.length (toList v))), HEq (ofList (toList v) i) (v (cast ⋯ i))
v : Vec α (Nat.succ n)
i : Fin2 (Nat.add (List.length (toList (drop v))) 0)
⊢ ℕ = ℕ
Tactic:
solve | intros; rfl
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso
Proof state before:
case H₂.H₁.H₄
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n} (i : Fin2 (List.length (toList v))), HEq (ofList (toList v) i) (v (cast ⋯ i))
v : Vec α (Nat.succ n)
i : Fin2 (Nat.add (List.length (toList (drop v))) 0)
⊢ ∀ (a : ℕ), (Fin2 a → Fin2 (Nat.succ a)) = (Fin2 (cast ?H₂.H₁.H₃ a) → Fin2 (Nat.succ (cast ?H₂.H₁.H₃ a)))
Tactic:
intros
Proof state after:
case H₂.H₁.H₄
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n} (i : Fin2 (List.length (toList v))), HEq (ofList (toList v) i) (v (cast ⋯ i))
v : Vec α (Nat.succ n)
i : Fin2 (Nat.add (List.length (toList (drop v))) 0)
a✝ : ℕ
⊢ (Fin2 a✝ → Fin2 (Nat.succ a✝)) = (Fin2 (cast ?H₂.H₁.H₃ a✝) → Fin2 (Nat.succ (cast ?H₂.H₁.H₃ a✝)))
Theorem: Vec.ofList_toList_iso
Proof state before:
case H₂.H₁.H₃
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n} (i : Fin2 (List.length (toList v))), HEq (ofList (toList v) i) (v (cast ⋯ i))
v : Vec α (Nat.succ n)
i : Fin2 (Nat.add (List.length (toList (drop v))) 0)
⊢ ℕ = ℕ
Tactic:
rfl
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso'
Proof state before:
α : Type ?u.9329
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
⊢ PFin2 (List.length (toList v)) = PFin2 n
Tactic:
rw[toList_length_eq_n]
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso'
Proof state before:
α : Type u_1
n : ℕ
v : Vec α n
⊢ HEq (fun j => ofList (toList v) (PFin2.toFin2 j)) fun j => v (PFin2.toFin2 (cast ⋯ j))
Tactic:
apply HEq.funext
Proof state after:
case type_eq
α : Type u_1
n : ℕ
v : Vec α n
⊢ (fun x => (fun x => α) (PFin2.toFin2 x)) = fun x => (fun x => α) (PFin2.toFin2 (cast ⋯ x))

case a
α : Type u_1
n : ℕ
v : Vec α n
⊢ ∀ (x : PFin2 (List.length (toList v))), HEq (ofList (toList v) (PFin2.toFin2 x)) (v (PFin2.toFin2 (cast ⋯ x)))
Theorem: Vec.ofList_toList_iso'
Proof state before:
case type_eq
α : Type u_1
n : ℕ
v : Vec α n
⊢ (fun x => (fun x => α) (PFin2.toFin2 x)) = fun x => (fun x => α) (PFin2.toFin2 (cast ⋯ x))

case a
α : Type u_1
n : ℕ
v : Vec α n
⊢ ∀ (x : PFin2 (List.length (toList v))), HEq (ofList (toList v) (PFin2.toFin2 x)) (v (PFin2.toFin2 (cast ⋯ x)))
Tactic:
. rfl
Proof state after:
case a
α : Type u_1
n : ℕ
v : Vec α n
⊢ ∀ (x : PFin2 (List.length (toList v))), HEq (ofList (toList v) (PFin2.toFin2 x)) (v (PFin2.toFin2 (cast ⋯ x)))
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a
α : Type u_1
n : ℕ
v : Vec α n
⊢ ∀ (x : PFin2 (List.length (toList v))), HEq (ofList (toList v) (PFin2.toFin2 x)) (v (PFin2.toFin2 (cast ⋯ x)))
Tactic:
intro j
Proof state after:
case a
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
⊢ HEq (ofList (toList v) (PFin2.toFin2 j)) (v (PFin2.toFin2 (cast ⋯ j)))
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
⊢ HEq (ofList (toList v) (PFin2.toFin2 j)) (v (PFin2.toFin2 (cast ⋯ j)))
Tactic:
have n_eq : (toList v).length = n := toList_length_eq_n
Proof state after:
case a
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ HEq (ofList (toList v) (PFin2.toFin2 j)) (v (PFin2.toFin2 (cast ⋯ j)))
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ HEq (ofList (toList v) (PFin2.toFin2 j)) (v (PFin2.toFin2 (cast ⋯ j)))
Tactic:
apply hcongr
Proof state after:
case a.H₁
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ HEq (ofList (toList v)) v

case a.H₂
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ HEq (PFin2.toFin2 j) (PFin2.toFin2 (cast ⋯ j))

case a.H₄
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ ∀ (a : Fin2 (List.length (toList v))), (fun x => α) a = (fun x => α) (cast ?a.H₃✝ a)

case a.H₃
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ Fin2 (List.length (toList v)) = Fin2 n
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a.H₁
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ HEq (ofList (toList v)) v

case a.H₂
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ HEq (PFin2.toFin2 j) (PFin2.toFin2 (cast ⋯ j))

case a.H₄
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ ∀ (a : Fin2 (List.length (toList v))), (fun x => α) a = (fun x => α) (cast ?a.H₃✝ a)

case a.H₃
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ Fin2 (List.length (toList v)) = Fin2 n
Tactic:
. apply ofList_toList_iso
Proof state after:
case a.H₂
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ HEq (PFin2.toFin2 j) (PFin2.toFin2 (cast ⋯ j))

case a.H₄
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ ∀ (a : Fin2 (List.length (toList v))), (fun x => α) a = (fun x => α) (cast ?a.H₃✝ a)

case a.H₃
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ Fin2 (List.length (toList v)) = Fin2 n
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a.H₂
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ HEq (PFin2.toFin2 j) (PFin2.toFin2 (cast ⋯ j))

case a.H₄
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ ∀ (a : Fin2 (List.length (toList v))), (fun x => α) a = (fun x => α) (cast ?a.H₃✝ a)

case a.H₃
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ Fin2 (List.length (toList v)) = Fin2 n
Tactic:
. intros
  apply hcongr <;> intros <;> (try rw[n_eq])
  . simp_heq
Proof state after:
case a.H₄
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ ∀ (a : Fin2 (List.length (toList v))), (fun x => α) a = (fun x => α) (cast ?a.H₃✝ a)

case a.H₃
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ Fin2 (List.length (toList v)) = Fin2 n
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a.H₄
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ ∀ (a : Fin2 (List.length (toList v))), (fun x => α) a = (fun x => α) (cast ?a.H₃✝ a)

case a.H₃
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ Fin2 (List.length (toList v)) = Fin2 n
Tactic:
. intros; simp
Proof state after:
case a.H₃
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ Fin2 (List.length (toList v)) = Fin2 n
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a.H₃
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ Fin2 (List.length (toList v)) = Fin2 n
Tactic:
. rw[n_eq]
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso'
Proof state before:
case type_eq
α : Type u_1
n : ℕ
v : Vec α n
⊢ (fun x => (fun x => α) (PFin2.toFin2 x)) = fun x => (fun x => α) (PFin2.toFin2 (cast ⋯ x))
Tactic:
rfl
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a.H₁
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ HEq (ofList (toList v)) v
Tactic:
apply ofList_toList_iso
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a.H₂
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ HEq (PFin2.toFin2 j) (PFin2.toFin2 (cast ⋯ j))
Tactic:
apply hcongr <;> intros <;> (try rw[n_eq])
Proof state after:
case a.H₂.H₂
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ HEq j (cast ⋯ j)
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a.H₂.H₂
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ HEq j (cast ⋯ j)
Tactic:
. simp_heq
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a.H₂.H₃
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ PFin2 (List.length (toList v)) = PFin2 n
Tactic:
try rw[n_eq]
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a.H₂.H₃
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ PFin2 (List.length (toList v)) = PFin2 n
Tactic:
rw[n_eq]
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a.H₂.H₂
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ HEq j (cast ⋯ j)
Tactic:
simp_heq
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a.H₄
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ ∀ (a : Fin2 (List.length (toList v))), (fun x => α) a = (fun x => α) (cast ?a.H₃✝ a)
Tactic:
intros
Proof state after:
case a.H₄
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
a✝ : Fin2 (List.length (toList v))
⊢ (fun x => α) a✝ = (fun x => α) (cast ?a.H₃✝ a✝)
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a.H₄
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
a✝ : Fin2 (List.length (toList v))
⊢ (fun x => α) a✝ = (fun x => α) (cast ?a.H₃✝ a✝)
Tactic:
simp
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso'
Proof state before:
case a.H₃
α : Type u_1
n : ℕ
v : Vec α n
j : PFin2 (List.length (toList v))
n_eq : List.length (toList v) = n
⊢ Fin2 (List.length (toList v)) = Fin2 n
Tactic:
rw[n_eq]
Proof state after:
no goals
Theorem: Vec.toList_ofList_iso
Proof state before:
α : Type u_1
as : List α
⊢ toList (ofList as) = as
Tactic:
induction as
Proof state after:
case nil
α : Type u_1
⊢ toList (ofList []) = []

case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : toList (ofList tail✝) = tail✝
⊢ toList (ofList (head✝ :: tail✝)) = head✝ :: tail✝
Theorem: Vec.toList_ofList_iso
Proof state before:
α : Type u_1
⊢ toList (ofList []) = []
Tactic:
case nil          => rfl
Proof state after:
no goals
Theorem: Vec.toList_ofList_iso
Proof state before:
α : Type u_1
a : α
as : List α
ih : toList (ofList as) = as
⊢ toList (ofList (a :: as)) = a :: as
Tactic:
case cons a as ih =>
  simp only [toList, ofList, append1, last, DVec.last, drop_append1', ih]
Proof state after:
no goals
Theorem: Vec.toList_ofList_iso
Proof state before:
α : Type u_1
⊢ toList (ofList []) = []
Tactic:
rfl
Proof state after:
no goals
Theorem: Vec.toList_ofList_iso
Proof state before:
α : Type u_1
a : α
as : List α
ih : toList (ofList as) = as
⊢ toList (ofList (a :: as)) = a :: as
Tactic:
simp only [toList, ofList, append1, last, DVec.last, drop_append1', ih]
Proof state after:
no goals
Theorem: TypeFun.reverseArgs_involution
Proof state before:
n : ℕ
F : TypeFun n
⊢ reverseArgs (reverseArgs F) = F
Tactic:
unfold reverseArgs
Proof state after:
n : ℕ
F : TypeFun n
⊢ (fun α => F (Vec.reverse (Vec.reverse α))) = F
Theorem: TypeFun.reverseArgs_involution
Proof state before:
n : ℕ
F : TypeFun n
⊢ (fun α => F (Vec.reverse (Vec.reverse α))) = F
Tactic:
simp only [Vec.reverse_involution]
Proof state after:
no goals
Theorem: TypeFun.curriedAux_ofCurriedAux_involution
Proof state before:
n : ℕ
F : CurriedTypeFun n
⊢ curriedAux (ofCurriedAux F) = F
Tactic:
cases n
Proof state after:
case zero
F : CurriedTypeFun Nat.zero
⊢ curriedAux (ofCurriedAux F) = F

case succ
n✝ : ℕ
F : CurriedTypeFun (Nat.succ n✝)
⊢ curriedAux (ofCurriedAux F) = F
Theorem: TypeFun.curriedAux_ofCurriedAux_involution
Proof state before:
F : CurriedTypeFun Nat.zero
⊢ curriedAux (ofCurriedAux F) = F
Tactic:
case zero => simp [curriedAux, ofCurriedAux]
Proof state after:
no goals
Theorem: TypeFun.curriedAux_ofCurriedAux_involution
Proof 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);
  }
}
Proof state after:
no goals
Theorem: TypeFun.curriedAux_ofCurriedAux_involution
Proof state before:
F : CurriedTypeFun Nat.zero
⊢ curriedAux (ofCurriedAux F) = F
Tactic:
simp [curriedAux, ofCurriedAux]
Proof state after:
no goals
Theorem: TypeFun.curriedAux_ofCurriedAux_involution
Proof state before:
n : ℕ
F : CurriedTypeFun (Nat.succ n)
⊢ curriedAux (ofCurriedAux F) = F
Tactic:
induction n
<;> simp [curriedAux, ofCurriedAux, Vec.append1]
Proof 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
Theorem: TypeFun.curriedAux_ofCurriedAux_involution
Proof 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);
}
Proof state after:
no goals
Theorem: TypeFun.curriedAux_ofCurriedAux_involution
Proof 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
Proof 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
Theorem: TypeFun.curriedAux_ofCurriedAux_involution
Proof 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)
Proof state after:
no goals
Theorem: TypeFun.curried_ofCurried_involution
Proof state before:
n : ℕ
F : CurriedTypeFun n
⊢ curried (ofCurried F) = F
Tactic:
simp only [curried, ofCurried, reverseArgs_involution]
Proof state after:
n : ℕ
F : CurriedTypeFun n
⊢ curriedAux (ofCurriedAux F) = F
Theorem: TypeFun.curried_ofCurried_involution
Proof state before:
n : ℕ
F : CurriedTypeFun n
⊢ curriedAux (ofCurriedAux F) = F
Tactic:
apply curriedAux_ofCurriedAux_involution
Proof state after:
no goals
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
n : ℕ
F : TypeFun n
⊢ ofCurriedAux (curriedAux F) = F
Tactic:
cases n
Proof state after:
case zero
F : TypeFun Nat.zero
⊢ ofCurriedAux (curriedAux F) = F

case succ
n✝ : ℕ
F : TypeFun (Nat.succ n✝)
⊢ ofCurriedAux (curriedAux F) = F
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
F : TypeFun Nat.zero
⊢ ofCurriedAux (curriedAux F) = F
Tactic:
case zero =>
  funext x;
  simp [curriedAux, ofCurriedAux, Matrix.vecEmpty]
  congr
  funext i
  contradiction
Proof state after:
no goals
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof 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']
  }
}
Proof state after:
no goals
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
F : TypeFun Nat.zero
⊢ ofCurriedAux (curriedAux F) = F
Tactic:
funext x
Proof state after:
case h
F : TypeFun Nat.zero
x : TypeVec.{u_1} Nat.zero
⊢ ofCurriedAux (curriedAux F) x = F x
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof 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]
Proof state after:
case h
F : TypeFun Nat.zero
x : TypeVec.{u_1} Nat.zero
⊢ F Vec.nil = F x
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
case h
F : TypeFun Nat.zero
x : TypeVec.{u_1} Nat.zero
⊢ F Vec.nil = F x
Tactic:
congr
Proof state after:
case h.e_a
F : TypeFun Nat.zero
x : TypeVec.{u_1} Nat.zero
⊢ Vec.nil = x
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
case h.e_a
F : TypeFun Nat.zero
x : TypeVec.{u_1} Nat.zero
⊢ Vec.nil = x
Tactic:
funext i
Proof 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
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof 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
Proof state after:
no goals
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
n : ℕ
F : TypeFun (Nat.succ n)
⊢ ofCurriedAux (curriedAux F) = F
Tactic:
induction n
Proof 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
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof 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
}
Proof state after:
no goals
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof 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']
}
Proof state after:
no goals
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof state before:
F : TypeFun (Nat.succ Nat.zero)
⊢ ofCurriedAux (curriedAux F) = F
Tactic:
funext x
Proof state after:
case h
F : TypeFun (Nat.succ Nat.zero)
x : TypeVec.{u_1} (Nat.succ Nat.zero)
⊢ ofCurriedAux (curriedAux F) x = F x
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof 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]
Proof 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
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof 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
Proof 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
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof 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
Proof 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
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof 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
Proof 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✝)
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof 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]
Proof 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✝)
Theorem: TypeFun.ofCurriedAux_curriedAux_involution
Proof 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
Proof state after:
no goals