internlm/Lean-Github huggingface dataset:
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
case h₂
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen s'
Tactic:
exact ihs'
Proof state after:
no goals
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
S : Set (Set α)
a✝ : ∀ s ∈ S, GenerateOpen g s
hS : ∀ s ∈ S, IsOpen s
⊢ IsOpen (⋃₀ S)
Tactic:
apply isOpen_sUnion
Proof state after:
case h
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
S : Set (Set α)
a✝ : ∀ s ∈ S, GenerateOpen g s
hS : ∀ s ∈ S, IsOpen s
⊢ ∀ t_1 ∈ S, IsOpen t_1
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
case h
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
S : Set (Set α)
a✝ : ∀ s ∈ S, GenerateOpen g s
hS : ∀ s ∈ S, IsOpen s
⊢ ∀ t_1 ∈ S, IsOpen t_1
Tactic:
exact hS
Proof state after:
no goals
Theorem: pow_two_le_fac
Proof state before:
case succ
n : ℕ
⊢ 2 ^ (Nat.succ n - 1) ≤ fac (Nat.succ n)
Tactic:
induction' n with n ih
Proof state after:
case succ.zero

⊢ 2 ^ (Nat.succ 0 - 1) ≤ fac (Nat.succ 0)

case succ.succ
n : ℕ
ih : 2 ^ (Nat.succ n - 1) ≤ fac (Nat.succ n)
⊢ 2 ^ (Nat.succ (n + 1) - 1) ≤ fac (Nat.succ (n + 1))
Theorem: pow_two_le_fac
Proof state before:
case succ.succ
n : ℕ
ih : 2 ^ (Nat.succ n - 1) ≤ fac (Nat.succ n)
⊢ 2 ^ (Nat.succ (n + 1) - 1) ≤ fac (Nat.succ (n + 1))
Tactic:
simp at *
Proof state after:
case succ.succ
n : ℕ
ih : 2 ^ n ≤ fac (Nat.succ n)
⊢ 2 ^ (n + 1) ≤ fac (Nat.succ (n + 1))
Theorem: pow_two_le_fac
Proof state before:
case succ.succ
n : ℕ
ih : 2 ^ n ≤ fac (Nat.succ n)
⊢ 2 ^ (n + 1) ≤ fac (Nat.succ (n + 1))
Tactic:
rw [pow_succ, fac]
Proof state after:
case succ.succ
n : ℕ
ih : 2 ^ n ≤ fac (Nat.succ n)
⊢ 2 * 2 ^ n ≤ (n + 1 + 1) * fac (n + 1)
Theorem: pow_two_le_fac
Proof state before:
case succ.succ
n : ℕ
ih : 2 ^ n ≤ fac (Nat.succ n)
⊢ 2 * 2 ^ n ≤ (n + 1 + 1) * fac (n + 1)
Tactic:
apply Nat.mul_le_mul _ ih
Proof state after:
n : ℕ
ih : 2 ^ n ≤ fac (Nat.succ n)
⊢ 2 ≤ n + 1 + 1
Theorem: pow_two_le_fac
Proof state before:
n : ℕ
ih : 2 ^ n ≤ fac (Nat.succ n)
⊢ 2 ≤ n + 1 + 1
Tactic:
repeat' apply Nat.succ_le_succ
Proof state after:
case a.a
n : ℕ
ih : 2 ^ n ≤ fac (Nat.succ n)
⊢ 0 ≤ n
Theorem: pow_two_le_fac
Proof state before:
case a.a
n : ℕ
ih : 2 ^ n ≤ fac (Nat.succ n)
⊢ 0 ≤ n
Tactic:
apply zero_le
Proof state after:
no goals
Theorem: pow_two_le_fac
Proof state before:
case succ.zero

⊢ 2 ^ (Nat.succ 0 - 1) ≤ fac (Nat.succ 0)
Tactic:
simp [fac]
Proof state after:
no goals
Theorem: pow_two_le_fac
Proof state before:
case a
n : ℕ
ih : 2 ^ n ≤ fac (Nat.succ n)
⊢ 1 ≤ n + 1
Tactic:
apply Nat.succ_le_succ
Proof state after:
case a.a
n : ℕ
ih : 2 ^ n ≤ fac (Nat.succ n)
⊢ 0 ≤ n
Theorem: sum_sqr
Proof state before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ ∑ i in range (n + 1), i ^ 2 = n * (n + 1) * (2 * n + 1) / 6
Tactic:
symm
Proof state after:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) * (2 * n + 1) / 6 = ∑ i in range (n + 1), i ^ 2
Theorem: sum_sqr
Proof state before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) * (2 * n + 1) / 6 = ∑ i in range (n + 1), i ^ 2
Tactic:
apply Nat.div_eq_of_eq_mul_right (by norm_num : 0 < 6)
Proof state after:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) * (2 * n + 1) = 6 * ∑ i in range (n + 1), i ^ 2
Theorem: sum_sqr
Proof state before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) * (2 * n + 1) = 6 * ∑ i in range (n + 1), i ^ 2
Tactic:
induction' n with n ih
Proof state after:
case zero
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n : ℕ
⊢ 0 * (0 + 1) * (2 * 0 + 1) = 6 * ∑ i in range (0 + 1), i ^ 2

case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) * (2 * n + 1) = 6 * ∑ i in range (n + 1), i ^ 2
⊢ (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) = 6 * ∑ i in range (n + 1 + 1), i ^ 2
Theorem: sum_sqr
Proof state before:
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) * (2 * n + 1) = 6 * ∑ i in range (n + 1), i ^ 2
⊢ (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) = 6 * ∑ i in range (n + 1 + 1), i ^ 2
Tactic:
rw [Finset.sum_range_succ, mul_add 6, ← ih]
Proof state after:
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) * (2 * n + 1) = 6 * ∑ i in range (n + 1), i ^ 2
⊢ (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) = n * (n + 1) * (2 * n + 1) + 6 * (n + 1) ^ 2
Theorem: sum_sqr
Proof state before:
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) * (2 * n + 1) = 6 * ∑ i in range (n + 1), i ^ 2
⊢ (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) = n * (n + 1) * (2 * n + 1) + 6 * (n + 1) ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: sum_sqr
Proof state before:
case zero
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n : ℕ
⊢ 0 * (0 + 1) * (2 * 0 + 1) = 6 * ∑ i in range (0 + 1), i ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
m n k : MyNat
⊢ add (add m n) k = add m (add n k)
Tactic:
induction' k with k ih
Proof state after:
case zero
m n : MyNat
⊢ add (add m n) zero = add m (add n zero)

case succ
m n k : MyNat
ih : add (add m n) k = add m (add n k)
⊢ add (add m n) (succ k) = add m (add n (succ k))
Theorem: MyNat.add_assoc
Proof state before:
case succ
m n k : MyNat
ih : add (add m n) k = add m (add n k)
⊢ add (add m n) (succ k) = add m (add n (succ k))
Tactic:
rw [add, ih]
Proof state after:
case succ
m n k : MyNat
ih : add (add m n) k = add m (add n k)
⊢ succ (add m (add n k)) = add m (add n (succ k))
Theorem: MyNat.add_assoc
Proof state before:
case succ
m n k : MyNat
ih : add (add m n) k = add m (add n k)
⊢ succ (add m (add n k)) = add m (add n (succ k))
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
case zero
m n : MyNat
⊢ add (add m n) zero = add m (add n zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.mul_add
Proof state before:
m n k : MyNat
⊢ mul m (add n k) = add (mul m n) (mul m k)
Tactic:
induction' k with k ih
Proof state after:
case zero
m n : MyNat
⊢ mul m (add n zero) = add (mul m n) (mul m zero)

case succ
m n k : MyNat
ih : mul m (add n k) = add (mul m n) (mul m k)
⊢ mul m (add n (succ k)) = add (mul m n) (mul m (succ k))
Theorem: MyNat.mul_add
Proof state before:
case succ
m n k : MyNat
ih : mul m (add n k) = add (mul m n) (mul m k)
⊢ mul m (add n (succ k)) = add (mul m n) (mul m (succ k))
Tactic:
rw [add, mul, mul, ih, add_assoc]
Proof state after:
no goals
Theorem: MyNat.mul_add
Proof state before:
case zero
m n : MyNat
⊢ mul m (add n zero) = add (mul m n) (mul m zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.zero_mul
Proof state before:
n : MyNat
⊢ mul zero n = zero
Tactic:
induction' n with n ih
Proof state after:
case zero

⊢ mul zero zero = zero

case succ
n : MyNat
ih : mul zero n = zero
⊢ mul zero (succ n) = zero
Theorem: MyNat.zero_mul
Proof state before:
case succ
n : MyNat
ih : mul zero n = zero
⊢ mul zero (succ n) = zero
Tactic:
rw [mul, ih]
Proof state after:
case succ
n : MyNat
ih : mul zero n = zero
⊢ add zero zero = zero
Theorem: MyNat.zero_mul
Proof state before:
case succ
n : MyNat
ih : mul zero n = zero
⊢ add zero zero = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.zero_mul
Proof state before:
case zero

⊢ mul zero zero = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
m n : MyNat
⊢ mul (succ m) n = add (mul m n) n
Tactic:
induction' n with n ih
Proof state after:
case zero
m : MyNat
⊢ mul (succ m) zero = add (mul m zero) zero

case succ
m n : MyNat
ih : mul (succ m) n = add (mul m n) n
⊢ mul (succ m) (succ n) = add (mul m (succ n)) (succ n)
Theorem: MyNat.succ_mul
Proof state before:
case succ
m n : MyNat
ih : mul (succ m) n = add (mul m n) n
⊢ mul (succ m) (succ n) = add (mul m (succ n)) (succ n)
Tactic:
rw [mul, mul, ih, add_assoc, add_assoc, add_comm n, succ_add]
Proof state after:
case succ
m n : MyNat
ih : mul (succ m) n = add (mul m n) n
⊢ add (mul m n) (succ (add m n)) = add (mul m n) (add m (succ n))
Theorem: MyNat.succ_mul
Proof state before:
case succ
m n : MyNat
ih : mul (succ m) n = add (mul m n) n
⊢ add (mul m n) (succ (add m n)) = add (mul m n) (add m (succ n))
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
case zero
m : MyNat
⊢ mul (succ m) zero = add (mul m zero) zero
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.mul_comm
Proof state before:
m n : MyNat
⊢ mul m n = mul n m
Tactic:
induction' n with n ih
Proof state after:
case zero
m : MyNat
⊢ mul m zero = mul zero m

case succ
m n : MyNat
ih : mul m n = mul n m
⊢ mul m (succ n) = mul (succ n) m
Theorem: MyNat.mul_comm
Proof state before:
case succ
m n : MyNat
ih : mul m n = mul n m
⊢ mul m (succ n) = mul (succ n) m
Tactic:
rw [mul, ih, succ_mul]
Proof state after:
no goals
Theorem: MyNat.mul_comm
Proof state before:
case zero
m : MyNat
⊢ mul m zero = mul zero m
Tactic:
rw [zero_mul]
Proof state after:
case zero
m : MyNat
⊢ mul m zero = zero
Theorem: MyNat.mul_comm
Proof state before:
case zero
m : MyNat
⊢ mul m zero = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: Lec3After.my_lemma_
Proof state before:
a b c : ℝ
h : a + b = a + c
⊢ b = c
Tactic:
exact add_left_cancel h
Proof state after:
no goals
Theorem: sequentialLimit_unique
Proof state before:
u : ℕ → ℝ
l l' : ℝ
⊢ SequentialLimit u l → SequentialLimit u l' → l = l'
Tactic:
intro hl hl'
Proof state after:
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
⊢ l = l'
Theorem: sequentialLimit_unique
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
⊢ l = l'
Tactic:
by_contra hll'
Proof state after:
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ False
Theorem: sequentialLimit_unique
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ False
Tactic:
have : |l - l'| > 0
Proof state after:
case this
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ |l - l'| > 0

u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
this : |l - l'| > 0
⊢ False
Theorem: sequentialLimit_unique
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
this : |l - l'| > 0
⊢ False
Tactic:
rw [SequentialLimit] at hl hl'
Proof state after:
u : ℕ → ℝ
l l' : ℝ
hl : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
⊢ False
Theorem: sequentialLimit_unique
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
⊢ False
Tactic:
specialize hl (|l - l'| / 2) (by linarith)
Proof state after:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
hl : ∃ N, ∀ n ≥ N, |u n - l| < |l - l'| / 2
⊢ False
Theorem: sequentialLimit_unique
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
hl : ∃ N, ∀ n ≥ N, |u n - l| < |l - l'| / 2
⊢ False
Tactic:
obtain ⟨N, hN⟩ := hl
Proof state after:
case intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| < |l - l'| / 2
⊢ False
Theorem: sequentialLimit_unique
Proof state before:
case intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| < |l - l'| / 2
⊢ False
Tactic:
obtain ⟨N', hN'⟩ := hl' (|l - l'| / 2) (by linarith)
Proof state after:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| < |l - l'| / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| < |l - l'| / 2
⊢ False
Theorem: sequentialLimit_unique
Proof state before:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| < |l - l'| / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| < |l - l'| / 2
⊢ False
Tactic:
let N₀ := max N N'
Proof state after:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| < |l - l'| / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| < |l - l'| / 2
N₀ : ℕ := max N N'
⊢ False
Theorem: sequentialLimit_unique
Proof state before:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| < |l - l'| / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| < |l - l'| / 2
N₀ : ℕ := max N N'
⊢ False
Tactic:
specialize hN N₀ (Nat.le_max_left N N')
Proof state after:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| < |l - l'| / 2
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
⊢ False
Theorem: sequentialLimit_unique
Proof state before:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| < |l - l'| / 2
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
⊢ False
Tactic:
specialize hN' N₀ (Nat.le_max_right N N')
Proof state after:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
⊢ False
Theorem: sequentialLimit_unique
Proof state before:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
⊢ False
Tactic:
have : |l - l'| < |l - l'| := by
  calc |l - l'|
      = |l - u N₀ + (u N₀ - l')| := by ring
    _ ≤ |l - u N₀| + |u N₀ - l'| := by exact abs_add (l - u N₀) (u N₀ - l')
    _ = |u N₀ - l| + |u N₀ - l'| := by rw [abs_sub_comm]
    _ < |l - l'| := by linarith
Proof state after:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this✝ : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
this : |l - l'| < |l - l'|
⊢ False
Theorem: sequentialLimit_unique
Proof state before:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this✝ : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
this : |l - l'| < |l - l'|
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: sequentialLimit_unique
Proof state before:
case this
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ |l - l'| > 0
Tactic:
apply abs_pos.2
Proof state after:
case this
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ l - l' ≠ 0
Theorem: sequentialLimit_unique
Proof state before:
case this
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ l - l' ≠ 0
Tactic:
apply sub_ne_zero.2
Proof state after:
case this
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ l ≠ l'
Theorem: sequentialLimit_unique
Proof state before:
case this
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ l ≠ l'
Tactic:
exact hll'
Proof state after:
no goals
Theorem: sequentialLimit_unique
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
⊢ |l - l'| / 2 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: sequentialLimit_unique
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| < |l - l'| / 2
⊢ |l - l'| / 2 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: sequentialLimit_unique
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
⊢ |l - l'| < |l - l'|
Tactic:
calc |l - l'|
    = |l - u N₀ + (u N₀ - l')| := by ring
  _ ≤ |l - u N₀| + |u N₀ - l'| := by exact abs_add (l - u N₀) (u N₀ - l')
  _ = |u N₀ - l| + |u N₀ - l'| := by rw [abs_sub_comm]
  _ < |l - l'| := by linarith
Proof state after:
no goals
Theorem: sequentialLimit_unique
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
⊢ |l - l'| = |l - u N₀ + (u N₀ - l')|
Tactic:
ring
Proof state after:
no goals
Theorem: sequentialLimit_unique
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
⊢ |l - u N₀ + (u N₀ - l')| ≤ |l - u N₀| + |u N₀ - l'|
Tactic:
exact abs_add (l - u N₀) (u N₀ - l')
Proof state after:
no goals
Theorem: sequentialLimit_unique
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
⊢ |l - u N₀| + |u N₀ - l'| = |u N₀ - l| + |u N₀ - l'|
Tactic:
rw [abs_sub_comm]
Proof state after:
no goals
Theorem: sequentialLimit_unique
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
⊢ |u N₀ - l| + |u N₀ - l'| < |l - l'|
Tactic:
linarith
Proof state after:
no goals
Theorem: convergesTo_const
Proof state before:
a : ℝ
⊢ SequentialLimit (fun n => a) a
Tactic:
sorry
Proof state after:
no goals
Theorem: SequentialLimit.add
Proof state before:
s t : ℕ → ℝ
a b : ℝ
hs : SequentialLimit s a
ht : SequentialLimit t b
⊢ SequentialLimit (fun n => s n + t n) (a + b)
Tactic:
sorry
Proof state after:
no goals
Theorem: inverse_of_a_commutator
Proof state before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ ⁅g, h⁆⁻¹ = ⁅h, g⁆
Tactic:
rw [commutatorElement_def, commutatorElement_def]
Proof state after:
G : Type u_1
inst✝ : Group G
g h : G
⊢ (g * h * g⁻¹ * h⁻¹)⁻¹ = h * g * h⁻¹ * g⁻¹
Theorem: inverse_of_a_commutator
Proof state before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ (g * h * g⁻¹ * h⁻¹)⁻¹ = h * g * h⁻¹ * g⁻¹
Tactic:
rw [mul_inv_rev (g * h * g⁻¹) h⁻¹]
Proof state after:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h⁻¹⁻¹ * (g * h * g⁻¹)⁻¹ = h * g * h⁻¹ * g⁻¹
Theorem: inverse_of_a_commutator
Proof state before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h⁻¹⁻¹ * (g * h * g⁻¹)⁻¹ = h * g * h⁻¹ * g⁻¹
Tactic:
rw [mul_inv_rev]
Proof state after:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h⁻¹⁻¹ * (g⁻¹⁻¹ * (g * h)⁻¹) = h * g * h⁻¹ * g⁻¹
Theorem: inverse_of_a_commutator
Proof state before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h⁻¹⁻¹ * (g⁻¹⁻¹ * (g * h)⁻¹) = h * g * h⁻¹ * g⁻¹
Tactic:
rw [mul_inv_rev]
Proof state after:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h⁻¹⁻¹ * (g⁻¹⁻¹ * (h⁻¹ * g⁻¹)) = h * g * h⁻¹ * g⁻¹
Theorem: inverse_of_a_commutator
Proof state before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h⁻¹⁻¹ * (g⁻¹⁻¹ * (h⁻¹ * g⁻¹)) = h * g * h⁻¹ * g⁻¹
Tactic:
rw [inv_inv, inv_inv]
Proof state after:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h * (g * (h⁻¹ * g⁻¹)) = h * g * h⁻¹ * g⁻¹
Theorem: inverse_of_a_commutator
Proof state before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h * (g * (h⁻¹ * g⁻¹)) = h * g * h⁻¹ * g⁻¹
Tactic:
rw [mul_assoc]
Proof state after:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h * (g * (h⁻¹ * g⁻¹)) = h * g * (h⁻¹ * g⁻¹)
Theorem: inverse_of_a_commutator
Proof state before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h * (g * (h⁻¹ * g⁻¹)) = h * g * (h⁻¹ * g⁻¹)
Tactic:
rw [mul_assoc]
Proof state after:
no goals
Theorem: my_equality
Proof state before:
a b : ℕ
⊢ a + b + a ≤ 2 * (a + b)
Tactic:
have c := a + b
Proof state after:
a b c : ℕ
⊢ a + b + a ≤ 2 * (a + b)
Theorem: my_equality
Proof state before:
a b c : ℕ
⊢ a + b + a ≤ 2 * (a + b)
Tactic:
have h : c = a + b := sorry
Proof state after:
a b c : ℕ
h : c = a + b
⊢ a + b + a ≤ 2 * (a + b)
Theorem: my_equality
Proof state before:
a b c : ℕ
h : c = a + b
⊢ a + b + a ≤ 2 * (a + b)
Tactic:
rw [← h]
Proof state after:
a b c : ℕ
h : c = a + b
⊢ c + a ≤ 2 * c
Theorem: my_equality
Proof state before:
a b c : ℕ
h : c = a + b
⊢ c + a ≤ 2 * c
Tactic:
sorry
Proof state after:
no goals
Theorem: my_lemma
Proof state before:
n : ℕ
⊢ 0 + Nat.succ n = Nat.succ n + 0
Tactic:
rw [Nat.add_succ, my_lemma n]
Proof state after:
no goals
Theorem: pow_self_ne_zero
Proof state before:
n : ℕ
⊢ n ^ n ≠ 0
Tactic:
by_cases hn : n = 0
Proof state after:
case pos
n : ℕ
hn : n = 0
⊢ n ^ n ≠ 0

case neg
n : ℕ
hn : ¬n = 0
⊢ n ^ n ≠ 0
Theorem: pow_self_ne_zero
Proof state before:
case pos
n : ℕ
hn : n = 0
⊢ n ^ n ≠ 0
Tactic:
simp [hn]
Proof state after:
no goals
Theorem: pow_self_ne_zero
Proof state before:
case neg
n : ℕ
hn : ¬n = 0
⊢ n ^ n ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: C05S03.two_le
Proof state before:
m : ℕ
h0 : m ≠ 0
h1 : m ≠ 1
⊢ 2 ≤ m
Tactic:
cases m
Proof state after:
case zero
h0 : 0 ≠ 0
h1 : 0 ≠ 1
⊢ 2 ≤ 0

case succ
n✝ : ℕ
h0 : n✝ + 1 ≠ 0
h1 : n✝ + 1 ≠ 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1
⊢ 2 ≤ n✝ + 1
Theorem: C05S03.two_le
Proof state before:
case zero
h0 : 0 ≠ 0
h1 : 0 ≠ 1
⊢ 2 ≤ 0

case succ
n✝ : ℕ
h0 : n✝ + 1 ≠ 0
h1 : n✝ + 1 ≠ 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1
⊢ 2 ≤ n✝ + 1
Tactic:
contradiction
Proof state after:
case succ
n✝ : ℕ
h0 : n✝ + 1 ≠ 0
h1 : n✝ + 1 ≠ 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1
⊢ 2 ≤ n✝ + 1
Theorem: C05S03.two_le
Proof state before:
m : ℕ
h0 : m + 1 ≠ 0
h1 : m + 1 ≠ 1
hm : m + 1 = m → 2 ≤ m + 1
⊢ 2 ≤ m + 1
Tactic:
case succ m hm =>
  cases m; contradiction
  repeat' apply Nat.succ_le_succ
  apply zero_le
Proof state after:
no goals
Theorem: C05S03.two_le
Proof state before:
m : ℕ
h0 : m + 1 ≠ 0
h1 : m + 1 ≠ 1
hm : m + 1 = m → 2 ≤ m + 1
⊢ 2 ≤ m + 1
Tactic:
cases m
Proof state after:
case zero
h0 : 0 + 1 ≠ 0
h1 : 0 + 1 ≠ 1
hm : 0 + 1 = 0 → 2 ≤ 0 + 1
⊢ 2 ≤ 0 + 1

case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 2 ≤ n✝ + 1 + 1
Theorem: C05S03.two_le
Proof state before:
case zero
h0 : 0 + 1 ≠ 0
h1 : 0 + 1 ≠ 1
hm : 0 + 1 = 0 → 2 ≤ 0 + 1
⊢ 2 ≤ 0 + 1

case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 2 ≤ n✝ + 1 + 1
Tactic:
contradiction
Proof state after:
case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 2 ≤ n✝ + 1 + 1
Theorem: C05S03.two_le
Proof state before:
case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 2 ≤ n✝ + 1 + 1
Tactic:
repeat' apply Nat.succ_le_succ
Proof state after:
case succ.a.a
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 0 ≤ n✝
Theorem: C05S03.two_le
Proof state before:
case succ.a.a
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 0 ≤ n✝
Tactic:
apply zero_le
Proof state after:
no goals
Theorem: C05S03.two_le
Proof state before:
case succ.a
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 1 ≤ n✝ + 1
Tactic:
apply Nat.succ_le_succ
Proof state after:
case succ.a.a
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 0 ≤ n✝
Theorem: C05S03.exists_prime_factor
Proof state before:
n : ℕ
h : 2 ≤ n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
by_cases np : n.Prime
Proof state after:
case pos
n : ℕ
h : 2 ≤ n
np : Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n

case neg
n : ℕ
h : 2 ≤ n
np : ¬Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n