Theorem: Fin.exists_eq_true_of_any_eq_true (Extra/Fin.lean)

State before:
x✝ : Fin 0 → Bool
h : Fin.any x✝ = true
⊢ ∃ i, x✝ i = true
Tactic:
simp at h
State after:
no goals

State before:
n : Nat
p : Fin (n + 1) → Bool
h : Fin.any p = true
⊢ ∃ i, p i = true
Tactic:
rw [Fin.any, Fin.foldr_succ, Bool.or_eq_true] at h
State after:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = true ∨ foldr n (fun i v => p i.succ || v) false = true
⊢ ∃ i, p i = true

State before:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = true ∨ foldr n (fun i v => p i.succ || v) false = true
⊢ ∃ i, p i = true
Tactic:
match h with
| .inl h => exists ⟨0, Nat.zero_lt_succ n⟩
| .inr h => match exists_eq_true_of_any_eq_true h with
  | ⟨⟨i,hi⟩,hp⟩ => exists ⟨i+1, Nat.succ_lt_succ hi⟩
State after:
no goals

State before:
n : Nat
p : Fin (n + 1) → Bool
h✝ : p 0 = true ∨ foldr n (fun i v => p i.succ || v) false = true
h : p 0 = true
⊢ ∃ i, p i = true
Tactic:
exists ⟨0, Nat.zero_lt_succ n⟩
State after:
no goals

State before:
n : Nat
p : Fin (n + 1) → Bool
h✝ : p 0 = true ∨ foldr n (fun i v => p i.succ || v) false = true
h : foldr n (fun i v => p i.succ || v) false = true
⊢ ∃ i, p i = true
Tactic:
match exists_eq_true_of_any_eq_true h with
| ⟨⟨i,hi⟩,hp⟩ => exists ⟨i+1, Nat.succ_lt_succ hi⟩
State after:
no goals

State before:
n : Nat
p : Fin (n + 1) → Bool
h✝ : p 0 = true ∨ foldr n (fun i v => p i.succ || v) false = true
h : foldr n (fun i v => p i.succ || v) false = true
i : Nat
hi : i < n
hp : p ⟨i, hi⟩.succ = true
⊢ ∃ i, p i = true
Tactic:
exists ⟨i+1, Nat.succ_lt_succ hi⟩
State after:
no goals