From 71db452d9604c7cb85a2571ffcf96ac538a41e24 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Tue, 18 Apr 2023 05:38:21 -0600
Subject: [PATCH] Add similar/congruent definitions.

---
 common/Common.lean                    |  1 +
 common/Common/Data/Real/Geometry.lean | 27 +++++++++++++++++++++++++++
 2 files changed, 28 insertions(+)
 create mode 100644 common/Common/Data/Real/Geometry.lean

diff --git a/common/Common.lean b/common/Common.lean
index 9058953..fe57c61 100644
--- a/common/Common.lean
+++ b/common/Common.lean
@@ -1,3 +1,4 @@
+import Common.Data.Real.Geometry
 import Common.Data.Real.Set
 import Common.Data.Real.Sequence
 import Common.Tuple
diff --git a/common/Common/Data/Real/Geometry.lean b/common/Common/Data/Real/Geometry.lean
new file mode 100644
index 0000000..bd54511
--- /dev/null
+++ b/common/Common/Data/Real/Geometry.lean
@@ -0,0 +1,27 @@
+import Mathlib.Data.Real.Sqrt
+import Mathlib.Logic.Function.Basic
+
+namespace Real
+
+notation "ℝ²" => ℝ × ℝ
+
+noncomputable def dist (x y : ℝ²) :=
+  Real.sqrt ((abs (y.1 - x.1)) ^ 2 + (abs (y.2 - x.2)) ^ 2)
+
+def similar (S T : Set ℝ²) : Prop :=
+  ∃ f : ℝ² → ℝ², Function.Bijective f ∧
+    ∃ s : ℝ, ∀ x y : ℝ², x ∈ S ∧ y ∈ T →
+      s * dist x y = dist (f x) (f y)
+
+def congruent (S T : Set (ℝ × ℝ)) : Prop :=
+  ∃ f : ℝ² → ℝ², Function.Bijective f ∧
+    ∀ x y : ℝ², x ∈ S ∧ y ∈ T →
+      dist x y = dist (f x) (f y)
+
+theorem congruent_similar {S T : Set ℝ²} : congruent S T → similar S T := by
+  intro hc
+  let ⟨f, ⟨hf, hs⟩⟩ := hc
+  conv at hs => intro x y hxy; arg 1; rw [← one_mul (dist x y)]
+  exact ⟨f, ⟨hf, ⟨1, hs⟩⟩⟩
+
+end Real
\ No newline at end of file