-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem extract.go₁_add_right_cancel (s : List Char) (i b e n : Nat) :
    go₁ s ⟨i + n⟩ ⟨b + n⟩ ⟨e + n⟩ = go₁ s ⟨i⟩ ⟨b⟩ ⟨e⟩

Proof state:
case ind
s : List Char
i✝ b e n : Nat
c : Char
cs : List Char
i : Nat
ih :
  go₁ cs { byteIdx := i + c.utf8Size + n } { byteIdx := b + n } { byteIdx := e + n } =
    go₁ cs { byteIdx := i + c.utf8Size } { byteIdx := b } { byteIdx := e }
h : ¬i = b
⊢ go₁ cs { byteIdx := i + n + c.utf8Size } { byteIdx := b + n } { byteIdx := e + n } =
    go₁ cs { byteIdx := i + c.utf8Size } { byteIdx := b } { byteIdx := e }

Tactic:
rw [Nat.add_right_comm]

Result:
case ind
s : List Char
i✝ b e n : Nat
c : Char
cs : List Char
i : Nat
ih :
  go₁ cs { byteIdx := i + c.utf8Size + n } { byteIdx := b + n } { byteIdx := e + n } =
    go₁ cs { byteIdx := i + c.utf8Size } { byteIdx := b } { byteIdx := e }
h : ¬i = b
⊢ go₁ cs { byteIdx := i + c.utf8Size + n } { byteIdx := b + n } { byteIdx := e + n } =
    go₁ cs { byteIdx := i + c.utf8Size } { byteIdx := b } { byteIdx := e }

Proof state:
case ind
s : List Char
i✝ b e n : Nat
c : Char
cs : List Char
i : Nat
ih :
  go₁ cs { byteIdx := i + c.utf8Size + n } { byteIdx := b + n } { byteIdx := e + n } =
    go₁ cs { byteIdx := i + c.utf8Size } { byteIdx := b } { byteIdx := e }
h : ¬i = b
⊢ go₁ cs { byteIdx := i + c.utf8Size + n } { byteIdx := b + n } { byteIdx := e + n } =
    go₁ cs { byteIdx := i + c.utf8Size } { byteIdx := b } { byteIdx := e }

Tactic:
exact ih

Result:
no goals

Proof state:
case ind
s : List Char
i✝ b e n : Nat
c : Char
cs : List Char
i : Nat
ih :
  go₁ cs { byteIdx := i + c.utf8Size + n } { byteIdx := b + n } { byteIdx := e + n } =
    go₁ cs { byteIdx := i + c.utf8Size } { byteIdx := b } { byteIdx := e }
h : ¬i = b
⊢ (if i + n = b + n then go₂ (c :: cs) { byteIdx := i + n } { byteIdx := e + n }
    else go₁ cs { byteIdx := i + n + c.utf8Size } { byteIdx := b + n } { byteIdx := e + n }) =
    if i = b then go₂ (c :: cs) { byteIdx := i } { byteIdx := e }
    else go₁ cs { byteIdx := i + c.utf8Size } { byteIdx := b } { byteIdx := e }

Tactic:
simp only [Nat.add_right_cancel_iff, h, ↓reduceIte]

Result:
case ind
s : List Char
i✝ b e n : Nat
c : Char
cs : List Char
i : Nat
ih :
  go₁ cs { byteIdx := i + c.utf8Size + n } { byteIdx := b + n } { byteIdx := e + n } =
    go₁ cs { byteIdx := i + c.utf8Size } { byteIdx := b } { byteIdx := e }
h : ¬i = b
⊢ go₁ cs { byteIdx := i + n + c.utf8Size } { byteIdx := b + n } { byteIdx := e + n } =
    go₁ cs { byteIdx := i + c.utf8Size } { byteIdx := b } { byteIdx := e }

Proof state:
case ind
s : List Char
i✝ b e n : Nat
c : Char
cs : List Char
i : Nat
h : ¬{ byteIdx := i } = { byteIdx := b }
ih :
  go₁ cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := b + n } { byteIdx := e + n } =
    go₁ cs ({ byteIdx := i } + c) { byteIdx := b } { byteIdx := e }
⊢ (if { byteIdx := { byteIdx := i }.byteIdx + n } = { byteIdx := b + n } then
      go₂ (c :: cs) { byteIdx := { byteIdx := i }.byteIdx + n } { byteIdx := e + n }
    else go₁ cs ({ byteIdx := { byteIdx := i }.byteIdx + n } + c) { byteIdx := b + n } { byteIdx := e + n }) =
    if { byteIdx := i } = { byteIdx := b } then go₂ (c :: cs) { byteIdx := i } { byteIdx := e }
    else go₁ cs ({ byteIdx := i } + c) { byteIdx := b } { byteIdx := e }

Tactic:
simp only [Pos.ext_iff, Pos.addChar_eq] at h ih ⊢

Result:
case ind
s : List Char
i✝ b e n : Nat
c : Char
cs : List Char
i : Nat
ih :
  go₁ cs { byteIdx := i + c.utf8Size + n } { byteIdx := b + n } { byteIdx := e + n } =
    go₁ cs { byteIdx := i + c.utf8Size } { byteIdx := b } { byteIdx := e }
h : ¬i = b
⊢ (if i + n = b + n then go₂ (c :: cs) { byteIdx := i + n } { byteIdx := e + n }
    else go₁ cs { byteIdx := i + n + c.utf8Size } { byteIdx := b + n } { byteIdx := e + n }) =
    if i = b then go₂ (c :: cs) { byteIdx := i } { byteIdx := e }
    else go₁ cs { byteIdx := i + c.utf8Size } { byteIdx := b } { byteIdx := e }

Proof state:
case eq
s : List Char
i b e n : Nat
⊢ ∀ (c : Char) (cs : List Char),
    go₂ (c :: cs) { byteIdx := b + n } { byteIdx := e + n } = go₂ (c :: cs) { byteIdx := b } { byteIdx := e }

Tactic:
intro c cs

Result:
case eq
s : List Char
i b e n : Nat
c : Char
cs : List Char
⊢ go₂ (c :: cs) { byteIdx := b + n } { byteIdx := e + n } = go₂ (c :: cs) { byteIdx := b } { byteIdx := e }

Proof state:
case eq
s : List Char
i b e n : Nat
c : Char
cs : List Char
⊢ go₂ (c :: cs) { byteIdx := b + n } { byteIdx := e + n } = go₂ (c :: cs) { byteIdx := b } { byteIdx := e }

Tactic:
apply go₂_add_right_cancel

Result:
no goals

Proof state:
case ind
s : List Char
i b e n : Nat
⊢ ∀ (c : Char) (cs : List Char) (i : Pos),
    ¬i = { byteIdx := b } →
      go₁ cs { byteIdx := i.byteIdx + c.utf8Size + n } { byteIdx := b + n } { byteIdx := e + n } =
          go₁ cs (i + c) { byteIdx := b } { byteIdx := e } →
        (if { byteIdx := i.byteIdx + n } = { byteIdx := b + n } then
            go₂ (c :: cs) { byteIdx := i.byteIdx + n } { byteIdx := e + n }
          else go₁ cs ({ byteIdx := i.byteIdx + n } + c) { byteIdx := b + n } { byteIdx := e + n }) =
          if i = { byteIdx := b } then go₂ (c :: cs) i { byteIdx := e }
          else go₁ cs (i + c) { byteIdx := b } { byteIdx := e }

Tactic:
intro c cs ⟨i⟩ h ih

Result:
case ind
s : List Char
i✝ b e n : Nat
c : Char
cs : List Char
i : Nat
h : ¬{ byteIdx := i } = { byteIdx := b }
ih :
  go₁ cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := b + n } { byteIdx := e + n } =
    go₁ cs ({ byteIdx := i } + c) { byteIdx := b } { byteIdx := e }
⊢ (if { byteIdx := { byteIdx := i }.byteIdx + n } = { byteIdx := b + n } then
      go₂ (c :: cs) { byteIdx := { byteIdx := i }.byteIdx + n } { byteIdx := e + n }
    else go₁ cs ({ byteIdx := { byteIdx := i }.byteIdx + n } + c) { byteIdx := b + n } { byteIdx := e + n }) =
    if { byteIdx := i } = { byteIdx := b } then go₂ (c :: cs) { byteIdx := i } { byteIdx := e }
    else go₁ cs ({ byteIdx := i } + c) { byteIdx := b } { byteIdx := e }

Proof state:
s : List Char
i b e n : Nat
⊢ go₁ s { byteIdx := i + n } { byteIdx := b + n } { byteIdx := e + n } =
    go₁ s { byteIdx := i } { byteIdx := b } { byteIdx := e }

Tactic:
apply utf8InductionOn s ⟨i⟩ ⟨b⟩ (motive := fun s i =>
  go₁ s ⟨i.byteIdx + n⟩ ⟨b + n⟩ ⟨e + n⟩ = go₁ s i ⟨b⟩ ⟨e⟩)
  <;> simp only [ne_eq, go₁, pos_add_char, implies_true, ↓reduceIte]

Result:
case eq
s : List Char
i b e n : Nat
⊢ ∀ (c : Char) (cs : List Char),
    go₂ (c :: cs) { byteIdx := b + n } { byteIdx := e + n } = go₂ (c :: cs) { byteIdx := b } { byteIdx := e }

case ind
s : List Char
i b e n : Nat
⊢ ∀ (c : Char) (cs : List Char) (i : Pos),
    ¬i = { byteIdx := b } →
      go₁ cs { byteIdx := i.byteIdx + c.utf8Size + n } { byteIdx := b + n } { byteIdx := e + n } =
          go₁ cs (i + c) { byteIdx := b } { byteIdx := e } →
        (if { byteIdx := i.byteIdx + n } = { byteIdx := b + n } then
            go₂ (c :: cs) { byteIdx := i.byteIdx + n } { byteIdx := e + n }
          else go₁ cs ({ byteIdx := i.byteIdx + n } + c) { byteIdx := b + n } { byteIdx := e + n }) =
          if i = { byteIdx := b } then go₂ (c :: cs) i { byteIdx := e }
          else go₁ cs (i + c) { byteIdx := b } { byteIdx := e }