awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
a b : IrreducibleCloseds β
hle :
  LE.le.{u_2} (α := (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
    (({
            toFun := fun (T : IrreducibleCloseds β) ↦
              Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
                Membership.mem (γ := Set (IrreducibleCloseds α))
                  {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
                (map f ⋯ T) ⋯,
            invFun := fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
              { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := ⋯, isClosed' := ⋯ },
            left_inv := ⋯, right_inv := ⋯ } :
          (a : IrreducibleCloseds β) → (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
        a :
      (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
    (({
            toFun := fun (T : IrreducibleCloseds β) ↦
              Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
                Membership.mem (γ := Set (IrreducibleCloseds α))
                  {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
                (map f ⋯ T) ⋯,
            invFun := fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
              { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := ⋯, isClosed' := ⋯ },
            left_inv := ⋯, right_inv := ⋯ } :
          (a : IrreducibleCloseds β) → (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
        b :
      (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
⊢ a ≤ b

Tactic:
simpa [← h.isEmbedding.closure_eq_preimage_closure_image, a.isClosed.closure_eq,
      b.isClosed.closure_eq] using Set.preimage_mono (f := f) hle

Premises used: Topology.IsOpenEmbedding.isEmbedding, IsClosed.closure_eq, TopologicalSpace.IrreducibleCloseds.isClosed, Set.preimage_mono, Topology.IsEmbedding.closure_eq_preimage_closure_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)
⊢ Eq.{u_1 + 1} (α := Set S)
    (⋃ (i : ι),
      ⋃ (h : Membership.mem (γ := Set ι) ∅ i),
        f i ''
          (↑((fun (x : ι) (x_1 : Membership.mem (γ := Set ι) ∅ x) ↦ ({ carrier := ∅, is_open' := ⋯ } : Opens (X x))) i
                h) :
            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)
U : Set S
inst_1 : Unique ι
⊢ IsCompactOpenCovered (X := X) f U ↔ ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U

Tactic:
⟨fun ⟨s, hs, V, hc, hcov⟩ ↦ ?_, fun ⟨V, hc, h⟩ ↦ ?_⟩

Premises used: Inhabited.default, Exists, IsCompactOpenCovered, TopologicalSpace.Opens.carrier, And, Iff.intro, Set.image, _private.0.IsCompactOpenCovered.iff_of_unique.match_2, _private.0.IsCompactOpenCovered.iff_of_unique.match_1, Eq, IsCompact
-- 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
inst_1 : Unique ι
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)
      (hcov : ⋃ (i : ι), ⋃ (h : i ∈ s), f i '' (↑(V i h) : Set (X i)) = U),
      ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U
refine_2 :
  (∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U) →
    ∀ (V : Opens (X default)) (hc : IsCompact V.carrier) (h : f default '' V.carrier = U),
      IsCompactOpenCovered (X := X) f U
⊢ IsCompactOpenCovered (X := X) f U ↔ ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U

Tactic:
refine ⟨fun ⟨s, hs, V, hc, hcov⟩ ↦ ?_, fun ⟨V, hc, 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)
U : Set S
inst_1 : Unique ι
h : 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
hcov : ⋃ (i : ι), ⋃ (h : i ∈ s), f i '' (↑(V i h) : Set (X i)) = U
refine_1 : s = ∅ → ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U
refine_1₁ : s = {default} → ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U
⊢ ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U

Tactic:
cases s.eq_empty_or_singleton_of_unique

Premises used: Set.eq_empty_or_singleton_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
inst_1 : Unique ι
h : 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
hcov : ⋃ (i : ι), ⋃ (h : i ∈ s), f i '' (↑(V i h) : Set (X i)) = U
h_1 : s = ∅
⊢ ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = 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)
U : Set S
inst_1 : Unique ι
h : 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
hcov : ⋃ (i : ι), ⋃ (h : i ∈ s), f i '' (↑(V i h) : Set (X i)) = U
h_1 : s = {default}
⊢ ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = 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)
U : Set S
inst_1 : Unique ι
h_1 : ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U
V : Opens (X default)
hc : IsCompact V.carrier
h : f default '' V.carrier = U
⊢ ⋃ (i : ι),
      ⋃ (h : Membership.mem (γ := Set ι) {default} i),
        f i ''
          (↑((fun (i : ι) (h : Membership.mem (γ := Set ι) {default} i) ↦
                  (Eq.rec (motive := fun (x : ι) (h : default = x) ↦ Opens (X x)) V ⋯ : Opens (X i)))
                i h) :
            Set (X 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
inst_1 : Unique ι
h_1 : ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U
V : Opens (X default)
hc : IsCompact V.carrier
h : f default '' V.carrier = U
refine_2 :
  ∀ (i : ι) (h : Membership.mem (γ := Set ι) {default} i),
    IsCompact.{u_3} (X := X i)
      (carrier
        ((fun (i : ι) (h : Membership.mem (γ := Set ι) {default} i) ↦
            (Eq.rec (motive := fun (x : ι) (h : default = x) ↦ Opens (X x)) V ⋯ : Opens (X i)))
          i h))
⊢ IsCompactOpenCovered (X := X) f U

Tactic:
refine ⟨{default}, Set.finite_singleton _, fun i h ↦ h ▸ V, fun i ↦ ?_, 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)
U : Set S
inst_1 : Unique ι
h_1 : ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U
V : Opens (X default)
hc : IsCompact V.carrier
h : f default '' V.carrier = U
⊢ IsCompact.{u_3} (X := X default)
    (carrier
      ((fun (i : ι) (h : Membership.mem (γ := Set ι) {default} i) ↦
          (Eq.rec (motive := fun (x : ι) (h : default = x) ↦ Opens (X x)) V ⋯ : Opens (X i)))
        default ⋯))

Tactic:
simpa
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
Goal:
S : Type u_1
U : Set S
inst : TopologicalSpace S
rw : (∃ (V : Opens S), IsCompact V.carrier ∧ id '' V.carrier = U) ↔ IsOpen U ∧ IsCompact U
⊢ IsCompactOpenCovered (X := fun (a : Unit) ↦ S) (fun (x : Unit) ↦ id) U ↔ IsOpen U ∧ IsCompact U

Tactic:
rw [iff_of_unique]

Premises used: IsCompactOpenCovered.iff_of_unique
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
Goal:
S : Type u_1
U : Set S
inst : TopologicalSpace S
h : IsOpen U ∧ IsCompact U
ho : IsOpen U
hc : IsCompact U
⊢ id '' { carrier := U, is_open' := ho : Opens S }.carrier = U

Tactic:
simp
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
Goal:
S : Type u_1
U : Set S
inst : TopologicalSpace S
refine :
  (∃ (V : Opens S), IsCompact V.carrier ∧ id '' V.carrier = U) →
    ∀ (V : Opens S) (hV : IsCompact V.carrier) (heq : id '' V.carrier = U), IsOpen U ∧ IsCompact U
⊢ (∃ (V : Opens S), IsCompact V.carrier ∧ id '' V.carrier = U) ↔ IsOpen U ∧ IsCompact U

Tactic:
refine ⟨fun ⟨V, hV, heq⟩ ↦ ?_, fun ⟨ho, hc⟩ ↦ ⟨⟨U, ho⟩, hc, by simp⟩⟩
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
Goal:
S : Type u_1
U : Set S
inst : TopologicalSpace S
h : ∃ (V : Opens S), IsCompact V.carrier ∧ id '' V.carrier = U
V : Opens S
hV : IsCompact V.carrier
heq : id '' V.carrier = U
simp : ∀ (heq : True), IsOpen (↑V : Set S) ∧ IsCompact (↑V : Set S)
⊢ IsOpen U ∧ IsCompact U

Tactic:
simp only [id_eq, Set.image_id', carrier_eq_coe, ← heq] at heq ⊢

Premises used: Set.image_id', TopologicalSpace.Opens.carrier_eq_coe, id_eq
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
Goal:
S : Type u_1
U : Set S
inst : TopologicalSpace S
h : ∃ (V : Opens S), IsCompact V.carrier ∧ id '' V.carrier = U
V : Opens S
hV : IsCompact V.carrier
heq : True
⊢ IsOpen (↑V : Set S) ∧ IsCompact (↑V : Set S)

Tactic:
⟨V.2, hV⟩

Premises used: And.intro, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Sets.CompactOpenCovered
Goal:
S : Type u_1
U : Set S
inst : TopologicalSpace S
h : ∃ (V : Opens S), IsCompact V.carrier ∧ id '' V.carrier = U
V : Opens S
hV : IsCompact V.carrier
heq : True
⊢ IsOpen (↑V : Set S) ∧ IsCompact (↑V : Set S)

Tactic:
exact ⟨V.2, hV⟩
-- 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 :
  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
⊢ 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:
rw [iff_of_unique (ι := Unit)]

Premises used: 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
⊢ 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

Tactic:
⟨fun ⟨s, hs, V, hc, hU⟩ ↦ ?_, fun ⟨V, hc, heq⟩ ↦ ?_⟩

Premises used: Exists, IsCompactOpenCovered, Sigma.fst, _private.0.IsCompactOpenCovered.iff_isCompactOpenCovered_sigmaMk.match_1, TopologicalSpace.Opens.carrier, And, Iff.intro, Set.image, _private.0.IsCompactOpenCovered.iff_of_unique.match_1, Sigma.snd, Eq, IsCompact
-- 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
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 :
  (∃ (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 ↔
    ∃ (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 ⟨fun ⟨s, hs, V, hc, hU⟩ ↦ ?_, fun ⟨V, hc, 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)
U : Set S
h : 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

Tactic:
⟨⟨s.sigma fun i ↦ if h : i ∈ s then V i h else ∅, isOpen_sigma_iff.mpr ?_⟩, ?_, ?_⟩

Premises used: Iff.mpr, Membership.mem, dite, SetLike.coe, TopologicalSpace.Opens.mk, Set.sigma, And.intro, Exists.intro, EmptyCollection.emptyCollection, isOpen_sigma_iff
-- 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 : 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
refine_1 :
  ∀ (i : ι),
    IsOpen.{u_3} (X := X i)
      (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹'
        s.sigma (α := X) fun (i : ι) ↦ if h : i ∈ s then (↑(V i h) : Set (X i)) else ∅)
refine_1₁ :
  IsCompact (X := (i : ι) × X i)
    (carrier
      { carrier := s.sigma (α := X) fun (i : ι) ↦ if h : i ∈ s then (↑(V i h) : Set (X i)) else ∅, is_open' := ⋯ })
refine_1₂ :
  (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) ''
      carrier
        { carrier := s.sigma (α := X) fun (i : ι) ↦ if h : i ∈ s then (↑(V i h) : Set (X i)) else ∅, is_open' := ⋯ } =
    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:
refine ⟨⟨s.sigma fun i ↦ if h : i ∈ s then V i h else ∅, isOpen_sigma_iff.mpr ?_⟩, ?_, ?_⟩
-- 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 : 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
i : ι
pos :
  ∀ (h : i ∈ s),
    IsOpen.{u_3} (X := X i)
      (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹'
        s.sigma (α := X) fun (i : ι) ↦ if h : i ∈ s then (↑(V i h) : Set (X i)) else ∅)
neg :
  ∀ (h : i ∉ s),
    IsOpen.{u_3} (X := X i)
      (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹'
        s.sigma (α := X) fun (i : ι) ↦ if h : i ∈ s then (↑(V i h) : Set (X i)) else ∅)
⊢ IsOpen.{u_3} (X := X i)
    (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹'
      s.sigma (α := X) fun (i : ι) ↦ if h : i ∈ s then (↑(V i h) : Set (X i)) else ∅)

Tactic:
by_cases h : i ∈ s
-- 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_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
i : ι
h : i ∈ s
⊢ IsOpen.{u_3} (X := X i)
    (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹'
      s.sigma (α := X) fun (i : ι) ↦ if h : i ∈ s then (↑(V i h) : Set (X i)) else ∅)

Tactic:
simpa [h] using (V _ _).2

Premises used: TopologicalSpace.Opens.is_open'
-- 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_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
i : ι
h : i ∉ s
⊢ IsOpen.{u_3} (X := X i)
    (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹'
      s.sigma (α := X) fun (i : ι) ↦ if h : i ∈ s then (↑(V i h) : Set (X i)) else ∅)

Tactic:
simp [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)
U : Set S
h : 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
i : ι
⊢ i ∈ s → IsCompact.{u_3} (X := X i) (if h : i ∈ s then (↑(V i h) : Set (X i)) else ∅)

Tactic:
simp_all
-- 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 : 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
⊢ IsCompact (X := (i : ι) × X i) (s.sigma (α := X) fun (i : ι) ↦ if h : i ∈ s then (↑(V i h) : Set (X i)) else ∅)

Tactic:
exact Set.isCompact_sigma hs fun i ↦ (by simp_all)

Premises used: Set.isCompact_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)
U : Set S
h : 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
⊢ (fun (p : (i : ι) × X i) ↦ f (p.fst (β := fun (i : ι) ↦ X i)) (p.snd (β := fun (i : ι) ↦ X i))) ''
      carrier
        { carrier := s.sigma (α := X) fun (i : ι) ↦ if h : i ∈ s then (↑(V i h) : Set (X i)) else ∅, is_open' := ⋯ } =
    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)
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 : 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
refine_2 :
  ∀ (s : Set ι) (t : (i : ι) → Set (X i)) (hs : s.Finite) (hc : ∀ (i : ι), IsCompact (t i))
    (heq' : s.sigma (α := X) t = V.carrier), IsCompactOpenCovered (X := X) f U
⊢ IsCompactOpenCovered (X := X) f U

Tactic:
obtain ⟨s, t, hs, hc, heq'⟩ := hc.sigma_exists_finite_sigma_eq

Premises used: IsCompact.sigma_exists_finite_sigma_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)
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
i : ι
hi : i ∈ s
rw : IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s.sigma (α := X) t)
⊢ IsOpen (t i)

Tactic:
rw [← Set.mk_preimage_sigma (t := t) hi]

Premises used: Set.mk_preimage_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)
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
i : ι
hi : i ∈ s
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s.sigma (α := X) t)

Tactic:
isOpen_sigma_iff.mp (heq' ▸ V.2) i

Premises used: Iff.mp, isOpen_sigma_iff
-- 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
i : ι
hi : i ∈ s
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s.sigma (α := X) t)

Tactic:
exact isOpen_sigma_iff.mp (heq' ▸ V.2) i

Premises used: Iff.mp, isOpen_sigma_iff
-- 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
⊢ ∀ (i : ι) (hi : i ∈ s), IsOpen (t i)

Tactic:
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
-- 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)
⊢ IsCompactOpenCovered (X := X) f U

Tactic:
⟨s, hs, fun i hi ↦ ⟨t i, this i hi⟩, fun i _ ↦ hc i, ?_⟩

Premises used: IsCompactOpenCovered, TopologicalSpace.Opens.mk, And.intro, Exists.intro