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

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

Tactic:
simp

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

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

Tactic:
rw [eq_comm, range'_eq_cons_iff, reverse_eq_iff] at h₂

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

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

Tactic:
omega

Result:
no goals

Proof state:
case mp.intro.intro.intro.left
n i : Nat
p : Nat → Bool
h✝ : p i = true
as : List Nat
h' : ∀ (a : Nat), a ∈ as → p a = false
xs : List Nat
h : i ∈ range' 1 n
⊢ 1 ≤ i ∧ i < 1 + n

Tactic:
simpa using h

Result:
no goals

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

Tactic:
intro j j₁ j₂

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

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

Tactic:
intro h

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

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

Tactic:
rw [find?_eq_some_iff_append]

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

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

Tactic:
rintro ⟨as, ⟨xs, h⟩, h'⟩

Result:
case mp.intro.intro.intro
n i : Nat
p : Nat → Bool
h✝ : p i = true
as : List Nat
h' : ∀ (a : Nat), a ∈ as → p a = false
xs : List Nat
h : range' 1 n = xs.reverse ++ i :: as.reverse
⊢ (1 ≤ i ∧ i < 1 + n) ∧ ∀ (j : Nat), i < j → j ≤ n → p j = false

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

Tactic:
constructor

Result:
case mpr.intro.intro.refine_1.left
n i : Nat
p : Nat → Bool
h✝ : p i = true
h : ∀ (j : Nat), i < j → j ≤ n → p j = false
i₁ : 1 ≤ i
i₂ : i < 1 + n
⊢ i - 1 ≤ n

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

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

Tactic:
constructor

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

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

Proof state:
case mpr.intro.intro.refine_1
n i : Nat
p : Nat → Bool
h✝ : p i = true
h : ∀ (j : Nat), i < j → j ≤ n → p j = false
i₁ : 1 ≤ i
i₂ : i < 1 + n
⊢ range' 1 n = range' 1 (i - 1) ++ range' i (n - i + 1)

Tactic:
rw [range'_eq_append_iff]

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

Proof state:
case mpr.intro.intro.refine_1
n i : Nat
p : Nat → Bool
h✝ : p i = true
h : ∀ (j : Nat), i < j → j ≤ n → p j = false
i₁ : 1 ≤ i
i₂ : i < 1 + n
⊢ ∃ k, k ≤ n ∧ range' 1 (i - 1) = range' 1 k ∧ range' i (n - i + 1) = range' (1 + k) (n - k)

Tactic:
refine ⟨i-1, ?_⟩

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

Proof state:
case mp.intro.intro.intro.right
n i : Nat
p : Nat → Bool
h✝ : p i = true
as : List Nat
h' : ∀ (a : Nat), a ∈ as → p a = false
xs : List Nat
h : ∃ k, k ≤ n ∧ xs = (range' 1 k).reverse ∧ i :: as.reverse = range' (1 + k) (n - k)
⊢ ∀ (j : Nat), i < j → j ≤ n → p j = false

Tactic:
obtain ⟨k, h₁, rfl, h₂⟩ := h

Result:
case mp.intro.intro.intro.right.intro.intro.intro
n i : Nat
p : Nat → Bool
h : p i = true
as : List Nat
h' : ∀ (a : Nat), a ∈ as → p a = false
k : Nat
h₁ : k ≤ n
h₂ : i :: as.reverse = range' (1 + k) (n - k)
⊢ ∀ (j : Nat), i < j → j ≤ n → p j = false

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

Tactic:
simp

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

Proof state:
case mp.intro.intro.intro.right
n i : Nat
p : Nat → Bool
h✝ : p i = true
as : List Nat
h' : ∀ (a : Nat), a ∈ as → p a = false
xs : List Nat
h : range' 1 n = xs.reverse ++ i :: as.reverse
⊢ ∀ (j : Nat), i < j → j ≤ n → p j = false

Tactic:
rw [range'_eq_append_iff] at h

Result:
case mp.intro.intro.intro.right
n i : Nat
p : Nat → Bool
h✝ : p i = true
as : List Nat
h' : ∀ (a : Nat), a ∈ as → p a = false
xs : List Nat
h : ∃ k, k ≤ n ∧ xs.reverse = range' 1 k ∧ i :: as.reverse = range' (1 + k) (n - k)
⊢ ∀ (j : Nat), i < j → j ≤ n → p j = false

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

Tactic:
omega

Result:
no goals