lean - 例如： ((p ∨ q) → r) → (p → r) ∧ (q → r)

Answer 1

您没有p ∨ q此示例的假设。所以，你必须(assume hpqr, _)直接从 到and_intro。我的意思是，像

example (p q r : Prop) : ((p ∨ q) → r) → (p → r) ∧ (q → r) := 
assume hpqr,
and.intro (assume p, _) (assume q, _)