case pos
α : Type u_1
β : Type ?u.378090
γ : Type ?u.378093
δ : Type ?u.378096
ι : Type ?u.378099
R : Type ?u.378102
R' : Type ?u.378105
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
s_mble : MeasurableSet s
hs : Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s

case neg
α : Type u_1
β : Type ?u.378090
γ : Type ?u.378093
δ : Type ?u.378096
ι : Type ?u.378099
R : Type ?u.378102
R' : Type ?u.378105
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
s_mble : MeasurableSet s
hs : ¬Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
α : Type u_1
β : Type ?u.378090
γ : Type ?u.378093
δ : Type ?u.378096
ι : Type ?u.378099
R : Type ?u.378102
R' : Type ?u.378105
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
s_mble : MeasurableSet s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
by_cases hs : s.Finite
no goals
case pos
α : Type u_1
β : Type ?u.378090
γ : Type ?u.378093
δ : Type ?u.378096
ι : Type ?u.378099
R : Type ?u.378102
R' : Type ?u.378105
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
s_mble : MeasurableSet s
hs : Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
simp [Set.Infinite, hs, count_apply_finite' hs s_mble]
case neg
α : Type u_1
β : Type ?u.378090
γ : Type ?u.378093
δ : Type ?u.378096
ι : Type ?u.378099
R : Type ?u.378102
R' : Type ?u.378105
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
s_mble : MeasurableSet s
hs : Set.Infinite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
case neg
α : Type u_1
β : Type ?u.378090
γ : Type ?u.378093
δ : Type ?u.378096
ι : Type ?u.378099
R : Type ?u.378102
R' : Type ?u.378105
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
s_mble : MeasurableSet s
hs : ¬Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
change s.Infinite at hs
no goals
case neg
α : Type u_1
β : Type ?u.378090
γ : Type ?u.378093
δ : Type ?u.378096
ι : Type ?u.378099
R : Type ?u.378102
R' : Type ?u.378105
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
s_mble : MeasurableSet s
hs : Set.Infinite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
simp [hs, count_apply_infinite]