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 : 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)
refine_1 :
  ⋃ (t : Opens S),
      ⋃ (_ : Membership.mem (γ := Set (Opens S)) {x : Opens S | ∃ (x_1 : S) (h : x_1 ∈ U), Us x_1 h = (↑x : Set S)} t),
        (↑t : Set S) =
    U
refine_2 :
  ∀ (t : Opens S),
    Membership.mem (γ := Set (Opens S)) {x : Opens S | ∃ (x_1 : S) (h : x_1 ∈ U), Us x_1 h = (↑x : Set S)} t →
      IsCompactOpenCovered (X := X) f (↑t : Set S)
⊢ IsCompactOpenCovered (X := X) f U

Tactic:
refine 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
-- 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)
⊢ ⋃ (t : Opens S),
      ⋃ (_ : Membership.mem (γ := Set (Opens S)) {x : Opens S | ∃ (x_1 : S) (h : x_1 ∈ U), Us x_1 h = (↑x : Set S)} t),
        (↑t : Set S) =
    U

Tactic:
subset_antisymm (fun x ↦ ?_) fun x hx ↦ ?_

Premises used: 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
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)
refine_1 :
  ∀ (x : S),
    Membership.mem (γ := Set S)
        (⋃ (t : Opens S),
          ⋃ (_ :
            Membership.mem (γ := Set (Opens S)) {x : Opens S | ∃ (x_1 : S) (h : x_1 ∈ U), Us x_1 h = (↑x : Set S)} t),
            (↑t : Set S))
        x →
      x ∈ U
refine_1₁ :
  ∀ (x : S) (hx : x ∈ U),
    Membership.mem (γ := Set S)
      (⋃ (t : Opens S),
        ⋃ (_ :
          Membership.mem (γ := Set (Opens S)) {x : Opens S | ∃ (x_1 : S) (h : x_1 ∈ U), Us x_1 h = (↑x : Set S)} t),
          (↑t : Set S))
      x
⊢ ⋃ (t : Opens S),
      ⋃ (_ : Membership.mem (γ := Set (Opens S)) {x : Opens S | ∃ (x_1 : S) (h : x_1 ∈ U), Us x_1 h = (↑x : Set S)} t),
        (↑t : Set S) =
    U

Tactic:
refine subset_antisymm (fun x ↦ ?_) fun x hx ↦ ?_

Premises used: 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
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)
x : S
refine_1 : ∀ (U_1 : Set S) (hU : IsOpen U_1) (x_1 : S) (x_2 : x_1 ∈ U) (h : Us x_1 ⋯ = U_1), x ∈ U_1 → x ∈ U
⊢ Membership.mem (γ := Set S)
      (⋃ (t : Opens S),
        ⋃ (_ :
          Membership.mem (γ := Set (Opens S)) {x : Opens S | ∃ (x_1 : S) (h : x_1 ∈ U), Us x_1 h = (↑x : Set S)} t),
          (↑t : Set S))
      x →
    x ∈ U

Tactic:
simp [Opens.forall]

Premises used: TopologicalSpace.Opens.forall
-- 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)
x : S
⊢ ∀ (U_1 : Set S) (hU : IsOpen U_1) (x_1 : S) (x_2 : x_1 ∈ U) (h : Us x_1 ⋯ = U_1), x ∈ U_1 → x ∈ U

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
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)
x : S
hx : x ∈ U
⊢ ∃ (x_1 : x ∈ U), Us x ⋯ = (↑{ carrier := Us x hx, is_open' := ⋯ : Opens S } : Set S)

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 : 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)
x : S
hx : x ∈ U
⊢ Membership.mem (γ := Set S)
    (⋃ (t : Opens S),
      ⋃ (_ : Membership.mem (γ := Set (Opens S)) {x : Opens S | ∃ (x_1 : S) (h : x_1 ∈ U), Us x_1 h = (↑x : Set S)} t),
        (↑t : Set S))
    x

Tactic:
simpa using ⟨⟨Us x hx, hUo _ _⟩, ⟨x, by simpa⟩, hUx _ _⟩
-- 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)
⊢ ∀ (t : Opens S),
    Membership.mem (γ := Set (Opens S)) {x : Opens S | ∃ (x_1 : S) (h : x_1 ∈ U), Us x_1 h = (↑x : Set S)} t →
      IsCompactOpenCovered (X := X) f (↑t : Set S)

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)
i : ι
V : Opens (X i)
hV : IsCompact (↑V : Set (X i))
⊢ IsCompact.{u_3} (X := X i)
    (carrier
      ((fun (j : ι) (hj : Membership.mem (γ := Set ι) {i} j) ↦
          (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Opens (X x)) V ⋯ : Opens (X j)))
        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)
i : ι
V : Opens (X i)
hV : IsCompact (↑V : Set (X i))
⊢ ⋃ (i_1 : ι),
      ⋃ (h : Membership.mem (γ := Set ι) {i} i_1),
        f i_1 ''
          (↑((fun (j : ι) (hj : Membership.mem (γ := Set ι) {i} j) ↦
                  (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Opens (X x)) V ⋯ : Opens (X j)))
                i_1 h) :
            Set (X i_1)) =
    f i '' (↑V : Set (X i))

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)
i : ι
V : Opens (X i)
hV : IsCompact (↑V : Set (X i))
⊢ IsCompactOpenCovered (X := X) f (f i '' (↑V : Set (X i)))

Tactic:
refine ⟨{i}, Set.finite_singleton i, fun j hj ↦ hj ▸ V, by rintro i rfl; simpa, by 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)
U : Set S
κ : Type u_4
inst_1 : Finite κ
a : κ → ι
V : (k : κ) → Opens (X (a k))
hV : ∀ (k : κ), IsCompact (V k).carrier
hU : ⋃ (k : κ), f (a k) '' (↑(V k) : Set (X (a k))) = U
⊢ IsCompactOpenCovered (X := X) f U

Tactic:
of_iUnion_eq_of_finite _ hU (fun _ ↦ .image _ (hV _))

Premises used: IsCompactOpenCovered.image, 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)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
hU : IsCompactOpenCovered (X := X) f U
h :
  ∃ (κ : Type (max u_2 u_3)) (_ : Finite κ) (a : κ → ι) (V : (i : κ) → Opens (X (a i))),
    (∀ (i : κ), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)) ∧
      (∀ (i : κ), IsCompact (V i).carrier) ∧ ⋃ (i : κ), f (a i) '' (↑(V i) : Set (X (a i))) = U
obtain :
  ∀ (κ : Type (max u_2 u_3)),
    Finite κ →
      ∀ (a : κ → ι) (V : (i : κ) → Opens (X (a i)))
        (hB : ∀ (i : κ), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i))
        (hc : ∀ (i : κ), IsCompact (V i).carrier) (hU : ⋃ (i : κ), f (a i) '' (↑(V i) : Set (X (a i))) = U),
        ∃ (n : ℕ) (a : Fin n → ι) (V : (i : Fin n) → Opens (X (a i))),
          (∀ (i : Fin n), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)) ∧
            ⋃ (i : Fin n), f (a i) '' (↑(V i) : Set (X (a i))) = U
⊢ ∃ (n : ℕ) (a : Fin n → ι) (V : (i : Fin n) → Opens (X (a i))),
    (∀ (i : Fin n), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)) ∧
      ⋃ (i : Fin n), f (a i) '' (↑(V i) : Set (X (a i))) = U

Tactic:
obtain ⟨κ, _, a, V, hB, hc, hU⟩ := 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)
B : (i : ι) → Set (Opens (X i))
hB_1 : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
hU_1 : IsCompactOpenCovered (X := X) f U
κ : Type (max u_2 u_3)
w : Finite κ
a : κ → ι
V : (i : κ) → Opens (X (a i))
hB : ∀ (i : κ), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)
hc : ∀ (i : κ), IsCompact (V i).carrier
hU : ⋃ (i : κ), f (a i) '' (↑(V i) : Set (X (a i))) = U
intro :
  ∀ (val : Fintype κ),
    ∃ (n : ℕ) (a : Fin n → ι) (V : (i : Fin n) → Opens (X (a i))),
      (∀ (i : Fin n), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)) ∧
        ⋃ (i : Fin n), f (a i) '' (↑(V i) : Set (X (a i))) = U
⊢ ∃ (n : ℕ) (a : Fin n → ι) (V : (i : Fin n) → Opens (X (a i))),
    (∀ (i : Fin n), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)) ∧
      ⋃ (i : Fin n), f (a i) '' (↑(V i) : Set (X (a i))) = U

Tactic:
cases nonempty_fintype κ

Premises used: nonempty_fintype
-- 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)
B : (i : ι) → Set (Opens (X i))
hB_1 : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
hU_1 : IsCompactOpenCovered (X := X) f U
κ : Type (max u_2 u_3)
w : Finite κ
a : κ → ι
V : (i : κ) → Opens (X (a i))
hB : ∀ (i : κ), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)
hc : ∀ (i : κ), IsCompact (V i).carrier
hU : ⋃ (i : κ), f (a i) '' (↑(V i) : Set (X (a i))) = U
val : Fintype κ
⊢ ∃ (n : ℕ) (a : Fin n → ι) (V : (i : Fin n) → Opens (X (a i))),
    (∀ (i : Fin n), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)) ∧
      ⋃ (i : Fin n), f (a i) '' (↑(V i) : Set (X (a i))) = U

Tactic:
⟨Fintype.card κ, a ∘ (Fintype.equivFin κ).symm, fun i ↦ V _, fun i ↦ hB _, ?_⟩

Premises used: Function.comp, Fintype.card, Fintype.equivFin, And.intro, Exists.intro, Equiv.symm, DFunLike.coe
-- 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)
B : (i : ι) → Set (Opens (X i))
hB_1 : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
hU_1 : IsCompactOpenCovered (X := X) f U
κ : Type (max u_2 u_3)
w : Finite κ
a : κ → ι
V : (i : κ) → Opens (X (a i))
hB : ∀ (i : κ), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)
hc : ∀ (i : κ), IsCompact (V i).carrier
hU : ⋃ (i : κ), f (a i) '' (↑(V i) : Set (X (a i))) = U
val : Fintype κ
intro :
  ⋃ (i : Fin (Fintype.card κ)),
      f ((a ∘ (⇑(Equiv.symm (Fintype.equivFin κ)) : (a : Fin (Fintype.card κ)) → κ)) i) ''
        (↑((fun (i : Fin (Fintype.card κ)) ↦
                (V ((Equiv.symm (Fintype.equivFin κ) : (a : Fin (Fintype.card κ)) → κ) i) :
                  Opens (X (a ((Equiv.symm (Fintype.equivFin κ) : (a : Fin (Fintype.card κ)) → κ) i)))))
              i) :
          Set (X ((a ∘ (⇑(Fintype.equivFin κ).symm : (a : Fin (Fintype.card κ)) → κ)) i))) =
    U
⊢ ∃ (n : ℕ) (a : Fin n → ι) (V : (i : Fin n) → Opens (X (a i))),
    (∀ (i : Fin n), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)) ∧
      ⋃ (i : Fin n), f (a i) '' (↑(V i) : Set (X (a i))) = U

Tactic:
refine ⟨Fintype.card κ, a ∘ (Fintype.equivFin κ).symm, fun i ↦ V _, fun i ↦ hB _, ?_⟩
-- 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)
B : (i : ι) → Set (Opens (X i))
hB_1 : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
hU_1 : IsCompactOpenCovered (X := X) f U
κ : Type (max u_2 u_3)
w : Finite κ
a : κ → ι
V : (i : κ) → Opens (X (a i))
hB : ∀ (i : κ), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)
hc : ∀ (i : κ), IsCompact (V i).carrier
hU : ⋃ (i : κ), f (a i) '' (↑(V i) : Set (X (a i))) = U
val : Fintype κ
⊢ ⋃ (i : Fin (Fintype.card κ)),
      f ((a ∘ (⇑(Equiv.symm (Fintype.equivFin κ)) : (a : Fin (Fintype.card κ)) → κ)) i) ''
        (↑((fun (i : Fin (Fintype.card κ)) ↦
                (V ((Equiv.symm (Fintype.equivFin κ) : (a : Fin (Fintype.card κ)) → κ) i) :
                  Opens (X (a ((Equiv.symm (Fintype.equivFin κ) : (a : Fin (Fintype.card κ)) → κ) i)))))
              i) :
          Set (X ((a ∘ (⇑(Fintype.equivFin κ).symm : (a : Fin (Fintype.card κ)) → κ)) i))) =
    U

Tactic:
simp [← hU, ← (Fintype.equivFin κ).symm.surjective.iUnion_comp, Function.comp_apply]

Premises used: Fintype.equivFin, Function.Surjective.iUnion_comp, Function.comp_apply, Equiv.surjective, Equiv.symm
-- 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)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
hU : IsCompactOpenCovered (X := X) f U
suffices :
  ∃ (κ : Type (max u_2 u_3)) (_ : Finite κ) (a : κ → ι) (V : (i : κ) → Opens (X (a i))),
    (∀ (i : κ), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)) ∧
      (∀ (i : κ), IsCompact (V i).carrier) ∧ ⋃ (i : κ), f (a i) '' (↑(V i) : Set (X (a i))) = U
⊢ ∃ (n : ℕ) (a : Fin n → ι) (V : (i : Fin n) → Opens (X (a i))),
    (∀ (i : Fin n), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)) ∧
      ⋃ (i : Fin n), f (a i) '' (↑(V i) : Set (X (a i))) = U

Tactic:
suffices h : ∃ (κ : Type _) (_ : Finite κ) (a : κ → ι) (V : ∀ i, Opens (X (a i))),
      (∀ i, V i ∈ B (a i)) ∧ (∀ i, IsCompact (V i).1) ∧ ⋃ i, f (a i) '' V i = U by
    obtain ⟨κ, _, a, V, hB, hc, hU⟩ := h
    cases nonempty_fintype κ
    refine ⟨Fintype.card κ, a ∘ (Fintype.equivFin κ).symm, fun i ↦ V _, fun i ↦ hB _, ?_⟩
    simp [← hU, ← (Fintype.equivFin κ).symm.surjective.iUnion_comp, 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)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
hU : IsCompactOpenCovered (X := X) f U
obtain :
  ∀ (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),
    ∃ (κ : Type (max u_2 u_3)) (_ : Finite κ) (a : κ → ι) (V : (i : κ) → Opens (X (a i))),
      (∀ (i : κ), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)) ∧
        (∀ (i : κ), IsCompact (V i).carrier) ∧ ⋃ (i : κ), f (a i) '' (↑(V i) : Set (X (a i))) = U
⊢ ∃ (κ : Type (max u_2 u_3)) (_ : Finite κ) (a : κ → ι) (V : (i : κ) → Opens (X (a i))),
    (∀ (i : κ), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)) ∧
      (∀ (i : κ), IsCompact (V i).carrier) ∧ ⋃ (i : κ), f (a i) '' (↑(V i) : Set (X (a i))) = U

Tactic:
obtain ⟨s, hs, V, hc, hunion⟩ := 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)
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
choose :
  ∀ (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)) (_ : Finite κ) (a : κ → ι) (V : (i : κ) → Opens (X (a i))),
      (∀ (i : κ), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)) ∧
        (∀ (i : κ), IsCompact (V i).carrier) ∧ ⋃ (i : κ), f (a i) '' (↑(V i) : Set (X (a i))) = U
⊢ ∃ (κ : Type (max u_2 u_3)) (_ : Finite κ) (a : κ → ι) (V : (i : κ) → Opens (X (a i))),
    (∀ (i : κ), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)) ∧
      (∀ (i : κ), IsCompact (V i).carrier) ∧ ⋃ (i : κ), f (a i) '' (↑(V i) : Set (X (a i))) = U

Tactic:
choose Us UsB hUsf hUs using fun i : s ↦ (hB i.1).exists_finite_of_isCompact (hc i i.2)

Premises used: TopologicalSpace.Opens.IsBasis.exists_finite_of_isCompact, Subtype.val, Subtype.property
-- 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)
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)
⊢ Finite.{u_2 + 1} (↑s : Type u_2)

Tactic:
have : Finite s := 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)
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 : Finite.{u_2 + 1} (↑s : Type u_2)
⊢ ∀ (i : (↑s : Type u_2)), Finite.{u_3 + 1} (↑(Us i) : Type u_3)

Tactic:
have (i : _) : Finite (Us i) := hUsf 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)
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)
i : σ
⊢ Membership.mem (γ := Set (Opens (X (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : ι))))
    (Us (i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))))
    ((fun (i : σ) ↦ (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : Opens (X (↑i.fst : ι)))) i)

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)
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 : σ
⊢ Membership.mem (γ := Set (Opens (X (↑(x.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : ι))))
    (Us (x.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))))
    ((fun (i : σ) ↦ (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : Opens (X (↑i.fst : ι)))) x)

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)
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)
refine :
  ⋃ (i : σ),
      f ((fun (i : σ) ↦ (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : ι)) i) ''
        (↑((fun (i : σ) ↦ (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : Opens (X (↑i.fst : ι))))
              i) :
          Set (X ((fun (i : σ) ↦ (↑i.fst : ι)) i))) =
    U
⊢ ∃ (κ : Type (max u_2 u_3)) (_ : Finite κ) (a : κ → ι) (V : (i : κ) → Opens (X (a i))),
    (∀ (i : κ), Membership.mem (γ := Set (Opens (X (a i)))) (B (a i)) (V i)) ∧
      (∀ (i : κ), IsCompact (V i).carrier) ∧ ⋃ (i : κ), f (a i) '' (↑(V i) : Set (X (a i))) = U

Tactic:
refine ⟨σ, inferInstance, fun i ↦ i.1.1, fun i ↦ i.2.1, fun i ↦ UsB _ (by simp),
      fun _ ↦ hBc _ _ (UsB _ (by simp)), ?_⟩