-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
    (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j

Proof state:
s n i : Nat
p : Nat → Bool
h : p i = true
h₃ : ∀ (j : Nat), s ≤ j → j < i → p j = false
h₁ : s ≤ i
h₂ : i < s + n
a : Nat
a₁ : s ≤ a
a₂ : a < s + (i - s)
⊢ a < i

Tactic:
omega

Result:
no goals

Proof state:
case mpr.intro.intro.refine_2
s n i : Nat
p : Nat → Bool
h : p i = true
h₃ : ∀ (j : Nat), s ≤ j → j < i → p j = false
h₁ : s ≤ i
h₂ : i < s + n
⊢ ∀ (a : Nat), s ≤ a → a < s + (i - s) → p a = false

Tactic:
intro a a₁ a₂

Result:
case mpr.intro.intro.refine_2
s n i : Nat
p : Nat → Bool
h : p i = true
h₃ : ∀ (j : Nat), s ≤ j → j < i → p j = false
h₁ : s ≤ i
h₂ : i < s + n
a : Nat
a₁ : s ≤ a
a₂ : a < s + (i - s)
⊢ p a = false

Proof state:
case mpr.intro.intro.refine_2
s n i : Nat
p : Nat → Bool
h : p i = true
h₃ : ∀ (j : Nat), s ≤ j → j < i → p j = false
h₁ : s ≤ i
h₂ : i < s + n
a : Nat
a₁ : s ≤ a
a₂ : a < s + (i - s)
⊢ p a = false

Tactic:
exact h₃ a a₁ (by omega)

Result:
no goals

Proof state:
s n i : Nat
p : Nat → Bool
⊢ p i = true →
    ((∃ as, (∃ x, range' s n = as ++ i :: x) ∧ ∀ (a : Nat), a ∈ as → p a = false) ↔
      (s ≤ i ∧ i < s + n) ∧ ∀ (j : Nat), s ≤ j → j < i → p j = false)

Tactic:
simp only [range'_eq_append_iff, eq_comm (a := i :: _), range'_eq_cons_iff]

Result:
s n i : Nat
p : Nat → Bool
⊢ p i = true →
    ((∃ as,
        (∃ x k, k ≤ n ∧ as = range' s k ∧ s + k = i ∧ 0 < n - k ∧ x = range' (i + 1) (n - k - 1)) ∧
          ∀ (a : Nat), a ∈ as → p a = false) ↔
      (s ≤ i ∧ i < s + n) ∧ ∀ (j : Nat), s ≤ j → j < i → p j = false)

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.left
s n : Nat
p : Nat → Bool
k : Nat
h₁ : k ≤ n
h₃ : ∀ (a : Nat), a ∈ range' s k → p a = false
h : p (s + k) = true
h₂ : 0 < n - k
⊢ s ≤ s + k ∧ s + k < s + n

Tactic:
omega

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
s n : Nat
p : Nat → Bool
k : Nat
h₁ : k ≤ n
h₃ : ∀ (a : Nat), a ∈ range' s k → p a = false
h : p (s + k) = true
h₂ : 0 < n - k
⊢ (s ≤ s + k ∧ s + k < s + n) ∧ ∀ (j : Nat), s ≤ j → j < s + k → p j = false

Tactic:
constructor

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.left
s n : Nat
p : Nat → Bool
k : Nat
h₁ : k ≤ n
h₃ : ∀ (a : Nat), a ∈ range' s k → p a = false
h : p (s + k) = true
h₂ : 0 < n - k
⊢ s ≤ s + k ∧ s + k < s + n

case mp.intro.intro.intro.intro.intro.intro.intro.intro.right
s n : Nat
p : Nat → Bool
k : Nat
h₁ : k ≤ n
h₃ : ∀ (a : Nat), a ∈ range' s k → p a = false
h : p (s + k) = true
h₂ : 0 < n - k
⊢ ∀ (j : Nat), s ≤ j → j < s + k → p j = false

Proof state:
case mpr.intro.intro.refine_1
s n i : Nat
p : Nat → Bool
h : p i = true
h₃ : ∀ (j : Nat), s ≤ j → j < i → p j = false
h₁ : s ≤ i
h₂ : i < s + n
⊢ i - s ≤ n ∧ s + (i - s) = i ∧ 0 < n - (i - s)

Tactic:
omega

Result:
no goals

Proof state:
s n i : Nat
p : Nat → Bool
⊢ (p i = true ∧ ∃ as bs, range' s n = as ++ i :: bs ∧ ∀ (a : Nat), a ∈ as → (!p a) = true) ↔
    p i = true ∧ i ∈ range' s n ∧ ∀ (j : Nat), s ≤ j → j < i → (!p j) = true

Tactic:
simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, mem_range'_1,
  and_congr_right_iff]

Result:
s n i : Nat
p : Nat → Bool
⊢ p i = true →
    ((∃ as, (∃ x, range' s n = as ++ i :: x) ∧ ∀ (a : Nat), a ∈ as → p a = false) ↔
      (s ≤ i ∧ i < s + n) ∧ ∀ (j : Nat), s ≤ j → j < i → p j = false)

Proof state:
s n i : Nat
p : Nat → Bool
⊢ find? p (range' s n) = some i ↔ p i = true ∧ i ∈ range' s n ∧ ∀ (j : Nat), s ≤ j → j < i → (!p j) = true

Tactic:
rw [find?_eq_some_iff_append]

Result:
s n i : Nat
p : Nat → Bool
⊢ (p i = true ∧ ∃ as bs, range' s n = as ++ i :: bs ∧ ∀ (a : Nat), a ∈ as → (!p a) = true) ↔
    p i = true ∧ i ∈ range' s n ∧ ∀ (j : Nat), s ≤ j → j < i → (!p j) = true

Proof state:
s n i : Nat
p : Nat → Bool
h : p i = true
⊢ (∃ as,
      (∃ x k, k ≤ n ∧ as = range' s k ∧ s + k = i ∧ 0 < n - k ∧ x = range' (i + 1) (n - k - 1)) ∧
        ∀ (a : Nat), a ∈ as → p a = false) ↔
    (s ≤ i ∧ i < s + n) ∧ ∀ (j : Nat), s ≤ j → j < i → p j = false

Tactic:
constructor

Result:
case mp
s n i : Nat
p : Nat → Bool
h : p i = true
⊢ (∃ as,
      (∃ x k, k ≤ n ∧ as = range' s k ∧ s + k = i ∧ 0 < n - k ∧ x = range' (i + 1) (n - k - 1)) ∧
        ∀ (a : Nat), a ∈ as → p a = false) →
    (s ≤ i ∧ i < s + n) ∧ ∀ (j : Nat), s ≤ j → j < i → p j = false

case mpr
s n i : Nat
p : Nat → Bool
h : p i = true
⊢ ((s ≤ i ∧ i < s + n) ∧ ∀ (j : Nat), s ≤ j → j < i → p j = false) →
    ∃ as,
      (∃ x k, k ≤ n ∧ as = range' s k ∧ s + k = i ∧ 0 < n - k ∧ x = range' (i + 1) (n - k - 1)) ∧
        ∀ (a : Nat), a ∈ as → p a = false

Proof state:
s n i : Nat
p : Nat → Bool
⊢ p i = true →
    ((∃ as,
        (∃ x k, k ≤ n ∧ as = range' s k ∧ s + k = i ∧ 0 < n - k ∧ x = range' (i + 1) (n - k - 1)) ∧
          ∀ (a : Nat), a ∈ as → p a = false) ↔
      (s ≤ i ∧ i < s + n) ∧ ∀ (j : Nat), s ≤ j → j < i → p j = false)

Tactic:
intro h

Result:
s n i : Nat
p : Nat → Bool
h : p i = true
⊢ (∃ as,
      (∃ x k, k ≤ n ∧ as = range' s k ∧ s + k = i ∧ 0 < n - k ∧ x = range' (i + 1) (n - k - 1)) ∧
        ∀ (a : Nat), a ∈ as → p a = false) ↔
    (s ≤ i ∧ i < s + n) ∧ ∀ (j : Nat), s ≤ j → j < i → p j = false

Proof state:
case mpr.intro.intro
s n i : Nat
p : Nat → Bool
h : p i = true
h₃ : ∀ (j : Nat), s ≤ j → j < i → p j = false
h₁ : s ≤ i
h₂ : i < s + n
⊢ ∃ as,
    (∃ x k, k ≤ n ∧ as = range' s k ∧ s + k = i ∧ 0 < n - k ∧ x = range' (i + 1) (n - k - 1)) ∧
      ∀ (a : Nat), a ∈ as → p a = false

Tactic:
refine ⟨range' s (i - s), ⟨⟨range' (i + 1) (n - (i - s) - 1), i - s, ?_⟩ , ?_⟩⟩

Result:
case mpr.intro.intro.refine_1
s n i : Nat
p : Nat → Bool
h : p i = true
h₃ : ∀ (j : Nat), s ≤ j → j < i → p j = false
h₁ : s ≤ i
h₂ : i < s + n
⊢ i - s ≤ n ∧
    range' s (i - s) = range' s (i - s) ∧
      s + (i - s) = i ∧ 0 < n - (i - s) ∧ range' (i + 1) (n - (i - s) - 1) = range' (i + 1) (n - (i - s) - 1)

case mpr.intro.intro.refine_2
s n i : Nat
p : Nat → Bool
h : p i = true
h₃ : ∀ (j : Nat), s ≤ j → j < i → p j = false
h₁ : s ≤ i
h₂ : i < s + n
⊢ ∀ (a : Nat), a ∈ range' s (i - s) → p a = false

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.right
s n : Nat
p : Nat → Bool
k : Nat
h₁ : k ≤ n
h₃ : ∀ (a : Nat), a ∈ range' s k → p a = false
h : p (s + k) = true
h₂ : 0 < n - k
⊢ ∀ (j : Nat), s ≤ j → j < s + k → p j = false

Tactic:
simpa using h₃

Result:
no goals

Proof state:
case mp
s n i : Nat
p : Nat → Bool
h : p i = true
⊢ (∃ as,
      (∃ x k, k ≤ n ∧ as = range' s k ∧ s + k = i ∧ 0 < n - k ∧ x = range' (i + 1) (n - k - 1)) ∧
        ∀ (a : Nat), a ∈ as → p a = false) →
    (s ≤ i ∧ i < s + n) ∧ ∀ (j : Nat), s ≤ j → j < i → p j = false

Tactic:
rintro ⟨as, ⟨x, k, h₁, rfl, rfl, h₂, rfl⟩, h₃⟩

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
s n : Nat
p : Nat → Bool
k : Nat
h₁ : k ≤ n
h₃ : ∀ (a : Nat), a ∈ range' s k → p a = false
h : p (s + k) = true
h₂ : 0 < n - k
⊢ (s ≤ s + k ∧ s + k < s + n) ∧ ∀ (j : Nat), s ≤ j → j < s + k → p j = false

Proof state:
case mpr.intro.intro.refine_2
s n i : Nat
p : Nat → Bool
h : p i = true
h₃ : ∀ (j : Nat), s ≤ j → j < i → p j = false
h₁ : s ≤ i
h₂ : i < s + n
⊢ ∀ (a : Nat), a ∈ range' s (i - s) → p a = false

Tactic:
simp only [mem_range'_1, and_imp]

Result:
case mpr.intro.intro.refine_2
s n i : Nat
p : Nat → Bool
h : p i = true
h₃ : ∀ (j : Nat), s ≤ j → j < i → p j = false
h₁ : s ≤ i
h₂ : i < s + n
⊢ ∀ (a : Nat), s ≤ a → a < s + (i - s) → p a = false