rearrangement_algebratheoremProved here from basic factspropext, Classical.choice, Quot.sound
rearrangement_algebraLean 4Proved here from basic factsFormally verified
/-- **The first rearrangement proof, algebraic step.** If a square of side `a + b` is made upof a tilted square of side `c` and four right triangles with legs `a`, `b` (area `ab/2` each),then `a² + b² = c²`.`(a + b)² = a² + 2ab + b²`, and the four triangles account for `4 · ab/2 = 2ab`. -/theorem rearrangement_algebra (a b c : Rat) (h : (a + b) ^ 2 = c ^ 2 + 4 * (a * b / 2)) : a ^ 2 + b ^ 2 = c ^ 2 := by have expand : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * (a * b) := by grind have four : 4 * (a * b / 2) = 2 * (a * b) := by grind calc a ^ 2 + b ^ 2 = (a + b) ^ 2 - 2 * (a * b) := by rw [expand]; grind _ = c ^ 2 + 4 * (a * b / 2) - 2 * (a * b) := by rw [h] _ = c ^ 2 := by rw [four]; grind
rearrangement_square_in_middletheoremProved here from basic factspropext, Classical.choice, Quot.sound
rearrangement_square_in_middleLean 4Proved here from basic factsFormally verified
/-- **The second dissection proof, algebraic step** (the “hypotenuse diagram”). If a square ofside `c` is made up of four right triangles with legs `a`, `b` and a small square of side`b - a` in the middle, then `a² + b² = c²`, because `(b - a)² + 2ab = a² + b²`. -/theorem rearrangement_square_in_middle (a b c : Rat) (h : c ^ 2 = (b - a) ^ 2 + 4 * (a * b / 2)) : a ^ 2 + b ^ 2 = c ^ 2 := by rw [h] grind
distance_exampletheoremProved here from basic factspropext, Classical.choice, Quot.sound
distance_exampleLean 4Proved here from basic factsFormally verified
/-- The distance from `(1, 2)` to `(4, 6)` is `5`: the legs are `3` and `4`, and`3² + 4² = 25 = 5²`. -/theorem distance_example : sqDist ⟨1, 2⟩ ⟨4, 6⟩ = 5 ^ 2 := by decide +kernel
/-- The angle `ACB` is a right angle: the step from `C` to `B` is the step from `C` to `A`turned through a quarter turn (`(p, q) ↦ (-q, p)`) and scaled by some factor `t`. -/def IsRightAngleAt (A B C : Point) : Prop := ∃ t : Rat, B.x - C.x = -t * (A.y - C.y) ∧ B.y - C.y = t * (A.x - C.x)
pythagoras_coordinatestheoremProved here from basic factspropext, Classical.choice, Quot.sound
pythagoras_coordinatesLean 4Proved here from basic factsFormally verified
/-- **The Pythagorean theorem in coordinates.** If the angle at `C` is a right angle, then`AB² = CA² + CB²`.Write `A - C = (p, q)`, so `B - C = (-tq, tp)`. Then `CA² = p² + q²`, `CB² = t²(p² + q²)` and`AB² = (-tq - p)² + (tp - q)² = (1 + t²)(p² + q²)`: the cross terms `±2tpq` cancel. -/theorem pythagoras_coordinates (A B C : Point) (h : IsRightAngleAt A B C) : sqDist A B = sqDist C A + sqDist C B := by obtain ⟨t, h1, h2⟩ := h unfold sqDist have e1 : B.x - A.x = (B.x - C.x) - (A.x - C.x) := by grind have e2 : B.y - A.y = (B.y - C.y) - (A.y - C.y) := by grind rw [e1, e2, h1, h2] grind
sq_nonnegtheoremProved here from basic factspropext, Classical.choice, Quot.sound
sq_nonnegLean 4Proved here from basic factsFormally verified
/-- A square is never negative: `0 ≤ p · p` (a positive times a positive, or a negative times anegative). -/theorem sq_nonneg (p : Rat) : 0 ≤ p * p := by by_cases h : 0 ≤ p · exact Rat.mul_nonneg h h · have h' : 0 ≤ -p := by grind have := Rat.mul_nonneg h' h' grind
sum_sq_postheoremProved here from basic factspropext, Classical.choice, Quot.sound
sum_sq_posLean 4Proved here from basic factsFormally verified
/-- If `p` and `q` are not both `0`, then `p² + q² > 0`. -/theorem sum_sq_pos (p q : Rat) (h : p ≠ 0 ∨ q ≠ 0) : 0 < p * p + q * q := by have hp := sq_nonneg p have hq := sq_nonneg q have pos : ∀ r : Rat, r ≠ 0 → 0 < r * r := by intro r hr by_cases h' : 0 < r · exact Rat.mul_pos h' h' · have h'' : 0 < -r := by grind have := Rat.mul_pos h'' h'' grind rcases h with h | h · have := pos p h grind · have := pos q h grind
converse_coordinatestheoremProved here from basic factspropext, Classical.choice, Quot.sound
converse_coordinatesLean 4Proved here from basic factsFormally verified
/-- **The converse in coordinates.** If `A ≠ C` and `AB² = CA² + CB²`, then the angle at `C`is a right angle.Expanding, `AB² = CA² + CB² - 2(p·r + q·s)` where `(p, q) = A - C` and `(r, s) = B - C`; so thehypothesis says exactly `p·r + q·s = 0`, and `quarter_turn_of_dot_zero` finishes. -/theorem converse_coordinates (A B C : Point) (hAC : A ≠ C) (h : sqDist A B = sqDist C A + sqDist C B) : IsRightAngleAt A B C := by have hpq : A.x - C.x ≠ 0 ∨ A.y - C.y ≠ 0 := by by_cases hx : A.x - C.x = 0 · right intro hy apply hAC cases A cases C simp only at hx hy grind · left exact hx have hdot : (A.x - C.x) * (B.x - C.x) + (A.y - C.y) * (B.y - C.y) = 0 := by unfold sqDist at h grind exact quarter_turn_of_dot_zero _ _ _ _ hpq hdot
not_right_exampletheoremProved here from basic factsNo axioms
not_right_exampleLean 4Proved here from basic factsFormally verified
/-- A triangle with sides `5, 6, 8` has **no** right angle: `5² + 6² = 61`, but `8² = 64`.(By the converse, a right angle would force `61 = 64`; and the right angle could only beopposite the longest side.) -/theorem not_right_example : 5 ^ 2 + 6 ^ 2 ≠ 8 ^ 2 := by decide
triple_scaletheoremProved here from basic factspropext, Classical.choice, Quot.sound
triple_scaleLean 4Proved here from basic factsFormally verified
/-- Scaling a triple gives a triple: if `a² + b² = c²` then `(ka)² + (kb)² = (kc)²`. -/theorem triple_scale (a b c k : Nat) (h : a ^ 2 + b ^ 2 = c ^ 2) : (k * a) ^ 2 + (k * b) ^ 2 = (k * c) ^ 2 := by calc (k * a) ^ 2 + (k * b) ^ 2 = k ^ 2 * (a ^ 2 + b ^ 2) := by grind _ = k ^ 2 * c ^ 2 := by rw [h] _ = (k * c) ^ 2 := by grind
infinitely_many_triplestheoremProved here from basic factspropext, Classical.choice, Quot.sound
infinitely_many_triplesLean 4Proved here from basic factsFormally verified
/-- **There are infinitely many Pythagorean triples**: beyond any number `N` there is a triplewith all sides positive and the first side bigger than `N`. Take `3k, 4k, 5k` with`k = N + 1`. -/theorem infinitely_many_triples (N : Nat) : ∃ a b c : Nat, N < a ∧ 0 < b ∧ a ^ 2 + b ^ 2 = c ^ 2 := by refine ⟨3 * (N + 1), 4 * (N + 1), 5 * (N + 1), by omega, by omega, ?_⟩ have h := triple_scale 3 4 5 (N + 1) (by decide) rw [Nat.mul_comm 3, Nat.mul_comm 4, Nat.mul_comm 5] exact h
sum_sq_lt_sq_sumtheoremProved here from basic factspropext, Classical.choice, Quot.sound
sum_sq_lt_sq_sumLean 4Proved here from basic factsFormally verified
/-- **`√(a² + b²)` is not `a + b`.** For positive `a, b`, `a² + b² < (a + b)²`: the square ofthe sum has the extra `2ab`. So the hypotenuse is always shorter than the two legs together. -/theorem sum_sq_lt_sq_sum (a b : Nat) (ha : 0 < a) (hb : 0 < b) : a ^ 2 + b ^ 2 < (a + b) ^ 2 := by have hab : 0 < a * b := Nat.mul_pos ha hb have expand : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * (a * b) := by grind omega
no_whole_sqrt_twotheoremProved here from basic factspropext, Quot.sound
no_whole_sqrt_twoLean 4Proved here from basic factsFormally verified
/-- The diagonal of a unit square has length `√2`, and `√2` is not a whole number: no wholenumber `n` has `n² = 2` (`1² = 1` is too small and `2² = 4` already too big). In fact `√2` is noteven a fraction — see the lesson on real numbers. -/theorem no_whole_sqrt_two : ¬ ∃ n : Nat, n ^ 2 = 2 := by intro ⟨n, h⟩ match n, h with | 0, h => exact absurd h (by decide) | 1, h => exact absurd h (by decide) | k + 2, h => have : 4 ≤ (k + 2) ^ 2 := by have := Nat.mul_le_mul (Nat.le_add_left 2 k) (Nat.le_add_left 2 k) rw [Nat.pow_two] exact this omega
/-- Show that `5² + 6² ≠ 8²`, so a triangle with sides `5, 6, 8` has no right angle.Hint: these are particular numbers — `decide` can compute both sides. -/theorem not_right_example : 5 ^ 2 + 6 ^ 2 ≠ 8 ^ 2 := by sorry
Show the compiled solution
not_right_exampleLean 4Proved here from basic factsFormally verified
/-- A triangle with sides `5, 6, 8` has **no** right angle: `5² + 6² = 61`, but `8² = 64`.(By the converse, a right angle would force `61 = 64`; and the right angle could only beopposite the longest side.) -/theorem not_right_example : 5 ^ 2 + 6 ^ 2 ≠ 8 ^ 2 := by decide
/-- Show that scaling a Pythagorean triple by `k` gives another triple.Hint: a `calc` chain: `(k * a) ^ 2 + (k * b) ^ 2 = k ^ 2 * (a ^ 2 + b ^ 2)` (by `grind`), thenuse `h`, then `k ^ 2 * c ^ 2 = (k * c) ^ 2` (by `grind`). -/theorem triple_scale (a b c k : Nat) (h : a ^ 2 + b ^ 2 = c ^ 2) : (k * a) ^ 2 + (k * b) ^ 2 = (k * c) ^ 2 := by sorry
Show the compiled solution
triple_scaleLean 4Proved here from basic factsFormally verified
/-- Scaling a triple gives a triple: if `a² + b² = c²` then `(ka)² + (kb)² = (kc)²`. -/theorem triple_scale (a b c k : Nat) (h : a ^ 2 + b ^ 2 = c ^ 2) : (k * a) ^ 2 + (k * b) ^ 2 = (k * c) ^ 2 := by calc (k * a) ^ 2 + (k * b) ^ 2 = k ^ 2 * (a ^ 2 + b ^ 2) := by grind _ = k ^ 2 * c ^ 2 := by rw [h] _ = (k * c) ^ 2 := by grind