[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
h : Nonempty α
inst✝ : IsEmpty β
⊢ IsEmpty (α → β)
[PROOFSTEP]
infer_instance
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
p : Prop
⊢ IsEmpty p ↔ ¬p
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_Prop]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
π : α → Sort u_4
⊢ IsEmpty ((a : α) → π a) ↔ ∃ a, IsEmpty (π a)
[PROOFSTEP]
simp only [← not_nonempty_iff, Classical.nonempty_pi, not_forall]
[GOAL]
α✝ : Sort u_1
β : Sort u_2
γ : Sort u_3
α : Type u_5
E : α → Type u_4
⊢ IsEmpty (Sigma E) ↔ ∀ (a : α), IsEmpty (E a)
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_sigma, not_exists]
[GOAL]
α✝ : Sort u_1
β : Sort u_2
γ : Sort u_3
α : Sort u_5
E : α → Sort u_4
⊢ IsEmpty (PSigma E) ↔ ∀ (a : α), IsEmpty (E a)
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_psigma, not_exists]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
⊢ IsEmpty (Subtype p) ↔ ∀ (x : α), ¬p x
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_subtype, not_exists]
[GOAL]
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
α : Type u_4
β : Type u_5
⊢ IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_prod, not_and_or]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
⊢ IsEmpty (PProd α β) ↔ IsEmpty α ∨ IsEmpty β
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_pprod, not_and_or]
[GOAL]
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
α : Type u_4
β : Type u_5
⊢ IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_sum, not_or]
[GOAL]
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
α : Sort u_4
β : Sort u_5
⊢ IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_psum, not_or]
[GOAL]
α✝ : Sort u_1
β : Sort u_2
γ : Sort u_3
α : Type u_4
⊢ IsEmpty (ULift α) ↔ IsEmpty α
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_ulift]
[GOAL]
α✝ : Sort u_1
β : Sort u_2
γ : Sort u_3
α : Sort u_4
⊢ IsEmpty (PLift α) ↔ IsEmpty α
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_plift]
