ワーキングメモリが一杯にならないために

infoviewに頼れ/りたくないとき、showを置く。
過剰にshowを置いた事例。やりすぎかもしれないけれども、クリスタルクリア、ブレインフレンドリー。
死んだ木に書かれたコードはここまでしてくれないと初学者には大変。
geminiによれば、すでにゴールがFalseならshow False、そうでないならexfalsoがよい。
なお、直接 left : P -> Falseとできればよいものの、それはできない様子。

-- de morgan
example (P Q : Prop) : ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q := by
  constructor
  --^ splitting iff into `mp` (modus ponens) and `mpr` (modus ponens reversed)
  case mp =>
    show ¬ (P ∨ Q) → ¬ P ∧ ¬ Q
    intro (h : ¬ (P ∨ Q))
    show ¬ P ∧ ¬ Q
    constructor -- splitting ∧ into `left` and `right`
    case left =>
      show P → False
      intro (p : P)
      show False
      exact (
        (h        : ¬ (P ∨ Q))
        (Or.inl p :    P ∨ Q)
        : False
      )
    case right =>
      show Q → False
      intro (q : Q)
      show False
      exact (
        (h        : ¬ (P ∨ Q))
        (Or.inr q :    P ∨ Q)
        : False
      )
  case mpr =>
    show (¬ P ∧ ¬ Q) → ((P ∨ Q) → False)
    intro (h₁ : ¬ P ∧ ¬ Q)
    show ((P ∨ Q) → False)
    intro (h₂ : P ∨ Q)
    show False
    cases h₂ with
    | inl p => exact ((h₁.left  : P → False) (p : P) : False)
    | inr q => exact ((h₁.right : Q → False) (q : Q) : False)

次の例では、mp枝のゴールはQだけどexfalsoがshow Falseよりというということだと思う。
なお、mprはhave+exactで型を明示したパターン。showやguard_target=\_sとの使い分けはまだ見えてこない。
また、contradictionはコンテキスト依存がexactより強いということらしく、脱コンテキストを目指すならexactの方が好ましいらしい（なぜかleanにはあまり強くないcopilot談）。

-- material conditional
example (P Q : Prop) : (¬ P ∨ Q) ↔ (P → Q) := by
  constructor
  case mp =>
    show¬ P ∨ Q → (P → Q)
    intro h₁
    intro p
    cases h₁ with
    | inl np => -- this term always results in False
      exfalso -- because we have both P and ¬ P
      exact (np p)
    | inr q => exact q
  case mpr =>
    have goal : (P → Q) → ¬ P ∨ Q := by
      intro h₁
      by_cases h₂ : P
      case pos => exact (Or.inr (h₁ h₂ : Q) : ¬ P ∨ Q)
      case neg => exact (Or.inl (h₂ : ¬ P)  : ¬ P ∨ Q)
    exact goal

参考文献