X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
⊢ toInductiveLimit I (succ n) ∘ f n = toInductiveLimit I n
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
⊢ toInductiveLimit I (succ n) ∘ f n = toInductiveLimit I n
let _ := inductivePremetric I
case h
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ (toInductiveLimit I (succ n) ∘ f n) x = toInductiveLimit I n x
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
⊢ toInductiveLimit I (succ n) ∘ f n = toInductiveLimit I n
funext x
case h
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ Quotient.mk'' { fst := succ n, snd := f n x } = Quotient.mk'' { fst := n, snd := x }
case h
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ (toInductiveLimit I (succ n) ∘ f n) x = toInductiveLimit I n x
simp only [comp, toInductiveLimit]
case h
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ dist { fst := succ n, snd := f n x } { fst := n, snd := x } = 0
case h
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ Quotient.mk'' { fst := succ n, snd := f n x } = Quotient.mk'' { fst := n, snd := x }
refine' UniformSpace.SeparationQuotient.mk_eq_mk.2 (Metric.inseparable_iff.2 _)
case h
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ inductiveLimitDist f { fst := succ n, snd := f n x } { fst := n, snd := x } = 0
case h
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ dist { fst := succ n, snd := f n x } { fst := n, snd := x } = 0
show inductiveLimitDist f ⟨n.succ, f n x⟩ ⟨n, x⟩ = 0
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ { fst := n, snd := x }.fst ≤ { fst := n, snd := x }.fst

case h.h2
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ { fst := n, snd := x }.fst ≤ n + 1

X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ { fst := succ n, snd := f n x }.fst ≤ { fst := succ n, snd := f n x }.fst
case h
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ inductiveLimitDist f { fst := succ n, snd := f n x } { fst := n, snd := x } = 0
rw [inductiveLimitDist_eq_dist I ⟨n.succ, f n x⟩ ⟨n, x⟩ n.succ, leRecOn_self,
  leRecOn_succ, leRecOn_self, dist_self]
no goals
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ { fst := n, snd := x }.fst ≤ { fst := n, snd := x }.fst

case h.h2
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ { fst := n, snd := x }.fst ≤ n + 1

X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ { fst := succ n, snd := f n x }.fst ≤ { fst := succ n, snd := f n x }.fst
exacts [le_rfl, le_succ _, le_rfl]