internlm/Lean-Github huggingface dataset:
Theorem: C03S06.convergesTo_unique
Proof state before:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
⊢ False
Tactic:
have absa : |s N - a| < ε := by sorry
Proof state after:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ False
Theorem: C03S06.convergesTo_unique
Proof state before:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ False
Tactic:
have absb : |s N - b| < ε := by sorry
Proof state after:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ False
Theorem: C03S06.convergesTo_unique
Proof state before:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ False
Tactic:
have : |a - b| < |a - b| := by sorry
Proof state after:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this✝ : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
this : |a - b| < |a - b|
⊢ False
Theorem: C03S06.convergesTo_unique
Proof state before:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this✝ : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
this : |a - b| < |a - b|
⊢ False
Tactic:
exact lt_irrefl _ this
Proof state after:
no goals
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ |a - b| > 0
Tactic:
sorry
Proof state after:
no goals
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
⊢ ε > 0
Tactic:
change |a - b| / 2 > 0
Proof state after:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
⊢ |a - b| / 2 > 0
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
⊢ |a - b| / 2 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
⊢ |s N - a| < ε
Tactic:
sorry
Proof state after:
no goals
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ |s N - b| < ε
Tactic:
sorry
Proof state after:
no goals
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ |a - b| < |a - b|
Tactic:
sorry
Proof state after:
no goals
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
⊢ a = b
Tactic:
by_contra abne
Proof state after:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ False
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
⊢ False
Tactic:
let ε := |a - b| / 2
Proof state after:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
⊢ False
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
⊢ False
Tactic:
have εpos : ε > 0 := by
  change |a - b| / 2 > 0
  linarith
Proof state after:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
⊢ False
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
⊢ False
Tactic:
rcases sa ε εpos with ⟨Na, hNa⟩
Proof state after:
case intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
⊢ False
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
case intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
⊢ False
Tactic:
rcases sb ε εpos with ⟨Nb, hNb⟩
Proof state after:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
⊢ False
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
⊢ False
Tactic:
let N := max Na Nb
Proof state after:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
⊢ False
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
⊢ False
Tactic:
have absa : |s N - a| < ε := by
  apply hNa
  apply le_max_left
Proof state after:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ False
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ False
Tactic:
have absb : |s N - b| < ε := by
  apply hNb
  apply le_max_right
Proof state after:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ False
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ False
Tactic:
have : |a - b| < |a - b|
Proof state after:
case this
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ |a - b| < |a - b|

case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this✝ : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
this : |a - b| < |a - b|
⊢ False
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
case this
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ |a - b| < |a - b|

case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this✝ : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
this : |a - b| < |a - b|
⊢ False
Tactic:
calc
  |a - b| = |(-(s N - a)) + (s N - b)| := by
    congr
    ring
  _ ≤ |(-(s N - a))| + |s N - b| := (abs_add _ _)
  _ = |s N - a| + |s N - b| := by rw [abs_neg]
  _ < ε + ε := (add_lt_add absa absb)
  _ = |a - b| := by norm_num [ε]
Proof state after:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this✝ : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
this : |a - b| < |a - b|
⊢ False
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this✝ : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
this : |a - b| < |a - b|
⊢ False
Tactic:
exact lt_irrefl _ this
Proof state after:
no goals
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ |a - b| > 0
Tactic:
apply lt_of_le_of_ne
Proof state after:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ 0 ≤ |a - b|

case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ 0 ≠ |a - b|
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ 0 ≠ |a - b|
Tactic:
intro h''
Proof state after:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
h'' : 0 = |a - b|
⊢ False
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
h'' : 0 = |a - b|
⊢ False
Tactic:
apply abne
Proof state after:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
h'' : 0 = |a - b|
⊢ a = b
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
h'' : 0 = |a - b|
⊢ a = b
Tactic:
apply eq_of_abs_sub_eq_zero h''.symm
Proof state after:
no goals
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ 0 ≤ |a - b|
Tactic:
apply abs_nonneg
Proof state after:
no goals
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
⊢ ε > 0
Tactic:
change |a - b| / 2 > 0
Proof state after:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
⊢ |a - b| / 2 > 0
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
⊢ |a - b| / 2 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
⊢ |s N - a| < ε
Tactic:
apply hNa
Proof state after:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
⊢ N ≥ Na
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
⊢ N ≥ Na
Tactic:
apply le_max_left
Proof state after:
no goals
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ |s N - b| < ε
Tactic:
apply hNb
Proof state after:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ N ≥ Nb
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ N ≥ Nb
Tactic:
apply le_max_right
Proof state after:
no goals
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ |a - b| = |-(s N - a) + (s N - b)|
Tactic:
congr
Proof state after:
case e_a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ a - b = -(s N - a) + (s N - b)
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
case e_a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ a - b = -(s N - a) + (s N - b)
Tactic:
ring
Proof state after:
no goals
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ |(-(s N - a))| + |s N - b| = |s N - a| + |s N - b|
Tactic:
rw [abs_neg]
Proof state after:
no goals
Theorem: C03S06.convergesTo_uniqueαα
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ ε + ε = |a - b|
Tactic:
norm_num [ε]
Proof state after:
no goals
Theorem: eq_bot_iff_card
Proof state before:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
⊢ H = ⊥ ↔ card ↥H = 1
Tactic:
suffices (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x by
  simpa [eq_bot_iff_forall, card_eq_one_iff]
Proof state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
⊢ (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x
Theorem: eq_bot_iff_card
Proof state before:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
⊢ (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x
Tactic:
constructor
Proof state after:
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
⊢ (∀ x ∈ H, x = 1) → ∃ x ∈ H, ∀ a ∈ H, a = x

case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
⊢ (∃ x ∈ H, ∀ a ∈ H, a = x) → ∀ x ∈ H, x = 1
Theorem: eq_bot_iff_card
Proof state before:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
this : (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x
⊢ H = ⊥ ↔ card ↥H = 1
Tactic:
simpa [eq_bot_iff_forall, card_eq_one_iff]
Proof state after:
no goals
Theorem: eq_bot_iff_card
Proof state before:
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
⊢ (∀ x ∈ H, x = 1) → ∃ x ∈ H, ∀ a ∈ H, a = x
Tactic:
intro h
Proof state after:
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
h : ∀ x ∈ H, x = 1
⊢ ∃ x ∈ H, ∀ a ∈ H, a = x
Theorem: eq_bot_iff_card
Proof state before:
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
h : ∀ x ∈ H, x = 1
⊢ ∃ x ∈ H, ∀ a ∈ H, a = x
Tactic:
use 1, H.one_mem
Proof state after:
no goals
Theorem: eq_bot_iff_card
Proof state before:
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
⊢ (∃ x ∈ H, ∀ a ∈ H, a = x) → ∀ x ∈ H, x = 1
Tactic:
rintro ⟨y, -, hy'⟩ x hx
Proof state after:
case mpr.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
y : G
hy' : ∀ a ∈ H, a = y
x : G
hx : x ∈ H
⊢ x = 1
Theorem: eq_bot_iff_card
Proof state before:
case mpr.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
y : G
hy' : ∀ a ∈ H, a = y
x : G
hx : x ∈ H
⊢ x = 1
Tactic:
calc x = y := hy' x hx
_      = 1 := (hy' 1 H.one_mem).symm
Proof state after:
no goals
Theorem: inf_bot_of_coprime
Proof state before:
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype ↥H
inst✝ : Fintype ↥K
h : (card ↥H).Coprime (card ↥K)
⊢ H ⊓ K = ⊥
Tactic:
have D₁ : card (H ⊓ K : Subgroup G) ∣ card H := card_dvd_of_le inf_le_left
Proof state after:
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype ↥H
inst✝ : Fintype ↥K
h : (card ↥H).Coprime (card ↥K)
D₁ : card ↥(H ⊓ K) ∣ card ↥H
⊢ H ⊓ K = ⊥
Theorem: inf_bot_of_coprime
Proof state before:
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype ↥H
inst✝ : Fintype ↥K
h : (card ↥H).Coprime (card ↥K)
D₁ : card ↥(H ⊓ K) ∣ card ↥H
⊢ H ⊓ K = ⊥
Tactic:
have D₂ : card (H ⊓ K : Subgroup G) ∣ card K := card_dvd_of_le inf_le_right
Proof state after:
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype ↥H
inst✝ : Fintype ↥K
h : (card ↥H).Coprime (card ↥K)
D₁ : card ↥(H ⊓ K) ∣ card ↥H
D₂ : card ↥(H ⊓ K) ∣ card ↥K
⊢ H ⊓ K = ⊥
Theorem: inf_bot_of_coprime
Proof state before:
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype ↥H
inst✝ : Fintype ↥K
h : (card ↥H).Coprime (card ↥K)
D₁ : card ↥(H ⊓ K) ∣ card ↥H
D₂ : card ↥(H ⊓ K) ∣ card ↥K
⊢ H ⊓ K = ⊥
Tactic:
exact eq_bot_iff_card.2 (Nat.eq_one_of_dvd_coprimes h D₁ D₂)
Proof state after:
no goals
Theorem: compat_myMap
Proof state before:
⊢ ∀ r ∈ {FreeGroup.of () ^ 3}, (FreeGroup.lift myMap) r = 1
Tactic:
rintro _ rfl
Proof state after:
⊢ (FreeGroup.lift myMap) (FreeGroup.of () ^ 3) = 1
Theorem: compat_myMap
Proof state before:
⊢ (FreeGroup.lift myMap) (FreeGroup.of () ^ 3) = 1
Tactic:
simp
Proof state after:
⊢ myMap () ^ 3 = 1
Theorem: compat_myMap
Proof state before:
⊢ myMap () ^ 3 = 1
Tactic:
decide
Proof state after:
no goals
Theorem: conjugate_one
Proof state before:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ conjugate 1 H = H
Tactic:
ext x
Proof state after:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
x : G
⊢ x ∈ conjugate 1 H ↔ x ∈ H
Theorem: conjugate_one
Proof state before:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
x : G
⊢ x ∈ conjugate 1 H ↔ x ∈ H
Tactic:
simp [conjugate]
Proof state after:
no goals
Theorem: aux_card_eq
Proof state before:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Fintype G
h' : card G = card ↥H * card ↥K
⊢ card (G ⧸ H) = card ↥K
Tactic:
have := calc
  card (G ⧸ H) * card H = card G := by rw [← H.index_eq_card, H.index_mul_card]
  _                     = card K * card H := by rw [h', mul_comm]
Proof state after:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Fintype G
h' : card G = card ↥H * card ↥K
this : card (G ⧸ H) * card ↥H = card ↥K * card ↥H
⊢ card (G ⧸ H) = card ↥K
Theorem: aux_card_eq
Proof state before:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Fintype G
h' : card G = card ↥H * card ↥K
this : card (G ⧸ H) * card ↥H = card ↥K * card ↥H
⊢ card (G ⧸ H) = card ↥K
Tactic:
exact Nat.eq_of_mul_eq_mul_right card_pos this
Proof state after:
no goals
Theorem: aux_card_eq
Proof state before:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Fintype G
h' : card G = card ↥H * card ↥K
⊢ card (G ⧸ H) * card ↥H = card G
Tactic:
rw [← H.index_eq_card, H.index_mul_card]
Proof state after:
no goals
Theorem: aux_card_eq
Proof state before:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Fintype G
h' : card G = card ↥H * card ↥K
⊢ card G = card ↥K * card ↥H
Tactic:
rw [h', mul_comm]
Proof state after:
no goals
Theorem: inverse_spec
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Inhabited α
P : α → Prop
h✝ : ∃ x, P x
f : α → β
y : β
h : ∃ x, f x = y
⊢ f (inverse f y) = y
Tactic:
rw [inverse, dif_pos h]
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Inhabited α
P : α → Prop
h✝ : ∃ x, P x
f : α → β
y : β
h : ∃ x, f x = y
⊢ f (choose h) = y
Theorem: inverse_spec
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Inhabited α
P : α → Prop
h✝ : ∃ x, P x
f : α → β
y : β
h : ∃ x, f x = y
⊢ f (choose h) = y
Tactic:
exact Classical.choose_spec h
Proof state after:
no goals
Theorem: Cantor
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
⊢ ∀ (f : α → Set α), ¬Surjective f
Tactic:
intro f surjf
Proof state after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
⊢ False
Theorem: Cantor
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
⊢ False
Tactic:
let S := { i | i ∉ f i }
Proof state after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
⊢ False
Theorem: Cantor
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
⊢ False
Tactic:
rcases surjf S with ⟨j, h⟩
Proof state after:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
⊢ False