case h
α : Type u_1
β : Type ?u.96997
ι : Type ?u.97000
M : Type ?u.97003
N : Type ?u.97006
G : Type u_2
inst✝ : Group G
s t : Set α
f✝ g : α → G
a : α
h : s ⊆ t
f : α → G
⊢ Disjoint (t \ s) s
α : Type u_1
β : Type ?u.96997
ι : Type ?u.97000
M : Type ?u.97003
N : Type ?u.97006
G : Type u_2
inst✝ : Group G
s t : Set α
f✝ g : α → G
a : α
h : s ⊆ t
f : α → G
⊢ mulIndicator (t \ s) f * mulIndicator s f = mulIndicator t f
rw [Pi.mul_def, ← mulIndicator_union_of_disjoint, diff_union_self,
  union_eq_self_of_subset_right h]
no goals
case h
α : Type u_1
β : Type ?u.96997
ι : Type ?u.97000
M : Type ?u.97003
N : Type ?u.97006
G : Type u_2
inst✝ : Group G
s t : Set α
f✝ g : α → G
a : α
h : s ⊆ t
f : α → G
⊢ Disjoint (t \ s) s
exact disjoint_sdiff_self_left