Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
l₃ : ListBlank Γ
l : List Γ
⊢ append (l₁ ++ l₂) (Quotient.mk (BlankRel.setoid Γ) l) = append l₁ (append l₂ (Quotient.mk (BlankRel.setoid Γ) l))
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
l₃ : ListBlank Γ
⊢ append (l₁ ++ l₂) l₃ = append l₁ (append l₂ l₃)
refine' l₃.inductionOn fun l ↦ _
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
l₃ : ListBlank Γ
l : List Γ
⊢ append (l₁ ++ l₂) (mk l) = append l₁ (append l₂ (mk l))
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
l₃ : ListBlank Γ
l : List Γ
⊢ append (l₁ ++ l₂) (Quotient.mk (BlankRel.setoid Γ) l) = append l₁ (append l₂ (Quotient.mk (BlankRel.setoid Γ) l))
suffices append (l₁ ++ l₂) (mk l) = append l₁ (append l₂ (mk l)) by exact this
no goals
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
l₃ : ListBlank Γ
l : List Γ
⊢ append (l₁ ++ l₂) (mk l) = append l₁ (append l₂ (mk l))
simp only [ListBlank.append_mk, List.append_assoc]
no goals
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
l₃ : ListBlank Γ
l : List Γ
this : append (l₁ ++ l₂) (mk l) = append l₁ (append l₂ (mk l))
⊢ append (l₁ ++ l₂) (Quotient.mk (BlankRel.setoid Γ) l) = append l₁ (append l₂ (Quotient.mk (BlankRel.setoid Γ) l))
exact this