【Lean4】constructor

constructor

目標が「かつ」や、複数の欄を持つ構造の場合に、目標を分割する

example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := by
  constructor
  · exact hP
  · exact hQ

example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := by
  constructor
  · exact hP
  · exact hQ

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