subst
等式を使って変数を置き換える
Plaintext
example (a b : ℕ) (h : a = b) : a + a = b + b := by
subst a
rfl
/-
subst aにより、a = bを使って文脈中のaがbに置き換わる
-/Lean4の関連記事
- 【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
