α : Sort u_1
β : Sort ?u.35535
σ : α → Sort ?u.35531
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (∃ x, ¬B x = a) ↔ ∃ h, a ≠ B h
α : Sort u_1
β : Sort ?u.35535
σ : α → Sort ?u.35531
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ dite P (fun x => a) B ≠ a ↔ ∃ h, a ≠ B h
rw [Ne.def, dite_eq_left_iff, not_forall]
no goals
α : Sort u_1
β : Sort ?u.35535
σ : α → Sort ?u.35531
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (∃ x, ¬B x = a) ↔ ∃ h, a ≠ B h
exact exists_congr fun h ↦ by rw [ne_comm]
no goals
α : Sort u_1
β : Sort ?u.35535
σ : α → Sort ?u.35531
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
h : ¬P
⊢ ¬B h = a ↔ a ≠ B h
rw [ne_comm]