α : Type u_2
β : Type ?u.42764
ι : Type ?u.42767
M : Type u_1
N : Type ?u.42773
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
⊢ r (if a ∈ s then f a else 1) (if a ∈ s then g a else 1)
α : Type u_2
β : Type ?u.42764
ι : Type ?u.42767
M : Type u_1
N : Type ?u.42773
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
⊢ r (mulIndicator s f a) (mulIndicator s g a)
simp only [mulIndicator]
case inl
α : Type u_2
β : Type ?u.42764
ι : Type ?u.42767
M : Type u_1
N : Type ?u.42773
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : a ∈ s
⊢ r (f a) (g a)

case inr
α : Type u_2
β : Type ?u.42764
ι : Type ?u.42767
M : Type u_1
N : Type ?u.42773
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : ¬a ∈ s
⊢ r 1 1
α : Type u_2
β : Type ?u.42764
ι : Type ?u.42767
M : Type u_1
N : Type ?u.42773
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
⊢ r (if a ∈ s then f a else 1) (if a ∈ s then g a else 1)
split_ifs with has
no goals
case inl
α : Type u_2
β : Type ?u.42764
ι : Type ?u.42767
M : Type u_1
N : Type ?u.42773
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : a ∈ s
⊢ r (f a) (g a)

case inr
α : Type u_2
β : Type ?u.42764
ι : Type ?u.42767
M : Type u_1
N : Type ?u.42773
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : ¬a ∈ s
⊢ r 1 1
exacts [ha has, h1]