case h
p : Pos
c₁ c₂ : Char
⊢ (p + c₁ + c₂).byteIdx = (p + c₂ + c₁).byteIdx
p : Pos
c₁ c₂ : Char
⊢ p + c₁ + c₂ = p + c₂ + c₁
apply ext
case h
p : Pos
c₁ c₂ : Char
⊢ p.byteIdx + csize c₁ + csize c₂ = p.byteIdx + csize c₂ + csize c₁
case h
p : Pos
c₁ c₂ : Char
⊢ (p + c₁ + c₂).byteIdx = (p + c₂ + c₁).byteIdx
repeat rw [pos_add_char]
no goals
case h
p : Pos
c₁ c₂ : Char
⊢ p.byteIdx + csize c₁ + csize c₂ = p.byteIdx + csize c₂ + csize c₁
apply Nat.add_right_comm
case h
p : Pos
c₁ c₂ : Char
⊢ p.byteIdx + csize c₁ + csize c₂ = p.byteIdx + csize c₂ + csize c₁
case h
p : Pos
c₁ c₂ : Char
⊢ p.byteIdx + csize c₁ + csize c₂ = p.byteIdx + csize c₂ + csize c₁
rw [pos_add_char]