From c231a9f88457eb0d87b317e3a7e7e38a5cd7bc6a Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 13 Jan 2025 16:18:07 +0100 Subject: [PATCH] fix spaces in 'Rational' example #48 --- Projects/mathlib-demo/MathlibLatest/Rational.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Projects/mathlib-demo/MathlibLatest/Rational.lean b/Projects/mathlib-demo/MathlibLatest/Rational.lean index 0ea15def..cb1c5482 100644 --- a/Projects/mathlib-demo/MathlibLatest/Rational.lean +++ b/Projects/mathlib-demo/MathlibLatest/Rational.lean @@ -9,7 +9,7 @@ variable (x y z : ℚ) example (h₁ : x < y) (h₂ : y + 3 < z + 10) : x + 37 < z + 44 := by linarith -- the `linarith` tactic can do this automatically --- let's prove that (x+y)^2=x^2+2*x*y+y^2 +-- let's prove that (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 -example : (x + y)^2 = x^2 + 2 * x * y + y^2 := by +example : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by ring -- the `ring` tactic can do this automatically