10 lines
155 B
Text
10 lines
155 B
Text
|
--
|
||
|
|
-- 5. Tactics
|
||
|
|
--
|
||
|
|
|
||
|
|
--
|
||
|
|
theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
|
||
|
|
apply And.intro
|
||
|
|
exact hp
|
||
|
|
exact { left := hq, right := hp }
|