awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
t : Set β
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure[t_1] cs
ct : Set β
ct_count : ct.Countable
hct : t ⊆ closure[inst] ct
⊢ s ×ˢ t ⊆ closure[instTopologicalSpaceProd] (cs ×ˢ ct)
have rw : s ×ˢ t ⊆ closure[t_1] cs ×ˢ closure[inst] ct
Tactic: rw [closure_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
hs : IsSeparable s
f : α → β
hf : Continuous[t, inst] f
⊢ IsSeparable (f '' s)
have rcases : ∀ (c : Set α) (c_count : c.Countable) (hc : s ⊆ closure[t] c), IsSeparable (f '' s)
Tactic: rcases hs with ⟨c, c_count, hc⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous[t, inst] f
c : Set α
c_count : c.Countable
hc : s ⊆ closure[t] c
⊢ IsSeparable (f '' s)
have refine : f '' s ⊆ closure[inst] (f '' c)
Tactic: refine ⟨f '' c, c_count.image _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous[t, inst] f
c : Set α
c_count : c.Countable
hc : s ⊆ closure[t] c
⊢ f '' s ⊆ closure[inst] (f '' c)
have rw : s ⊆ f ⁻¹' closure[inst] (f '' c)
Tactic: rw [image_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
⊢ IsSeparable s ↔ SeparableSpace α
have simp_rw : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ SeparableSpace α
Tactic: simp_rw [IsSeparable, separableSpace_iff, dense_iff_closure_eq, ← univ_subset_iff,
    ← hs.closure_eq, isClosed_closure.closure_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
simp_rw : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ SeparableSpace α
⊢ IsSeparable s ↔ SeparableSpace α
have simp_rw₁ : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ (s : Set α), s.Countable ∧ Dense s
Tactic: simp_rw [IsSeparable, separableSpace_iff, dense_iff_closure_eq, ← univ_subset_iff,
    ← hs.closure_eq, isClosed_closure.closure_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
simp_rw : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ SeparableSpace α
simp_rw₁ : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ (s : Set α), s.Countable ∧ Dense s
⊢ IsSeparable s ↔ SeparableSpace α
have simp_rw₂ : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ (s : Set α), s.Countable ∧ closure[t] s = univ
Tactic: simp_rw [IsSeparable, separableSpace_iff, dense_iff_closure_eq, ← univ_subset_iff,
    ← hs.closure_eq, isClosed_closure.closure_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
simp_rw : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ SeparableSpace α
simp_rw₁ : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ (s : Set α), s.Countable ∧ Dense s
simp_rw₂ : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ (s : Set α), s.Countable ∧ closure[t] s = univ
⊢ IsSeparable s ↔ SeparableSpace α
have simp_rw₃ : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ (s : Set α), s.Countable ∧ univ ⊆ closure[t] s
Tactic: simp_rw [IsSeparable, separableSpace_iff, dense_iff_closure_eq, ← univ_subset_iff,
    ← hs.closure_eq, isClosed_closure.closure_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
simp_rw : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ SeparableSpace α
simp_rw₁ : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ (s : Set α), s.Countable ∧ Dense s
simp_rw₂ : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ (s : Set α), s.Countable ∧ closure[t] s = univ
simp_rw₃ : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ (s : Set α), s.Countable ∧ univ ⊆ closure[t] s
⊢ IsSeparable s ↔ SeparableSpace α
have simp_rw₄ : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ (s_1 : Set α), s_1.Countable ∧ closure[t] s ⊆ closure[t] s_1
Tactic: simp_rw [IsSeparable, separableSpace_iff, dense_iff_closure_eq, ← univ_subset_iff,
    ← hs.closure_eq, isClosed_closure.closure_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
⊢ IsTopologicalBasis.{u_1} (α := β)
    {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}
have refine_1 : ∀ (u : Set β),
  Membership.mem (γ := Set (Set β))
      {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i} u →
    IsOpen[⨅ (i : ι), t i] u
Tactic: refine isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
refine_1 :
  ∀ (u : Set β),
    Membership.mem (γ := Set (Set β))
        {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i} u →
      IsOpen[⨅ (i : ι), t i] u
⊢ IsTopologicalBasis.{u_1} (α := β)
    {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}
have refine_2 : ∀ (a : β) (u : Set β),
  a ∈ u →
    IsOpen[⨅ (i : ι), t i] u →
      ∃ (v : Set β),
        Membership.mem (γ := Set (Set β))
            {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i} v ∧
          a ∈ v ∧ v ⊆ u
Tactic: refine isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
⊢ ∃ (v : Set β),
    Membership.mem (γ := Set (Set β))
        {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i} v ∧
      a ∈ v ∧ v ⊆ u
have refine_2 : ∀ (F : Set ι) (U : (i : ι) → Set β) (hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u) (hF : (F, U).1.Finite)
  (hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i),
  ∃ (v : Set β),
    Membership.mem (γ := Set (Set β))
        {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i} v ∧
      a ∈ v ∧ v ⊆ u
Tactic: rcases (nhds_iInf (t := t) (a := a)).symm ▸ HasBasis.iInf'
      (fun i ↦ (h_basis i).nhds_hasBasis (t := t i)) |>.mem_iff.1 (hu.mem_nhds ha)
      with ⟨⟨F, U⟩, ⟨hF, hU⟩, hUu⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∃ (v : Set β),
    Membership.mem (γ := Set (Set β))
        {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i} v ∧
      a ∈ v ∧ v ⊆ u
have refine_2 : ∀ i ∈ hF.toFinset (s := (F, U).1), U i ∈ T i
Tactic: refine ⟨_, ⟨U, hF.toFinset, ?_, rfl⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
refine_2 : ∀ i ∈ hF.toFinset (s := (F, U).1), U i ∈ T i
⊢ ∃ (v : Set β),
    Membership.mem (γ := Set (Set β))
        {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i} v ∧
      a ∈ v ∧ v ⊆ u
have refine_2₁ : Membership.mem (γ := Set β) (⋂ i ∈ hF.toFinset (s := (F, U).1), U i) a
Tactic: refine ⟨_, ⟨U, hF.toFinset, ?_, rfl⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
refine_2 : ∀ i ∈ hF.toFinset (s := (F, U).1), U i ∈ T i
refine_2₁ : Membership.mem (γ := Set β) (⋂ i ∈ hF.toFinset (s := (F, U).1), U i) a
⊢ ∃ (v : Set β),
    Membership.mem (γ := Set (Set β))
        {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i} v ∧
      a ∈ v ∧ v ⊆ u
have refine_2₂ : ⋂ i ∈ hF.toFinset (s := (F, U).1), U i ⊆ u
Tactic: refine ⟨_, ⟨U, hF.toFinset, ?_, rfl⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∀ i ∈ hF.toFinset (s := (F, U).1), U i ∈ T i
have refine_2 : ∀ i ∈ F, U i ∈ T i
Tactic: simp only [Finite.mem_toFinset, mem_iInter]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ Membership.mem (γ := Set β) (⋂ i ∈ hF.toFinset (s := (F, U).1), U i) a
have refine_2 : ∀ (i : ι) (i_1 : i ∈ F), a ∈ U i
Tactic: simp only [Finite.mem_toFinset, mem_iInter]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ⋂ i ∈ hF.toFinset (s := (F, U).1), U i ⊆ u
have refine_2 : ⋂ i ∈ F, U i ⊆ u
Tactic: simp only [Finite.mem_toFinset, mem_iInter]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
⊢ IsTopologicalBasis.{u_1} (α := β)
    {S : Set β | ∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i}
have h : ∀ (S : Set β),
  (∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) ↔
    ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i
Tactic: convert! IsTopologicalBasis.iInf (fun i ↦ (cond i).induced (f i)) with S
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
⊢ (∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) ↔
    ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i
have h : (∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) →
  ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
h :
  (∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) →
    ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i
⊢ (∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) ↔
    ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i
have h₁ : (∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i) →
  ∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
U : ι → Set β
F : Finset ι
hUT : ∀ i ∈ F, U i ∈ preimage (f i) '' T i
hSU : S = ⋂ i ∈ F, U i
⊢ ∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i
have h : ∀ (U' : (i : ι) → Set (X i)) (hU' : ∀ i ∈ F, U' i ∈ T i) (hUU' : ∀ i ∈ F, f i ⁻¹' U' i = U i),
  ∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i
Tactic: choose! U' hU' hUU' using hUT
Cleared hypotheses: hUT
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
⊢ IsOpenMap (X := (x : ι) → X x) (eval (β := X) i)
have refine : ∀ (s : Set ((i : ι) → X i)),
  Membership.mem (γ := Set (Set ((i : ι) → X i)))
      {S : Set ((i : ι) → X i) |
        ∃ (U : (i : ι) → Set (X i)) (F : Finset ι),
          (∀ i ∈ F, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)) ∧
            S = (↑F : Set ι).pi (α := X) U}
      s →
    IsOpen[inst i] (eval (β := X) i '' s)
Tactic: refine (isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)
⊢ IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
have inl : ∀ (h : (↑s : Set ι).pi (α := X) U = ∅), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
Tactic: obtain h | h := ((s : Set ι).pi U).eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)
inl : ∀ (h : (↑s : Set ι).pi (α := X) U = ∅), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
⊢ IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
have inr : ∀ (h : ((↑s : Set ι).pi (α := X) U).Nonempty), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
Tactic: obtain h | h := ((s : Set ι).pi U).eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)
h : ((↑s : Set ι).pi (α := X) U).Nonempty
⊢ IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
have pos : ∀ (hi : i ∈ s), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)
h : ((↑s : Set ι).pi (α := X) U).Nonempty
pos : ∀ (hi : i ∈ s), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
⊢ IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
have neg : ∀ (hi : i ∉ s), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)
h : ((↑s : Set ι).pi (α := X) U).Nonempty
hi : i ∈ s
⊢ IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
have pos : IsOpen[inst i] (U i)
Tactic: rw [eval_image_pi (mod_cast hi) h]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)
h : ((↑s : Set ι).pi (α := X) U).Nonempty
hi : i ∉ s
⊢ IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
have neg : IsOpen[inst i] univ
Tactic: rw [eval_image_pi_of_notMem (mod_cast hi), if_pos h]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
⊢ IsOpenMap (X := (x : ι) → X x) (eval (β := X) i)
have refine : ∀ (s : Set ((i : ι) → X i)),
  Membership.mem (γ := Set (Set ((i : ι) → X i)))
      {S : Set ((i : ι) → X i) |
        ∃ (U : (i : ι) → Set (X i)) (F : Finset ι),
          (∀ i ∈ F, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)) ∧
            S = (↑F : Set ι).pi (α := X) U}
      s →
    IsOpen[inst i] (eval (β := X) i '' s)
Tactic: classical
  refine (isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_
  rintro _ ⟨U, s, hU, rfl⟩
  obtain h | h := ((s : Set ι).pi U).eq_empty_or_nonempty
  · simp [h]
  by_cases hi : i ∈ s
  · rw [eval_image_pi (mod_cast hi) h]
    exact hU _ hi
  · rw [eval_image_pi_of_notMem (mod_cast hi), if_pos h]
    exact isOpen_univ
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
refine :
  ∀ (s : Set ((i : ι) → X i)),
    Membership.mem (γ := Set (Set ((i : ι) → X i)))
        {S : Set ((i : ι) → X i) |
          ∃ (U : (i : ι) → Set (X i)) (F : Finset ι),
            (∀ i ∈ F, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)) ∧
              S = (↑F : Set ι).pi (α := X) U}
        s →
      IsOpen[inst i] (eval (β := X) i '' s)
⊢ IsOpenMap (X := (x : ι) → X x) (eval (β := X) i)
have refine₁ : ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
  (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)),
  IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
Tactic: classical
  refine (isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_
  rintro _ ⟨U, s, hU, rfl⟩
  obtain h | h := ((s : Set ι).pi U).eq_empty_or_nonempty
  · simp [h]
  by_cases hi : i ∈ s
  · rw [eval_image_pi (mod_cast hi) h]
    exact hU _ hi
  · rw [eval_image_pi_of_notMem (mod_cast hi), if_pos h]
    exact isOpen_univ
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
refine :
  ∀ (s : Set ((i : ι) → X i)),
    Membership.mem (γ := Set (Set ((i : ι) → X i)))
        {S : Set ((i : ι) → X i) |
          ∃ (U : (i : ι) → Set (X i)) (F : Finset ι),
            (∀ i ∈ F, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)) ∧
              S = (↑F : Set ι).pi (α := X) U}
        s →
      IsOpen[inst i] (eval (β := X) i '' s)
refine₁ :
  ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
    (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)),
    IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
⊢ IsOpenMap (X := (x : ι) → X x) (eval (β := X) i)
have inl : ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
  (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i))
  (h : (↑s : Set ι).pi (α := X) U = ∅), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
Tactic: classical
  refine (isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_
  rintro _ ⟨U, s, hU, rfl⟩
  obtain h | h := ((s : Set ι).pi U).eq_empty_or_nonempty
  · simp [h]
  by_cases hi : i ∈ s
  · rw [eval_image_pi (mod_cast hi) h]
    exact hU _ hi
  · rw [eval_image_pi_of_notMem (mod_cast hi), if_pos h]
    exact isOpen_univ
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
refine :
  ∀ (s : Set ((i : ι) → X i)),
    Membership.mem (γ := Set (Set ((i : ι) → X i)))
        {S : Set ((i : ι) → X i) |
          ∃ (U : (i : ι) → Set (X i)) (F : Finset ι),
            (∀ i ∈ F, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)) ∧
              S = (↑F : Set ι).pi (α := X) U}
        s →
      IsOpen[inst i] (eval (β := X) i '' s)
refine₁ :
  ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
    (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)),
    IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
inl :
  ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
    (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i))
    (h : (↑s : Set ι).pi (α := X) U = ∅), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
⊢ IsOpenMap (X := (x : ι) → X x) (eval (β := X) i)
have inr : ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
  (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i))
  (h : ((↑s : Set ι).pi (α := X) U).Nonempty), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
Tactic: classical
  refine (isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_
  rintro _ ⟨U, s, hU, rfl⟩
  obtain h | h := ((s : Set ι).pi U).eq_empty_or_nonempty
  · simp [h]
  by_cases hi : i ∈ s
  · rw [eval_image_pi (mod_cast hi) h]
    exact hU _ hi
  · rw [eval_image_pi_of_notMem (mod_cast hi), if_pos h]
    exact isOpen_univ