Theorem: Fin.exists_eq_false_of_all_eq_false (Extra/Fin/Basic.lean)

State before:
p : Fin 0 → Bool
h : Fin.all p = false
⊢ ∃ i, p i = false
Tactic:
simp at h
State after:
no goals

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

State before:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = false ∨ foldr n (fun i v => p i.succ && v) true = false
⊢ ∃ i, p i = false
Tactic:
match h with
| .inl h => exists ⟨0, Nat.zero_lt_succ n⟩
| .inr h => match exists_eq_false_of_all_eq_false 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 = false ∨ foldr n (fun i v => p i.succ && v) true = false
h : p 0 = false
⊢ ∃ i, p i = false
Tactic:
exists ⟨0, Nat.zero_lt_succ n⟩
State after:
no goals

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