m n : ℕ
α : Type u_1
β : Type ?u.7741
γ : Type ?u.7744
P : (Fin 0 → α) → Prop
⊢ P Fin.elim0' ↔ P finZeroElim
m n : ℕ
α : Type u_1
β : Type ?u.7741
γ : Type ?u.7744
P : (Fin 0 → α) → Prop
⊢ Exists P ↔ ∃ x, P x
simp only [Exists, Fin.exists_fin_zero_pi, Matrix.vecEmpty]
no goals
m n : ℕ
α : Type u_1
β : Type ?u.7741
γ : Type ?u.7744
P : (Fin 0 → α) → Prop
⊢ P Fin.elim0' ↔ P finZeroElim
rfl
no goals
m n✝ : ℕ
α : Type u_1
β : Type ?u.7741
γ : Type ?u.7744
n : ℕ
P : (Fin (Nat.succ n) → α) → Prop
⊢ Exists P ↔ ∃ x, P x
simp only [Exists, exists_iff, Fin.exists_fin_succ_pi, Matrix.vecCons]