α : Type u_1
β : Type ?u.9864
ι : Type ?u.9867
M : Type u_2
N : Type ?u.9873
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
h : EqOn f g s
x : α
⊢ (if x ∈ s then f x else 1) = if x ∈ s then g x else 1
α : Type u_1
β : Type ?u.9864
ι : Type ?u.9867
M : Type u_2
N : Type ?u.9873
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
h : EqOn f g s
x : α
⊢ mulIndicator s f x = mulIndicator s g x
simp only [mulIndicator]
case inl
α : Type u_1
β : Type ?u.9864
ι : Type ?u.9867
M : Type u_2
N : Type ?u.9873
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
h : EqOn f g s
x : α
h_1 : x ∈ s
⊢ f x = g x

case inr
α : Type u_1
β : Type ?u.9864
ι : Type ?u.9867
M : Type u_2
N : Type ?u.9873
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
h : EqOn f g s
x : α
h_1 : ¬x ∈ s
⊢ 1 = 1
α : Type u_1
β : Type ?u.9864
ι : Type ?u.9867
M : Type u_2
N : Type ?u.9873
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
h : EqOn f g s
x : α
⊢ (if x ∈ s then f x else 1) = if x ∈ s then g x else 1
split_ifs with h_1
no goals
case inr
α : Type u_1
β : Type ?u.9864
ι : Type ?u.9867
M : Type u_2
N : Type ?u.9873
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
h : EqOn f g s
x : α
h_1 : ¬x ∈ s
⊢ 1 = 1
rfl
no goals
case inl
α : Type u_1
β : Type ?u.9864
ι : Type ?u.9867
M : Type u_2
N : Type ?u.9873
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
h : EqOn f g s
x : α
h_1 : x ∈ s
⊢ f x = g x
exact h h_1