internlm/Lean-Github huggingface dataset:
Theorem: Section2sheet5.tendsTo_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
n : ℕ
hn : X ≤ n ∧ Y ≤ n
hX : |a n - t| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Tactic:
specialize hY n hn.2
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X Y n : ℕ
hn : X ≤ n ∧ Y ≤ n
hX : |a n - t| < ε / 2
hY : |b n - u| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Theorem: Section2sheet5.tendsTo_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X Y n : ℕ
hn : X ≤ n ∧ Y ≤ n
hX : |a n - t| < ε / 2
hY : |b n - u| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Tactic:
rw [abs_lt] at *
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X Y n : ℕ
hn : X ≤ n ∧ Y ≤ n
hX : -(ε / 2) < a n - t ∧ a n - t < ε / 2
hY : -(ε / 2) < b n - u ∧ b n - u < ε / 2
⊢ -ε < a n + b n - (t + u) ∧ a n + b n - (t + u) < ε
Theorem: Section2sheet5.tendsTo_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X Y n : ℕ
hn : X ≤ n ∧ Y ≤ n
hX : -(ε / 2) < a n - t ∧ a n - t < ε / 2
hY : -(ε / 2) < b n - u ∧ b n - u < ε / 2
⊢ -ε < a n + b n - (t + u) ∧ a n + b n - (t + u) < ε
Tactic:
constructor <;>linarith
Proof state after:
no goals
Theorem: Section2sheet5.tendsTo_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
⊢ 0 < ε / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Section2sheet5.tendsTo_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
⊢ 0 < ε / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Section2sheet5.tendsTo_sub
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo a t
hb : TendsTo b u
⊢ TendsTo (fun n => a n - b n) (t - u)
Tactic:
sorry
Proof state after:
no goals
Theorem: Section15Sheet3.infinite_setOf_solutions
Proof state before:
⊢ Set.Infinite {n | 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1}
Tactic:
rw [infinite_iff_arb_large]
Proof state after:
⊢ ∀ (N : ℕ), ∃ n > N, n ∈ {n | 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1}
Theorem: Section15Sheet3.infinite_setOf_solutions
Proof state before:
⊢ ∀ (N : ℕ), ∃ n > N, n ∈ {n | 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1}
Tactic:
exact arb_large_soln
Proof state after:
no goals
Theorem: Section10sheet1Solutions.Real.isOpen_univ
Proof state before:
X : Type
⊢ IsOpen Set.univ
Tactic:
intro x hx
Proof state after:
X : Type
x : ℝ
hx : x ∈ Set.univ
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ Set.univ
Theorem: Section10sheet1Solutions.Real.isOpen_univ
Proof state before:
X : Type
x : ℝ
hx : x ∈ Set.univ
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ Set.univ
Tactic:
use 37
Proof state after:
case h
X : Type
x : ℝ
hx : x ∈ Set.univ
⊢ 37 > 0 ∧ ∀ (y : ℝ), x - 37 < y ∧ y < x + 37 → y ∈ Set.univ
Theorem: Section10sheet1Solutions.Real.isOpen_univ
Proof state before:
case h
X : Type
x : ℝ
hx : x ∈ Set.univ
⊢ 37 > 0 ∧ ∀ (y : ℝ), x - 37 < y ∧ y < x + 37 → y ∈ Set.univ
Tactic:
norm_num
Proof state after:
no goals
Theorem: Section10sheet1Solutions.Real.isOpen_inter
Proof state before:
X : Type
s t : Set ℝ
hs : IsOpen s
ht : IsOpen t
⊢ IsOpen (s ∩ t)
Tactic:
intro x hx
Proof state after:
X : Type
s t : Set ℝ
hs : IsOpen s
ht : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ s ∩ t
Theorem: Section10sheet1Solutions.Real.isOpen_inter
Proof state before:
X : Type
s t : Set ℝ
hs : IsOpen s
ht : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ s ∩ t
Tactic:
obtain ⟨δs, δspos, hs⟩ := hs x (by aesop)
Proof state after:
case intro.intro
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ s ∩ t
Theorem: Section10sheet1Solutions.Real.isOpen_inter
Proof state before:
case intro.intro
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ s ∩ t
Tactic:
obtain ⟨δt, δtpos, ht⟩ := ht x (by aesop)
Proof state after:
case intro.intro.intro.intro
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ s ∩ t
Theorem: Section10sheet1Solutions.Real.isOpen_inter
Proof state before:
case intro.intro.intro.intro
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ s ∩ t
Tactic:
use min δs δt, by positivity
Proof state after:
case right
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
⊢ ∀ (y : ℝ), x - min δs δt < y ∧ y < x + min δs δt → y ∈ s ∩ t
Theorem: Section10sheet1Solutions.Real.isOpen_inter
Proof state before:
case right
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
⊢ ∀ (y : ℝ), x - min δs δt < y ∧ y < x + min δs δt → y ∈ s ∩ t
Tactic:
rintro y ⟨h1, h2⟩
Proof state after:
case right.intro
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ y ∈ s ∩ t
Theorem: Section10sheet1Solutions.Real.isOpen_inter
Proof state before:
case right.intro
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ y ∈ s ∩ t
Tactic:
constructor
Proof state after:
case right.intro.left
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ y ∈ s

case right.intro.right
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ y ∈ t
Theorem: Section10sheet1Solutions.Real.isOpen_inter
Proof state before:
X : Type
s t : Set ℝ
hs : IsOpen s
ht : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
⊢ x ∈ s
Tactic:
aesop
Proof state after:
no goals
Theorem: Section10sheet1Solutions.Real.isOpen_inter
Proof state before:
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
⊢ x ∈ t
Tactic:
aesop
Proof state after:
no goals
Theorem: Section10sheet1Solutions.Real.isOpen_inter
Proof state before:
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
⊢ min δs δt > 0
Tactic:
positivity
Proof state after:
no goals
Theorem: Section10sheet1Solutions.Real.isOpen_inter
Proof state before:
case right.intro.left
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ y ∈ s
Tactic:
apply hs
Proof state after:
case right.intro.left.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ x - δs < y ∧ y < x + δs
Theorem: Section10sheet1Solutions.Real.isOpen_inter
Proof state before:
case right.intro.left.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ x - δs < y ∧ y < x + δs
Tactic:
have foo : min δs δt ≤ δs := min_le_left δs δt
Proof state after:
case right.intro.left.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
foo : min δs δt ≤ δs
⊢ x - δs < y ∧ y < x + δs
Theorem: Section10sheet1Solutions.Real.isOpen_inter
Proof state before:
case right.intro.left.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
foo : min δs δt ≤ δs
⊢ x - δs < y ∧ y < x + δs
Tactic:
constructor <;> linarith
Proof state after:
no goals
Theorem: Section10sheet1Solutions.Real.isOpen_inter
Proof state before:
case right.intro.right
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ y ∈ t
Tactic:
apply ht
Proof state after:
case right.intro.right.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ x - δt < y ∧ y < x + δt
Theorem: Section10sheet1Solutions.Real.isOpen_inter
Proof state before:
case right.intro.right.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ x - δt < y ∧ y < x + δt
Tactic:
have foo : min δs δt ≤ δt := min_le_right δs δt
Proof state after:
case right.intro.right.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
foo : min δs δt ≤ δt
⊢ x - δt < y ∧ y < x + δt
Theorem: Section10sheet1Solutions.Real.isOpen_inter
Proof state before:
case right.intro.right.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
foo : min δs δt ≤ δt
⊢ x - δt < y ∧ y < x + δt
Tactic:
constructor <;> linarith
Proof state after:
no goals
Theorem: Section10sheet1Solutions.Real.isOpen_sUnion
Proof state before:
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
⊢ IsOpen (⋃₀ F)
Tactic:
intro x hx
Proof state after:
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
hx : x ∈ ⋃₀ F
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ ⋃₀ F
Theorem: Section10sheet1Solutions.Real.isOpen_sUnion
Proof state before:
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
hx : x ∈ ⋃₀ F
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ ⋃₀ F
Tactic:
simp_rw [Set.mem_sUnion] at hx ⊢
Proof state after:
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
hx : ∃ t ∈ F, x ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t
Theorem: Section10sheet1Solutions.Real.isOpen_sUnion
Proof state before:
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
hx : ∃ t ∈ F, x ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t
Tactic:
rcases hx with ⟨t, htF, hxt⟩
Proof state after:
case intro.intro
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t
Theorem: Section10sheet1Solutions.Real.isOpen_sUnion
Proof state before:
case intro.intro
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t
Tactic:
obtain ⟨δ, hδpos, h⟩ := hF t htF x hxt
Proof state after:
case intro.intro.intro.intro
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
δ : ℝ
hδpos : δ > 0
h : ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t
Theorem: Section10sheet1Solutions.Real.isOpen_sUnion
Proof state before:
case intro.intro.intro.intro
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
δ : ℝ
hδpos : δ > 0
h : ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t
Tactic:
use δ, hδpos
Proof state after:
case right
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
δ : ℝ
hδpos : δ > 0
h : ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ t
⊢ ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t
Theorem: Section10sheet1Solutions.Real.isOpen_sUnion
Proof state before:
case right
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
δ : ℝ
hδpos : δ > 0
h : ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ t
⊢ ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t
Tactic:
peel h with h1 y hyt
Proof state after:
case right.h.h
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
δ : ℝ
hδpos : δ > 0
h : ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ t
y : ℝ
hyt : x - δ < y ∧ y < x + δ
h1 : y ∈ t
⊢ ∃ t ∈ F, y ∈ t
Theorem: Section10sheet1Solutions.Real.isOpen_sUnion
Proof state before:
case right.h.h
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
δ : ℝ
hδpos : δ > 0
h : ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ t
y : ℝ
hyt : x - δ < y ∧ y < x + δ
h1 : y ∈ t
⊢ ∃ t ∈ F, y ∈ t
Tactic:
use t, htF
Proof state after:
no goals
Theorem: Section2sheet3.tendsTo_def
Proof state before:
a : ℕ → ℝ
t : ℝ
⊢ TendsTo a t ↔ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
Tactic:
rfl
Proof state after:
no goals
Theorem: Section2sheet3.tendsTo_thirtyseven
Proof state before:
⊢ TendsTo (fun n => 37) 37
Tactic:
rw [tendsTo_def]
Proof state after:
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |37 - 37| < ε
Theorem: Section2sheet3.tendsTo_thirtyseven
Proof state before:
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |37 - 37| < ε
Tactic:
intro ε hε
Proof state after:
ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 - 37| < ε
Theorem: Section2sheet3.tendsTo_thirtyseven
Proof state before:
ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 - 37| < ε
Tactic:
use 100
Proof state after:
case h
ε : ℝ
hε : 0 < ε
⊢ ∀ (n : ℕ), 100 ≤ n → |37 - 37| < ε
Theorem: Section2sheet3.tendsTo_thirtyseven
Proof state before:
case h
ε : ℝ
hε : 0 < ε
⊢ ∀ (n : ℕ), 100 ≤ n → |37 - 37| < ε
Tactic:
intro n hn
Proof state after:
case h
ε : ℝ
hε : 0 < ε
n : ℕ
hn : 100 ≤ n
⊢ |37 - 37| < ε
Theorem: Section2sheet3.tendsTo_thirtyseven
Proof state before:
case h
ε : ℝ
hε : 0 < ε
n : ℕ
hn : 100 ≤ n
⊢ |37 - 37| < ε
Tactic:
norm_num
Proof state after:
case h
ε : ℝ
hε : 0 < ε
n : ℕ
hn : 100 ≤ n
⊢ 0 < ε
Theorem: Section2sheet3.tendsTo_thirtyseven
Proof state before:
case h
ε : ℝ
hε : 0 < ε
n : ℕ
hn : 100 ≤ n
⊢ 0 < ε
Tactic:
exact hε
Proof state after:
no goals
Theorem: Section2sheet3.tendsTo_const
Proof state before:
c : ℝ
⊢ TendsTo (fun n => c) c
Tactic:
intro ε hε
Proof state after:
c ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c) n - c| < ε
Theorem: Section2sheet3.tendsTo_const
Proof state before:
c ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c) n - c| < ε
Tactic:
dsimp only
Proof state after:
c ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |c - c| < ε
Theorem: Section2sheet3.tendsTo_const
Proof state before:
c ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |c - c| < ε
Tactic:
use 37
Proof state after:
case h
c ε : ℝ
hε : ε > 0
⊢ ∀ (n : ℕ), 37 ≤ n → |c - c| < ε
Theorem: Section2sheet3.tendsTo_const
Proof state before:
case h
c ε : ℝ
hε : ε > 0
⊢ ∀ (n : ℕ), 37 ≤ n → |c - c| < ε
Tactic:
intro n hn
Proof state after:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ |c - c| < ε
Theorem: Section2sheet3.tendsTo_const
Proof state before:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ |c - c| < ε
Tactic:
ring_nf
Proof state after:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ |0| < ε
Theorem: Section2sheet3.tendsTo_const
Proof state before:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ |0| < ε
Tactic:
norm_num
Proof state after:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ 0 < ε
Theorem: Section2sheet3.tendsTo_const
Proof state before:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ 0 < ε
Tactic:
exact hε
Proof state after:
no goals
Theorem: Section2sheet3.tendsTo_add_const
Proof state before:
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => a n + c) (t + c)
Tactic:
sorry
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_thirtyseven_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => 37 * a n) (37 * t)
Tactic:
intro ε hε
Proof state after:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => 37 * a n) n - 37 * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_thirtyseven_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => 37 * a n) n - 37 * t| < ε
Tactic:
obtain ⟨X, hX⟩ := h (ε / 37) (by linarith)
Proof state after:
case intro
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 37
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => 37 * a n) n - 37 * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_thirtyseven_mul
Proof state before:
case intro
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 37
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => 37 * a n) n - 37 * t| < ε
Tactic:
use X
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 37
⊢ ∀ (n : ℕ), X ≤ n → |(fun n => 37 * a n) n - 37 * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_thirtyseven_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 37
⊢ ∀ (n : ℕ), X ≤ n → |(fun n => 37 * a n) n - 37 * t| < ε
Tactic:
intro n hn
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 37
n : ℕ
hn : X ≤ n
⊢ |(fun n => 37 * a n) n - 37 * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_thirtyseven_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 37
n : ℕ
hn : X ≤ n
⊢ |(fun n => 37 * a n) n - 37 * t| < ε
Tactic:
specialize hX n hn
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / 37
⊢ |(fun n => 37 * a n) n - 37 * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_thirtyseven_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / 37
⊢ |(fun n => 37 * a n) n - 37 * t| < ε
Tactic:
simp
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / 37
⊢ |37 * a n - 37 * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_thirtyseven_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / 37
⊢ |37 * a n - 37 * t| < ε
Tactic:
rw [← mul_sub, abs_mul, abs_of_nonneg] <;> linarith
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_thirtyseven_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
ε : ℝ
hε : ε > 0
⊢ ε / 37 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_pos_const_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
⊢ TendsTo (fun n => c * a n) (c * t)
Tactic:
intro ε hε
Proof state after:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c * a n) n - c * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_pos_const_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c * a n) n - c * t| < ε
Tactic:
obtain ⟨X, hX⟩ := h (ε / c) (div_pos hε hc)
Proof state after:
case intro
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / c
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c * a n) n - c * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_pos_const_mul
Proof state before:
case intro
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / c
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c * a n) n - c * t| < ε
Tactic:
use X
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / c
⊢ ∀ (n : ℕ), X ≤ n → |(fun n => c * a n) n - c * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_pos_const_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / c
⊢ ∀ (n : ℕ), X ≤ n → |(fun n => c * a n) n - c * t| < ε
Tactic:
intro n hn
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / c
n : ℕ
hn : X ≤ n
⊢ |(fun n => c * a n) n - c * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_pos_const_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / c
n : ℕ
hn : X ≤ n
⊢ |(fun n => c * a n) n - c * t| < ε
Tactic:
specialize hX n hn
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / c
⊢ |(fun n => c * a n) n - c * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_pos_const_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / c
⊢ |(fun n => c * a n) n - c * t| < ε
Tactic:
simp
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / c
⊢ |c * a n - c * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_pos_const_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / c
⊢ |c * a n - c * t| < ε
Tactic:
rw [← mul_sub, abs_mul, abs_of_pos hc]
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / c
⊢ c * |a n - t| < ε
Theorem: Section2sheet6Solutions.tendsTo_pos_const_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / c
⊢ c * |a n - t| < ε
Tactic:
exact (lt_div_iff' hc).mp hX
Proof state after:
no goals