-- Mathlib/Topology/Compactness/SigmaCompact.lean
/-- If `f : X → Y` is an inducing map, the image `f '' s` of a set `s` is σ-compact
  if and only `s` is σ-compact. -/
lemma Topology.IsInducing.isSigmaCompact_iff {f : X → Y} {s : Set X}
    (hf : IsInducing f) : IsSigmaCompact s ↔ IsSigmaCompact (f '' s)

Proof state:
case mpr.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ ∀ (n : ℕ), IsCompact ((fun n => f ⁻¹' L n ∩ s) n)

Tactic:
intro n

Result:
case mpr.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
n : ℕ
⊢ IsCompact ((fun n => f ⁻¹' L n ∩ s) n)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
n : ℕ
⊢ L n ⊆ f '' s

Tactic:
exact (subset_iUnion _ n).trans hcov.le

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ ⋃ n, f ⁻¹' L n ∩ s = (f ⁻¹' ⋃ n, L n) ∩ s

Tactic:
rw [preimage_iUnion, iUnion_inter]

Result:
no goals

Proof state:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ IsSigmaCompact s

Tactic:
refine ⟨fun n ↦ f ⁻¹' (L n) ∩ s, ?_, ?_⟩

Result:
case mpr.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ ∀ (n : ℕ), IsCompact ((fun n => f ⁻¹' L n ∩ s) n)

case mpr.intro.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ ⋃ n, (fun n => f ⁻¹' L n ∩ s) n = s

Proof state:
case mpr.intro.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ ⋃ n, (fun n => f ⁻¹' L n ∩ s) n = s

Tactic:
calc ⋃ n, f ⁻¹' L n ∩ s
  _ = f ⁻¹' (⋃ n, L n) ∩ s  := by rw [preimage_iUnion, iUnion_inter]
  _ = f ⁻¹' (f '' s) ∩ s := by rw [hcov]
  _ = s := inter_eq_right.mpr (subset_preimage_image _ _)

Result:
no goals

Proof state:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
⊢ IsSigmaCompact s → IsSigmaCompact (f '' s)

Tactic:
exact fun h ↦ h.image hf.continuous

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
⊢ IsSigmaCompact s ↔ IsSigmaCompact (f '' s)

Tactic:
constructor

Result:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
⊢ IsSigmaCompact s → IsSigmaCompact (f '' s)

case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
⊢ IsSigmaCompact (f '' s) → IsSigmaCompact s

Proof state:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
⊢ IsSigmaCompact (f '' s) → IsSigmaCompact s

Tactic:
rintro ⟨L, hcomp, hcov⟩

Result:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ IsSigmaCompact s

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
n : ℕ
⊢ f '' (f ⁻¹' L n ∩ s) = L n

Tactic:
rw [image_preimage_inter, inter_eq_left.mpr]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
n : ℕ
⊢ L n ⊆ f '' s

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ (f ⁻¹' ⋃ n, L n) ∩ s = f ⁻¹' (f '' s) ∩ s

Tactic:
rw [hcov]

Result:
no goals

Proof state:
case mpr.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
n : ℕ
this : f '' (f ⁻¹' L n ∩ s) = L n
⊢ IsCompact ((fun n => f ⁻¹' L n ∩ s) n)

Tactic:
apply hf.isCompact_iff.mpr (this.symm ▸ (hcomp n))

Result:
no goals

Proof state:
case mpr.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
n : ℕ
⊢ IsCompact ((fun n => f ⁻¹' L n ∩ s) n)

Tactic:
have : f '' (f ⁻¹' (L n) ∩ s) = L n := by
  rw [image_preimage_inter, inter_eq_left.mpr]
  exact (subset_iUnion _ n).trans hcov.le

Result:
case mpr.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
n : ℕ
this : f '' (f ⁻¹' L n ∩ s) = L n
⊢ IsCompact ((fun n => f ⁻¹' L n ∩ s) n)