internlm/Lean-Github huggingface dataset:
Theorem: sb_surjective
Proof state before:
case pos.intro
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
n : ℕ
hn : g y ∈ sb_aux f g n
⊢ ∃ a, h a = y
Tactic:
cases n with
| zero =>
  simp [sb_aux] at hn
| succ n =>
  simp [sb_aux] at hn
  rcases hn with ⟨x, xmem, hx⟩
  use x
  have : x ∈ A := by
    rw [A_def, sb_set, mem_iUnion]
    exact ⟨n, xmem⟩
  simp only [h_def, sb_fun, if_pos this]
  exact hg hx
Proof state after:
no goals
Theorem: sb_surjective
Proof state before:
case pos.intro.zero
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
hn : g y ∈ sb_aux f g Nat.zero
⊢ ∃ a, h a = y
Tactic:
simp [sb_aux] at hn
Proof state after:
no goals
Theorem: sb_surjective
Proof state before:
case pos.intro.succ
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
n : ℕ
hn : g y ∈ sb_aux f g (Nat.succ n)
⊢ ∃ a, h a = y
Tactic:
simp [sb_aux] at hn
Proof state after:
case pos.intro.succ
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
n : ℕ
hn : ∃ a ∈ sb_aux f g n, g (f a) = g y
⊢ ∃ a, h a = y
Theorem: sb_surjective
Proof state before:
case pos.intro.succ
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
n : ℕ
hn : ∃ a ∈ sb_aux f g n, g (f a) = g y
⊢ ∃ a, h a = y
Tactic:
rcases hn with ⟨x, xmem, hx⟩
Proof state after:
case pos.intro.succ.intro.intro
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
⊢ ∃ a, h a = y
Theorem: sb_surjective
Proof state before:
case pos.intro.succ.intro.intro
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
⊢ ∃ a, h a = y
Tactic:
use x
Proof state after:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
⊢ h x = y
Theorem: sb_surjective
Proof state before:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
⊢ h x = y
Tactic:
have : x ∈ A := by
  rw [A_def, sb_set, mem_iUnion]
  exact ⟨n, xmem⟩
Proof state after:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
this : x ∈ A
⊢ h x = y
Theorem: sb_surjective
Proof state before:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
this : x ∈ A
⊢ h x = y
Tactic:
simp only [h_def, sb_fun, if_pos this]
Proof state after:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
this : x ∈ A
⊢ f x = y
Theorem: sb_surjective
Proof state before:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
this : x ∈ A
⊢ f x = y
Tactic:
exact hg hx
Proof state after:
no goals
Theorem: sb_surjective
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
⊢ x ∈ A
Tactic:
rw [A_def, sb_set, mem_iUnion]
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
⊢ ∃ i, x ∈ sb_aux f g i
Theorem: sb_surjective
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
⊢ ∃ i, x ∈ sb_aux f g i
Tactic:
exact ⟨n, xmem⟩
Proof state after:
no goals
Theorem: sb_surjective
Proof state before:
case neg
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
gyA : g y ∉ A
⊢ ∃ a, h a = y
Tactic:
use g y
Proof state after:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
gyA : g y ∉ A
⊢ h (g y) = y
Theorem: sb_surjective
Proof state before:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
gyA : g y ∉ A
⊢ h (g y) = y
Tactic:
simp [sb_fun, gyA]
Proof state after:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
gyA : g y ∉ A
⊢ invFun g (g y) = y
Theorem: sb_surjective
Proof state before:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
gyA : g y ∉ A
⊢ invFun g (g y) = y
Tactic:
apply hg
Proof state after:
case h.a
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
gyA : g y ∉ A
⊢ g (invFun g (g y)) = g y
Theorem: sb_surjective
Proof state before:
case h.a
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
y : β
gyA : g y ∉ A
⊢ g (invFun g (g y)) = g y
Tactic:
exact apply_invFun_apply
Proof state after:
no goals
Theorem: eq_of_abs_sub_le_all
Proof state before:
case h
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
⊢ |x - y| ≤ 0
Tactic:
by_contra! H
Proof state after:
case h
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
H : 0 < |x - y|
⊢ False
Theorem: eq_of_abs_sub_le_all
Proof state before:
case h
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
H : 0 < |x - y|
⊢ False
Tactic:
specialize h ( |x-y|/2) (by linarith)
Proof state after:
case h
x y : ℝ
H : 0 < |x - y|
h : |x - y| ≤ |x - y| / 2
⊢ False
Theorem: eq_of_abs_sub_le_all
Proof state before:
case h
x y : ℝ
H : 0 < |x - y|
h : |x - y| ≤ |x - y| / 2
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: unique_limit
Proof state before:
case a
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
⊢ |l - l'| ≤ ε
Tactic:
specialize hl (ε/2) (by linarith)
Proof state after:
case a
u : ℕ → ℝ
l l' : ℝ
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
hl : ∃ N, ∀ n ≥ N, |u n - l| ≤ ε / 2
⊢ |l - l'| ≤ ε
Theorem: unique_limit
Proof state before:
case a
u : ℕ → ℝ
l l' : ℝ
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
hl : ∃ N, ∀ n ≥ N, |u n - l| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
cases' hl with N hN
Proof state after:
case a.intro
u : ℕ → ℝ
l l' : ℝ
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
⊢ |l - l'| ≤ ε
Theorem: unique_limit
Proof state before:
case a.intro
u : ℕ → ℝ
l l' : ℝ
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
specialize hl' (ε/2) (by linarith)
Proof state after:
case a.intro
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
hl' : ∃ N, ∀ n ≥ N, |u n - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
Theorem: unique_limit
Proof state before:
case a.intro
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
hl' : ∃ N, ∀ n ≥ N, |u n - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
cases' hl' with N' hN'
Proof state after:
case a.intro.intro
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
Theorem: unique_limit
Proof state before:
case a.intro.intro
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
specialize hN (max N N') (le_max_left _ _)
Proof state after:
case a.intro.intro
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
hN : |u (max N N') - l| ≤ ε / 2
⊢ |l - l'| ≤ ε
Theorem: unique_limit
Proof state before:
case a.intro.intro
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
hN : |u (max N N') - l| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
specialize hN' (max N N') (le_max_right _ _)
Proof state after:
case a.intro.intro
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
Theorem: unique_limit
Proof state before:
case a.intro.intro
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
calc |l - l'| = |(l-u (max N N')) + (u (max N N') -l')| := by ring_nf
_ ≤ |l - u (max N N')| + |u (max N N') - l'| := by apply abs_add
_ = |u (max N N') - l| + |u (max N N') - l'| := by rw [abs_sub_comm]
_ ≤ ε/2 + ε/2 := by linarith
_ = ε := by ring
Proof state after:
no goals
Theorem: unique_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
⊢ ε / 2 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: unique_limit
Proof state before:
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - l'| = |l - u (max N N') + (u (max N N') - l')|
Tactic:
ring_nf
Proof state after:
no goals
Theorem: unique_limit
Proof state before:
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - u (max N N') + (u (max N N') - l')| ≤ |l - u (max N N')| + |u (max N N') - l'|
Tactic:
apply abs_add
Proof state after:
no goals
Theorem: unique_limit
Proof state before:
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - u (max N N')| + |u (max N N') - l'| = |u (max N N') - l| + |u (max N N') - l'|
Tactic:
rw [abs_sub_comm]
Proof state after:
no goals
Theorem: unique_limit
Proof state before:
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |u (max N N') - l| + |u (max N N') - l'| ≤ ε / 2 + ε / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: unique_limit
Proof state before:
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ ε / 2 + ε / 2 = ε
Tactic:
ring
Proof state after:
no goals
Theorem: le_of_le_add_all
Proof state before:
x y : ℝ
⊢ (∀ ε > 0, y ≤ x + ε) → y ≤ x
Tactic:
contrapose!
Proof state after:
x y : ℝ
⊢ x < y → ∃ ε > 0, x + ε < y
Theorem: le_of_le_add_all
Proof state before:
x y : ℝ
⊢ x < y → ∃ ε > 0, x + ε < y
Tactic:
intro h
Proof state after:
x y : ℝ
h : x < y
⊢ ∃ ε > 0, x + ε < y
Theorem: le_of_le_add_all
Proof state before:
x y : ℝ
h : x < y
⊢ ∃ ε > 0, x + ε < y
Tactic:
use (y-x)/2
Proof state after:
case h
x y : ℝ
h : x < y
⊢ (y - x) / 2 > 0 ∧ x + (y - x) / 2 < y
Theorem: le_of_le_add_all
Proof state before:
case h
x y : ℝ
h : x < y
⊢ (y - x) / 2 > 0 ∧ x + (y - x) / 2 < y
Tactic:
constructor <;> linarith
Proof state after:
no goals
Theorem: lt_sup
Proof state before:
A : Set ℝ
x : ℝ
hx : is_sup A x
⊢ ∀ y < x, ∃ a ∈ A, y < a
Tactic:
intro y
Proof state after:
A : Set ℝ
x : ℝ
hx : is_sup A x
y : ℝ
⊢ y < x → ∃ a ∈ A, y < a
Theorem: lt_sup
Proof state before:
A : Set ℝ
x : ℝ
hx : is_sup A x
y : ℝ
⊢ y < x → ∃ a ∈ A, y < a
Tactic:
contrapose!
Proof state after:
A : Set ℝ
x : ℝ
hx : is_sup A x
y : ℝ
⊢ (∀ a ∈ A, a ≤ y) → x ≤ y
Theorem: lt_sup
Proof state before:
A : Set ℝ
x : ℝ
hx : is_sup A x
y : ℝ
⊢ (∀ a ∈ A, a ≤ y) → x ≤ y
Tactic:
exact hx.right y
Proof state after:
no goals
Theorem: squeeze
Proof state before:
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
⊢ seq_limit v l
Tactic:
intros ε ε_pos
Proof state after:
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |v n - l| ≤ ε
Theorem: squeeze
Proof state before:
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |v n - l| ≤ ε
Tactic:
cases' hu ε ε_pos with N hN
Proof state after:
case intro
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∃ N, ∀ n ≥ N, |v n - l| ≤ ε
Theorem: squeeze
Proof state before:
case intro
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∃ N, ∀ n ≥ N, |v n - l| ≤ ε
Tactic:
cases' hw ε ε_pos with N' hN'
Proof state after:
case intro.intro
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
⊢ ∃ N, ∀ n ≥ N, |v n - l| ≤ ε
Theorem: squeeze
Proof state before:
case intro.intro
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
⊢ ∃ N, ∀ n ≥ N, |v n - l| ≤ ε
Tactic:
use max N N'
Proof state after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
⊢ ∀ n ≥ max N N', |v n - l| ≤ ε
Theorem: squeeze
Proof state before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
⊢ ∀ n ≥ max N N', |v n - l| ≤ ε
Tactic:
intros n hn
Proof state after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ max N N'
⊢ |v n - l| ≤ ε
Theorem: squeeze
Proof state before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ max N N'
⊢ |v n - l| ≤ ε
Tactic:
rw [ge_max_iff] at hn
Proof state after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ N ∧ n ≥ N'
⊢ |v n - l| ≤ ε
Theorem: squeeze
Proof state before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ N ∧ n ≥ N'
⊢ |v n - l| ≤ ε
Tactic:
specialize hN n (by linarith)
Proof state after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
⊢ |v n - l| ≤ ε
Theorem: squeeze
Proof state before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
⊢ |v n - l| ≤ ε
Tactic:
specialize hN' n (by linarith)
Proof state after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
hN' : |w n - l| ≤ ε
⊢ |v n - l| ≤ ε
Theorem: squeeze
Proof state before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
hN' : |w n - l| ≤ ε
⊢ |v n - l| ≤ ε
Tactic:
specialize h n
Proof state after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
hN' : |w n - l| ≤ ε
h : u n ≤ v n
⊢ |v n - l| ≤ ε
Theorem: squeeze
Proof state before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
hN' : |w n - l| ≤ ε
h : u n ≤ v n
⊢ |v n - l| ≤ ε
Tactic:
specialize h' n
Proof state after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
hN' : |w n - l| ≤ ε
h : u n ≤ v n
h' : v n ≤ w n
⊢ |v n - l| ≤ ε
Theorem: squeeze
Proof state before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
hN' : |w n - l| ≤ ε
h : u n ≤ v n
h' : v n ≤ w n
⊢ |v n - l| ≤ ε
Tactic:
rw [abs_le] at *
Proof state after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : -ε ≤ u n - l ∧ u n - l ≤ ε
hN' : -ε ≤ w n - l ∧ w n - l ≤ ε
h : u n ≤ v n
h' : v n ≤ w n
⊢ -ε ≤ v n - l ∧ v n - l ≤ ε
Theorem: squeeze
Proof state before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : -ε ≤ u n - l ∧ u n - l ≤ ε
hN' : -ε ≤ w n - l ∧ w n - l ≤ ε
h : u n ≤ v n
h' : v n ≤ w n
⊢ -ε ≤ v n - l ∧ v n - l ≤ ε
Tactic:
constructor <;> linarith
Proof state after:
no goals
Theorem: squeeze
Proof state before:
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ N ∧ n ≥ N'
⊢ n ≥ N
Tactic:
linarith
Proof state after:
no goals
Theorem: squeeze
Proof state before:
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
⊢ n ≥ N'
Tactic:
linarith
Proof state after:
no goals
Theorem: lim_le
Proof state before:
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
⊢ x ≤ y
Tactic:
apply le_of_le_add_all
Proof state after:
case a
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
⊢ ∀ ε > 0, x ≤ y + ε
Theorem: lim_le
Proof state before:
case a
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
⊢ ∀ ε > 0, x ≤ y + ε
Tactic:
intros ε ε_pos
Proof state after:
case a
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
ε : ℝ
ε_pos : ε > 0
⊢ x ≤ y + ε
Theorem: lim_le
Proof state before:
case a
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
ε : ℝ
ε_pos : ε > 0
⊢ x ≤ y + ε
Tactic:
cases' hu ε ε_pos with N hN
Proof state after:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ ε
⊢ x ≤ y + ε
Theorem: lim_le
Proof state before:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ ε
⊢ x ≤ y + ε
Tactic:
specialize hN N (by linarith)
Proof state after:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : |u N - x| ≤ ε
⊢ x ≤ y + ε
Theorem: lim_le
Proof state before:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : |u N - x| ≤ ε
⊢ x ≤ y + ε
Tactic:
specialize ineg N
Proof state after:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : |u N - x| ≤ ε
ineg : u N ≤ y
⊢ x ≤ y + ε
Theorem: lim_le
Proof state before:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : |u N - x| ≤ ε
ineg : u N ≤ y
⊢ x ≤ y + ε
Tactic:
rw [abs_le] at hN
Proof state after:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : -ε ≤ u N - x ∧ u N - x ≤ ε
ineg : u N ≤ y
⊢ x ≤ y + ε
Theorem: lim_le
Proof state before:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : -ε ≤ u N - x ∧ u N - x ≤ ε
ineg : u N ≤ y
⊢ x ≤ y + ε
Tactic:
linarith
Proof state after:
no goals
Theorem: lim_le
Proof state before:
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ ε
⊢ N ≥ N
Tactic:
linarith
Proof state after:
no goals
Theorem: inv_succ_le_all
Proof state before:
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
Tactic:
intro ε hε
Proof state after:
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, 1 / (↑n + 1) ≤ ε