α : Type u_1
β : Type ?u.68899
ι : Type ?u.68902
M : Type u_2
N : Type ?u.68908
inst✝ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
⊢ (f * g) x = g x
α : Type u_1
β : Type ?u.68899
ι : Type ?u.68902
M : Type u_2
N : Type ?u.68908
inst✝ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
⊢ mulIndicator (mulSupport g) (f * g) = g
refine' (mulIndicator_congr fun x hx => _).trans mulIndicator_mulSupport
α : Type u_1
β : Type ?u.68899
ι : Type ?u.68902
M : Type u_2
N : Type ?u.68908
inst✝ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
⊢ (f * g) x = g x
α : Type u_1
β : Type ?u.68899
ι : Type ?u.68902
M : Type u_2
N : Type ?u.68908
inst✝ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
⊢ (f * g) x = g x
have : f x = 1 := nmem_mulSupport.1 (disjoint_right.1 h hx)
no goals
α : Type u_1
β : Type ?u.68899
ι : Type ?u.68902
M : Type u_2
N : Type ?u.68908
inst✝ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
⊢ (f * g) x = g x
rw [Pi.mul_apply, this, one_mul]