no goals
α : Type u_4
β : Type ?u.9665
A : Type ?u.9668
B : Type ?u.9671
M : Type u_2
N : Type u_3
P : Type u_1
R : Type ?u.9683
S : Type ?u.9686
G : Type ?u.9689
M₀ : Type ?u.9692
G₀ : Type ?u.9695
ι : Sort ?u.9698
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
op : M → N → P
op1 : op 1 1 = 1
f : α → M
g : α → N
x : α
hx : x ∈ mulSupport fun x => op (f x) (g x)
hf : f x = 1
hg : g x = 1
⊢ (fun x => op (f x) (g x)) x = 1
simp only [hf, hg, op1]