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)
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
have 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
Tactic: refine ⟨Fintype.card κ, a ∘ (Fintype.equivFin κ).symm, fun i ↦ V _, fun i ↦ hB _, ?_⟩
-- 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)
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
⊢ ∃ (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
have 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
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]
-- 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)
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
⊢ ∃ (κ : 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
have 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
Tactic: obtain ⟨s, hs, V, hc, hunion⟩ := hU
Cleared hypotheses: hU
-- 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)
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
⊢ ∃ (κ : 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
have 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 : ι) sorry = 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
Tactic: choose Us UsB hUsf hUs using fun i : s ↦ (hB i.1).exists_finite_of_isCompact (hc i i.2)
-- 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)
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)
⊢ ∃ (κ : 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
have this : Finite.{u_2 + 1} (↑s : Type u_2)
Tactic: have : Finite s := hs
-- 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)
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)
⊢ ∃ (κ : 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
have this₁ : ∀ (i : (↑s : Type u_2)), Finite.{u_3 + 1} (↑(Us i) : Type u_3)
Tactic: have (i : _) : Finite (Us i) := hUsf 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)
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)
⊢ ∃ (κ : 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
have 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
Tactic: refine ⟨σ, inferInstance, fun i ↦ i.1.1, fun i ↦ i.2.1, fun i ↦ UsB _ (by simp),
      fun _ ↦ hBc _ _ (UsB _ (by simp)), ?_⟩
-- 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)
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 : σ),
      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
have 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)))
Tactic: rw [← hunion]
-- 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)
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)
⊢ 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)))
have 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
Tactic: ext x
-- 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)
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
⊢ 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
have 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))
Tactic: simp_rw [Set.mem_iUnion]
-- 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)
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
⊢ (∃ (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))
have 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
Tactic: refine ⟨fun ⟨i, hi, o, ho⟩ ↦ by aesop, fun ⟨i, hi, h, hmem, heq⟩ ↦ ?_⟩
-- 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)
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 : σ),
    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
have 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
Tactic: rw [hUs ⟨i, hi⟩, coe_sSup, Set.mem_iUnion] at hmem
Cleared hypotheses: hmem, 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)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨a, ha⟩ := hmem
Cleared hypotheses: hmem
-- 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)
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
⊢ ∃ (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
have ha₁ : 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
Cleared hypotheses: ha
-- 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)
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 (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
⊢ ∃ (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
have w : σ
Tactic: use ⟨⟨i, hi⟩, ⟨a, ha.1⟩⟩, h, ha.2, heq