-- Mathlib/Topology/GDelta/Basic.lean
/-- A set is meagre iff it is contained in a countable union of nowhere dense sets. -/
lemma isMeagre_iff_countable_union_isNowhereDense {s : Set X} :
    IsMeagre s ↔ ∃ S : Set (Set X), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Proof state:
case h
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
S : Set (Set X)
hS : ∀ t ∈ S, IsNowhereDense t
hc : S.Countable
hsub : s ⊆ ⋃₀ S
⊢ (∀ ⦃x : Set X⦄, x ∈ S → IsClosed (closure x) ∧ IsNowhereDense (closure x)) ∧
    (compl '' (closure '' S)).Countable ∧ s ⊆ ⋃₀ (closure '' S)

Tactic:
exact ⟨fun s hs ↦ ⟨isClosed_closure, (hS s hs).closure⟩,
  (hc.image _).image _, hsub.trans (sUnion_mono_subsets fun s ↦ subset_closure)⟩

Result:
no goals

Proof state:
case refine_1
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
x✝ : ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
S : Set (Set X)
hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed x ∧ IsNowhereDense x
hc : (compl '' S).Countable
hsub : s ⊆ ⋃₀ S
⊢ (compl '' (compl '' S)).Countable

Tactic:
exact hc.image _

Result:
no goals

Proof state:
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
⊢ IsMeagre s ↔ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
rw [IsMeagre, mem_residual_iff, compl_bijective.surjective.image_surjective.exists]

Result:
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x, (∀ t ∈ compl '' x, IsOpen t) ∧ (∀ t ∈ compl '' x, Dense t) ∧ (compl '' x).Countable ∧ ⋂₀ (compl '' x) ⊆ sᶜ) ↔
    ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Proof state:
case h
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
S : Set (Set X)
hS : ∀ t ∈ S, IsNowhereDense t
hc : S.Countable
hsub : s ⊆ ⋃₀ S
⊢ (∀ ⦃x : Set X⦄, x ∈ closure '' S → IsClosed x ∧ IsNowhereDense x) ∧
    (compl '' (closure '' S)).Countable ∧ s ⊆ ⋃₀ (closure '' S)

Tactic:
rw [forall_mem_image]

Result:
case h
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
S : Set (Set X)
hS : ∀ t ∈ S, IsNowhereDense t
hc : S.Countable
hsub : s ⊆ ⋃₀ S
⊢ (∀ ⦃x : Set X⦄, x ∈ S → IsClosed (closure x) ∧ IsNowhereDense (closure x)) ∧
    (compl '' (closure '' S)).Countable ∧ s ⊆ ⋃₀ (closure '' S)

Proof state:
case refine_2
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
S : Set (Set X)
hS : ∀ t ∈ S, IsNowhereDense t
hc : S.Countable
hsub : s ⊆ ⋃₀ S
⊢ ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x

Tactic:
use closure '' S

Result:
case h
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
S : Set (Set X)
hS : ∀ t ∈ S, IsNowhereDense t
hc : S.Countable
hsub : s ⊆ ⋃₀ S
⊢ (∀ ⦃x : Set X⦄, x ∈ closure '' S → IsClosed x ∧ IsNowhereDense x) ∧
    (compl '' (closure '' S)).Countable ∧ s ⊆ ⋃₀ (closure '' S)

Proof state:
case refine_1
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
x✝ : ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
S : Set (Set X)
hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed x ∧ IsNowhereDense x
hc : (compl '' S).Countable
hsub : s ⊆ ⋃₀ S
⊢ S.Countable

Tactic:
rw [← compl_compl_image S]

Result:
case refine_1
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
x✝ : ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
S : Set (Set X)
hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed x ∧ IsNowhereDense x
hc : (compl '' S).Countable
hsub : s ⊆ ⋃₀ S
⊢ (compl '' (compl '' S)).Countable

Proof state:
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x) ↔
    ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
refine ⟨fun ⟨S, hS, hc, hsub⟩ ↦ ⟨S, fun s hs ↦ (hS hs).2, ?_, hsub⟩, ?_⟩

Result:
case refine_1
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
x✝ : ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
S : Set (Set X)
hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed x ∧ IsNowhereDense x
hc : (compl '' S).Countable
hsub : s ⊆ ⋃₀ S
⊢ S.Countable

case refine_2
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S) →
    ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x

Proof state:
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x, (∀ t ∈ compl '' x, IsOpen t) ∧ (∀ t ∈ compl '' x, Dense t) ∧ (compl '' x).Countable ∧ ⋂₀ (compl '' x) ⊆ sᶜ) ↔
    ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
simp_rw [← and_assoc, ← forall_and, forall_mem_image, ← isClosed_isNowhereDense_iff_compl,
  sInter_image, ← compl_iUnion₂, compl_subset_compl, ← sUnion_eq_biUnion, and_assoc]

Result:
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x) ↔
    ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Proof state:
case refine_2
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S) →
    ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x

Tactic:
intro ⟨S, hS, hc, hsub⟩

Result:
case refine_2
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
S : Set (Set X)
hS : ∀ t ∈ S, IsNowhereDense t
hc : S.Countable
hsub : s ⊆ ⋃₀ S
⊢ ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x