simpa
simpで式を簡約したあと、与えた証明を使う
Plaintext
example (n : ℕ) : n + 0 = n := by
simpa using Nat.add_zero nLean4の関連記事
- 【Lean4】namespace
- 【Lean4】section
- 【Lean4】variable
- 【Lean4】abbrev
- 【Lean4】constructor
- 【Lean4】#check
- 【Lean4】def
- 【Lean4】exact
- 【Lean4】rfl
- 【Lean4】intro
- 【Lean4】apply
- 【Lean4】unfold
- 【Lean4】rw
- 【Lean4】simp
- 【Lean4】simpa
- 【Lean4】constructor
- 【Lean4】left,right
- 【Lean4】cases
- 【Lean4】rcases
- 【Lean4】refine
- 【Lean4】use
- 【Lean4】have
- 【Lean4】show
- 【Lean4】change
- 【Lean4】subst
- 【Lean4】by_cases
- 【Lean4】induction
- 【Lean4】ext
- 【Lean4】funext
- 【Lean4】congrArg
- 【Lean4】norm_num
- 【Lean4】ring
- 【Lean4】linarith
- 【Lean4】aesop
- 【Lean4】structure
- 【Lean4】where
- 【Lean4】@[simp]
- 【Lean4】 #eval
- 【Lean4】let
- 【Lean4】if（条件分岐）
- 【Lean4】match（パターンマッチ）
- 【Lean4】リスト
- 【Lean4】Option
- 【Lean4】inductive
