ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
⊢ CompleteSpace ((i : ι) × E i)
ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
⊢ CompleteSpace ((i : ι) × E i)
set s : ι → Set (Σi, E i) := fun i => Sigma.fst ⁻¹' {i}
ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
⊢ CompleteSpace ((i : ι) × E i)
ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
⊢ CompleteSpace ((i : ι) × E i)
set U := { p : (Σk, E k) × Σk, E k | dist p.1 p.2 < 1 }
ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
hc : ∀ (i : ι), IsComplete (s i)
⊢ CompleteSpace ((i : ι) × E i)
ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
⊢ CompleteSpace ((i : ι) × E i)
have hc : ∀ i, IsComplete (s i) := fun i => by
  simp only [← range_sigmaMk]
  exact (isometry_mk i).uniformInducing.isComplete_range
ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
hc : ∀ (i : ι), IsComplete (s i)
hd : ∀ (i j : ι) (x : (i : ι) × E i), x ∈ s i → ∀ (y : (i : ι) × E i), y ∈ s j → (x, y) ∈ U → i = j
⊢ CompleteSpace ((i : ι) × E i)
ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
hc : ∀ (i : ι), IsComplete (s i)
⊢ CompleteSpace ((i : ι) × E i)
have hd : ∀ (i j), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j := fun i j x hx y hy hxy =>
  (Eq.symm hx).trans ((fst_eq_of_dist_lt_one _ _ hxy).trans hy)
ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
hc : ∀ (i : ι), IsComplete (s i)
hd : ∀ (i j : ι) (x : (i : ι) × E i), x ∈ s i → ∀ (y : (i : ι) × E i), y ∈ s j → (x, y) ∈ U → i = j
⊢ IsComplete univ
ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
hc : ∀ (i : ι), IsComplete (s i)
hd : ∀ (i j : ι) (x : (i : ι) × E i), x ∈ s i → ∀ (y : (i : ι) × E i), y ∈ s j → (x, y) ∈ U → i = j
⊢ CompleteSpace ((i : ι) × E i)
refine' completeSpace_of_isComplete_univ _
case h.e'_3
ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
hc : ∀ (i : ι), IsComplete (s i)
hd : ∀ (i j : ι) (x : (i : ι) × E i), x ∈ s i → ∀ (y : (i : ι) × E i), y ∈ s j → (x, y) ∈ U → i = j
⊢ univ = ⋃ (i : ι), s i
ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
hc : ∀ (i : ι), IsComplete (s i)
hd : ∀ (i j : ι) (x : (i : ι) × E i), x ∈ s i → ∀ (y : (i : ι) × E i), y ∈ s j → (x, y) ∈ U → i = j
⊢ IsComplete univ
convert isComplete_iUnion_separated hc (dist_mem_uniformity zero_lt_one) hd
no goals
case h.e'_3
ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
hc : ∀ (i : ι), IsComplete (s i)
hd : ∀ (i j : ι) (x : (i : ι) × E i), x ∈ s i → ∀ (y : (i : ι) × E i), y ∈ s j → (x, y) ∈ U → i = j
⊢ univ = ⋃ (i : ι), s i
simp only [← preimage_iUnion, iUnion_of_singleton, preimage_univ]
ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
i : ι
⊢ IsComplete (range (Sigma.mk i))
ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
i : ι
⊢ IsComplete (s i)
simp only [← range_sigmaMk]
no goals
ι : Type u_2
E : ι → Type u_1
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
i : ι
⊢ IsComplete (range (Sigma.mk i))
exact (isometry_mk i).uniformInducing.isComplete_range