-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem set_next_add (s : String) (i : Pos) (c : Char) (b₁ b₂)
    (h : (s.next i).1 + b₁ = s.endPos.1 + b₂) :
    ((s.set i c).next i).1 + b₁ = (s.set i c).endPos.1 + b₂

Proof state:
s : String
i : Pos
c : Char
b₁✝ b₂✝ : Nat
h✝ : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁✝) = utf8ByteSize.go s.data + b₂✝
c' : Char
cs : List Char
a : Pos
b₁ b₂ : Nat
h' : a = i
h : c'.utf8Size + b₁ = c'.utf8Size + (utf8ByteSize.go cs + b₂)
⊢ c.utf8Size + b₁ = c.utf8Size + (utf8ByteSize.go cs + b₂)

Tactic:
rw [Nat.add_left_cancel h]

Result:
no goals

Proof state:
s : String
i : Pos
c : Char
b₁✝ b₂✝ : Nat
h✝ : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁✝) = utf8ByteSize.go s.data + b₂✝
c' : Char
cs : List Char
a : Pos
b₁ b₂ : Nat
h' : ¬a = i
h : (utf8GetAux cs (a + c') i).utf8Size + b₁ = utf8ByteSize.go cs + c'.utf8Size + b₂
⊢ (utf8GetAux (utf8SetAux c cs (a + c') i) (a + c') i).utf8Size + b₁ =
    utf8ByteSize.go (utf8SetAux c cs (a + c') i) + c'.utf8Size + b₂

Tactic:
rw [Nat.add_assoc] at h ⊢

Result:
s : String
i : Pos
c : Char
b₁✝ b₂✝ : Nat
h✝ : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁✝) = utf8ByteSize.go s.data + b₂✝
c' : Char
cs : List Char
a : Pos
b₁ b₂ : Nat
h' : ¬a = i
h : (utf8GetAux cs (a + c') i).utf8Size + b₁ = utf8ByteSize.go cs + (c'.utf8Size + b₂)
⊢ (utf8GetAux (utf8SetAux c cs (a + c') i) (a + c') i).utf8Size + b₁ =
    utf8ByteSize.go (utf8SetAux c cs (a + c') i) + (c'.utf8Size + b₂)

Proof state:
s : String
i : Pos
c : Char
b₁ b₂ : Nat
h : i.byteIdx + (utf8GetAux s.data 0 i).utf8Size + b₁ = utf8ByteSize.go s.data + b₂
⊢ i.byteIdx + (utf8GetAux (utf8SetAux c s.data 0 i) 0 i).utf8Size + b₁ = utf8ByteSize.go (utf8SetAux c s.data 0 i) + b₂

Tactic:
rw [Nat.add_comm i.1, Nat.add_assoc] at h ⊢

Result:
s : String
i : Pos
c : Char
b₁ b₂ : Nat
h : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁) = utf8ByteSize.go s.data + b₂
⊢ (utf8GetAux (utf8SetAux c s.data 0 i) 0 i).utf8Size + (i.byteIdx + b₁) =
    utf8ByteSize.go (utf8SetAux c s.data 0 i) + b₂

Proof state:
case hpos
s : String
i : Pos
c : Char
b₁✝ b₂✝ : Nat
h✝ : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁✝) = utf8ByteSize.go s.data + b₂✝
c' : Char
cs : List Char
a : Pos
b₁ b₂ : Nat
h' : a = i
h : c'.utf8Size + b₁ = utf8ByteSize.go cs + c'.utf8Size + b₂
⊢ c.utf8Size + b₁ = utf8ByteSize.go cs + c.utf8Size + b₂

case hneg
s : String
i : Pos
c : Char
b₁✝ b₂✝ : Nat
h✝ : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁✝) = utf8ByteSize.go s.data + b₂✝
c' : Char
cs : List Char
a : Pos
b₁ b₂ : Nat
h' : ¬a = i
h : (utf8GetAux cs (a + c') i).utf8Size + b₁ = utf8ByteSize.go cs + c'.utf8Size + b₂
⊢ (utf8GetAux (utf8SetAux c cs (a + c') i) (a + c') i).utf8Size + b₁ =
    utf8ByteSize.go (utf8SetAux c cs (a + c') i) + c'.utf8Size + b₂

Tactic:
next =>
  rw [Nat.add_assoc, Nat.add_left_comm] at h ⊢; rw [Nat.add_left_cancel h]

Result:
case hneg
s : String
i : Pos
c : Char
b₁✝ b₂✝ : Nat
h✝ : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁✝) = utf8ByteSize.go s.data + b₂✝
c' : Char
cs : List Char
a : Pos
b₁ b₂ : Nat
h' : ¬a = i
h : (utf8GetAux cs (a + c') i).utf8Size + b₁ = utf8ByteSize.go cs + c'.utf8Size + b₂
⊢ (utf8GetAux (utf8SetAux c cs (a + c') i) (a + c') i).utf8Size + b₁ =
    utf8ByteSize.go (utf8SetAux c cs (a + c') i) + c'.utf8Size + b₂

Proof state:
s : String
i : Pos
c : Char
b₁✝ b₂✝ : Nat
h✝ : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁✝) = utf8ByteSize.go s.data + b₂✝
c' : Char
cs : List Char
a : Pos
b₁ b₂ : Nat
h : (utf8GetAux (c' :: cs) a i).utf8Size + b₁ = utf8ByteSize.go (c' :: cs) + b₂
⊢ (utf8GetAux (ite (a = i) (c :: cs) (c' :: utf8SetAux c cs (a + c') i)) a i).utf8Size + b₁ =
    utf8ByteSize.go (ite (a = i) (c :: cs) (c' :: utf8SetAux c cs (a + c') i)) + b₂

Tactic:
apply iteInduction (motive := fun p => (utf8GetAux p a i).utf8Size + b₁ = utf8ByteSize.go p + b₂) <;>
  intro h' <;> simp [utf8GetAux, h', utf8ByteSize.go] at h ⊢

Result:
case hpos
s : String
i : Pos
c : Char
b₁✝ b₂✝ : Nat
h✝ : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁✝) = utf8ByteSize.go s.data + b₂✝
c' : Char
cs : List Char
a : Pos
b₁ b₂ : Nat
h' : a = i
h : c'.utf8Size + b₁ = utf8ByteSize.go cs + c'.utf8Size + b₂
⊢ c.utf8Size + b₁ = utf8ByteSize.go cs + c.utf8Size + b₂

case hneg
s : String
i : Pos
c : Char
b₁✝ b₂✝ : Nat
h✝ : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁✝) = utf8ByteSize.go s.data + b₂✝
c' : Char
cs : List Char
a : Pos
b₁ b₂ : Nat
h' : ¬a = i
h : (utf8GetAux cs (a + c') i).utf8Size + b₁ = utf8ByteSize.go cs + c'.utf8Size + b₂
⊢ (utf8GetAux (utf8SetAux c cs (a + c') i) (a + c') i).utf8Size + b₁ =
    utf8ByteSize.go (utf8SetAux c cs (a + c') i) + c'.utf8Size + b₂

Proof state:
s : String
i : Pos
c : Char
b₁✝ b₂✝ : Nat
h✝ : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁✝) = utf8ByteSize.go s.data + b₂✝
c' : Char
cs : List Char
a : Pos
b₁ b₂ : Nat
h' : ¬a = i
h : (utf8GetAux cs (a + c') i).utf8Size + b₁ = utf8ByteSize.go cs + (c'.utf8Size + b₂)
⊢ (utf8GetAux (utf8SetAux c cs (a + c') i) (a + c') i).utf8Size + b₁ =
    utf8ByteSize.go (utf8SetAux c cs (a + c') i) + (c'.utf8Size + b₂)

Tactic:
refine foo cs (a + c') b₁ (c'.utf8Size + b₂) h

Result:
no goals

Proof state:
s : String
i : Pos
c : Char
b₁✝ b₂✝ : Nat
h✝ : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁✝) = utf8ByteSize.go s.data + b₂✝
c' : Char
cs : List Char
a : Pos
b₁ b₂ : Nat
h : (utf8GetAux (c' :: cs) a i).utf8Size + b₁ = utf8ByteSize.go (c' :: cs) + b₂
⊢ (utf8GetAux (utf8SetAux c (c' :: cs) a i) a i).utf8Size + b₁ = utf8ByteSize.go (utf8SetAux c (c' :: cs) a i) + b₂

Tactic:
unfold utf8SetAux

Result:
s : String
i : Pos
c : Char
b₁✝ b₂✝ : Nat
h✝ : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁✝) = utf8ByteSize.go s.data + b₂✝
c' : Char
cs : List Char
a : Pos
b₁ b₂ : Nat
h : (utf8GetAux (c' :: cs) a i).utf8Size + b₁ = utf8ByteSize.go (c' :: cs) + b₂
⊢ (utf8GetAux (ite (a = i) (c :: cs) (c' :: utf8SetAux c cs (a + c') i)) a i).utf8Size + b₁ =
    utf8ByteSize.go (ite (a = i) (c :: cs) (c' :: utf8SetAux c cs (a + c') i)) + b₂

Proof state:
s : String
i : Pos
c : Char
b₁ b₂ : Nat
h : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁) = utf8ByteSize.go s.data + b₂
⊢ (utf8GetAux (utf8SetAux c s.data 0 i) 0 i).utf8Size + (i.byteIdx + b₁) =
    utf8ByteSize.go (utf8SetAux c s.data 0 i) + b₂

Tactic:
exact foo s.1 0 _ _ h

Result:
no goals

Proof state:
s : String
i : Pos
c : Char
b₁✝ b₂✝ : Nat
h✝ : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁✝) = utf8ByteSize.go s.data + b₂✝
c' : Char
cs : List Char
a : Pos
b₁ b₂ : Nat
h' : a = i
h : c'.utf8Size + b₁ = utf8ByteSize.go cs + c'.utf8Size + b₂
⊢ c.utf8Size + b₁ = utf8ByteSize.go cs + c.utf8Size + b₂

Tactic:
rw [Nat.add_assoc, Nat.add_left_comm] at h ⊢

Result:
s : String
i : Pos
c : Char
b₁✝ b₂✝ : Nat
h✝ : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁✝) = utf8ByteSize.go s.data + b₂✝
c' : Char
cs : List Char
a : Pos
b₁ b₂ : Nat
h' : a = i
h : c'.utf8Size + b₁ = c'.utf8Size + (utf8ByteSize.go cs + b₂)
⊢ c.utf8Size + b₁ = c.utf8Size + (utf8ByteSize.go cs + b₂)

Proof state:
case hneg
s : String
i : Pos
c : Char
b₁✝ b₂✝ : Nat
h✝ : (utf8GetAux s.data 0 i).utf8Size + (i.byteIdx + b₁✝) = utf8ByteSize.go s.data + b₂✝
c' : Char
cs : List Char
a : Pos
b₁ b₂ : Nat
h' : ¬a = i
h : (utf8GetAux cs (a + c') i).utf8Size + b₁ = utf8ByteSize.go cs + c'.utf8Size + b₂
⊢ (utf8GetAux (utf8SetAux c cs (a + c') i) (a + c') i).utf8Size + b₁ =
    utf8ByteSize.go (utf8SetAux c cs (a + c') i) + c'.utf8Size + b₂

Tactic:
next =>
  rw [Nat.add_assoc] at h ⊢
  refine foo cs (a + c') b₁ (c'.utf8Size + b₂) h

Result:
no goals