Theorem: Finite.forall_eq_false_of_any_eq_false (GMLInit/Class/Finite.lean)

State before:
α✝ : Type ?u.2776
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
⊢ Finite.any p = false → ∀ (x : α), p x = false
Tactic:
intro h x
State after:
α✝ : Type ?u.2776
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = false
x : α
⊢ p x = false

State before:
α✝ : Type ?u.2776
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = false
x : α
⊢ p x = false
Tactic:
have hany := Fin.forall_eq_false_of_any_eq_false h
State after:
α✝ : Type ?u.2776
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = false
x : α
hany : ∀ (i : Fin toArray.size), p (Finite.get α i) = false
⊢ p x = false

State before:
α✝ : Type ?u.2776
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = false
x : α
hany : ∀ (i : Fin toArray.size), p (Finite.get α i) = false
⊢ p x = false
Tactic:
rw [←hany (Finite.find x)]
State after:
α✝ : Type ?u.2776
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = false
x : α
hany : ∀ (i : Fin toArray.size), p (Finite.get α i) = false
⊢ p x = p (Finite.get α (find x))

State before:
α✝ : Type ?u.2776
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = false
x : α
hany : ∀ (i : Fin toArray.size), p (Finite.get α i) = false
⊢ p x = p (Finite.get α (find x))
Tactic:
rw [Finite.get_find]
State after:
no goals