case mp
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
⊢ (∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y) →
    ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n

case mpr
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
⊢ (∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n) →
    ∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
⊢ (∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y) ↔
    ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
constructor
case mp
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y
x y : (n : ℕ) → E n
n : ℕ
hxy : y ∈ cylinder x n
⊢ dist (f x) (f y) ≤ (1 / 2) ^ n
case mp
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
⊢ (∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y) →
    ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
intro H x y n hxy
case mp
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y
x y : (n : ℕ) → E n
n : ℕ
hxy : y ∈ cylinder x n
⊢ dist x y ≤ (1 / 2) ^ n
case mp
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y
x y : (n : ℕ) → E n
n : ℕ
hxy : y ∈ cylinder x n
⊢ dist (f x) (f y) ≤ (1 / 2) ^ n
apply (H x y).trans
case mp
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y
x y : (n : ℕ) → E n
n : ℕ
hxy : y ∈ cylinder x n
⊢ dist y x ≤ (1 / 2) ^ n
case mp
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y
x y : (n : ℕ) → E n
n : ℕ
hxy : y ∈ cylinder x n
⊢ dist x y ≤ (1 / 2) ^ n
rw [PiNat.dist_comm]
no goals
case mp
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y
x y : (n : ℕ) → E n
n : ℕ
hxy : y ∈ cylinder x n
⊢ dist y x ≤ (1 / 2) ^ n
exact mem_cylinder_iff_dist_le.1 hxy
case mpr
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
⊢ dist (f x) (f y) ≤ dist x y
case mpr
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
⊢ (∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n) →
    ∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y
intro H x y
case mpr.inl
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x : (n : ℕ) → E n
⊢ dist (f x) (f x) ≤ dist x x

case mpr.inr
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
⊢ dist (f x) (f y) ≤ dist x y
case mpr
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
⊢ dist (f x) (f y) ≤ dist x y
rcases eq_or_ne x y with (rfl | hne)
case mpr.inr
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
⊢ dist (f x) (f y) ≤ (1 / 2) ^ firstDiff x y
case mpr.inr
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
⊢ dist (f x) (f y) ≤ dist x y
rw [dist_eq_of_ne hne]
case mpr.inr
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
⊢ y ∈ cylinder x (firstDiff x y)
case mpr.inr
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
⊢ dist (f x) (f y) ≤ (1 / 2) ^ firstDiff x y
apply H x y (firstDiff x y)
case mpr.inr
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
⊢ y ∈ cylinder x (firstDiff y x)
case mpr.inr
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
⊢ y ∈ cylinder x (firstDiff x y)
rw [firstDiff_comm]
no goals
case mpr.inr
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
⊢ y ∈ cylinder x (firstDiff y x)
exact mem_cylinder_firstDiff _ _
no goals
case mpr.inl
E : ℕ → Type u_2
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x : (n : ℕ) → E n
⊢ dist (f x) (f x) ≤ dist x x
simp [PiNat.dist_nonneg]