internlm/Lean-Github huggingface dataset:
Theorem: Section2sheet5solutions.tendsTo_add
Proof state before:
case intro
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
obtain ⟨Y, hY⟩ := hb (ε / 2) (by linarith)
Proof state after:
case intro.intro
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: Section2sheet5solutions.tendsTo_add
Proof state before:
case intro.intro
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
use max X Y
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
⊢ ∀ (n : ℕ), max X Y ≤ n → |a n + b n - (t + u)| < ε
Theorem: Section2sheet5solutions.tendsTo_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
⊢ ∀ (n : ℕ), max X Y ≤ n → |a n + b n - (t + u)| < ε
Tactic:
intro n hn
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
n : ℕ
hn : max X Y ≤ n
⊢ |a n + b n - (t + u)| < ε
Theorem: Section2sheet5solutions.tendsTo_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
n : ℕ
hn : max X Y ≤ n
⊢ |a n + b n - (t + u)| < ε
Tactic:
rw [max_le_iff] at hn
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
n : ℕ
hn : X ≤ n ∧ Y ≤ n
⊢ |a n + b n - (t + u)| < ε
Theorem: Section2sheet5solutions.tendsTo_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
n : ℕ
hn : X ≤ n ∧ Y ≤ n
⊢ |a n + b n - (t + u)| < ε
Tactic:
specialize hX n hn.1
Proof state after:
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)| < ε
Theorem: Section2sheet5solutions.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: Section2sheet5solutions.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: Section2sheet5solutions.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: Section2sheet5solutions.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: Section2sheet5solutions.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: Section2sheet5solutions.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:
simpa [sub_eq_add_neg] using tendsTo_add ha (tendsTo_neg hb)
Proof state after:
no goals
Theorem: Section15Sheet3Solutions.divides_of_cong_four
Proof state before:
t : ℕ
⊢ 5 ∣ 4 * (65 * t + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * t + 4) ^ 2 + 1
Tactic:
constructor
Proof state after:
case left
t : ℕ
⊢ 5 ∣ 4 * (65 * t + 4) ^ 2 + 1

case right
t : ℕ
⊢ 13 ∣ 4 * (65 * t + 4) ^ 2 + 1
Theorem: Section15Sheet3Solutions.divides_of_cong_four
Proof state before:
case left
t : ℕ
⊢ 5 ∣ 4 * (65 * t + 4) ^ 2 + 1
Tactic:
use 3380 * t ^ 2 + 416 * t + 13
Proof state after:
case h
t : ℕ
⊢ 4 * (65 * t + 4) ^ 2 + 1 = 5 * (3380 * t ^ 2 + 416 * t + 13)
Theorem: Section15Sheet3Solutions.divides_of_cong_four
Proof state before:
case h
t : ℕ
⊢ 4 * (65 * t + 4) ^ 2 + 1 = 5 * (3380 * t ^ 2 + 416 * t + 13)
Tactic:
ring
Proof state after:
no goals
Theorem: Section15Sheet3Solutions.divides_of_cong_four
Proof state before:
case right
t : ℕ
⊢ 13 ∣ 4 * (65 * t + 4) ^ 2 + 1
Tactic:
use 1300 * t ^ 2 + 160 * t + 5
Proof state after:
case h
t : ℕ
⊢ 4 * (65 * t + 4) ^ 2 + 1 = 13 * (1300 * t ^ 2 + 160 * t + 5)
Theorem: Section15Sheet3Solutions.divides_of_cong_four
Proof state before:
case h
t : ℕ
⊢ 4 * (65 * t + 4) ^ 2 + 1 = 13 * (1300 * t ^ 2 + 160 * t + 5)
Tactic:
ring
Proof state after:
no goals
Theorem: Section15Sheet3Solutions.arb_large_soln
Proof state before:
⊢ ∀ (N : ℕ), ∃ n > N, 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1
Tactic:
intro N
Proof state after:
N : ℕ
⊢ ∃ n > N, 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1
Theorem: Section15Sheet3Solutions.arb_large_soln
Proof state before:
N : ℕ
⊢ ∃ n > N, 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1
Tactic:
use 65 * N + 4
Proof state after:
case h
N : ℕ
⊢ 65 * N + 4 > N ∧ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Theorem: Section15Sheet3Solutions.arb_large_soln
Proof state before:
case h
N : ℕ
⊢ 65 * N + 4 > N ∧ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Tactic:
constructor
Proof state after:
case h.left
N : ℕ
⊢ 65 * N + 4 > N

case h.right
N : ℕ
⊢ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Theorem: Section15Sheet3Solutions.arb_large_soln
Proof state before:
case h.left
N : ℕ
⊢ 65 * N + 4 > N
Tactic:
linarith
Proof state after:
no goals
Theorem: Section15Sheet3Solutions.arb_large_soln
Proof state before:
case h.right
N : ℕ
⊢ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Tactic:
apply divides_of_cong_four
Proof state after:
no goals
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
S : Set ℕ
⊢ Set.Infinite S ↔ ∀ (N : ℕ), ∃ n > N, n ∈ S
Tactic:
constructor
Proof state after:
case mp
S : Set ℕ
⊢ Set.Infinite S → ∀ (N : ℕ), ∃ n > N, n ∈ S

case mpr
S : Set ℕ
⊢ (∀ (N : ℕ), ∃ n > N, n ∈ S) → Set.Infinite S
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case mp
S : Set ℕ
⊢ Set.Infinite S → ∀ (N : ℕ), ∃ n > N, n ∈ S
Tactic:
intro h n
Proof state after:
case mp
S : Set ℕ
h : Set.Infinite S
n : ℕ
⊢ ∃ n_1 > n, n_1 ∈ S
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case mp
S : Set ℕ
h : Set.Infinite S
n : ℕ
⊢ ∃ n_1 > n, n_1 ∈ S
Tactic:
have h2 := Set.Infinite.exists_not_mem_finset h (Finset.range (n + 1))
Proof state after:
case mp
S : Set ℕ
h : Set.Infinite S
n : ℕ
h2 : ∃ a ∈ S, a ∉ Finset.range (n + 1)
⊢ ∃ n_1 > n, n_1 ∈ S
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case mp
S : Set ℕ
h : Set.Infinite S
n : ℕ
h2 : ∃ a ∈ S, a ∉ Finset.range (n + 1)
⊢ ∃ n_1 > n, n_1 ∈ S
Tactic:
rcases h2 with ⟨m, hm, h3⟩
Proof state after:
case mp.intro.intro
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ∉ Finset.range (n + 1)
⊢ ∃ n_1 > n, n_1 ∈ S
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case mp.intro.intro
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ∉ Finset.range (n + 1)
⊢ ∃ n_1 > n, n_1 ∈ S
Tactic:
use m
Proof state after:
case h
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ∉ Finset.range (n + 1)
⊢ m > n ∧ m ∈ S
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case h
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ∉ Finset.range (n + 1)
⊢ m > n ∧ m ∈ S
Tactic:
refine' ⟨_, hm⟩
Proof state after:
case h
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ∉ Finset.range (n + 1)
⊢ m > n
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case h
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ∉ Finset.range (n + 1)
⊢ m > n
Tactic:
contrapose! h3
Proof state after:
case h
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ≤ n
⊢ m ∈ Finset.range (n + 1)
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case h
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ≤ n
⊢ m ∈ Finset.range (n + 1)
Tactic:
exact Finset.mem_range_succ_iff.mpr h3
Proof state after:
no goals
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case mpr
S : Set ℕ
⊢ (∀ (N : ℕ), ∃ n > N, n ∈ S) → Set.Infinite S
Tactic:
contrapose!
Proof state after:
case mpr
S : Set ℕ
⊢ ¬Set.Infinite S → ∃ N, ∀ n > N, n ∉ S
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case mpr
S : Set ℕ
⊢ ¬Set.Infinite S → ∃ N, ∀ n > N, n ∉ S
Tactic:
intro h
Proof state after:
case mpr
S : Set ℕ
h : ¬Set.Infinite S
⊢ ∃ N, ∀ n > N, n ∉ S
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case mpr
S : Set ℕ
h : ¬Set.Infinite S
⊢ ∃ N, ∀ n > N, n ∉ S
Tactic:
rw [Set.not_infinite] at h
Proof state after:
case mpr
S : Set ℕ
h : Set.Finite S
⊢ ∃ N, ∀ n > N, n ∉ S
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case mpr
S : Set ℕ
h : Set.Finite S
⊢ ∃ N, ∀ n > N, n ∉ S
Tactic:
let S2 : Finset ℕ := Set.Finite.toFinset h
Proof state after:
case mpr
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ N, ∀ n > N, n ∉ S
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case mpr
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ N, ∀ n > N, n ∉ S
Tactic:
have h2 : ∃ B, ∀ n ∈ S2, n ≤ B := by
  use Finset.sup S2 id
  intros _ H
  apply Finset.le_sup H
Proof state after:
case mpr
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
h2 : ∃ B, ∀ n ∈ S2, n ≤ B
⊢ ∃ N, ∀ n > N, n ∉ S
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case mpr
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
h2 : ∃ B, ∀ n ∈ S2, n ≤ B
⊢ ∃ N, ∀ n > N, n ∉ S
Tactic:
cases' h2 with N hN
Proof state after:
case mpr.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
⊢ ∃ N, ∀ n > N, n ∉ S
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case mpr.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
⊢ ∃ N, ∀ n > N, n ∉ S
Tactic:
use N
Proof state after:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
⊢ ∀ n > N, n ∉ S
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
⊢ ∀ n > N, n ∉ S
Tactic:
have h3 : ∀ n : ℕ, n ∈ S ↔ n ∈ S2
Proof state after:
case h3
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
⊢ ∀ (n : ℕ), n ∈ S ↔ n ∈ S2

case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
⊢ ∀ n > N, n ∉ S
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case h3
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
⊢ ∀ (n : ℕ), n ∈ S ↔ n ∈ S2

case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
⊢ ∀ n > N, n ∉ S
Tactic:
intro n
Proof state after:
case h3
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
n : ℕ
⊢ n ∈ S ↔ n ∈ S2

case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
⊢ ∀ n > N, n ∉ S
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case h3
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
n : ℕ
⊢ n ∈ S ↔ n ∈ S2

case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
⊢ ∀ n > N, n ∉ S
Tactic:
exact (Set.Finite.mem_toFinset h).symm
Proof state after:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
⊢ ∀ n > N, n ∉ S
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
⊢ ∀ n > N, n ∉ S
Tactic:
intro n hn h4
Proof state after:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S
⊢ False
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S
⊢ False
Tactic:
rw [h3] at h4
Proof state after:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S2
⊢ False
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S2
⊢ False
Tactic:
specialize hN n h4
Proof state after:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S2
hN : n ≤ N
⊢ False
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S2
hN : n ≤ N
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ B, ∀ n ∈ S2, n ≤ B
Tactic:
use Finset.sup S2 id
Proof state after:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∀ n ∈ S2, n ≤ Finset.sup S2 id
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∀ n ∈ S2, n ≤ Finset.sup S2 id
Tactic:
intros _ H
Proof state after:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
n✝ : ℕ
H : n✝ ∈ S2
⊢ n✝ ≤ Finset.sup S2 id
Theorem: Section15Sheet3Solutions.infinite_iff_arb_large
Proof state before:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
n✝ : ℕ
H : n✝ ∈ S2
⊢ n✝ ≤ Finset.sup S2 id
Tactic:
apply Finset.le_sup H
Proof state after:
no goals
Theorem: Section15Sheet3Solutions.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: Section15Sheet3Solutions.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: Section4sheet1.subset_def
Proof state before:
X : Type
A B C D : Set X
⊢ A ⊆ B ↔ ∀ x ∈ A, x ∈ B
Tactic:
rfl
Proof state after:
no goals
Theorem: Section4sheet1.mem_union_iff
Proof state before:
X : Type
A B C D : Set X
x : X
⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
Tactic:
rfl
Proof state after:
no goals
Theorem: Section5sheet2.WeakGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : WeakGroup G
a b c : G
h : a * b = a * c
⊢ b = c
Tactic:
sorry
Proof state after:
no goals
Theorem: Section5sheet2.WeakGroup.mul_eq_of_eq_inv_mul
Proof state before:
G : Type
inst✝ : WeakGroup G
a b c : G
h : b = a⁻¹ * c
⊢ a * b = c
Tactic:
sorry
Proof state after:
no goals
Theorem: Section5sheet2.WeakGroup.mul_one
Proof state before:
G : Type
inst✝ : WeakGroup G
a✝ b c a : G
⊢ a * 1 = a
Tactic:
sorry
Proof state after:
no goals
Theorem: Section5sheet2.WeakGroup.mul_inv_self
Proof state before:
G : Type
inst✝ : WeakGroup G
a✝ b c a : G
⊢ a * a⁻¹ = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: Section3sheet1solutions.Yb_ne_Yc
Proof state before:
⊢ Y.b ≠ Y.c
Tactic:
intro h
Proof state after:
h : Y.b = Y.c
⊢ False
Theorem: Section3sheet1solutions.Yb_ne_Yc
Proof state before:
h : Y.b = Y.c
⊢ False
Tactic:
cases h
Proof state after:
no goals
Theorem: Section3sheet1solutions.gYb_eq_gYc
Proof state before:
⊢ g Y.b = g Y.c
Tactic:
rfl
Proof state after:
no goals
Theorem: Section3sheet1solutions.gf_injective
Proof state before:
⊢ Injective (g ∘ f)
Tactic:
rintro ⟨_⟩ ⟨_⟩ _
Proof state after:
case a.a
a✝ : (g ∘ f) X.a = (g ∘ f) X.a
⊢ X.a = X.a
Theorem: Section3sheet1solutions.gf_injective
Proof state before:
case a.a
a✝ : (g ∘ f) X.a = (g ∘ f) X.a
⊢ X.a = X.a
Tactic:
rfl
Proof state after:
no goals
Theorem: Section3sheet1solutions.gf_surjective
Proof state before:
⊢ Surjective (g ∘ f)
Tactic:
intro z
Proof state after:
z : Z
⊢ ∃ a, (g ∘ f) a = z
Theorem: Section3sheet1solutions.gf_surjective
Proof state before:
z : Z
⊢ ∃ a, (g ∘ f) a = z
Tactic:
use X.a
Proof state after:
no goals
Theorem: Section2sheet5.tendsTo_neg
Proof state before:
a : ℕ → ℝ
t : ℝ
ha : TendsTo a t
⊢ TendsTo (fun n => -a n) (-t)
Tactic:
sorry
Proof state after:
no goals
Theorem: Section2sheet5.tendsTo_add
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:
rw [tendsTo_def] at *
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
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| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
intro ε hε
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
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 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
specialize ha (ε / 2) (by linarith)
Proof state after:
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
ha : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: Section2sheet5.tendsTo_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
ha : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
cases' ha with X hX
Proof state after:
case intro
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: Section2sheet5.tendsTo_add
Proof state before:
case intro
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
obtain ⟨Y, hY⟩ := hb (ε / 2) (by linarith)
Proof state after:
case intro.intro
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: Section2sheet5.tendsTo_add
Proof state before:
case intro.intro
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
use max X Y
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
⊢ ∀ (n : ℕ), max X Y ≤ n → |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 : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
⊢ ∀ (n : ℕ), max X Y ≤ n → |a n + b n - (t + u)| < ε
Tactic:
intro n hn
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
n : ℕ
hn : max X Y ≤ n
⊢ |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 : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
n : ℕ
hn : max X Y ≤ n
⊢ |a n + b n - (t + u)| < ε
Tactic:
rw [max_le_iff] at hn
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
n : ℕ
hn : X ≤ n ∧ Y ≤ n
⊢ |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 : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
n : ℕ
hn : X ≤ n ∧ Y ≤ n
⊢ |a n + b n - (t + u)| < ε
Tactic:
specialize hX n hn.1
Proof state after:
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)| < ε