Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
a : Γ
l✝ : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
l : List Γ
⊢ bind (cons a (Quotient.mk (BlankRel.setoid Γ) l)) f hf = append (f a) (bind (Quotient.mk (BlankRel.setoid Γ) l) f hf)
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
a : Γ
l : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
⊢ bind (cons a l) f hf = append (f a) (bind l f hf)
refine' l.inductionOn fun l ↦ _
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
a : Γ
l✝ : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
l : List Γ
⊢ bind (cons a (mk l)) f hf = append (f a) (bind (mk l) f hf)
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
a : Γ
l✝ : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
l : List Γ
⊢ bind (cons a (Quotient.mk (BlankRel.setoid Γ) l)) f hf = append (f a) (bind (Quotient.mk (BlankRel.setoid Γ) l) f hf)
suffices ((mk l).cons a).bind f hf = ((mk l).bind f hf).append (f a) by exact this
no goals
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
a : Γ
l✝ : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
l : List Γ
⊢ bind (cons a (mk l)) f hf = append (f a) (bind (mk l) f hf)
simp only [ListBlank.append_mk, ListBlank.bind_mk, ListBlank.cons_mk, List.cons_bind]
no goals
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
a : Γ
l✝ : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
l : List Γ
this : bind (cons a (mk l)) f hf = append (f a) (bind (mk l) f hf)
⊢ bind (cons a (Quotient.mk (BlankRel.setoid Γ) l)) f hf = append (f a) (bind (Quotient.mk (BlankRel.setoid Γ) l) f hf)
exact this