awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsGδ s ↔ ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ s = ⋂ (n : ℕ), f n
have refine_1 : IsGδ s → ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ s = ⋂ (n : ℕ), f n
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
refine_1 : IsGδ s → ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ s = ⋂ (n : ℕ), f n
⊢ IsGδ s ↔ ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ s = ⋂ (n : ℕ), f n
have refine_2 : (∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ s = ⋂ (n : ℕ), f n) → IsGδ s
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
T : Set (Set X)
hT : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
⊢ ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ ⋂₀ T = ⋂ (n : ℕ), f n
have refine_1 : ∀ (hT : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t)
  (T_count : Set.Countable.{u_1} (α := Set X) ∅),
  ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋂₀ ∅) (⋂ (n : ℕ), f n)
Tactic: rcases Set.eq_empty_or_nonempty T with rfl | hT
Cleared hypotheses: T, hT, T_count
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
T : Set (Set X)
hT : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
refine_1 :
  ∀ (hT : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t)
    (T_count : Set.Countable.{u_1} (α := Set X) ∅),
    ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋂₀ ∅) (⋂ (n : ℕ), f n)
⊢ ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ ⋂₀ T = ⋂ (n : ℕ), f n
have refine_1₁ : ∀ (hT : T.Nonempty), ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ ⋂₀ T = ⋂ (n : ℕ), f n
Tactic: rcases Set.eq_empty_or_nonempty T with rfl | hT
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
T : Set (Set X)
hT_1 : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
hT : T.Nonempty
⊢ ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ ⋂₀ T = ⋂ (n : ℕ), f n
have refine_1 : ∀ (f : ℕ → Set X) (hf : T = range f), ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ ⋂₀ T = ⋂ (n : ℕ), f n
Tactic: obtain ⟨f, hf⟩ : ∃ (f : ℕ → Set X), T = range f := Countable.exists_eq_range T_count hT
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
s : ι' → Set X
hs : ∀ (i : ι'), IsGδ (s i)
⊢ IsGδ.{u_1} (X := X) (⋂ (i : ι'), s i)
have choose : ∀ (T : (i : ι') → Set (Set X)) (hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen[inst] t) (hTc : ∀ (i : ι'), (T i).Countable)
  (hTs : ∀ (i : ι'), s i = ⋂₀ T i), IsGδ.{u_1} (X := X) (⋂ (i : ι'), s i)
Tactic: choose T hTo hTc hTs using hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
s : ι' → Set X
T : (i : ι') → Set (Set X)
hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen[inst] t
hTc : ∀ (i : ι'), (T i).Countable
hTs : ∀ (i : ι'), s i = ⋂₀ T i
⊢ IsGδ.{u_1} (X := X) (⋂ (i : ι'), s i)
have obtain : ∀ (hTs : ∀ (i : ι'), (fun (i : ι') ↦ ⋂₀ T i) i = ⋂₀ T i), IsGδ.{u_1} (X := X) (⋂ (i : ι'), (fun (i : ι') ↦ ⋂₀ T i) i)
Tactic: obtain rfl : s = fun i => ⋂₀ T i := funext hTs
Cleared hypotheses: s, hTs
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
T : (i : ι') → Set (Set X)
hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen[inst] t
hTc : ∀ (i : ι'), (T i).Countable
hTs : ∀ (i : ι'), (fun (i : ι') ↦ ⋂₀ T i) i = ⋂₀ T i
⊢ IsGδ.{u_1} (X := X) (⋂ (i : ι'), (fun (i : ι') ↦ ⋂₀ T i) i)
have refine : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) (⋃ (i : ι'), T i) t → IsOpen[inst] t
Tactic: refine ⟨⋃ i, T i, ?_, countable_iUnion hTc, (sInter_iUnion _).symm⟩
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ.{u_1} (X := X) (⋂ (i : ι), ⋂ (h : i ∈ s), t i h)
have rw : IsGδ.{u_1} (X := X) (⋂ (x : (↑s : Type u_3)), t (↑x : ι) sorry)
Tactic: rw [biInter_eq_iInter]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (hypothesis)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ.{u_1} (X := X) (⋂ (x : (↑s : Type u_3)), t (↑x : ι) ⋯)
have this : Countable.{u_3 + 1} (↑s : Type u_3)
Tactic: haveI := hs.to_subtype
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (s ∩ t)
have rw : IsGδ.{u_1} (X := X) (⋂ (b : Bool), bif b then s else t)
Tactic: rw [inter_eq_iInter]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (s ∪ t)
have rcases : ∀ (S : Set (Set X)) (Sopen : ∀ t ∈ S, IsOpen[inst] t) (Scount : S.Countable), IsGδ (⋂₀ S ∪ t)
Tactic: rcases hs with ⟨S, Sopen, Scount, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
t : Set X
ht : IsGδ t
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen[inst] t
Scount : S.Countable
⊢ IsGδ (⋂₀ S ∪ t)
have rcases : ∀ (T : Set (Set X)) (Topen : ∀ t ∈ T, IsOpen[inst] t) (Tcount : T.Countable), IsGδ (⋂₀ S ∪ ⋂₀ T)
Tactic: rcases ht with ⟨T, Topen, Tcount, rfl⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen[inst] t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen[inst] t
Tcount : T.Countable
⊢ IsGδ (⋂₀ S ∪ ⋂₀ T)
have rw : IsGδ.{u_1} (X := X) (⋂ p ∈ S ×ˢ T, p.1 ∪ p.2)
Tactic: rw [sInter_union_sInter]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen[inst] t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen[inst] t
Tcount : T.Countable
⊢ IsGδ.{u_1} (X := X) (⋂ p ∈ S ×ˢ T, p.1 ∪ p.2)
have refine : ∀ i ∈ S ×ˢ T, IsOpen[inst] (i.1 ∪ i.2)
Tactic: refine .biInter_of_isOpen (Scount.prod Tcount) ?_
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
a : Set X
s : Set (Set X)
h_1 : a ∉ s
hs : s.Finite
ih : ∀ (h : ∀ s_1 ∈ s, IsGδ s_1), IsGδ (⋃₀ s)
h : ∀ s_1 ∈ insert a s, IsGδ s_1
⊢ IsGδ (⋃₀ insert a s)
have insert : ∀ (h : IsGδ a ∧ ∀ x ∈ s, IsGδ x), IsGδ (a ∪ ⋃₀ s)
Tactic: simp only [forall_mem_insert, sUnion_insert] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
h : ∀ s ∈ S, IsGδ s
⊢ IsGδ (⋃₀ S)
have empty : ∀ (h : ∀ (s : Set X), Membership.mem (γ := Set (Set X)) ∅ s → IsGδ s), IsGδ.{u_1} (X := X) (⋃₀ ∅)
Tactic: induction S, hS using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ ih =>
    simp only [forall_mem_insert, sUnion_insert] at *
    exact h.1.union (ih h.2)
Cleared hypotheses: hS, h
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
h : ∀ s ∈ S, IsGδ s
empty : ∀ (h : ∀ (s : Set X), Membership.mem (γ := Set (Set X)) ∅ s → IsGδ s), IsGδ.{u_1} (X := X) (⋃₀ ∅)
⊢ IsGδ (⋃₀ S)
have insert : ∀ {a : Set X} {s : Set (Set X)},
  a ∉ s →
    s.Finite →
      ∀ (ih : ∀ (h : ∀ s_1 ∈ s, IsGδ s_1), IsGδ (⋃₀ s)) (h : ∀ s_1 ∈ insert a s, IsGδ s_1), IsGδ (⋃₀ insert a s)
Tactic: induction S, hS using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ ih =>
    simp only [forall_mem_insert, sUnion_insert] at *
    exact h.1.union (ih h.2)
Cleared hypotheses: hS, h
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
s : Set ι
hs : s.Finite
f : ι → Set X
h : ∀ i ∈ s, IsGδ (f i)
⊢ IsGδ.{u_1} (X := X) (⋃ i ∈ s, f i)
have rw : IsGδ (⋃₀ (f '' s))
Tactic: rw [← sUnion_image]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : Continuous[inst, inst_1] f
hs : IsGδ s
⊢ IsGδ (f ⁻¹' s)
have obtain : ∀ (U : ℕ → Set Y) (hU1 : ∀ (n : ℕ), IsOpen[inst_1] (U n)) (hU2 : s = ⋂ (n : ℕ), U n), IsGδ (f ⁻¹' s)
Tactic: obtain ⟨U, hU1, hU2⟩ := hs.eq_iInter_nat
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : Continuous[inst, inst_1] f
hs : IsGδ s
U : ℕ → Set Y
hU1 : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hU2 : s = ⋂ (n : ℕ), U n
⊢ IsGδ (f ⁻¹' s)
have simp_all : ∀ (hs : IsGδ.{u_2} (X := Y) (⋂ (n : ℕ), U n)) (hU1 : ∀ (n : ℕ), IsOpen[inst_1] (U n)) (hU2 : s = ⋂ (n : ℕ), U n),
  IsGδ.{u_1} (X := X) (⋂ (i : ℕ), f ⁻¹' U i)
Tactic: simp_all only [preimage_iInter]
Cleared hypotheses: hs, hU1, hU2
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
ho : IsGδ s
hd : Dense s
⊢ s ∈ residual X
have rcases : ∀ (T : Set (Set X)) (To : ∀ t ∈ T, IsOpen[inst] t) (Tct : T.Countable) (hd : Dense (⋂₀ T)), ⋂₀ T ∈ residual X
Tactic: rcases ho with ⟨T, To, Tct, rfl⟩
Cleared hypotheses: s, ho, hd
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ (∃ S ⊆ {t : Set X | IsOpen[inst] t ∧ Dense t}, S.Countable ∧ ⋂₀ S ⊆ s) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsOpen[inst] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s
have simp_rw : (∃ (S : Set (Set X)),
    (∀ x ∈ S, Membership.mem (γ := Set (Set X)) {t : Set X | IsOpen[inst] t ∧ Dense t} x) ∧
      S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s) ↔
  ∃ (S : Set (Set X)), (∀ t ∈ S, IsOpen[inst] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s
Tactic: simp_rw [subset_def, mem_setOf, forall_and, and_assoc]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
simp_rw :
  (∃ (S : Set (Set X)),
      (∀ x ∈ S, Membership.mem (γ := Set (Set X)) {t : Set X | IsOpen[inst] t ∧ Dense t} x) ∧
        S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsOpen[inst] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s
⊢ (∃ S ⊆ {t : Set X | IsOpen[inst] t ∧ Dense t}, S.Countable ∧ ⋂₀ S ⊆ s) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsOpen[inst] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s
have simp_rw₁ : (∃ (S : Set (Set X)), (∀ x ∈ S, IsOpen[inst] x ∧ Dense x) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s) ↔
  ∃ (S : Set (Set X)), (∀ t ∈ S, IsOpen[inst] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s
Tactic: simp_rw [subset_def, mem_setOf, forall_and, and_assoc]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
simp_rw :
  (∃ (S : Set (Set X)),
      (∀ x ∈ S, Membership.mem (γ := Set (Set X)) {t : Set X | IsOpen[inst] t ∧ Dense t} x) ∧
        S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsOpen[inst] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s
simp_rw₁ :
  (∃ (S : Set (Set X)), (∀ x ∈ S, IsOpen[inst] x ∧ Dense x) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsOpen[inst] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s
⊢ (∃ S ⊆ {t : Set X | IsOpen[inst] t ∧ Dense t}, S.Countable ∧ ⋂₀ S ⊆ s) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsOpen[inst] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s
have simp_rw₂ : (∃ (S : Set (Set X)),
    ((∀ (x : Set X) (x_1 : x ∈ S), IsOpen[inst] x) ∧ ∀ (x : Set X) (x_1 : x ∈ S), Dense x) ∧
      S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s) ↔
  ∃ (S : Set (Set X)), (∀ t ∈ S, IsOpen[inst] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s
Tactic: simp_rw [subset_def, mem_setOf, forall_and, and_assoc]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsNowhereDense.{u_1} (X := X) ∅
have rw : Eq.{u_1 + 1} (α := Set X) (interior (closure[inst] ∅)) ∅
Tactic: rw [IsNowhereDense, closure_empty, interior_empty]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
rw : Eq.{u_1 + 1} (α := Set X) (interior (closure[inst] ∅)) ∅
⊢ IsNowhereDense.{u_1} (X := X) ∅
have rw₁ : Eq.{u_1 + 1} (α := Set X) (interior ∅) ∅
Tactic: rw [IsNowhereDense, closure_empty, interior_empty]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
rw : Eq.{u_1 + 1} (α := Set X) (interior (closure[inst] ∅)) ∅
rw₁ : Eq.{u_1 + 1} (α := Set X) (interior ∅) ∅
⊢ IsNowhereDense.{u_1} (X := X) ∅
have rw₂ : Eq.{u_1 + 1} (α := Set X) ∅ ∅
Tactic: rw [IsNowhereDense, closure_empty, interior_empty]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
ht : t ⊆ s
hs : IsNowhereDense s
⊢ interior (closure[inst] t) ⊆ ∅
have grw : interior (closure[inst] s) ⊆ ∅
Tactic: grw [ht]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
ht : t ⊆ s
hs : IsNowhereDense s
⊢ interior (closure[inst] s) ⊆ ∅
have rw : Subset.{u_1} (α := Set X) ∅ ∅
Tactic: rw [hs]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
⊢ IsNowhereDense s ↔ interior s = ∅
have rw : interior (closure[inst] s) = ∅ ↔ interior s = ∅
Tactic: rw [IsNowhereDense, IsClosed.closure_eq hs]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
rw : interior (closure[inst] s) = ∅ ↔ interior s = ∅
⊢ IsNowhereDense s ↔ interior s = ∅
have rw₁ : interior s = ∅ ↔ interior s = ∅
Tactic: rw [IsNowhereDense, IsClosed.closure_eq hs]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsNowhereDense s
⊢ IsNowhereDense (closure[inst] s)
have rwa : interior (closure[inst] (closure[inst] s)) = ∅
Tactic: rwa [IsNowhereDense, closure_closure]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsNowhereDense s
rwa : interior (closure[inst] (closure[inst] s)) = ∅
⊢ IsNowhereDense (closure[inst] s)
have rwa₁ : interior (closure[inst] s) = ∅
Tactic: rwa [IsNowhereDense, closure_closure]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsClosed[inst] s ∧ IsNowhereDense s ↔ IsOpen[inst] sᶜ ∧ Dense sᶜ
have rw : IsClosed[inst] s ∧ interior s = ∅ ↔ IsOpen[inst] sᶜ ∧ Dense sᶜ
Tactic: rw [and_congr_right IsClosed.isNowhereDense_iff,
    isOpen_compl_iff, interior_eq_empty_iff_dense_compl]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : IsClosed[inst] s ∧ interior s = ∅ ↔ IsOpen[inst] sᶜ ∧ Dense sᶜ
⊢ IsClosed[inst] s ∧ IsNowhereDense s ↔ IsOpen[inst] sᶜ ∧ Dense sᶜ
have rw₁ : IsClosed[inst] s ∧ interior s = ∅ ↔ IsClosed[inst] s ∧ Dense sᶜ
Tactic: rw [and_congr_right IsClosed.isNowhereDense_iff,
    isOpen_compl_iff, interior_eq_empty_iff_dense_compl]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : IsClosed[inst] s ∧ interior s = ∅ ↔ IsOpen[inst] sᶜ ∧ Dense sᶜ
rw₁ : IsClosed[inst] s ∧ interior s = ∅ ↔ IsClosed[inst] s ∧ Dense sᶜ
⊢ IsClosed[inst] s ∧ IsNowhereDense s ↔ IsOpen[inst] sᶜ ∧ Dense sᶜ
have rw₂ : IsClosed[inst] s ∧ Dense sᶜ ↔ IsClosed[inst] s ∧ Dense sᶜ
Tactic: rw [and_congr_right IsClosed.isNowhereDense_iff,
    isOpen_compl_iff, interior_eq_empty_iff_dense_compl]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : IsNowhereDense s
⊢ IsNowhereDense (f '' s)
have rw : ∀ (h : ∀ x ∈ s, closure[inst] s ∉ 𝓝 x) ⦃x : X⦄, x ∈ s → closure[inst_1] (f '' s) ∉ 𝓝 (f x)
Tactic: rw [isNowhereDense_iff_forall_notMem_nhds, forall_mem_image] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : ∀ x ∈ s, closure[inst] s ∉ 𝓝 x
⊢ ∀ ⦃x : X⦄, x ∈ s → closure[inst_1] (f '' s) ∉ 𝓝 (f x)
have h₁ : ∀ x ∈ s, f ⁻¹' closure[inst_1] (f '' s) ∉ comap f (𝓝 (f x))
Tactic: simp_rw [hf.nhds_eq_comap, hf.closure_eq_preimage_closure_image] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsMeagre.{u_1} (X := X) ∅
have rw : univ ∈ residual X
Tactic: rw [IsMeagre, compl_empty]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsMeagre s
ht : IsMeagre t
⊢ IsMeagre (s ∪ t)
have rw : sᶜ ∩ tᶜ ∈ residual X
Tactic: rw [IsMeagre, compl_union]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
f : ι' → Set X
hs : ∀ (i : ι'), IsMeagre (f i)
⊢ IsMeagre.{u_1} (X := X) (⋃ (i : ι'), f i)
have rw : ⋂ (i : ι'), (f i)ᶜ ∈ residual X
Tactic: rw [IsMeagre, compl_iUnion]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
⊢ IsMeagre.{u_1} (X := X) (⋃ i ∈ I, f i)
have suffices : IsMeagre.{u_1} (X := X) (⋃ (i : (↑I : Type u_3)), f (↑i : ι))
Tactic: suffices IsMeagre (⋃ i : I, f i) by simpa
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (hypothesis)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
⊢ IsMeagre.{u_1} (X := X) (⋃ (i : (↑I : Type u_3)), f (↑i : ι))
have this : Countable.{u_3 + 1} (↑I : Type u_3)
Tactic: have : Countable I := c
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
this : Countable.{u_3 + 1} (↑I : Type u_3)
⊢ IsMeagre.{u_1} (X := X) (⋃ (i : (↑I : Type u_3)), f (↑i : ι))
have hs : ∀ (i : (↑I : Type u_3)), IsMeagre (f (↑i : ι))
Tactic: apply isMeagre_iUnion
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsMeagre s ↔ ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
have rw : (∃ (x : Set (Set X)),
    (∀ t ∈ compl '' x, IsOpen[inst] t) ∧ (∀ t ∈ compl '' x, Dense t) ∧ (compl '' x).Countable ∧ ⋂₀ (compl '' x) ⊆ sᶜ) ↔
  ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
Tactic: rw [IsMeagre, mem_residual_iff, compl_bijective.surjective.image_surjective.exists]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ (∃ (x : Set (Set X)),
      (∀ t ∈ compl '' x, IsOpen[inst] t) ∧
        (∀ t ∈ compl '' x, Dense t) ∧ (compl '' x).Countable ∧ ⋂₀ (compl '' x) ⊆ sᶜ) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
have simp_rw : (∃ (x : Set (Set X)),
    (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x) ↔
  ∃ (S : Set (Set X)), (∀ 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]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ (∃ (x : Set (Set X)),
      (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
have refine_1 : (∃ (x : Set (Set X)),
    (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x) →
  ∀ (S : Set (Set X)) (hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst] x ∧ IsNowhereDense x) (hc : (compl '' S).Countable)
    (hsub : s ⊆ ⋃₀ S), S.Countable
Tactic: refine ⟨fun ⟨S, hS, hc, hsub⟩ ↦ ⟨S, fun s hs ↦ (hS hs).2, ?_, hsub⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
refine_1 :
  (∃ (x : Set (Set X)),
      (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x) →
    ∀ (S : Set (Set X)) (hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst] x ∧ IsNowhereDense x) (hc : (compl '' S).Countable)
      (hsub : s ⊆ ⋃₀ S), S.Countable
⊢ (∃ (x : Set (Set X)),
      (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
have refine_2 : (∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S) →
  ∃ (x : Set (Set X)),
    (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
Tactic: refine ⟨fun ⟨S, hS, hc, hsub⟩ ↦ ⟨S, fun s hs ↦ (hS hs).2, ?_, hsub⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h :
  ∃ (x : Set (Set X)),
    (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
S : Set (Set X)
hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst] x ∧ IsNowhereDense x
hc : (compl '' S).Countable
hsub : s ⊆ ⋃₀ S
⊢ S.Countable
have refine_1 : (compl '' compl '' S).Countable
Tactic: rw [← compl_compl_image S]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
S : Set (Set X)
hS : ∀ t ∈ S, IsNowhereDense t
hc : S.Countable
hsub : s ⊆ ⋃₀ S
⊢ ∃ (x : Set (Set X)),
    (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
have h : (∀ ⦃x : Set X⦄, x ∈ closure[inst] '' S → IsClosed[inst] x ∧ IsNowhereDense x) ∧
  (compl '' closure[inst] '' S).Countable ∧ s ⊆ ⋃₀ (closure[inst] '' S)
Tactic: use closure '' S
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
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[inst] '' S → IsClosed[inst] x ∧ IsNowhereDense x) ∧
    (compl '' closure[inst] '' S).Countable ∧ s ⊆ ⋃₀ (closure[inst] '' S)
have h : (∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst] (closure[inst] x) ∧ IsNowhereDense (closure[inst] x)) ∧
  (compl '' closure[inst] '' S).Countable ∧ s ⊆ ⋃₀ (closure[inst] '' S)
Tactic: rw [forall_mem_image]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : ¬IsMeagre s
⊢ s.Nonempty
have contrapose! : ∀ (hs : s = ∅), IsMeagre s
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsNowhereDense s
⊢ IsMeagre s
have rw : ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
Tactic: rw [isMeagre_iff_countable_union_isNowhereDense]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
c : I.Countable
A : ι → Set X
h : ¬IsMeagre.{u_1} (X := X) (⋃ i ∈ I, A i)
⊢ ∃ i ∈ I, ¬IsMeagre (A i)
have contrapose! : ∀ (h : ∀ (i : ι) (_ : i ∈ I), IsMeagre (A i)), IsMeagre.{u_1} (X := X) (⋃ i ∈ I, A i)
Tactic: contrapose! h
Cleared hypotheses: h