awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
⊢ IsPreirreducible s
have pos : ∀ (huniv : s ⊆ u), IsPreirreducible s
Tactic: by_cases huniv : s ⊆ u
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
pos : ∀ (huniv : s ⊆ u), IsPreirreducible s
⊢ IsPreirreducible s
have neg : ∀ (huniv : ¬s ⊆ u), IsPreirreducible s
Tactic: by_cases huniv : s ⊆ u
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (hypothesis)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
⊢ IsPreirreducible s
have huo : IsOpen[inst] uᶜ
Tactic: have huo : IsOpen uᶜ :=
        IsClosed.isOpen_compl (self := isClosed_of_mem_irreducibleComponents u hu)
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst] uᶜ
⊢ IsPreirreducible s
have neg : ∀ (a : X) (ha₁ : a ∈ s) (ha₂ : a ∉ u), IsPreirreducible s
Tactic: rcases not_subset.mp huniv with ⟨a, ⟨ha₁, ha₂⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
⊢ IsPreirreducible s
have neg : ∀ (j : ι) (haj : a ∈ (↑(U j) : Set X)), IsPreirreducible s
Tactic: choose j haj using mem_iUnion.mp <| hsU ha₁
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (hypothesis)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
j : ι
haj : a ∈ (↑(U j) : Set X)
⊢ IsPreirreducible s
have hji : j ≠ i
Tactic: have hji : j ≠ i := fun hji' ↦ ha₂ <| hUu <| hji' ▸ haj
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
j : ι
haj : a ∈ (↑(U j) : Set X)
hji : j ≠ i
⊢ IsPreirreducible s
have neg : ∀ (x : X) (hx₁ : x ∈ (↑(U i) : Set X)) (hx₂ : x ∈ uᶜ), IsPreirreducible s
Tactic: rcases inter_nonempty_iff_exists_left.mp
        ((h j) (U i) uᶜ (U i).isOpen huo
        (not_disjoint_iff_nonempty_inter.mp (by simpa using hn hji)) ⟨a, ⟨haj, ha₂⟩⟩).right
        with ⟨x, hx₁, hx₂⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x_1 : X
hx : x_1 ∈ s
i : ι
hi : x_1 ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
j : ι
haj : a ∈ (↑(U j) : Set X)
hji : j ≠ i
x : X
hx₁ : x ∈ (↑(U i) : Set X)
hx₂ : x ∈ uᶜ
⊢ IsPreirreducible s
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
Us : Set (Opens α)
x : α
⊢ x ∈ sSup Us ↔ ∃ u ∈ Us, x ∈ u
have simp_rw : Membership.mem (γ := Opens α) (⨆ a ∈ Us, a) x ↔ ∃ u ∈ Us, x ∈ u
Tactic: simp_rw [sSup_eq_iSup, mem_iSup, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
Us : Set (Opens α)
x : α
simp_rw : Membership.mem (γ := Opens α) (⨆ a ∈ Us, a) x ↔ ∃ u ∈ Us, x ∈ u
⊢ x ∈ sSup Us ↔ ∃ u ∈ Us, x ∈ u
have simp_rw₁ : (∃ (i : Opens α) (_ : i ∈ Us), x ∈ i) ↔ ∃ u ∈ Us, x ∈ u
Tactic: simp_rw [sSup_eq_iSup, mem_iSup, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
U V : Opens α
i : U ≤ V
⊢ IsOpen[instTopologicalSpaceSubtype] (range (Set.inclusion (s := (↑U : Set α)) (t := (↑V : Set α)) ⋯))
have rw : IsOpen[instTopologicalSpaceSubtype] {x : (↑(↑V : Set α) : Type u_2) | (↑x : α) ∈ (↑U : Set α)}
Tactic: rw [Set.range_inclusion i]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
⊢ ¬(↑U : Set α).Nonempty ↔ U = ⊥
have rw : ¬(↑U : Set α).Nonempty ↔ (↑U : Set α) = (↑⊥ : Set α)
Tactic: rw [← coe_inj, coe_bot, ← Set.not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
rw : ¬(↑U : Set α).Nonempty ↔ (↑U : Set α) = (↑⊥ : Set α)
⊢ ¬(↑U : Set α).Nonempty ↔ U = ⊥
have rw₁ : ¬(↑U : Set α).Nonempty ↔ (↑U : Set α) = ∅
Tactic: rw [← coe_inj, coe_bot, ← Set.not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
rw : ¬(↑U : Set α).Nonempty ↔ (↑U : Set α) = (↑⊥ : Set α)
rw₁ : ¬(↑U : Set α).Nonempty ↔ (↑U : Set α) = ∅
⊢ ¬(↑U : Set α).Nonempty ↔ U = ⊥
have rw₂ : ¬(↑U : Set α).Nonempty ↔ ¬(↑U : Set α).Nonempty
Tactic: rw [← coe_inj, coe_bot, ← Set.not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
⊢ U ≠ ⊥ ↔ (↑U : Set α).Nonempty
have rw : ¬U = ⊥ ↔ (↑U : Set α).Nonempty
Tactic: rw [Ne, ← not_nonempty_iff_eq_bot, not_not]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
rw : ¬U = ⊥ ↔ (↑U : Set α).Nonempty
⊢ U ≠ ⊥ ↔ (↑U : Set α).Nonempty
have rw₁ : ¬¬(↑U : Set α).Nonempty ↔ (↑U : Set α).Nonempty
Tactic: rw [Ne, ← not_nonempty_iff_eq_bot, not_not]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
rw : ¬U = ⊥ ↔ (↑U : Set α).Nonempty
rw₁ : ¬¬(↑U : Set α).Nonempty ↔ (↑U : Set α).Nonempty
⊢ U ≠ ⊥ ↔ (↑U : Set α).Nonempty
have rw₂ : (↑U : Set α).Nonempty ↔ (↑U : Set α).Nonempty
Tactic: rw [Ne, ← not_nonempty_iff_eq_bot, not_not]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : IndiscreteTopology α
U : Opens α
⊢ U = ⊥ ∨ U = ⊤
have rw : IsOpen[inst] (↑U : Set α)
Tactic: rw [← coe_eq_empty, ← coe_eq_univ, ← IndiscreteTopology.isOpen_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
⊢ IsBasis B ↔ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
have mp : IsBasis B → ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
mp : IsBasis B → ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
⊢ IsBasis B ↔ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
have mpr : (∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U) → IsBasis B
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU : Opens α }
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }
have mp : ∀ (sV : Set α) (hsV : x ∈ sV ∧ sV ⊆ sU) (V : Opens α) (H₁ : V ∈ B) (H₂ : (↑V : Set α) = sV),
  ∃ U' ∈ B, x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }
Tactic: rcases h.mem_nhds_iff.mp (IsOpen.mem_nhds hU hx) with ⟨sV, ⟨⟨V, H₁, H₂⟩, hsV⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU : Opens α }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
V : Opens α
H₁ : V ∈ B
H₂ : (↑V : Set α) = sV
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }
have mp : x ∈ V ∧ V ≤ { carrier := sU, is_open' := hU }
Tactic: refine ⟨V, H₁, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU : Opens α }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
V : Opens α
H₁ : V ∈ B
H₂ : (↑V : Set α) = sV
⊢ x ∈ V ∧ V ≤ { carrier := sU, is_open' := hU }
have mp : ∀ (carrier : Set α) (is_open' : IsOpen[inst] carrier) (H₁ : { carrier := carrier, is_open' := is_open' : Opens α } ∈ B)
  (H₂ : (↑{ carrier := carrier, is_open' := is_open' : Opens α } : Set α) = sV),
  x ∈ { carrier := carrier, is_open' := is_open' : Opens α } ∧
    { carrier := carrier, is_open' := is_open' : Opens α } ≤ { carrier := sU, is_open' := hU }
Tactic: cases V
Cleared hypotheses: V, H₁, H₂
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (hypothesis)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU : Opens α }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
carrier : Set α
is_open' : IsOpen[inst] carrier
H₁ : { carrier := carrier, is_open' := is_open' : Opens α } ∈ B
H₂ : carrier = sV
⊢ x ∈ { carrier := carrier, is_open' := is_open' : Opens α } ∧
    { carrier := carrier, is_open' := is_open' : Opens α } ≤ { carrier := sU, is_open' := hU }
have hsV₁ : x ∈ carrier ∧ carrier ⊆ sU
Tactic: subst H₂
Cleared hypotheses: sV, hsV, H₂
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
⊢ IsBasis B
have mpr : ∀ u ∈ SetLike.coe '' B, IsOpen[inst] u
Tactic: refine isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
mpr : ∀ u ∈ SetLike.coe '' B, IsOpen[inst] u
⊢ IsBasis B
have mpr₁ : ∀ (a : α) (u : Set α), a ∈ u → IsOpen[inst] u → ∃ v ∈ SetLike.coe '' B, a ∈ v ∧ v ⊆ u
Tactic: refine isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen[inst] sU
⊢ ∃ v ∈ SetLike.coe '' B, x ∈ v ∧ v ⊆ sU
have mpr : ∀ (V : Opens α) (hV : V ∈ B) (H : x ∈ V ∧ V ≤ { carrier := sU, is_open' := hsU }),
  ∃ v ∈ SetLike.coe '' B, x ∈ v ∧ v ⊆ sU
Tactic: rcases @h ⟨sU, hsU⟩ x hx with ⟨V, hV, H⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
⊢ IsBasis B ↔ ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
have mp : IsBasis B → ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
mp : IsBasis B → ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
⊢ IsBasis B ↔ ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
have mpr : (∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us) → IsBasis B
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ∃ Us ⊆ B, U = sSup Us
have mp : (↑U : Set α) = (↑(sSup {V : Opens α | V ∈ B ∧ V ≤ U}) : Set α)
Tactic: refine ⟨{ V : Opens α | V ∈ B ∧ V ≤ U }, fun U hU => hU.left, ext ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ (↑U : Set α) = (↑(sSup {V : Opens α | V ∈ B ∧ V ≤ U}) : Set α)
have mp : Eq.{u_2 + 1} (α := Set α) (⋃₀ {s : Set α | s ∈ SetLike.coe '' B ∧ s ⊆ (↑U : Set α)})
  (⋃ (i : Opens α), ⋃ (_ : Membership.mem (γ := Set (Opens α)) {V : Opens α | V ∈ B ∧ V ≤ U} i), (↑i : Set α))
Tactic: rw [coe_sSup, hB.open_eq_sUnion' U.isOpen]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ Eq.{u_2 + 1} (α := Set α) (⋃₀ {s : Set α | s ∈ SetLike.coe '' B ∧ s ⊆ (↑U : Set α)})
    (⋃ (i : Opens α), ⋃ (_ : Membership.mem (γ := Set (Opens α)) {V : Opens α | V ∈ B ∧ V ≤ U} i), (↑i : Set α))
have mp : Eq.{u_2 + 1} (α := Set α) (⨆ b ∈ B, ⨆ (_ : (↑b : Set α) ⊆ (↑U : Set α)), (↑b : Set α))
  (⨆ i ∈ B, ⨆ (_ : i ≤ U), (↑i : Set α))
Tactic: simp_rw [sUnion_eq_biUnion, iUnion, mem_setOf_eq, iSup_and, iSup_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
⊢ IsBasis B
have mpr : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
Tactic: rw [isBasis_iff_nbhd]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
U : Opens α
x : α
hx : x ∈ U
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
have mpr : ∀ (Us : Set (Opens α)) (hUs : Us ⊆ B) (hx : x ∈ sSup Us), ∃ U' ∈ B, x ∈ U' ∧ U' ≤ sSup Us
Tactic: rcases h U with ⟨Us, hUs, rfl⟩
Cleared hypotheses: U, hx
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
x : α
Us : Set (Opens α)
hUs : Us ⊆ B
hx : x ∈ sSup Us
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ sSup Us
have mpr : ∀ (U : Opens α) (Us_1 : U ∈ Us) (xU : x ∈ U), ∃ U' ∈ B, x ∈ U' ∧ U' ≤ sSup Us
Tactic: rcases mem_sSup.1 hx with ⟨U, Us, xU⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact (↑(b i) : Set α)
U : Set α
⊢ IsCompact U ∧ IsOpen[inst] U ↔ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, (↑(b i) : Set α)
have hb₁ : IsTopologicalBasis.{u_2} (α := α) (range fun (i : ι) ↦ (b i).carrier)
Tactic: apply isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis fun i : ι => (b i).1
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact (↑(b i) : Set α)
U : Set α
hb₁ : IsTopologicalBasis.{u_2} (α := α) (range fun (i : ι) ↦ (b i).carrier)
⊢ IsCompact U ∧ IsOpen[inst] U ↔ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, (↑(b i) : Set α)
have hb'₁ : ∀ (i : ι), IsCompact (b i).carrier
Tactic: apply isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis fun i : ι => (b i).1
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact (↑(b i) : Set α)
U : Set α
⊢ IsTopologicalBasis.{u_2} (α := α) (range fun (i : ι) ↦ (b i).carrier)
have h : (range fun (i : ι) ↦ (b i).carrier) = SetLike.coe '' range b
Tactic: convert! (config := { transparency := .default }) hb
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact (↑(b i) : Set α)
U : Set α
⊢ (range fun (i : ι) ↦ (b i).carrier) = SetLike.coe '' range b
have h : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) (range fun (i : ι) ↦ (b i).carrier) x ↔ x ∈ SetLike.coe '' range b
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
⊢ ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
have obtain : ∀ (Us' : Set (Opens α)) (hsub : Us' ⊆ B) (hsup : U = sSup Us'), ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
Tactic: obtain ⟨Us', hsub, hsup⟩ := isBasis_iff_cover.mp hB U
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
⊢ ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
have obtain : ∀ (t : Finset (↑Us' : Type u_2)) (ht : U.carrier ⊆ ⋃ i ∈ t, (↑(↑i : Opens α) : Set α)),
  ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
Tactic: obtain ⟨t, ht⟩ := hU.elim_finite_subcover (fun s : Us' ↦ s.1) (fun s ↦ s.1.2) (by simp [hsup])
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
t : Finset (↑Us' : Type u_2)
ht : U.carrier ⊆ ⋃ i ∈ t, (↑(↑i : Opens α) : Set α)
⊢ ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
have refine : U = sSup (↑(Finset.image (Subtype.val (p := fun (x : Opens α) ↦ x ∈ Us')) t) : Set (Opens α))
Tactic: refine ⟨Finset.image Subtype.val t, subset_trans (by simp) hsub, Finset.finite_toSet _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
⊢ ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
have obtain : ∀ (Us' : Set (Opens α)) (hsub : Us' ⊆ B) (hsup : U = sSup Us'), ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
Tactic: classical
  obtain ⟨Us', hsub, hsup⟩ := isBasis_iff_cover.mp hB U
  obtain ⟨t, ht⟩ := hU.elim_finite_subcover (fun s : Us' ↦ s.1) (fun s ↦ s.1.2) (by simp [hsup])
  refine ⟨Finset.image Subtype.val t, subset_trans (by simp) hsub, Finset.finite_toSet _, ?_⟩
  exact le_antisymm (subset_trans ht (by simp)) (le_trans (sSup_le_sSup (by simp)) hsup.ge)
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
obtain : ∀ (Us' : Set (Opens α)) (hsub : Us' ⊆ B) (hsup : U = sSup Us'), ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
⊢ ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
have obtain₁ : ∀ (Us' : Set (Opens α)) (hsub : Us' ⊆ B) (hsup : U = sSup Us') (t : Finset (↑Us' : Type u_2))
  (ht : U.carrier ⊆ ⋃ i ∈ t, (↑(↑i : Opens α) : Set α)), ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
Tactic: classical
  obtain ⟨Us', hsub, hsup⟩ := isBasis_iff_cover.mp hB U
  obtain ⟨t, ht⟩ := hU.elim_finite_subcover (fun s : Us' ↦ s.1) (fun s ↦ s.1.2) (by simp [hsup])
  refine ⟨Finset.image Subtype.val t, subset_trans (by simp) hsub, Finset.finite_toSet _, ?_⟩
  exact le_antisymm (subset_trans ht (by simp)) (le_trans (sSup_le_sSup (by simp)) hsup.ge)
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
obtain : ∀ (Us' : Set (Opens α)) (hsub : Us' ⊆ B) (hsup : U = sSup Us'), ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
obtain₁ :
  ∀ (Us' : Set (Opens α)) (hsub : Us' ⊆ B) (hsup : U = sSup Us') (t : Finset (↑Us' : Type u_2))
    (ht : U.carrier ⊆ ⋃ i ∈ t, (↑(↑i : Opens α) : Set α)), ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
⊢ ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
have obtain₂ : ∀ (Us' : Set (Opens α)) (hsub : Us' ⊆ B) (hsup : U = sSup Us') (t : Finset (↑Us' : Type u_2))
  (ht : U.carrier ⊆ ⋃ i ∈ t, (↑(↑i : Opens α) : Set α)),
  U = sSup (↑(Finset.image (Subtype.val (p := fun (x : Opens α) ↦ x ∈ Us')) t) : Set (Opens α))
Tactic: classical
  obtain ⟨Us', hsub, hsup⟩ := isBasis_iff_cover.mp hB U
  obtain ⟨t, ht⟩ := hU.elim_finite_subcover (fun s : Us' ↦ s.1) (fun s ↦ s.1.2) (by simp [hsup])
  refine ⟨Finset.image Subtype.val t, subset_trans (by simp) hsub, Finset.finite_toSet _, ?_⟩
  exact le_antisymm (subset_trans ht (by simp)) (le_trans (sSup_le_sSup (by simp)) hsup.ge)
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_5
t₁ t₂ : TopologicalSpace α
Us : Set (Opens α)
hUs : IsBasis Us
| t₁ ≤ t₂
have rw : t₁ ≤ generateFrom (SetLike.coe '' Us)
Tactic: rw [hUs.eq_generateFrom]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_5
t₁ t₂ : TopologicalSpace α
Us : Set (Opens α)
hUs : IsBasis Us
⊢ t₁ ≤ t₂ ↔ ∀ U ∈ Us, IsOpen[t₁] (↑U : Set α)
have conv_lhs : t₁ ≤ generateFrom (SetLike.coe '' Us) ↔ ∀ U ∈ Us, IsOpen[t₁] (↑U : Set α)
Tactic: conv_lhs => rw [hUs.eq_generateFrom]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → TopologicalSpace (α i)
B : (i : ι) → Set (Opens (α i))
hB : ∀ (i : ι), IsBasis (B i)
⊢ IsBasis (α := Sigma α)
    (⋃ (i : ι), (fun (U : Opens (α i)) ↦ { carrier := Sigma.mk (β := α) i '' U.carrier, is_open' := ⋯ }) '' B i)
have a : IsBasis (α := Sigma α)
    (⋃ (i : ι), (fun (U : Opens (α i)) ↦ { carrier := Sigma.mk (β := α) i '' U.carrier, is_open' := sorry }) '' B i) ↔
  IsTopologicalBasis (α := (i : ι) × α i)
    (⋃ (i : ι), (fun (u : Set (α i)) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i '' u) '' SetLike.coe '' B i)
Tactic: convert! TopologicalSpace.IsTopologicalBasis.sigma hB
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → TopologicalSpace (α i)
B : (i : ι) → Set (Opens (α i))
hB : ∀ (i : ι), IsBasis (B i)
⊢ IsBasis (α := Sigma α)
      (⋃ (i : ι), (fun (U : Opens (α i)) ↦ { carrier := Sigma.mk (β := α) i '' U.carrier, is_open' := ⋯ }) '' B i) ↔
    IsTopologicalBasis (α := (i : ι) × α i)
      (⋃ (i : ι), (fun (u : Set (α i)) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i '' u) '' SetLike.coe '' B i)
have a : IsTopologicalBasis (α := Sigma α)
    (⋃ (i : ι),
      (comp (β := Opens (Sigma α)) SetLike.coe fun (U : Opens (α i)) ↦
          { carrier := Sigma.mk (β := α) i '' U.carrier, is_open' := sorry }) ''
        B i) ↔
  IsTopologicalBasis (α := (i : ι) × α i)
    (⋃ (i : ι), (fun (u : Set (α i)) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i '' u) ∘ SetLike.coe '' B i)
Tactic: simp only [IsBasis, Set.image_iUnion, ← Set.image_comp]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
B : Set (Opens β)
H : IsTopologicalBasis (SetLike.coe '' B)
f : α → β
h : IsInducing f
⊢ IsTopologicalBasis
    (image (α := Opens α) SetLike.coe
      {x : Opens α | ∃ U ∈ B, { carrier := f ⁻¹' (↑U : Set β), is_open' := ⋯ : Opens α } = x})
have h₁ : image (α := Opens α) SetLike.coe
    {x : Opens α | ∃ U ∈ B, { carrier := f ⁻¹' (↑U : Set β), is_open' := sorry : Opens α } = x} =
  preimage f '' SetLike.coe '' B
Tactic: convert! H.isInducing h