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)
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)
rw :
  Eq.{u_1 + 1} (α := Set S)
    (⋃ (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))))
    (⋃ (i : ι), ⋃ (h : i ∈ s), f i '' (↑(V i h) : Set (X i)))
⊢ ⋃ (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

Tactic:
rw [← hunion]
-- 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)
h :
  ∀ (x : S),
    Membership.mem (γ := Set S)
        (⋃ (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))))
        x ↔
      Membership.mem (γ := Set S) (⋃ (i : ι), ⋃ (h : i ∈ s), f i '' (↑(V i h) : Set (X i))) x
⊢ Eq.{u_1 + 1} (α := Set S)
    (⋃ (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))))
    (⋃ (i : ι), ⋃ (h : i ∈ s), f i '' (↑(V i h) : Set (X i)))

Tactic:
ext x
-- 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 : S
h :
  (∃ (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) ↔
    ∃ (i : ι) (i_1 : i ∈ s), x ∈ f i '' (↑(V i i_1) : Set (X i))
⊢ Membership.mem (γ := Set S)
      (⋃ (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))))
      x ↔
    Membership.mem (γ := Set S) (⋃ (i : ι), ⋃ (h : i ∈ s), f i '' (↑(V i h) : Set (X i))) x

Tactic:
simp_rw [Set.mem_iUnion]

Premises used: Set.mem_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)
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 :
  ∃ (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
i : σ
hi : X (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : ι)
o :
  hi ∈
    (↑(↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : Opens (X (↑i.fst : ι))) :
      Set (X (↑i.fst : ι)))
ho :
  (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)
      hi =
    x
⊢ ∃ (i : ι) (i_1 : i ∈ s), x ∈ f i '' (↑(V i i_1) : Set (X i))

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)
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 :
  (∃ (i : ι) (i_1 : i ∈ s), x ∈ f i '' (↑(V i i_1) : Set (X i))) →
    ∀ (i : ι) (hi : i ∈ s) (h : X i) (hmem : h ∈ (↑(V i hi) : Set (X i))) (heq : f i h = x),
      ∃ (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
⊢ (∃ (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) ↔
    ∃ (i : ι) (i_1 : i ∈ s), x ∈ f i '' (↑(V i i_1) : Set (X i))

Tactic:
refine ⟨fun ⟨i, hi, o, ho⟩ ↦ by aesop, fun ⟨i, hi, h, hmem, heq⟩ ↦ ?_⟩
-- 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 : 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
hmem : h ∈ (↑(V i hi) : Set (X i))
heq : f i h = x
⊢ ∃ (i_1 : Opens (X i)),
    Membership.mem (γ := Set (X i))
      (⋃ (_ :
        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) : ι))))
          i_1),
        (↑i_1 : Set (X i)))
      h

Tactic:
rw [hUs ⟨i, hi⟩, coe_sSup, Set.mem_iUnion] at hmem

Premises used: Set.mem_iUnion, Subtype.mk, TopologicalSpace.Opens.coe_sSup
-- 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 : 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
hmem : h ∈ (↑(V i hi) : Set (X i))
heq : f i h = x
hmem₁ :
  ∃ (i_1 : Opens (X i)),
    Membership.mem (γ := Set (X i))
      (⋃ (_ :
        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) : ι))))
          i_1),
        (↑i_1 : Set (X i)))
      h
⊢ f i h = x

Tactic:
rw [hUs ⟨i, hi⟩, coe_sSup, Set.mem_iUnion] at hmem

Premises used: Set.mem_iUnion, Subtype.mk, TopologicalSpace.Opens.coe_sSup
-- 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 : 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
hmem :
  ∃ (i_1 : Opens (X i)),
    Membership.mem (γ := Set (X i))
      (⋃ (_ :
        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) : ι))))
          i_1),
        (↑i_1 : Set (X i)))
      h
heq : f i h = x
h₁ :
  ∀ (a : Opens (X i))
    (ha :
      Membership.mem (γ := Set (X i))
        (⋃ (_ :
          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),
          (↑a : Set (X i)))
        h),
    ∃ (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
⊢ ∃ (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

Tactic:
obtain ⟨a, ha⟩ := hmem
-- 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 : 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 (X i))
    (⋃ (_ :
      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),
      (↑a : Set (X i)))
    h
⊢ 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

Tactic:
simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop] at ha

Premises used: Set.mem_iUnion, exists_prop, SetLike.mem_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)
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
⊢ ⋃ (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)) ⊆
    U

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 : 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
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' := ⋯ : Opens (X i) })
                  i h) :
              Set (X i)))
      x
⊢ IsCompactOpenCovered (X := X) f U

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 ↦ ?_⟩
-- 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 : 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
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' := ⋯ : Opens (X i) })
                  i h) :
              Set (X i)))
      (f i y)
⊢ 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

Tactic:
obtain ⟨i, y, rfl⟩ := hs x hx

Premises used: rfl
-- 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 : 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
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' := ⋯ : Opens (X i) })
                i h) :
            Set (X i)))
    (f i y)

Tactic:
simpa using ⟨i, y, hx, rfl⟩
-- 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
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
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)
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

Tactic:
(isOpenMap_sigma.mpr h).exists_opens_image_eq_of_prespectralSpace
      (continuous_sigma_iff.mpr hfc) (fun x hx ↦ ?_) hU hc

Premises used: Iff.mpr, IsOpenMap.exists_opens_image_eq_of_prespectralSpace, continuous_sigma_iff, isOpenMap_sigma
-- 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
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
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
⊢ ∃ (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 (isOpenMap_sigma.mpr h).exists_opens_image_eq_of_prespectralSpace
      (continuous_sigma_iff.mpr hfc) (fun x hx ↦ ?_) hU hc

Premises used: Iff.mpr, IsOpenMap.exists_opens_image_eq_of_prespectralSpace, continuous_sigma_iff, isOpenMap_sigma
-- 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
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
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:
simpa using hs x hx
-- 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 : IsCompactOpenCovered (X := Y) g U
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
⊢ IsCompactOpenCovered (X := X) f U

Tactic:
rw [iff_isCompactOpenCovered_sigmaMk, iff_of_unique] at hU ⊢

Premises used: IsCompactOpenCovered.iff_isCompactOpenCovered_sigmaMk, IsCompactOpenCovered.iff_of_unique