case mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
y : (i : ι) × E i
fst✝ : ι
snd✝ : E fst✝
h : dist { fst := fst✝, snd := snd✝ } y < 1
⊢ { fst := fst✝, snd := snd✝ }.fst = y.fst
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
x y : (i : ι) × E i
h : dist x y < 1
⊢ x.fst = y.fst
cases x
case mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
fst✝¹ : ι
snd✝¹ : E fst✝¹
fst✝ : ι
snd✝ : E fst✝
h : dist { fst := fst✝¹, snd := snd✝¹ } { fst := fst✝, snd := snd✝ } < 1
⊢ { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst
case mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
y : (i : ι) × E i
fst✝ : ι
snd✝ : E fst✝
h : dist { fst := fst✝, snd := snd✝ } y < 1
⊢ { fst := fst✝, snd := snd✝ }.fst = y.fst
cases y
case mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
fst✝¹ : ι
snd✝¹ : E fst✝¹
fst✝ : ι
snd✝ : E fst✝
h : fst✝¹ ≠ fst✝
⊢ 1 ≤ dist { fst := fst✝¹, snd := snd✝¹ } { fst := fst✝, snd := snd✝ }
case mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
fst✝¹ : ι
snd✝¹ : E fst✝¹
fst✝ : ι
snd✝ : E fst✝
h : dist { fst := fst✝¹, snd := snd✝¹ } { fst := fst✝, snd := snd✝ } < 1
⊢ { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst
contrapose! h
no goals
case mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
fst✝¹ : ι
snd✝¹ : E fst✝¹
fst✝ : ι
snd✝ : E fst✝
h : fst✝¹ ≠ fst✝
⊢ 1 ≤ dist { fst := fst✝¹, snd := snd✝¹ } { fst := fst✝, snd := snd✝ }
apply one_le_dist_of_ne h