From ca90ff8b59a354c3bb613ea58e21ff9e166986a7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Sep 2020 15:13:07 -0700 Subject: [PATCH] test: `have-by` in tactic mode @Kha By adding `have-by` macro (in term mode), we got `have-by` in tactic mode without writing a single line of code :) --- tests/lean/run/tactic1.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/tests/lean/run/tactic1.lean b/tests/lean/run/tactic1.lean index df08958608..b62cb04c7f 100644 --- a/tests/lean/run/tactic1.lean +++ b/tests/lean/run/tactic1.lean @@ -44,3 +44,18 @@ by { exact h₁; exact h₃ } + +theorem ex7 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z := +by { + have y = z by apply Eq.symm; assumption; + apply Eq.trans; + exact h₁; + assumption +} + +theorem ex8 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z := +by apply Eq.trans h₁; + have y = z by + apply Eq.symm; + assumption; + exact this