-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem erase_range' :
    (range' s n).erase i =
      range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Proof state:
case pos
s n i : Nat
h : s ≤ i → s + n ≤ i
h' : s ≤ i
p : min s (i + 1) + n - (i + 1) = 0
⊢ range' s n = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Tactic:
simp [p]

Result:
case pos
s n i : Nat
h : s ≤ i → s + n ≤ i
h' : s ≤ i
p : min s (i + 1) + n - (i + 1) = 0
⊢ n = min n (i - s)

Proof state:
case pos.intro.intro.intro
s n i : Nat
h : i ∈ range' s n
as bs : List Nat
h₁ : ∃ k, k ≤ n ∧ as = range' s k ∧ i :: bs = range' (s + k) (n - k)
h₂ : ¬i ∈ as
⊢ as ++ bs = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Tactic:
obtain ⟨k, -, rfl, hbs⟩ := h₁

Result:
case pos.intro.intro.intro.intro.intro.intro
s n i : Nat
h : i ∈ range' s n
bs : List Nat
k : Nat
hbs : i :: bs = range' (s + k) (n - k)
h₂ : ¬i ∈ range' s k
⊢ range' s k ++ bs = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Proof state:
case neg
s n i : Nat
h : ¬i ∈ range' s n
⊢ (range' s n).erase i = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Tactic:
rw [erase_of_not_mem h]

Result:
case neg
s n i : Nat
h : ¬i ∈ range' s n
⊢ range' s n = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Proof state:
case neg
s n i : Nat
h : ¬i ∈ range' s n
⊢ range' s n = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Tactic:
simp only [mem_range'_1, not_and, Nat.not_lt] at h

Result:
case neg
s n i : Nat
h : s ≤ i → s + n ≤ i
⊢ range' s n = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Proof state:
case pos
s n i : Nat
h : s ≤ i → s + n ≤ i
h' : s ≤ i
⊢ range' s n = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Tactic:
have p : min s (i + 1) + n - (i + 1) = 0 := by omega

Result:
case pos
s n i : Nat
h : s ≤ i → s + n ≤ i
h' : s ≤ i
p : min s (i + 1) + n - (i + 1) = 0
⊢ range' s n = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Proof state:
case pos.intro.intro.intro.intro.intro.intro
s n i : Nat
h : i ∈ range' s n
bs : List Nat
k : Nat
hbs : s + k = i ∧ 0 < n - k ∧ bs = range' (i + 1) (n - k - 1)
h₂ : ¬i ∈ range' s k
⊢ range' s k ++ bs = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Tactic:
obtain ⟨rfl, -, rfl⟩ := hbs

Result:
case pos.intro.intro.intro.intro.intro.intro.intro.intro
s n k : Nat
h : s + k ∈ range' s n
h₂ : ¬s + k ∈ range' s k
⊢ range' s k ++ range' (s + k + 1) (n - k - 1) =
    range' s (min n (s + k - s)) ++ range' (max s (s + k + 1)) (min s (s + k + 1) + n - (s + k + 1))

Proof state:
case neg
s n i : Nat
h : s ≤ i → s + n ≤ i
⊢ range' s n = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Tactic:
by_cases h' : s ≤ i

Result:
case pos
s n i : Nat
h : s ≤ i → s + n ≤ i
h' : s ≤ i
⊢ range' s n = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

case neg
s n i : Nat
h : s ≤ i → s + n ≤ i
h' : ¬s ≤ i
⊢ range' s n = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Proof state:
s n i : Nat
h : s ≤ i → s + n ≤ i
h' : ¬s ≤ i
⊢ i - s = 0

Tactic:
omega

Result:
no goals

Proof state:
case pos.intro.intro.intro.intro.intro.intro.intro.intro
s n k : Nat
h₂ : ¬s + k ∈ range' s k
h : k < n
⊢ range' s k ++ range' (s + k + 1) (n - k - 1) =
    range' s (min n (s + k - s)) ++ range' (max s (s + k + 1)) (min s (s + k + 1) + n - (s + k + 1))

Tactic:
congr 2 <;> omega

Result:
no goals

Proof state:
case pos
s n i : Nat
h : s ≤ i → s + n ≤ i
h' : s ≤ i
p : min s (i + 1) + n - (i + 1) = 0
⊢ n = min n (i - s)

Tactic:
omega

Result:
no goals

Proof state:
s n i : Nat
⊢ (range' s n).erase i = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Tactic:
by_cases h : i ∈ range' s n

Result:
case pos
s n i : Nat
h : i ∈ range' s n
⊢ (range' s n).erase i = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

case neg
s n i : Nat
h : ¬i ∈ range' s n
⊢ (range' s n).erase i = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Proof state:
case pos.intro.intro.intro
s n i : Nat
h : i ∈ range' s n
as bs : List Nat
h₁ : range' s n = as ++ i :: bs
h₂ : ¬i ∈ as
⊢ as ++ bs = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Tactic:
rw [range'_eq_append_iff] at h₁

Result:
case pos.intro.intro.intro
s n i : Nat
h : i ∈ range' s n
as bs : List Nat
h₁ : ∃ k, k ≤ n ∧ as = range' s k ∧ i :: bs = range' (s + k) (n - k)
h₂ : ¬i ∈ as
⊢ as ++ bs = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Proof state:
s n i : Nat
h : s ≤ i → s + n ≤ i
h' : s ≤ i
⊢ min s (i + 1) + n - (i + 1) = 0

Tactic:
omega

Result:
no goals

Proof state:
case neg
s n i : Nat
h : s ≤ i → s + n ≤ i
h' : ¬s ≤ i
p : i - s = 0
⊢ range' s n = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Tactic:
simp [p]

Result:
case neg
s n i : Nat
h : s ≤ i → s + n ≤ i
h' : ¬s ≤ i
p : i - s = 0
⊢ n = min s (i + 1) + n - (i + 1) ∧ (n = 0 ∨ s = max s (i + 1))

Proof state:
case neg
s n i : Nat
h : s ≤ i → s + n ≤ i
h' : ¬s ≤ i
p : i - s = 0
⊢ n = min s (i + 1) + n - (i + 1) ∧ (n = 0 ∨ s = max s (i + 1))

Tactic:
omega

Result:
no goals

Proof state:
case pos.intro.intro.intro.intro.intro.intro.intro.intro
s n k : Nat
h : s + k ∈ range' s n
h₂ : ¬s + k ∈ range' s k
⊢ range' s k ++ range' (s + k + 1) (n - k - 1) =
    range' s (min n (s + k - s)) ++ range' (max s (s + k + 1)) (min s (s + k + 1) + n - (s + k + 1))

Tactic:
simp at h

Result:
case pos.intro.intro.intro.intro.intro.intro.intro.intro
s n k : Nat
h₂ : ¬s + k ∈ range' s k
h : k < n
⊢ range' s k ++ range' (s + k + 1) (n - k - 1) =
    range' s (min n (s + k - s)) ++ range' (max s (s + k + 1)) (min s (s + k + 1) + n - (s + k + 1))

Proof state:
case pos
s n i : Nat
h : i ∈ range' s n
⊢ (range' s n).erase i = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Tactic:
obtain ⟨as, bs, h₁, h₂⟩ := eq_append_cons_of_mem h

Result:
case pos.intro.intro.intro
s n i : Nat
h : i ∈ range' s n
as bs : List Nat
h₁ : range' s n = as ++ i :: bs
h₂ : ¬i ∈ as
⊢ (range' s n).erase i = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Proof state:
case neg
s n i : Nat
h : s ≤ i → s + n ≤ i
h' : ¬s ≤ i
⊢ range' s n = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Tactic:
have p : i - s = 0 := by omega

Result:
case neg
s n i : Nat
h : s ≤ i → s + n ≤ i
h' : ¬s ≤ i
p : i - s = 0
⊢ range' s n = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Proof state:
case pos.intro.intro.intro.intro.intro.intro
s n i : Nat
h : i ∈ range' s n
bs : List Nat
k : Nat
hbs : i :: bs = range' (s + k) (n - k)
h₂ : ¬i ∈ range' s k
⊢ range' s k ++ bs = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Tactic:
rw [eq_comm, range'_eq_cons_iff] at hbs

Result:
case pos.intro.intro.intro.intro.intro.intro
s n i : Nat
h : i ∈ range' s n
bs : List Nat
k : Nat
hbs : s + k = i ∧ 0 < n - k ∧ bs = range' (i + 1) (n - k - 1)
h₂ : ¬i ∈ range' s k
⊢ range' s k ++ bs = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))