case pos
α : Type u_1
β : Type u_2
γ : Type ?u.388219
δ : Type ?u.388222
ι : Type ?u.388225
R : Type ?u.388228
R' : Type ?u.388231
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Injective f
s : Set β
hs : Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.388219
δ : Type ?u.388222
ι : Type ?u.388225
R : Type ?u.388228
R' : Type ?u.388231
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Injective f
s : Set β
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s
α : Type u_1
β : Type u_2
γ : Type ?u.388219
δ : Type ?u.388222
ι : Type ?u.388225
R : Type ?u.388228
R' : Type ?u.388231
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Injective f
s : Set β
⊢ ↑↑count (f '' s) = ↑↑count s
by_cases hs : s.Finite
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.388219
δ : Type ?u.388222
ι : Type ?u.388225
R : Type ?u.388228
R' : Type ?u.388231
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Injective f
s : Set β
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ⊤
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.388219
δ : Type ?u.388222
ι : Type ?u.388225
R : Type ?u.388228
R' : Type ?u.388231
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Injective f
s : Set β
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s
rw [count_apply_infinite hs]
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.388219
δ : Type ?u.388222
ι : Type ?u.388225
R : Type ?u.388228
R' : Type ?u.388231
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Injective f
s : Set β
hs : ¬Set.Finite (f '' s)
⊢ ↑↑count (f '' s) = ⊤
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.388219
δ : Type ?u.388222
ι : Type ?u.388225
R : Type ?u.388228
R' : Type ?u.388231
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Injective f
s : Set β
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ⊤
rw [← finite_image_iff <| hf.injOn _] at hs
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.388219
δ : Type ?u.388222
ι : Type ?u.388225
R : Type ?u.388228
R' : Type ?u.388231
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Injective f
s : Set β
hs : ¬Set.Finite (f '' s)
⊢ ↑↑count (f '' s) = ⊤
rw [count_apply_infinite hs]
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.388219
δ : Type ?u.388222
ι : Type ?u.388225
R : Type ?u.388228
R' : Type ?u.388231
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Injective f
s : Set β
hs : Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s
exact count_injective_image' hf hs.measurableSet (Finite.image f hs).measurableSet