Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ nth (map f (Quotient.mk (BlankRel.setoid Γ) l)) n = PointedMap.f f (nth (Quotient.mk (BlankRel.setoid Γ) l) n)
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
n : ℕ
⊢ nth (map f l) n = PointedMap.f f (nth l n)
refine' l.inductionOn fun l ↦ _
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ nth (map f (mk l)) n = PointedMap.f f (nth (mk l) n)
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ nth (map f (Quotient.mk (BlankRel.setoid Γ) l)) n = PointedMap.f f (nth (Quotient.mk (BlankRel.setoid Γ) l) n)
suffices ((mk l).map f).nth n = f ((mk l).nth n) by exact this
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ Option.iget (Option.map f.f (List.get? l n)) = PointedMap.f f (Option.iget (List.get? l n))
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ nth (map f (mk l)) n = PointedMap.f f (nth (mk l) n)
simp only [List.get?_map, ListBlank.map_mk, ListBlank.nth_mk, List.getI_eq_iget_get?]
case none
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ Option.iget (Option.map f.f none) = PointedMap.f f (Option.iget none)

case some
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
val✝ : Γ
⊢ Option.iget (Option.map f.f (some val✝)) = PointedMap.f f (Option.iget (some val✝))
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ Option.iget (Option.map f.f (List.get? l n)) = PointedMap.f f (Option.iget (List.get? l n))
cases l.get? n
no goals
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
this : nth (map f (mk l)) n = PointedMap.f f (nth (mk l) n)
⊢ nth (map f (Quotient.mk (BlankRel.setoid Γ) l)) n = PointedMap.f f (nth (Quotient.mk (BlankRel.setoid Γ) l) n)
exact this
no goals
case none
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ Option.iget (Option.map f.f none) = PointedMap.f f (Option.iget none)
exact f.2.symm
no goals
case some
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
val✝ : Γ
⊢ Option.iget (Option.map f.f (some val✝)) = PointedMap.f f (Option.iget (some val✝))
rfl