theorem-proving - LEANを使用して命題論理で2つのステートメントを証明する方法は?

Question

LEAN チュートリアルの第 3 章の最後にある 2 つの証明のうち、私がまだ苦労している (そのため、マニュアルを読み進められない) は次のとおりです。

theorem T11 : ¬(p ↔ ¬p) := sorry

正しい含意を証明する私の試みは、この時点で停止しました。

theorem T11R : ¬(p → ¬p) := 
begin 
    assume hyp : p → ¬ p, 
    cases (em p) with hp hnp, 
    exact (hyp hp) hp, 
    exact sorry 
end

明らかに、私はまだ を利用する方法を知りません¬p。左の含意を示す方法もわかりません。もう1つはこれです：

theorem T2R : ((p ∨ q) → r) → (p → r) ∧ (q → r) := 
begin
    intros porqr, sorry
end

以下を示すために（正しい意味として）使用していると思われます：

theorem T2 : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := 
begin    
    have goR : ((p ∨ q) → r) → (p → r) ∧ (q → r), from T2R p q r,
    have goL : (p → r) ∧ (q → r) → ((p ∨ q) → r), from T2L p q r,
    exact iff.intro (goR) (goL)
end

ここで私は左側に行きました：

theorem T2L : (p → r) ∧ (q → r) → ((p ∨ q) → r) := 
begin
    intros prqr,
    assume porq : p ∨ q,
    exact or.elim porq prqr.left prqr.right
end