awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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
⊢ ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U
have refine_1₁ : s = {default} → ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U
Tactic: cases s.eq_empty_or_singleton_of_unique
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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
⊢ IsCompactOpenCovered (X := X) f U
have 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 sorry : Opens (X i)))
        i h))
Tactic: refine ⟨{default}, Set.finite_singleton _, fun i h ↦ h ▸ V, fun i ↦ ?_, by simpa⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
U : Set S
inst : TopologicalSpace S
⊢ IsCompactOpenCovered (X := fun (a : Unit) ↦ S) (fun (x : Unit) ↦ id) U ↔ IsOpen U ∧ IsCompact U
have rw : (∃ (V : Opens S), IsCompact V.carrier ∧ id '' V.carrier = U) ↔ IsOpen U ∧ IsCompact U
Tactic: rw [iff_of_unique]
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
U : Set S
inst : TopologicalSpace S
⊢ (∃ (V : Opens S), IsCompact V.carrier ∧ id '' V.carrier = U) ↔ IsOpen U ∧ IsCompact U
have 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
Tactic: refine ⟨fun ⟨V, hV, heq⟩ ↦ ?_, fun ⟨ho, hc⟩ ↦ ⟨⟨U, ho⟩, hc, by simp⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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
⊢ IsOpen U ∧ IsCompact U
have simp : ∀ (heq : True), IsOpen (↑V : Set S) ∧ IsCompact (↑V : Set S)
Tactic: simp only [id_eq, Set.image_id', carrier_eq_coe, ← heq] at heq ⊢
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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 ↔
    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
have 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
Tactic: rw [iff_of_unique (ι := Unit)]
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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
have 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
Tactic: refine ⟨fun ⟨s, hs, V, hc, hU⟩ ↦ ?_, fun ⟨V, hc, heq⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun ⟨s, hs, V, hc, hU⟩ ↦ ?_, fun ⟨V, hc, heq⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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
have 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 ∅)
Tactic: refine ⟨⟨s.sigma fun i ↦ if h : i ∈ s then V i h else ∅, isOpen_sigma_iff.mpr ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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 ∅)
⊢ ∃ (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
have 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' := sorry })
Tactic: refine ⟨⟨s.sigma fun i ↦ if h : i ∈ s then V i h else ∅, isOpen_sigma_iff.mpr ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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' := ⋯ })
⊢ ∃ (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
have 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' := sorry } =
  U
Tactic: refine ⟨⟨s.sigma fun i ↦ if h : i ∈ s then V i h else ∅, isOpen_sigma_iff.mpr ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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 : ι
⊢ 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 ∅)
have 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 ∅)
Tactic: by_cases h : i ∈ s
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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 ∅)
⊢ 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 ∅)
have 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 ∅)
Tactic: by_cases h : i ∈ s
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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
⊢ IsCompactOpenCovered (X := X) f U
have 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
Tactic: obtain ⟨s, t, hs, hc, heq'⟩ := hc.sigma_exists_finite_sigma_eq
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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)
have rw : IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s.sigma (α := X) t)
Tactic: rw [← Set.mk_preimage_sigma (t := t) hi]
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (hypothesis)
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
⊢ IsCompactOpenCovered (X := X) f U
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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
have refine_2 : ⋃ (i : ι),
    ⋃ (h : i ∈ s),
      f i '' (↑((fun (i : ι) (hi : i ∈ s) ↦ { carrier := t i, is_open' := sorry : Opens (X i) }) i h) : Set (X i)) =
  U
Tactic: refine ⟨s, hs, fun i hi ↦ ⟨t i, this i hi⟩, fun i _ ↦ hc i, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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
⊢ ⋃ (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
have refine_2₂ : ⋃ i ∈ s, f i '' t i = U
Tactic: simp_rw [coe_mk, ← heq, ← heq', Set.image_sigma_eq_iUnion, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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
⊢ ⋃ (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
have 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)
Tactic: simp_rw [coe_mk, ← heq, ← heq', Set.image_sigma_eq_iUnion, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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)
⊢ ⋃ (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
have 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)
Tactic: simp_rw [coe_mk, ← heq, ← heq', Set.image_sigma_eq_iUnion, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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)
⊢ ⋃ (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
have 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)
Tactic: simp_rw [coe_mk, ← heq, ← heq', Set.image_sigma_eq_iUnion, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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 ↔
    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
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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
⊢ 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
have 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
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]