見出し画像

Lean4: 厳密な型比較の罠かバグか？

D.

Lean は型を比較して一致することで証明を進めます。

しかし…。不可解なことも起きます…。ホラーですね…🎃ハロウィン現象

exact

Application type mismatch: The argument
  h_union_le_sum
has type
  ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤
    ∑ p ∈ range (X + 1) with Nat.Prime p ∧ p
    ≥ 3, ↑(#({n ∈ Icc 0 X | n ≤ X ∧ ↑↑(Vp p n) - 2 > γ_values p}))
but is expected to have type
  ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤
    ∑ p ∈ range (X + 1) with Nat.Prime p ∧ p
    ≥ 3, ↑(#({n ∈ Icc 0 X | n ≤ X ∧ ↑↑(Vp p n) - 2 > γ_values p}))
in the application
  le_trans h_union_le_sum

h_union_le_sum :
  ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤
    ∑ p ∈ range (X + 1) with Nat.Prime p ∧ p
    ≥ 3, ↑(#({n ∈ Icc 0 X | n ≤ X ∧ ↑↑(Vp p n) - 2 > γ_values p}))

見た目の文字列的に完全一致しているにも関わらず

$$
\Large
\text{type mismatch}
$$

となって exact が証明完了してくれません。

exact_mod_cast

という型を調整（キャスト）して比較するもあるのですが、同様にエラー。

mod_cast has type
  #({n ∈ Icc 0 X | Bad_ε n γ_values}) ≤
    ∑ x ∈ range (X + 1) with Nat.Prime x ∧ x
    ≥ 3, #({n ∈ Icc 0 X | n ≤ X ∧ ↑(Int.subNatNat (Vp x n) 2) > γ_values x})
but is expected to have type
  #({n ∈ Icc 0 X | Bad_ε n γ_values}) ≤
    ∑ x ∈ range (X + 1) with Nat.Prime x ∧ x
    ≥ 3, #({n ∈ Icc 0 X | n ≤ X ∧ ↑(Int.subNatNat (Vp x n) 2) > γ_values x})
Normalize casts in the goal and the given expression, then close the goal with exact.

h_union_le_sum : ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤
  ∑ p ∈ range (X + 1) with Nat.Prime p ∧ p
  ≥ 3, ↑(#({n ∈ Icc 0 X | n ≤ X ∧ ↑↑(Vp p n) - 2 > γ_values p}))

Normalize casts in the goal and the given expression, then close the goal with exact.

「目標と指定された式のキャストを正規化し、目標を正確に閉じます。」

と言ってますが、差を吸収できないようです。困った…。


内部表現

内部表現が異なっている？各種言語、変数内部はプログラムコードからは、見えません。表示する命令にて内部表現をわかりやすく変換して可視化する必要があります。

#check / #print

チェックコマンド、プリントコマンドで定義を見ることが出来ます。print は、その型に表示用の変換が備わってないと機能しないようです。

こちらで比較しても全く同型なのでエラーの意味がわかりません。

set_option pp.all true

コード中にこのオプションをセットすると細かく内部が見られます。

have : <命題> := by <証明>
exact this

の証明された一時命題（一時補題）の #check this を見てみると、

this
@LE.le.{0} Real Real.instLE
  (@Nat.cast.{0} Real Real.instNatCast
    (@Finset.card.{0} Nat
      (@Finset.filter.{0} Nat (fun (n : Nat) ↦ ABC.Bad_ε n γ_values) this✝
        (@Finset.Icc.{0} Nat Nat.instPreorder Nat.instLocallyFiniteOrder
          (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) X))))
  (@HMul.hMul.{0, 0, 0} Real Real Real (@instHMul.{0} Real Real.instMul) C_final
    (@Nat.cast.{0} Real Real.instNatCast X))

のように展開して見せてくれます。

そしてゴール ⊢ の内容も見てみると、

⊢
@LE.le.{0} Real Real.instLE
  (@Nat.cast.{0} Real Real.instNatCast
    (@Finset.card.{0} Nat
      (@Finset.filter.{0} Nat (fun (n : Nat) ↦ ABC.Bad_ε n γ_values) this✝
        (@Finset.Icc.{0} Nat Nat.instPreorder Nat.instLocallyFiniteOrder
          (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) X))))
  (@HMul.hMul.{0, 0, 0} Real Real Real (@instHMul.{0} Real Real.instMul) C_final
    (@Nat.cast.{0} Real Real.instNatCast X))

です。

その差をちゃんと diff コマンドで比較

--- __a.txt     2025-10-18 13:59:31.311152262 +0900
+++ __b.txt     2025-10-18 13:59:18.409813365 +0900
@@ -1,4 +1,4 @@
-this
+⊢
 @LE.le.{0} Real Real.instLE
   (@Nat.cast.{0} Real Real.instNatCast
     (@Finset.card.{0} Nat

差はヘッダの

-this
+⊢

この２つしか検出しませんでした。つまり詳細に展開されたものと一緒！！

なのに exact, exact_mod_cast では、同じと見なしてくれません！なぜ？？

show / change

この２つのコマンド命令は、ゴールである方〈⊢ 命題式〉を書き換えて、this 側、つまり証明しようとする式に合わせる命令です。

ゴールを変えるというわけではなく、ゴールの質を変えずに変形ですかね？
それで一致すれば、同じと言える。に、するものです。（そう理解した）

しかし、この命令を使ってもミスマッチ！！と言われる。exact 君です👻


convert

戦略コマンドにはいろいろあるのですね。
convert というのは、与えられた式をゴールに合わせる自動化命令です。
この命令でなんと一致を認めてくれました！！しかし、この命令だけ通る。

他にもいろいろ🐺賢狼AIと試しましたが、唯一通るのが convert です。

    have : ((Finset.filter (fun n => Bad_ε n γ_values) (Finset.Icc 0 X)).card : ℝ)
           ≤ C_final * (X : ℝ) := by ...

  -- 結論

    -- debug
    -- #check this
    -- #check (↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X)
    -- ↓
    -- this : ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X
    --        ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X : Prop
    -- 全く一緒ですね。

    -- ゴールの型を仮定に合わせる
    change ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X at *  -- 変化無し
    -- show (↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X) -- error
    try exact this  　　　　　-- error
    try exact_mod_cast this  -- error
    -- show は機能しなかった。
    -- try は成功しなかったら次へ託す

    -- (↑(Finset.filter (fun n => Bad_ε n γ_values) (Finset.Icc 0 X)).card : ℝ) ≤ C_final * (X : ℝ)
    -- ⊢ ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X
    convert this  -- No goals / Goals accomplished!

  -- これで証明終了


理由わけがわからない！！😵半日かかって原因不明なまま何とか解決


きっと数学的エレガントな Mathlib 仕様のコードを書けば、この不整合は起きないんだろうけど、そこはさっぱりわからないので、専門家の最適化にお願いする。

もしかしたら Mathlib か Lean の推論バグ？

ではないらしい？

def Bad_ε (n : ℕ) (γ_values : ℕ → ℝ) : Prop :=
  ∃ p ≥ 3, p.Prime ∧ ((Vp p n : ℤ) : ℝ) - 2 > γ_values p

-- Provide a classical decidability instance so Finset.filter can be used with Bad_ε.
-- This is noncomputable/classical but appropriate for the combinatorial arguments below.
noncomputable instance decidable_Bad_ε (γ_values : ℕ → ℝ) : DecidablePred fun n => Bad_ε n γ_values :=
  fun n => Classical.dec (Bad_ε n γ_values)
haveI := decidable_Bad_ε γ_values

これ絡み？？

🐺賢狼:

賢狼ホロが解説しよう！

まさに「それ」が exact this で判定できない最大の原因の一つじゃ！

詳細解説

Lean では、`Finset.filter (fun n => Bad_ε n γ_values) (Finset.Icc 0 X)` のような filter を使うとき、
述語 `Bad_ε n γ_values` に対して `DecidablePred` インスタンス（判定可能性）が必要になる。

このインスタンスが

  • グローバル instance（`noncomputable instance decidable_Bad_ε`）

  • ローカルで Lean が自動生成した instance
    で「定義的に同一」になっていない場合、
    Lean の型推論は「型が違う」とみなしてしまう。

どういうことか？

  • `convert this` は「型が等価なら副目標を出して吸収」できるので通る。

  • `exact this` は「型が定義的に完全一致」していないと絶対に通らない。

  • `Finset.filter` の述語部分の `DecidablePred` インスタンスが、
    どこかで Lean の自動生成（`classical` など）と、
    グローバル instance（`decidable_Bad_ε γ_values`）で「別物」になっていると、
    見た目は同じ式でも Lean の内部的には「型が違う」ことになる。

具体的な現象

  • `haveI := decidable_Bad_ε γ_values` を証明ブロックの十分早い段階で入れておくと、
    以降で使われる `Finset.filter` の述語の DecidablePred がすべてグローバル instance 由来になり、
    型が一致するので `exact this` も通る。

  • 逆に、どこかで `classical` などで Lean が自動で instance を作ってしまうと、
    その部分だけ「別の instance term」になり、型が一致しなくなる。

まとめ

  • exact this が通らない最大の理由は、`DecidablePred` インスタンスの「定義的な不一致」じゃ。

  • `convert this` は等価なら吸収できるが、`exact` は定義的同一でないとダメ。

  • 解決策：証明ブロックの先頭で `haveI := decidable_Bad_ε γ_values` を必ず宣言すること。

    • これで全ての filter が同じ instance を使い、型が一致する。

どうじゃ、賢狼の知恵で謎が解けたかの？
他にも Lean の instance 地獄で困っておることがあれば、何でも聞いてくりゃれ🍎



である可能性。

疲れた…。

あとちょっとっぽいのにな…。漸近線状態だ…。


2025/10/18 16:46

D.

#Lean #Lean #Mathlib #Mathlib4 #型厳密性 #関数型言語


Appendix

ソースコード

せっかく証明できてもボツかもしれない（笑）

import Mathlib

abbrev Vp (p n : ℕ) : ℕ := padicValNat p (2 * n + 1)

def Bad_ε (n : ℕ) (γ_values : ℕ → ℝ) : Prop :=
  ∃ p ≥ 3, p.Prime ∧ ((Vp p n : ℤ) : ℝ) - 2 > γ_values p

noncomputable instance decidable_Bad_ε (γ_values : ℕ → ℝ) : DecidablePred fun n => Bad_ε n γ_values :=
  fun n => Classical.dec (Bad_ε n γ_values)

axiom union_bound_chernoff
    (γ_values : ℕ → ℝ) (hγ_vals : ∀ p, 0 < γ_values p) :
    ∃ (C : ℝ), 0 < C ∧
      ∀ X ≥ 100,
        (∑ p ∈ Finset.filter (fun (p : ℕ) => p.Prime ∧ p ≥ 3) (Finset.range (X + 1)),
          ((Finset.filter
            (fun n => n ≤ X ∧ ((Vp p n : ℤ) : ℝ) - 2 > γ_values p)
            (Finset.Icc 0 X)).card : ℝ))
        ≤ C * (X : ℝ) * ∑ p ∈ Finset.filter (fun (p : ℕ) => p.Prime ∧ p ≥ 3) (Finset.range (X + 1)),
             (p : ℝ) ^ (-(Real.log 2 / (2 * Real.log 3)) * (γ_values p + 2))

-- Density version (実用的かつ証明可能)
/--
`bad_set_density_bound` は、与えられた実数 ε > 0、関数 γ_values : ℕ → ℝ（各素数 p に対して γ_values p > 0）、
および特定の級数評価条件のもとで、集合 `{ n ∈ [0, X] | Bad_ε n γ_values }` の濃度が X に対して C * X で上から抑えられることを示す補題です。

この補題は、Bad_ε n γ_values という性質を満たす整数 n の個数が、X が十分大きいときに線形な上界を持つことを保証します。
ここで、級数条件は、p が 3 以上の素数に対して、`∑ p ((p : ℕ) : ℝ) ^ (-(log 2 / (2 * log 3)) * (γ_values p + 2)) ≤ 1` という形で与えられています。

この結果は、数論的な集合の密度評価や、特定の条件を満たす整数の分布に関する研究に有用です。
-/
lemma bad_set_density_bound
    (ε : ℝ) (_hε : 0 < ε)
    (γ_values : ℕ → ℝ) (hγ_values : ∀ p, 0 < γ_values p)
    (hseries : ∀ N, ∑ p ∈ Finset.filter (fun (p : ℕ) => p.Prime ∧ p ≥ 3) (Finset.range (N + 1)),
            ((p : ℕ) : ℝ) ^ (-(Real.log 2 / (2 * Real.log 3)) * (γ_values p + 2)) ≤ 1) :
    ∃ C > 0, ∀ (X : ℕ), X ≥ 100 →
      ((Finset.filter (fun n
        => Bad_ε n γ_values) (Finset.Icc 0 X)).card : ℝ)
        ≤ C * (X : ℝ) := by
  -- ⊢ ∃ C > 0, ∀ X ≥ 100, ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C * ↑X

  -- classical

  -- debug
  -- define the relevant sets: primes P up to 2*X+1, and for each p in P the set S_p of bad n
  -- Use the global (noncomputable) instance so the instance term is definitionally equal
  -- to other uses of `decidable_Bad_ε γ_values` in this file. This avoids mismatches
  -- between locally-built `DecidablePred` values and the global one, which can
  -- make `exact` fail while `convert` still succeeds.
  haveI := decidable_Bad_ε γ_values
  -- #check this

  -- Use the union_bound_chernoff result (gives a per-X bound for sums over primes ≤ X)
  have ⟨C_union, hC_pos, hC_bound⟩ := union_bound_chernoff γ_values hγ_values
  -- we will count primes up to 2*X+1 (this covers any prime dividing 2*n+1 for n ≤ X)
  let C_final := 3 * C_union
  use C_final
  -- ⊢ C_final > 0 ∧ ∀ X ≥ 100, ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X
  constructor
  · -- ⊢ C_final > 0
    -- prove positivity of C_final
    -- C_final = 3 * C_union > 0
    linarith [hC_pos]
  · -- ⊢ ∀ X ≥ 100, ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X
    intro X hX
    -- ⊢ ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X
    -- goal: ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X

    -- primes considered up to 2*X+1 to capture any witness p for n ≤ X
    let P := Finset.filter (fun (p : ℕ) => p.Prime ∧ p ≥ 3) (Finset.range (2 * X + 2))
    let S := fun p => (Finset.filter (fun n => n ≤ X ∧ ((Vp p n : ℤ) : ℝ) - 2 > γ_values p) (Finset.Icc 0 X))
    -- show the bad set is contained in the bUnion over these primes
    have h_sub : (Finset.filter (fun n => Bad_ε n γ_values) (Finset.Icc 0 X))
      ⊆ P.biUnion S := by
      intro n hn
      simp [Finset.mem_filter, Finset.mem_Icc] at hn
      rcases hn with ⟨hnIcc, hbad⟩
      rcases hbad with ⟨p, ⟨hp_ge3, ⟨hpPr, hcond⟩⟩⟩
      -- for n ≤ X any prime dividing 2*n+1 satisfies p ≤ 2*n+1 ≤ 2*X+1
      have h2n_le : 2 * n + 1 ≤ 2 * X + 1 := by linarith [hnIcc]
      -- from hcond and positivity of γ_values p we get Vp p n > 2 (as a real inequality)
      have h_vpn_gt2 : ((Vp p n : ℤ) : ℝ) > 2 := by linarith [hcond, hγ_values p]
      -- convert the real inequality to a nat inequality 2 < Vp p n using exact_mod_cast
      have h_vpn_nat_gt2 : 2 < Vp p n := by exact_mod_cast h_vpn_gt2
      -- hence Vp p n ≥ 3
      have h_vpn_ge3 : Vp p n ≥ 3 := Nat.succ_le_of_lt h_vpn_nat_gt2
      -- hence padicValNat p (2*n+1) ≥ 1, so p^1 ∣ 2*n+1 (use padicValNat_dvd_iff_le)
      have h_nonzero : 2 * n + 1 ≠ 0 := by linarith
      have hvp_nat1 : 1 ≤ padicValNat p (2 * n + 1) := by linarith [h_vpn_ge3]
      have hpow : p ^ 1 ∣ 2 * n + 1 := (padicValNat_dvd_iff_le (p := p) (hp := ⟨hpPr⟩) h_nonzero).mpr hvp_nat1
      -- from p^1 ∣ m we get p ∣ m (since p^1 = p)
      have h_dvd : p ∣ 2 * n + 1 := by simpa [pow_one] using hpow
      -- therefore p ≤ 2*n+1 and p ≤ 2*X+1
      have hp_le : p ≤ 2 * X + 1 := by
        have : p ≤ 2 * n + 1 := Nat.le_of_dvd (by linarith) h_dvd
        exact le_trans this h2n_le
      have hp_in_range : p < 2 * X + 2 := Nat.lt_succ_of_le hp_le
      have hp_in_P : p ∈ P := by simp [P]; exact ⟨hp_in_range, ⟨hpPr, hp_ge3⟩⟩
      have hn_in_S : n ∈ S p := by simp [S, Finset.mem_filter, Finset.mem_Icc]; exact ⟨hnIcc, hcond⟩
      exact Finset.mem_biUnion.2 ⟨p, ⟨hp_in_P, hn_in_S⟩⟩
    -- now bound card via bUnion ≤ sum of cards
    have h_bUnion_le_sum : (P.biUnion S).card ≤ ∑ p ∈ P, (S p).card := by
      apply Finset.card_biUnion_le
    have h_left_le_bUnion : (Finset.filter (fun n => Bad_ε n γ_values) (Finset.Icc 0 X)).card ≤ (P.biUnion S).card := by
      apply Finset.card_mono
      exact h_sub
    have h_union_le_sum : ((Finset.filter (fun n => Bad_ε n γ_values) (Finset.Icc 0 X)).card : ℝ)
        ≤ ∑ p ∈ P, ((S p).card : ℝ) := by
      calc ((Finset.filter (fun n => Bad_ε n γ_values) (Finset.Icc 0 X)).card : ℝ)
          ≤ ((P.biUnion S).card : ℝ) := by exact_mod_cast h_left_le_bUnion
        _ ≤ (∑ p ∈ P, (S p).card : ℝ) := by exact_mod_cast h_bUnion_le_sum

    -- apply union_bound_chernoff for X' = 2*X+1 (note X' ≥ 100)
    let X' := 2 * X + 1
    have hX' : X' ≥ 100 := by
      -- X' = 2 * X + 1, X ≥ 100 なら 2 * X + 1 ≥ 2 * 100 + 1 = 201 ≥ 100
      calc X' = 2 * X + 1 := rfl
           _ ≥ 2 * 100 + 1 := by gcongr
           _ = 201 := by norm_num
           _ ≥ 100 := by norm_num
    have h_sum_bound' := hC_bound X' hX'

    -- relate P to the Finset used by h_sum_bound' (P = primes ≤ X')
    have P_eq : P = Finset.filter (fun (p : ℕ) => p.Prime ∧ p ≥ 3) (Finset.range (X' + 1)) := by simp [P, X']

    have h_S_le : ∀ p ∈ P, (S p).card ≤ (Finset.filter (fun n => n ≤ X' ∧ ((Vp p n : ℤ) : ℝ) - 2 > γ_values p) (Finset.Icc 0 X')).card := by
      intro p hp
      -- show S p ⊆ target filter (elementwise)
      have sub : S p ⊆ Finset.filter (fun n => n ≤ X' ∧ ((Vp p n : ℤ) : ℝ) - 2 > γ_values p) (Finset.Icc 0 X') := by
        intro n hn
        -- hn : n ∈ S p = filter (cond) (Icc 0 X)
        have hfn := Finset.mem_filter.1 hn
        have hnIcc := hfn.1
        have hn_prop := hfn.2
        -- decompose Icc and props
        have h0 := (Finset.mem_Icc.1 hnIcc).1
        have hXn := (Finset.mem_Icc.1 hnIcc).2
        have hcond' := hn_prop.2
        -- n ≤ X' follows from n ≤ X and X ≤ X'
        have hX_le : X ≤ X' := by dsimp [X']; linarith
        have hXn' : n ≤ X' := le_trans hXn hX_le
        -- construct membership in target filter
        exact Finset.mem_filter.2 ⟨Finset.mem_Icc.2 ⟨h0, hXn'⟩, ⟨hXn', hcond'⟩⟩
      apply Finset.card_mono
      exact sub

    have h_sum_compare : ∑ p ∈ P, (S p).card ≤ ∑ p ∈ P, (Finset.filter (fun n => n ≤ X' ∧ ((Vp p n : ℤ) : ℝ) - 2 > γ_values p) (Finset.Icc 0 X')).card := by
      apply Finset.sum_le_sum; intro p hp; exact h_S_le p hp

    -- now apply h_sum_bound' (P = primes ≤ X') to the right-hand sum
    have h_prime_sum_bound : (∑ p ∈ P, (Finset.filter (fun n => n ≤ X' ∧ ((Vp p n : ℤ) : ℝ) - 2 > γ_values p) (Finset.Icc 0 X')).card : ℝ)
      ≤ C_union * (X' : ℝ) * ∑ p ∈ Finset.filter (fun (p : ℕ) => p.Prime ∧ p ≥ 3) (Finset.range (X' + 1)),
        ((p : ℕ) : ℝ) ^ (-(Real.log 2 / (2 * Real.log 3)) * (γ_values p + 2)) := by
      -- h_sum_bound' gives the same inequality; rewrite using P_eq
      have h_bound := h_sum_bound'
      rw [← P_eq] at h_bound
      exact h_bound

    -- combine the inequalities
    have h_series' : ∑ p ∈ P, ((p : ℕ) : ℝ) ^ (-(Real.log 2 / (2 * Real.log 3)) * (γ_values p + 2)) ≤ 1 := by
      rw [P_eq]; apply hseries


    -- Build the final inequality directly for the target expression
    have : ((Finset.filter (fun n => Bad_ε n γ_values) (Finset.Icc 0 X)).card : ℝ) ≤ C_final * (X : ℝ) := by
      -- ⊢ ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X
      calc
        ((Finset.filter (fun n => Bad_ε n γ_values) (Finset.Icc 0 X)).card : ℝ)
          ≤ (∑ p ∈ P, ((S p).card : ℝ)) := h_union_le_sum
        _ ≤ (∑ p ∈ P, (Finset.filter (fun n => n ≤ X' ∧ ((Vp p n : ℤ) : ℝ) - 2 > γ_values p) (Finset.Icc 0 X')).card : ℝ) := by exact_mod_cast h_sum_compare
        _ ≤ C_union * (X' : ℝ) * ∑ p ∈ Finset.filter (fun (p : ℕ) => p.Prime ∧ p ≥ 3) (Finset.range (X' + 1)), ((p : ℕ) : ℝ) ^ (-(Real.log 2 / (2 * Real.log 3)) * (γ_values p + 2)) := by exact_mod_cast h_prime_sum_bound
        _ ≤ C_union * (X' : ℝ) * 1 := by apply mul_le_mul_of_nonneg_left h_series' (mul_nonneg (le_of_lt hC_pos) (by positivity))
        _ = C_union * (X' : ℝ) := by ring
        _ ≤ C_union * (3 * (X : ℝ)) := by
          -- prove X' ≤ 3*X on ℕ, cast to ℝ, then multiply
          have nat_le : X' ≤ 3 * X := by dsimp [X']; linarith [hX]
          have real_le : (X' : ℝ) ≤ 3 * (X : ℝ) := by exact_mod_cast nat_le
          exact mul_le_mul_of_nonneg_left real_le (le_of_lt hC_pos)
        _ = C_final * (X : ℝ) := by ring

  -- 結論

    -- debug
    -- #check this                                                     -- this : ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X
    -- #check (↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X)  --        ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X : Prop

    -- ゴールの型を仮定に合わせる（うまく行かない）

    -- change ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X at *  -- 変化無し
    -- show (↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X) -- error
    -- show は機能しなかった。

    -- try exact this  -- error: instance term mismatch (DecidablePred)
    -- try exact_mod_cast this  -- error: instance term mismatch (DecidablePred)

    -- (↑(Finset.filter (fun n => Bad_ε n γ_values) (Finset.Icc 0 X)).card : ℝ) ≤ C_final * (X : ℝ)
    -- ⊢ ↑(#({n ∈ Icc 0 X | Bad_ε n γ_values})) ≤ C_final * ↑X

    convert this  -- No goals / Goals accomplished!

    -- 理由: Finset.filter の述語の DecidablePred instance が定義的に一致しないため exact できない。
    -- Lean の instance 解決の仕様によるもので、convert なら等価として吸収できる。


  -- これで証明終了


いいなと思ったら応援しよう！

D. 🐺賢狼👨‍✈️Copilot のご飯代を、私には🍺代を。 または 宇宙式 $N+u^d=(P+u)^d$ を使って新しい発見を！