awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
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
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))
⊢ 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:
ext
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
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
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:
simp [hge, p, Sigma.map]

Premises used: Sigma.map
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
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))

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]
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
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))
⊢ Continuous p

Tactic:
have hp : Continuous p := Continuous.sigma_map ht
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
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
⊢ Continuous (Y := S) fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))

Tactic:
simp [hf]
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
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
⊢ 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]
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
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))
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
⊢ ∃ (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
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
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
⊢ p '' V.carrier ⊆ (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) ⁻¹' U

Tactic:
simp [← heq, ← Set.preimage_comp, hcomp, Set.subset_preimage_image]

Premises used: Set.preimage_comp, Set.subset_preimage_image
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
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
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
⊢ ∃ (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]

Premises used: IsOpen.preimage, IsCompact.image, PrespectralSpace.exists_isCompact_and_isOpen_between
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
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
⊢ (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 ⊆
    U

Tactic:
simpa
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
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
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
⊢ ∃ (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:
refine ⟨⟨K, ho⟩, hK, subset_antisymm (by simpa) ?_⟩
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
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
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)
⊢ 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:
rw [← heq, ← hcomp, Set.image_comp]

Premises used: Set.image_comp
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
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
⊢ Subset.{u_1} (α := Set S)
    ((fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) '' K)
    ((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:
simp
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
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
⊢ 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:
exact subset_trans (Set.image_mono hVK) (by simp)

Premises used: Set.image_mono, subset_trans
-- Module: Mathlib.Topology.Sets.Compacts
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
mk :
  ∀ (carrier : Set α) (isCompact' : IsCompact carrier)
    (h : { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier = t.carrier),
    { carrier := carrier, isCompact' := isCompact' : Compacts α } = t
⊢ s = t

Tactic:
cases s
-- Module: Mathlib.Topology.Sets.Compacts
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
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 }
⊢ { carrier := carrier, isCompact' := isCompact' : Compacts α } = t

Tactic:
cases t
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
carrier : Set α
isCompact' : IsCompact carrier
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:
congr
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Compacts α
⊢ IsCompact (↑s : Set α)

Tactic:
s.isCompact'

Premises used: TopologicalSpace.Compacts.isCompact'
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
K : Compacts α
⊢ CompactSpace.{u_1} ↥K

Tactic:
isCompact_iff_compactSpace.1 K.isCompact

Premises used: isCompact_iff_compactSpace, TopologicalSpace.Compacts.isCompact, Iff.mp
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
x : α
s : Compacts α
⊢ x ∈ s.toCloseds ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := Compacts α) toCloseds

Tactic:
.of_comp (f := SetLike.coe) SetLike.coe_injective

Premises used: SetLike.coe_injective, Function.Injective.of_comp
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Compacts α
h : (↑s : Set α) = (↑t : Set α)
⊢ s = t

Tactic:
SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : IsCompact s
⊢ (↑{ carrier := s, isCompact' := h : Compacts α } : Set α) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Compacts α
⊢ s.carrier = (↑s : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Compacts α
⊢ (↑(s ⊔ t) : Set α) = (↑s : Set α) ∪ (↑t : Set α)

Tactic:
rfl

Premises used: Set.union, setOf, rfl