case inl
E : ℕ → Type u_1
y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder y n ↔ dist y y ≤ (1 / 2) ^ n

case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ y ∈ cylinder x n ↔ dist y x ≤ (1 / 2) ^ n
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder x n ↔ dist y x ≤ (1 / 2) ^ n
rcases eq_or_ne y x with (rfl | hne)
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ (∀ (i : ℕ), i < n → y i = x i) ↔ n ≤ firstDiff y x
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ y ∈ cylinder x n ↔ dist y x ≤ (1 / 2) ^ n
suffices (∀ i : ℕ, i < n → y i = x i) ↔ n ≤ firstDiff y x by simpa [dist_eq_of_ne hne]
case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ (∀ (i : ℕ), i < n → y i = x i) → n ≤ firstDiff y x

case inr.mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ n ≤ firstDiff y x → ∀ (i : ℕ), i < n → y i = x i
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ (∀ (i : ℕ), i < n → y i = x i) ↔ n ≤ firstDiff y x
constructor
no goals
case inl
E : ℕ → Type u_1
y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder y n ↔ dist y y ≤ (1 / 2) ^ n
simp [PiNat.dist_self]
no goals
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
this : (∀ (i : ℕ), i < n → y i = x i) ↔ n ≤ firstDiff y x
⊢ y ∈ cylinder x n ↔ dist y x ≤ (1 / 2) ^ n
simpa [dist_eq_of_ne hne]
case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
hy : ∀ (i : ℕ), i < n → y i = x i
⊢ n ≤ firstDiff y x
case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ (∀ (i : ℕ), i < n → y i = x i) → n ≤ firstDiff y x
intro hy
case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
hy : ∀ (i : ℕ), i < n → y i = x i
H : firstDiff y x < n
⊢ False
case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
hy : ∀ (i : ℕ), i < n → y i = x i
⊢ n ≤ firstDiff y x
by_contra' H
no goals
case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
hy : ∀ (i : ℕ), i < n → y i = x i
H : firstDiff y x < n
⊢ False
exact apply_firstDiff_ne hne (hy _ H)
case inr.mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
h : n ≤ firstDiff y x
i : ℕ
hi : i < n
⊢ y i = x i
case inr.mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ n ≤ firstDiff y x → ∀ (i : ℕ), i < n → y i = x i
intro h i hi
no goals
case inr.mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
h : n ≤ firstDiff y x
i : ℕ
hi : i < n
⊢ y i = x i
exact apply_eq_of_lt_firstDiff (hi.trans_le h)