ι : Sort ?u.14066
α : Sort u_1
κ : ι → Sort ?u.14068
p q : α → Prop
b : Prop
ha : Nonempty α
a : α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b
ι : Sort ?u.14066
α : Sort u_1
κ : ι → Sort ?u.14068
p q : α → Prop
b : Prop
ha : Nonempty α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b
let ⟨a⟩ := ha
ι : Sort ?u.14066
α : Sort u_1
κ : ι → Sort ?u.14068
p q : α → Prop
b : Prop
ha : Nonempty α
a : α
h : (∀ (x : α), p x) → b
h' : ∀ (x : α), ¬(p x → b)
⊢ False
ι : Sort ?u.14066
α : Sort u_1
κ : ι → Sort ?u.14068
p q : α → Prop
b : Prop
ha : Nonempty α
a : α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b
refine ⟨fun h ↦ not_forall_not.1 fun h' ↦ ?_, fun ⟨x, hx⟩ h ↦ hx (h x)⟩
no goals
ι : Sort ?u.14066
α : Sort u_1
κ : ι → Sort ?u.14068
p q : α → Prop
b : Prop
ha : Nonempty α
a : α
h : (∀ (x : α), p x) → b
h' : ∀ (x : α), ¬(p x → b)
⊢ False
exact if hb : b then h' a fun _ ↦ hb else hb <| h fun x ↦ (not_imp.1 (h' x)).1