Theorem: UniformCauchySeqOn.bounded (Ray/Misc/Topology.lean)

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
u : UniformCauchySeqOn f atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
Tactic:
generalize hc : (fun n ↦ Classical.choose ((sc.bddAbove_image (fc n).norm).exists_ge 0)) = c
State after:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
u : UniformCauchySeqOn f atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
u : UniformCauchySeqOn f atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
Tactic:
have cs : ∀ n, 0 ≤ c n ∧ ∀ x, x ∈ s → ‖f n x‖ ≤ c n := fun n ↦ by
  simpa only [← hc, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] using
    Classical.choose_spec ((sc.bddAbove_image (fc n).norm).exists_ge 0)
State after:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
u : UniformCauchySeqOn f atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
u : UniformCauchySeqOn f atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
Tactic:
rw [Metric.uniformCauchySeqOn_iff] at u
State after:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
u : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < ε
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
u : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < ε
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
Tactic:
rcases u 1 (by norm_num) with ⟨N, H⟩
State after:
case intro
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
u : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < ε
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b

State before:
case intro
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
u : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < ε
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
Tactic:
clear u
State after:
case intro
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b

State before:
case intro
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
Tactic:
generalize hbs : Finset.image c (Finset.range (N + 1)) = bs
State after:
case intro
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b

State before:
case intro
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
Tactic:
have c0 : c 0 ∈ bs := by simp [← hbs]; exists 0; simp
State after:
case intro
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b

State before:
case intro
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
Tactic:
generalize hb : 1 + bs.max' ⟨_, c0⟩ = b
State after:
case intro
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b

State before:
case intro
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
⊢ ∃ b, 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
Tactic:
exists b
State after:
case intro
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
⊢ 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b

State before:
case intro
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
⊢ 0 ≤ b ∧ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
Tactic:
constructor
State after:
case intro.left
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
⊢ 0 ≤ b

case intro.right
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
⊢ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
u : UniformCauchySeqOn f atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
n : ℕ
⊢ 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
Tactic:
simpa only [← hc, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] using
  Classical.choose_spec ((sc.bddAbove_image (fc n).norm).exists_ge 0)
State after:
no goals

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
u : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < ε
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
⊢ 1 > 0
Tactic:
norm_num
State after:
no goals

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
⊢ c 0 ∈ bs
Tactic:
simp [← hbs]
State after:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
⊢ ∃ a < N + 1, c a = c 0

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
⊢ ∃ a < N + 1, c a = c 0
Tactic:
exists 0
State after:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
⊢ 0 < N + 1 ∧ c 0 = c 0

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
⊢ 0 < N + 1 ∧ c 0 = c 0
Tactic:
simp
State after:
no goals

State before:
case intro.left
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
⊢ 0 ≤ b
Tactic:
rw [← hb]
State after:
case intro.left
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
⊢ 0 ≤ 1 + bs.max' ⋯

State before:
case intro.left
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
⊢ 0 ≤ 1 + bs.max' ⋯
Tactic:
exact add_nonneg (by norm_num) (_root_.trans (cs 0).1 (Finset.le_max' _ _ c0))
State after:
no goals

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
⊢ 0 ≤ 1
Tactic:
norm_num
State after:
no goals

State before:
case intro.right
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
⊢ ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
Tactic:
intro n x xs
State after:
case intro.right
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
⊢ ‖f n x‖ ≤ b

State before:
case intro.right
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
⊢ ‖f n x‖ ≤ b
Tactic:
by_cases nN : n ≤ N
State after:
case pos
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : n ≤ N
⊢ ‖f n x‖ ≤ b

case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : ¬n ≤ N
⊢ ‖f n x‖ ≤ b

State before:
case pos
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : n ≤ N
⊢ ‖f n x‖ ≤ b
Tactic:
have cn : c n ∈ bs := by simp [← hbs]; exists n; simp [Nat.lt_add_one_iff.mpr nN]
State after:
case pos
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : n ≤ N
cn : c n ∈ bs
⊢ ‖f n x‖ ≤ b

State before:
case pos
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : n ≤ N
cn : c n ∈ bs
⊢ ‖f n x‖ ≤ b
Tactic:
exact _root_.trans ((cs n).2 x xs) (_root_.trans (Finset.le_max' _ _ cn)
  (by simp only [le_add_iff_nonneg_left, zero_le_one, ← hb]))
State after:
no goals

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : n ≤ N
⊢ c n ∈ bs
Tactic:
simp [← hbs]
State after:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : n ≤ N
⊢ ∃ a < N + 1, c a = c n

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : n ≤ N
⊢ ∃ a < N + 1, c a = c n
Tactic:
exists n
State after:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : n ≤ N
⊢ n < N + 1 ∧ c n = c n

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : n ≤ N
⊢ n < N + 1 ∧ c n = c n
Tactic:
simp [Nat.lt_add_one_iff.mpr nN]
State after:
no goals

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : n ≤ N
cn : c n ∈ bs
⊢ bs.max' ⋯ ≤ b
Tactic:
simp only [le_add_iff_nonneg_left, zero_le_one, ← hb]
State after:
no goals

State before:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : ¬n ≤ N
⊢ ‖f n x‖ ≤ b
Tactic:
simp at nN
State after:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
⊢ ‖f n x‖ ≤ b

State before:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
⊢ ‖f n x‖ ≤ b
Tactic:
specialize H N le_rfl n nN.le x xs
State after:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
⊢ ‖f n x‖ ≤ b

State before:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
⊢ ‖f n x‖ ≤ b
Tactic:
have cN : c N ∈ bs := by simp [← hbs]; exists N; simp
State after:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
cN : c N ∈ bs
⊢ ‖f n x‖ ≤ b

State before:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
cN : c N ∈ bs
⊢ ‖f n x‖ ≤ b
Tactic:
have bN := _root_.trans ((cs N).2 x xs) (Finset.le_max' _ _ cN)
State after:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
cN : c N ∈ bs
bN : ‖f N x‖ ≤ bs.max' ⋯
⊢ ‖f n x‖ ≤ b

State before:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
cN : c N ∈ bs
bN : ‖f N x‖ ≤ bs.max' ⋯
⊢ ‖f n x‖ ≤ b
Tactic:
rw [dist_eq_norm] at H
State after:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : ‖f N x - f n x‖ < 1
cN : c N ∈ bs
bN : ‖f N x‖ ≤ bs.max' ⋯
⊢ ‖f n x‖ ≤ b

State before:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : ‖f N x - f n x‖ < 1
cN : c N ∈ bs
bN : ‖f N x‖ ≤ bs.max' ⋯
⊢ ‖f n x‖ ≤ b
Tactic:
calc ‖f n x‖ = ‖f N x - (f N x - f n x)‖ := by rw [sub_sub_cancel]
  _ ≤ ‖f N x‖ + ‖f N x - f n x‖ := norm_sub_le _ _
  _ ≤ bs.max' _ + 1 := add_le_add bN H.le
  _ = 1 + bs.max' _ := by ring
  _ = b := by simp only [hb]
State after:
no goals

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
⊢ c N ∈ bs
Tactic:
simp [← hbs]
State after:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
⊢ ∃ a < N + 1, c a = c N

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
⊢ ∃ a < N + 1, c a = c N
Tactic:
exists N
State after:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
⊢ N < N + 1 ∧ c N = c N

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
⊢ N < N + 1 ∧ c N = c N
Tactic:
simp
State after:
no goals

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : ‖f N x - f n x‖ < 1
cN : c N ∈ bs
bN : ‖f N x‖ ≤ bs.max' ⋯
⊢ ‖f n x‖ = ‖f N x - (f N x - f n x)‖
Tactic:
rw [sub_sub_cancel]
State after:
no goals

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : ‖f N x - f n x‖ < 1
cN : c N ∈ bs
bN : ‖f N x‖ ≤ bs.max' ⋯
⊢ bs.max' ⋯ + 1 = 1 + bs.max' ?m.16989
Tactic:
ring
State after:
no goals

State before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : ‖f N x - f n x‖ < 1
cN : c N ∈ bs
bN : ‖f N x‖ ≤ bs.max' ⋯
⊢ 1 + bs.max' ⋯ = b
Tactic:
simp only [hb]
State after:
no goals