Convモードの中で，have を使用して補題を宣言する

[Seasawher]

@aconite-ac

Lean 勉強会の analysis3 に取り組んでいるのですが，theorem «0.9999999 = 1» で詰まっています．

theorem «0.9999999 = 1» : Real.ofCauchy (Quotient.mk CauSeq.equiv «0.9999999») = (1 : ℝ) := by
  calc _ = Real.ofCauchy (Quotient.mk CauSeq.equiv (CauSeq.const abs 1)) := ?_
       _ = (1 : ℝ) := Real.ofCauchy_one
  rw [«0.9999999»]
  congr 1
  apply Quotient.sound
  intro ε ε0
  suffices ∃ i, ∀ (j : ℕ), j ≥ i → (10 ^ j : ℚ)⁻¹ < ε by simpa [abs]
  -- ヒント: `pow_unbounded_of_one_lt`と`inv_lt_of_inv_lt`を使って、欲しい`i`を手に入れよう
  
  -- 示すべき式を書き換える
  conv =>
    congr
    intro i j hji
    -- have ε⁻¹ < 10 ^ j → (10 ^ j)⁻¹ < ε := by sorry
    rfl
  
  sorry

-- have ε⁻¹ < 10 ^ j → (10 ^ j)⁻¹ < ε := by sorry のところがエラーになって動きません．ゴールにある (10 ^ j)⁻¹ < ε を補題を使って書き換えたいのですが，conv の中では have を使うことはできないのでしょうか？

[aconite-ac]

convモード内で

tactic =>
  <tactic sequence>

と書くと、通常のタクティクの列<tactic sequence>を使うことができます。

今回の場合は、

    tactic => 
      have h₁ : ε⁻¹ < 10 ^ j → (10 ^ j : ℚ)⁻¹ < ε := by

と書き始めることができます。

[Seasawher]

ありがとうございます．

しかし，よく見たら TPiL4 に書かれていますね…
https://aconite-ac.github.io/theorem_proving_in_lean4_ja/conv.html#other-tactics-inside-conversion-mode-%E5%A4%89%E6%8F%9B%E3%83%A2%E3%83%BC%E3%83%89%E3%81%AB%E3%81%8A%E3%81%91%E3%82%8B%E4%BB%96%E3%81%AE%E3%82%BF%E3%82%AF%E3%83%86%E3%82%A3%E3%82%AF

失礼しました．次からもっと気を付けます．

[aconite-ac]

そうですね、概ねTPiL4の11章が参考になります。

今回の質問に関して言えば、TPiL4に書かれている通りに、改行せずに

tactic => <tactic sequence>

と書くと、タクティクブロックのインデントが<の高さになってしまう(したがってインデントを高くしないとエラーがでる)ため、
改行して

tactic => 
  <tactic sequence>

と書いた方が見やすくなることに気付きましたので、共有させていただきました。