Theorem: Vec.ofList_toList_iso (Qpf/Util/Vec.lean)

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)
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))

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]
State after:
no goals

State before:
α : Type u_1
n : ℕ
v : Vec α n
⊢ HEq (cast ⋯ v) v
Tactic:
case h₂ =>
  apply cast_heq
State after:
no goals

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
  }
State after:
no goals

State before:
α : Type u_1
n : ℕ
v : Vec α n
⊢ Vec α n = Vec α (List.length (toList v))
Tactic:
simp only [toList_length_eq_n]
State after:
no goals

State before:
α : Type u_1
n : ℕ
v : Vec α n
⊢ HEq (cast ⋯ v) v
Tactic:
apply cast_heq
State after:
no goals

State before:
α : Type u_1
n : ℕ
v : Vec α n
⊢ HEq (ofList (toList v)) (cast ⋯ v)
Tactic:
apply heq_of_eq
State after:
case h
α : Type u_1
n : ℕ
v : Vec α n
⊢ ofList (toList v) = cast ⋯ v

State before:
case h
α : Type u_1
n : ℕ
v : Vec α n
⊢ ofList (toList v) = cast ⋯ v
Tactic:
funext i
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

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
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)

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);
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)))

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
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))

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
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✝)))

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
}
State after:
no goals

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
}
State after:
no goals

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)
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
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))

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)
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))

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)
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)

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
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

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)
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)))

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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✝)

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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✝))

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
State after:
no goals

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]
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)))

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)
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)))

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)
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))

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
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)

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
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)

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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)
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)))

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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✝)

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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 _
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))))

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
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)))

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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✝)))

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
State after:
no goals