by_cases
命題が成り立つ場合と成り立たない場合に分ける
Plaintext
example (P : Prop) [Decidable P] : P ∨ ¬P := by
by_cases h : P
· left
exact h
· right
exact h
/-
証明状態が
1つ目：
h : P
2つ目：
h : ¬P
に分かれる
-/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
