-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_flatten {l : List (List α)} {p : α → Bool} :
    l.flatten.findIdx? p =
      (l.findIdx? (·.any p)).map
        fun i => ((l.take i).map List.length).sum +
          (l[i]?.map fun xs => xs.findIdx p).getD 0

Proof state:
case cons.isTrue
α : Type u_1
p : α → Bool
xs : List α
l : List (List α)
ih :
  findIdx? p l.flatten =
    Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)
h : ∃ x, x ∈ xs ∧ p x = true
⊢ (findIdx? p xs).or
      (Option.map (fun i => i + xs.length)
        (Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
          (findIdx? (fun x => x.any p) l))) =
    Option.map
      (fun i => (map length (take i (xs :: l))).sum + (Option.map (fun xs => findIdx p xs) (xs :: l)[i]?).getD 0)
      (some 0)

Tactic:
rw [Option.or_of_isSome (by simp_all [findIdx?_isSome])]

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
xs : List α
l : List (List α)
ih :
  findIdx? p l.flatten =
    Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)
h : ∃ x, x ∈ xs ∧ p x = true
⊢ findIdx? p xs =
    Option.map
      (fun i => (map length (take i (xs :: l))).sum + (Option.map (fun xs => findIdx p xs) (xs :: l)[i]?).getD 0)
      (some 0)

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ findIdx? p [].flatten =
    Option.map (fun i => (map length (take i [])).sum + (Option.map (fun xs => findIdx p xs) [][i]?).getD 0)
      (findIdx? (fun x => x.any p) [])

Tactic:
simp

Result:
no goals

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
xs : List α
l : List (List α)
ih :
  findIdx? p l.flatten =
    Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)
h : ¬xs.any p = true
⊢ Option.map (fun i => i + xs.length)
      (Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
        (findIdx? (fun x => x.any p) l)) =
    Option.map
      (fun i => (map length (take i (xs :: l))).sum + (Option.map (fun xs => findIdx p xs) (xs :: l)[i]?).getD 0)
      (Option.map (fun i => i + 1) (findIdx? (fun x => x.any p) l))

Tactic:
simp [Function.comp_def, Nat.add_comm, Nat.add_assoc]

Result:
no goals

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
xs : List α
l : List (List α)
ih :
  findIdx? p l.flatten =
    Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)
h : ¬xs.any p = true
⊢ (findIdx? p xs).or
      (Option.map (fun i => i + xs.length)
        (Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
          (findIdx? (fun x => x.any p) l))) =
    Option.map
      (fun i => (map length (take i (xs :: l))).sum + (Option.map (fun xs => findIdx p xs) (xs :: l)[i]?).getD 0)
      (Option.map (fun i => i + 1) (findIdx? (fun x => x.any p) l))

Tactic:
rw [Option.or_of_isNone (by simp_all [findIdx?_isNone])]

Result:
case cons.isFalse
α : Type u_1
p : α → Bool
xs : List α
l : List (List α)
ih :
  findIdx? p l.flatten =
    Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)
h : ¬xs.any p = true
⊢ Option.map (fun i => i + xs.length)
      (Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
        (findIdx? (fun x => x.any p) l)) =
    Option.map
      (fun i => (map length (take i (xs :: l))).sum + (Option.map (fun xs => findIdx p xs) (xs :: l)[i]?).getD 0)
      (Option.map (fun i => i + 1) (findIdx? (fun x => x.any p) l))

Proof state:
case cons
α : Type u_1
p : α → Bool
xs : List α
l : List (List α)
ih :
  findIdx? p l.flatten =
    Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)
⊢ findIdx? p (xs :: l).flatten =
    Option.map
      (fun i => (map length (take i (xs :: l))).sum + (Option.map (fun xs => findIdx p xs) (xs :: l)[i]?).getD 0)
      (findIdx? (fun x => x.any p) (xs :: l))

Tactic:
rw [flatten_cons, findIdx?_append, ih, findIdx?_cons]

Result:
case cons
α : Type u_1
p : α → Bool
xs : List α
l : List (List α)
ih :
  findIdx? p l.flatten =
    Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)
⊢ (findIdx? p xs).or
      (Option.map (fun i => i + xs.length)
        (Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
          (findIdx? (fun x => x.any p) l))) =
    Option.map
      (fun i => (map length (take i (xs :: l))).sum + (Option.map (fun xs => findIdx p xs) (xs :: l)[i]?).getD 0)
      (if xs.any p = true then some 0 else Option.map (fun i => i + 1) (findIdx? (fun x => x.any p) l))

Proof state:
α : Type u_1
p : α → Bool
xs : List α
l : List (List α)
ih :
  findIdx? p l.flatten =
    Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)
h : ∃ x, x ∈ xs ∧ p x = true
⊢ (findIdx? p xs).isSome = true

Tactic:
simp_all [findIdx?_isSome]

Result:
no goals

Proof state:
case cons.isTrue
α : Type u_1
p : α → Bool
xs : List α
l : List (List α)
ih :
  findIdx? p l.flatten =
    Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)
h : ∃ x, x ∈ xs ∧ p x = true
⊢ findIdx? p xs =
    Option.map
      (fun i => (map length (take i (xs :: l))).sum + (Option.map (fun xs => findIdx p xs) (xs :: l)[i]?).getD 0)
      (some 0)

Tactic:
simp_all [findIdx?_eq_some_of_exists]

Result:
no goals

Proof state:
case cons.isTrue
α : Type u_1
p : α → Bool
xs : List α
l : List (List α)
ih :
  findIdx? p l.flatten =
    Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)
h : xs.any p = true
⊢ (findIdx? p xs).or
      (Option.map (fun i => i + xs.length)
        (Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
          (findIdx? (fun x => x.any p) l))) =
    Option.map
      (fun i => (map length (take i (xs :: l))).sum + (Option.map (fun xs => findIdx p xs) (xs :: l)[i]?).getD 0)
      (some 0)

Tactic:
simp only [any_eq_true] at h

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
xs : List α
l : List (List α)
ih :
  findIdx? p l.flatten =
    Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)
h : ∃ x, x ∈ xs ∧ p x = true
⊢ (findIdx? p xs).or
      (Option.map (fun i => i + xs.length)
        (Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
          (findIdx? (fun x => x.any p) l))) =
    Option.map
      (fun i => (map length (take i (xs :: l))).sum + (Option.map (fun xs => findIdx p xs) (xs :: l)[i]?).getD 0)
      (some 0)