case refine'_1
s : Set ℂ
hs : Set.Countable (exp ⁻¹' s)
⊢ Set.Countable s

case refine'_2
s : Set ℂ
hs : Set.Countable s
⊢ Set.Countable (exp ⁻¹' s)
s : Set ℂ
⊢ Set.Countable (exp ⁻¹' s) ↔ Set.Countable s
refine' ⟨fun hs => _, fun hs => _⟩
case refine'_1
s : Set ℂ
hs : Set.Countable (exp ⁻¹' s)
⊢ s ⊆ insert 0 (exp '' (exp ⁻¹' s))
case refine'_1
s : Set ℂ
hs : Set.Countable (exp ⁻¹' s)
⊢ Set.Countable s
refine' ((hs.image exp).insert 0).mono _
case refine'_1
s : Set ℂ
hs : Set.Countable (exp ⁻¹' s)
⊢ s ⊆ s ∪ {0}
case refine'_1
s : Set ℂ
hs : Set.Countable (exp ⁻¹' s)
⊢ s ⊆ insert 0 (exp '' (exp ⁻¹' s))
rw [Set.image_preimage_eq_inter_range, range_exp, ←Set.diff_eq, ←Set.union_singleton,
    Set.diff_union_self]
no goals
case refine'_1
s : Set ℂ
hs : Set.Countable (exp ⁻¹' s)
⊢ s ⊆ s ∪ {0}
exact Set.subset_union_left _ _
case refine'_2
s : Set ℂ
hs : Set.Countable s
⊢ Set.Countable (⋃ (y : ℂ) (_ : y ∈ s), exp ⁻¹' {y})
case refine'_2
s : Set ℂ
hs : Set.Countable s
⊢ Set.Countable (exp ⁻¹' s)
rw [← Set.biUnion_preimage_singleton]
case refine'_2
s : Set ℂ
hs : Set.Countable s
z : ℂ
hz : z ∈ s
⊢ Set.Countable (exp ⁻¹' {z})
case refine'_2
s : Set ℂ
hs : Set.Countable s
⊢ Set.Countable (⋃ (y : ℂ) (_ : y ∈ s), exp ⁻¹' {y})
refine' hs.biUnion fun z hz => _
case refine'_2.inl.intro
s : Set ℂ
hs : Set.Countable s
w : ℂ
hz : exp w ∈ s
⊢ Set.Countable (exp ⁻¹' {exp w})

case refine'_2.inr
s : Set ℂ
hs : Set.Countable s
z : ℂ
hz : z ∈ s
hne : ¬∃ w, exp w = z
⊢ Set.Countable (exp ⁻¹' {z})
case refine'_2
s : Set ℂ
hs : Set.Countable s
z : ℂ
hz : z ∈ s
⊢ Set.Countable (exp ⁻¹' {z})
rcases em (∃ w, exp w = z) with (⟨w, rfl⟩ | hne)
case refine'_2.inl.intro
s : Set ℂ
hs : Set.Countable s
w : ℂ
hz : exp w ∈ s
⊢ Set.Countable (⋃ (i : ℤ), {x | x = w + ↑i * (2 * ↑π * I)})
case refine'_2.inl.intro
s : Set ℂ
hs : Set.Countable s
w : ℂ
hz : exp w ∈ s
⊢ Set.Countable (exp ⁻¹' {exp w})
simp only [Set.preimage, Set.mem_singleton_iff, exp_eq_exp_iff_exists_int, Set.setOf_exists]
no goals
case refine'_2.inl.intro
s : Set ℂ
hs : Set.Countable s
w : ℂ
hz : exp w ∈ s
⊢ Set.Countable (⋃ (i : ℤ), {x | x = w + ↑i * (2 * ↑π * I)})
exact Set.countable_iUnion fun m => Set.countable_singleton _
case refine'_2.inr
s : Set ℂ
hs : Set.Countable s
z : ℂ
hz : z ∈ s
hne : ∀ (w : ℂ), exp w ≠ z
⊢ Set.Countable (exp ⁻¹' {z})
case refine'_2.inr
s : Set ℂ
hs : Set.Countable s
z : ℂ
hz : z ∈ s
hne : ¬∃ w, exp w = z
⊢ Set.Countable (exp ⁻¹' {z})
push_neg  at hne
no goals
case refine'_2.inr
s : Set ℂ
hs : Set.Countable s
z : ℂ
hz : z ∈ s
hne : ∀ (w : ℂ), exp w ≠ z
⊢ Set.Countable (exp ⁻¹' {z})
simp [Set.preimage, hne]