awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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})
have 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})
Tactic: rw [pi_generateFrom_eq]
-- 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
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})
have 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}
Tactic: refine le_antisymm (generateFrom_anti ?_) (le_generateFrom ?_)
-- 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
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}
⊢ 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})
have 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
Tactic: refine le_antisymm (generateFrom_anti ?_) (le_generateFrom ?_)
-- 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
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)
have 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
Tactic: refine isOpen_iff_forall_mem_open.2 fun f hf => ?_
-- 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
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
⊢ ∃ 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
have 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
Tactic: choose c hcg hfc using fun a => sUnion_eq_univ_iff.1 (hg a) (f a)
-- 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
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
have 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)
Tactic: refine ⟨pi i t ∩ pi ((↑i)ᶜ : Set ι) c, inter_subset_left, ?_, ⟨hf, fun a _ => hfc a⟩⟩
-- 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
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}]
    ((↑i : Set ι).pi (α := X) t ∩ (↑i : Set ι)ᶜ.pi (α := X) c)
have 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))
Tactic: rw [← univ_pi_piecewise]
-- 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
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))
have intro : ∀ (a : ι), (↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c a ∈ g a
Tactic: refine GenerateOpen.basic _ ⟨_, fun a => ?_, rfl⟩
-- 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
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 : ι
⊢ (↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c a ∈ g a
have pos : a ∈ i → (↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c a ∈ g a
Tactic: by_cases a ∈ i
-- 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
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
⊢ (↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c a ∈ g a
have neg : a ∉ i → (↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c a ∈ g a
Tactic: by_cases a ∈ i
-- 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
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}]
    ((↑i : Set ι).pi (α := X) t ∩ (↑i : Set ι)ᶜ.pi (α := X) c)
have 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))
Tactic: classical
    rw [← univ_pi_piecewise]
    refine GenerateOpen.basic _ ⟨_, fun a => ?_, rfl⟩
    by_cases a ∈ i <;> simp [*]
-- 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
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))
⊢ 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)
have intro₃ : ∀ (a : ι), (↑i : Set ι).piecewise (β := fun (i : ι) ↦ Set (X i)) t c a ∈ g a
Tactic: classical
    rw [← univ_pi_piecewise]
    refine GenerateOpen.basic _ ⟨_, fun a => ?_, rfl⟩
    by_cases a ∈ i <;> simp [*]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
X : Type u_9
f : X → (i : ι) → A i
⊢ induced f (Pi.topologicalSpace (Y := A)) =
    ⨅ (i : ι), induced.{u_9, u_6} (Y := A i) (fun (x : X) ↦ f x i) inferInstance
have 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
Tactic: simp_rw [Pi.topologicalSpace, induced_iInf, induced_compose, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
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
⊢ induced f (Pi.topologicalSpace (Y := A)) =
    ⨅ (i : ι), induced.{u_9, u_6} (Y := A i) (fun (x : X) ↦ f x i) inferInstance
have 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)
Tactic: simp_rw [Pi.topologicalSpace, induced_iInf, induced_compose, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
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)
⊢ induced f (Pi.topologicalSpace (Y := A)) =
    ⨅ (i : ι), induced.{u_9, u_6} (Y := A i) (fun (x : X) ↦ f x i) inferInstance
have 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)
Tactic: simp_rw [Pi.topologicalSpace, induced_iInf, induced_compose, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
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] {x}
have rw : IsOpen[topologicalSpace] (Set.pi (α := A) univ fun (i : ι) ↦ {x i})
Tactic: rw [← univ_pi_singleton]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
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
have refine : ∀ (x : n → X), 𝓝 x = comap (fun (x : n → X) ↦ x ∘ f) (𝓝 (x ∘ f))
Tactic: refine ⟨isInducing_iff_nhds.mpr fun x ↦ ?_, hf.injective_comp_right⟩
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
s : Set (Sigma σ)
⊢ IsOpen[instTopologicalSpaceSigma] s ↔ ∀ (i : ι), IsOpen[inst i] (Sigma.mk (β := σ) i ⁻¹' s)
have rw : (∀ (i : ι), IsOpen[coinduced (Sigma.mk i) (inst i)] s) ↔ ∀ (i : ι), IsOpen[inst i] (Sigma.mk (β := σ) i ⁻¹' s)
Tactic: rw [isOpen_iSup_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst i] s
⊢ IsOpen[instTopologicalSpaceSigma] (Sigma.mk (β := σ) i '' s)
have rw : ∀ (i_1 : ι), IsOpen[inst i_1] (Sigma.mk (β := σ) i_1 ⁻¹' Sigma.mk (β := σ) i '' s)
Tactic: rw [isOpen_sigma_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst i] s
j : ι
⊢ IsOpen[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) i '' s)
have inl : ∀ (s : Set (σ j)) (hs : IsOpen[inst j] s), IsOpen[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) j '' s)
Tactic: rcases eq_or_ne j i with (rfl | hne)
Cleared hypotheses: i, s, hs
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
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)
⊢ IsOpen[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) i '' s)
have inr : ∀ (hne : j ≠ i), IsOpen[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) i '' s)
Tactic: rcases eq_or_ne j i with (rfl | hne)
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst i] s
j : ι
hne : j ≠ i
⊢ IsOpen[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) i '' s)
have inr : IsOpen[inst j] ∅
Tactic: rw [preimage_image_sigmaMk_of_ne hne]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst i] s
⊢ IsClosed[instTopologicalSpaceSigma] (Sigma.mk (β := σ) i '' s)
have rw : ∀ (i_1 : ι), IsClosed[inst i_1] (Sigma.mk (β := σ) i_1 ⁻¹' Sigma.mk (β := σ) i '' s)
Tactic: rw [isClosed_sigma_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst i] s
j : ι
⊢ IsClosed[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) i '' s)
have inl : ∀ (s : Set (σ j)) (hs : IsClosed[inst j] s), IsClosed[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) j '' s)
Tactic: rcases eq_or_ne j i with (rfl | hne)
Cleared hypotheses: i, s, hs
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst i] s
j : ι
inl : ∀ (s : Set (σ j)) (hs : IsClosed[inst j] s), IsClosed[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) j '' s)
⊢ IsClosed[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) i '' s)
have inr : ∀ (hne : j ≠ i), IsClosed[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) i '' s)
Tactic: rcases eq_or_ne j i with (rfl | hne)
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst i] s
j : ι
hne : j ≠ i
⊢ IsClosed[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) i '' s)
have inr : IsClosed[inst j] ∅
Tactic: rw [preimage_image_sigmaMk_of_ne hne]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
x : Sigma σ
⊢ 𝓝 x = Filter.map (mk (β := σ) (x.fst (β := σ))) (𝓝 (x.snd (β := σ)))
have mk : ∀ (fst : ι) (snd : σ fst),
  𝓝 (mk (β := σ) fst snd) =
    Filter.map (mk (β := σ) ((mk (β := σ) fst snd).fst (β := σ))) (𝓝 ((mk (β := σ) fst snd).snd (β := σ)))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen[instTopologicalSpaceSigma] (Sigma.fst (β := fun (a : ι) ↦ σ a) ⁻¹' s)
have rw : IsOpen[instTopologicalSpaceSigma] (⋃ i ∈ s, Sigma.fst (β := fun (a : ι) ↦ σ a) ⁻¹' {i})
Tactic: rw [← biUnion_of_singleton s, preimage_iUnion₂]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen[instTopologicalSpaceSigma] (⋃ i ∈ s, Sigma.fst (β := fun (a : ι) ↦ σ a) ⁻¹' {i})
have simp : IsOpen[instTopologicalSpaceSigma] (⋃ i ∈ s, range (Sigma.mk (β := fun (a : ι) ↦ σ a) i))
Tactic: simp only [← range_sigmaMk]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
⊢ Continuous[⨆ (i : ι), coinduced (Sigma.mk i) (inst i), inst_1] f ↔
    ∀ (i : ι), Continuous[inst i, inst_1] fun (a : σ i) ↦ f (Sigma.mk (β := σ) i a)
have rw : (∀ (i : ι), Continuous[coinduced (Sigma.mk i) (inst i), inst_1] f) ↔
  ∀ (i : ι), Continuous[inst i, inst_1] fun (a : σ i) ↦ f (Sigma.mk (β := σ) i a)
Tactic: rw [continuous_iSup_dom]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
⊢ IsInducing f ↔
    (∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
      ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
have refine_1 : ∀ (h : IsInducing f) (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
Tactic: refine ⟨fun h ↦ ⟨fun i ↦ h.comp IsEmbedding.sigmaMk.1, fun i ↦ ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
refine_1 : ∀ (h : IsInducing f) (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
⊢ IsInducing f ↔
    (∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
      ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
have refine_2 : ((∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
    ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i) →
  IsInducing f
Tactic: refine ⟨fun h ↦ ⟨fun i ↦ h.comp IsEmbedding.sigmaMk.1, fun i ↦ ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
h : IsInducing f
i : ι
⊢ ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
have refine_1 : ∀ (U : Set X) (hUo : IsOpen[inst_1] U) (hU : f ⁻¹' U = range (Sigma.mk (β := σ) i)),
  ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
Tactic: rcases h.isOpen_iff.1 (isOpen_range_sigmaMk (i := i)) with ⟨U, hUo, hU⟩
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
h : IsInducing f
i : ι
U : Set X
hUo : IsOpen[inst_1] U
hU : f ⁻¹' U = range (Sigma.mk (β := σ) i)
⊢ ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
have refine_1 : ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
Tactic: refine ⟨U, hUo, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
⊢ ((∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
      ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i) →
    IsInducing f
have refine_2 : ((∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
    ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i) →
  ∀ (h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i))
    (h₂ : ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i) (x : Sigma σ)
    (i : ι) (x : σ i), 𝓝 (Sigma.mk (β := σ) i x) = comap f (𝓝 (f (Sigma.mk (β := σ) i x)))
Tactic: refine fun ⟨h₁, h₂⟩ ↦ isInducing_iff_nhds.2 fun ⟨i, x⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
h :
  (∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
    ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)
h₂ : ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
x_1 : Sigma σ
i : ι
x : σ i
⊢ 𝓝 (Sigma.mk (β := σ) i x) = comap f (𝓝 (f (Sigma.mk (β := σ) i x)))
have refine_2 : range (Sigma.mk (β := σ) i) ∈ comap f (𝓝 (f (Sigma.mk (β := σ) i x)))
Tactic: rw [Sigma.nhds_mk, (h₁ i).nhds_eq_comap, comp_apply, ← comap_comap, map_comap_of_mem]