awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hSA : ∀ i ∈ S, IsCompact (A i)
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ 𝓝 x
have this : WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]
Tactic: haveI := weaklyLocallyCompactSpace_of_principal hS hSA
-- 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)
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
hSA : ∀ i ∈ S, IsCompact (A i)
this : WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ 𝓝 x
have rcases : ∀ (x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]) (hxx' : inclusion R A hS x' = x),
  ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ 𝓝 x
Tactic: rcases exists_inclusion_eq_of_eventually R A hS hSx with ⟨x', hxx'⟩
-- 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)
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
hSA : ∀ i ∈ S, IsCompact (A i)
this : WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ 𝓝 x
have rw : ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ Filter.map (inclusion R A hS) (𝓝 x')
Tactic: rw [← hxx', nhds_eq_map_inclusion hAopen]
-- 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)
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
hSA : ∀ i ∈ S, IsCompact (A i)
this : WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ Filter.map (inclusion R A hS) (𝓝 x')
have rcases : ∀ (K : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (K_compact : IsCompact K) (hK : K ∈ 𝓝 x'),
  ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ Filter.map (inclusion R A hS) (𝓝 x')
Tactic: rcases exists_compact_mem_nhds x' with ⟨K, K_compact, hK⟩
-- 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 : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
⊢ Continuous[instTopologicalSpaceProd, inst_1] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)
have refine : ∀
  (H :
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)),
  Continuous[instTopologicalSpaceProd, inst_1] f
Tactic: refine ⟨fun H S hS ↦ H.comp ((continuous_inclusion hS).prodMap continuous_id),
    fun H ↦ ?_⟩
-- 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 : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)
⊢ Continuous[instTopologicalSpaceProd, inst_1] f
have simp_rw : ∀ (x : Πʳ (i : ι), [R i, A i] × Y), Tendsto f (𝓝 x) (𝓝 (f x))
Tactic: simp_rw [continuous_iff_continuousAt, ContinuousAt]
-- 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)
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)
x : Πʳ (i : ι), [R i, A i]
y : Y
S : Set ι := {i : ι | (x : (a : ι) → R a) i ∈ A i}
⊢ Tendsto f (𝓝 (x, y)) (𝓝 (f (x, y)))
have hS : cofinite ≤ 𝓟 S
Tactic: have hS : cofinite ≤ 𝓟 S := le_principal_iff.mpr 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)
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)
x : Πʳ (i : ι), [R i, A i]
y : Y
S : Set ι := {i : ι | (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
⊢ Tendsto f (𝓝 (x, y)) (𝓝 (f (x, y)))
have hxS : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
Tactic: have hxS : ∀ i ∈ S, x i ∈ A i := fun i hi ↦ hi
-- 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 : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)
x : Πʳ (i : ι), [R i, A i]
y : Y
S : Set ι := {i : ι | (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
⊢ Tendsto f (𝓝 (x, y)) (𝓝 (f (x, y)))
have rcases : ∀ (x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]) (hxx' : inclusion R A hS x' = x), Tendsto f (𝓝 (x, y)) (𝓝 (f (x, y)))
Tactic: rcases exists_inclusion_eq_of_eventually R A hS hxS with ⟨x', hxx'⟩
-- 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 : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)
x : Πʳ (i : ι), [R i, A i]
y : Y
S : Set ι := {i : ι | (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ Tendsto f (𝓝 (x, y)) (𝓝 (f (x, y)))
have rw : Tendsto (f ∘ fun (p : Πʳ (i : ι), [R i, A i]_[𝓟 S] × Y) ↦ (inclusion R A hS p.1, id p.2)) (𝓝 (x', y))
  (𝓝 (f (inclusion R A hS x', y)))
Tactic: rw [← hxx', nhds_prod_eq, nhds_eq_map_inclusion hAopen hS x',
    ← Filter.map_id (f := 𝓝 y), prod_map_map_eq, ← nhds_prod_eq, tendsto_map'_iff]
-- 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 : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
⊢ Continuous[instTopologicalSpaceProd, inst_1] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))
have refine : ∀
  (H :
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))),
  Continuous[instTopologicalSpaceProd, inst_1] f
Tactic: refine ⟨fun H S hS ↦ H.comp (continuous_id.prodMap (continuous_inclusion hS)),
    fun H ↦ ?_⟩
-- 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 : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))
⊢ Continuous[instTopologicalSpaceProd, inst_1] f
have simp_rw : ∀ (x : Y × Πʳ (i : ι), [R i, A i]), Tendsto f (𝓝 x) (𝓝 (f x))
Tactic: simp_rw [continuous_iff_continuousAt, ContinuousAt]
-- 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)
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))
y : Y
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | (x : (a : ι) → R a) i ∈ A i}
⊢ Tendsto f (𝓝 (y, x)) (𝓝 (f (y, x)))
have hS : cofinite ≤ 𝓟 S
Tactic: have hS : cofinite ≤ 𝓟 S := le_principal_iff.mpr 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)
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))
y : Y
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
⊢ Tendsto f (𝓝 (y, x)) (𝓝 (f (y, x)))
have hxS : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
Tactic: have hxS : ∀ i ∈ S, x i ∈ A i := fun i hi ↦ hi
-- 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 : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))
y : Y
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
⊢ Tendsto f (𝓝 (y, x)) (𝓝 (f (y, x)))
have rcases : ∀ (x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]) (hxx' : inclusion R A hS x' = x), Tendsto f (𝓝 (y, x)) (𝓝 (f (y, x)))
Tactic: rcases exists_inclusion_eq_of_eventually R A hS hxS with ⟨x', hxx'⟩
-- 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 : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))
y : Y
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ Tendsto f (𝓝 (y, x)) (𝓝 (f (y, x)))
have rw : Tendsto (f ∘ fun (p : Y × Πʳ (i : ι), [R i, A i]_[𝓟 S]) ↦ (id p.1, inclusion R A hS p.2)) (𝓝 (y, x'))
  (𝓝 (f (y, inclusion R A hS x')))
Tactic: rw [← hxx', nhds_prod_eq, nhds_eq_map_inclusion hAopen hS x',
    ← Filter.map_id (f := 𝓝 y), prod_map_map_eq, ← nhds_prod_eq, tendsto_map'_iff]
-- 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)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst_1 : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst_1 i] (A' i)
X : Type u_4
inst_2 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
⊢ Continuous[instTopologicalSpaceProd, inst_2] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
have simp_rw : (∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S) (S_1 : Set ι) (hS_1 : cofinite ≤ 𝓟 S_1),
    Continuous[instTopologicalSpaceProd, inst_2]
      ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hS_1))) ↔
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
Tactic: simp_rw [continuous_dom_prod_right hAopen, continuous_dom_prod_left hAopen']
-- 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)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst_1 : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst_1 i] (A' i)
X : Type u_4
inst_2 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
⊢ (∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S) (S_1 : Set ι) (hS_1 : cofinite ≤ 𝓟 S_1),
      Continuous[instTopologicalSpaceProd, inst_2]
        ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hS_1))) ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
have refine : ∀
  (H :
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS)))
  (S : Set ι) (hS : cofinite ≤ 𝓟 S) (T : Set ι) (hT : cofinite ≤ 𝓟 T),
  Continuous[instTopologicalSpaceProd, inst_2] ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hT))
Tactic: refine ⟨fun H S hS ↦ H S hS S hS, fun H S hS T hT ↦ ?_⟩
-- 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)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst_1 : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst_1 i] (A' i)
X : Type u_4
inst_2 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
S : Set ι
hS : cofinite ≤ 𝓟 S
T : Set ι
hT : cofinite ≤ 𝓟 T
U : Set ι := S ∩ T
⊢ Continuous[instTopologicalSpaceProd, inst_2] ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hT))
have hU : cofinite ≤ 𝓟 (S ∩ T)
Tactic: have hU : cofinite ≤ 𝓟 (S ∩ T) := inf_principal ▸ le_inf hS hT
-- 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)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst_1 : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst_1 i] (A' i)
X : Type u_4
inst_2 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
S : Set ι
hS : cofinite ≤ 𝓟 S
T : Set ι
hT : cofinite ≤ 𝓟 T
U : Set ι := S ∩ T
hU : cofinite ≤ 𝓟 (S ∩ T)
⊢ Continuous[instTopologicalSpaceProd, inst_2] ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hT))
have hSU : 𝓟 U ≤ 𝓟 S
Tactic: have hSU : 𝓟 U ≤ 𝓟 S := principal_mono.mpr inter_subset_left
-- 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)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst_1 : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst_1 i] (A' i)
X : Type u_4
inst_2 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
S : Set ι
hS : cofinite ≤ 𝓟 S
T : Set ι
hT : cofinite ≤ 𝓟 T
U : Set ι := S ∩ T
hU : cofinite ≤ 𝓟 (S ∩ T)
hSU : 𝓟 U ≤ 𝓟 S
⊢ Continuous[instTopologicalSpaceProd, inst_2] ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hT))
have hTU : 𝓟 U ≤ 𝓟 T
Tactic: have hTU : 𝓟 U ≤ 𝓟 T := principal_mono.mpr inter_subset_right
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
n : Type u_3
inst : Finite n
X : Type u_4
inst_1 : TopologicalSpace X
A : n → ι → Type u_5
inst_2 : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst_2 j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
⊢ Continuous[Pi.topologicalSpace, inst_1] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[Pi.topologicalSpace, inst_1]
        (f ∘
          Pi.map (α := fun (x : n) ↦ Πʳ (i : ι), [A x i, C x i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
            fun (x : n) ↦ inclusion (A x) (C x) hS)
have refine : ∀
  (H :
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[Pi.topologicalSpace, inst_1]
        (f ∘
          Pi.map (α := fun (x : n) ↦ Πʳ (i : ι), [A x i, C x i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
            fun (x : n) ↦ inclusion (A x) (C x) hS)),
  Continuous[Pi.topologicalSpace, inst_1] f
Tactic: refine ⟨by fun_prop, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
n : Type u_3
inst : Finite n
X : Type u_4
inst_1 : TopologicalSpace X
A : n → ι → Type u_5
inst_2 : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst_2 j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst_1]
      (f ∘
        Pi.map (α := fun (x : n) ↦ Πʳ (i : ι), [A x i, C x i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
          fun (x : n) ↦ inclusion (A x) (C x) hS)
⊢ Continuous[Pi.topologicalSpace, inst_1] f
have simp_rw : ∀ (x : (j : n) → Πʳ (i : ι), [A j i, C j i]), Tendsto f (𝓝 x) (𝓝 (f x))
Tactic: simp_rw [continuous_iff_continuousAt, ContinuousAt]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
n : Type u_3
inst : Finite n
X : Type u_4
inst_1 : TopologicalSpace X
A : n → ι → Type u_5
inst_2 : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst_2 j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst_1]
      (f ∘
        Pi.map (α := fun (x : n) ↦ Πʳ (i : ι), [A x i, C x i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
          fun (x : n) ↦ inclusion (A x) (C x) hS)
x : (j : n) → Πʳ (i : ι), [A j i, C j i]
S : Set ι := {i : ι | ∀ (j : n), (x j : (a : ι) → A j a) i ∈ C j i}
⊢ cofinite ≤ 𝓟 S
have rw : Membership.mem (γ := Filter ι) cofinite S
Tactic: rw [le_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
n : Type u_3
inst : Finite n
X : Type u_4
inst_1 : TopologicalSpace X
A : n → ι → Type u_5
inst_2 : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst_2 j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst_1]
      (f ∘
        Pi.map (α := fun (x : n) ↦ Πʳ (i : ι), [A x i, C x i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
          fun (x : n) ↦ inclusion (A x) (C x) hS)
x : (j : n) → Πʳ (i : ι), [A j i, C j i]
S : Set ι := {i : ι | ∀ (j : n), (x j : (a : ι) → A j a) i ∈ C j i}
⊢ Membership.mem (γ := Filter ι) cofinite S
have change : ∀ᶠ (i : ι) in cofinite, ∀ (j : n), (x j : (a : ι) → A j a) i ∈ C j i
Tactic: change ∀ᶠ i in cofinite, ∀ j : n, x j i ∈ C j i
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (hypothesis)
Goal:
ι : Type u_1
n : Type u_3
inst : Finite n
X : Type u_4
inst_1 : TopologicalSpace X
A : n → ι → Type u_5
inst_2 : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst_2 j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst_1]
      (f ∘
        Pi.map (α := fun (x : n) ↦ Πʳ (i : ι), [A x i, C x i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
          fun (x : n) ↦ inclusion (A x) (C x) hS)
x : (j : n) → Πʳ (i : ι), [A j i, C j i]
S : Set ι := {i : ι | ∀ (j : n), (x j : (a : ι) → A j a) i ∈ C j i}
⊢ Tendsto f (𝓝 x) (𝓝 (f x))
have hS : cofinite ≤ 𝓟 S
Tactic: have hS : cofinite ≤ 𝓟 S := by
    rw [le_principal_iff]
    change ∀ᶠ i in cofinite, ∀ j : n, x j i ∈ C j i
    simp [-eventually_cofinite]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (hypothesis)
Goal:
ι : Type u_1
n : Type u_3
inst : Finite n
X : Type u_4
inst_1 : TopologicalSpace X
A : n → ι → Type u_5
inst_2 : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst_2 j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst_1]
      (f ∘
        Pi.map (α := fun (x : n) ↦ Πʳ (i : ι), [A x i, C x i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
          fun (x : n) ↦ inclusion (A x) (C x) hS)
x : (j : n) → Πʳ (i : ι), [A j i, C j i]
S : Set ι := {i : ι | ∀ (j : n), (x j : (a : ι) → A j a) i ∈ C j i}
hS : cofinite ≤ 𝓟 S
x' : (j : n) → Πʳ (i : ι), [A j i, C j i]_[𝓟 S] :=
  fun (j : n) ↦ mk (R := A j) (A := C j) (fun (i : ι) ↦ (x j : (a : ι) → A j a) i) ⋯
⊢ Tendsto f (𝓝 x) (𝓝 (f x))
have hxx' : Pi.map (α := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
    (fun (j : n) ↦ inclusion (A j) (C j) hS) x' =
  x
Tactic: have hxx' : Pi.map (fun j ↦ inclusion _ _ hS) x' = x := rfl