awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
n : ℕ
A : Fin (n + 1) → Type u_9
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : X → A 0
g : X → (j : Fin n) → A j.succ
hf : Continuous[inst, inst_1 0] f
hg : Continuous[inst, Pi.topologicalSpace] g
⊢ Continuous[inst, Pi.topologicalSpace] fun (a : X) ↦ Fin.cons (α := A) (f a) (g a)

Tactic:
continuous_iff_continuousAt.2 fun _ => hf.continuousAt.finCons hg.continuousAt

Premises used: Iff.mpr, Continuous.continuousAt, ContinuousAt.finCons, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
Z : Type u_1
inst : TopologicalSpace Z
n : ℕ
f : Y → Z
g : Y → Fin n → Z
l : Filter Y
x : Z
y : Fin n → Z
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
⊢ Tendsto (fun (a : Y) ↦ Matrix.vecCons (f a) (g a)) l (𝓝 (Matrix.vecCons x y))

Tactic:
hf.finCons hg

Premises used: Matrix.vecCons, Filter.Tendsto.finCons
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Z : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Z
n : ℕ
f : X → Z
g : X → Fin n → Z
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt.{u, u_1} (Y := Fin n.succ → Z) (fun (a : X) ↦ Matrix.vecCons (f a) (g a)) x

Tactic:
hf.finCons hg

Premises used: ContinuousAt.finCons, Matrix.vecCons
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Z : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Z
n : ℕ
f : X → Z
g : X → Fin n → Z
hf : Continuous[inst, inst_1] f
hg : Continuous[inst, Pi.topologicalSpace] g
⊢ Continuous[inst, Pi.topologicalSpace] fun (a : X) ↦ Matrix.vecCons (f a) (g a)

Tactic:
hf.finCons hg

Premises used: Continuous.finCons, Matrix.vecCons
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → (j : Fin n) → A j.castSucc
g : Y → A (Fin.last n)
l : Filter Y
x : (j : Fin n) → A j.castSucc
y : A (Fin.last n)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ Tendsto (β := A (Fin.last n)) (fun (i : Y) ↦ Fin.snoc (α := A) (f i) (g i) (Fin.last n)) l
    (𝓝 (Fin.snoc (α := A) x y (Fin.last n)))

Tactic:
simpa
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → (j : Fin n) → A j.castSucc
g : Y → A (Fin.last n)
l : Filter Y
x : (j : Fin n) → A j.castSucc
y : A (Fin.last n)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (i : Fin n),
    Tendsto (β := A i.castSucc) (fun (i_1 : Y) ↦ Fin.snoc (α := A) (f i_1) (g i_1) i.castSucc) l
      (𝓝 (Fin.snoc (α := A) x y i.castSucc))

Tactic:
simpa using tendsto_pi_nhds.1 hf

Premises used: tendsto_pi_nhds, Iff.mp
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
n : ℕ
A : Fin (n + 1) → Type u_9
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : X → (j : Fin n) → A j.castSucc
g : X → A (Fin.last n)
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt.{u, u_9} (Y := (i : Fin (n + 1)) → A i) (fun (a : X) ↦ Fin.snoc (α := A) (f a) (g a)) x

Tactic:
hf.tendsto.finSnoc hg

Premises used: ContinuousAt, ContinuousAt.tendsto, Filter.Tendsto.finSnoc
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
n : ℕ
A : Fin (n + 1) → Type u_9
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : X → (j : Fin n) → A j.castSucc
g : X → A (Fin.last n)
hf : Continuous[inst, Pi.topologicalSpace] f
hg : Continuous[inst, inst_1 (Fin.last n)] g
⊢ Continuous[inst, Pi.topologicalSpace] fun (a : X) ↦ Fin.snoc (α := A) (f a) (g a)

Tactic:
continuous_iff_continuousAt.2 fun _ => hf.continuousAt.finSnoc hg.continuousAt

Premises used: Iff.mpr, ContinuousAt.finSnoc, Continuous.continuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst : (i : Fin (n + 1)) → TopologicalSpace (A i)
i : Fin (n + 1)
f : Y → A i
g : Y → (j : Fin n) → A (i.succAbove j)
l : Filter Y
x : A i
y : (j : Fin n) → A (i.succAbove j)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ Tendsto (fun (i_1 : Y) ↦ i.insertNth (α := A) (f i_1) (g i_1) i) l (𝓝 (i.insertNth (α := A) x y i))

Tactic:
simpa
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst : (i : Fin (n + 1)) → TopologicalSpace (A i)
i : Fin (n + 1)
f : Y → A i
g : Y → (j : Fin n) → A (i.succAbove j)
l : Filter Y
x : A i
y : (j : Fin n) → A (i.succAbove j)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (j : Fin n),
    Tendsto (β := A (i.succAbove j)) (fun (i_1 : Y) ↦ i.insertNth (α := A) (f i_1) (g i_1) (i.succAbove j)) l
      (𝓝 (i.insertNth (α := A) x y (i.succAbove j)))

Tactic:
simpa using tendsto_pi_nhds.1 hg

Premises used: tendsto_pi_nhds, Iff.mp
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
n : ℕ
A : Fin (n + 1) → Type u_9
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)
i : Fin (n + 1)
f : X → A i
g : X → (j : Fin n) → A (i.succAbove j)
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt.{u, u_9} (Y := (j : Fin (n + 1)) → A j) (fun (a : X) ↦ i.insertNth (α := A) (f a) (g a)) x

Tactic:
hf.tendsto.finInsertNth i hg

Premises used: ContinuousAt, Filter.Tendsto.finInsertNth, ContinuousAt.tendsto
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
n : ℕ
A : Fin (n + 1) → Type u_9
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)
i : Fin (n + 1)
f : X → A i
g : X → (j : Fin n) → A (i.succAbove j)
hf : Continuous[inst, inst_1 i] f
hg : Continuous[inst, Pi.topologicalSpace] g
⊢ Continuous[inst, Pi.topologicalSpace] fun (a : X) ↦ i.insertNth (α := A) (f a) (g a)

Tactic:
continuous_iff_continuousAt.2 fun _ => hf.continuousAt.finInsertNth i hg.continuousAt

Premises used: Iff.mpr, ContinuousAt.finInsertNth, Continuous.continuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → (j : Fin (n + 1)) → A j
l : Filter Y
x : (j : Fin (n + 1)) → A j
hg : Tendsto f l (𝓝 x)
⊢ Tendsto (fun (a : Y) ↦ Fin.init (α := A) (f a)) l (𝓝 (Fin.init (α := A) x))

Tactic:
tendsto_pi_nhds.2 fun j ↦ apply_nhds hg j.castSucc

Premises used: Iff.mpr, tendsto_pi_nhds, Filter.Tendsto.apply_nhds, Fin.castSucc
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
n : ℕ
A : Fin (n + 1) → Type u_9
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : X → (j : Fin (n + 1)) → A j
x : X
hf : ContinuousAt f x
⊢ ContinuousAt.{u, u_9} (Y := (i : Fin n) → A i.castSucc) (fun (a : X) ↦ Fin.init (α := A) (f a)) x

Tactic:
hf.tendsto.finInit

Premises used: ContinuousAt, Filter.Tendsto.finInit, ContinuousAt.tendsto
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
n : ℕ
A : Fin (n + 1) → Type u_9
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : X → (j : Fin (n + 1)) → A j
hf : Continuous[inst, Pi.topologicalSpace] f
⊢ Continuous[inst, Pi.topologicalSpace] fun (a : X) ↦ Fin.init (α := A) (f a)

Tactic:
continuous_iff_continuousAt.2 fun _ ↦ hf.continuousAt.finInit

Premises used: Iff.mpr, ContinuousAt.finInit, Continuous.continuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → (j : Fin (n + 1)) → A j
l : Filter Y
x : (j : Fin (n + 1)) → A j
hg : Tendsto f l (𝓝 x)
⊢ Tendsto (fun (a : Y) ↦ Fin.tail (α := A) (f a)) l (𝓝 (Fin.tail (α := A) x))

Tactic:
tendsto_pi_nhds.2 fun j ↦ apply_nhds hg j.succ

Premises used: Iff.mpr, Fin.succ, tendsto_pi_nhds, Filter.Tendsto.apply_nhds
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
n : ℕ
A : Fin (n + 1) → Type u_9
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : X → (j : Fin (n + 1)) → A j
x : X
hf : ContinuousAt f x
⊢ ContinuousAt.{u, u_9} (Y := (i : Fin n) → A i.succ) (fun (a : X) ↦ Fin.tail (α := A) (f a)) x

Tactic:
hf.tendsto.finTail

Premises used: ContinuousAt, ContinuousAt.tendsto, Filter.Tendsto.finTail
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
n : ℕ
A : Fin (n + 1) → Type u_9
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : X → (j : Fin (n + 1)) → A j
hf : Continuous[inst, Pi.topologicalSpace] f
⊢ Continuous[inst, Pi.topologicalSpace] fun (a : X) ↦ Fin.tail (α := A) (f a)

Tactic:
continuous_iff_continuousAt.2 fun _ ↦ hf.continuousAt.finTail

Premises used: Iff.mpr, Continuous.continuousAt, ContinuousAt.finTail, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hi : i.Finite
hs : ∀ a ∈ i, IsOpen[T a] (s a)
rw : IsOpen[Pi.topologicalSpace] (⋂ a ∈ i, eval (β := A) a ⁻¹' s a)
⊢ IsOpen[Pi.topologicalSpace] (i.pi (α := A) s)

Tactic:
rw [pi_def]

Premises used: Set.pi_def
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hi : i.Finite
hs : ∀ a ∈ i, IsOpen[T a] (s a)
⊢ IsOpen[Pi.topologicalSpace] (⋂ a ∈ i, eval (β := A) a ⁻¹' s a)

Tactic:
hi.isOpen_biInter fun a ha => (hs _ ha).preimage (continuous_apply _)

Premises used: continuous_apply, Set.Finite.isOpen_biInter, IsOpen.preimage
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hi : i.Finite
hs : ∀ a ∈ i, IsOpen[T a] (s a)
⊢ IsOpen[Pi.topologicalSpace] (⋂ a ∈ i, eval (β := A) a ⁻¹' s a)

Tactic:
exact hi.isOpen_biInter fun a ha => (hs _ ha).preimage (continuous_apply _)

Premises used: continuous_apply, Set.Finite.isOpen_biInter, IsOpen.preimage
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
rw :
  (∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔
    ∀ f ∈ s,
      ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
        (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I : Set ι).pi (α := A) u ⊆ s
⊢ IsOpen[Pi.topologicalSpace] s ↔
    ∀ f ∈ s,
      ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
        (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I : Set ι).pi (α := A) u ⊆ s

Tactic:
rw [isOpen_iff_nhds]

Premises used: isOpen_iff_nhds
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
simp_rw :
  (∀ 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,
      ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
        (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I : Set ι).pi (α := A) u ⊆ s
⊢ (∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔
    ∀ f ∈ s,
      ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
        (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I : Set ι).pi (α := A) u ⊆ s

Tactic:
simp_rw [le_principal_iff, nhds_pi, Filter.mem_pi', mem_nhds_iff]

Premises used: Filter.mem_pi', Filter.le_principal_iff, mem_nhds_iff, nhds_pi
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
⊢ (∀ 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,
      ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
        (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I : Set ι).pi (α := A) u ⊆ s

Tactic:
forall₂_congr fun a _ => ⟨?_, ?_⟩

Premises used: forall₂_congr, Iff.intro
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
refine_1 :
  ∀ 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) →
      ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
        (∀ a_2 ∈ I, IsOpen[T a_2] (u a_2) ∧ a a_2 ∈ u a_2) ∧ (↑I : Set ι).pi (α := A) u ⊆ s
refine_2 :
  ∀ a ∈ s,
    (∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
        (∀ a_1 ∈ I, IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ (↑I : Set ι).pi (α := A) 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
⊢ (∀ 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,
      ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
        (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I : Set ι).pi (α := A) u ⊆ s

Tactic:
refine forall₂_congr fun a _ => ⟨?_, ?_⟩

Premises used: forall₂_congr, Iff.intro
-- Module: Mathlib.Topology.Constructions
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 : Finset ι) (u : (a : ι) → Set (A a)),
    (∀ a_1 ∈ I, IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ (↑I : Set ι).pi (α := A) u ⊆ s

Tactic:
⟨I, fun a => eval a '' (I : Set ι).pi fun a => (h1 a).choose, fun i hi => ?_, ?_⟩

Premises used: Function.eval, SetLike.coe, And.intro, Exists.intro, Set.image, Exists.choose, Set.pi
-- Module: Mathlib.Topology.Constructions
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
refine_1 :
  ∀ (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)
refine_1₁ :
  ((↑I : Set ι).pi (α := A) 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)) ⊆
    s
⊢ ∃ (I : Finset ι) (u : (a : ι) → Set (A a)),
    (∀ a_1 ∈ I, IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ (↑I : Set ι).pi (α := A) u ⊆ s

Tactic:
refine ⟨I, fun a => eval a '' (I : Set ι).pi fun a => (h1 a).choose, fun i hi => ?_, ?_⟩
-- Module: Mathlib.Topology.Constructions
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
refine_1 :
  IsOpen[T i] (⋯.choose (p := fun (t_1 : Set (A i)) ↦ t_1 ⊆ t i ∧ IsOpen[T i] t_1 ∧ a i ∈ t_1)) ∧
    a i ∈ ⋯.choose (p := fun (t_1 : Set (A i)) ↦ t_1 ⊆ t i ∧ IsOpen[T i] t_1 ∧ a i ∈ t_1)
⊢ 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)

Tactic:
simp_rw [eval_image_pi (Finset.mem_coe.mpr hi)
          (pi_nonempty_iff.mpr fun i => ⟨_, fun _ => (h1 i).choose_spec.2.2⟩)]

Premises used: Iff.mpr, Exists.choose_spec, And.right, Exists.intro, Set.eval_image_pi, Finset.mem_coe, Set.pi_nonempty_iff
-- Module: Mathlib.Topology.Constructions
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] (⋯.choose (p := fun (t_1 : Set (A i)) ↦ t_1 ⊆ t i ∧ IsOpen[T i] t_1 ∧ a i ∈ t_1)) ∧
    a i ∈ ⋯.choose (p := fun (t_1 : Set (A i)) ↦ t_1 ⊆ t i ∧ IsOpen[T i] t_1 ∧ a i ∈ t_1)

Tactic:
(h1 i).choose_spec.2

Premises used: Exists.choose_spec, And.right
-- Module: Mathlib.Topology.Constructions
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] (⋯.choose (p := fun (t_1 : Set (A i)) ↦ t_1 ⊆ t i ∧ IsOpen[T i] t_1 ∧ a i ∈ t_1)) ∧
    a i ∈ ⋯.choose (p := fun (t_1 : Set (A i)) ↦ t_1 ⊆ t i ∧ IsOpen[T i] t_1 ∧ a i ∈ t_1)

Tactic:
exact (h1 i).choose_spec.2

Premises used: Exists.choose_spec, And.right
-- Module: Mathlib.Topology.Constructions
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 : Set ι).pi (α := A) 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)) ⊆
    s

Tactic:
Subset.trans
        (pi_mono fun i hi => (eval_image_pi_subset hi).trans (h1 i).choose_spec.1) h2

Premises used: Exists.choose_spec, Set.eval_image_pi_subset, Set.Subset.trans, HasSubset.Subset.trans, And.left, Set.pi_mono
-- Module: Mathlib.Topology.Constructions
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 : Set ι).pi (α := A) 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)) ⊆
    s

Tactic:
exact Subset.trans
        (pi_mono fun i hi => (eval_image_pi_subset hi).trans (h1 i).choose_spec.1) h2

Premises used: Set.eval_image_pi_subset, Set.Subset.trans, HasSubset.Subset.trans, Set.pi_mono
-- Module: Mathlib.Topology.Constructions
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

Tactic:
⟨I, fun a => ite (a ∈ I) (t a) univ, fun i => ?_, ?_⟩

Premises used: Set.univ, Membership.mem, And.intro, Exists.intro, ite
-- Module: Mathlib.Topology.Constructions
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
refine_2₁ : ((↑I : Set ι).pi (α := A) fun (a : ι) ↦ if a ∈ I then t a else univ) ⊆ 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 ⟨I, fun a => ite (a ∈ I) (t a) univ, fun i => ?_, ?_⟩
-- Module: Mathlib.Topology.Constructions
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
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
⊢ ∃ 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
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
h_1 : 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
h : t i ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i ∧ IsOpen[T i] (t i) ∧ a i ∈ t i
⊢ ∃ t_1 ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1

Tactic:
use t i
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
h_1 : 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
h : t i ⊆ t i ∧ IsOpen[T i] (t i) ∧ a i ∈ t i
⊢ t i ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i ∧ IsOpen[T i] (t i) ∧ a i ∈ t i

Tactic:
simp_rw [if_pos hi]

Premises used: if_pos
-- Module: Mathlib.Topology.Constructions
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 ⊆ t i ∧ IsOpen[T i] (t i) ∧ a i ∈ t i

Tactic:
⟨Subset.rfl, (h1 i) hi⟩

Premises used: Set.Subset.rfl, And.intro
-- Module: Mathlib.Topology.Constructions
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 ⊆ t i ∧ IsOpen[T i] (t i) ∧ a i ∈ t i

Tactic:
exact ⟨Subset.rfl, (h1 i) hi⟩
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
h_1 : 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
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)
⊢ ∃ t_1 ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1

Tactic:
use univ

Premises used: Set.univ
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
h_1 : 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
h : Subset.{u_6} (α := Set (A i)) univ univ ∧ IsOpen[T i] univ ∧ Membership.mem (γ := Set (A i)) univ (a 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)

Tactic:
simp_rw [if_neg hi]

Premises used: if_neg
-- Module: Mathlib.Topology.Constructions
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 univ ∧ IsOpen[T i] univ ∧ Membership.mem (γ := Set (A i)) univ (a i)

Tactic:
⟨Subset.rfl, isOpen_univ, mem_univ _⟩

Premises used: isOpen_univ, Set.Subset.rfl, And.intro, Set.mem_univ