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

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

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

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

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