awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hst : s ⊆ t
rw : Dense (range (inclusion (s := s) (t := t) hst)) ↔ t ⊆ closure[inst] s
rw₁ : t ⊆ closure[inst] ↑(range (inclusion (s := s) (t := t) hst)) ↔ t ⊆ closure[inst] s
rw₂ :
  t ⊆ closure[inst] (range (Subtype.val (p := fun (x : X) ↦ x ∈ t) ∘ inclusion (s := s) (t := t) hst)) ↔
    t ⊆ closure[inst] s
⊢ DenseRange (inclusion (s := s) (t := t) hst) ↔ t ⊆ closure[inst] s
have rw₃ : t ⊆ closure[inst] (range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : X) ↦ x ∈ s))) ↔ t ⊆ closure[inst] s
Tactic: rw [DenseRange, Subtype.dense_iff, ← range_comp, val_comp_inclusion, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hst : s ⊆ t
rw : Dense (range (inclusion (s := s) (t := t) hst)) ↔ t ⊆ closure[inst] s
rw₁ : t ⊆ closure[inst] ↑(range (inclusion (s := s) (t := t) hst)) ↔ t ⊆ closure[inst] s
rw₂ :
  t ⊆ closure[inst] (range (Subtype.val (p := fun (x : X) ↦ x ∈ t) ∘ inclusion (s := s) (t := t) hst)) ↔
    t ⊆ closure[inst] s
rw₃ : t ⊆ closure[inst] (range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : X) ↦ x ∈ s))) ↔ t ⊆ closure[inst] s
⊢ DenseRange (inclusion (s := s) (t := t) hst) ↔ t ⊆ closure[inst] s
have rw₄ : t ⊆ closure[inst] s ↔ t ⊆ closure[inst] s
Tactic: rw [DenseRange, Subtype.dense_iff, ← range_comp, val_comp_inclusion, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
x : (↑s : Type u)
⊢ map (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x) = 𝓝[s] (↑x : X)
have rw : 𝓝[range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))] (↑x : X) = 𝓝[s] (↑x : X)
Tactic: rw [IsInducing.subtypeVal.map_nhds_eq, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
x : (↑s : Type u)
rw : 𝓝[range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))] (↑x : X) = 𝓝[s] (↑x : X)
⊢ map (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x) = 𝓝[s] (↑x : X)
have rw₁ : 𝓝[s] (↑x : X) = 𝓝[s] (↑x : X)
Tactic: rw [IsInducing.subtypeVal.map_nhds_eq, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
p : X → Prop
x : X
hx : p x
h : ∀ᶠ (x : X) in 𝓝 x, p x
⊢ range (ι := Subtype p) (Subtype.val (p := p)) ∈ 𝓝 (↑(Subtype.mk (p := p) x hx) : X)
have rw : p ∈ 𝓝 (↑(Subtype.mk (p := p) x hx) : X)
Tactic: rw [Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_5
p : X → Prop
l : Filter Y
f : Y → Subtype p
a : X
ha : p a
⊢ Tendsto f l (𝓝 (Subtype.mk (p := p) a ha)) ↔
    Tendsto (fun (x : Y) ↦ (↑(f x) : X)) l (𝓝 (↑(Subtype.mk (p := p) a ha) : X))
have rw : Tendsto (Subtype.val (p := p) ∘ f) l (𝓝 a) ↔
  Tendsto (fun (x : Y) ↦ (↑(f x) : X)) l (𝓝 (↑(Subtype.mk (p := p) a ha) : X))
Tactic: rw [nhds_subtype_eq_comap, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
t : Set Y
H : MapsTo f s t
hs : IsOpen[inst] s
⊢ IsOpen[instTopologicalSpaceSubtype] (range (MapsTo.restrict f s t H))
have rw : IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : Y) ↦ x ∈ t) ⁻¹' f '' s)
Tactic: rw [MapsTo.range_restrict]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hst : s ⊆ t
hs : IsOpen[instTopologicalSpaceSubtype] (t ↓∩ s)
⊢ IsOpen[instTopologicalSpaceSubtype] (range (inclusion (s := s) (t := t) hst))
have rwa : IsOpen[instTopologicalSpaceSubtype] {x : (↑t : Type u) | (↑x : X) ∈ s}
Tactic: rwa [range_inclusion]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hst : s ⊆ t
hs : IsClosed[instTopologicalSpaceSubtype] (t ↓∩ s)
⊢ IsClosed[instTopologicalSpaceSubtype] (range (inclusion (s := s) (t := t) hst))
have rwa : IsClosed[instTopologicalSpaceSubtype] {x : (↑t : Type u) | (↑x : X) ∈ s}
Tactic: rwa [range_inclusion]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst_1] s
⊢ IsCoinducing (s.restrictPreimage f)
have refine : ∀ (x : Set (↑s : Type v)),
  IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔ IsOpen[instTopologicalSpaceSubtype] x
Tactic: refine .of_isOpen_preimage_iff_isOpen fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst_1] s
x : Set (↑s : Type v)
⊢ IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔ IsOpen[instTopologicalSpaceSubtype] x
have rw : IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔
  IsOpen[inst_1] (Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x)
Tactic: rw [hs.isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen, ← hf.isOpen_preimage,
    (hs.preimage hf.continuous).isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen,
    image_val_preimage_restrictPreimage]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst_1] s
x : Set (↑s : Type v)
rw :
  IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔
    IsOpen[inst_1] (Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x)
⊢ IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔ IsOpen[instTopologicalSpaceSubtype] x
have rw₁ : IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔
  IsOpen[inst] (f ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x)
Tactic: rw [hs.isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen, ← hf.isOpen_preimage,
    (hs.preimage hf.continuous).isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen,
    image_val_preimage_restrictPreimage]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst_1] s
x : Set (↑s : Type v)
rw :
  IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔
    IsOpen[inst_1] (Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x)
rw₁ :
  IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔
    IsOpen[inst] (f ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x)
⊢ IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔ IsOpen[instTopologicalSpaceSubtype] x
have rw₂ : IsOpen[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' s) '' s.restrictPreimage f ⁻¹' x) ↔
  IsOpen[inst] (f ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x)
Tactic: rw [hs.isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen, ← hf.isOpen_preimage,
    (hs.preimage hf.continuous).isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen,
    image_val_preimage_restrictPreimage]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst_1] s
x : Set (↑s : Type v)
rw :
  IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔
    IsOpen[inst_1] (Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x)
rw₁ :
  IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔
    IsOpen[inst] (f ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x)
rw₂ :
  IsOpen[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' s) '' s.restrictPreimage f ⁻¹' x) ↔
    IsOpen[inst] (f ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x)
⊢ IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔ IsOpen[instTopologicalSpaceSubtype] x
have rw₃ : IsOpen[inst] (f ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x) ↔
  IsOpen[inst] (f ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x)
Tactic: rw [hs.isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen, ← hf.isOpen_preimage,
    (hs.preimage hf.continuous).isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen,
    image_val_preimage_restrictPreimage]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t) ↔ s ∩ closure[inst] (s ∩ t) ⊆ t
have rw : s ∩ closure[inst] (s ∩ t) ⊆ s
Tactic: rw [← closure_eq_iff_isClosed, IsEmbedding.subtypeVal.closure_eq_preimage_closure_image,
    ← Subtype.val_injective.image_injective.eq_iff, Subtype.image_preimage_coe,
    Subtype.image_preimage_coe, subset_antisymm_iff, and_iff_left, Set.subset_inter_iff,
    and_iff_right]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
rw : s ∩ closure[inst] (s ∩ t) ⊆ s
⊢ IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t) ↔ s ∩ closure[inst] (s ∩ t) ⊆ t
have rw₁ : s ∩ t ⊆ s ∩ closure[inst] (s ∩ t)
Tactic: rw [← closure_eq_iff_isClosed, IsEmbedding.subtypeVal.closure_eq_preimage_closure_image,
    ← Subtype.val_injective.image_injective.eq_iff, Subtype.image_preimage_coe,
    Subtype.image_preimage_coe, subset_antisymm_iff, and_iff_left, Set.subset_inter_iff,
    and_iff_right]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : Dense s
u : Set (↑s : Type u)
huo : IsOpen[instTopologicalSpaceSubtype] u
hud : Dense u
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ Dense v ∧ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u
have choose : ∀ (v : Set X) (hv1 : IsOpen[inst] v) (hv2 : Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u),
  ∃ (v : Set X), IsOpen[inst] v ∧ Dense v ∧ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u
Tactic: choose v hv1 hv2 using huo
Cleared hypotheses: huo
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : Dense s
u : Set (↑s : Type u)
hud : Dense u
v : Set X
hv1 : IsOpen[inst] v
hv2 : Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ Dense v ∧ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u
have refine : Dense v
Tactic: refine ⟨v, hv1, ?_, hv2⟩
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : Dense s
u : Set (↑s : Type u)
hud : Dense u
v : Set X
hv1 : IsOpen[inst] v
hv2 : Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u
⊢ Dense v
have rw : ∀ (hs : ∀ (U : Set X), IsOpen[inst] U → U.Nonempty → (U ∩ s).Nonempty) {u : Set (↑s : Type u)}
  (hud : ∀ (U : Set (↑s : Type u)), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ u).Nonempty) (v : Set X)
  (hv1 : IsOpen[inst] v) (hv2 : Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u) (U : Set X),
  IsOpen[inst] U → U.Nonempty → (U ∩ v).Nonempty
Tactic: rw [dense_iff_inter_open] at *
Cleared hypotheses: hs, u, hud, v, hv1, hv2
-- Lean 4 proof step from Mathlib.Topology.Constructions (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst] U → U.Nonempty → (U ∩ s).Nonempty
u : Set (↑s : Type u)
hud : ∀ (U : Set (↑s : Type u)), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ u).Nonempty
v : Set X
hv1 : IsOpen[inst] v
hv2 : Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u
t : Set X
ht : IsOpen[inst] t
ht' : t.Nonempty
⊢ (t ∩ v).Nonempty
have hud₁ : ∀ (U : Set (↑s : Type u)),
  IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v).Nonempty
Tactic: subst hv2
Cleared hypotheses: u, hud, hv2
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst] v
t : Set X
ht : IsOpen[inst] t
ht' : t.Nonempty
hud :
  ∀ (U : Set (↑s : Type u)),
    IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v).Nonempty
⊢ (t ∩ v).Nonempty
have refine_1 : IsOpen[instTopologicalSpaceSubtype] (s ↓∩ t)
Tactic: refine nonempty_of_nonempty_preimage (f := (Subtype.val : s → X)) (hud (Subtype.val ⁻¹' t) ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst] v
t : Set X
ht : IsOpen[inst] t
ht' : t.Nonempty
hud :
  ∀ (U : Set (↑s : Type u)),
    IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v).Nonempty
refine_1 : IsOpen[instTopologicalSpaceSubtype] (s ↓∩ t)
⊢ (t ∩ v).Nonempty
have refine_2 : Set.Nonempty (α := (↑s : Type u)) (s ↓∩ t)
Tactic: refine nonempty_of_nonempty_preimage (f := (Subtype.val : s → X)) (hud (Subtype.val ⁻¹' t) ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst] v
t : Set X
ht : IsOpen[inst] t
ht' : t.Nonempty
hud :
  ∀ (U : Set (↑s : Type u)),
    IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v).Nonempty
⊢ Set.Nonempty (α := (↑s : Type u)) (s ↓∩ t)
have refine_2 : ∀ (x : X) (hx : x ∈ t ∩ s), Set.Nonempty (α := (↑s : Type u)) (s ↓∩ t)
Tactic: obtain ⟨x, hx⟩ := hs t ht ht'
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
⊢ IsOpenMap (Pi.map (α := A) (β := B) f)
have refine : ∀ (x : (i : ι) → A i), 𝓝 (Pi.map (α := A) (β := B) f x) ≤ map (Pi.map (α := A) (β := B) f) (𝓝 x)
Tactic: refine IsOpenMap.of_nhds_le fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → A i
⊢ 𝓝 (Pi.map (α := A) (β := B) f x) ≤ map (Pi.map (α := A) (β := B) f) (𝓝 x)
have rw : LE.le (α := Filter ((i : ι) → B i)) (Filter.pi (α := B) fun (i : ι) ↦ 𝓝 (Pi.map (α := A) (β := B) f x i))
  (Filter.pi (α := B) fun (i : ι) ↦ map (f i) (𝓝 (x i)))
Tactic: rw [nhds_pi, nhds_pi, map_piMap_pi hsurj]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
f : Y → (i : ι) → A i
g : (i : ι) → A i
u : Filter Y
⊢ Tendsto f u (𝓝 g) ↔ ∀ (x : ι), Tendsto (fun (i : Y) ↦ f i x) u (𝓝 (g x))
have rw : Tendsto f u (Filter.pi (α := A) fun (i : ι) ↦ 𝓝 (g i)) ↔ ∀ (x : ι), Tendsto (fun (i : Y) ↦ f i x) u (𝓝 (g x))
Tactic: rw [nhds_pi, Filter.tendsto_pi]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
f : Y → (i : ι) → A i
g : (i : ι) → A i
u : Filter Y
rw : Tendsto f u (Filter.pi (α := A) fun (i : ι) ↦ 𝓝 (g i)) ↔ ∀ (x : ι), Tendsto (fun (i : Y) ↦ f i x) u (𝓝 (g x))
⊢ Tendsto f u (𝓝 g) ↔ ∀ (x : ι), Tendsto (fun (i : Y) ↦ f i x) u (𝓝 (g x))
have rw₁ : (∀ (i : ι), Tendsto (fun (x : Y) ↦ f x i) u (𝓝 (g i))) ↔ ∀ (x : ι), Tendsto (fun (i : Y) ↦ f i x) u (𝓝 (g x))
Tactic: rw [nhds_pi, Filter.tendsto_pi]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
𝔖 : Set (Set ι)
⊢ Eq (α := TopologicalSpace ((a : ι) → A a))
    (induced ((⋃₀ 𝔖).restrict (π := A)) (topologicalSpace (Y := fun (i : (↑(⋃₀ 𝔖) : Type u_5)) ↦ A (↑i : ι))))
    (⨅ S ∈ 𝔖, induced (S.restrict (π := A)) (topologicalSpace (Y := fun (a : (↑S : Type u_5)) ↦ A (↑a : ι))))
have simp_rw : Eq (α := TopologicalSpace ((a : ι) → A a)) (⨅ i ∈ ⋃₀ 𝔖, induced (eval (β := A) i) (T i))
  (⨅ S ∈ 𝔖, ⨅ i ∈ S, induced (eval (β := A) i) (T i))
Tactic: simp_rw [Pi.induced_restrict, iInf_sUnion]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : DecidableEq ι
l : Filter Y
f : Y → (i : ι) → A i
x : (i : ι) → A i
hf : Tendsto f l (𝓝 x)
i : ι
g : Y → A i
xi : A i
hg : Tendsto g l (𝓝 xi)
j : ι
⊢ Tendsto (fun (i_1 : Y) ↦ Function.update (β := A) (f i_1) i (g i_1) j) l (𝓝 (Function.update (β := A) x i xi j))
have inl : ∀ {g : Y → A j} {xi : A j} (hg : Tendsto g l (𝓝 xi)),
  Tendsto (fun (i : Y) ↦ Function.update (β := A) (f i) j (g i) j) l (𝓝 (Function.update (β := A) x j xi j))
Tactic: rcases eq_or_ne j i with (rfl | hj)
Cleared hypotheses: i, g, xi, hg
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : DecidableEq ι
l : Filter Y
f : Y → (i : ι) → A i
x : (i : ι) → A i
hf : Tendsto f l (𝓝 x)
i : ι
g : Y → A i
xi : A i
hg : Tendsto g l (𝓝 xi)
j : ι
inl :
  ∀ {g : Y → A j} {xi : A j} (hg : Tendsto g l (𝓝 xi)),
    Tendsto (fun (i : Y) ↦ Function.update (β := A) (f i) j (g i) j) l (𝓝 (Function.update (β := A) x j xi j))
⊢ Tendsto (fun (i_1 : Y) ↦ Function.update (β := A) (f i_1) i (g i_1) j) l (𝓝 (Function.update (β := A) x i xi j))
have inr : ∀ (hj : j ≠ i),
  Tendsto (fun (i_1 : Y) ↦ Function.update (β := A) (f i_1) i (g i_1) j) l (𝓝 (Function.update (β := A) x i xi j))
Tactic: rcases eq_or_ne j i with (rfl | hj)
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hi : i.Finite
hs : ∀ a ∈ i, IsOpen[T a] (s a)
⊢ IsOpen[Pi.topologicalSpace] (i.pi (α := A) s)
have rw : IsOpen[Pi.topologicalSpace] (⋂ a ∈ i, eval (β := A) a ⁻¹' s a)
Tactic: rw [pi_def]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
⊢ IsOpen[Pi.topologicalSpace] s ↔
    ∀ f ∈ s,
      ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
        (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I : Set ι).pi (α := A) u ⊆ s
have rw : (∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔
  ∀ f ∈ s,
    ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
      (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I : Set ι).pi (α := A) u ⊆ s
Tactic: rw [isOpen_iff_nhds]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
⊢ (∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔
    ∀ f ∈ s,
      ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
        (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I : Set ι).pi (α := A) u ⊆ s
have simp_rw : (∀ x ∈ s,
    ∃ (I : Finset ι) (t : (i : ι) → Set (A i)),
      (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ x i ∈ t_1) ∧ (↑I : Set ι).pi (α := A) t ⊆ s) ↔
  ∀ f ∈ s,
    ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
      (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I : Set ι).pi (α := A) u ⊆ s
Tactic: simp_rw [le_principal_iff, nhds_pi, Filter.mem_pi', mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
⊢ (∀ x ∈ s,
      ∃ (I : Finset ι) (t : (i : ι) → Set (A i)),
        (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ x i ∈ t_1) ∧ (↑I : Set ι).pi (α := A) t ⊆ s) ↔
    ∀ f ∈ s,
      ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
        (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I : Set ι).pi (α := A) u ⊆ s
have refine_1 : ∀ a ∈ s,
  (∃ (I : Finset ι) (t : (i : ι) → Set (A i)),
      (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I : Set ι).pi (α := A) t ⊆ s) →
    ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
      (∀ a_2 ∈ I, IsOpen[T a_2] (u a_2) ∧ a a_2 ∈ u a_2) ∧ (↑I : Set ι).pi (α := A) u ⊆ s
Tactic: refine forall₂_congr fun a _ => ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
refine_1 :
  ∀ a ∈ s,
    (∃ (I : Finset ι) (t : (i : ι) → Set (A i)),
        (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I : Set ι).pi (α := A) t ⊆ s) →
      ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
        (∀ a_2 ∈ I, IsOpen[T a_2] (u a_2) ∧ a a_2 ∈ u a_2) ∧ (↑I : Set ι).pi (α := A) u ⊆ s
⊢ (∀ x ∈ s,
      ∃ (I : Finset ι) (t : (i : ι) → Set (A i)),
        (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ x i ∈ t_1) ∧ (↑I : Set ι).pi (α := A) t ⊆ s) ↔
    ∀ f ∈ s,
      ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
        (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I : Set ι).pi (α := A) u ⊆ s
have refine_2 : ∀ a ∈ s,
  (∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
      (∀ a_1 ∈ I, IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ (↑I : Set ι).pi (α := A) u ⊆ s) →
    ∃ (I : Finset ι) (t : (i : ι) → Set (A i)),
      (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I : Set ι).pi (α := A) t ⊆ s
Tactic: refine forall₂_congr fun a _ => ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
h : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
⊢ ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
    (∀ a_1 ∈ I, IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ (↑I : Set ι).pi (α := A) u ⊆ s
have refine_1 : ∀ (i : ι) (hi : i ∈ I),
  IsOpen[T i]
      ((fun (a_1 : ι) ↦
          (eval (β := A) a_1 ''
              (↑I : Set ι).pi (α := A) fun (a_2 : ι) ↦
                sorry.choose (p := fun (t_1 : Set (A a_2)) ↦ t_1 ⊆ t a_2 ∧ IsOpen[T a_2] t_1 ∧ a a_2 ∈ t_1) :
            Set (A a_1)))
        i) ∧
    Membership.mem (γ := Set (A i))
      ((fun (a_1 : ι) ↦
          (eval (β := A) a_1 ''
              (↑I : Set ι).pi (α := A) fun (a_2 : ι) ↦
                sorry.choose (p := fun (t_1 : Set (A a_2)) ↦ t_1 ⊆ t a_2 ∧ IsOpen[T a_2] t_1 ∧ a a_2 ∈ t_1) :
            Set (A a_1)))
        i)
      (a i)
Tactic: refine ⟨I, fun a => eval a '' (I : Set ι).pi fun a => (h1 a).choose, fun i hi => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
h : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
refine_1 :
  ∀ (i : ι) (hi : i ∈ I),
    IsOpen[T i]
        ((fun (a_1 : ι) ↦
            (eval (β := A) a_1 ''
                (↑I : Set ι).pi (α := A) fun (a_2 : ι) ↦
                  ⋯.choose (p := fun (t_1 : Set (A a_2)) ↦ t_1 ⊆ t a_2 ∧ IsOpen[T a_2] t_1 ∧ a a_2 ∈ t_1) :
              Set (A a_1)))
          i) ∧
      Membership.mem (γ := Set (A i))
        ((fun (a_1 : ι) ↦
            (eval (β := A) a_1 ''
                (↑I : Set ι).pi (α := A) fun (a_2 : ι) ↦
                  ⋯.choose (p := fun (t_1 : Set (A a_2)) ↦ t_1 ⊆ t a_2 ∧ IsOpen[T a_2] t_1 ∧ a a_2 ∈ t_1) :
              Set (A a_1)))
          i)
        (a i)
⊢ ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
    (∀ a_1 ∈ I, IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ (↑I : Set ι).pi (α := A) u ⊆ s
have refine_1₁ : ((↑I : Set ι).pi (α := A) fun (a_1 : ι) ↦
    eval (β := A) a_1 ''
      (↑I : Set ι).pi (α := A) fun (a_2 : ι) ↦
        sorry.choose (p := fun (t_1 : Set (A a_2)) ↦ t_1 ⊆ t a_2 ∧ IsOpen[T a_2] t_1 ∧ a a_2 ∈ t_1)) ⊆
  s
Tactic: refine ⟨I, fun a => eval a '' (I : Set ι).pi fun a => (h1 a).choose, fun i hi => ?_, ?_⟩