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

State before:
α : Type u_1
β : Type u_2
x : α
b : β
A : Set (α × β)
⊢ (x ∈ A.fst b) = ((x, b) ∈ A)
Tactic:
rfl
State after:
no goals