-- Mathlib/MeasureTheory/Measure/Count.lean
theorem count_injective_image' {f : β → α} (hf : Function.Injective f) {s : Set β}
    (s_mble : MeasurableSet s) (fs_mble : MeasurableSet (f '' s)) : count (f '' s) = count s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
⊢ count (f '' s) = count s

Tactic:
by_cases hs : s.Finite

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : s.Finite
⊢ count (f '' s) = count s

case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬s.Finite
⊢ count (f '' s) = count s

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬(f '' s).Finite
⊢ count (f '' s) = ⊤

Tactic:
rw [count_apply_infinite hs]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ MeasurableSet ↑(Finset.image f s)

Tactic:
simpa only [Finset.coe_image] using fs_mble

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬s.Finite
⊢ count (f '' s) = count s

Tactic:
rw [count_apply_infinite hs]

Result:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬s.Finite
⊢ count (f '' s) = ⊤

Proof state:
case pos.intro
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ count (f '' ↑s) = count ↑s

Tactic:
rw [← Finset.coe_image, count_apply_finset' _, count_apply_finset' s_mble,
  s.card_image_of_injective hf]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ MeasurableSet ↑(Finset.image f s)

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬s.Finite
⊢ count (f '' s) = ⊤

Tactic:
rw [← finite_image_iff hf.injOn] at hs

Result:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬(f '' s).Finite
⊢ count (f '' s) = ⊤

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : s.Finite
⊢ count (f '' s) = count s

Tactic:
lift s to Finset β using hs

Result:
case pos.intro
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ count (f '' ↑s) = count ↑s