case pos
α : Type u_1
β : Type ?u.378850
γ : Type ?u.378853
δ : Type ?u.378856
ι : Type ?u.378859
R : Type ?u.378862
R' : Type ?u.378865
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
hs : Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s

case neg
α : Type u_1
β : Type ?u.378850
γ : Type ?u.378853
δ : Type ?u.378856
ι : Type ?u.378859
R : Type ?u.378862
R' : Type ?u.378865
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
hs : ¬Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
α : Type u_1
β : Type ?u.378850
γ : Type ?u.378853
δ : Type ?u.378856
ι : Type ?u.378859
R : Type ?u.378862
R' : Type ?u.378865
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
by_cases hs : s.Finite
no goals
case pos
α : Type u_1
β : Type ?u.378850
γ : Type ?u.378853
δ : Type ?u.378856
ι : Type ?u.378859
R : Type ?u.378862
R' : Type ?u.378865
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
hs : Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
exact count_apply_eq_top' hs.measurableSet
case neg
α : Type u_1
β : Type ?u.378850
γ : Type ?u.378853
δ : Type ?u.378856
ι : Type ?u.378859
R : Type ?u.378862
R' : Type ?u.378865
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
hs : Set.Infinite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
case neg
α : Type u_1
β : Type ?u.378850
γ : Type ?u.378853
δ : Type ?u.378856
ι : Type ?u.378859
R : Type ?u.378862
R' : Type ?u.378865
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
hs : ¬Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
change s.Infinite at hs
no goals
case neg
α : Type u_1
β : Type ?u.378850
γ : Type ?u.378853
δ : Type ?u.378856
ι : Type ?u.378859
R : Type ?u.378862
R' : Type ?u.378865
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
hs : Set.Infinite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
simp [hs, count_apply_infinite]