α : Type u_1
β : Type u_3
ι : Type ?u.20670
M : Type u_2
N : Type ?u.20676
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f : β → α
g : α → M
x : β
⊢ (if x ∈ f ⁻¹' s then g (f x) else 1) = if f x ∈ s then g (f x) else 1
α : Type u_1
β : Type u_3
ι : Type ?u.20670
M : Type u_2
N : Type ?u.20676
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f : β → α
g : α → M
x : β
⊢ mulIndicator (f ⁻¹' s) (g ∘ f) x = mulIndicator s g (f x)
simp only [mulIndicator, Function.comp]
no goals
α : Type u_1
β : Type u_3
ι : Type ?u.20670
M : Type u_2
N : Type ?u.20676
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f : β → α
g : α → M
x : β
⊢ (if x ∈ f ⁻¹' s then g (f x) else 1) = if f x ∈ s then g (f x) else 1
split_ifs with h h' h'' <;> first | rfl | contradiction
no goals
case inr.inr
α : Type u_1
β : Type u_3
ι : Type ?u.20670
M : Type u_2
N : Type ?u.20676
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f : β → α
g : α → M
x : β
h : ¬x ∈ f ⁻¹' s
h'' : ¬f x ∈ s
⊢ 1 = 1
rfl
no goals
case inr.inl
α : Type u_1
β : Type u_3
ι : Type ?u.20670
M : Type u_2
N : Type ?u.20676
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f : β → α
g : α → M
x : β
h : ¬x ∈ f ⁻¹' s
h'' : f x ∈ s
⊢ 1 = g (f x)
contradiction