Theorem: HList.append_nil (GMLInit/Data/List/HList.lean)

State before:
case nil
αs : List (Sort u_1)
⊢ nil.append nil ≅ nil
Tactic:
rw [HList.nil_append]
State after:
no goals

State before:
case cons
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ (a✝¹ :: a✝).append nil ≅ a✝¹ :: a✝
Tactic:
rw [HList.cons_append]
State after:
case cons
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ a✝¹ :: a✝.append nil ≅ a✝¹ :: a✝

State before:
case cons
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ a✝¹ :: a✝.append nil ≅ a✝¹ :: a✝
Tactic:
apply HList.cons_hcongr
State after:
case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ α✝ = α✝

case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ αs✝ ++ [] = αs✝

case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ a✝¹ ≅ a✝¹

case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ a✝.append nil ≅ a✝

State before:
case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ α✝ = α✝
Tactic:
reflexivity
State after:
no goals

State before:
case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ αs✝ ++ [] = αs✝
Tactic:
rw [List.append_nil]
State after:
no goals

State before:
case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ a✝¹ ≅ a✝¹
Tactic:
reflexivity using (.≅.)
State after:
no goals

State before:
case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ a✝.append nil ≅ a✝
Tactic:
exact ih
State after:
no goals