internlm/Lean-Github huggingface dataset:
Theorem: Vec.append1_drop_last
Proof state before:
α : Type u_1
n : ℕ
v : Vec α (n + 1)
i : Fin2 (Nat.succ n)
⊢ append1 (drop v) (last v) i = v i
Tactic:
cases i
Proof state after:
case fz
α : Type u_1
n : ℕ
v : Vec α (n + 1)
⊢ append1 (drop v) (last v) Fin2.fz = v Fin2.fz

case fs
α : Type u_1
n : ℕ
v : Vec α (n + 1)
a✝ : Fin2 n
⊢ append1 (drop v) (last v) (Fin2.fs a✝) = v (Fin2.fs a✝)
Theorem: Vec.append1_drop_last
Proof state before:
case fz
α : Type u_1
n : ℕ
v : Vec α (n + 1)
⊢ append1 (drop v) (last v) Fin2.fz = v Fin2.fz

case fs
α : Type u_1
n : ℕ
v : Vec α (n + 1)
a✝ : Fin2 n
⊢ append1 (drop v) (last v) (Fin2.fs a✝) = v (Fin2.fs a✝)
Tactic:
rfl
Proof state after:
case fs
α : Type u_1
n : ℕ
v : Vec α (n + 1)
a✝ : Fin2 n
⊢ append1 (drop v) (last v) (Fin2.fs a✝) = v (Fin2.fs a✝)
Theorem: Vec.append1_drop_last
Proof state before:
case fs
α : Type u_1
n : ℕ
v : Vec α (n + 1)
a✝ : Fin2 n
⊢ append1 (drop v) (last v) (Fin2.fs a✝) = v (Fin2.fs a✝)
Tactic:
rfl
Proof state after:
no goals
Theorem: Vec.reverse_involution
Proof state before:
α : Type u_1
n : ℕ
v : Vec α n
⊢ reverse (reverse v) = v
Tactic:
funext i
Proof state after:
case h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 n
⊢ reverse (reverse v) i = v i
Theorem: Vec.reverse_involution
Proof state before:
case h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 n
⊢ reverse (reverse v) i = v i
Tactic:
dsimp only [reverse]
Proof state after:
case h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 n
⊢ v (Fin2.inv (Fin2.inv i)) = v i
Theorem: Vec.reverse_involution
Proof state before:
case h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 n
⊢ v (Fin2.inv (Fin2.inv i)) = v i
Tactic:
apply congrArg
Proof state after:
case h.h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 n
⊢ Fin2.inv (Fin2.inv i) = i
Theorem: Vec.reverse_involution
Proof state before:
case h.h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 n
⊢ Fin2.inv (Fin2.inv i) = i
Tactic:
simp only [Fin2.inv, PFin2.toFin2_ofFin2, PFin2.inv_involution, PFin2.ofFin2_toFin2]
Proof state after:
no goals
Theorem: Vec.toList_length_eq_n
Proof state before:
α : Type u_1
n : ℕ
v : Vec α n
⊢ List.length (toList v) = n
Tactic:
induction n
Proof state after:
case zero
α : Type u_1
v : Vec α Nat.zero
⊢ List.length (toList v) = Nat.zero

case succ
α : Type u_1
n✝ : ℕ
n_ih✝ : ∀ {v : Vec α n✝}, List.length (toList v) = n✝
v : Vec α (Nat.succ n✝)
⊢ List.length (toList v) = Nat.succ n✝
Theorem: Vec.toList_length_eq_n
Proof state before:
α : Type u_1
v : Vec α Nat.zero
⊢ List.length (toList v) = Nat.zero
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Vec.toList_length_eq_n
Proof state before:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ List.length (toList v) = Nat.succ n
Tactic:
case succ n ih =>
  dsimp only [toList, List.length]
  dsimp only [HAdd.hAdd, Add.add, Nat.add]
  apply congrArg
  apply ih
Proof state after:
no goals
Theorem: Vec.toList_length_eq_n
Proof state before:
α : Type u_1
v : Vec α Nat.zero
⊢ List.length (toList v) = Nat.zero
Tactic:
rfl
Proof state after:
no goals
Theorem: Vec.toList_length_eq_n
Proof state before:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ List.length (toList v) = Nat.succ n
Tactic:
dsimp only [toList, List.length]
Proof state after:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ List.length (toList (drop v)) + 1 = Nat.succ n
Theorem: Vec.toList_length_eq_n
Proof state before:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ List.length (toList (drop v)) + 1 = Nat.succ n
Tactic:
dsimp only [HAdd.hAdd, Add.add, Nat.add]
Proof state after:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ Nat.succ (List.length (toList (drop v))) = Nat.succ n
Theorem: Vec.toList_length_eq_n
Proof state before:
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ Nat.succ (List.length (toList (drop v))) = Nat.succ n
Tactic:
apply congrArg
Proof state after:
case h
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ List.length (toList (drop v)) = n
Theorem: Vec.toList_length_eq_n
Proof state before:
case h
α : Type u_1
n : ℕ
ih : ∀ {v : Vec α n}, List.length (toList v) = n
v : Vec α (Nat.succ n)
⊢ List.length (toList (drop v)) = n
Tactic:
apply ih
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso
Proof state before:
α : Type u_1
n : ℕ
v : Vec α n
⊢ HEq (ofList (toList v)) v
Tactic:
apply HEq.trans (b := cast (β:=Vec α (List.length (toList v))) ?hc v)
Proof state after:
case h₁
α : Type u_1
n : ℕ
v : Vec α n
⊢ HEq (ofList (toList v)) (cast ?hc v)

case h₂
α : Type u_1
n : ℕ
v : Vec α n
⊢ HEq (cast ?hc v) v

case hc
α : Type u_1
n : ℕ
v : Vec α n
⊢ Vec α n = Vec α (List.length (toList v))
Theorem: Vec.ofList_toList_iso
Proof state before:
α : Type u_1
n : ℕ
v : Vec α n
⊢ Vec α n = Vec α (List.length (toList v))
Tactic:
case hc =>
  simp only [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 (cast ⋯ v) v
Tactic:
case h₂ =>
  apply cast_heq
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso
Proof state before:
α : Type u_1
n : ℕ
v : Vec α n
⊢ HEq (ofList (toList v)) (cast ⋯ v)
Tactic:
case h₁ =>
  apply heq_of_eq;
  funext i;
  apply eq_of_heq;
  rw[cast_arg] <;> try (solve | simp);
  simp_heq
  induction n <;> cases i;
  case succ.fz n ih => {
    dsimp only [toList, last, DVec.last, ofList, append1, List.length_cons, Nat.succ_eq_add_one]
    show HEq (v .fz) (v <| cast _ Fin2.fz)
    apply hcongr <;> (try solve | intros; rfl)
    simp_heq
    apply hcongr <;> (try solve | intros; rfl)
    simp
  }
  case succ.fs n ih i => {
    dsimp[ofList, toList, append1, drop]
    apply HEq.trans (@ih (fun i => v (.fs i)) i);
    apply hcongr <;> (try solve | intros; rfl)
    simp_heq
    apply hcongr;
    case H₂ => apply cast_heq
    case H₃ => apply congrArg; simp
    case H₄ => intro _; apply congrArg; simp
    apply hcongr <;> (try solve | intros; rfl);
    simp
  }
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso
Proof state before:
α : Type u_1
n : ℕ
v : Vec α n
⊢ Vec α n = Vec α (List.length (toList v))
Tactic:
simp only [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 (cast ⋯ v) v
Tactic:
apply cast_heq
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso
Proof state before:
α : Type u_1
n : ℕ
v : Vec α n
⊢ HEq (ofList (toList v)) (cast ⋯ v)
Tactic:
apply heq_of_eq
Proof state after:
case h
α : Type u_1
n : ℕ
v : Vec α n
⊢ ofList (toList v) = cast ⋯ v
Theorem: Vec.ofList_toList_iso
Proof state before:
case h
α : Type u_1
n : ℕ
v : Vec α n
⊢ ofList (toList v) = cast ⋯ v
Tactic:
funext i
Proof state after:
case h.h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 (List.length (toList v))
⊢ ofList (toList v) i = cast ⋯ v i
Theorem: Vec.ofList_toList_iso
Proof state before:
case h.h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 (List.length (toList v))
⊢ ofList (toList v) i = cast ⋯ v i
Tactic:
apply eq_of_heq
Proof state after:
case h.h.h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 (List.length (toList v))
⊢ HEq (ofList (toList v) i) (cast ⋯ v i)
Theorem: Vec.ofList_toList_iso
Proof state before:
case h.h.h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 (List.length (toList v))
⊢ HEq (ofList (toList v) i) (cast ⋯ v i)
Tactic:
rw[cast_arg] <;> try (solve | simp);
Proof state after:
case h.h.h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 (List.length (toList v))
⊢ HEq (ofList (toList v) i) (cast ⋯ (v (cast ⋯ i)))
Theorem: Vec.ofList_toList_iso
Proof state before:
case h.h.h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 (List.length (toList v))
⊢ HEq (ofList (toList v) i) (cast ⋯ (v (cast ⋯ i)))
Tactic:
simp_heq
Proof state after:
case h.h.h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 (List.length (toList v))
⊢ HEq (ofList (toList v) i) (v (cast ⋯ i))
Theorem: Vec.ofList_toList_iso
Proof state before:
case h.h.h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 (List.length (toList v))
⊢ HEq (ofList (toList v) i) (v (cast ⋯ i))
Tactic:
induction n <;> cases i
Proof state after:
case h.h.h.succ.fz
α : Type u_1
n✝ : ℕ
n_ih✝ : ∀ {v : Vec α n✝} (i : Fin2 (List.length (toList v))), HEq (ofList (toList v) i) (v (cast ⋯ i))
v : Vec α (Nat.succ n✝)
⊢ HEq (ofList (toList v) Fin2.fz) (v (cast ⋯ Fin2.fz))

case h.h.h.succ.fs
α : Type u_1
n✝ : ℕ
n_ih✝ : ∀ {v : Vec α n✝} (i : Fin2 (List.length (toList v))), HEq (ofList (toList v) i) (v (cast ⋯ i))
v : Vec α (Nat.succ n✝)
a✝ : Fin2 (Nat.add (List.length (toList (drop v))) 0)
⊢ HEq (ofList (toList v) (Fin2.fs a✝)) (v (cast ⋯ (Fin2.fs a✝)))
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)
⊢ HEq (ofList (toList v) Fin2.fz) (v (cast ⋯ Fin2.fz))
Tactic:
case succ.fz n ih => {
  dsimp only [toList, last, DVec.last, ofList, append1, List.length_cons, Nat.succ_eq_add_one]
  show HEq (v .fz) (v <| cast _ Fin2.fz)
  apply hcongr <;> (try solve | intros; rfl)
  simp_heq
  apply hcongr <;> (try solve | intros; rfl)
  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)
⊢ HEq (ofList (toList v) (Fin2.fs i)) (v (cast ⋯ (Fin2.fs i)))
Tactic:
case succ.fs n ih i => {
  dsimp[ofList, toList, append1, drop]
  apply HEq.trans (@ih (fun i => v (.fs i)) i);
  apply hcongr <;> (try solve | intros; rfl)
  simp_heq
  apply hcongr;
  case H₂ => apply cast_heq
  case H₃ => apply congrArg; simp
  case H₄ => intro _; apply congrArg; simp
  apply hcongr <;> (try solve | intros; rfl);
  simp
}
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso
Proof state before:
case h.h.h.h₃
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 (List.length (toList v))
⊢ ∀ (a' : Fin2 (List.length (toList v))), (fun x => α) (cast ⋯ a') = (fun x => α) a'
Tactic:
(solve | simp)
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso
Proof state before:
case h.h.h.h₃
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 (List.length (toList v))
⊢ ∀ (a' : Fin2 (List.length (toList v))), (fun x => α) (cast ⋯ a') = (fun x => α) a'
Tactic:
solve | simp
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso
Proof state before:
case h.h.h.h₃
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 (List.length (toList v))
⊢ ∀ (a' : Fin2 (List.length (toList v))), (fun x => α) (cast ⋯ a') = (fun x => α) a'
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)
⊢ HEq (ofList (toList v) Fin2.fz) (v (cast ⋯ Fin2.fz))
Tactic:
dsimp only [toList, last, DVec.last, ofList, append1, List.length_cons, Nat.succ_eq_add_one]
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)
⊢ HEq (v 0) (v (cast ⋯ Fin2.fz))
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)
⊢ HEq (v 0) (v (cast ⋯ Fin2.fz))
Tactic:
show HEq (v .fz) (v <| cast _ Fin2.fz)
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)
⊢ HEq (v Fin2.fz) (v (cast ⋯ Fin2.fz))
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)
⊢ HEq (v Fin2.fz) (v (cast ⋯ Fin2.fz))
Tactic:
apply hcongr <;> (try solve | intros; rfl)
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)
⊢ HEq Fin2.fz (cast ⋯ Fin2.fz)
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)
⊢ HEq Fin2.fz (cast ⋯ Fin2.fz)
Tactic:
simp_heq
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)
⊢ HEq Fin2.fz Fin2.fz
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)
⊢ HEq Fin2.fz Fin2.fz
Tactic:
apply hcongr <;> (try solve | intros; rfl)
Proof state after:
case 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)
⊢ HEq n (List.length (toList (drop v)))
Theorem: Vec.ofList_toList_iso
Proof state before:
case 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)
⊢ HEq n (List.length (toList (drop v)))
Tactic:
simp
Proof state after:
no goals
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)
⊢ Fin2 (Nat.succ n) = Fin2 (Nat.succ n)
Tactic:
try solve | intros; rfl
Proof state after:
no goals
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)
⊢ Fin2 (Nat.succ n) = Fin2 (Nat.succ n)
Tactic:
solve | intros; rfl
Proof state after:
no goals
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)
⊢ ∀ (a : Fin2 (Nat.succ n)), (fun x => α) a = (fun x => α) (cast ?H₃ a)
Tactic:
intros
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)
a✝ : Fin2 (Nat.succ n)
⊢ (fun x => α) a✝ = (fun x => α) (cast ?H₃ a✝)
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)
⊢ Fin2 (Nat.succ n) = Fin2 (Nat.succ n)
Tactic:
rfl
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso
Proof state before:
case 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)
⊢ ℕ = ℕ
Tactic:
try solve | intros; rfl
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso
Proof state before:
case 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)
⊢ ℕ = ℕ
Tactic:
solve | intros; rfl
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso
Proof state before:
case 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)
⊢ ∀ (a : ℕ), Fin2 (Nat.succ a) = Fin2 (Nat.succ (cast ?H₂.H₃ a))
Tactic:
intros
Proof state after:
case 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)
a✝ : ℕ
⊢ Fin2 (Nat.succ a✝) = Fin2 (Nat.succ (cast ?H₂.H₃ a✝))
Theorem: Vec.ofList_toList_iso
Proof state before:
case 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)
⊢ ℕ = ℕ
Tactic:
rfl
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)
⊢ HEq (ofList (toList v) (Fin2.fs i)) (v (cast ⋯ (Fin2.fs i)))
Tactic:
dsimp[ofList, toList, append1, drop]
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)
⊢ HEq (ofList (toList (drop v)) i) (v (cast ⋯ (Fin2.fs i)))
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)
⊢ HEq (ofList (toList (drop v)) i) (v (cast ⋯ (Fin2.fs i)))
Tactic:
apply HEq.trans (@ih (fun i => v (.fs i)) i)
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)
⊢ HEq (v (Fin2.fs (cast ⋯ i))) (v (cast ⋯ (Fin2.fs i)))
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)
⊢ HEq (v (Fin2.fs (cast ⋯ i))) (v (cast ⋯ (Fin2.fs i)))
Tactic:
apply hcongr <;> (try solve | intros; rfl)
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)
⊢ HEq (Fin2.fs (cast ⋯ i)) (cast ⋯ (Fin2.fs i))
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)
⊢ HEq (Fin2.fs (cast ⋯ i)) (cast ⋯ (Fin2.fs i))
Tactic:
simp_heq
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)
⊢ HEq (Fin2.fs (cast ⋯ i)) (Fin2.fs i)
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)
⊢ HEq (Fin2.fs (cast ⋯ i)) (Fin2.fs i)
Tactic:
apply hcongr
Proof state after:
case 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)
⊢ HEq Fin2.fs Fin2.fs

case 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)
⊢ HEq (cast ⋯ i) i

case 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)
⊢ Fin2 n → Fin2 (Nat.succ n) = Fin2 (Nat.succ (List.length (toList (drop v))))

case 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)
⊢ Fin2 n = Fin2 (Nat.add (List.length (toList (drop v))) 0)
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)
⊢ HEq (cast ⋯ i) i
Tactic:
case H₂ => apply cast_heq
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.add (List.length (toList (drop v))) 0)
Tactic:
case H₃ => apply congrArg; 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:
case H₄ => intro _; apply congrArg; simp
Proof state after:
no goals
Theorem: Vec.ofList_toList_iso
Proof state before:
case 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)
⊢ HEq Fin2.fs Fin2.fs
Tactic:
apply hcongr <;> (try solve | intros; rfl)
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)
⊢ HEq n (List.length (toList (drop v)))
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)
⊢ HEq n (List.length (toList (drop v)))
Tactic:
simp
Proof state after:
no goals
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)
⊢ Fin2 (Nat.succ n) = Fin2 (Nat.succ n)
Tactic:
try solve | intros; rfl
Proof state after:
no goals
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)
⊢ Fin2 (Nat.succ n) = Fin2 (Nat.succ n)
Tactic:
solve | intros; rfl
Proof state after:
no goals
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 (Nat.succ n)), (fun x => α) a = (fun x => α) (cast ?H₃ a)
Tactic:
intros
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 (Nat.succ n)
⊢ (fun x => α) a✝ = (fun x => α) (cast ?H₃ a✝)
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)
⊢ Fin2 (Nat.succ n) = Fin2 (Nat.succ n)
Tactic:
rfl
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)
⊢ HEq (cast ⋯ i) i
Tactic:
apply cast_heq
Proof state after:
no goals