awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Spectral.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : SpectralMap β γ
f₁ f₂ : SpectralMap α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Spectral.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : SpectralMap β γ
f₁ f₂ : SpectralMap α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Spectral.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : SpectralMap β γ
f₁ f₂ : SpectralMap α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
U : ι → Opens X
hU : IsOpenCover U
inst_1 : ∀ (i : ι), PrespectralSpace.{u_1} ↥(U i)
⊢ PrespectralSpace X
have refine : ∀ (U_1 : Set X),
  Membership.mem (γ := Set (Set X))
      (⋃ (i : ι),
        (fun (x : Set ↥(U i)) ↦ Subtype.val (p := fun (x : X) ↦ x ∈ U i) '' x) ''
          {U_2 : Set ↥(U i) | IsOpen[instTopologicalSpaceSubtype] U_2 ∧ IsCompact U_2})
      U_1 →
    IsCompact U_1
Tactic: refine .of_isTopologicalBasis (hU.isTopologicalBasis fun i ↦ isTopologicalBasis) ?_
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
U : ι → Opens X
hU : IsOpenCover U
inst_1 : ∀ (i : ι), PrespectralSpace.{u_1} ↥(U i)
⊢ ∀ (U_1 : Set X),
    Membership.mem (γ := Set (Set X))
        (⋃ (i : ι),
          (fun (x : Set ↥(U i)) ↦ Subtype.val (p := fun (x : X) ↦ x ∈ U i) '' x) ''
            {U_2 : Set ↥(U i) | IsOpen[instTopologicalSpaceSubtype] U_2 ∧ IsCompact U_2})
        U_1 →
      IsCompact U_1
have simp : ∀ (b : ι) (b_1 : Set ↥(U b)) (a : IsOpen[instTopologicalSpaceSubtype] b_1),
  IsCompact b_1 → IsCompact (Subtype.val (p := fun (x : X) ↦ x ∈ U b) '' b_1)
Tactic: simp only [Set.mem_iUnion, Set.mem_image, Set.mem_setOf_eq, forall_exists_index, and_imp,
    forall_comm (α := Set _), forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace Y
f : X → Y
hf : IsInducing f
hf' : IsSpectralMap f
⊢ ∀ U ∈ Set.preimage f '' {U : Set Y | IsOpen[inst_1] U ∧ IsCompact U}, IsCompact U
have simp : ∀ (U : Set X) (x : Set Y), IsOpen[inst_1] x → IsCompact x → f ⁻¹' x = U → IsCompact U
Tactic: simp only [Set.mem_image, Set.mem_setOf_eq, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace Y
f : X → Y
hf : IsOpenEmbedding f
⊢ IsTopologicalBasis.{u_1} (α := X) {U : Set X | IsOpen[inst] U ∧ IsCompact U}
have apply : ∀ (x : X) (U : Set X) (hx : x ∈ U) (hU : IsOpen[inst] U),
  ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} v ∧ x ∈ v ∧ v ⊆ U
Tactic: apply isTopologicalBasis_of_isOpen_of_nhds (fun U hU ↦ hU.1) <| fun x U hx hU ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace Y
f : X → Y
hf : IsOpenEmbedding f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} v ∧ x ∈ v ∧ v ⊆ U
have obtain : ∀ (V : Set Y) (hoV : IsOpen[inst_1] V) (hcV : IsCompact V) (hfx : f x ∈ V) (hVf : V ⊆ f '' U),
  ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} v ∧ x ∈ v ∧ v ⊆ U
Tactic: obtain ⟨V, ⟨hoV, hcV⟩, hfx, hVf⟩ : ∃ V ∈ {V | IsOpen V ∧ IsCompact V}, f x ∈ V ∧ V ⊆ f '' U :=
      (PrespectralSpace.isTopologicalBasis (X := Y)).isOpen_iff.mp
        (hf.isOpen_iff_image_isOpen.mp hU) (f x) ⟨x, hx, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace Y
f : X → Y
hf : IsOpenEmbedding f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
V : Set Y
hoV : IsOpen[inst_1] V
hcV : IsCompact V
hfx : f x ∈ V
hVf : V ⊆ f '' U
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} v ∧ x ∈ v ∧ v ⊆ U
have refine_1 : IsCompact (f ⁻¹' V)
Tactic: refine ⟨f ⁻¹' V, ⟨hoV.preimage hf.continuous, ?_⟩, ⟨hfx, fun y hy ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace Y
f : X → Y
hf : IsOpenEmbedding f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
V : Set Y
hoV : IsOpen[inst_1] V
hcV : IsCompact V
hfx : f x ∈ V
hVf : V ⊆ f '' U
refine_1 : IsCompact (f ⁻¹' V)
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} v ∧ x ∈ v ∧ v ⊆ U
have refine_2 : ∀ (y : X) (hy : y ∈ f ⁻¹' V), y ∈ U
Tactic: refine ⟨f ⁻¹' V, ⟨hoV.preimage hf.continuous, ?_⟩, ⟨hfx, fun y hy ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (hypothesis)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
ι : Type u_3
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), PrespectralSpace.{u_4} (X i)
U : Set ((i : ι) × X i)
hU :
  Membership.mem (γ := Set (Set ((i : ι) × X i)))
    (⋃ (i : ι),
      (fun (u : Set (X i)) ↦ Sigma.mk (β := fun (i : ι) ↦ X i) i '' u) ''
        {U : Set (X i) | IsOpen[inst_2 i] U ∧ IsCompact U})
    U
⊢ IsCompact U
have hU₁ : ∃ (i : ι),
  Membership.mem (γ := Set (Set ((i : ι) × X i)))
    ((fun (u : Set (X i)) ↦ Sigma.mk (β := fun (i : ι) ↦ X i) i '' u) ''
      {U : Set (X i) | IsOpen[inst_2 i] U ∧ IsCompact U})
    U
Tactic: simp_rw [Set.mem_iUnion] at hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
ι : Type u_3
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), PrespectralSpace.{u_4} (X i)
U : Set ((i : ι) × X i)
hU :
  ∃ (i : ι),
    Membership.mem (γ := Set (Set ((i : ι) × X i)))
      ((fun (u : Set (X i)) ↦ Sigma.mk (β := fun (i : ι) ↦ X i) i '' u) ''
        {U : Set (X i) | IsOpen[inst_2 i] U ∧ IsCompact U})
      U
⊢ IsCompact U
have obtain : ∀ (i : ι) (V : Set (X i))
  (hV : Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst_2 i] U ∧ IsCompact U} V),
  IsCompact (X := (i : ι) × X i) ((fun (u : Set (X i)) ↦ Sigma.mk (β := fun (i : ι) ↦ X i) i '' u) V)
Tactic: obtain ⟨i, V, hV, rfl⟩ := hU
Cleared hypotheses: U, hU
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
⊢ IsTopologicalBasis (Set.image (α := Opens X) SetLike.coe {U : Opens X | IsCompact (↑U : Set X)})
have h : Set.image (α := Opens X) SetLike.coe {U : Opens X | IsCompact (↑U : Set X)} = {U : Set X | IsOpen[inst] U ∧ IsCompact U}
Tactic: convert! isTopologicalBasis (X := X)
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
⊢ Set.image (α := Opens X) SetLike.coe {U : Opens X | IsCompact (↑U : Set X)} =
    {U : Set X | IsOpen[inst] U ∧ IsCompact U}
have h : ∀ (s : Set X),
  s ∈ Set.image (α := Opens X) SetLike.coe {U : Opens X | IsCompact (↑U : Set X)} ↔
    Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} s
Tactic: ext s
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U : Opens X
⊢ (fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X))
      ((fun (U : Opens X) ↦
          { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ :
            Order.Ideal (CompactOpens X) })
        U) =
    U
have a : (fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X))
    ((fun (U : Opens X) ↦
        { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := sorry, nonempty' := sorry, directed' := sorry :
          Order.Ideal (CompactOpens X) })
      U) ≤
  U
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U : Opens X
a :
  (fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X))
      ((fun (U : Opens X) ↦
          { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ :
            Order.Ideal (CompactOpens X) })
        U) ≤
    U
⊢ (fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X))
      ((fun (U : Opens X) ↦
          { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ :
            Order.Ideal (CompactOpens X) })
        U) =
    U
have a₁ : U ≤
  (fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X))
    ((fun (U : Opens X) ↦
        { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := sorry, nonempty' := sorry, directed' := sorry :
          Order.Ideal (CompactOpens X) })
      U)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U : Opens X
⊢ (fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X))
      ((fun (U : Opens X) ↦
          { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ :
            Order.Ideal (CompactOpens X) })
        U) ≤
    U
have a : ∀ (i : CompactOpens X)
  (i_1 :
    i ∈
      { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := sorry, nonempty' := sorry, directed' := sorry :
        Order.Ideal (CompactOpens X) }),
  i.toOpens ≤ U
Tactic: simp only [iSup_le_iff]
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U : Opens X
x : X
hxU : x ∈ U
⊢ Membership.mem (γ := Opens X)
    ((fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X))
      ((fun (U : Opens X) ↦
          { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ :
            Order.Ideal (CompactOpens X) })
        U))
    x
have a : ∀ (V : Set X) (h₁ : IsOpen[inst] V) (h₂ : IsCompact V) (hxV : x ∈ V) (hVU : V ⊆ (↑U : Set X)),
  Membership.mem (γ := Opens X)
    ((fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X))
      ((fun (U : Opens X) ↦
          { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := sorry, nonempty' := sorry, directed' := sorry :
            Order.Ideal (CompactOpens X) })
        U))
    x
Tactic: obtain ⟨V, ⟨h₁, h₂⟩, hxV, hVU⟩ := isTopologicalBasis.exists_subset_of_mem_open hxU U.2
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U : Opens X
x : X
hxU : x ∈ U
V : Set X
h₁ : IsOpen[inst] V
h₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ (↑U : Set X)
⊢ Membership.mem (γ := Opens X)
    ((fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X))
      ((fun (U : Opens X) ↦
          { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ :
            Order.Ideal (CompactOpens X) })
        U))
    x
have a : ∃ (i : CompactOpens X) (_ :
  i ∈
    { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := sorry, nonempty' := sorry, directed' := sorry :
      Order.Ideal (CompactOpens X) }),
  x ∈ i.toOpens
Tactic: simp only [Opens.mem_iSup]
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
⊢ (fun (U : Opens X) ↦
        { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ :
          Order.Ideal (CompactOpens X) })
      ((fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X)) I) =
    I
have a : ∀ (U : CompactOpens X),
  U ∈
      (↑((fun (U : Opens X) ↦
              { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := sorry, nonempty' := sorry,
                directed' := sorry : Order.Ideal (CompactOpens X) })
            ((fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X)) I)) :
        Set (CompactOpens X)) ↔
    U ∈ (↑I : Set (CompactOpens X))
Tactic: ext U
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
⊢ U ∈
      (↑{ carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑(⨆ U ∈ I, U.toOpens) : Set X)}, lower' := ⋯, nonempty' := ⋯,
            directed' := ⋯ : Order.Ideal (CompactOpens X) } :
        Set (CompactOpens X)) ↔
    U ∈ (↑I : Set (CompactOpens X))
have a : U.toOpens ≤ ⨆ U ∈ I, U.toOpens ↔ U ∈ (↑I : Set (CompactOpens X))
Tactic: change U.toOpens ≤ _ ↔ _
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
⊢ U.toOpens ≤ ⨆ U ∈ I, U.toOpens ↔ U ∈ (↑I : Set (CompactOpens X))
have a : ∀ (H : U.toOpens ≤ ⨆ U ∈ I, U.toOpens), U ∈ (↑I : Set (CompactOpens X))
Tactic: refine ⟨fun H ↦ ?_, fun h ↦ le_iSup₂ (f := fun U (h : U ∈ I) ↦ U.toOpens) U h⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
H : U.toOpens ≤ ⨆ U ∈ I, U.toOpens
⊢ U ∈ (↑I : Set (CompactOpens X))
have H₁ : (↑U.toOpens : Set X) ⊆ ⋃ i ∈ I, (↑i.toOpens : Set X)
Tactic: simp only [← SetLike.coe_subset_coe, Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
H : (↑U.toOpens : Set X) ⊆ ⋃ i ∈ I, (↑i.toOpens : Set X)
⊢ U ∈ (↑I : Set (CompactOpens X))
have a : ∀ (s : Set (CompactOpens X)) (hsI : s ⊆ (↑I : Set (CompactOpens X))) (hs : s.Finite)
  (hU : (↑U : Set X) ⊆ ⋃ i ∈ s, (↑i.toOpens : Set X)), U ∈ (↑I : Set (CompactOpens X))
Tactic: obtain ⟨s, hsI, hs, hU⟩ := U.isCompact.elim_finite_subcover_image (fun U _ ↦ U.2) H
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U V : Opens X
⊢ (∀ (W : CompactOpens X), (↑W : Set X) ⊆ (↑U : Set X) → (↑W : Set X) ⊆ (↑V : Set X)) ↔ U ≤ V
have refine : (∀ (W : CompactOpens X), (↑W : Set X) ⊆ (↑U : Set X) → (↑W : Set X) ⊆ (↑V : Set X)) → U ≤ V
Tactic: refine ⟨?_, fun H W ↦ (le_trans · H)⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U V : Opens X
H : ∀ (W : CompactOpens X), (↑W : Set X) ⊆ (↑U : Set X) → (↑W : Set X) ⊆ (↑V : Set X)
x : X
hxU : x ∈ U
⊢ x ∈ V
have obtain : ∀ (W : Set X) (h₁ : IsOpen[inst] W) (h₂ : IsCompact W) (hxW : x ∈ W) (hWU : W ⊆ (↑U : Set X)), x ∈ V
Tactic: obtain ⟨W, ⟨h₁, h₂⟩, hxW, hWU⟩ := isTopologicalBasis.exists_subset_of_mem_open hxU U.2
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
⊢ ∃ (V : Opens X), IsCompact V.carrier ∧ f '' (↑V : Set X) = U
have obtain : ∀ (Us : Set (Opens X)) (hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)})
  (heq : { carrier := f ⁻¹' U, is_open' := sorry : Opens X } = sSup Us),
  ∃ (V : Opens X), IsCompact V.carrier ∧ f '' (↑V : Set X) = U
Tactic: obtain ⟨Us, hUs, heq⟩ := TopologicalSpace.Opens.isBasis_iff_cover.mp
    (PrespectralSpace.isBasis_opens X) ⟨f ⁻¹' U, hU.preimage hfc⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
⊢ ∃ (t : Finset (↑Us : Type u_1)), U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
have refine : ∀ (x : Y) (hx : x ∈ U),
  Membership.mem (γ := Set Y)
    (⋃ (i : (↑Us : Type u_1)), (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i) x
Tactic: refine hc.elim_finite_subcover (fun s : Us ↦ f '' s.1) (fun s ↦ h _ s.1.2) (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
x : Y
hx : x ∈ U
⊢ Membership.mem (γ := Set Y)
    (⋃ (i : (↑Us : Type u_1)), (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i) x
have obtain : ∀ (x : X) (hx : f x ∈ U),
  Membership.mem (γ := Set Y)
    (⋃ (i : (↑Us : Type u_1)), (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i) (f x)
Tactic: obtain ⟨x, rfl⟩ := hs hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
x : X
hx : f x ∈ U
⊢ x ∈ sSup Us
have rwa : x ∈ { carrier := f ⁻¹' U, is_open' := sorry : Opens X }
Tactic: rwa [← heq]
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
x : X
hx : f x ∈ U
⊢ Membership.mem (γ := Set Y)
    (⋃ (i : (↑Us : Type u_1)), (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i) (f x)
have obtain : ∀ (i : Opens X) (hi : i ∈ Us) (hx : x ∈ i),
  Membership.mem (γ := Set Y)
    (⋃ (i : (↑Us : Type u_1)), (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i) (f x)
Tactic: obtain ⟨i, hi, hx⟩ := mem_sSup.mp <| by rwa [← heq]
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
⊢ ∃ (V : Opens X), IsCompact V.carrier ∧ f '' (↑V : Set X) = U
have obtain : ∀ (t : Finset (↑Us : Type u_1)) (ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i),
  ∃ (V : Opens X), IsCompact V.carrier ∧ f '' (↑V : Set X) = U
Tactic: obtain ⟨t, ht⟩ := by
    refine hc.elim_finite_subcover (fun s : Us ↦ f '' s.1) (fun s ↦ h _ s.1.2) (fun x hx ↦ ?_)
    obtain ⟨x, rfl⟩ := hs hx
    obtain ⟨i, hi, hx⟩ := mem_sSup.mp <| by rwa [← heq]
    exact Set.mem_iUnion.mpr ⟨⟨i, hi⟩, x, hx, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
⊢ ∃ (V : Opens X), IsCompact V.carrier ∧ f '' (↑V : Set X) = U
have refine_1 : IsCompact.{u_1} (X := X) (carrier (⨆ s ∈ t, (↑s : Opens X)))
Tactic: refine ⟨⨆ s ∈ t, s.1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
refine_1 : IsCompact.{u_1} (X := X) (carrier (⨆ s ∈ t, (↑s : Opens X)))
⊢ ∃ (V : Opens X), IsCompact V.carrier ∧ f '' (↑V : Set X) = U
have refine_2 : f '' (↑(⨆ s ∈ t, (↑s : Opens X)) : Set X) = U
Tactic: refine ⟨⨆ s ∈ t, s.1, ?_, ?_⟩