internlm/Lean-Github huggingface dataset:
Theorem: inv_succ_le_all
Proof state before:
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
Tactic:
obtain ⟨N, hN⟩ := Metric.tendsto_atTop.1 tendsto_one_div_add_atTop_nhds_0_nat (ε/2) (by linarith)
Proof state after:
case intro
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
⊢ ∃ N, ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
Theorem: inv_succ_le_all
Proof state before:
case intro
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
⊢ ∃ N, ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
Tactic:
refine ⟨N, fun n hn ↦ ?_⟩
Proof state after:
case intro
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 1 / (↑n + 1) ≤ ε
Theorem: inv_succ_le_all
Proof state before:
case intro
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 1 / (↑n + 1) ≤ ε
Tactic:
convert (lt_trans (hN n hn) (half_lt_self hε)).le using 1
Proof state after:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 1 / (↑n + 1) = dist (1 / (↑n + 1)) 0
Theorem: inv_succ_le_all
Proof state before:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 1 / (↑n + 1) = dist (1 / (↑n + 1)) 0
Tactic:
simp only [one_div, Real.dist_eq, sub_zero]
Proof state after:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ (↑n + 1)⁻¹ = |(↑n + 1)⁻¹|
Theorem: inv_succ_le_all
Proof state before:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ (↑n + 1)⁻¹ = |(↑n + 1)⁻¹|
Tactic:
rw [abs_of_nonneg]
Proof state after:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 0 ≤ (↑n + 1)⁻¹
Theorem: inv_succ_le_all
Proof state before:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 0 ≤ (↑n + 1)⁻¹
Tactic:
simp only [inv_nonneg]
Proof state after:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 0 ≤ ↑n + 1
Theorem: inv_succ_le_all
Proof state before:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 0 ≤ ↑n + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: inv_succ_le_all
Proof state before:
ε : ℝ
hε : ε > 0
⊢ ε / 2 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: limit_const
Proof state before:
x ε : ℝ
ε_pos : ε > 0
x✝¹ : ℕ
x✝ : x✝¹ ≥ 0
⊢ |(fun x_1 => x) x✝¹ - x| ≤ ε
Tactic:
simp [le_of_lt ε_pos]
Proof state after:
no goals
Theorem: limit_of_sub_le_inv_succ
Proof state before:
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
⊢ seq_limit u x
Tactic:
intros ε ε_pos
Proof state after:
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |u n - x| ≤ ε
Theorem: limit_of_sub_le_inv_succ
Proof state before:
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |u n - x| ≤ ε
Tactic:
rcases inv_succ_le_all ε ε_pos with ⟨N, hN⟩
Proof state after:
case intro
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
⊢ ∃ N, ∀ n ≥ N, |u n - x| ≤ ε
Theorem: limit_of_sub_le_inv_succ
Proof state before:
case intro
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
⊢ ∃ N, ∀ n ≥ N, |u n - x| ≤ ε
Tactic:
use N
Proof state after:
case h
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
⊢ ∀ n ≥ N, |u n - x| ≤ ε
Theorem: limit_of_sub_le_inv_succ
Proof state before:
case h
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
⊢ ∀ n ≥ N, |u n - x| ≤ ε
Tactic:
intros n hn
Proof state after:
case h
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
n : ℕ
hn : n ≥ N
⊢ |u n - x| ≤ ε
Theorem: limit_of_sub_le_inv_succ
Proof state before:
case h
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
n : ℕ
hn : n ≥ N
⊢ |u n - x| ≤ ε
Tactic:
specialize h n
Proof state after:
case h
u : ℕ → ℝ
x ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
n : ℕ
hn : n ≥ N
h : |u n - x| ≤ 1 / (↑n + 1)
⊢ |u n - x| ≤ ε
Theorem: limit_of_sub_le_inv_succ
Proof state before:
case h
u : ℕ → ℝ
x ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
n : ℕ
hn : n ≥ N
h : |u n - x| ≤ 1 / (↑n + 1)
⊢ |u n - x| ≤ ε
Tactic:
specialize hN n hn
Proof state after:
case h
u : ℕ → ℝ
x ε : ℝ
ε_pos : ε > 0
N n : ℕ
hn : n ≥ N
h : |u n - x| ≤ 1 / (↑n + 1)
hN : 1 / (↑n + 1) ≤ ε
⊢ |u n - x| ≤ ε
Theorem: limit_of_sub_le_inv_succ
Proof state before:
case h
u : ℕ → ℝ
x ε : ℝ
ε_pos : ε > 0
N n : ℕ
hn : n ≥ N
h : |u n - x| ≤ 1 / (↑n + 1)
hN : 1 / (↑n + 1) ≤ ε
⊢ |u n - x| ≤ ε
Tactic:
linarith
Proof state after:
no goals
Theorem: limit_const_add_inv_succ
Proof state before:
x : ℝ
n : ℕ
⊢ |x + 1 / (↑n + 1) - x| ≤ 1 / (↑n + 1)
Tactic:
rw [abs_of_pos] <;> linarith [@Nat.one_div_pos_of_nat ℝ _ n]
Proof state after:
no goals
Theorem: limit_const_sub_inv_succ
Proof state before:
x : ℝ
⊢ seq_limit (fun n => x - 1 / (↑n + 1)) x
Tactic:
refine limit_of_sub_le_inv_succ (fun n ↦ ?_)
Proof state after:
x : ℝ
n : ℕ
⊢ |x - 1 / (↑n + 1) - x| ≤ 1 / (↑n + 1)
Theorem: limit_const_sub_inv_succ
Proof state before:
x : ℝ
n : ℕ
⊢ |x - 1 / (↑n + 1) - x| ≤ 1 / (↑n + 1)
Tactic:
rw [show x - 1 / (n + 1) - x = -(1/(n+1)) from by ring, abs_neg,  abs_of_pos]
Proof state after:
x : ℝ
n : ℕ
⊢ 0 < 1 / (↑n + 1)
Theorem: limit_const_sub_inv_succ
Proof state before:
x : ℝ
n : ℕ
⊢ 0 < 1 / (↑n + 1)
Tactic:
linarith [@Nat.one_div_pos_of_nat ℝ _ n]
Proof state after:
no goals
Theorem: limit_const_sub_inv_succ
Proof state before:
x : ℝ
n : ℕ
⊢ x - 1 / (↑n + 1) - x = -(1 / (↑n + 1))
Tactic:
ring
Proof state after:
no goals
Theorem: id_le_extraction
Proof state before:
φ : ℕ → ℕ
⊢ extraction φ → ∀ (n : ℕ), n ≤ φ n
Tactic:
intros hyp n
Proof state after:
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
⊢ n ≤ φ n
Theorem: id_le_extraction
Proof state before:
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
⊢ n ≤ φ n
Tactic:
induction' n with n hn
Proof state after:
case zero
φ : ℕ → ℕ
hyp : extraction φ
⊢ Nat.zero ≤ φ Nat.zero

case succ
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
hn : n ≤ φ n
⊢ Nat.succ n ≤ φ (Nat.succ n)
Theorem: id_le_extraction
Proof state before:
case zero
φ : ℕ → ℕ
hyp : extraction φ
⊢ Nat.zero ≤ φ Nat.zero
Tactic:
exact Nat.zero_le _
Proof state after:
no goals
Theorem: id_le_extraction
Proof state before:
case succ
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
hn : n ≤ φ n
⊢ Nat.succ n ≤ φ (Nat.succ n)
Tactic:
exact Nat.succ_le_of_lt (by linarith [hyp n (n+1) (by linarith)])
Proof state after:
no goals
Theorem: id_le_extraction
Proof state before:
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
hn : n ≤ φ n
⊢ n < φ (Nat.succ n)
Tactic:
linarith [hyp n (n+1) (by linarith)]
Proof state after:
no goals
Theorem: id_le_extraction
Proof state before:
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
hn : n ≤ φ n
⊢ n < n + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: seq_limit_id
Proof state before:
⊢ tendsto_infinity fun n => ↑n
Tactic:
intros A
Proof state after:
A : ℝ
⊢ ∃ N, ∀ n ≥ N, (fun n => ↑n) n ≥ A
Theorem: seq_limit_id
Proof state before:
A : ℝ
⊢ ∃ N, ∀ n ≥ N, (fun n => ↑n) n ≥ A
Tactic:
cases' exists_nat_gt A with N hN
Proof state after:
case intro
A : ℝ
N : ℕ
hN : A < ↑N
⊢ ∃ N, ∀ n ≥ N, (fun n => ↑n) n ≥ A
Theorem: seq_limit_id
Proof state before:
case intro
A : ℝ
N : ℕ
hN : A < ↑N
⊢ ∃ N, ∀ n ≥ N, (fun n => ↑n) n ≥ A
Tactic:
use N
Proof state after:
case h
A : ℝ
N : ℕ
hN : A < ↑N
⊢ ∀ n ≥ N, (fun n => ↑n) n ≥ A
Theorem: seq_limit_id
Proof state before:
case h
A : ℝ
N : ℕ
hN : A < ↑N
⊢ ∀ n ≥ N, (fun n => ↑n) n ≥ A
Tactic:
intros n hn
Proof state after:
case h
A : ℝ
N : ℕ
hN : A < ↑N
n : ℕ
hn : n ≥ N
⊢ (fun n => ↑n) n ≥ A
Theorem: seq_limit_id
Proof state before:
case h
A : ℝ
N : ℕ
hN : A < ↑N
n : ℕ
hn : n ≥ N
⊢ (fun n => ↑n) n ≥ A
Tactic:
have : (n : ℝ) ≥ N := by exact_mod_cast hn
Proof state after:
case h
A : ℝ
N : ℕ
hN : A < ↑N
n : ℕ
hn : n ≥ N
this : ↑n ≥ ↑N
⊢ (fun n => ↑n) n ≥ A
Theorem: seq_limit_id
Proof state before:
case h
A : ℝ
N : ℕ
hN : A < ↑N
n : ℕ
hn : n ≥ N
this : ↑n ≥ ↑N
⊢ (fun n => ↑n) n ≥ A
Tactic:
linarith
Proof state after:
no goals
Theorem: seq_limit_id
Proof state before:
A : ℝ
N : ℕ
hN : A < ↑N
n : ℕ
hn : n ≥ N
⊢ ↑n ≥ ↑N
Tactic:
exact_mod_cast hn
Proof state after:
no goals
Theorem: bolzano_weierstrass
Proof state before:
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
⊢ ∃ c ∈ Icc a b, cluster_point u c
Tactic:
rcases (isCompact_Icc : IsCompact (Icc a b)).tendsto_subseq h with ⟨c, c_in, φ, hφ, lim⟩
Proof state after:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : Tendsto ((fun n => u n) ∘ φ) atTop (nhds c)
⊢ ∃ c ∈ Icc a b, cluster_point u c
Theorem: bolzano_weierstrass
Proof state before:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : Tendsto ((fun n => u n) ∘ φ) atTop (nhds c)
⊢ ∃ c ∈ Icc a b, cluster_point u c
Tactic:
refine ⟨c, c_in, φ, hφ, ?_⟩
Proof state after:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : Tendsto ((fun n => u n) ∘ φ) atTop (nhds c)
⊢ seq_limit (u ∘ φ) c
Theorem: bolzano_weierstrass
Proof state before:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : Tendsto ((fun n => u n) ∘ φ) atTop (nhds c)
⊢ seq_limit (u ∘ φ) c
Tactic:
simp_rw [Metric.tendsto_nhds, eventually_atTop, Real.dist_eq] at lim
Proof state after:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
⊢ seq_limit (u ∘ φ) c
Theorem: bolzano_weierstrass
Proof state before:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
⊢ seq_limit (u ∘ φ) c
Tactic:
intros ε ε_pos
Proof state after:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - c| ≤ ε
Theorem: bolzano_weierstrass
Proof state before:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - c| ≤ ε
Tactic:
rcases lim ε ε_pos with ⟨N, hN⟩
Proof state after:
case intro.intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ b ≥ N, |((fun n => u n) ∘ φ) b - c| < ε
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - c| ≤ ε
Theorem: bolzano_weierstrass
Proof state before:
case intro.intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ b ≥ N, |((fun n => u n) ∘ φ) b - c| < ε
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - c| ≤ ε
Tactic:
use N
Proof state after:
case h
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ b ≥ N, |((fun n => u n) ∘ φ) b - c| < ε
⊢ ∀ n ≥ N, |(u ∘ φ) n - c| ≤ ε
Theorem: bolzano_weierstrass
Proof state before:
case h
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ b ≥ N, |((fun n => u n) ∘ φ) b - c| < ε
⊢ ∀ n ≥ N, |(u ∘ φ) n - c| ≤ ε
Tactic:
intros n hn
Proof state after:
case h
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ b ≥ N, |((fun n => u n) ∘ φ) b - c| < ε
n : ℕ
hn : n ≥ N
⊢ |(u ∘ φ) n - c| ≤ ε
Theorem: bolzano_weierstrass
Proof state before:
case h
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ b ≥ N, |((fun n => u n) ∘ φ) b - c| < ε
n : ℕ
hn : n ≥ N
⊢ |(u ∘ φ) n - c| ≤ ε
Tactic:
exact le_of_lt (hN n hn)
Proof state after:
no goals
Theorem: not_seq_limit_of_tendstoinfinity
Proof state before:
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
⊢ tendsto_infinity u → ∀ (x : ℝ), ¬seq_limit u x
Tactic:
intros lim_infinie x lim_x
Proof state after:
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
⊢ False
Theorem: not_seq_limit_of_tendstoinfinity
Proof state before:
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
⊢ False
Tactic:
cases' lim_x 1 (by linarith) with N hN
Proof state after:
case intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ 1
⊢ False
Theorem: not_seq_limit_of_tendstoinfinity
Proof state before:
case intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ 1
⊢ False
Tactic:
cases' lim_infinie (x+2) with N' hN'
Proof state after:
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ 1
N' : ℕ
hN' : ∀ n ≥ N', u n ≥ x + 2
⊢ False
Theorem: not_seq_limit_of_tendstoinfinity
Proof state before:
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ 1
N' : ℕ
hN' : ∀ n ≥ N', u n ≥ x + 2
⊢ False
Tactic:
let N₀ := max N N'
Proof state after:
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ 1
N' : ℕ
hN' : ∀ n ≥ N', u n ≥ x + 2
N₀ : ℕ := max N N'
⊢ False
Theorem: not_seq_limit_of_tendstoinfinity
Proof state before:
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ 1
N' : ℕ
hN' : ∀ n ≥ N', u n ≥ x + 2
N₀ : ℕ := max N N'
⊢ False
Tactic:
specialize hN N₀ (le_max_left _ _)
Proof state after:
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N N' : ℕ
hN' : ∀ n ≥ N', u n ≥ x + 2
N₀ : ℕ := max N N'
hN : |u N₀ - x| ≤ 1
⊢ False
Theorem: not_seq_limit_of_tendstoinfinity
Proof state before:
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N N' : ℕ
hN' : ∀ n ≥ N', u n ≥ x + 2
N₀ : ℕ := max N N'
hN : |u N₀ - x| ≤ 1
⊢ False
Tactic:
specialize hN' N₀ (le_max_right _ _)
Proof state after:
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - x| ≤ 1
hN' : u N₀ ≥ x + 2
⊢ False
Theorem: not_seq_limit_of_tendstoinfinity
Proof state before:
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - x| ≤ 1
hN' : u N₀ ≥ x + 2
⊢ False
Tactic:
rw [abs_le] at hN
Proof state after:
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N N' : ℕ
N₀ : ℕ := max N N'
hN : -1 ≤ u N₀ - x ∧ u N₀ - x ≤ 1
hN' : u N₀ ≥ x + 2
⊢ False
Theorem: not_seq_limit_of_tendstoinfinity
Proof state before:
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N N' : ℕ
N₀ : ℕ := max N N'
hN : -1 ≤ u N₀ - x ∧ u N₀ - x ≤ 1
hN' : u N₀ ≥ x + 2
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: not_seq_limit_of_tendstoinfinity
Proof state before:
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
⊢ 1 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: sup_segment
Proof state before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
⊢ ∃ x ∈ Icc a b, is_sup A x
Tactic:
have b_maj :  ∀ (y : ℝ), y ∈ A → y ≤ b := fun y y_in ↦ (h y_in).2
Proof state after:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
⊢ ∃ x ∈ Icc a b, is_sup A x
Theorem: sup_segment
Proof state before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
⊢ ∃ x ∈ Icc a b, is_sup A x
Tactic:
have Sup_maj : upper_bound A (sSup A) := by
  intro x
  apply le_csSup
  exact ⟨b, b_maj⟩
Proof state after:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ ∃ x ∈ Icc a b, is_sup A x
Theorem: sup_segment
Proof state before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ ∃ x ∈ Icc a b, is_sup A x
Tactic:
refine ⟨sSup A, ?_, ?_⟩
Proof state after:
case refine_1
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ sSup A ∈ Icc a b

case refine_2
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ is_sup A (sSup A)
Theorem: sup_segment
Proof state before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
⊢ upper_bound A (sSup A)
Tactic:
intro x
Proof state after:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
x : ℝ
⊢ x ∈ A → x ≤ sSup A
Theorem: sup_segment
Proof state before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
x : ℝ
⊢ x ∈ A → x ≤ sSup A
Tactic:
apply le_csSup
Proof state after:
case h₁
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
x : ℝ
⊢ BddAbove A
Theorem: sup_segment
Proof state before:
case h₁
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
x : ℝ
⊢ BddAbove A
Tactic:
exact ⟨b, b_maj⟩
Proof state after:
no goals
Theorem: sup_segment
Proof state before:
case refine_1
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ sSup A ∈ Icc a b
Tactic:
constructor
Proof state after:
case refine_1.left
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ a ≤ sSup A

case refine_1.right
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ sSup A ≤ b
Theorem: sup_segment
Proof state before:
case refine_1.left
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ a ≤ sSup A
Tactic:
cases' hnonvide with x x_in
Proof state after:
case refine_1.left.intro
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
x : ℝ
x_in : x ∈ A
⊢ a ≤ sSup A
Theorem: sup_segment
Proof state before:
case refine_1.left.intro
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
x : ℝ
x_in : x ∈ A
⊢ a ≤ sSup A
Tactic:
exact le_trans (h x_in).1 (Sup_maj _ x_in)
Proof state after:
no goals
Theorem: sup_segment
Proof state before:
case refine_1.right
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ sSup A ≤ b
Tactic:
apply csSup_le hnonvide b_maj
Proof state after:
no goals
Theorem: sup_segment
Proof state before:
case refine_2
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ is_sup A (sSup A)
Tactic:
exact ⟨Sup_maj, fun y ↦ csSup_le hnonvide⟩
Proof state after:
no goals
Theorem: subseq_tendsto_of_tendsto
Proof state before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
⊢ seq_limit (u ∘ φ) l
Tactic:
intros ε ε_pos
Proof state after:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Theorem: subseq_tendsto_of_tendsto
Proof state before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Tactic:
cases' h ε ε_pos with N hN
Proof state after:
case intro
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Theorem: subseq_tendsto_of_tendsto
Proof state before:
case intro
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Tactic:
use N
Proof state after:
case h
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Theorem: subseq_tendsto_of_tendsto
Proof state before:
case h
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Tactic:
intros n hn
Proof state after:
case h
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ |(u ∘ φ) n - l| ≤ ε
Theorem: subseq_tendsto_of_tendsto
Proof state before:
case h
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ |(u ∘ φ) n - l| ≤ ε
Tactic:
apply hN
Proof state after:
case h.a
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ φ n ≥ N
Theorem: subseq_tendsto_of_tendsto
Proof state before:
case h.a
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ φ n ≥ N
Tactic:
calc N ≤ n := hn
_ ≤ φ n := id_le_extraction hφ n
Proof state after:
no goals
Theorem: L1
Proof state before:
P Q R : Prop
h1 : Q → P
h2 : R → P
h3 : Q ∨ R
⊢ P
Tactic:
sorry
Proof state after:
no goals
Theorem: L2
Proof state before:
P Q : Prop
h : ¬Q ↔ P
⊢ (¬P → Q) ∧ (P → ¬Q)
Tactic:
sorry
Proof state after:
no goals
Theorem: L3
Proof state before:
P Q R : Prop
h : P ∨ R ∨ Q → ¬(R ∧ Q ∧ P)
⊢ R ∨ Q ∨ P → ¬((P ∧ Q) ∧ R)
Tactic:
sorry
Proof state after:
no goals
Theorem: N.add_zero'
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n✝ m n : N
⊢ n + zero = n
Tactic:
rfl
Proof state after:
no goals
Theorem: N.zero_add
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ 0 + a = a
Tactic:
induction a with
| zero =>
  rfl
| succ i hi =>
  rw [add_succ, hi]
Proof state after:
no goals