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

State before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
⊢ decide (∃ x, p x) = Finite.any fun x => decide (p x)
Tactic:
match h : Finite.any fun x => decide (p x) with
| true =>
  apply decide_eq_true
  match exists_eq_true_of_any_eq_true h with
  | ⟨x, hx⟩ =>
    exists x
    exact of_decide_eq_true hx
| false =>
  apply decide_eq_false
  intro ⟨x, hx⟩
  absurd forall_eq_false_of_any_eq_false h x
  rw [decide_eq_true hx]
  trivial
State after:
no goals

State before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any 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.any 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.any fun x => decide (p x)) = true
⊢ ∃ x, p x
Tactic:
match exists_eq_true_of_any_eq_true h with
| ⟨x, hx⟩ =>
  exists x
  exact of_decide_eq_true hx
State after:
no goals

State before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = true
x : α
hx : decide (p x) = true
⊢ ∃ x, p x
Tactic:
exists x
State after:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = true
x : α
hx : decide (p x) = true
⊢ p x

State before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = true
x : α
hx : decide (p x) = true
⊢ p x
Tactic:
exact of_decide_eq_true hx
State after:
no goals

State before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any 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.any 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.any fun x => decide (p x)) = false
⊢ ¬∃ x, p x
Tactic:
intro ⟨x, hx⟩
State after:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
x : α
hx : p x
⊢ False

State before:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
x : α
hx : p x
⊢ False
Tactic:
absurd forall_eq_false_of_any_eq_false h x
State after:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
x : α
hx : p x
⊢ ¬decide (p x) = false

State before:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
x : α
hx : p x
⊢ ¬decide (p x) = false
Tactic:
rw [decide_eq_true hx]
State after:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
x : α
hx : p x
⊢ ¬true = false

State before:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
x : α
hx : p x
⊢ ¬true = false
Tactic:
trivial
State after:
no goals