with_unfolding_all の使用例

Zulip: decide that can see through irreducible

import Mathlib.Algebra.Group.Nat

structure A where
  n : ℕ
  deriving DecidableEq

instance : LE A where le x y := x.n ≤ y.n

instance : DecidableRel (@LE.le A _) := by
  intro x y
  exact x.n.decLe y.n

@[irreducible] def sqr (x : A) : A := ⟨x.n ^ 2⟩

example : sqr (⟨3⟩ : A) ≤ ⟨9⟩ := by native_decide  -- Works, but is native_decide
example : sqr (⟨3⟩ : A) ≤ ⟨9⟩ := by decide  -- Fails
example : sqr (⟨3⟩ : A) ≤ ⟨9⟩ := by rfl  -- Fails

-- Answer

example : sqr (⟨3⟩ : A) ≤ ⟨9⟩ := by with_unfolding_all decide

The issue supplies a complete Lean example demonstrating with_unfolding_all with an irreducible definition, but it names no destination file or test. First inspect the repository’s existing example organization, then add the example in the appropriate location and verify that it renders and checks successfully.