-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem nextn : ∀ {s}, ValidFor l (m₁ ++ m₂) r s →
    ∀ n, s.nextn n ⟨utf8Len m₁⟩ = ⟨utf8Len m₁ + utf8Len (m₂.take n)⟩
  | _, _, 0 => by simp [Substring.nextn]
  | s, h, n+1 => by
    simp only [Substring.nextn]
    match m₂ with
    | [] => simp at h; simp [h.next_stop, h.nextn_stop]
    | c::m₂ =>
      rw [h.next]
      have := @nextn l (m₁ ++ [c]) m₂ r s (by simp [h]) n
      simp at this; rw [this]; simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]

Proof state:
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
this :
  s.nextn n { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ + c.utf8Size + utf8Len (List.take n m₂) }
⊢ { byteIdx := utf8Len m₁ + c.utf8Size + utf8Len (List.take n m₂) } =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }

Tactic:
simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]

Result:
no goals

Proof state:
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
⊢ s.nextn n { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }

Tactic:
have := @nextn l (m₁ ++ [c]) m₂ r s (by simp [h]) n

Result:
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
this : s.nextn n { byteIdx := utf8Len (m₁ ++ [c]) } = { byteIdx := utf8Len (m₁ ++ [c]) + utf8Len (List.take n m₂) }
⊢ s.nextn n { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }

Proof state:
l m₁ m₂ r : List Char
s : Substring
h : ValidFor l (m₁ ++ m₂) r s
n : Nat
⊢ s.nextn n (s.next { byteIdx := utf8Len m₁ }) = { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) m₂) }

Tactic:
match m₂ with
| [] => simp at h; simp [h.next_stop, h.nextn_stop]
| c::m₂ =>
  rw [h.next]
  have := @nextn l (m₁ ++ [c]) m₂ r s (by simp [h]) n
  simp at this; rw [this]; simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]

Result:
no goals

Proof state:
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
this : s.nextn n { byteIdx := utf8Len (m₁ ++ [c]) } = { byteIdx := utf8Len (m₁ ++ [c]) + utf8Len (List.take n m₂) }
⊢ s.nextn n { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }

Tactic:
simp at this

Result:
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
this :
  s.nextn n { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ + c.utf8Size + utf8Len (List.take n m₂) }
⊢ s.nextn n { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }

Proof state:
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
this :
  s.nextn n { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ + c.utf8Size + utf8Len (List.take n m₂) }
⊢ s.nextn n { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }

Tactic:
rw [this]

Result:
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
this :
  s.nextn n { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ + c.utf8Size + utf8Len (List.take n m₂) }
⊢ { byteIdx := utf8Len m₁ + c.utf8Size + utf8Len (List.take n m₂) } =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }

Proof state:
l m₁ m₂ r : List Char
s : Substring
h : ValidFor l (m₁ ++ m₂) r s
n : Nat
⊢ s.nextn (n + 1) { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) m₂) }

Tactic:
simp only [Substring.nextn]

Result:
l m₁ m₂ r : List Char
s : Substring
h : ValidFor l (m₁ ++ m₂) r s
n : Nat
⊢ s.nextn n (s.next { byteIdx := utf8Len m₁ }) = { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) m₂) }

Proof state:
l m₁ m₂ r : List Char
x✝¹ : Substring
x✝ : ValidFor l (m₁ ++ m₂) r x✝¹
⊢ x✝¹.nextn 0 { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take 0 m₂) }

Tactic:
simp [Substring.nextn]

Result:
no goals

Proof state:
l m₁ m₂ r : List Char
s : Substring
n : Nat
h : ValidFor l (m₁ ++ []) r s
⊢ s.nextn n (s.next { byteIdx := utf8Len m₁ }) = { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) []) }

Tactic:
simp at h

Result:
l m₁ m₂ r : List Char
s : Substring
n : Nat
h : ValidFor l m₁ r s
⊢ s.nextn n (s.next { byteIdx := utf8Len m₁ }) = { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) []) }

Proof state:
l m₁ m₂ r : List Char
s : Substring
n : Nat
h : ValidFor l m₁ r s
⊢ s.nextn n (s.next { byteIdx := utf8Len m₁ }) = { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) []) }

Tactic:
simp [h.next_stop, h.nextn_stop]

Result:
no goals

Proof state:
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
⊢ s.nextn n (s.next { byteIdx := utf8Len m₁ }) = { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }

Tactic:
rw [h.next]

Result:
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
⊢ s.nextn n { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }

Proof state:
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
⊢ ValidFor l (m₁ ++ [c] ++ m₂) r s

Tactic:
simp [h]

Result:
no goals