suffices の挙動が意図と異なる

[Seasawher]

@lean-ja

Lean 勉強会 Analysis 3 を進めていますが，suffices の挙動が理解できません．

以下が私の書いたコードです：

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
    tactic =>
      have h1: ε⁻¹ < 10 ^ j ↔ (10 ^ j: ℚ)⁻¹ < ε := by
        constructor
        · apply inv_lt_of_inv_lt
          assumption
        · apply inv_lt_of_inv_lt
          apply pow_pos
          linarith
    rw [←h1]
  
  -- `ε⁻¹ < 10 ^ n` となる `n` が存在する
  have ⟨ N, h2 ⟩ : ∃ n, ε⁻¹ < 10 ^ n := by
    exact pow_unbounded_of_one_lt ε⁻¹ rfl
  
  exists N
  intro j hj

  -- `10 ^ N ≤ 10 ^ j` を示せば十分であることを言いたい
  suffices 10 ^ N ≤ 10 ^ j by
    -- この時点でなぜかゴールが `10 ^ N ≤ 10 ^ j` になる
    sorry -- sorry の頭にカーソルを置くと，仮定が正しく追加されている

  sorry

上記コメントにあるように，suffices を書いた直後にゴールが置き換わってしまいます．（期待している挙動は，ゴールはそのままで仮定が追加されていること）

どうしてこういうことが起こるのでしょうか？

[haruhisa-enomoto]

自分もsuffices .... byのあとのインデントブロックで同じ状況に遭遇して不便だと思ったときがあります。
たぶんバグだとは思いますが（Zulip chatのログとかはあまり調べていない）、解決策（？）として、

• suffices ... from byと書くとなぜかそういうことは起きない（tacticの説明だとbyのみなものはfrom byの省略形だと書いてありますがここの振る舞いが何故か違うみたいです）
• インデントブロックの中の最初にskip tacticを置いて改行すると、ちゃんと意図した感じになる

（きちんとしたことはZulip chatに聞くほうがいいかもしれません）

[Seasawher]

ありがとうございます

なるほど，詳しいことはわかりませんが，suffices ... from by と書く癖をつけた方がよさそうですね

[Seasawher]

@haruhisa-enomoto zulip で訊いてみたところ，やはりバグかもしれないようです