-- Mathlib/Topology/Compactness/SigmaCompact.lean
/-- Countable unions of σ-compact sets are σ-compact. -/
lemma isSigmaCompact_iUnion [Countable ι] (s : ι → Set X)
    (hcomp : ∀ i, IsSigmaCompact (s i)) : IsSigmaCompact (⋃ i, s i)

Proof state:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
have := calc
  ⋃ i, s i
  _ = ⋃ i, ⋃ n, (K i n) := by simp_rw [hcov]
  _ = ⋃ (i) (n : ℕ), (K.uncurry ⟨i, n⟩) := by rw [Function.uncurry_def]
  _ = ⋃ x, K.uncurry x := by rw [← iUnion_prod']

Result:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
this : ⋃ i, s i = ⋃ x, Function.uncurry K x
⊢ IsSigmaCompact (⋃ i, s i)

Proof state:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
this : ⋃ i, s i = ⋃ x, Function.uncurry K x
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
rw [this]

Result:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
this : ⋃ i, s i = ⋃ x, Function.uncurry K x
⊢ IsSigmaCompact (⋃ x, Function.uncurry K x)

Proof state:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
this : ⋃ i, s i = ⋃ x, Function.uncurry K x
⊢ IsSigmaCompact (⋃ x, Function.uncurry K x)

Tactic:
exact isSigmaCompact_iUnion_of_isCompact K.uncurry fun x ↦ (hcomp x.1 x.2)

Result:
no goals

Proof state:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
⊢ ⋃ i, ⋃ n, K i n = ⋃ i, ⋃ n, Function.uncurry K (i, n)

Tactic:
rw [Function.uncurry_def]

Result:
no goals

Proof state:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
⊢ ⋃ i, ⋃ n, Function.uncurry K (i, n) = ⋃ x, Function.uncurry K x

Tactic:
rw [← iUnion_prod']

Result:
no goals

Proof state:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
⊢ ⋃ i, s i = ⋃ i, ⋃ n, K i n

Tactic:
simp_rw [hcov]

Result:
no goals

Proof state:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsSigmaCompact (s i)
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
choose K hcomp hcov using fun i ↦ hcomp i

Result:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
⊢ IsSigmaCompact (⋃ i, s i)