case mp
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ IsOpen s → ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s

case mpr
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ (∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s) → IsOpen s
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ IsOpen s ↔ ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
constructor
case mp.mk
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
⊢ ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist { fst := i, snd := x } y < ε → y ∈ s
case mp
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ IsOpen s → ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
rintro hs ⟨i, x⟩ hx
case mp.mk.intro.intro
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
⊢ ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist { fst := i, snd := x } y < ε → y ∈ s
case mp.mk
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
⊢ ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist { fst := i, snd := x } y < ε → y ∈ s
obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ball x ε ⊆ Sigma.mk i ⁻¹' s :=
  Metric.isOpen_iff.1 (isOpen_sigma_iff.1 hs i) x hx
case mp.mk.intro.intro
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
⊢ ∀ (y : (i : ι) × E i), dist { fst := i, snd := x } y < min ε 1 → y ∈ s
case mp.mk.intro.intro
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
⊢ ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist { fst := i, snd := x } y < ε → y ∈ s
refine' ⟨min ε 1, lt_min εpos zero_lt_one, _⟩
case mp.mk.intro.intro.mk
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
j : ι
y : E j
hy : dist { fst := i, snd := x } { fst := j, snd := y } < min ε 1
⊢ { fst := j, snd := y } ∈ s
case mp.mk.intro.intro
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
⊢ ∀ (y : (i : ι) × E i), dist { fst := i, snd := x } y < min ε 1 → y ∈ s
rintro ⟨j, y⟩ hy
case mp.mk.intro.intro.mk.inl
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
y : E i
hy : dist { fst := i, snd := x } { fst := i, snd := y } < min ε 1
⊢ { fst := i, snd := y } ∈ s

case mp.mk.intro.intro.mk.inr
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
j : ι
y : E j
hy : dist { fst := i, snd := x } { fst := j, snd := y } < min ε 1
hij : i ≠ j
⊢ { fst := j, snd := y } ∈ s
case mp.mk.intro.intro.mk
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
j : ι
y : E j
hy : dist { fst := i, snd := x } { fst := j, snd := y } < min ε 1
⊢ { fst := j, snd := y } ∈ s
rcases eq_or_ne i j with (rfl | hij)
case mp.mk.intro.intro.mk.inl
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
y : E i
hy : dist x y < ε ∧ dist x y < 1
⊢ { fst := i, snd := y } ∈ s
case mp.mk.intro.intro.mk.inl
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
y : E i
hy : dist { fst := i, snd := x } { fst := i, snd := y } < min ε 1
⊢ { fst := i, snd := y } ∈ s
simp only [Sigma.dist_same, lt_min_iff] at hy
no goals
case mp.mk.intro.intro.mk.inl
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
y : E i
hy : dist x y < ε ∧ dist x y < 1
⊢ { fst := i, snd := y } ∈ s
exact hε (mem_ball'.2 hy.1)
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
j : ι
y : E j
hy : dist { fst := i, snd := x } { fst := j, snd := y } < min ε 1
hij : i ≠ j
⊢ 1 < 1
case mp.mk.intro.intro.mk.inr
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
j : ι
y : E j
hy : dist { fst := i, snd := x } { fst := j, snd := y } < min ε 1
hij : i ≠ j
⊢ { fst := j, snd := y } ∈ s
apply (lt_irrefl (1 : ℝ) _).elim
no goals
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
j : ι
y : E j
hy : dist { fst := i, snd := x } { fst := j, snd := y } < min ε 1
hij : i ≠ j
⊢ 1 < 1
calc
  1 ≤ Sigma.dist ⟨i, x⟩ ⟨j, y⟩ := Sigma.one_le_dist_of_ne hij _ _
  _ < 1 := hy.trans_le (min_le_right _ _)
case mpr
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
⊢ ∃ ε, ε > 0 ∧ ball x ε ⊆ Sigma.mk i ⁻¹' s
case mpr
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ (∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s) → IsOpen s
refine fun H => isOpen_sigma_iff.2 fun i => Metric.isOpen_iff.2 fun x hx => ?_
case mpr.intro.intro
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist { fst := i, snd := x } y < ε → y ∈ s
⊢ ∃ ε, ε > 0 ∧ ball x ε ⊆ Sigma.mk i ⁻¹' s
case mpr
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
⊢ ∃ ε, ε > 0 ∧ ball x ε ⊆ Sigma.mk i ⁻¹' s
obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ∀ y, dist (⟨i, x⟩ : Σj, E j) y < ε → y ∈ s :=
  H ⟨i, x⟩ hx
case mpr.intro.intro
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist { fst := i, snd := x } y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
⊢ y ∈ Sigma.mk i ⁻¹' s
case mpr.intro.intro
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist { fst := i, snd := x } y < ε → y ∈ s
⊢ ∃ ε, ε > 0 ∧ ball x ε ⊆ Sigma.mk i ⁻¹' s
refine' ⟨ε, εpos, fun y hy => _⟩
case mpr.intro.intro
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist { fst := i, snd := x } y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
⊢ dist { fst := i, snd := x } { fst := i, snd := y } < ε
case mpr.intro.intro
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist { fst := i, snd := x } y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
⊢ y ∈ Sigma.mk i ⁻¹' s
apply hε ⟨i, y⟩
case mpr.intro.intro
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist { fst := i, snd := x } y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
⊢ dist x y < ε
case mpr.intro.intro
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist { fst := i, snd := x } y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
⊢ dist { fst := i, snd := x } { fst := i, snd := y } < ε
rw [Sigma.dist_same]
no goals
case mpr.intro.intro
ι : Type u_2
E : ι → Type u_1
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist { fst := i, snd := x } y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
⊢ dist x y < ε
exact mem_ball'.1 hy