awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ (i : ι), ⋃ (h : i ∈ s), f i '' (↑(V i h) : Set (X i)) = U
Us : (i : (↑s : Type u_2)) → Set (Opens (X (↑i : ι)))
UsB : ∀ (i : (↑s : Type u_2)), Us i ⊆ B (↑i : ι)
hUsf : ∀ (i : (↑s : Type u_2)), (Us i).Finite
hUs : ∀ (i : (↑s : Type u_2)), V (↑i : ι) ⋯ = sSup (Us i)
σ : Type (max u_2 u_3) := (i : (↑s : Type u_2)) × (↑(Us i) : Type u_3)
this_1 : Finite.{u_2 + 1} (↑s : Type u_2)
this : ∀ (i : (↑s : Type u_2)), Finite.{u_3 + 1} (↑(Us i) : Type u_3)
x : S
h_1 : ∃ (i : ι) (i_1 : i ∈ s), x ∈ f i '' (↑(V i i_1) : Set (X i))
i : ι
hi : i ∈ s
h : X i
heq : f i h = x
a : Opens (X i)
ha :
  Membership.mem (γ := Set (Opens (X i)))
      (Us (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) :
        Set (Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))))
      a ∧
    h ∈ a
w : σ
⊢ ∃ (i : σ),
    Membership.mem (γ := Set S)
      ((fun (a : X (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : ι)) ↦
          f (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : ι) a) ''
        (↑(↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : Opens (X (↑i.fst : ι))) :
          Set (X (↑i.fst : ι))))
      x
have w₁ : X
  (↑(Sigma.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))
        (Sigma.mk (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)
          (Subtype.mk (p := fun (x : Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))) ↦
            Membership.mem (γ := Set (Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))))
              (Us (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) x)
            a sorry))) :
    ι)
Tactic: use ⟨⟨i, hi⟩, ⟨a, ha.1⟩⟩, h, ha.2, heq
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ (i : ι), ⋃ (h : i ∈ s), f i '' (↑(V i h) : Set (X i)) = U
Us : (i : (↑s : Type u_2)) → Set (Opens (X (↑i : ι)))
UsB : ∀ (i : (↑s : Type u_2)), Us i ⊆ B (↑i : ι)
hUsf : ∀ (i : (↑s : Type u_2)), (Us i).Finite
hUs : ∀ (i : (↑s : Type u_2)), V (↑i : ι) ⋯ = sSup (Us i)
σ : Type (max u_2 u_3) := (i : (↑s : Type u_2)) × (↑(Us i) : Type u_3)
this_1 : Finite.{u_2 + 1} (↑s : Type u_2)
this : ∀ (i : (↑s : Type u_2)), Finite.{u_3 + 1} (↑(Us i) : Type u_3)
x : S
h_1 : ∃ (i : ι) (i_1 : i ∈ s), x ∈ f i '' (↑(V i i_1) : Set (X i))
i : ι
hi : i ∈ s
h : X i
heq : f i h = x
a : Opens (X i)
ha :
  Membership.mem (γ := Set (Opens (X i)))
      (Us (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) :
        Set (Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))))
      a ∧
    h ∈ a
w : σ
w₁ :
  X
    (↑(Sigma.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))
          (Sigma.mk (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)
            (Subtype.mk (p := fun (x : Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))) ↦
              Membership.mem (γ := Set (Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))))
                (Us (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) x)
              a ⋯))) :
      ι)
⊢ ∃ (i : σ),
    Membership.mem (γ := Set S)
      ((fun (a : X (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : ι)) ↦
          f (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : ι) a) ''
        (↑(↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : Opens (X (↑i.fst : ι))) :
          Set (X (↑i.fst : ι))))
      x
have left : h ∈
  (↑(↑(Sigma.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))
            (Sigma.mk (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))
              (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)
              (Subtype.mk (p := fun (x : Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))) ↦
                Membership.mem (γ := Set (Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))))
                  (Us (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) x)
                a sorry))) :
        Opens (X (↑⟨⟨i, hi⟩, ⟨a, sorry⟩⟩.fst : ι))) :
    Set (X (↑⟨⟨i, hi⟩, ⟨a, sorry⟩⟩.fst : ι)))
Tactic: use ⟨⟨i, hi⟩, ⟨a, ha.1⟩⟩, h, ha.2, heq
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : Finite ι
inst_2 : TopologicalSpace S
hf : ∀ (i : ι), IsSpectralMap (f i)
U : Set S
hs : ∀ x ∈ U, ∃ (i : ι), x ∈ Set.range (f i)
hU : IsOpen U
hc : IsCompact U
⊢ IsCompactOpenCovered (X := X) f U
have refine : ∀ (x : S) (hx : x ∈ U),
  Membership.mem (γ := Set S)
    (⋃ (i : ι),
      ⋃ (h : Membership.mem (γ := Set ι) Set.univ i),
        f i ''
          (↑((fun (i : ι) (x : Membership.mem (γ := Set ι) Set.univ i) ↦
                  { carrier := f i ⁻¹' U, is_open' := sorry : Opens (X i) })
                i h) :
            Set (X i)))
    x
Tactic: refine ⟨.univ, Set.finite_univ, fun i _ ↦ ⟨f i ⁻¹' U, hU.preimage (hf i).1⟩,
    fun i _ ↦ hc.preimage_of_isOpen (hf i) hU, subset_antisymm (by simp) fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : Finite ι
inst_2 : TopologicalSpace S
hf : ∀ (i : ι), IsSpectralMap (f i)
U : Set S
hs : ∀ x ∈ U, ∃ (i : ι), x ∈ Set.range (f i)
hU : IsOpen U
hc : IsCompact U
x : S
hx : x ∈ U
⊢ Membership.mem (γ := Set S)
    (⋃ (i : ι),
      ⋃ (h : Membership.mem (γ := Set ι) Set.univ i),
        f i ''
          (↑((fun (i : ι) (x : Membership.mem (γ := Set ι) Set.univ i) ↦
                  { carrier := f i ⁻¹' U, is_open' := ⋯ : Opens (X i) })
                i h) :
            Set (X i)))
    x
have obtain : ∀ (i : ι) (y : X i) (hx : f i y ∈ U),
  Membership.mem (γ := Set S)
    (⋃ (i : ι),
      ⋃ (h : Membership.mem (γ := Set ι) Set.univ i),
        f i ''
          (↑((fun (i : ι) (x : Membership.mem (γ := Set ι) Set.univ i) ↦
                  { carrier := f i ⁻¹' U, is_open' := sorry : Opens (X i) })
                i h) :
            Set (X i)))
    (f i y)
Tactic: obtain ⟨i, y, rfl⟩ := hs x hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : TopologicalSpace S
inst_2 : ∀ (i : ι), PrespectralSpace.{u_3} (X i)
hfc : ∀ (i : ι), Continuous (f i)
h : ∀ (i : ι), IsOpenMap (f i)
U : Set S
hs : ∀ x ∈ U, ∃ (i : ι), x ∈ Set.range (f i)
hU : IsOpen U
hc : IsCompact U
⊢ IsCompactOpenCovered (X := X) f U
have rw : ∃ (V : Opens ((i : ι) × X i)),
  IsCompact V.carrier ∧
    (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) '' V.carrier = U
Tactic: rw [iff_isCompactOpenCovered_sigmaMk, iff_of_unique]
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : TopologicalSpace S
inst_2 : ∀ (i : ι), PrespectralSpace.{u_3} (X i)
hfc : ∀ (i : ι), Continuous (f i)
h : ∀ (i : ι), IsOpenMap (f i)
U : Set S
hs : ∀ x ∈ U, ∃ (i : ι), x ∈ Set.range (f i)
hU : IsOpen U
hc : IsCompact U
⊢ ∃ (V : Opens ((i : ι) × X i)),
    IsCompact V.carrier ∧
      (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) '' V.carrier = U
have refine : ∀ (x : S) (hx : x ∈ U),
  Membership.mem (γ := Set S)
    (Set.range fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) x
Tactic: refine (isOpenMap_sigma.mpr h).exists_opens_image_eq_of_prespectralSpace
      (continuous_sigma_iff.mpr hfc) (fun x hx ↦ ?_) hU hc
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), PrespectralSpace.{u_3} (X i)
inst_2 : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst_3 : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf : ∀ (i : ι), Continuous (f i)
U : Set S
ho : IsOpen U
hU : IsCompactOpenCovered (X := Y) g U
⊢ IsCompactOpenCovered (X := X) f U
have rw : ∀
  (hU :
    ∃ (V : Opens ((i : σ) × Y i)),
      IsCompact V.carrier ∧
        (fun (p : (i : σ) × Y i) ↦ g (p.fst (β := fun (i : σ) ↦ Y i)) (p.snd (β := fun (i : σ) ↦ Y i))) '' V.carrier =
          U),
  ∃ (V : Opens ((i : ι) × X i)),
    IsCompact V.carrier ∧
      (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) '' V.carrier = U
Tactic: rw [iff_isCompactOpenCovered_sigmaMk, iff_of_unique] at hU ⊢
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), PrespectralSpace.{u_3} (X i)
inst_2 : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst_3 : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf : ∀ (i : ι), Continuous (f i)
U : Set S
ho : IsOpen U
hU :
  ∃ (V : Opens ((i : σ) × Y i)),
    IsCompact V.carrier ∧
      (fun (p : (i : σ) × Y i) ↦ g (p.fst (β := fun (i : σ) ↦ Y i)) (p.snd (β := fun (i : σ) ↦ Y i))) '' V.carrier = U
p : (i : σ) × Y i → (i : ι) × X i := Sigma.map (β₁ := fun (i : σ) ↦ Y i) (β₂ := fun (i : ι) ↦ X i) a t
⊢ Eq (α := (i : σ) × Y i → S)
    ((fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) ∘ p)
    fun (x : (i : σ) × Y i) ↦ g (x.fst (β := fun (i : σ) ↦ Y i)) (x.snd (β := fun (i : σ) ↦ Y i))
have h : ∀ (x : (i : σ) × Y i),
  ((fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) ∘ p) x =
    g (x.fst (β := fun (i : σ) ↦ Y i)) (x.snd (β := fun (i : σ) ↦ Y i))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (hypothesis)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), PrespectralSpace.{u_3} (X i)
inst_2 : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst_3 : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf : ∀ (i : ι), Continuous (f i)
U : Set S
ho : IsOpen U
hU :
  ∃ (V : Opens ((i : σ) × Y i)),
    IsCompact V.carrier ∧
      (fun (p : (i : σ) × Y i) ↦ g (p.fst (β := fun (i : σ) ↦ Y i)) (p.snd (β := fun (i : σ) ↦ Y i))) '' V.carrier = U
p : (i : σ) × Y i → (i : ι) × X i := Sigma.map (β₁ := fun (i : σ) ↦ Y i) (β₂ := fun (i : ι) ↦ X i) a t
⊢ ∃ (V : Opens ((i : ι) × X i)),
    IsCompact V.carrier ∧
      (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) '' V.carrier = U
have hcomp : Eq (α := (i : σ) × Y i → S)
  ((fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) ∘ p)
  fun (x : (i : σ) × Y i) ↦ g (x.fst (β := fun (i : σ) ↦ Y i)) (x.snd (β := fun (i : σ) ↦ Y i))
Tactic: have hcomp : (fun x ↦ f x.1 x.2) ∘ p = fun x ↦ g x.1 x.2 := by
    ext
    simp [hge, p, Sigma.map]
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (hypothesis)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), PrespectralSpace.{u_3} (X i)
inst_2 : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst_3 : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf : ∀ (i : ι), Continuous (f i)
U : Set S
ho : IsOpen U
hU :
  ∃ (V : Opens ((i : σ) × Y i)),
    IsCompact V.carrier ∧
      (fun (p : (i : σ) × Y i) ↦ g (p.fst (β := fun (i : σ) ↦ Y i)) (p.snd (β := fun (i : σ) ↦ Y i))) '' V.carrier = U
p : (i : σ) × Y i → (i : ι) × X i := Sigma.map (β₁ := fun (i : σ) ↦ Y i) (β₂ := fun (i : ι) ↦ X i) a t
hcomp :
  Eq (α := (i : σ) × Y i → S)
    ((fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) ∘ p)
    fun (x : (i : σ) × Y i) ↦ g (x.fst (β := fun (i : σ) ↦ Y i)) (x.snd (β := fun (i : σ) ↦ Y i))
⊢ ∃ (V : Opens ((i : ι) × X i)),
    IsCompact V.carrier ∧
      (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) '' V.carrier = U
have hp : Continuous p
Tactic: have hp : Continuous p := Continuous.sigma_map ht
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (hypothesis)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), PrespectralSpace.{u_3} (X i)
inst_2 : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst_3 : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf : ∀ (i : ι), Continuous (f i)
U : Set S
ho : IsOpen U
hU :
  ∃ (V : Opens ((i : σ) × Y i)),
    IsCompact V.carrier ∧
      (fun (p : (i : σ) × Y i) ↦ g (p.fst (β := fun (i : σ) ↦ Y i)) (p.snd (β := fun (i : σ) ↦ Y i))) '' V.carrier = U
p : (i : σ) × Y i → (i : ι) × X i := Sigma.map (β₁ := fun (i : σ) ↦ Y i) (β₂ := fun (i : ι) ↦ X i) a t
hcomp :
  Eq (α := (i : σ) × Y i → S)
    ((fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) ∘ p)
    fun (x : (i : σ) × Y i) ↦ g (x.fst (β := fun (i : σ) ↦ Y i)) (x.snd (β := fun (i : σ) ↦ Y i))
hp : Continuous p
⊢ ∃ (V : Opens ((i : ι) × X i)),
    IsCompact V.carrier ∧
      (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) '' V.carrier = U
have hf₁ : Continuous (Y := S) fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))
Tactic: have hf : Continuous (fun p : Σ i, X i ↦ f p.1 p.2) := by simp [hf]
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), PrespectralSpace.{u_3} (X i)
inst_2 : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst_3 : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf_1 : ∀ (i : ι), Continuous (f i)
U : Set S
ho : IsOpen U
hU :
  ∃ (V : Opens ((i : σ) × Y i)),
    IsCompact V.carrier ∧
      (fun (p : (i : σ) × Y i) ↦ g (p.fst (β := fun (i : σ) ↦ Y i)) (p.snd (β := fun (i : σ) ↦ Y i))) '' V.carrier = U
p : (i : σ) × Y i → (i : ι) × X i := Sigma.map (β₁ := fun (i : σ) ↦ Y i) (β₂ := fun (i : ι) ↦ X i) a t
hcomp :
  Eq (α := (i : σ) × Y i → S)
    ((fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) ∘ p)
    fun (x : (i : σ) × Y i) ↦ g (x.fst (β := fun (i : σ) ↦ Y i)) (x.snd (β := fun (i : σ) ↦ Y i))
hp : Continuous p
hf : Continuous (Y := S) fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))
⊢ ∃ (V : Opens ((i : ι) × X i)),
    IsCompact V.carrier ∧
      (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) '' V.carrier = U
have obtain : ∀ (V : Opens ((i : σ) × Y i)) (hV : IsCompact V.carrier)
  (heq :
    (fun (p : (i : σ) × Y i) ↦ g (p.fst (β := fun (i : σ) ↦ Y i)) (p.snd (β := fun (i : σ) ↦ Y i))) '' V.carrier = U),
  ∃ (V : Opens ((i : ι) × X i)),
    IsCompact V.carrier ∧
      (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) '' V.carrier = U
Tactic: obtain ⟨V, hV, heq⟩ := hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), PrespectralSpace.{u_3} (X i)
inst_2 : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst_3 : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf_1 : ∀ (i : ι), Continuous (f i)
U : Set S
ho : IsOpen U
p : (i : σ) × Y i → (i : ι) × X i := Sigma.map (β₁ := fun (i : σ) ↦ Y i) (β₂ := fun (i : ι) ↦ X i) a t
hcomp :
  Eq (α := (i : σ) × Y i → S)
    ((fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) ∘ p)
    fun (x : (i : σ) × Y i) ↦ g (x.fst (β := fun (i : σ) ↦ Y i)) (x.snd (β := fun (i : σ) ↦ Y i))
hp : Continuous p
hf : Continuous (Y := S) fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))
V : Opens ((i : σ) × Y i)
hV : IsCompact V.carrier
heq : (fun (p : (i : σ) × Y i) ↦ g (p.fst (β := fun (i : σ) ↦ Y i)) (p.snd (β := fun (i : σ) ↦ Y i))) '' V.carrier = U
⊢ ∃ (V : Opens ((i : ι) × X i)),
    IsCompact V.carrier ∧
      (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) '' V.carrier = U
have obtain : ∀ (K : Set ((i : ι) × X i)) (hK : IsCompact K) (ho : IsOpen K) (hVK : p '' V.carrier ⊆ K)
  (hKU : K ⊆ (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) ⁻¹' U),
  ∃ (V : Opens ((i : ι) × X i)),
    IsCompact V.carrier ∧
      (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) '' V.carrier = U
Tactic: obtain ⟨K, hK, ho, hVK, hKU⟩ := PrespectralSpace.exists_isCompact_and_isOpen_between
      (hV.image hp) (ho.preimage hf) <| by
    simp [← heq, ← Set.preimage_comp, hcomp, Set.subset_preimage_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), PrespectralSpace.{u_3} (X i)
inst_2 : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst_3 : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf_1 : ∀ (i : ι), Continuous (f i)
U : Set S
ho_1 : IsOpen U
p : (i : σ) × Y i → (i : ι) × X i := Sigma.map (β₁ := fun (i : σ) ↦ Y i) (β₂ := fun (i : ι) ↦ X i) a t
hcomp :
  Eq (α := (i : σ) × Y i → S)
    ((fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) ∘ p)
    fun (x : (i : σ) × Y i) ↦ g (x.fst (β := fun (i : σ) ↦ Y i)) (x.snd (β := fun (i : σ) ↦ Y i))
hp : Continuous p
hf : Continuous (Y := S) fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))
V : Opens ((i : σ) × Y i)
hV : IsCompact V.carrier
heq : (fun (p : (i : σ) × Y i) ↦ g (p.fst (β := fun (i : σ) ↦ Y i)) (p.snd (β := fun (i : σ) ↦ Y i))) '' V.carrier = U
K : Set ((i : ι) × X i)
hK : IsCompact K
ho : IsOpen K
hVK : p '' V.carrier ⊆ K
hKU : K ⊆ (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) ⁻¹' U
⊢ ∃ (V : Opens ((i : ι) × X i)),
    IsCompact V.carrier ∧
      (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) '' V.carrier = U
have refine : U ⊆
  (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) ''
    { carrier := K, is_open' := ho : Opens ((i : ι) × X i) }.carrier
Tactic: refine ⟨⟨K, ho⟩, hK, subset_antisymm (by simpa) ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), PrespectralSpace.{u_3} (X i)
inst_2 : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst_3 : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf_1 : ∀ (i : ι), Continuous (f i)
U : Set S
ho_1 : IsOpen U
p : (i : σ) × Y i → (i : ι) × X i := Sigma.map (β₁ := fun (i : σ) ↦ Y i) (β₂ := fun (i : ι) ↦ X i) a t
hcomp :
  Eq (α := (i : σ) × Y i → S)
    ((fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) ∘ p)
    fun (x : (i : σ) × Y i) ↦ g (x.fst (β := fun (i : σ) ↦ Y i)) (x.snd (β := fun (i : σ) ↦ Y i))
hp : Continuous p
hf : Continuous (Y := S) fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))
V : Opens ((i : σ) × Y i)
hV : IsCompact V.carrier
heq : (fun (p : (i : σ) × Y i) ↦ g (p.fst (β := fun (i : σ) ↦ Y i)) (p.snd (β := fun (i : σ) ↦ Y i))) '' V.carrier = U
K : Set ((i : ι) × X i)
hK : IsCompact K
ho : IsOpen K
hVK : p '' V.carrier ⊆ K
hKU : K ⊆ (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) ⁻¹' U
⊢ U ⊆
    (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) ''
      { carrier := K, is_open' := ho : Opens ((i : ι) × X i) }.carrier
have rw : Subset.{u_1} (α := Set S)
  ((fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) '' p '' V.carrier)
  ((fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) ''
    { carrier := K, is_open' := ho : Opens ((i : ι) × X i) }.carrier)
Tactic: rw [← heq, ← hcomp, Set.image_comp]
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s t : Compacts α
h : s.carrier = t.carrier
⊢ s = t
have mk : ∀ (carrier : Set α) (isCompact' : IsCompact carrier)
  (h : { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier = t.carrier),
  { carrier := carrier, isCompact' := isCompact' : Compacts α } = t
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
t : Compacts α
carrier : Set α
isCompact' : IsCompact carrier
h : { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier = t.carrier
⊢ { carrier := carrier, isCompact' := isCompact' : Compacts α } = t
have mk : ∀ (carrier_1 : Set α) (isCompact'_1 : IsCompact carrier_1)
  (h :
    { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier =
      { carrier := carrier_1, isCompact' := isCompact'_1 : Compacts α }.carrier),
  { carrier := carrier, isCompact' := isCompact' : Compacts α } = { carrier := carrier_1, isCompact' := isCompact'_1 }
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
s : Finset ι
f : ι → Compacts α
⊢ (↑(s.sup f) : Set α) = s.sup fun (i : ι) ↦ (↑(f i) : Set α)
have refine : ∀ (a : ι) (s : Finset ι) (x : a ∉ s) (h : (↑(s.sup f) : Set α) = s.sup fun (i : ι) ↦ (↑(f i) : Set α)),
  (↑((Finset.cons a s x).sup f) : Set α) = (Finset.cons a s x).sup fun (i : ι) ↦ (↑(f i) : Set α)
Tactic: refine Finset.cons_induction_on s rfl fun a s _ h => ?_