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

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

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

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

State before:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h✝ : (Fin.all fun i => decide (p i)) = true
h : ∀ (i : Fin n), decide (p i) = true
⊢ ∀ (i : Fin n), p i
Tactic:
intro i
State after:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h✝ : (Fin.all fun i => decide (p i)) = true
h : ∀ (i : Fin n), decide (p i) = true
i : Fin n
⊢ p i

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

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

State before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h : (Fin.all fun i => decide (p i)) = false
⊢ decide (∀ (i : Fin n), p i) = false
Tactic:
match exists_eq_false_of_all_eq_false h with
| ⟨i, hi⟩ =>
  have hi := of_decide_eq_false hi
  apply decide_eq_false
  intro h
  apply hi
  exact h i
State after:
no goals

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

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

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

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

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