case pos
α : Type u_2
β : Type u_1
γ : Type ?u.386958
δ : Type ?u.386961
ι : Type ?u.386964
R : Type ?u.386967
R' : Type ?u.386970
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
f : β → α
hf : Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s

case neg
α : Type u_2
β : Type u_1
γ : Type ?u.386958
δ : Type ?u.386961
ι : Type ?u.386964
R : Type ?u.386967
R' : Type ?u.386970
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
f : β → α
hf : Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s
α : Type u_2
β : Type u_1
γ : Type ?u.386958
δ : Type ?u.386961
ι : Type ?u.386964
R : Type ?u.386967
R' : Type ?u.386970
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
f : β → α
hf : Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
⊢ ↑↑count (f '' s) = ↑↑count s
by_cases hs : s.Finite
case pos.intro
α : Type u_2
β : Type u_1
γ : Type ?u.386958
δ : Type ?u.386961
ι : Type ?u.386964
R : Type ?u.386967
R' : Type ?u.386970
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
f : β → α
hf : Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ ↑↑count (f '' ↑s) = ↑↑count ↑s
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.386958
δ : Type ?u.386961
ι : Type ?u.386964
R : Type ?u.386967
R' : Type ?u.386970
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
f : β → α
hf : Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s
lift s to Finset β using hs
α : Type u_2
β : Type u_1
γ : Type ?u.386958
δ : Type ?u.386961
ι : Type ?u.386964
R : Type ?u.386967
R' : Type ?u.386970
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
f : β → α
hf : Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ MeasurableSet ↑(Finset.image f s)
case pos.intro
α : Type u_2
β : Type u_1
γ : Type ?u.386958
δ : Type ?u.386961
ι : Type ?u.386964
R : Type ?u.386967
R' : Type ?u.386970
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
f : β → α
hf : Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ ↑↑count (f '' ↑s) = ↑↑count ↑s
rw [← Finset.coe_image, count_apply_finset' _, count_apply_finset' s_mble,
  s.card_image_of_injective hf]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.386958
δ : Type ?u.386961
ι : Type ?u.386964
R : Type ?u.386967
R' : Type ?u.386970
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
f : β → α
hf : Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ MeasurableSet ↑(Finset.image f s)
simpa only [Finset.coe_image] using fs_mble
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.386958
δ : Type ?u.386961
ι : Type ?u.386964
R : Type ?u.386967
R' : Type ?u.386970
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
f : β → α
hf : Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ⊤
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.386958
δ : Type ?u.386961
ι : Type ?u.386964
R : Type ?u.386967
R' : Type ?u.386970
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
f : β → α
hf : Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s
rw [count_apply_infinite hs]
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.386958
δ : Type ?u.386961
ι : Type ?u.386964
R : Type ?u.386967
R' : Type ?u.386970
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
f : β → α
hf : Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬Set.Finite (f '' s)
⊢ ↑↑count (f '' s) = ⊤
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.386958
δ : Type ?u.386961
ι : Type ?u.386964
R : Type ?u.386967
R' : Type ?u.386970
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
f : β → α
hf : Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ⊤
rw [← finite_image_iff <| hf.injOn _] at hs
no goals
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.386958
δ : Type ?u.386961
ι : Type ?u.386964
R : Type ?u.386967
R' : Type ?u.386970
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
f : β → α
hf : Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬Set.Finite (f '' s)
⊢ ↑↑count (f '' s) = ⊤
rw [count_apply_infinite hs]