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

State before:
n : Nat
p : Fin (n + 1) → Bool
h : Fin.any p = false
isLt✝ : 0 < n + 1
⊢ p ⟨0, isLt✝⟩ = false
Tactic:
rw [Fin.any, Fin.foldr_succ, Bool.or_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) false = false
isLt✝ : 0 < n + 1
⊢ p ⟨0, isLt✝⟩ = false

State before:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = false ∧ foldr n (fun i v => p i.succ || v) false = false
isLt✝ : 0 < n + 1
⊢ p ⟨0, isLt✝⟩ = false
Tactic:
exact h.left
State after:
no goals

State before:
n : Nat
p : Fin (n + 1) → Bool
h : Fin.any p = false
i : Nat
hi : i + 1 < n + 1
⊢ p ⟨i + 1, hi⟩ = false
Tactic:
rw [Fin.any, Fin.foldr_succ, Bool.or_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) false = false
i : Nat
hi : i + 1 < n + 1
⊢ p ⟨i + 1, hi⟩ = false

State before:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = false ∧ foldr n (fun i v => p i.succ || v) false = false
i : Nat
hi : i + 1 < n + 1
⊢ p ⟨i + 1, hi⟩ = false
Tactic:
exact forall_eq_false_of_any_eq_false h.right ⟨i, Nat.lt_of_succ_lt_succ hi⟩
State after:
no goals