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

State before:
case nil
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
⊢ (LList.nil.append bs).append cs ≅ LList.nil.append (bs.append cs)
Tactic:
rw [LList.nil_append, LList.nil_append]
State after:
no goals

State before:
case cons
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ ((a✝ :: as✝).append bs).append cs ≅ (a✝ :: as✝).append (bs.append cs)
Tactic:
rw [LList.cons_append, LList.cons_append, LList.cons_append]
State after:
case cons
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ a✝ :: (as✝.append bs).append cs ≅ a✝ :: as✝.append (bs.append cs)

State before:
case cons
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ a✝ :: (as✝.append bs).append cs ≅ a✝ :: as✝.append (bs.append cs)
Tactic:
apply LList.cons_hcongr
State after:
case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ α = α

case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ n + (m + n✝) = n + m + n✝

case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ a✝ ≅ a✝

case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ (as✝.append bs).append cs ≅ as✝.append (bs.append cs)

State before:
case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ α = α
Tactic:
reflexivity
State after:
no goals

State before:
case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ n + (m + n✝) = n + m + n✝
Tactic:
rw [Nat.add_assoc]
State after:
no goals

State before:
case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ a✝ ≅ a✝
Tactic:
reflexivity using (.≅.)
State after:
no goals

State before:
case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
Tactic:
exact ih ..
State after:
no goals