α : Type u_1
β : Type u_2
ι : Type ?u.132367
M : Type u_3
N : Type ?u.132373
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
⊢ (if x ∈ s ∧ y ∈ t then OfNat.ofNat 1 (x, y) else 0) =
    (if x ∈ s then OfNat.ofNat 1 x else 0) * if y ∈ t then OfNat.ofNat 1 y else 0
α : Type u_1
β : Type u_2
ι : Type ?u.132367
M : Type u_3
N : Type ?u.132373
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
⊢ indicator (s ×ˢ t) 1 (x, y) = indicator s 1 x * indicator t 1 y
simp_rw [indicator, mem_prod_eq]
no goals
α : Type u_1
β : Type u_2
ι : Type ?u.132367
M : Type u_3
N : Type ?u.132373
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
⊢ (if x ∈ s ∧ y ∈ t then OfNat.ofNat 1 (x, y) else 0) =
    (if x ∈ s then OfNat.ofNat 1 x else 0) * if y ∈ t then OfNat.ofNat 1 y else 0
split_ifs with h₀ <;> simp only [Pi.one_apply, mul_one, mul_zero] <;> tauto