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

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

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

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

case cons.a
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ αs✝ ++ βs ++ γs = αs✝ ++ (βs ++ γs)

case cons.a
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ a✝¹ ≅ a✝¹

case cons.a
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ (a✝.append bs).append cs ≅ a✝.append (bs.append cs)

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

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

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

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