-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem prevn : ∀ {s}, ValidFor l (m₁.reverse ++ m₂) r s →
    ∀ n, s.prevn n ⟨utf8Len m₁⟩ = ⟨utf8Len (m₁.drop n)⟩
  | _, _, 0 => by simp [Substring.prevn]
  | s, h, n+1 => by
    simp only [Substring.prevn]
    match m₁ with
    | [] => simp
    | c::m₁ =>
      rw [List.reverse_cons, List.append_assoc] at h
      have := h.prev; simp at this; simp [this, h.prevn n]

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

Tactic:
simp only [Substring.prevn]

Result:
l m₂ r m₁ : List Char
s : Substring
h : ValidFor l (m₁.reverse ++ m₂) r s
n : Nat
⊢ s.prevn n (s.prev { byteIdx := utf8Len m₁ }) = { byteIdx := utf8Len (List.drop (n + 1) m₁) }

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

Tactic:
rw [List.reverse_cons, List.append_assoc] at h

Result:
l m₂ r m₁✝ : List Char
s : Substring
n : Nat
c : Char
m₁ : List Char
h : ValidFor l (m₁.reverse ++ ([c] ++ m₂)) r s
⊢ s.prevn n (s.prev { byteIdx := utf8Len (c :: m₁) }) = { byteIdx := utf8Len (List.drop (n + 1) (c :: m₁)) }

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

Tactic:
simp

Result:
no goals

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

Tactic:
match m₁ with
| [] => simp
| c::m₁ =>
  rw [List.reverse_cons, List.append_assoc] at h
  have := h.prev; simp at this; simp [this, h.prevn n]

Result:
no goals

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

Tactic:
simp at this

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

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

Tactic:
simp [this, h.prevn n]

Result:
no goals

Proof state:
l m₂ r m₁✝ : List Char
s : Substring
n : Nat
c : Char
m₁ : List Char
h : ValidFor l (m₁.reverse ++ ([c] ++ m₂)) r s
⊢ s.prevn n (s.prev { byteIdx := utf8Len (c :: m₁) }) = { byteIdx := utf8Len (List.drop (n + 1) (c :: m₁)) }

Tactic:
have := h.prev

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

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

Tactic:
simp [Substring.prevn]

Result:
no goals