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

State before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
⊢ decide (∃ i, p i) = Fin.any fun i => decide (p i)
Tactic:
match h : Fin.any fun i => decide (p i) with
| true =>
  match exists_eq_true_of_any_eq_true h with
  | ⟨i, hi⟩ =>
    have hi := of_decide_eq_true hi
    apply decide_eq_true
    exists i
| false =>
  have h := forall_eq_false_of_any_eq_false h
  apply decide_eq_false
  intro ⟨i, hi⟩
  absurd hi
  apply of_decide_eq_false
  exact h i
State after:
no goals

State before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h : (Fin.any fun i => decide (p i)) = true
⊢ decide (∃ i, p i) = true
Tactic:
match exists_eq_true_of_any_eq_true h with
| ⟨i, hi⟩ =>
  have hi := of_decide_eq_true hi
  apply decide_eq_true
  exists i
State after:
no goals

State before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h : (Fin.any fun i => decide (p i)) = true
i : Fin n
hi : decide (p i) = true
⊢ decide (∃ i, p i) = true
Tactic:
have hi := of_decide_eq_true hi
State after:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h : (Fin.any fun i => decide (p i)) = true
i : Fin n
hi✝ : decide (p i) = true
hi : p i
⊢ decide (∃ i, p i) = true

State before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h : (Fin.any fun i => decide (p i)) = true
i : Fin n
hi✝ : decide (p i) = true
hi : p i
⊢ decide (∃ i, p i) = true
Tactic:
apply decide_eq_true
State after:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h : (Fin.any fun i => decide (p i)) = true
i : Fin n
hi✝ : decide (p i) = true
hi : p i
⊢ ∃ i, p i

State before:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h : (Fin.any fun i => decide (p i)) = true
i : Fin n
hi✝ : decide (p i) = true
hi : p i
⊢ ∃ i, p i
Tactic:
exists i
State after:
no goals

State before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h : (Fin.any fun i => decide (p i)) = false
⊢ decide (∃ i, p i) = false
Tactic:
have h := forall_eq_false_of_any_eq_false h
State after:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
⊢ decide (∃ i, p i) = false

State before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
⊢ decide (∃ i, p i) = false
Tactic:
apply decide_eq_false
State after:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
⊢ ¬∃ i, p i

State before:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
⊢ ¬∃ i, p i
Tactic:
intro ⟨i, hi⟩
State after:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
i : Fin n
hi : p i
⊢ False

State before:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
i : Fin n
hi : p i
⊢ False
Tactic:
absurd hi
State after:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
i : Fin n
hi : p i
⊢ ¬p i

State before:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
i : Fin n
hi : p i
⊢ ¬p i
Tactic:
apply of_decide_eq_false
State after:
case a.a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
i : Fin n
hi : p i
⊢ decide (p i) = false

State before:
case a.a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
i : Fin n
hi : p i
⊢ decide (p i) = false
Tactic:
exact h i
State after:
no goals