awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have have : ∀ (this : ∀ (i : ι), ∃ (K : Set (R i)), IsCompact K ∧ K ∈ 𝓝 ((x : (a : ι) → R a) i)),
  ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
Tactic: classical
    have : ∀ i, ∃ K, IsCompact K ∧ K ∈ 𝓝 (x i) := fun i ↦ exists_compact_mem_nhds (x i)
    choose K K_compact hK using this
    set Q : Set (Π i, R i) := univ.pi (fun i ↦ if i ∈ S then A i else K i) with Q_def
    have Q_compact : IsCompact Q := isCompact_univ_pi fun i ↦ by
      split_ifs with his
      · exact hAcompact i his
      · exact K_compact i
    set U : Set (Π i, R i) := Sᶜ.pi K
    have U_nhds : U ∈ 𝓝 (x : Π i, R i) := set_pi_mem_nhds hS fun i _ ↦ hK i
    have QU : (↑) ⁻¹' U ⊆ ((↑) ⁻¹' Q : Set (Πʳ i, [R i, A i]_[𝓟 S])) := fun y H i _ ↦ by
      dsimp only
      split_ifs with hi
      · exact y.2 hi
      · exact H i hi
    refine ⟨((↑) ⁻¹' Q), ?_, mem_of_superset ?_ QU⟩
    · refine isEmbedding_coe_of_principal.isCompact_preimage_iff ?_ |>.mpr Q_compact
      simp_rw [range_coe_principal, Q_def, pi_if, mem_univ, true_and]
      exact inter_subset_left
    · simpa only [isEmbedding_coe_of_principal.nhds_eq_comap] using preimage_mem_comap U_nhds
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
have have₁ have₂ :
  ∀ (this : ∀ (i : ι), ∃ (K : Set (R i)), IsCompact K ∧ K ∈ 𝓝 ((x : (a : ι) → R a) i)),
    ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have have₃ : ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i)) (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)),
  ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
Tactic: classical
    have : ∀ i, ∃ K, IsCompact K ∧ K ∈ 𝓝 (x i) := fun i ↦ exists_compact_mem_nhds (x i)
    choose K K_compact hK using this
    set Q : Set (Π i, R i) := univ.pi (fun i ↦ if i ∈ S then A i else K i) with Q_def
    have Q_compact : IsCompact Q := isCompact_univ_pi fun i ↦ by
      split_ifs with his
      · exact hAcompact i his
      · exact K_compact i
    set U : Set (Π i, R i) := Sᶜ.pi K
    have U_nhds : U ∈ 𝓝 (x : Π i, R i) := set_pi_mem_nhds hS fun i _ ↦ hK i
    have QU : (↑) ⁻¹' U ⊆ ((↑) ⁻¹' Q : Set (Πʳ i, [R i, A i]_[𝓟 S])) := fun y H i _ ↦ by
      dsimp only
      split_ifs with hi
      · exact y.2 hi
      · exact H i hi
    refine ⟨((↑) ⁻¹' Q), ?_, mem_of_superset ?_ QU⟩
    · refine isEmbedding_coe_of_principal.isCompact_preimage_iff ?_ |>.mpr Q_compact
      simp_rw [range_coe_principal, Q_def, pi_if, mem_univ, true_and]
      exact inter_subset_left
    · simpa only [isEmbedding_coe_of_principal.nhds_eq_comap] using preimage_mem_comap U_nhds
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
have have₁ have₂ :
  ∀ (this : ∀ (i : ι), ∃ (K : Set (R i)), IsCompact K ∧ K ∈ 𝓝 ((x : (a : ι) → R a) i)),
    ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have₃ :
  ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i))
    (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)), ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have have₄ : ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i)) (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)),
  let Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i;
  ∀ (Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i),
    ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
Tactic: classical
    have : ∀ i, ∃ K, IsCompact K ∧ K ∈ 𝓝 (x i) := fun i ↦ exists_compact_mem_nhds (x i)
    choose K K_compact hK using this
    set Q : Set (Π i, R i) := univ.pi (fun i ↦ if i ∈ S then A i else K i) with Q_def
    have Q_compact : IsCompact Q := isCompact_univ_pi fun i ↦ by
      split_ifs with his
      · exact hAcompact i his
      · exact K_compact i
    set U : Set (Π i, R i) := Sᶜ.pi K
    have U_nhds : U ∈ 𝓝 (x : Π i, R i) := set_pi_mem_nhds hS fun i _ ↦ hK i
    have QU : (↑) ⁻¹' U ⊆ ((↑) ⁻¹' Q : Set (Πʳ i, [R i, A i]_[𝓟 S])) := fun y H i _ ↦ by
      dsimp only
      split_ifs with hi
      · exact y.2 hi
      · exact H i hi
    refine ⟨((↑) ⁻¹' Q), ?_, mem_of_superset ?_ QU⟩
    · refine isEmbedding_coe_of_principal.isCompact_preimage_iff ?_ |>.mpr Q_compact
      simp_rw [range_coe_principal, Q_def, pi_if, mem_univ, true_and]
      exact inter_subset_left
    · simpa only [isEmbedding_coe_of_principal.nhds_eq_comap] using preimage_mem_comap U_nhds
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
have have₁ have₂ :
  ∀ (this : ∀ (i : ι), ∃ (K : Set (R i)), IsCompact K ∧ K ∈ 𝓝 ((x : (a : ι) → R a) i)),
    ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have₃ :
  ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i))
    (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)), ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have₄ :
  ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i))
    (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)),
    let Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i;
    ∀ (Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i),
      ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have have₅ : ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i)) (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)),
  let Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i;
  ∀ (Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i) (Q_compact : IsCompact Q),
    ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
Tactic: classical
    have : ∀ i, ∃ K, IsCompact K ∧ K ∈ 𝓝 (x i) := fun i ↦ exists_compact_mem_nhds (x i)
    choose K K_compact hK using this
    set Q : Set (Π i, R i) := univ.pi (fun i ↦ if i ∈ S then A i else K i) with Q_def
    have Q_compact : IsCompact Q := isCompact_univ_pi fun i ↦ by
      split_ifs with his
      · exact hAcompact i his
      · exact K_compact i
    set U : Set (Π i, R i) := Sᶜ.pi K
    have U_nhds : U ∈ 𝓝 (x : Π i, R i) := set_pi_mem_nhds hS fun i _ ↦ hK i
    have QU : (↑) ⁻¹' U ⊆ ((↑) ⁻¹' Q : Set (Πʳ i, [R i, A i]_[𝓟 S])) := fun y H i _ ↦ by
      dsimp only
      split_ifs with hi
      · exact y.2 hi
      · exact H i hi
    refine ⟨((↑) ⁻¹' Q), ?_, mem_of_superset ?_ QU⟩
    · refine isEmbedding_coe_of_principal.isCompact_preimage_iff ?_ |>.mpr Q_compact
      simp_rw [range_coe_principal, Q_def, pi_if, mem_univ, true_and]
      exact inter_subset_left
    · simpa only [isEmbedding_coe_of_principal.nhds_eq_comap] using preimage_mem_comap U_nhds
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
have have₁ have₂ :
  ∀ (this : ∀ (i : ι), ∃ (K : Set (R i)), IsCompact K ∧ K ∈ 𝓝 ((x : (a : ι) → R a) i)),
    ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have₃ :
  ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i))
    (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)), ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have₄ :
  ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i))
    (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)),
    let Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i;
    ∀ (Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i),
      ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have₅ have₆ :
  ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i))
    (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)),
    let Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i;
    ∀ (Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i) (Q_compact : IsCompact Q),
      ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have have₇ : ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i)) (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)),
  let Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i;
  ∀ (Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i) (Q_compact : IsCompact Q),
    let U := Sᶜ.pi (α := R) K;
    ∀ (U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a)), ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
Tactic: classical
    have : ∀ i, ∃ K, IsCompact K ∧ K ∈ 𝓝 (x i) := fun i ↦ exists_compact_mem_nhds (x i)
    choose K K_compact hK using this
    set Q : Set (Π i, R i) := univ.pi (fun i ↦ if i ∈ S then A i else K i) with Q_def
    have Q_compact : IsCompact Q := isCompact_univ_pi fun i ↦ by
      split_ifs with his
      · exact hAcompact i his
      · exact K_compact i
    set U : Set (Π i, R i) := Sᶜ.pi K
    have U_nhds : U ∈ 𝓝 (x : Π i, R i) := set_pi_mem_nhds hS fun i _ ↦ hK i
    have QU : (↑) ⁻¹' U ⊆ ((↑) ⁻¹' Q : Set (Πʳ i, [R i, A i]_[𝓟 S])) := fun y H i _ ↦ by
      dsimp only
      split_ifs with hi
      · exact y.2 hi
      · exact H i hi
    refine ⟨((↑) ⁻¹' Q), ?_, mem_of_superset ?_ QU⟩
    · refine isEmbedding_coe_of_principal.isCompact_preimage_iff ?_ |>.mpr Q_compact
      simp_rw [range_coe_principal, Q_def, pi_if, mem_univ, true_and]
      exact inter_subset_left
    · simpa only [isEmbedding_coe_of_principal.nhds_eq_comap] using preimage_mem_comap U_nhds
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst : (i : ι) → TopologicalSpace (R i)
⊢ topologicalSpace R A 𝓕 =
    ⨆ (S : Set ι), ⨆ (hS : 𝓕 ≤ 𝓟 S), TopologicalSpace.coinduced (inclusion R A hS) (topologicalSpace R A (𝓟 S))
have simp_rw : topologicalSpace R A 𝓕 =
  ⨆ (S : Set ι),
    ⨆ (x : 𝓕 ≤ 𝓟 S),
      TopologicalSpace.coinduced (inclusion R A sorry) (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance)
Tactic: simp_rw [topologicalSpace_eq_of_principal, topologicalSpace]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst : (i : ι) → TopologicalSpace (R i)
X : Type u_3
inst_1 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i]_[𝓕] → X
⊢ Continuous[topologicalSpace R A 𝓕, inst_1] f ↔
    ∀ (S : Set ι) (hS : 𝓕 ≤ 𝓟 S), Continuous[topologicalSpace R A (𝓟 S), inst_1] (f ∘ inclusion R A hS)
have simp_rw : Continuous[topologicalSpace R A 𝓕, inst_1] f ↔
  ∀ (S : Set ι) (hS : 𝓕 ≤ 𝓟 S),
    Continuous[TopologicalSpace.induced DFunLike.coe inferInstance, inst_1] (f ∘ inclusion R A hS)
Tactic: simp_rw +instances [topologicalSpace_eq_of_principal, continuous_iSup_dom,
    continuous_coinduced_dom]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst : (i : ι) → TopologicalSpace (R i)
X : Type u_3
inst_1 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i]_[𝓕] → X
simp_rw :
  Continuous[topologicalSpace R A 𝓕, inst_1] f ↔
    ∀ (S : Set ι) (hS : 𝓕 ≤ 𝓟 S),
      Continuous[TopologicalSpace.induced DFunLike.coe inferInstance, inst_1] (f ∘ inclusion R A hS)
⊢ Continuous[topologicalSpace R A 𝓕, inst_1] f ↔
    ∀ (S : Set ι) (hS : 𝓕 ≤ 𝓟 S), Continuous[topologicalSpace R A (𝓟 S), inst_1] (f ∘ inclusion R A hS)
have simp_rw₁ : (∀ (i : Set ι) (i_1 : 𝓕 ≤ 𝓟 i),
    Continuous[TopologicalSpace.coinduced (inclusion R A i_1) (TopologicalSpace.induced DFunLike.coe inferInstance),
        inst_1]
      f) ↔
  ∀ (S : Set ι) (hS : 𝓕 ≤ 𝓟 S),
    Continuous[TopologicalSpace.induced DFunLike.coe inferInstance, inst_1] (f ∘ inclusion R A hS)
Tactic: simp_rw +instances [topologicalSpace_eq_of_principal, continuous_iSup_dom,
    continuous_coinduced_dom]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : cofinite ≤ 𝓟 S
p : ι → Prop
⊢ IsOpen[topologicalSpace R A (𝓟 S)]
    {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}
have rw : ∀ (hS : Membership.mem (γ := Filter ι) cofinite S) {p : ι → Prop},
  IsOpen[topologicalSpace R A (𝓟 S)]
    {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}
Tactic: rw [le_principal_iff] at hS
Cleared hypotheses: hS, p
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : Membership.mem (γ := Filter ι) cofinite S
p : ι → Prop
⊢ IsOpen[topologicalSpace R A (𝓟 S)]
    {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}
have h : Eq (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
  {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}
  (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A)
Tactic: convert!
    isOpen_set_pi (hS.inter_of_left {i | p i}) (fun i _ ↦ hAopen i) |>.preimage continuous_coe
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : Membership.mem (γ := Filter ι) cofinite S
p : ι → Prop
⊢ Eq (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
    {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}
    (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A)
have h : ∀ (f : Πʳ (i : ι), [R i, A i]_[𝓟 S]),
  Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
      {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i} f ↔
    Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
      (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A) f
Tactic: ext f
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : Membership.mem (γ := Filter ι) cofinite S
p : ι → Prop
f : Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
      {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i} f ↔
    Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
      (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A) f
have h : ∀
  (H :
    Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
      (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A) f)
  (i : ι) (hiT : p i), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i
Tactic: refine ⟨fun H i hi ↦ H i hi.2, fun H i hiT ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : Membership.mem (γ := Filter ι) cofinite S
p : ι → Prop
f : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H :
  Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A)
    f
i : ι
hiT : p i
⊢ (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i
have pos : ∀ (hiS : i ∈ S), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i
Tactic: by_cases hiS : i ∈ S
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : Membership.mem (γ := Filter ι) cofinite S
p : ι → Prop
f : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H :
  Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A)
    f
i : ι
hiT : p i
pos : ∀ (hiS : i ∈ S), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i
⊢ (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i
have neg : ∀ (hiS : i ∉ S), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i
Tactic: by_cases hiS : i ∈ S
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : cofinite ≤ 𝓟 S
⊢ IsOpen[topologicalSpace R A (𝓟 S)]
    {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}
have h : ∀ (x : Πʳ (i : ι), [R i, A i]_[𝓟 S]) (a : ι),
  (↑x : (i : ι) → (fun (i : ι) ↦ R i) i) a ∈ A a ↔ True → (↑x : (i : ι) → (fun (i : ι) ↦ R i) i) a ∈ A a
Tactic: convert! isOpen_forall_imp_mem_of_principal hAopen hS (p := fun _ ↦ True)
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
p : ι → Prop
⊢ IsOpen[topologicalSpace R A cofinite]
    {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}
have simp_rw : ∀ (i : Set ι) (i_1 : cofinite ≤ 𝓟 i),
  IsOpen[topologicalSpace R A (𝓟 i)]
    (inclusion R A i_1 ⁻¹' {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), p i → (↑f : (i : ι) → R i) i ∈ A i})
Tactic: simp_rw +instances [topologicalSpace_eq_iSup cofinite, isOpen_iSup_iff, isOpen_coinduced]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
⊢ IsOpen[topologicalSpace R A cofinite]
    {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}
have simp_rw : ∀ (i : Set ι) (i_1 : cofinite ≤ 𝓟 i),
  IsOpen[topologicalSpace R A (𝓟 i)]
    (inclusion R A i_1 ⁻¹' {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), (↑f : (i : ι) → R i) i ∈ A i})
Tactic: simp_rw +instances [topologicalSpace_eq_iSup cofinite, isOpen_iSup_iff, isOpen_coinduced]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : cofinite ≤ 𝓟 S
⊢ IsOpen[topologicalSpace R A cofinite] (range (inclusion R A hS))
have rw : IsOpen[topologicalSpace R A cofinite] {x : Πʳ (i : ι), [R i, A i] | ∀ᶠ (i : ι) in 𝓟 S, (x : (a : ι) → R a) i ∈ A i}
Tactic: rw [range_inclusion]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
⊢ IsOpen[topologicalSpace R A cofinite] (range (structureMap R A cofinite))
have rw : IsOpen[topologicalSpace R A cofinite]
  {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}
Tactic: rw [range_structureMap]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : cofinite ≤ 𝓟 S
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ 𝓝 (inclusion R A hS x) = Filter.map (inclusion R A hS) (𝓝 x)
have rw : 𝓝 (inclusion R A hS x) = 𝓝 (inclusion R A hS x)
Tactic: rw [isOpenEmbedding_inclusion_principal hAopen hS |>.map_nhds_eq x]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
x : (i : ι) → (↑(A i) : Type u_2)
⊢ Eq (α := Filter Πʳ (i : ι), [R i, A i]) (𝓝 (structureMap R A cofinite x))
    (Filter.map (structureMap R A cofinite) (𝓝 x))
have rw : Eq (α := Filter Πʳ (i : ι), [R i, A i]) (𝓝 (structureMap R A cofinite x)) (𝓝 (structureMap R A cofinite x))
Tactic: rw [isOpenEmbedding_structureMap hAopen |>.map_nhds_eq x]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (hypothesis)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | IsCompact (A i) ∧ (x : (a : ι) → R a) i ∈ A i}
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ 𝓝 x
have hS : cofinite ≤ 𝓟 S
Tactic: have hS : cofinite ≤ 𝓟 S := le_principal_iff.mpr (hAcompact.and x.2)
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (hypothesis)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | IsCompact (A i) ∧ (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ 𝓝 x
have hSx : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
Tactic: have hSx : ∀ i ∈ S, x i ∈ A i := fun i hi ↦ hi.2
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (hypothesis)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | IsCompact (A i) ∧ (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ 𝓝 x
have hSA : ∀ i ∈ S, IsCompact (A i)
Tactic: have hSA : ∀ i ∈ S, IsCompact (A i) := fun i hi ↦ hi.1