awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Constructions
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
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))
⊢ 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:
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]

Premises used: le_iInf, coinduced_le_iff_le_induced, Iff.mp, le_generateFrom
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
⊢ Eq (α := TopologicalSpace ((i : ι) → A i)) (Pi.topologicalSpace (Y := A)) (Pi.topologicalSpace (Y := A))

Tactic:
simp +instances only [generateFrom_setOf_isOpen]

Premises used: TopologicalSpace.generateFrom_setOf_isOpen
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
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})
⊢ 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 ι

Premises used: nonempty_fintype
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
intro :
  Eq (α := TopologicalSpace ((i : ι) → X i))
    (generateFrom
      {t : Set ((i : ι) → X i) |
        ∃ (s : (a : ι) → Set (X a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := X) s})
    (generateFrom
      {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s})
⊢ 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:
rw [pi_generateFrom_eq]

Premises used: pi_generateFrom_eq
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
⊢ Eq (α := TopologicalSpace ((i : ι) → X i))
    (generateFrom
      {t : Set ((i : ι) → X i) |
        ∃ (s : (a : ι) → Set (X a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := X) s})
    (generateFrom
      {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s})

Tactic:
le_antisymm (generateFrom_anti ?_) (le_generateFrom ?_)

Premises used: TopologicalSpace.generateFrom_anti, le_antisymm, le_generateFrom
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
intro :
  Subset (α := Set (Set ((i : ι) → X i)))
    {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s}
    {t : Set ((i : ι) → X i) |
      ∃ (s : (a : ι) → Set (X a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := X) s}
intro₁ :
  ∀ (s : Set ((i : ι) → X i)),
    Membership.mem (γ := Set (Set ((i : ι) → X i)))
        {t : Set ((i : ι) → X i) |
          ∃ (s : (a : ι) → Set (X a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := X) s}
        s →
      IsOpen[generateFrom
            {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}]
        s
⊢ Eq (α := TopologicalSpace ((i : ι) → X i))
    (generateFrom
      {t : Set ((i : ι) → X i) |
        ∃ (s : (a : ι) → Set (X a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := X) s})
    (generateFrom
      {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s})

Tactic:
refine le_antisymm (generateFrom_anti ?_) (le_generateFrom ?_)

Premises used: TopologicalSpace.generateFrom_anti, le_antisymm, le_generateFrom
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
s : Set ((i : ι) → X i)
h :
  Membership.mem (γ := Set (Set ((i : ι) → X i)))
    {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s} s
t : (a : ι) → Set (X a)
ht : ∀ (a : ι), t a ∈ g a
Eq : s = Set.pi (α := X) univ t
⊢ (∀ (a : ι), Membership.mem (γ := Finset ι) Finset.univ a → t a ∈ g a) ∧ s = (↑Finset.univ : Set ι).pi (α := X) t

Tactic:
simp [ht, Eq]
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
⊢ Subset (α := Set (Set ((i : ι) → X i)))
    {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s}
    {t : Set ((i : ι) → X i) |
      ∃ (s : (a : ι) → Set (X a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := X) s}

Tactic:
exact fun s ⟨t, ht, Eq⟩ => ⟨t, Finset.univ, by simp [ht, Eq]⟩
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) :=
  generateFrom
    {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s}
⊢ IsOpen[generateFrom {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}]
    ((↑i : Set ι).pi (α := X) t)

Tactic:
isOpen_iff_forall_mem_open.2 fun f hf => ?_

Premises used: Iff.mpr, isOpen_iff_forall_mem_open
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) :=
  generateFrom
    {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s}
intro :
  ∀ (f : (i : ι) → X i) (hf : f ∈ (↑i : Set ι).pi (α := X) t),
    ∃ t_1 ⊆ (↑i : Set ι).pi (α := X) t,
      IsOpen[generateFrom
              {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}]
          t_1 ∧
        f ∈ t_1
⊢ IsOpen[generateFrom {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}]
    ((↑i : Set ι).pi (α := X) t)

Tactic:
refine isOpen_iff_forall_mem_open.2 fun f hf => ?_

Premises used: Iff.mpr, isOpen_iff_forall_mem_open
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) :=
  generateFrom
    {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s}
f : (i : ι) → X i
hf : f ∈ (↑i : Set ι).pi (α := X) t
intro :
  ∀ (c : (a : ι) → Set (X a)) (hcg : ∀ (a : ι), c a ∈ g a) (hfc : ∀ (a : ι), f a ∈ c a),
    ∃ t_1 ⊆ (↑i : Set ι).pi (α := X) t,
      IsOpen[generateFrom
              {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}]
          t_1 ∧
        f ∈ t_1
⊢ ∃ t_1 ⊆ (↑i : Set ι).pi (α := X) t,
    IsOpen[generateFrom {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}]
        t_1 ∧
      f ∈ t_1

Tactic:
choose c hcg hfc using fun a => sUnion_eq_univ_iff.1 (hg a) (f a)

Premises used: Iff.mp, Set.sUnion_eq_univ_iff
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) :=
  generateFrom
    {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s}
f : (i : ι) → X i
hf : f ∈ (↑i : Set ι).pi (α := X) t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
⊢ ∃ t_1 ⊆ (↑i : Set ι).pi (α := X) t,
    IsOpen[generateFrom {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}]
        t_1 ∧
      f ∈ t_1

Tactic:
⟨pi i t ∩ pi ((↑i)ᶜ : Set ι) c, inter_subset_left, ?_, ⟨hf, fun a _ => hfc a⟩⟩

Premises used: Compl.compl, Set.inter_subset_left, Inter.inter, SetLike.coe, And.intro, Exists.intro, Set.pi
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) :=
  generateFrom
    {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s}
f : (i : ι) → X i
hf : f ∈ (↑i : Set ι).pi (α := X) t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
intro :
  IsOpen[generateFrom {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}]
    ((↑i : Set ι).pi (α := X) t ∩ (↑i : Set ι)ᶜ.pi (α := X) c)
⊢ ∃ t_1 ⊆ (↑i : Set ι).pi (α := X) t,
    IsOpen[generateFrom {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}]
        t_1 ∧
      f ∈ t_1

Tactic:
refine ⟨pi i t ∩ pi ((↑i)ᶜ : Set ι) c, inter_subset_left, ?_, ⟨hf, fun a _ => hfc a⟩⟩
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) :=
  generateFrom
    {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s}
f : (i : ι) → X i
hf : f ∈ (↑i : Set ι).pi (α := X) t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
intro :
  IsOpen[generateFrom {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}]
    (Set.pi (α := X) univ ((↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c))
⊢ IsOpen[generateFrom {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}]
    ((↑i : Set ι).pi (α := X) t ∩ (↑i : Set ι)ᶜ.pi (α := X) c)

Tactic:
rw [← univ_pi_piecewise]

Premises used: Set.univ_pi_piecewise
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) :=
  generateFrom
    {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s}
f : (i : ι) → X i
hf : f ∈ (↑i : Set ι).pi (α := X) t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
⊢ IsOpen[generateFrom {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}]
    (Set.pi (α := X) univ ((↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c))

Tactic:
GenerateOpen.basic _ ⟨_, fun a => ?_, rfl⟩

Premises used: TopologicalSpace.GenerateOpen.basic, And.intro, Exists.intro, IsOpen, rfl
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) :=
  generateFrom
    {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s}
f : (i : ι) → X i
hf : f ∈ (↑i : Set ι).pi (α := X) t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
intro : ∀ (a : ι), (↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c a ∈ g a
⊢ IsOpen[generateFrom {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}]
    (Set.pi (α := X) univ ((↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c))

Tactic:
refine GenerateOpen.basic _ ⟨_, fun a => ?_, rfl⟩
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) :=
  generateFrom
    {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s}
f : (i : ι) → X i
hf : f ∈ (↑i : Set ι).pi (α := X) t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
pos : a ∈ i → (↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c a ∈ g a
neg : a ∉ i → (↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c a ∈ g a
⊢ (↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c a ∈ g a

Tactic:
by_cases a ∈ i
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) :=
  generateFrom
    {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s}
f : (i : ι) → X i
hf : f ∈ (↑i : Set ι).pi (α := X) t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
h : a ∈ i
⊢ (↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c a ∈ g a

Tactic:
simp [*]
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) :=
  generateFrom
    {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s}
f : (i : ι) → X i
hf : f ∈ (↑i : Set ι).pi (α := X) t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
h : a ∉ i
⊢ (↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c a ∈ g a

Tactic:
simp [*]
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) :=
  generateFrom
    {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi (α := X) univ s}
f : (i : ι) → X i
hf : f ∈ (↑i : Set ι).pi (α := X) t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
intro intro₁ intro₂ :
  IsOpen[generateFrom {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}]
    (Set.pi (α := X) univ ((↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c))
intro₃ : ∀ (a : ι), (↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c a ∈ g a
⊢ IsOpen[generateFrom {t : Set ((i : ι) → X i) | ∃ (s : (a : ι) → Set (X a)), (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}]
    ((↑i : Set ι).pi (α := X) t ∩ (↑i : Set ι)ᶜ.pi (α := X) c)

Tactic:
classical
    rw [← univ_pi_piecewise]
    refine GenerateOpen.basic _ ⟨_, fun a => ?_, rfl⟩
    by_cases a ∈ i <;> simp [*]

Premises used: Set.univ_pi_piecewise
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
X : Type u_9
f : X → (i : ι) → A i
simp_rw :
  induced f (⨅ (i : ι), induced (fun (f : (i : ι) → A i) ↦ f i) (T i)) =
    ⨅ (i : ι), induced.{u_9, u_6} (Y := A i) (fun (x : X) ↦ f x i) inferInstance
simp_rw₁ :
  Eq.{u_9 + 1} (α := TopologicalSpace X) (⨅ (i : ι), induced f (induced (fun (f : (i : ι) → A i) ↦ f i) (T i)))
    (⨅ (i : ι), induced.{u_9, u_6} (Y := A i) (fun (x : X) ↦ f x i) inferInstance)
simp_rw₂ :
  Eq.{u_9 + 1} (α := TopologicalSpace X) (⨅ (i : ι), induced ((fun (f : (i : ι) → A i) ↦ f i) ∘ f) (T i))
    (⨅ (i : ι), induced.{u_9, u_6} (Y := A i) (fun (x : X) ↦ f x i) inferInstance)
⊢ induced f (Pi.topologicalSpace (Y := A)) =
    ⨅ (i : ι), induced.{u_9, u_6} (Y := A i) (fun (x : X) ↦ f x i) inferInstance

Tactic:
simp_rw [Pi.topologicalSpace, induced_iInf, induced_compose, Function.comp_def]

Premises used: Pi.topologicalSpace, induced_compose, Function.comp_def, induced_iInf
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
X : Type u_9
f : (i : ι) → X → A i
⊢ IsInducing (Y := (i : ι) → A i) fun (x : X) (i : ι) ↦ f i x

Tactic:
letI := ⨅ i, induced (f i) inferInstance; ⟨(induced_to_pi _).symm⟩

Premises used: Topology.IsInducing.mk, induced_to_pi, Eq.symm
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
κ : Type u_8
inst : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
inst_1 : (i : ι) → TopologicalSpace (B i)
f : X → (i : ι) → A i
inst_2 : TopologicalSpace Z
inst_3 : Finite ι
inst_4 : ∀ (i : ι), DiscreteTopology.{u_6} (A i)
x : (i : ι) → A i
rw : IsOpen[topologicalSpace] (Set.pi (α := A) univ fun (i : ι) ↦ {x i})
⊢ IsOpen[topologicalSpace] {x}

Tactic:
rw [← univ_pi_singleton]

Premises used: Set.univ_pi_singleton
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
κ : Type u_8
inst : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
inst_1 : (i : ι) → TopologicalSpace (B i)
f : X → (i : ι) → A i
inst_2 : TopologicalSpace Z
inst_3 : Finite ι
inst_4 : ∀ (i : ι), DiscreteTopology.{u_6} (A i)
x : (i : ι) → A i
⊢ IsOpen[topologicalSpace] (Set.pi (α := A) univ fun (i : ι) ↦ {x i})

Tactic:
isOpen_set_pi finite_univ fun i _ => (isOpen_discrete {x i})

Premises used: isOpen_set_pi, Set.finite_univ, isOpen_discrete, Singleton.singleton
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
κ : Type u_8
inst : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
inst_1 : (i : ι) → TopologicalSpace (B i)
f : X → (i : ι) → A i
inst_2 : TopologicalSpace Z
inst_3 : Finite ι
inst_4 : ∀ (i : ι), DiscreteTopology.{u_6} (A i)
x : (i : ι) → A i
⊢ IsOpen[topologicalSpace] (Set.pi (α := A) univ fun (i : ι) ↦ {x i})

Tactic:
exact isOpen_set_pi finite_univ fun i _ => (isOpen_discrete {x i})

Premises used: isOpen_set_pi, Set.finite_univ, isOpen_discrete, Singleton.singleton
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
n : Type u_9
m : Type u_10
f : m → n
hf : Surjective f
⊢ IsEmbedding (Y := m → X) fun (x : n → X) ↦ x ∘ f

Tactic:
⟨isInducing_iff_nhds.mpr fun x ↦ ?_, hf.injective_comp_right⟩

Premises used: Iff.mpr, Function.Surjective.injective_comp_right, Topology.isInducing_iff_nhds, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
n : Type u_9
m : Type u_10
f : m → n
hf : Surjective f
refine : ∀ (x : n → X), 𝓝 x = comap (fun (x : n → X) ↦ x ∘ f) (𝓝 (x ∘ f))
⊢ IsEmbedding (Y := m → X) fun (x : n → X) ↦ x ∘ f

Tactic:
refine ⟨isInducing_iff_nhds.mpr fun x ↦ ?_, hf.injective_comp_right⟩
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
n : Type u_9
m : Type u_10
f : m → n
hf : Surjective f
x : n → X
⊢ 𝓝 x = comap (fun (x : n → X) ↦ x ∘ f) (𝓝 (x ∘ f))

Tactic:
simp only [nhds_pi, Filter.pi, Filter.comap_iInf, ← hf.iInf_congr, Filter.comap_comap,
    Function.comp_def]

Premises used: nhds_pi, Filter.comap_iInf, Function.comp_def, Filter.comap_comap, Filter.pi, Function.Surjective.iInf_congr
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
⊢ Continuous[inst i, instTopologicalSpaceSigma] (Sigma.mk (β := σ) i)

Tactic:
continuous_iSup_rng continuous_coinduced_rng

Premises used: continuous_iSup_rng, continuous_coinduced_rng
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
s : Set (Sigma σ)
rw : (∀ (i : ι), IsOpen[coinduced (Sigma.mk i) (inst i)] s) ↔ ∀ (i : ι), IsOpen[inst i] (Sigma.mk (β := σ) i ⁻¹' s)
⊢ IsOpen[instTopologicalSpaceSigma] s ↔ ∀ (i : ι), IsOpen[inst i] (Sigma.mk (β := σ) i ⁻¹' s)

Tactic:
rw [isOpen_iSup_iff]

Premises used: isOpen_iSup_iff
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
s : Set (Sigma σ)
⊢ (∀ (i : ι), IsOpen[coinduced (Sigma.mk i) (inst i)] s) ↔ ∀ (i : ι), IsOpen[inst i] (Sigma.mk (β := σ) i ⁻¹' s)

Tactic:
rfl
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
s : Set (Sigma σ)
⊢ IsClosed[instTopologicalSpaceSigma] s ↔ ∀ (i : ι), IsClosed[inst i] (Sigma.mk (β := σ) i ⁻¹' s)

Tactic:
simp only [← isOpen_compl_iff, isOpen_sigma_iff, preimage_compl]

Premises used: Set.preimage_compl, isOpen_sigma_iff, isOpen_compl_iff
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst i] s
rw : ∀ (i_1 : ι), IsOpen[inst i_1] (Sigma.mk (β := σ) i_1 ⁻¹' Sigma.mk (β := σ) i '' s)
⊢ IsOpen[instTopologicalSpaceSigma] (Sigma.mk (β := σ) i '' s)

Tactic:
rw [isOpen_sigma_iff]

Premises used: isOpen_sigma_iff
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst i] s
j : ι
inl : ∀ (s : Set (σ j)) (hs : IsOpen[inst j] s), IsOpen[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) j '' s)
inr : ∀ (hne : j ≠ i), IsOpen[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) i '' s)
⊢ IsOpen[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) i '' s)

Tactic:
rcases eq_or_ne j i with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
j : ι
s : Set (σ j)
hs inl inl₁ inl₂ inl₃ : IsOpen[inst j] s
⊢ IsOpen[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) j '' s)

Tactic:
rwa [preimage_image_eq _ sigma_mk_injective]

Premises used: Set.preimage_image_eq, sigma_mk_injective
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst i] s
j : ι
hne : j ≠ i
inr : IsOpen[inst j] ∅
⊢ IsOpen[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) i '' s)

Tactic:
rw [preimage_image_sigmaMk_of_ne hne]

Premises used: Set.preimage_image_sigmaMk_of_ne