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

case inl.inl.inr
α : Type u_1
β : Type ?u.12298
ι : Type ?u.12301
M : Type u_2
N : Type ?u.12307
inst✝¹ : One M
inst✝ : One N
s✝ t✝ : Set α
f✝ g : α → M
a : α
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : x ∈ t
h✝ : ¬x ∈ s ∩ t
⊢ f x = 1

case inl.inr.inl
α : Type u_1
β : Type ?u.12298
ι : Type ?u.12301
M : Type u_2
N : Type ?u.12307
inst✝¹ : One M
inst✝ : One N
s✝ t✝ : Set α
f✝ g : α → M
a : α
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : ¬x ∈ t
h✝ : x ∈ s ∩ t
⊢ 1 = f x

case inl.inr.inr
α : Type u_1
β : Type ?u.12298
ι : Type ?u.12301
M : Type u_2
N : Type ?u.12307
inst✝¹ : One M
inst✝ : One N
s✝ t✝ : Set α
f✝ g : α → M
a : α
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : ¬x ∈ t
h✝ : ¬x ∈ s ∩ t
⊢ 1 = 1

case inr.inl
α : Type u_1
β : Type ?u.12298
ι : Type ?u.12301
M : Type u_2
N : Type ?u.12307
inst✝¹ : One M
inst✝ : One N
s✝ t✝ : Set α
f✝ g : α → M
a : α
s t : Set α
f : α → M
x : α
h✝¹ : ¬x ∈ s
h✝ : x ∈ s ∩ t
⊢ 1 = f x

case inr.inr
α : Type u_1
β : Type ?u.12298
ι : Type ?u.12301
M : Type u_2
N : Type ?u.12307
inst✝¹ : One M
inst✝ : One N
s✝ t✝ : Set α
f✝ g : α → M
a : α
s t : Set α
f : α → M
x : α
h✝¹ : ¬x ∈ s
h✝ : ¬x ∈ s ∩ t
⊢ 1 = 1
α : Type u_1
β : Type ?u.12298
ι : Type ?u.12301
M : Type u_2
N : Type ?u.12307
inst✝¹ : One M
inst✝ : One N
s✝ t✝ : Set α
f✝ g : α → M
a : α
s t : Set α
f : α → M
x : α
⊢ (if x ∈ s then if x ∈ t then f x else 1 else 1) = if x ∈ s ∩ t then f x else 1
split_ifs
no goals
case inl.inl.inl
α : Type u_1
β : Type ?u.12298
ι : Type ?u.12301
M : Type u_2
N : Type ?u.12307
inst✝¹ : One M
inst✝ : One N
s✝ t✝ : Set α
f✝ g : α → M
a : α
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : x ∈ t
h✝ : x ∈ s ∩ t
⊢ f x = f x

case inl.inl.inr
α : Type u_1
β : Type ?u.12298
ι : Type ?u.12301
M : Type u_2
N : Type ?u.12307
inst✝¹ : One M
inst✝ : One N
s✝ t✝ : Set α
f✝ g : α → M
a : α
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : x ∈ t
h✝ : ¬x ∈ s ∩ t
⊢ f x = 1

case inl.inr.inl
α : Type u_1
β : Type ?u.12298
ι : Type ?u.12301
M : Type u_2
N : Type ?u.12307
inst✝¹ : One M
inst✝ : One N
s✝ t✝ : Set α
f✝ g : α → M
a : α
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : ¬x ∈ t
h✝ : x ∈ s ∩ t
⊢ 1 = f x

case inl.inr.inr
α : Type u_1
β : Type ?u.12298
ι : Type ?u.12301
M : Type u_2
N : Type ?u.12307
inst✝¹ : One M
inst✝ : One N
s✝ t✝ : Set α
f✝ g : α → M
a : α
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : ¬x ∈ t
h✝ : ¬x ∈ s ∩ t
⊢ 1 = 1

case inr.inl
α : Type u_1
β : Type ?u.12298
ι : Type ?u.12301
M : Type u_2
N : Type ?u.12307
inst✝¹ : One M
inst✝ : One N
s✝ t✝ : Set α
f✝ g : α → M
a : α
s t : Set α
f : α → M
x : α
h✝¹ : ¬x ∈ s
h✝ : x ∈ s ∩ t
⊢ 1 = f x

case inr.inr
α : Type u_1
β : Type ?u.12298
ι : Type ?u.12301
M : Type u_2
N : Type ?u.12307
inst✝¹ : One M
inst✝ : One N
s✝ t✝ : Set α
f✝ g : α → M
a : α
s t : Set α
f : α → M
x : α
h✝¹ : ¬x ∈ s
h✝ : ¬x ∈ s ∩ t
⊢ 1 = 1
repeat' simp_all (config := { contextual := true })
no goals
case inr.inr
α : Type u_1
β : Type ?u.12298
ι : Type ?u.12301
M : Type u_2
N : Type ?u.12307
inst✝¹ : One M
inst✝ : One N
s✝ t✝ : Set α
f✝ g : α → M
a : α
s t : Set α
f : α → M
x : α
h✝¹ : ¬x ∈ s
h✝ : ¬x ∈ s ∩ t
⊢ 1 = 1
simp_all (config := { contextual := true })