internlm/Lean-Github huggingface dataset:
Theorem: pow_mul_nat
Proof state before:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : n = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Tactic:
rw [n0]
Proof state after:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : n = 0
⊢ (0 ^ w) ^ 0 = 0 ^ (w * ↑0)
Theorem: pow_mul_nat
Proof state before:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : n = 0
⊢ (0 ^ w) ^ 0 = 0 ^ (w * ↑0)
Tactic:
simp
Proof state after:
no goals
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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)
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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⟩
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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)
Proof state after:
no goals
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof state after:
no goals
Theorem: UniformCauchySeqOn.bounded
Proof 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]
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof state after:
no goals
Theorem: UniformCauchySeqOn.bounded
Proof 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]
Proof 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' ⋯
Theorem: UniformCauchySeqOn.bounded
Proof 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))
Proof state after:
no goals
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof state after:
no goals
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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]
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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]))
Proof state after:
no goals
Theorem: UniformCauchySeqOn.bounded
Proof 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]
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof 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
Theorem: UniformCauchySeqOn.bounded
Proof 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]
Proof state after:
no goals
Theorem: UniformCauchySeqOn.bounded
Proof 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]
Proof state after:
no goals
Theorem: UniformCauchySeqOn.bounded
Proof 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
Proof 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