【Lean4】rfl

rfl

Plaintext

example (x : ℕ) : x = x := by
  rfl

/-
x（左辺）とx（右辺）は同じ
-/

example (x : ℕ) : x = x := by
  rfl

/-
x（左辺）とx（右辺）は同じ
-/

定義を展開すると同じ式になる場合にも使える

Plaintext

def double (n : ℕ) : ℕ :=
  n + n

example (n : ℕ) : double n = n + n := by
  rfl

def double (n : ℕ) : ℕ :=
  n + n

example (n : ℕ) : double n = n + n := by
  rfl