-- 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_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
⊢ n - i + 1 = n - (i - 1) ∧ i = 1 + (i - 1)

Tactic:
omega

Result:
no goals

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)
⊢ a ≤ n

Tactic:
omega

Result:
no goals

Proof state:
case mpr.intro.intro
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
⊢ ∃ as, (∃ x, range' 1 n = x.reverse ++ i :: as.reverse) ∧ ∀ (a : Nat), a ∈ as → p a = false

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

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
⊢ range' 1 n = (range' 1 (i - 1)).reverse.reverse ++ i :: (range' (i + 1) (n - i)).reverse.reverse

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

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.reverse = range' 1 k ∧ i :: as.reverse = range' (1 + k) (n - k)
⊢ ∀ (j : Nat), i < j → j ≤ n → p j = false

Tactic:
simp [reverse_eq_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 = (range' 1 k).reverse ∧ 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
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

Tactic:
obtain ⟨rfl, -, rfl⟩ := h₂

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), 1 + k < j → j ≤ n → p j = false

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 : range' 1 n = xs.reverse ++ i :: as.reverse
⊢ 1 ≤ i ∧ i < 1 + n

Tactic:
replace h : i ∈ range' 1 n := by
  rw [h]
  exact mem_append_cons_self

Result:
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

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)).reverse.reverse ++ i :: (range' (i + 1) (n - i)).reverse.reverse

Tactic:
simp [← range'_succ]

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
⊢ range' 1 n = range' 1 (i - 1) ++ range' i (n - i + 1)

Proof state:
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
⊢ i ∈ xs.reverse ++ i :: as.reverse

Tactic:
exact mem_append_cons_self

Result:
no goals

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₁ : i + 1 ≤ a
a₂ : a < i + 1 + (n - i)
⊢ p a = false

Tactic:
apply h

Result:
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

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)
⊢ a ≤ n

Proof state:
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

Tactic:
constructor

Result:
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 : range' 1 n = xs.reverse ++ i :: as.reverse
⊢ 1 ≤ i ∧ i < 1 + n

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

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
j₁ : 1 + k < j
j₂ : j ≤ n
⊢ p j = false

Tactic:
apply h'

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
⊢ j ∈ (range' (1 + k + 1) (n - k - 1)).reverse

Proof state:
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

Tactic:
simp only [iota_eq_reverse_range', reverse_eq_append_iff, reverse_cons, append_assoc, cons_append,
  nil_append, Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, mem_reverse, mem_range'_1,
  and_congr_right_iff]

Result:
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)

Proof state:
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
⊢ i ∈ range' 1 n

Tactic:
rw [h]

Result:
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
⊢ i ∈ xs.reverse ++ i :: as.reverse

Proof state:
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

Tactic:
rintro ⟨⟨i₁, i₂⟩, h⟩

Result:
case mpr.intro.intro
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
⊢ ∃ as, (∃ x, range' 1 n = x.reverse ++ i :: as.reverse) ∧ ∀ (a : Nat), a ∈ as → p a = false

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), i + 1 ≤ a → a < i + 1 + (n - i) → p a = false

Tactic:
intros a a₁ a₂

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
a₁ : i + 1 ≤ a
a₂ : a < i + 1 + (n - i)
⊢ p a = false