awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι
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)
have refine_1 : IsOpen[T i] (sorry.choose (p := fun (t_1 : Set (A i)) ↦ t_1 ⊆ t i ∧ IsOpen[T i] t_1 ∧ a i ∈ t_1)) ∧
  a i ∈ sorry.choose (p := fun (t_1 : Set (A i)) ↦ t_1 ⊆ t i ∧ IsOpen[T i] t_1 ∧ a i ∈ t_1)
Tactic: simp_rw [eval_image_pi (Finset.mem_coe.mpr hi)
          (pi_nonempty_iff.mpr fun i => ⟨_, fun _ => (h1 i).choose_spec.2.2⟩)]
-- 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 : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ 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
have refine_2 : ∀ (i : ι), ∃ t_1 ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1
Tactic: refine ⟨I, fun a => ite (a ∈ I) (t a) univ, fun i => ?_, ?_⟩
-- 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 : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
refine_2 : ∀ (i : ι), ∃ t_1 ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1
⊢ ∃ (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
have refine_2₁ : ((↑I : Set ι).pi (α := A) fun (a : ι) ↦ if a ∈ I then t a else univ) ⊆ s
Tactic: refine ⟨I, fun a => ite (a ∈ I) (t a) univ, fun i => ?_, ?_⟩
-- 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 : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
i : ι
⊢ ∃ t_1 ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1
have pos : ∀ (hi : i ∈ I), ∃ t_1 ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1
Tactic: by_cases hi : i ∈ I
-- 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 : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
i : ι
pos : ∀ (hi : i ∈ I), ∃ t_1 ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1
⊢ ∃ t_1 ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1
have neg : ∀ (hi : i ∉ I), ∃ t_1 ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1
Tactic: by_cases hi : i ∈ I
-- 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 : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
i : ι
hi : i ∈ I
⊢ ∃ t_1 ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1
have h : t i ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i ∧ IsOpen[T i] (t i) ∧ a i ∈ t i
Tactic: use t i
-- 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 : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
i : ι
hi : i ∈ I
⊢ t i ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i ∧ IsOpen[T i] (t i) ∧ a i ∈ t i
have h : t i ⊆ t i ∧ IsOpen[T i] (t i) ∧ a i ∈ t i
Tactic: simp_rw [if_pos 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 : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
i : ι
hi : i ∉ I
⊢ ∃ t_1 ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1
have h : Subset.{u_6} (α := Set (A i)) univ ((fun (a : ι) ↦ if a ∈ I then t a else univ) i) ∧
  IsOpen[T i] univ ∧ Membership.mem (γ := Set (A i)) univ (a i)
Tactic: use univ
-- 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 : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
i : ι
hi : i ∉ I
⊢ Subset.{u_6} (α := Set (A i)) univ ((fun (a : ι) ↦ if a ∈ I then t a else univ) i) ∧
    IsOpen[T i] univ ∧ Membership.mem (γ := Set (A i)) univ (a i)
have h : Subset.{u_6} (α := Set (A i)) univ univ ∧ IsOpen[T i] univ ∧ Membership.mem (γ := Set (A i)) univ (a i)
Tactic: simp_rw [if_neg 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 : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
⊢ ((↑I : Set ι).pi (α := A) fun (a : ι) ↦ if a ∈ I then t a else univ) ⊆ s
have refine_2 : (Set.pi (α := A) univ fun (i : ι) ↦ if i ∈ (↑I : Set ι) then if i ∈ I then t i else univ else univ) ⊆ s
Tactic: rw [← univ_pi_ite]
-- 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 : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ 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
have refine_2 : ∀ (i : ι), ∃ t_1 ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1
Tactic: classical
    refine ⟨I, fun a => ite (a ∈ I) (t a) univ, fun i => ?_, ?_⟩
    · by_cases hi : i ∈ I
      · use t i
        simp_rw [if_pos hi]
        exact ⟨Subset.rfl, (h1 i) hi⟩
      · use univ
        simp_rw [if_neg hi]
        exact ⟨Subset.rfl, isOpen_univ, mem_univ _⟩
    · rw [← univ_pi_ite]
      simp only [← ite_and, ← Finset.mem_coe, and_self_iff, univ_pi_ite, h2]
-- 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 : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
refine_2 : ∀ (i : ι), ∃ t_1 ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1
⊢ ∃ (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
have refine_2₁ : ((↑I : Set ι).pi (α := A) fun (a : ι) ↦ if a ∈ I then t a else univ) ⊆ s
Tactic: classical
    refine ⟨I, fun a => ite (a ∈ I) (t a) univ, fun i => ?_, ?_⟩
    · by_cases hi : i ∈ I
      · use t i
        simp_rw [if_pos hi]
        exact ⟨Subset.rfl, (h1 i) hi⟩
      · use univ
        simp_rw [if_neg hi]
        exact ⟨Subset.rfl, isOpen_univ, mem_univ _⟩
    · rw [← univ_pi_ite]
      simp only [← ite_and, ← Finset.mem_coe, and_self_iff, univ_pi_ite, h2]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : Finite ι
s : Set ((a : ι) → A a)
⊢ IsOpen[Pi.topologicalSpace] s ↔
    ∀ f ∈ s, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ u ⊆ s
have intro : ∀ (val : Fintype ι),
  IsOpen[Pi.topologicalSpace] s ↔
    ∀ f ∈ s, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ u ⊆ s
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
⊢ IsOpen[Pi.topologicalSpace] s ↔
    ∀ f ∈ s, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ u ⊆ s
have intro : (∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔
  ∀ f ∈ s, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ 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)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
⊢ (∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔
    ∀ f ∈ s, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ u ⊆ s
have intro : (∀ 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, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ 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)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
⊢ (∀ 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, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ u ⊆ s
have intro : ∀ 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) →
    ∃ (u : (a : ι) → Set (A a)), (∀ (a_2 : ι), IsOpen[T a_2] (u a_2) ∧ a a_2 ∈ u a_2) ∧ Set.pi (α := A) univ 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)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
intro :
  ∀ 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) →
      ∃ (u : (a : ι) → Set (A a)), (∀ (a_2 : ι), IsOpen[T a_2] (u a_2) ∧ a a_2 ∈ u a_2) ∧ Set.pi (α := A) univ 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, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ u ⊆ s
have intro₁ : ∀ a ∈ s,
  (∃ (u : (a : ι) → Set (A a)), (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi (α := A) univ 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)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
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
⊢ ∃ (u : (a : ι) → Set (A a)), (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi (α := A) univ u ⊆ s
have intro : Set.pi (α := A) univ t ⊆ (↑I : Set ι).pi (α := A) t
Tactic: refine
      ⟨fun i => (h1 i).choose,
        ⟨fun i => (h1 i).choose_spec.2,
          (pi_mono fun i _ => (h1 i).choose_spec.1).trans (Subset.trans ?_ h2)⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
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
⊢ Set.pi (α := A) univ t ⊆ (↑I : Set ι).pi (α := A) t
have intro : (↑I : Set ι).pi (α := A) t ∩ (↑I : Set ι)ᶜ.pi (α := A) t ⊆ (↑I : Set ι).pi (α := A) t
Tactic: rw [← pi_inter_compl (I : Set ι)]
-- 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)
hs : ∀ a ∈ i, IsClosed[T a] (s a)
⊢ IsClosed[Pi.topologicalSpace] (i.pi (α := A) s)
have rw : IsClosed[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)
I : Set ι
s : (i : ι) → Set (A i)
a : (i : ι) → A i
hs : I.pi (α := A) s ∈ 𝓝 a
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)
have rw : ∀ (hs : Membership.mem (γ := Filter ((i : ι) → A i)) (Filter.pi (α := A) fun (i : ι) ↦ 𝓝 (a i)) (I.pi (α := A) s))
  {i : ι} (hi : i ∈ I), s i ∈ 𝓝 (a i)
Tactic: rw [nhds_pi] at hs
Cleared hypotheses: hs, i, hi
-- 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)
x : (a : ι) → A a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
⊢ i.pi (α := A) s ∈ 𝓝 x
have rw : ∀ i_1 ∈ i, eval (β := A) i_1 ⁻¹' s i_1 ∈ 𝓝 x
Tactic: rw [pi_def, biInter_mem hi]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (A i)
a : (i : ι) → A i
⊢ I.pi (α := A) s ∈ 𝓝 a ↔ ∀ i ∈ I, s i ∈ 𝓝 (a i)
have rw : Membership.mem (γ := Filter ((i : ι) → A i)) (Filter.pi (α := A) fun (i : ι) ↦ 𝓝 (a i)) (I.pi (α := A) s) ↔
  ∀ i ∈ I, s i ∈ 𝓝 (a i)
Tactic: rw [nhds_pi, pi_mem_pi_iff hI]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (A i)
a : (i : ι) → A i
rw :
  Membership.mem (γ := Filter ((i : ι) → A i)) (Filter.pi (α := A) fun (i : ι) ↦ 𝓝 (a i)) (I.pi (α := A) s) ↔
    ∀ i ∈ I, s i ∈ 𝓝 (a i)
⊢ I.pi (α := A) s ∈ 𝓝 a ↔ ∀ i ∈ I, s i ∈ 𝓝 (a i)
have rw₁ : (∀ i ∈ I, s i ∈ 𝓝 (a i)) ↔ ∀ i ∈ I, s i ∈ 𝓝 (a i)
Tactic: rw [nhds_pi, pi_mem_pi_iff hI]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (A i)
⊢ interior (I.pi (α := A) s) = I.pi (α := A) fun (i : ι) ↦ interior (s i)
have h : ∀ (a : (i : ι) → A i),
  a ∈ interior (I.pi (α := A) s) ↔
    Membership.mem (γ := Set ((i : ι) → A i)) (I.pi (α := A) fun (i : ι) ↦ interior (s i)) a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Topology.Constructions (hypothesis)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : DecidableEq ι
s : Set ((a : ι) → A a)
x : (a : ι) → A a
hs : s ∈ 𝓝 x
y : (a : ι) → A a
⊢ ∃ (I : Finset ι), I.piecewise (π := A) x y ∈ s
have hs₁ : ∃ (I : Finset ι) (t : (i : ι) → Set (A i)), (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ (↑I : Set ι).pi (α := A) t ⊆ s
Tactic: simp only [nhds_pi, Filter.mem_pi'] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : DecidableEq ι
s : Set ((a : ι) → A a)
x y : (a : ι) → A a
hs : ∃ (I : Finset ι) (t : (i : ι) → Set (A i)), (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ (↑I : Set ι).pi (α := A) t ⊆ s
⊢ ∃ (I : Finset ι), I.piecewise (π := A) x y ∈ s
have rcases : ∀ (I : Finset ι) (t : (i : ι) → Set (A i)) (htx : ∀ (i : ι), t i ∈ 𝓝 (x i)) (hts : (↑I : Set ι).pi (α := A) t ⊆ s),
  ∃ (I : Finset ι), I.piecewise (π := A) x y ∈ s
Tactic: rcases hs with ⟨I, t, htx, hts⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : DecidableEq ι
s : Set ((a : ι) → A a)
x y : (a : ι) → A a
I : Finset ι
t : (i : ι) → Set (A i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : (↑I : Set ι).pi (α := A) t ⊆ s
⊢ ∃ (I : Finset ι), I.piecewise (π := A) x y ∈ s
have refine : ∀ (i : ι) (hi : i ∈ (↑I : Set ι)), I.piecewise (π := A) x y i ∈ t i
Tactic: refine ⟨I, hts fun i hi => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ Eq (α := TopologicalSpace ((i : ι) → A i)) (Pi.topologicalSpace (Y := A))
    (generateFrom
      {t : Set ((i : ι) → A i) |
        ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})
have refine_1 : LE.le (α := TopologicalSpace ((i : ι) → A i)) (Pi.topologicalSpace (Y := A))
  (generateFrom
    {t : Set ((i : ι) → A i) |
      ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
refine_1 :
  LE.le (α := TopologicalSpace ((i : ι) → A i)) (Pi.topologicalSpace (Y := A))
    (generateFrom
      {t : Set ((i : ι) → A i) |
        ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})
⊢ Eq (α := TopologicalSpace ((i : ι) → A i)) (Pi.topologicalSpace (Y := A))
    (generateFrom
      {t : Set ((i : ι) → A i) |
        ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})
have refine_2 : LE.le (α := TopologicalSpace ((i : ι) → A i))
  (generateFrom
    {t : Set ((i : ι) → A i) |
      ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})
  (Pi.topologicalSpace (Y := A))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ LE.le (α := TopologicalSpace ((i : ι) → A i)) (Pi.topologicalSpace (Y := A))
    (generateFrom
      {t : Set ((i : ι) → A i) |
        ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})
have refine_1 : ∀ (s : Set ((i : ι) → A i)),
  Membership.mem (γ := Set (Set ((i : ι) → A i)))
      {t : Set ((i : ι) → A i) |
        ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s}
      s →
    IsOpen[Pi.topologicalSpace] s
Tactic: apply le_generateFrom
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ LE.le (α := TopologicalSpace ((i : ι) → A i))
    (generateFrom
      {t : Set ((i : ι) → A i) |
        ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})
    (Pi.topologicalSpace (Y := A))
have refine_2 : ∀ (i : ι) (s : Set (A i)) (hs : s ∈ g i),
  IsOpen[coinduced (fun (f : (i : ι) → A i) ↦ f i)
        (generateFrom
          {t : Set ((i : ι) → A i) |
            ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi s})]
    s
Tactic: refine le_iInf fun i => coinduced_le_iff_le_induced.1 <| le_generateFrom fun s hs => ?_
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
i : ι
s : Set (A i)
hs : s ∈ g i
⊢ IsOpen[coinduced (fun (f : (i : ι) → A i) ↦ f i)
        (generateFrom
          {t : Set ((i : ι) → A i) |
            ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi s})]
    s
have refine_2 : (∀ (a : ι),
    Membership.mem (γ := Finset ι) {i} a →
      Membership.mem (α := Set (A a)) (g a)
        (update (β := fun (a : ι) ↦ Set (A a)) (fun (i : ι) ↦ univ) i s a : Set (A a))) ∧
  Eq (α := Set ((i : ι) → A i)) ((fun (f : (i : ι) → A i) ↦ f i) ⁻¹' s)
    ((↑{i} : Set ι).pi (α := A) (update (β := fun (a : ι) ↦ Set (A a)) (fun (i : ι) ↦ univ) i s))
Tactic: refine GenerateOpen.basic _ ⟨update (fun i => univ) i s, {i}, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ LE.le (α := TopologicalSpace ((i : ι) → A i))
    (generateFrom
      {t : Set ((i : ι) → A i) |
        ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})
    (Pi.topologicalSpace (Y := A))
have refine_2 : ∀ (i : ι) (s : Set (A i)) (hs : s ∈ g i),
  IsOpen[coinduced (fun (f : (i : ι) → A i) ↦ f i)
        (generateFrom
          {t : Set ((i : ι) → A i) |
            ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi s})]
    s
Tactic: classical
    refine le_iInf fun i => coinduced_le_iff_le_induced.1 <| le_generateFrom fun s hs => ?_
    refine GenerateOpen.basic _ ⟨update (fun i => univ) i s, {i}, ?_⟩
    simp [hs]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
refine_2 :
  ∀ (i : ι) (s : Set (A i)) (hs : s ∈ g i),
    IsOpen[coinduced (fun (f : (i : ι) → A i) ↦ f i)
          (generateFrom
            {t : Set ((i : ι) → A i) |
              ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi s})]
      s
⊢ LE.le (α := TopologicalSpace ((i : ι) → A i))
    (generateFrom
      {t : Set ((i : ι) → A i) |
        ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})
    (Pi.topologicalSpace (Y := A))
have refine_2₁ : ∀ (i : ι) (s : Set (A i)) (hs : s ∈ g i),
  (∀ (a : ι),
      Membership.mem (γ := Finset ι) {i} a →
        Membership.mem (α := Set (A a)) (g a)
          (update (β := fun (a : ι) ↦ Set (A a)) (fun (i : ι) ↦ univ) i s a : Set (A a))) ∧
    Eq (α := Set ((i : ι) → A i)) ((fun (f : (i : ι) → A i) ↦ f i) ⁻¹' s)
      ((↑{i} : Set ι).pi (α := A) (update (β := fun (a : ι) ↦ Set (A a)) (fun (i : ι) ↦ univ) i s))
Tactic: classical
    refine le_iInf fun i => coinduced_le_iff_le_induced.1 <| le_generateFrom fun s hs => ?_
    refine GenerateOpen.basic _ ⟨update (fun i => univ) i s, {i}, ?_⟩
    simp [hs]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
⊢ Eq (α := TopologicalSpace ((i : ι) → X i)) (Pi.topologicalSpace (Y := X))
    (generateFrom
      {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s})
have intro : ∀ (val : Fintype ι),
  Eq (α := TopologicalSpace ((i : ι) → X i)) (Pi.topologicalSpace (Y := X))
    (generateFrom
      {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s})
Tactic: cases nonempty_fintype ι