awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → MulZeroClass (G i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_4} (S i) (G i)
inst_4 : ∀ (i : ι), MulMemClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]
⊢ single (S := S) (G := G) A i ((x : (a : ι) → G a) i * r) = x * single (S := S) (G := G) A i r
have h : ∀ (j : ι),
  (single (S := S) (G := G) A i ((x : (a : ι) → G a) i * r) : (a : ι) → G a) j =
    (x * single (S := S) (G := G) A i r : (a : ι) → G a) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → MulZeroClass (G i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_4} (S i) (G i)
inst_4 : ∀ (i : ι), MulMemClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]
j : ι
⊢ (single (S := S) (G := G) A i ((x : (a : ι) → G a) i * r) : (a : ι) → G a) j =
    (x * single (S := S) (G := G) A i r : (a : ι) → G a) j
have h : (single (S := S) (G := G) A i ((x : (a : ι) → G a) i * r) : (a : ι) → G a) i =
  (x * single (S := S) (G := G) A i r : (a : ι) → G a) i
Tactic: rcases eq_or_ne i j with rfl | hne
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → MulZeroClass (G i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_4} (S i) (G i)
inst_4 : ∀ (i : ι), MulMemClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]
j : ι
h :
  (single (S := S) (G := G) A i ((x : (a : ι) → G a) i * r) : (a : ι) → G a) i =
    (x * single (S := S) (G := G) A i r : (a : ι) → G a) i
⊢ (single (S := S) (G := G) A i ((x : (a : ι) → G a) i * r) : (a : ι) → G a) j =
    (x * single (S := S) (G := G) A i r : (a : ι) → G a) j
have h₁ : ∀ (hne : i ≠ j),
  (single (S := S) (G := G) A i ((x : (a : ι) → G a) i * r) : (a : ι) → G a) j =
    (x * single (S := S) (G := G) A i r : (a : ι) → G a) j
Tactic: rcases eq_or_ne i j with rfl | hne
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → MulZeroClass (G i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_4} (S i) (G i)
inst_4 : ∀ (i : ι), MulMemClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]
⊢ single (S := S) (G := G) A i (r * (x : (a : ι) → G a) i) = single (S := S) (G := G) A i r * x
have h : ∀ (j : ι),
  (single (S := S) (G := G) A i (r * (x : (a : ι) → G a) i) : (a : ι) → G a) j =
    (single (S := S) (G := G) A i r * x : (a : ι) → G a) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → MulZeroClass (G i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_4} (S i) (G i)
inst_4 : ∀ (i : ι), MulMemClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]
j : ι
⊢ (single (S := S) (G := G) A i (r * (x : (a : ι) → G a) i) : (a : ι) → G a) j =
    (single (S := S) (G := G) A i r * x : (a : ι) → G a) j
have h : (single (S := S) (G := G) A i (r * (x : (a : ι) → G a) i) : (a : ι) → G a) i =
  (single (S := S) (G := G) A i r * x : (a : ι) → G a) i
Tactic: rcases eq_or_ne i j with rfl | hne
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → MulZeroClass (G i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_4} (S i) (G i)
inst_4 : ∀ (i : ι), MulMemClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]
j : ι
h :
  (single (S := S) (G := G) A i (r * (x : (a : ι) → G a) i) : (a : ι) → G a) i =
    (single (S := S) (G := G) A i r * x : (a : ι) → G a) i
⊢ (single (S := S) (G := G) A i (r * (x : (a : ι) → G a) i) : (a : ι) → G a) j =
    (single (S := S) (G := G) A i r * x : (a : ι) → G a) j
have h₁ : ∀ (hne : i ≠ j),
  (single (S := S) (G := G) A i (r * (x : (a : ι) → G a) i) : (a : ι) → G a) j =
    (single (S := S) (G := G) A i r * x : (a : ι) → G a) j
Tactic: rcases eq_or_ne i j with rfl | hne
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → Group (G i)
inst_3 : ∀ (i : ι), SubgroupClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
⊢ Eq (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i r⁻¹)
    (mulSingle (S := S) (G := G) A i r)⁻¹
have h : ∀ (i_1 : ι),
  (mulSingle (S := S) (G := G) A i r⁻¹ : (a : ι) → G a) i_1 =
    ((mulSingle (S := S) (G := G) A i r)⁻¹ : (a : ι) → G a) i_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → Group (G i)
inst_3 : ∀ (i : ι), SubgroupClass.{u_3, u_4} (S i) (G i)
i : ι
r s : G i
⊢ mulSingle (S := S) (G := G) A i (r / s) =
    HDiv.hDiv (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i r)
      (mulSingle (S := S) (G := G) A i s)
have h : ∀ (i_1 : ι),
  (mulSingle (S := S) (G := G) A i (r / s) : (a : ι) → G a) i_1 =
    (HDiv.hDiv (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i r)
          (mulSingle (S := S) (G := G) A i s) :
        (a : ι) → G a)
      i_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → Monoid (G i)
inst_3 : ∀ (i : ι), SubmonoidClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
n : ℕ
⊢ mulSingle (S := S) (G := G) A i (r ^ n) =
    HPow.hPow (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i r) n
have h : ∀ (i_1 : ι),
  (mulSingle (S := S) (G := G) A i (r ^ n) : (a : ι) → G a) i_1 =
    (HPow.hPow (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i r) n :
        (a : ι) → G a)
      i_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → Group (G i)
inst_3 : ∀ (i : ι), SubgroupClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
n : ℤ
⊢ mulSingle (S := S) (G := G) A i (r ^ n) =
    HPow.hPow (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i r) n
have h : ∀ (i_1 : ι),
  (mulSingle (S := S) (G := G) A i (r ^ n) : (a : ι) → G a) i_1 =
    (HPow.hPow (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i r) n :
        (a : ι) → G a)
      i_1
Tactic: ext
-- 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)
𝓖 : Filter ι
h : 𝓕 ≤ 𝓖
⊢ Continuous[topologicalSpace R A 𝓖, topologicalSpace R A 𝓕] (inclusion R A h)
have simp_rw : LE.le (α := TopologicalSpace Πʳ (i : ι), [R i, A i]_[𝓕])
  (⨆ (i : Set ι),
    ⨆ (x : 𝓖 ≤ 𝓟 i),
      TopologicalSpace.coinduced (inclusion R A h ∘ inclusion R A sorry)
        (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance))
  (⨆ (S : Set ι),
    ⨆ (hS : 𝓕 ≤ 𝓟 S),
      TopologicalSpace.coinduced (inclusion R A hS) (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance))
Tactic: simp_rw [continuous_iff_coinduced_le, topologicalSpace, coinduced_iSup, coinduced_compose]
-- 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 ι
⊢ LE.le (α := TopologicalSpace Πʳ (i : ι), [R i, A i]_[𝓟 S])
    (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance)
    (TopologicalSpace.coinduced (inclusion R A ⋯) (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance))
have rw : LE.le (α := TopologicalSpace Πʳ (i : ι), [R i, A i]_[𝓟 S])
  (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance)
  (TopologicalSpace.coinduced id (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance))
Tactic: rw [inclusion_eq_id R A (𝓟 S), @coinduced_id]
-- 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 ι
rw :
  LE.le (α := TopologicalSpace Πʳ (i : ι), [R i, A i]_[𝓟 S])
    (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance)
    (TopologicalSpace.coinduced id (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance))
⊢ LE.le (α := TopologicalSpace Πʳ (i : ι), [R i, A i]_[𝓟 S])
    (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance)
    (TopologicalSpace.coinduced (inclusion R A ⋯) (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance))
have rw₁ : LE.le (α := TopologicalSpace Πʳ (i : ι), [R i, A i]_[𝓟 S])
  (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance)
  (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance)
Tactic: rw [inclusion_eq_id R A (𝓟 S), @coinduced_id]
-- 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 : cofinite ≤ 𝓟 S
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 rw : ∀ (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
Tactic: rw [le_principal_iff, mem_cofinite] at hS
Cleared hypotheses: hS, hAcompact, 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)
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 this : ∀ (i : ι), ∃ (K : Set (R i)), IsCompact K ∧ K ∈ 𝓝 ((x : (a : ι) → R a) i)
Tactic: have : ∀ i, ∃ K, IsCompact K ∧ K ∈ 𝓝 (x i) := fun i ↦ exists_compact_mem_nhds (x i)
-- 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]
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 choose : ∀ (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: choose K K_compact hK using this
Cleared hypotheses: this
-- 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)
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]
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 Q_def : let Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i;
Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Tactic: set Q : Set (Π i, R i) := univ.pi (fun i ↦ if i ∈ S then A i else K i) with Q_def
-- 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]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
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
i : ι
⊢ IsCompact (if i ∈ S then A i else K i)
have pos : ∀ (his : i ∈ S), IsCompact (A i)
Tactic: split_ifs with his
-- 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]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
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
i : ι
pos : ∀ (his : i ∈ S), IsCompact (A i)
⊢ IsCompact (if i ∈ S then A i else K i)
have neg : ∀ (his : i ∉ S), IsCompact (K i)
Tactic: split_ifs with his
-- 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)
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]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
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 Q_compact : IsCompact Q
Tactic: have Q_compact : IsCompact Q := isCompact_univ_pi fun i ↦ by
      split_ifs with his
      · exact hAcompact i his
      · exact K_compact i
-- 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)
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]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
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
U : Set ((i : ι) → R i) := Sᶜ.pi (α := R) K
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a)
Tactic: have U_nhds : U ∈ 𝓝 (x : Π i, R i) := set_pi_mem_nhds hS fun i _ ↦ hK i
-- 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]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
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
U : Set ((i : ι) → R i) := Sᶜ.pi (α := R) K
U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a)
y : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H : Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) y
i : ι
h : Membership.mem (γ := Set ι) univ i
⊢ (y : (a : ι) → R a) i ∈ if i ∈ S then A i else K i
have pos : ∀ (hi : i ∈ S), (y : (a : ι) → R a) i ∈ A i
Tactic: split_ifs with 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)
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]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
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
U : Set ((i : ι) → R i) := Sᶜ.pi (α := R) K
U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a)
y : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H : Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) y
i : ι
h : Membership.mem (γ := Set ι) univ i
pos : ∀ (hi : i ∈ S), (y : (a : ι) → R a) i ∈ A i
⊢ (y : (a : ι) → R a) i ∈ if i ∈ S then A i else K i
have neg : ∀ (hi : i ∉ S), (y : (a : ι) → R a) i ∈ K i
Tactic: split_ifs with hi
-- 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)
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]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
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
U : Set ((i : ι) → R i) := Sᶜ.pi (α := R) K
U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a)
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have QU : Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)
Tactic: 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
-- 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]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
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
U : Set ((i : ι) → R i) := Sᶜ.pi (α := R) K
U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a)
QU : Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have refine_1 : IsCompact (X := Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' Q)
Tactic: refine ⟨((↑) ⁻¹' Q), ?_, mem_of_superset ?_ QU⟩
-- 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]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
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
U : Set ((i : ι) → R i) := Sᶜ.pi (α := R) K
U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a)
QU : Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)
refine_1 : IsCompact (X := Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' Q)
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have refine_2 : DFunLike.coe (β := R) ⁻¹' U ∈ 𝓝 x
Tactic: refine ⟨((↑) ⁻¹' Q), ?_, mem_of_superset ?_ QU⟩
-- 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]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
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
U : Set ((i : ι) → R i) := Sᶜ.pi (α := R) K
U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a)
QU : Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)
⊢ IsCompact (X := Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' Q)
have refine_1 : Q ⊆ range (ι := Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R))
Tactic: refine isEmbedding_coe_of_principal.isCompact_preimage_iff ?_ |>.mpr Q_compact
-- 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]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
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
U : Set ((i : ι) → R i) := Sᶜ.pi (α := R) K
U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a)
QU : Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)
⊢ Q ⊆ range (ι := Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R))
have refine_1 : Set.pi (α := R) {i : ι | i ∈ S} A ∩ Set.pi (α := R) {i : ι | i ∉ S} K ⊆ S.pi (α := R) A
Tactic: simp_rw [range_coe_principal, Q_def, pi_if, mem_univ, true_and]