Theorem: Tutorial.«0.9999999 = 1» (Tutorial/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:
sorry
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