case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
hxy : dist x x = 0
⊢ x = x

case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy : dist x y = 0
h : x ≠ y
⊢ x = y
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy : dist x y = 0
⊢ x = y
rcases eq_or_ne x y with (rfl | h)
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
hxy : 2 ^ firstDiff x y = 0
⊢ x = y
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy : dist x y = 0
h : x ≠ y
⊢ x = y
simp [dist_eq_of_ne h] at hxy
no goals
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
hxy : 2 ^ firstDiff x y = 0
⊢ x = y
exact (two_ne_zero (pow_eq_zero hxy)).elim
no goals
case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
hxy : dist x x = 0
⊢ x = x
rfl