α : Sort u_1
p q : α → Prop
b : Prop
a' : α
⊢ (∃ a, p a ∧ b ∧ a = a') ↔ p a' ∧ b
α : Sort u_1
p q : α → Prop
b : Prop
a' : α
⊢ (∃ a, p a ∧ b ∧ a' = a) ↔ p a' ∧ b
(conv in _=_ => rw [eq_comm])
no goals
α : Sort u_1
p q : α → Prop
b : Prop
a' : α
⊢ (∃ a, p a ∧ b ∧ a = a') ↔ p a' ∧ b
simp
α : Sort u_1
p q : α → Prop
b : Prop
a' : α
⊢ (∃ a, p a ∧ b ∧ a = a') ↔ p a' ∧ b
α : Sort u_1
p q : α → Prop
b : Prop
a' : α
⊢ (∃ a, p a ∧ b ∧ a' = a) ↔ p a' ∧ b
conv in _=_ => rw [eq_comm]