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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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