Theorem: Tutorial.«0.9999999 = 1» (Solution/Advanced/Analysis/Lecture3.lean)

State before:
⊢ { cauchy := ⟦«0.9999999»⟧ } = 1
Tactic:
calc _ = Real.ofCauchy (Quotient.mk CauSeq.equiv (CauSeq.const abs 1)) := ?_
     _ = (1 : ℝ) := Real.ofCauchy_one
State after:
⊢ { cauchy := ⟦«0.9999999»⟧ } = { cauchy := ⟦CauSeq.const abs 1⟧ }

State before:
⊢ { cauchy := ⟦«0.9999999»⟧ } = { cauchy := ⟦CauSeq.const abs 1⟧ }
Tactic:
rw [«0.9999999»]
State after:
⊢ { cauchy := ⟦{ val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 }⟧ } =
    { cauchy := ⟦CauSeq.const abs 1⟧ }

State before:
⊢ { cauchy := ⟦{ val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 }⟧ } =
    { cauchy := ⟦CauSeq.const abs 1⟧ }
Tactic:
congr 1
State after:
case e_cauchy

⊢ ⟦{ val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 }⟧ = ⟦CauSeq.const abs 1⟧

State before:
case e_cauchy

⊢ ⟦{ val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 }⟧ = ⟦CauSeq.const abs 1⟧
Tactic:
apply Quotient.sound
State after:
case e_cauchy.a

⊢ { val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 } ≈ CauSeq.const abs 1

State before:
case e_cauchy.a

⊢ { val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 } ≈ CauSeq.const abs 1
Tactic:
intro ε ε0
State after:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |↑({ val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 } - CauSeq.const abs 1) j| < ε

State before:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |↑({ val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 } - CauSeq.const abs 1) j| < ε
Tactic:
suffices ∃ i, ∀ (j : ℕ), j ≥ i → (10 ^ j : ℚ)⁻¹ < ε by simpa [abs_of_ten_inv]
State after:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, (10 ^ j)⁻¹ < ε

State before:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, (10 ^ j)⁻¹ < ε
Tactic:
have ⟨n, hn⟩ : ∃ n : ℕ, ε⁻¹ < 10 ^ n := pow_unbounded_of_one_lt ε⁻¹ rfl
State after:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
⊢ ∃ i, ∀ j ≥ i, (10 ^ j)⁻¹ < ε

State before:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
⊢ ∃ i, ∀ j ≥ i, (10 ^ j)⁻¹ < ε
Tactic:
have : (10 ^ n : ℚ)⁻¹ < ε := inv_lt_of_inv_lt ε0 hn
State after:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
this : (10 ^ n)⁻¹ < ε
⊢ ∃ i, ∀ j ≥ i, (10 ^ j)⁻¹ < ε

State before:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
this : (10 ^ n)⁻¹ < ε
⊢ ∃ i, ∀ j ≥ i, (10 ^ j)⁻¹ < ε
Tactic:
exists n
State after:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
this : (10 ^ n)⁻¹ < ε
⊢ ∀ j ≥ n, (10 ^ j)⁻¹ < ε

State before:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
this : (10 ^ n)⁻¹ < ε
⊢ ∀ j ≥ n, (10 ^ j)⁻¹ < ε
Tactic:
intro h hj
State after:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
this : (10 ^ n)⁻¹ < ε
h : ℕ
hj : h ≥ n
⊢ (10 ^ h)⁻¹ < ε

State before:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
this : (10 ^ n)⁻¹ < ε
h : ℕ
hj : h ≥ n
⊢ (10 ^ h)⁻¹ < ε
Tactic:
calc (10 ^ h : ℚ )⁻¹ ≤ (10 ^ n : ℚ)⁻¹ := inv_pow_le_inv_pow_of_le (by linarith) hj
  _ < ε := this
State after:
no goals

State before:
ε : ℚ
ε0 : ε > 0
this : ∃ i, ∀ j ≥ i, (10 ^ j)⁻¹ < ε
⊢ ∃ i, ∀ j ≥ i, |↑({ val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 } - CauSeq.const abs 1) j| < ε
Tactic:
simpa [abs_of_ten_inv]
State after:
no goals

State before:
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
this : (10 ^ n)⁻¹ < ε
h : ℕ
hj : h ≥ n
⊢ 1 ≤ 10
Tactic:
linarith
State after:
no goals