Merge pull request #8 from BoltonBailey/main

Golf proof using field_simp

.gitignore

@@ -0,0 +1 @@
+.lake/**

SampCert/Samplers/Gaussian/Properties.lean

@@ -208,229 +208,21 @@ theorem alg_auto (num den : ℕ+) (x : ℤ) :
     rw [← Cast]
     rw [Y]
 
-    have A : y * τ * β * α * (β⁻¹ * ((τ ^ 2)⁻¹ * (α⁻¹ * ((2: ℝ))⁻¹)))
-      = y * ((2: ℕ+): ℝ)⁻¹ * τ⁻¹ := by
-      rw [mul_assoc]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      conv =>
-        right
-        rw [mul_assoc]
-      congr 1
-      simp [← mul_assoc]
-      conv =>
-        right
-        rw [mul_comm]
-      congr 1
-      conv =>
-        left
-        left
-        left
-        rw [mul_assoc]
-        rw [mul_assoc]
-        right
-        rw [mul_comm]
-        rw [mul_assoc]
-        right
-        simp
-      rw [mul_one]
-      conv =>
-        left
-        rw [mul_assoc]
-        rw [mul_assoc]
-        right
-        rw [mul_comm]
-        rw [mul_assoc]
-        simp
-      rw [pow_two]
-      rw [mul_inv]
-      rw [← mul_assoc]
-      rw [mul_inv_cancel Tau_ne0]
+    have Alpha_ne0 : α ≠ 0 := by
+      unfold_let
       simp
 
-    rw [A]
-    clear A
-
-    have B : α * (y * τ * β) * (β⁻¹ * ((τ ^ 2)⁻¹ * (α⁻¹ * ((2: ℝ))⁻¹)))
-      = y * ((2: ℕ+): ℝ)⁻¹ * τ⁻¹ := by
-      rw [mul_rotate]
-      rw [mul_assoc]
-      conv =>
-        left
-        right
-        rw [mul_assoc]
-        right
-        rw [mul_assoc]
-        right
-        rw [mul_comm]
-        rw [← mul_assoc]
-        simp
-      rw [mul_assoc]
-      conv =>
-        left
-        right
-        rw [← mul_assoc]
-        simp
-      rw [mul_assoc]
-      rw [mul_assoc]
-      congr 1
-      rw [← mul_assoc]
-      conv =>
-        right
-        rw [mul_comm]
-      congr 1
-      rw [pow_two]
-      rw [mul_inv]
-      rw [← mul_assoc]
-      rw [mul_inv_cancel Tau_ne0]
+    have Beta_ne0 : β ≠ 0 := by
+      unfold_let
       simp
 
-    rw [B]
-    clear B
-
-    have C : (y * τ * β * (y * τ * β) * (β⁻¹ * ((τ ^ 2)⁻¹ * (α⁻¹ * ((2: ℝ))⁻¹))))
-      = y ^ 2 * β * α⁻¹ * (((2: ℕ+): ℝ))⁻¹ := by
-      rw [pow_two]
-      rw [pow_two]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      congr 1
-      rw [mul_comm]
-      conv =>
-        right
-        rw [mul_comm]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      congr 1
-      rw [mul_comm]
-      congr 1
-      conv =>
-        left
-        right
-        right
-        right
-        right
-        rw [← mul_assoc]
-        rw [mul_comm]
-      rw [← mul_assoc]
-      rw [← mul_assoc]
-      rw [← mul_assoc]
-      rw [← mul_assoc]
-      rw [← mul_assoc]
-      congr 1
-      rw [mul_inv]
-      rw [← mul_assoc]
-      conv =>
-        left
-        left
-        rw [mul_assoc]
-        right
-        rw [mul_comm]
-        rw [(mul_inv_cancel Tau_ne0)]
-      rw [mul_one]
-      conv =>
-        left
-        left
-        left
-        rw [mul_assoc]
-        right
-        simp
-      rw [mul_one]
-      rw [(mul_inv_cancel Tau_ne0)]
-      simp
-
-    rw [C]
-    clear C
-
-    have D : α * α * (β⁻¹ * ((τ ^ 2)⁻¹ * (α⁻¹ * ((2: ℝ))⁻¹)))
-      = α * β⁻¹ * (τ ^ 2)⁻¹ * (((2: ℕ+): ℝ))⁻¹ := by
-      rw [mul_assoc]
-      rw [mul_assoc]
-      rw [mul_assoc]
-      congr 1
-      rw [← mul_assoc]
-      rw [← mul_assoc]
-      rw [← mul_assoc]
-      rw [← mul_assoc]
-      congr 1
-      rw [mul_assoc]
-      rw [mul_assoc]
-      rw [mul_comm]
-      rw [← mul_assoc]
-      rw [mul_assoc]
-      simp
-
-    rw [D]
-    clear D
-
-    rw [(sub_add (_ - _) _ _).symm]
-    rw [sub_eq_neg_add]
-    rw [sub_eq_neg_add]
-    rw [← add_assoc]
-    rw [← add_assoc]
-    rw [← add_assoc]
-
-    have E : y * τ⁻¹ + -(y * (((2: ℕ+): ℝ))⁻¹ * τ⁻¹) + -(y * (((2: ℕ+): ℝ))⁻¹ * τ⁻¹) = 0 := by
-      rw [add_assoc]
-      rw [(neg_add _ _).symm]
-      conv =>
-        left
-        right
-        right
-        congr
-        . rw [mul_assoc]
-          rw [mul_comm]
-          rw [mul_assoc]
-          right
-          rw [mul_comm]
-        . rw [mul_assoc]
-          rw [mul_comm]
-          rw [mul_assoc]
-          right
-          rw [mul_comm]
-      rw [(add_mul _ _ _).symm]
-      have X : (1/(2: ℕ+)) + (1/(2 : ℕ+)) = (1 : ℝ) := by
-        simp
-        rw [← two_mul]
-        exact mul_inv_cancel_of_invertible 2
-      conv =>
-        left
-        right
-        right
-        left
-        rw [inv_eq_one_div]
-      rw [X]
-      rw [one_mul]
-      simp
-
-    rw [E]
-    rw [zero_add]
-
-    rw [add_comm]
-    congr 1
-    . rw [← mul_assoc]
-      rw [← mul_assoc]
-      congr 1
-      rw [mul_comm]
-      rw [← mul_assoc]
-      congr 1
-      rw [mul_comm]
-    . rw [← mul_assoc]
-      congr 3
+    field_simp [Alpha_ne0, Beta_ne0, Tau_ne0]
+    have xsq_eq_ysq : (x : ℝ) ^ 2 = y ^ 2 := by
       rw [← Y]
       simp
+    rw [xsq_eq_ysq]
+    ring
+
 
   . simp [exp_nonneg]