Theorem: LList.cons_append (GMLInit/Data/List/LList.lean)

State before:
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (a :: as).append bs = a :: as.append bs
Tactic:
apply eq_of_heq
State after:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (a :: as).append bs ≅ a :: as.append bs

State before:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (a :: as).append bs ≅ a :: as.append bs
Tactic:
unfold LList.append LList.cons
State after:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (let_fun this := ⋯ ▸ (HList.cons a as).append bs;
    this) ≅
    HList.cons a
      (let_fun this := ⋯ ▸ HList.append as bs;
      this)

State before:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (let_fun this := ⋯ ▸ (HList.cons a as).append bs;
    this) ≅
    HList.cons a
      (let_fun this := ⋯ ▸ HList.append as bs;
      this)
Tactic:
elim_casts
State after:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (HList.cons a as).append bs ≅ HList.cons a (⋯ ▸ HList.append as bs)

State before:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (HList.cons a as).append bs ≅ HList.cons a (⋯ ▸ HList.append as bs)
Tactic:
rw [HList.cons_append]
State after:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ HList.cons a (HList.append as bs) ≅ HList.cons a (⋯ ▸ HList.append as bs)

State before:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ HList.cons a (HList.append as bs) ≅ HList.cons a (⋯ ▸ HList.append as bs)
Tactic:
apply HList.cons_hcongr
State after:
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ α = α

case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ List.replicate n α ++ List.replicate m α = List.replicate (m + n) α

case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ a ≅ a

case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ HList.append as bs ≅ ⋯ ▸ HList.append as bs

State before:
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ α = α
Tactic:
reflexivity
State after:
no goals

State before:
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ List.replicate n α ++ List.replicate m α = List.replicate (m + n) α
Tactic:
rw [List.replicate_add]
State after:
no goals

State before:
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ a ≅ a
Tactic:
reflexivity using (.≅.)
State after:
no goals

State before:
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ HList.append as bs ≅ ⋯ ▸ HList.append as bs
Tactic:
elim_casts
State after:
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ HList.append as bs ≅ HList.append as bs

State before:
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ HList.append as bs ≅ HList.append as bs
Tactic:
reflexivity using (.≅.)
State after:
no goals