Theorem: Set.mem_snd (SciLean/Mathlib/Set.lean)

State before:
α : Type u_1
β : Type u_2
a : α
y : β
A : Set (α × β)
⊢ (y ∈ A.snd a) = ((a, y) ∈ A)
Tactic:
rfl
State after:
no goals