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

State before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
⊢ decide (∀ (x : α), p x) = Finite.all fun x => decide (p x)
Tactic:
match h : Finite.all fun x => decide (p x) with
| false =>
  apply decide_eq_false
  match exists_eq_false_of_all_eq_false h with
  | ⟨x, hx⟩ =>
    intro h
    rw [decide_eq_true (h x)] at hx
    contradiction
| true =>
  apply decide_eq_true
  intro x
  apply of_decide_eq_true
  apply forall_eq_true_of_all_eq_true h
State after:
no goals

State before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = false
⊢ decide (∀ (x : α), p x) = false
Tactic:
apply decide_eq_false
State after:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = false
⊢ ¬∀ (x : α), p x

State before:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = false
⊢ ¬∀ (x : α), p x
Tactic:
match exists_eq_false_of_all_eq_false h with
| ⟨x, hx⟩ =>
  intro h
  rw [decide_eq_true (h x)] at hx
  contradiction
State after:
no goals

State before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = false
x : α
hx : decide (p x) = false
⊢ ¬∀ (x : α), p x
Tactic:
intro h
State after:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h✝ : (Finite.all fun x => decide (p x)) = false
x : α
hx : decide (p x) = false
h : ∀ (x : α), p x
⊢ False

State before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h✝ : (Finite.all fun x => decide (p x)) = false
x : α
hx : decide (p x) = false
h : ∀ (x : α), p x
⊢ False
Tactic:
rw [decide_eq_true (h x)] at hx
State after:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h✝ : (Finite.all fun x => decide (p x)) = false
x : α
hx : true = false
h : ∀ (x : α), p x
⊢ False

State before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h✝ : (Finite.all fun x => decide (p x)) = false
x : α
hx : true = false
h : ∀ (x : α), p x
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
⊢ decide (∀ (x : α), p x) = true
Tactic:
apply decide_eq_true
State after:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
⊢ ∀ (x : α), p x

State before:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
⊢ ∀ (x : α), p x
Tactic:
intro x
State after:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
x : α
⊢ p x

State before:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
x : α
⊢ p x
Tactic:
apply of_decide_eq_true
State after:
case a.a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
x : α
⊢ decide (p x) = true

State before:
case a.a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
x : α
⊢ decide (p x) = true
Tactic:
apply forall_eq_true_of_all_eq_true h
State after:
no goals