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)
U : Set S
h :
  ∃ (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)
hc_1 : IsCompact V.carrier
heq : (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) '' V.carrier = U
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
hc : ∀ (i : ι), IsCompact (t i)
heq' : s.sigma (α := X) t = V.carrier
this : ∀ (i : ι) (hi : i ∈ s), IsOpen (t i)
refine_2 :
  ⋃ (i : ι),
      ⋃ (h : i ∈ s),
        f i '' (↑((fun (i : ι) (hi : i ∈ s) ↦ { carrier := t i, is_open' := ⋯ : Opens (X i) }) i h) : Set (X i)) =
    U
⊢ IsCompactOpenCovered (X := X) f U

Tactic:
refine ⟨s, hs, fun i hi ↦ ⟨t i, this i hi⟩, fun i _ ↦ hc i, ?_⟩
-- 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)
U : Set S
h :
  ∃ (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)
hc_1 : IsCompact V.carrier
heq : (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) '' V.carrier = U
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
hc : ∀ (i : ι), IsCompact (t i)
heq' : s.sigma (α := X) t = V.carrier
this : ∀ (i : ι) (hi : i ∈ s), IsOpen (t i)
refine_2 refine_2₁ : ⋃ (i : ι), ⋃ (x : i ∈ s), f i '' (↑{ carrier := t i, is_open' := ⋯ : Opens (X i) } : Set (X i)) = U
refine_2₂ : ⋃ i ∈ s, f i '' t i = U
refine_2₃ :
  Eq.{u_1 + 1} (α := Set S) (⋃ i ∈ s, f i '' t i)
    ((fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) '' V.carrier)
refine_2₄ :
  Eq.{u_1 + 1} (α := Set S) (⋃ i ∈ s, f i '' t i)
    ((fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) ''
      s.sigma (α := X) t)
refine_2₅ :
  Eq.{u_1 + 1} (α := Set S) (⋃ i ∈ s, f i '' t i)
    (⋃ i ∈ s,
      (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) ∘
          Sigma.mk (β := fun (i : ι) ↦ X i) i ''
        t i)
⊢ ⋃ (i : ι),
      ⋃ (h : i ∈ s),
        f i '' (↑((fun (i : ι) (hi : i ∈ s) ↦ { carrier := t i, is_open' := ⋯ : Opens (X i) }) i h) : Set (X i)) =
    U

Tactic:
simp_rw [coe_mk, ← heq, ← heq', Set.image_sigma_eq_iUnion, Function.comp_apply]

Premises used: Set.image_sigma_eq_iUnion, TopologicalSpace.Opens.coe_mk, Function.comp_apply
-- 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)
U : Set S
rw rw₁ rw₂ :
  IsCompactOpenCovered (X := X) f 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
refine_1 :
  IsCompactOpenCovered (X := X) f U →
    ∀ (s : Set ι) (hs : s.Finite) (V : (i : ι) → i ∈ s → Opens (X i))
      (hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier)
      (hU : ⋃ (i : ι), ⋃ (h : i ∈ s), f i '' (↑(V i h) : Set (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
refine_2 refine_2₁ :
  (∃ (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)) (hc : IsCompact V.carrier)
      (heq :
        (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) '' V.carrier =
          U),
      IsCompactOpenCovered (X := X) f U
⊢ IsCompactOpenCovered (X := X) f U ↔
    IsCompactOpenCovered (X := fun (x : Unit) ↦ (i : ι) × X i)
      (fun (x : Unit) (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) U

Tactic:
classical
  rw [iff_of_unique (ι := Unit)]
  refine ⟨fun ⟨s, hs, V, hc, hU⟩ ↦ ?_, fun ⟨V, hc, heq⟩ ↦ ?_⟩
  · refine ⟨⟨s.sigma fun i ↦ if h : i ∈ s then V i h else ∅, isOpen_sigma_iff.mpr ?_⟩, ?_, ?_⟩
    · intro i
      by_cases h : i ∈ s
      · simpa [h] using (V _ _).2
      · simp [h]
    · dsimp only
      exact Set.isCompact_sigma hs fun i ↦ (by simp_all)
    · aesop
  · obtain ⟨s, t, hs, hc, heq'⟩ := hc.sigma_exists_finite_sigma_eq
    have (i : ι) (hi : i ∈ s) : IsOpen (t i) := by
      rw [← Set.mk_preimage_sigma (t := t) hi]
      exact isOpen_sigma_iff.mp (heq' ▸ V.2) i
    refine ⟨s, hs, fun i hi ↦ ⟨t i, this i hi⟩, fun i _ ↦ hc i, ?_⟩
    simp_rw [coe_mk, ← heq, ← heq', Set.image_sigma_eq_iUnion, Function.comp_apply]

Premises used: Set.image_sigma_eq_iUnion, IsCompactOpenCovered.iff_of_unique, TopologicalSpace.Opens.coe_mk, Function.comp_apply
-- 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)
U : Set S
κ : Type u_4
inst_1 : Finite κ
s : κ → Set S
hs : ⋃ (i : κ), s i = U
H : ∀ (i : κ), IsCompactOpenCovered (X := X) f (s i)
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
⊢ IsCompactOpenCovered (X := X) f U

Tactic:
rw [iff_isCompactOpenCovered_sigmaMk, iff_of_unique]

Premises used: IsCompactOpenCovered.iff_isCompactOpenCovered_sigmaMk, IsCompactOpenCovered.iff_of_unique
-- 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)
U : Set S
κ : Type u_4
inst_1 : Finite κ
s : κ → Set S
hs : ⋃ (i : κ), s i = U
H : ∀ (i : κ), IsCompactOpenCovered (X := X) f (s i)
i : κ
⊢ IsCompactOpenCovered (X := X) f (s i)

Tactic:
H i
-- 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)
U : Set S
κ : Type u_4
inst_1 : Finite κ
s : κ → Set S
hs : ⋃ (i : κ), s i = U
H : ∀ (i : κ), IsCompactOpenCovered (X := X) f (s i)
i : κ
a :
  (∃ (V : Opens ((i : ι) × X i)),
      IsCompact V.carrier ∧
        (fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) '' V.carrier =
          s i) ↔
    IsCompactOpenCovered (X := X) f (s i)
⊢ ∃ (V : Opens ((i : ι) × X i)),
    IsCompact V.carrier ∧
      (fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) '' V.carrier = s i

Tactic:
convert! H i
-- 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)
U : Set S
κ : Type u_4
inst_1 : Finite κ
s : κ → Set S
hs : ⋃ (i : κ), s i = U
H : ∀ (i : κ), IsCompactOpenCovered (X := X) f (s i)
i : κ
a :
  (∃ (V : Opens ((i : ι) × X i)),
      IsCompact V.carrier ∧
        (fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) '' V.carrier =
          s i) ↔
    IsCompactOpenCovered (X := fun (x : Unit) ↦ (i : ι) × X i)
      (fun (x : Unit) (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) (s i)
a₁ a₂ :
  (∃ (V : Opens ((i : ι) × X i)),
      IsCompact V.carrier ∧
        (fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) '' V.carrier =
          s 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 =
          s i
⊢ (∃ (V : Opens ((i : ι) × X i)),
      IsCompact V.carrier ∧
        (fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) '' V.carrier =
          s i) ↔
    IsCompactOpenCovered (X := X) f (s i)

Tactic:
rw [iff_isCompactOpenCovered_sigmaMk, iff_of_unique]

Premises used: IsCompactOpenCovered.iff_isCompactOpenCovered_sigmaMk, IsCompactOpenCovered.iff_of_unique
-- 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)
U : Set S
κ : Type u_4
inst_1 : Finite κ
s : κ → Set S
hs : ⋃ (i : κ), s i = U
H : ∀ (i : κ), IsCompactOpenCovered (X := X) f (s i)
⊢ ∀ (i : κ),
    ∃ (V : Opens ((i : ι) × X i)),
      IsCompact V.carrier ∧
        (fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) '' V.carrier =
          s i

Tactic:
have (i : κ) : ∃ (V : Opens (Σ i, X i)), IsCompact V.1 ∧ (f _ ·.snd) '' V.1 = s i := by
    convert! H i; rw [iff_isCompactOpenCovered_sigmaMk, iff_of_unique]
-- 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)
U : Set S
κ : Type u_4
inst_1 : Finite κ
s : κ → Set S
hs : ⋃ (i : κ), s i = U
H : ∀ (i : κ), IsCompactOpenCovered (X := X) f (s i)
this :
  ∀ (i : κ),
    ∃ (V : Opens ((i : ι) × X i)),
      IsCompact V.carrier ∧
        (fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) '' V.carrier =
          s i
choose :
  ∀ (V : (i : κ) → Opens ((i : ι) × X i)) (hVeq : ∀ (i : κ), IsCompact (V i).carrier)
    (hVc :
      ∀ (i : κ),
        (fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) ''
            (V i).carrier =
          s 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
⊢ ∃ (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:
choose V hVeq hVc using this
-- 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)
U : Set S
κ : Type u_4
inst_1 : Finite κ
s : κ → Set S
hs : ⋃ (i : κ), s i = U
H : ∀ (i : κ), IsCompactOpenCovered (X := X) f (s i)
V : (i : κ) → Opens ((i : ι) × X i)
hVeq : ∀ (i : κ), IsCompact (V i).carrier
hVc :
  ∀ (i : κ),
    (fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) '' (V i).carrier =
      s i
⊢ IsCompact (X := (i : ι) × X i) (carrier (⨆ (i : κ), V i))

Tactic:
simpa using isCompact_iUnion hVeq

Premises used: isCompact_iUnion
-- 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)
U : Set S
κ : Type u_4
inst_1 : Finite κ
s : κ → Set S
hs : ⋃ (i : κ), s i = U
H : ∀ (i : κ), IsCompactOpenCovered (X := X) f (s i)
V : (i : κ) → Opens ((i : ι) × X i)
hVeq : ∀ (i : κ), IsCompact (V i).carrier
hVc :
  ∀ (i : κ),
    (fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) '' (V i).carrier =
      s i
⊢ (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) ''
      carrier (⨆ (i : κ), V i) =
    U

Tactic:
simp_all [Set.image_iUnion, ← hs]

Premises used: Set.image_iUnion
-- 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)
U : Set S
κ : Type u_4
inst_1 : Finite κ
s : κ → Set S
hs : ⋃ (i : κ), s i = U
H : ∀ (i : κ), IsCompactOpenCovered (X := X) f (s i)
V : (i : κ) → Opens ((i : ι) × X i)
hVeq : ∀ (i : κ), IsCompact (V i).carrier
hVc :
  ∀ (i : κ),
    (fun (x : (i : ι) × X i) ↦ f (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i))) '' (V i).carrier =
      s 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

Tactic:
exact ⟨⨆ i, V i, by simpa using isCompact_iUnion hVeq, by simp_all [Set.image_iUnion, ← hs]⟩
-- 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)
U : Set S
s : Set (Set S)
hs : ⋃ t ∈ s, t = U
hf : s.Finite
H : ∀ t ∈ s, IsCompactOpenCovered (X := X) f t
⊢ Finite.{u_1 + 1} (↑s : Type u_1)

Tactic:
have := hf.to_subtype
-- 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)
U : Set S
s : Set (Set S)
hs : ⋃ t ∈ s, t = U
hf : s.Finite
H : ∀ t ∈ s, IsCompactOpenCovered (X := X) f t
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ ⋃ (i : (↑s : Type u_1)), (fun (i : (↑s : Type u_1)) ↦ (↑i : Set S)) i = 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)
U : Set S
s : Set (Set S)
hs : ⋃ t ∈ s, t = U
hf : s.Finite
H : ∀ t ∈ s, IsCompactOpenCovered (X := X) f t
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ ∀ (i : (↑s : Type u_1)), IsCompactOpenCovered (X := X) f ((fun (i : (↑s : Type u_1)) ↦ (↑i : Set S)) i)

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)
U : Set S
s : Set (Set S)
hs : ⋃ t ∈ s, t = U
hf : s.Finite
H : ∀ t ∈ s, IsCompactOpenCovered (X := X) f t
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ IsCompactOpenCovered (X := X) f U

Tactic:
exact of_iUnion_eq_of_finite (fun i : s ↦ i.1) (by simpa) (by simpa)

Premises used: Subtype.val, IsCompactOpenCovered.of_iUnion_eq_of_finite
-- 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 : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, (↑t : Set S) = U
H : ∀ t ∈ s, IsCompactOpenCovered (X := X) f (↑t : Set S)
⊢ U ⊆ ⋃ (i : (↑s : Type u_1)), (fun (V : (↑s : Type u_1)) ↦ (↑(↑V : Opens S) : Set S)) i

Tactic:
simp [← hs]
-- 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 : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, (↑t : Set S) = U
H : ∀ t ∈ s, IsCompactOpenCovered (X := X) f (↑t : Set S)
obtain : ∀ (t : Finset (↑s : Type u_1)) (ht : U ⊆ ⋃ i ∈ t, (↑(↑i : Opens S) : Set S)), IsCompactOpenCovered (X := X) f U
⊢ IsCompactOpenCovered (X := X) f U

Tactic:
obtain ⟨t, ht⟩ := hU.elim_finite_subcover (fun V : s ↦ V.1) (fun V ↦ V.1.2) (by simp [← hs])

Premises used: IsCompact.elim_finite_subcover, SetLike.coe, TopologicalSpace.Opens.is_open', Subtype.val
-- 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 : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, (↑t : Set S) = U
H : ∀ t ∈ s, IsCompactOpenCovered (X := X) f (↑t : Set S)
t : Finset (↑s : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (↑(↑i : Opens S) : Set S)
⊢ IsCompactOpenCovered (X := X) f U

Tactic:
of_biUnion_eq_of_finite (SetLike.coe '' (t.image Subtype.val : Set (Opens S))) ?_ ?_ ?_

Premises used: SetLike.coe, Set.image, Subtype.val, Finset.image, IsCompactOpenCovered.of_biUnion_eq_of_finite
-- 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 : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, (↑t : Set S) = U
H : ∀ t ∈ s, IsCompactOpenCovered (X := X) f (↑t : Set S)
t : Finset (↑s : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (↑(↑i : Opens S) : Set S)
refine_1 :
  ⋃ t_1 ∈ SetLike.coe '' (↑(Finset.image (Subtype.val (p := fun (x : Opens S) ↦ x ∈ s)) t) : Set (Opens S)), t_1 = U
refine_2 : (SetLike.coe '' (↑(Finset.image (Subtype.val (p := fun (x : Opens S) ↦ x ∈ s)) t) : Set (Opens S))).Finite
refine_3 :
  ∀ t_1 ∈ SetLike.coe '' (↑(Finset.image (Subtype.val (p := fun (x : Opens S) ↦ x ∈ s)) t) : Set (Opens S)),
    IsCompactOpenCovered (X := X) f t_1
⊢ IsCompactOpenCovered (X := X) f U

Tactic:
refine of_biUnion_eq_of_finite (SetLike.coe '' (t.image Subtype.val : Set (Opens S))) ?_ ?_ ?_

Premises used: SetLike.coe, Set.image, Subtype.val, Finset.image, IsCompactOpenCovered.of_biUnion_eq_of_finite
-- 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 : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, (↑t : Set S) = U
H : ∀ t ∈ s, IsCompactOpenCovered (X := X) f (↑t : Set S)
t : Finset (↑s : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (↑(↑i : Opens S) : Set S)
x : S
h :
  Membership.mem (γ := Set S)
    (⋃ t_1 ∈ SetLike.coe '' (↑(Finset.image (Subtype.val (p := fun (x : Opens S) ↦ x ∈ s)) t) : Set (Opens S)), t_1) x
⊢ x ∈ U

Tactic:
aesop
-- 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 : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, (↑t : Set S) = U
H : ∀ t ∈ s, IsCompactOpenCovered (X := X) f (↑t : Set S)
t : Finset (↑s : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (↑(↑i : Opens S) : Set S)
⊢ Subset.{u_1} (α := Set S) (⋃ i ∈ t, (↑(↑i : Opens S) : Set S))
    (⋃ t_1 ∈ SetLike.coe '' (↑(Finset.image (Subtype.val (p := fun (x : Opens S) ↦ x ∈ s)) t) : Set (Opens S)), t_1)

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 : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, (↑t : Set S) = U
H : ∀ t ∈ s, IsCompactOpenCovered (X := X) f (↑t : Set S)
t : Finset (↑s : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (↑(↑i : Opens S) : Set S)
⊢ ⋃ t_1 ∈ SetLike.coe '' (↑(Finset.image (Subtype.val (p := fun (x : Opens S) ↦ x ∈ s)) t) : Set (Opens S)), t_1 = U

Tactic:
exact subset_antisymm (fun x h ↦ by aesop) (subset_trans ht <| by simp)

Premises used: subset_trans, subset_antisymm
-- 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 : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, (↑t : Set S) = U
H : ∀ t ∈ s, IsCompactOpenCovered (X := X) f (↑t : Set S)
t : Finset (↑s : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (↑(↑i : Opens S) : Set S)
⊢ (SetLike.coe '' (↑(Finset.image (Subtype.val (p := fun (x : Opens S) ↦ x ∈ s)) t) : Set (Opens S))).Finite

Tactic:
Set.toFinite _

Premises used: Set.toFinite
-- 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 : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, (↑t : Set S) = U
H : ∀ t ∈ s, IsCompactOpenCovered (X := X) f (↑t : Set S)
t : Finset (↑s : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (↑(↑i : Opens S) : Set S)
⊢ (SetLike.coe '' (↑(Finset.image (Subtype.val (p := fun (x : Opens S) ↦ x ∈ s)) t) : Set (Opens S))).Finite

Tactic:
exact Set.toFinite _

Premises used: Set.toFinite
-- 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 : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, (↑t : Set S) = U
H : ∀ t ∈ s, IsCompactOpenCovered (X := X) f (↑t : Set S)
t : Finset (↑s : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (↑(↑i : Opens S) : Set S)
⊢ ∀ t_1 ∈ SetLike.coe '' (↑(Finset.image (Subtype.val (p := fun (x : Opens S) ↦ x ∈ s)) t) : Set (Opens S)),
    IsCompactOpenCovered (X := X) f t_1

Tactic:
grind
-- 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 : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, (↑t : Set S) = U
H : ∀ t ∈ s, IsCompactOpenCovered (X := X) f (↑t : Set S)
obtain : ∀ (t : Finset (↑s : Type u_1)) (ht : U ⊆ ⋃ i ∈ t, (↑(↑i : Opens S) : Set S)), IsCompactOpenCovered (X := X) f U
refine_1 :
  ∀ (t : Finset (↑s : Type u_1)) (ht : U ⊆ ⋃ i ∈ t, (↑(↑i : Opens S) : Set S)),
    ⋃ t_1 ∈ SetLike.coe '' (↑(Finset.image (Subtype.val (p := fun (x : Opens S) ↦ x ∈ s)) t) : Set (Opens S)), t_1 = U
refine_2 :
  ∀ (t : Finset (↑s : Type u_1)) (ht : U ⊆ ⋃ i ∈ t, (↑(↑i : Opens S) : Set S)),
    (SetLike.coe '' (↑(Finset.image (Subtype.val (p := fun (x : Opens S) ↦ x ∈ s)) t) : Set (Opens S))).Finite
refine_3 :
  ∀ (t : Finset (↑s : Type u_1)) (ht : U ⊆ ⋃ i ∈ t, (↑(↑i : Opens S) : Set S)),
    ∀ t_1 ∈ SetLike.coe '' (↑(Finset.image (Subtype.val (p := fun (x : Opens S) ↦ x ∈ s)) t) : Set (Opens S)),
      IsCompactOpenCovered (X := X) f t_1
refine_2₁ :
  ∀ (t : Finset (↑s : Type u_1)) (ht : U ⊆ ⋃ i ∈ t, (↑(↑i : Opens S) : Set S)),
    (SetLike.coe '' (↑(Finset.image (Subtype.val (p := fun (x : Opens S) ↦ x ∈ s)) t) : Set (Opens S))).Finite
refine_3₁ refine_3₂ :
  ∀ (t : Finset (↑s : Type u_1)) (ht : U ⊆ ⋃ i ∈ t, (↑(↑i : Opens S) : Set S)),
    ∀ t_1 ∈ SetLike.coe '' (↑(Finset.image (Subtype.val (p := fun (x : Opens S) ↦ x ∈ s)) t) : Set (Opens S)),
      IsCompactOpenCovered (X := X) f t_1
⊢ IsCompactOpenCovered (X := X) f U

Tactic:
classical
  obtain ⟨t, ht⟩ := hU.elim_finite_subcover (fun V : s ↦ V.1) (fun V ↦ V.1.2) (by simp [← hs])
  refine of_biUnion_eq_of_finite (SetLike.coe '' (t.image Subtype.val : Set (Opens S))) ?_ ?_ ?_
  · exact subset_antisymm (fun x h ↦ by aesop) (subset_trans ht <| by simp)
  · exact Set.toFinite _
  · grind

Premises used: Set.toFinite, IsCompact.elim_finite_subcover, SetLike.coe, TopologicalSpace.Opens.is_open', Subtype.val
-- 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 : TopologicalSpace S
U : Set S
hU : IsCompact U
H : ∀ x ∈ U, ∃ t ⊆ U, x ∈ t ∧ IsOpen t ∧ IsCompactOpenCovered (X := X) f t
choose :
  ∀ (Us : (x : S) → x ∈ U → Set S) (hU' : ∀ (x : S) (a : x ∈ U), Us x a ⊆ U) (hUx : ∀ (x : S) (a : x ∈ U), x ∈ Us x a)
    (hUo : ∀ (x : S) (a : x ∈ U), IsOpen (Us x a))
    (hU'' : ∀ (x : S) (a : x ∈ U), IsCompactOpenCovered (X := X) f (Us x a)), IsCompactOpenCovered (X := X) f U
⊢ IsCompactOpenCovered (X := X) f U

Tactic:
choose Us hU' hUx hUo hU'' using H
-- 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 : TopologicalSpace S
U : Set S
hU : IsCompact U
Us : (x : S) → x ∈ U → Set S
hU' : ∀ (x : S) (a : x ∈ U), Us x a ⊆ U
hUx : ∀ (x : S) (a : x ∈ U), x ∈ Us x a
hUo : ∀ (x : S) (a : x ∈ U), IsOpen (Us x a)
hU'' : ∀ (x : S) (a : x ∈ U), IsCompactOpenCovered (X := X) f (Us x a)
⊢ IsCompactOpenCovered (X := X) f U

Tactic:
of_biUnion_eq_of_isCompact hU { Us x h | (x : S) (h : x ∈ U) } ?_ ?_

Premises used: setOf, Exists, SetLike.coe, IsCompactOpenCovered.of_biUnion_eq_of_isCompact, Eq