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

State before:
case nil
α : Sort u_1
n : Nat
⊢ LList.nil.append LList.nil ≅ LList.nil
Tactic:
rw [LList.nil_append]
State after:
no goals

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

State before:
case cons
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ a✝ :: as✝.append LList.nil ≅ a✝ :: as✝
Tactic:
apply LList.cons_hcongr
State after:
case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ α = α

case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ 0 + n✝ = n✝

case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ a✝ ≅ a✝

case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ as✝.append LList.nil ≅ as✝

State before:
case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ α = α
Tactic:
reflexivity
State after:
no goals

State before:
case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ 0 + n✝ = n✝
Tactic:
rw [Nat.zero_add]
State after:
no goals

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

State before:
case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ as✝.append LList.nil ≅ as✝
Tactic:
exact ih ..
State after:
no goals