3.2. Absolute value / Modulus🔗

Definition 1.3.5. The modulus of z = a + bi is defined as |z| = \sqrt{a^2 + b^2}. It is also called the absolute value or the magnitude.

In Mathlib, we first define the squared norm by α^2+b^2, and then define the norm as the square root of the squared norm. The API normSq and ‖·‖ are used to refer to the squared norm and the norm respectively. Both of the examples below are true by definition.

example {z:ℂ} : normSq z = z.re * z.re + z.im * z.im := byz:ℂ⊢ normSq z = z.re * z.re + z.im * z.im
  -- By definition, normSq z = z.re^2 + z.im^2
  rflAll goals completed! 🐙

example {z:ℂ} : ‖z‖ = Real.sqrt (normSq z) := byz:ℂ⊢ ‖z‖ = √(normSq z)
  -- By definition, ‖z‖ = square root of (normSq z)
  rflAll goals completed! 🐙

Theorem 1.3.6.

(a): |z|^2 = z z^* for all z \in \mathbb{C}.
(b): For all z_1, z_2 \in \mathbb{C}, |z_1 z_2| = |z_1|\,|z_2|.

We use a theorem normSq_eq_norm_sq in Mathlib to finish the proof of part (a). In part (b), we use the API abs_of_nonneg.

Complex.normSq_eq_norm_sq (z : ℂ) : normSq z = ‖z‖ ^ 2#check normSq_eq_norm_sq
abs_of_nonneg.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] (h : 0 ≤ a) : |a| = a#check abs_of_nonneg

/-- Theorem 1.3.6, part (a)
   z z^* = |z|^2
-/
example (z : ℂ) : z * conj z = ‖z‖ ^ 2 := byz:ℂ⊢ z * (starRingEnd ℂ) z = ↑‖z‖ ^ 2
  rw [Complex.mul_conj]z:ℂ⊢ ↑(normSq z) = ↑‖z‖ ^ 2  -- z (conj z) = normSq z
  rw [← Complex.ofReal_pow]z:ℂ⊢ ↑(normSq z) = ↑(‖z‖ ^ 2)
  norm_castz:ℂ⊢ normSq z = ‖z‖ ^ 2
  -- reduce to show: normSq z = ‖z‖^2
  exact normSq_eq_norm_sq zAll goals completed! 🐙


/-- Theorem 1.3.6, part (b)
  |z₁ z₂| = |z₁| |z₂|
-/
-- detailed proof
example (z₁ z₂ : ℂ) : ‖z₁ * z₂‖  = ‖z₁‖ * ‖z₂‖ := byz₁:ℂz₂:ℂ⊢ ‖z₁ * z₂‖ = ‖z₁‖ * ‖z₂‖
  -- Since norms are non-negative, x = |x|.
  -- Rewrite the goal A = B to |A| = |B|
  rw [← abs_of_nonneg (norm_nonneg _)]z₁:ℂz₂:ℂ⊢ |‖z₁ * z₂‖| = ‖z₁‖ * ‖z₂‖
  rw [← abs_of_nonneg (mul_nonneg (norm_nonneg _)
     (norm_nonneg _))]z₁:ℂz₂:ℂ⊢ |‖z₁ * z₂‖| = |‖z₁‖ * ‖z₂‖|

  -- Apply the API: |A| = |B| ↔ A^2 = B^2
  rw [← sq_eq_sq_iff_abs_eq_abs]z₁:ℂz₂:ℂ⊢ ‖z₁ * z₂‖ ^ 2 = (‖z₁‖ * ‖z₂‖) ^ 2

  -- To prove real x = y, it suffices to prove ↑x = ↑y
  rw [← ofReal_inj]z₁:ℂz₂:ℂ⊢ ↑(‖z₁ * z₂‖ ^ 2) = ↑((‖z₁‖ * ‖z₂‖) ^ 2)

  -- Switch to Complex numbers to use conjugate properties
  push_castz₁:ℂz₂:ℂ⊢ ↑‖z₁ * z₂‖ ^ 2 = (↑‖z₁‖ * ↑‖z₂‖) ^ 2

  -- Finish the proof by calculations
  calc
    (‖z₁ * z₂‖ : ℂ) ^ 2
    _ = (z₁ * z₂) * conj (z₁ * z₂)
        := byz₁:ℂz₂:ℂ⊢ ↑‖z₁ * z₂‖ ^ 2 = z₁ * z₂ * (starRingEnd ℂ) (z₁ * z₂) rw [← mul_conj' (z₁*z₂)]All goals completed! 🐙
    _ = (z₁ * z₂) * (conj z₁ * conj z₂) := byz₁:ℂz₂:ℂ⊢ z₁ * z₂ * (starRingEnd ℂ) (z₁ * z₂) = z₁ * z₂ * ((starRingEnd ℂ) z₁ * (starRingEnd ℂ) z₂) rw [map_mul]All goals completed! 🐙
    _ = (z₁ * conj z₁) * (z₂ * conj z₂) := byz₁:ℂz₂:ℂ⊢ z₁ * z₂ * ((starRingEnd ℂ) z₁ * (starRingEnd ℂ) z₂) = z₁ * (starRingEnd ℂ) z₁ * (z₂ * (starRingEnd ℂ) z₂) ringAll goals completed! 🐙
    _ = (‖z₁‖ : ℂ)^2 * (‖z₂‖ : ℂ)^2
        := byz₁:ℂz₂:ℂ⊢ z₁ * (starRingEnd ℂ) z₁ * (z₂ * (starRingEnd ℂ) z₂) = ↑‖z₁‖ ^ 2 * ↑‖z₂‖ ^ 2 rw [mul_conj' z₁ , mul_conj' z₂]All goals completed! 🐙
    _ = (‖z₁‖ * ‖z₂‖ : ℂ) ^ 2           := byz₁:ℂz₂:ℂ⊢ ↑‖z₁‖ ^ 2 * ↑‖z₂‖ ^ 2 = (↑‖z₁‖ * ↑‖z₂‖) ^ 2 rw [mul_pow]All goals completed! 🐙;

The multiplicative property of norm is already proof in Mathlib as norm_mul. We can use this to give a more concise proof.

example (z₁ z₂ : ℂ) : ‖z₁ * z₂‖  = ‖z₁‖ * ‖z₂‖ :=
-- prove by using existing api in Mathlib
  byz₁:ℂz₂:ℂ⊢ ‖z₁ * z₂‖ = ‖z₁‖ * ‖z₂‖ exact norm_mul z₁ z₂All goals completed! 🐙

Although the triangle inequality is geometrically clear, we give an algebraic proof to show its compatibility with complex arithmetic.

Theorem 1.3.7. (Triangle inequality) For any z_1, z_2 \in \mathbb{C},

|z_1 + z_2| \le |z_1| + |z_2|.

/--
 Theorem 1.3.7
   Triangle inequality |z₁+z₂| ≤ |z₁| + |z₂|
-/
example (z₁ z₂ : ℂ) : ‖z₁ + z₂‖ ≤ ‖z₁‖ + ‖z₂‖ := byz₁:ℂz₂:ℂ⊢ ‖z₁ + z₂‖ ≤ ‖z₁‖ + ‖z₂‖
  -- Since norms are non-negative, x = |x|.
  -- rewrite the goal A = B to |A| = |B|,
  -- so the lemma matches.
  rw [← abs_of_nonneg (norm_nonneg _)]z₁:ℂz₂:ℂ⊢ |‖z₁ + z₂‖| ≤ ‖z₁‖ + ‖z₂‖
  rw [← abs_of_nonneg (add_nonneg (norm_nonneg _)
     (norm_nonneg _))]z₁:ℂz₂:ℂ⊢ |‖z₁ + z₂‖| ≤ |‖z₁‖ + ‖z₂‖|

  -- Apply the API: |A| = |B| ↔ A^2 = B^2
  rw [←sq_le_sq]z₁:ℂz₂:ℂ⊢ ‖z₁ + z₂‖ ^ 2 ≤ (‖z₁‖ + ‖z₂‖) ^ 2

  have h : ‖z₁ + z₂‖ ^ 2 = ‖z₁‖^2 + ‖z₂‖^2
      + 2 * (z₁ * conj z₂).re := byz₁:ℂz₂:ℂ⊢ ‖z₁ + z₂‖ ≤ ‖z₁‖ + ‖z₂‖
    -- Convert Norm^2 to Real Part of (z * conj z)
    rw [← normSq_eq_norm_sq]z₁:ℂz₂:ℂ⊢ normSq (z₁ + z₂) = ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * (z₁ * (starRingEnd ℂ) z₂).re
    rw [← ofReal_re (normSq (z₁ + z₂))]z₁:ℂz₂:ℂ⊢ (↑(normSq (z₁ + z₂))).re = ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * (z₁ * (starRingEnd ℂ) z₂).re
    rw [← mul_conj]z₁:ℂz₂:ℂ⊢ ((z₁ + z₂) * (starRingEnd ℂ) (z₁ + z₂)).re = ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * (z₁ * (starRingEnd ℂ) z₂).re
    rw [RingHom.map_add]z₁:ℂz₂:ℂ⊢ ((z₁ + z₂) * ((starRingEnd ℂ) z₁ + (starRingEnd ℂ) z₂)).re = ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * (z₁ * (starRingEnd ℂ) z₂).re
    ring_nfz₁:ℂz₂:ℂ⊢ (z₁ * (starRingEnd ℂ) z₁ + z₁ * (starRingEnd ℂ) z₂ + z₂ * (starRingEnd ℂ) z₁ + z₂ * (starRingEnd ℂ) z₂).re =
  ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + (z₁ * (starRingEnd ℂ) z₂).re * 2  -- Expand: z1z1* + z1z2* + z2z1* + z2z2*
    -- Distribute `re` across the addition
    rw [add_re]z₁:ℂz₂:ℂ⊢ (z₁ * (starRingEnd ℂ) z₁ + z₁ * (starRingEnd ℂ) z₂ + z₂ * (starRingEnd ℂ) z₁).re + (z₂ * (starRingEnd ℂ) z₂).re =
  ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + (z₁ * (starRingEnd ℂ) z₂).re * 2
    -- Convert (z * conj z).re back to ‖z‖^2
    -- We do this for z1 and z2.
    -- The sequence is: (z * conj z).re ->
    --    (normSq z).re -> normSq z -> ‖z‖^2
    simp only [mul_conj, ofReal_re, normSq_eq_norm_sq]z₁:ℂz₂:ℂ⊢ (↑(‖z₁‖ ^ 2) + z₁ * (starRingEnd ℂ) z₂ + z₂ * (starRingEnd ℂ) z₁).re + ‖z₂‖ ^ 2 =
  ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + (z₁ * (starRingEnd ℂ) z₂).re * 2
    rw [add_re, add_re]z₁:ℂz₂:ℂ⊢ (↑(‖z₁‖ ^ 2)).re + (z₁ * (starRingEnd ℂ) z₂).re + (z₂ * (starRingEnd ℂ) z₁).re + ‖z₂‖ ^ 2 =
  ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + (z₁ * (starRingEnd ℂ) z₂).re * 2
    -- Key step: z2 * z1* is the conjugate of z1 * z2*
    -- they have the same Real part.
    simp only [ofReal_re]z₁:ℂz₂:ℂ⊢ ‖z₁‖ ^ 2 + (z₁ * (starRingEnd ℂ) z₂).re + (z₂ * (starRingEnd ℂ) z₁).re + ‖z₂‖ ^ 2 =
  ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + (z₁ * (starRingEnd ℂ) z₂).re * 2
    -- Simplify the conjugate term:
    --   conj(z2 * conj z1) -> z1 * conj z2
    rw [← conj_re (z₂ * conj z₁)]z₁:ℂz₂:ℂ⊢ ‖z₁‖ ^ 2 + (z₁ * (starRingEnd ℂ) z₂).re + ((starRingEnd ℂ) (z₂ * (starRingEnd ℂ) z₁)).re + ‖z₂‖ ^ 2 =
  ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + (z₁ * (starRingEnd ℂ) z₂).re * 2
    -- Simplify Re(↑‖z1‖^2) to ‖z1‖^2
    rw [map_mul, conj_conj, mul_comm]z₁:ℂz₂:ℂ⊢ ‖z₁‖ ^ 2 + ((starRingEnd ℂ) z₂ * z₁).re + ((starRingEnd ℂ) z₂ * z₁).re + ‖z₂‖ ^ 2 =
  ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + ((starRingEnd ℂ) z₂ * z₁).re * 2
    -- the rest is algebra
    ringAll goals completed! 🐙

  calc
    ‖z₁ + z₂‖ ^ 2
    _ = ‖z₁‖^2 + ‖z₂‖^2 + 2 * (z₁ * conj z₂).re := byz₁:ℂz₂:ℂh:‖z₁ + z₂‖ ^ 2 = ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * (z₁ * (starRingEnd ℂ) z₂).re⊢ ‖z₁ + z₂‖ ^ 2 = ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * (z₁ * (starRingEnd ℂ) z₂).re rw [h]All goals completed! 🐙
    -- Apply Inequality: Re(w) <= |w|
    _ ≤ ‖z₁‖^2 + ‖z₂‖^2 + 2 * ‖z₁ * conj z₂‖ := byz₁:ℂz₂:ℂh:‖z₁ + z₂‖ ^ 2 = ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * (z₁ * (starRingEnd ℂ) z₂).re⊢ ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * (z₁ * (starRingEnd ℂ) z₂).re ≤ ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * ‖z₁ * (starRingEnd ℂ) z₂‖
        gcongrbc.hbcz₁:ℂz₂:ℂh:‖z₁ + z₂‖ ^ 2 = ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * (z₁ * (starRingEnd ℂ) z₂).re⊢ (z₁ * (starRingEnd ℂ) z₂).re ≤ ‖z₁ * (starRingEnd ℂ) z₂‖ -- 1. Strips away the common terms
        apply re_le_normAll goals completed! 🐙 -- 2. Applies Re(w) ≤ ‖w‖
    -- Break product |z1 z2*| = |z1| |z2|
    _ = ‖z₁‖^2 + ‖z₂‖^2 + 2 * (‖z₁‖ * ‖conj z₂‖) := byz₁:ℂz₂:ℂh:‖z₁ + z₂‖ ^ 2 = ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * (z₁ * (starRingEnd ℂ) z₂).re⊢ ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * ‖z₁ * (starRingEnd ℂ) z₂‖ = ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * (‖z₁‖ * ‖(starRingEnd ℂ) z₂‖)
        rw [norm_mul]All goals completed! 🐙
    _ = ‖z₁‖^2 + ‖z₂‖^2 + 2 * ‖z₁‖ * (‖conj z₂‖) := byz₁:ℂz₂:ℂh:‖z₁ + z₂‖ ^ 2 = ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * (z₁ * (starRingEnd ℂ) z₂).re⊢ ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * (‖z₁‖ * ‖(starRingEnd ℂ) z₂‖) = ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * ‖z₁‖ * ‖(starRingEnd ℂ) z₂‖ ringAll goals completed! 🐙
    _ = ‖z₁‖^2 + ‖z₂‖^2 + 2 * ‖z₁‖ * (‖z₂‖) := byz₁:ℂz₂:ℂh:‖z₁ + z₂‖ ^ 2 = ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * (z₁ * (starRingEnd ℂ) z₂).re⊢ ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * ‖z₁‖ * ‖(starRingEnd ℂ) z₂‖ = ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * ‖z₁‖ * ‖z₂‖
        rw [norm_conj]All goals completed! 🐙
    -- Factor perfect square
    _ = (‖z₁‖ + ‖z₂‖) ^ 2 := byz₁:ℂz₂:ℂh:‖z₁ + z₂‖ ^ 2 = ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * (z₁ * (starRingEnd ℂ) z₂).re⊢ ‖z₁‖ ^ 2 + ‖z₂‖ ^ 2 + 2 * ‖z₁‖ * ‖z₂‖ = (‖z₁‖ + ‖z₂‖) ^ 2 ringAll goals completed! 🐙

example (z₁ z₂ : ℂ) : ‖z₁ + z₂‖ ≤ ‖z₁‖ + ‖z₂‖ :=
-- proof of triangle inequality using existing theorem
  byz₁:ℂz₂:ℂ⊢ ‖z₁ + z₂‖ ≤ ‖z₁‖ + ‖z₂‖ exact norm_add_le z₁ z₂All goals completed! 🐙

Example. Using the identity |z_1 z_2| = |z_1| |z_2| and mathematical induction to show that |z^n| = |z|^n, for n=1,2,3,\ldots.

We prove this for all natural numbers n (0, 1, 2, \ldots), which implies the case for n = 1, 2, 3, \ldots.

example (z : ℂ) (n : ℕ) : ‖z^n‖ = ‖z‖ ^ n := byz:ℂn:ℕ⊢ ‖z ^ n‖ = ‖z‖ ^ n
  -- We proceed by induction on n
  induction n with
  | zero =>zeroz:ℂ⊢ ‖z ^ 0‖ = ‖z‖ ^ 0
    -- Base Case: n = 0
    -- Goal: |z^0| = |z|^0
    -- Since z^0 = 1 and x^0 = 1, we show |1| = 1
    simpAll goals completed! 🐙  -- solved by simplification

  | succ n ih =>succz:ℂn:ℕih:‖z ^ n‖ = ‖z‖ ^ n⊢ ‖z ^ (n + 1)‖ = ‖z‖ ^ (n + 1)
    -- Inductive Step: Assume true for n, prove for n + 1
    -- ih (Inductive Hypothesis): abs (z ^ n) = (abs z) ^ n
    calc
      ‖z ^ (n + 1)‖
        = ‖z ^ n * z‖
          := byz:ℂn:ℕih:‖z ^ n‖ = ‖z‖ ^ n⊢ ‖z ^ (n + 1)‖ = ‖z ^ n * z‖ rw [pow_succ]All goals completed! 🐙 -- Definition of power
      _ = ‖z^n‖  * ‖z‖
          -- Use the specific identity |z1 z2| = |z1| |z2|
          := byz:ℂn:ℕih:‖z ^ n‖ = ‖z‖ ^ n⊢ ‖z ^ n * z‖ = ‖z ^ n‖ * ‖z‖ rw [norm_mul]All goals completed! 🐙
      _ = ‖z‖ ^ n * ‖z‖
        -- Apply Induction Hypothesis
        := byz:ℂn:ℕih:‖z ^ n‖ = ‖z‖ ^ n⊢ ‖z ^ n‖ * ‖z‖ = ‖z‖ ^ n * ‖z‖ rw [ih]All goals completed! 🐙
      _ = ‖z‖ ^ (n + 1)
        -- Definition of power (in reverse)
        := byz:ℂn:ℕih:‖z ^ n‖ = ‖z‖ ^ n⊢ ‖z‖ ^ n * ‖z‖ = ‖z‖ ^ (n + 1) rw [pow_succ]All goals completed! 🐙

Example. Show that three points z₁, z₂ and z₃ on the complex plane form an equilateral triangle if and only if they satisfy

z₁^2 + z₂^2 + z₃^2 = z₁*z₂ + z₂*z₃ + z₃*z₁.

z₁, z₂ and z₃ are the vertices of a equilateral triangle if and only if

‖z₁ - z₂‖^2 = ‖z₂ - z₃‖^2 = ‖z₃ - z₁‖^2.

example (z₁ z₂ z₃ : ℂ) :
  ‖z₁ - z₂‖^2 = ‖z₂ - z₃‖^2 ∧
  ‖z₂ - z₃‖^2 = ‖z₃ - z₁‖^2
   ↔ z₁^2 + z₂^2 + z₃^2 = z₁*z₂ + z₂*z₃ + z₃*z₁ := byz₁:ℂz₂:ℂz₃:ℂ⊢ ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 ↔ z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁
  constructormpz₁:ℂz₂:ℂz₃:ℂ⊢ ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 → z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁mprz₁:ℂz₂:ℂz₃:ℂ⊢ z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁ → ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2;
  ·mpz₁:ℂz₂:ℂz₃:ℂ⊢ ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 → z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁ by_contra h_contrampz₁:ℂz₂:ℂz₃:ℂh_contra:¬(‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 →
    z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁)⊢ False;
    -- Let $w = \frac{z_1 - z_2}{z_2 - z_3}$.
    -- Then $|w| = 1$ and $|w + 1| = 1$.
    set w : ℂ := (z₁ - z₂) / (z₂ - z₃)mpz₁:ℂz₂:ℂz₃:ℂh_contra:¬(‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 →
    z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁)w:ℂ := (z₁ - z₂) / (z₂ - z₃)⊢ False
    have hw : ‖w‖ = 1 ∧ ‖w + 1‖ = 1 := byz₁:ℂz₂:ℂz₃:ℂ⊢ ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 ↔ z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁
      by_cases h₂ : z₂ - z₃ = 0posz₁:ℂz₂:ℂz₃:ℂh_contra:¬(‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 →
    z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁)w:ℂ := (z₁ - z₂) / (z₂ - z₃)h₂:z₂ - z₃ = 0⊢ ‖w‖ = 1 ∧ ‖w + 1‖ = 1negz₁:ℂz₂:ℂz₃:ℂh_contra:¬(‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 →
    z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁)w:ℂ := (z₁ - z₂) / (z₂ - z₃)h₂:¬z₂ - z₃ = 0⊢ ‖w‖ = 1 ∧ ‖w + 1‖ = 1 <;>posz₁:ℂz₂:ℂz₃:ℂh_contra:¬(‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 →
    z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁)w:ℂ := (z₁ - z₂) / (z₂ - z₃)h₂:z₂ - z₃ = 0⊢ ‖w‖ = 1 ∧ ‖w + 1‖ = 1negz₁:ℂz₂:ℂz₃:ℂh_contra:¬(‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 →
    z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁)w:ℂ := (z₁ - z₂) / (z₂ - z₃)h₂:¬z₂ - z₃ = 0⊢ ‖w‖ = 1 ∧ ‖w + 1‖ = 1 simp_all  [ sq ]negz₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)h_contra:‖z₁ - z₂‖ * ‖z₁ - z₂‖ = ‖z₂ - z₃‖ * ‖z₂ - z₃‖ ∧
  ‖z₂ - z₃‖ * ‖z₂ - z₃‖ = ‖z₃ - z₁‖ * ‖z₃ - z₁‖ ∧ ¬z₁ * z₁ + z₂ * z₂ + z₃ * z₃ = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h₂:¬z₂ - z₃ = 0⊢ ‖w‖ = 1 ∧ ‖w + 1‖ = 1;
      ·posz₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)h_contra:z₁ - z₂ = 0 ∧ z₃ - z₁ = 0 ∧ ¬z₁ * z₁ + z₂ * z₂ + z₃ * z₃ = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h₂:z₂ - z₃ = 0⊢ ‖w‖ = 1 ∧ ‖w + 1‖ = 1 grindAll goals completed! 🐙;
      ·negz₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)h_contra:‖z₁ - z₂‖ * ‖z₁ - z₂‖ = ‖z₂ - z₃‖ * ‖z₂ - z₃‖ ∧
  ‖z₂ - z₃‖ * ‖z₂ - z₃‖ = ‖z₃ - z₁‖ * ‖z₃ - z₁‖ ∧ ¬z₁ * z₁ + z₂ * z₂ + z₃ * z₃ = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h₂:¬z₂ - z₃ = 0⊢ ‖w‖ = 1 ∧ ‖w + 1‖ = 1 rw [ div_add_one, norm_div ]negz₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)h_contra:‖z₁ - z₂‖ * ‖z₁ - z₂‖ = ‖z₂ - z₃‖ * ‖z₂ - z₃‖ ∧
  ‖z₂ - z₃‖ * ‖z₂ - z₃‖ = ‖z₃ - z₁‖ * ‖z₃ - z₁‖ ∧ ¬z₁ * z₁ + z₂ * z₂ + z₃ * z₃ = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h₂:¬z₂ - z₃ = 0⊢ ‖z₁ - z₂‖ / ‖z₂ - z₃‖ = 1 ∧ ‖(z₁ - z₂ + (z₂ - z₃)) / (z₂ - z₃)‖ = 1negz₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)h_contra:‖z₁ - z₂‖ * ‖z₁ - z₂‖ = ‖z₂ - z₃‖ * ‖z₂ - z₃‖ ∧
  ‖z₂ - z₃‖ * ‖z₂ - z₃‖ = ‖z₃ - z₁‖ * ‖z₃ - z₁‖ ∧ ¬z₁ * z₁ + z₂ * z₂ + z₃ * z₃ = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h₂:¬z₂ - z₃ = 0⊢ z₂ - z₃ ≠ 0 <;>negz₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)h_contra:‖z₁ - z₂‖ * ‖z₁ - z₂‖ = ‖z₂ - z₃‖ * ‖z₂ - z₃‖ ∧
  ‖z₂ - z₃‖ * ‖z₂ - z₃‖ = ‖z₃ - z₁‖ * ‖z₃ - z₁‖ ∧ ¬z₁ * z₁ + z₂ * z₂ + z₃ * z₃ = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h₂:¬z₂ - z₃ = 0⊢ ‖z₁ - z₂‖ / ‖z₂ - z₃‖ = 1 ∧ ‖(z₁ - z₂ + (z₂ - z₃)) / (z₂ - z₃)‖ = 1negz₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)h_contra:‖z₁ - z₂‖ * ‖z₁ - z₂‖ = ‖z₂ - z₃‖ * ‖z₂ - z₃‖ ∧
  ‖z₂ - z₃‖ * ‖z₂ - z₃‖ = ‖z₃ - z₁‖ * ‖z₃ - z₁‖ ∧ ¬z₁ * z₁ + z₂ * z₂ + z₃ * z₃ = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h₂:¬z₂ - z₃ = 0⊢ z₂ - z₃ ≠ 0
          simp_all [ sub_eq_iff_eq_add ]All goals completed! 🐙;
        constructorneg.leftz₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)h_contra:‖z₁ - z₂‖ * ‖z₁ - z₂‖ = ‖z₂ - z₃‖ * ‖z₂ - z₃‖ ∧
  ‖z₂ - z₃‖ * ‖z₂ - z₃‖ = ‖z₃ - z₁‖ * ‖z₃ - z₁‖ ∧ ¬z₁ * z₁ + z₂ * z₂ + z₃ * z₃ = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h₂:¬z₂ = z₃⊢ ‖z₁ - z₂‖ / ‖z₂ - z₃‖ = 1neg.rightz₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)h_contra:‖z₁ - z₂‖ * ‖z₁ - z₂‖ = ‖z₂ - z₃‖ * ‖z₂ - z₃‖ ∧
  ‖z₂ - z₃‖ * ‖z₂ - z₃‖ = ‖z₃ - z₁‖ * ‖z₃ - z₁‖ ∧ ¬z₁ * z₁ + z₂ * z₂ + z₃ * z₃ = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h₂:¬z₂ = z₃⊢ ‖z₁ - z₃‖ / ‖z₂ - z₃‖ = 1
        ·neg.leftz₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)h_contra:‖z₁ - z₂‖ * ‖z₁ - z₂‖ = ‖z₂ - z₃‖ * ‖z₂ - z₃‖ ∧
  ‖z₂ - z₃‖ * ‖z₂ - z₃‖ = ‖z₃ - z₁‖ * ‖z₃ - z₁‖ ∧ ¬z₁ * z₁ + z₂ * z₂ + z₃ * z₃ = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h₂:¬z₂ = z₃⊢ ‖z₁ - z₂‖ / ‖z₂ - z₃‖ = 1 rw [ div_eq_iff ( norm_ne_zero_iff.mpr
            ( sub_ne_zero.mpr h₂ ) ) ]neg.leftz₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)h_contra:‖z₁ - z₂‖ * ‖z₁ - z₂‖ = ‖z₂ - z₃‖ * ‖z₂ - z₃‖ ∧
  ‖z₂ - z₃‖ * ‖z₂ - z₃‖ = ‖z₃ - z₁‖ * ‖z₃ - z₁‖ ∧ ¬z₁ * z₁ + z₂ * z₂ + z₃ * z₃ = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h₂:¬z₂ = z₃⊢ ‖z₁ - z₂‖ = 1 * ‖z₂ - z₃‖ ;
          nlinarith [ norm_nonneg ( z₁ - z₂ ),
            norm_nonneg ( z₂ - z₃ ) ]All goals completed! 🐙
        ·neg.rightz₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)h_contra:‖z₁ - z₂‖ * ‖z₁ - z₂‖ = ‖z₂ - z₃‖ * ‖z₂ - z₃‖ ∧
  ‖z₂ - z₃‖ * ‖z₂ - z₃‖ = ‖z₃ - z₁‖ * ‖z₃ - z₁‖ ∧ ¬z₁ * z₁ + z₂ * z₂ + z₃ * z₃ = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h₂:¬z₂ = z₃⊢ ‖z₁ - z₃‖ / ‖z₂ - z₃‖ = 1 rw [ div_eq_iff ( norm_ne_zero_iff.mpr
            ( sub_ne_zero.mpr h₂ ) ) ]neg.rightz₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)h_contra:‖z₁ - z₂‖ * ‖z₁ - z₂‖ = ‖z₂ - z₃‖ * ‖z₂ - z₃‖ ∧
  ‖z₂ - z₃‖ * ‖z₂ - z₃‖ = ‖z₃ - z₁‖ * ‖z₃ - z₁‖ ∧ ¬z₁ * z₁ + z₂ * z₂ + z₃ * z₃ = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h₂:¬z₂ = z₃⊢ ‖z₁ - z₃‖ = 1 * ‖z₂ - z₃‖ ;
          rw [ norm_sub_rev z₃ z₁ ] at *neg.rightz₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)h_contra:‖z₁ - z₂‖ * ‖z₁ - z₂‖ = ‖z₂ - z₃‖ * ‖z₂ - z₃‖ ∧
  ‖z₂ - z₃‖ * ‖z₂ - z₃‖ = ‖z₁ - z₃‖ * ‖z₁ - z₃‖ ∧ ¬z₁ * z₁ + z₂ * z₂ + z₃ * z₃ = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h₂:¬z₂ = z₃⊢ ‖z₁ - z₃‖ = 1 * ‖z₂ - z₃‖;
          nlinarith [ norm_nonneg ( z₁ - z₃ ),
            norm_nonneg ( z₂ - z₃ ) ]All goals completed! 🐙
    -- Since $|w| = 1$ and $|w + 1| = 1$,
    -- we have $w^2 + w + 1 = 0$.
    have hw_eq : w^2 + w + 1 = 0 := byz₁:ℂz₂:ℂz₃:ℂ⊢ ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 ↔ z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁
      norm_num [ Complex.norm_def, Complex.normSq ] at *z₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)h_contra:√((z₁.re - z₂.re) * (z₁.re - z₂.re) + (z₁.im - z₂.im) * (z₁.im - z₂.im)) =
    √((z₂.re - z₃.re) * (z₂.re - z₃.re) + (z₂.im - z₃.im) * (z₂.im - z₃.im)) ∧
  √((z₂.re - z₃.re) * (z₂.re - z₃.re) + (z₂.im - z₃.im) * (z₂.im - z₃.im)) =
      √((z₃.re - z₁.re) * (z₃.re - z₁.re) + (z₃.im - z₁.im) * (z₃.im - z₁.im)) ∧
    ¬z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁hw:w.re * w.re + w.im * w.im = 1 ∧ (w.re + 1) * (w.re + 1) + w.im * w.im = 1⊢ w ^ 2 + w + 1 = 0;
      norm_num [ Complex.ext_iff, sq ] at *z₁:ℂz₂:ℂz₃:ℂw:ℂ := (z₁ - z₂) / (z₂ - z₃)hw:w.re * w.re + w.im * w.im = 1 ∧ (w.re + 1) * (w.re + 1) + w.im * w.im = 1h_contra:√((z₁.re - z₂.re) * (z₁.re - z₂.re) + (z₁.im - z₂.im) * (z₁.im - z₂.im)) =
    √((z₂.re - z₃.re) * (z₂.re - z₃.re) + (z₂.im - z₃.im) * (z₂.im - z₃.im)) ∧
  √((z₂.re - z₃.re) * (z₂.re - z₃.re) + (z₂.im - z₃.im) * (z₂.im - z₃.im)) =
      √((z₃.re - z₁.re) * (z₃.re - z₁.re) + (z₃.im - z₁.im) * (z₃.im - z₁.im)) ∧
    (z₁.re * z₁.re - z₁.im * z₁.im + (z₂.re * z₂.re - z₂.im * z₂.im) + (z₃.re * z₃.re - z₃.im * z₃.im) =
        z₁.re * z₂.re - z₁.im * z₂.im + (z₂.re * z₃.re - z₂.im * z₃.im) + (z₃.re * z₁.re - z₃.im * z₁.im) →
      ¬z₁.re * z₁.im + z₁.im * z₁.re + (z₂.re * z₂.im + z₂.im * z₂.re) + (z₃.re * z₃.im + z₃.im * z₃.re) =
          z₁.re * z₂.im + z₁.im * z₂.re + (z₂.re * z₃.im + z₂.im * z₃.re) + (z₃.re * z₁.im + z₃.im * z₁.re))⊢ w.re * w.re - w.im * w.im + w.re + 1 = 0 ∧ w.re * w.im + w.im * w.re + w.im = 0;
      grindAll goals completed! 🐙;
    grindAll goals completed! 🐙;
  ·mprz₁:ℂz₂:ℂz₃:ℂ⊢ z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁ → ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 intro hmprz₁:ℂz₂:ℂz₃:ℂh:z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁⊢ ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2
    have h_eq : (z₁-z₂)^2 + (z₂-z₃)^2 + (z₃-z₁)^2 = 0 := byz₁:ℂz₂:ℂz₃:ℂ⊢ ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 ↔ z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁
      linear_combination' h * 2All goals completed! 🐙;
    -- From h_eq, deduce that $(z₁ - z₂) = (z₂ - z₃)\omega$
    -- or $(z₁ - z₂) = (z₂ - z₃)\omega^2$,
    -- where $\omega$ is a primitive cube root of unity.
    have h_cases : (z₁ - z₂) = (z₂ - z₃) *
      (-1 / 2 + Complex.I * (Real.sqrt 3 / 2)) ∨
      (z₁ - z₂) = (z₂ - z₃) *
      (-1 / 2 - Complex.I * (Real.sqrt 3 / 2)) := byz₁:ℂz₂:ℂz₃:ℂ⊢ ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 ↔ z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁
      exact Classical.or_iff_not_imp_left.2
        fun h =>mul_left_cancel₀ ( sub_ne_zero_of_ne h ) <|
        byz₁:ℂz₂:ℂz₃:ℂh✝:z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h_eq:(z₁ - z₂) ^ 2 + (z₂ - z₃) ^ 2 + (z₃ - z₁) ^ 2 = 0h:¬z₁ - z₂ = (z₂ - z₃) * (-1 / 2 + I * (↑√3 / 2))⊢ (z₁ - z₂ - (z₂ - z₃) * (-1 / 2 + I * (↑√3 / 2))) * (z₁ - z₂) =
  (z₁ - z₂ - (z₂ - z₃) * (-1 / 2 + I * (↑√3 / 2))) * ((z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2))) ring_nfz₁:ℂz₂:ℂz₃:ℂh✝:z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h_eq:(z₁ - z₂) ^ 2 + (z₂ - z₃) ^ 2 + (z₃ - z₁) ^ 2 = 0h:¬z₁ - z₂ = (z₂ - z₃) * (-1 / 2 + I * (↑√3 / 2))⊢ z₁ * z₂ * (-3 / 2) + z₁ * z₂ * I * ↑√3 * (-1 / 2) + z₁ * z₃ * (-1 / 2) + z₁ * z₃ * I * ↑√3 * (1 / 2) + z₁ ^ 2 +
          z₂ * z₃ * (1 / 2) +
        z₂ * z₃ * I * ↑√3 * (-1 / 2) +
      z₂ ^ 2 * (1 / 2) +
    z₂ ^ 2 * I * ↑√3 * (1 / 2) =
  z₁ * z₂ * (-1 / 2) + z₁ * z₂ * I * ↑√3 * (-1 / 2) + z₁ * z₃ * (1 / 2) + z₁ * z₃ * I * ↑√3 * (1 / 2) +
                z₂ * z₃ * I * ↑√3 * (-1 / 2) +
              z₂ * z₃ * I ^ 2 * ↑√3 ^ 2 * (-1 / 2) +
            z₂ ^ 2 * (1 / 4) +
          z₂ ^ 2 * I * ↑√3 * (1 / 2) +
        z₂ ^ 2 * I ^ 2 * ↑√3 ^ 2 * (1 / 4) +
      z₃ ^ 2 * (-1 / 4) +
    z₃ ^ 2 * I ^ 2 * ↑√3 ^ 2 * (1 / 4);
           norm_num [ ← Complex.ofReal_pow ]z₁:ℂz₂:ℂz₃:ℂh✝:z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h_eq:(z₁ - z₂) ^ 2 + (z₂ - z₃) ^ 2 + (z₃ - z₁) ^ 2 = 0h:¬z₁ - z₂ = (z₂ - z₃) * (-1 / 2 + I * (↑√3 / 2))⊢ -(z₁ * z₂ * (3 / 2)) + -(z₁ * z₂ * I * ↑√3 * (1 / 2)) + -(z₁ * z₃ * (1 / 2)) + z₁ * z₃ * I * ↑√3 * (1 / 2) + z₁ ^ 2 +
          z₂ * z₃ * (1 / 2) +
        -(z₂ * z₃ * I * ↑√3 * (1 / 2)) +
      z₂ ^ 2 * (1 / 2) +
    z₂ ^ 2 * I * ↑√3 * (1 / 2) =
  -(z₁ * z₂ * (1 / 2)) + -(z₁ * z₂ * I * ↑√3 * (1 / 2)) + z₁ * z₃ * (1 / 2) + z₁ * z₃ * I * ↑√3 * (1 / 2) +
                -(z₂ * z₃ * I * ↑√3 * (1 / 2)) +
              z₂ * z₃ * 3 * (1 / 2) +
            z₂ ^ 2 * (1 / 4) +
          z₂ ^ 2 * I * ↑√3 * (1 / 2) +
        -(z₂ ^ 2 * 3 * (1 / 4)) +
      -(z₃ ^ 2 * (1 / 4)) +
    -(z₃ ^ 2 * 3 * (1 / 4)) ;
           linear_combination h_eq / 2All goals completed! 🐙;
    rcases h_cases with h_cases | h_casesmpr.inlz₁:ℂz₂:ℂz₃:ℂh:z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h_eq:(z₁ - z₂) ^ 2 + (z₂ - z₃) ^ 2 + (z₃ - z₁) ^ 2 = 0h_cases:z₁ - z₂ = (z₂ - z₃) * (-1 / 2 + I * (↑√3 / 2))⊢ ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2mpr.inrz₁:ℂz₂:ℂz₃:ℂh:z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h_eq:(z₁ - z₂) ^ 2 + (z₂ - z₃) ^ 2 + (z₃ - z₁) ^ 2 = 0h_cases:z₁ - z₂ = (z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2))⊢ ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 <;>mpr.inlz₁:ℂz₂:ℂz₃:ℂh:z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h_eq:(z₁ - z₂) ^ 2 + (z₂ - z₃) ^ 2 + (z₃ - z₁) ^ 2 = 0h_cases:z₁ - z₂ = (z₂ - z₃) * (-1 / 2 + I * (↑√3 / 2))⊢ ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2mpr.inrz₁:ℂz₂:ℂz₃:ℂh:z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h_eq:(z₁ - z₂) ^ 2 + (z₂ - z₃) ^ 2 + (z₃ - z₁) ^ 2 = 0h_cases:z₁ - z₂ = (z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2))⊢ ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2
    rw [ sub_eq_iff_eq_add ] at h_casesmpr.inrz₁:ℂz₂:ℂz₃:ℂh:z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h_eq:(z₁ - z₂) ^ 2 + (z₂ - z₃) ^ 2 + (z₃ - z₁) ^ 2 = 0h_cases:z₁ = (z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂⊢ ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2 <;>mpr.inlz₁:ℂz₂:ℂz₃:ℂh:z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h_eq:(z₁ - z₂) ^ 2 + (z₂ - z₃) ^ 2 + (z₃ - z₁) ^ 2 = 0h_cases:z₁ = (z₂ - z₃) * (-1 / 2 + I * (↑√3 / 2)) + z₂⊢ ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2mpr.inrz₁:ℂz₂:ℂz₃:ℂh:z₁ ^ 2 + z₂ ^ 2 + z₃ ^ 2 = z₁ * z₂ + z₂ * z₃ + z₃ * z₁h_eq:(z₁ - z₂) ^ 2 + (z₂ - z₃) ^ 2 + (z₃ - z₁) ^ 2 = 0h_cases:z₁ = (z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂⊢ ‖z₁ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧ ‖z₂ - z₃‖ ^ 2 = ‖z₃ - z₁‖ ^ 2
    subst_varsmpr.inrz₂:ℂz₃:ℂh:((z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂) ^ 2 + z₂ ^ 2 + z₃ ^ 2 =
  ((z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂) * z₂ + z₂ * z₃ + z₃ * ((z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂)h_eq:((z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂ - z₂) ^ 2 + (z₂ - z₃) ^ 2 +
    (z₃ - ((z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂)) ^ 2 =
  0⊢ ‖(z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧
  ‖z₂ - z₃‖ ^ 2 = ‖z₃ - ((z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂)‖ ^ 2 <;>mpr.inlz₂:ℂz₃:ℂh:((z₂ - z₃) * (-1 / 2 + I * (↑√3 / 2)) + z₂) ^ 2 + z₂ ^ 2 + z₃ ^ 2 =
  ((z₂ - z₃) * (-1 / 2 + I * (↑√3 / 2)) + z₂) * z₂ + z₂ * z₃ + z₃ * ((z₂ - z₃) * (-1 / 2 + I * (↑√3 / 2)) + z₂)h_eq:((z₂ - z₃) * (-1 / 2 + I * (↑√3 / 2)) + z₂ - z₂) ^ 2 + (z₂ - z₃) ^ 2 +
    (z₃ - ((z₂ - z₃) * (-1 / 2 + I * (↑√3 / 2)) + z₂)) ^ 2 =
  0⊢ ‖(z₂ - z₃) * (-1 / 2 + I * (↑√3 / 2)) + z₂ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧
  ‖z₂ - z₃‖ ^ 2 = ‖z₃ - ((z₂ - z₃) * (-1 / 2 + I * (↑√3 / 2)) + z₂)‖ ^ 2mpr.inrz₂:ℂz₃:ℂh:((z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂) ^ 2 + z₂ ^ 2 + z₃ ^ 2 =
  ((z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂) * z₂ + z₂ * z₃ + z₃ * ((z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂)h_eq:((z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂ - z₂) ^ 2 + (z₂ - z₃) ^ 2 +
    (z₃ - ((z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂)) ^ 2 =
  0⊢ ‖(z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂ - z₂‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧
  ‖z₂ - z₃‖ ^ 2 = ‖z₃ - ((z₂ - z₃) * (-1 / 2 - I * (↑√3 / 2)) + z₂)‖ ^ 2 ring_nf at *mpr.inrz₂:ℂz₃:ℂh_eq:-(z₂ * z₃ * 3) - z₂ * z₃ * I ^ 2 * ↑√3 ^ 2 + z₂ ^ 2 * (3 / 2) + z₂ ^ 2 * I ^ 2 * ↑√3 ^ 2 * (1 / 2) + z₃ ^ 2 * (3 / 2) +
    z₃ ^ 2 * I ^ 2 * ↑√3 ^ 2 * (1 / 2) =
  0h:z₂ * z₃ * (1 / 2) + z₂ * z₃ * I ^ 2 * ↑√3 ^ 2 * (-1 / 2) + z₂ ^ 2 * (5 / 4) + z₂ ^ 2 * I * ↑√3 * (-1 / 2) +
          z₂ ^ 2 * I ^ 2 * ↑√3 ^ 2 * (1 / 4) +
        z₃ ^ 2 * (5 / 4) +
      z₃ ^ 2 * I * ↑√3 * (1 / 2) +
    z₃ ^ 2 * I ^ 2 * ↑√3 ^ 2 * (1 / 4) =
  z₂ * z₃ * 2 + z₂ ^ 2 * (1 / 2) + z₂ ^ 2 * I * ↑√3 * (-1 / 2) + z₃ ^ 2 * (1 / 2) + z₃ ^ 2 * I * ↑√3 * (1 / 2)⊢ ‖z₂ * (-1 / 2) + z₂ * I * ↑√3 * (-1 / 2) + z₃ * (1 / 2) + z₃ * I * ↑√3 * (1 / 2)‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧
  ‖z₂ - z₃‖ ^ 2 = ‖z₂ * (-1 / 2) + z₂ * I * ↑√3 * (1 / 2) + z₃ * (1 / 2) + z₃ * I * ↑√3 * (-1 / 2)‖ ^ 2 <;>mpr.inlz₂:ℂz₃:ℂh_eq:-(z₂ * z₃ * 3) - z₂ * z₃ * I ^ 2 * ↑√3 ^ 2 + z₂ ^ 2 * (3 / 2) + z₂ ^ 2 * I ^ 2 * ↑√3 ^ 2 * (1 / 2) + z₃ ^ 2 * (3 / 2) +
    z₃ ^ 2 * I ^ 2 * ↑√3 ^ 2 * (1 / 2) =
  0h:z₂ * z₃ * (1 / 2) + z₂ * z₃ * I ^ 2 * ↑√3 ^ 2 * (-1 / 2) + z₂ ^ 2 * (5 / 4) + z₂ ^ 2 * I * ↑√3 * (1 / 2) +
          z₂ ^ 2 * I ^ 2 * ↑√3 ^ 2 * (1 / 4) +
        z₃ ^ 2 * (5 / 4) +
      z₃ ^ 2 * I * ↑√3 * (-1 / 2) +
    z₃ ^ 2 * I ^ 2 * ↑√3 ^ 2 * (1 / 4) =
  z₂ * z₃ * 2 + z₂ ^ 2 * (1 / 2) + z₂ ^ 2 * I * ↑√3 * (1 / 2) + z₃ ^ 2 * (1 / 2) + z₃ ^ 2 * I * ↑√3 * (-1 / 2)⊢ ‖z₂ * (-1 / 2) + z₂ * I * ↑√3 * (1 / 2) + z₃ * (1 / 2) + z₃ * I * ↑√3 * (-1 / 2)‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧
  ‖z₂ - z₃‖ ^ 2 = ‖z₂ * (-1 / 2) + z₂ * I * ↑√3 * (-1 / 2) + z₃ * (1 / 2) + z₃ * I * ↑√3 * (1 / 2)‖ ^ 2mpr.inrz₂:ℂz₃:ℂh_eq:-(z₂ * z₃ * 3) - z₂ * z₃ * I ^ 2 * ↑√3 ^ 2 + z₂ ^ 2 * (3 / 2) + z₂ ^ 2 * I ^ 2 * ↑√3 ^ 2 * (1 / 2) + z₃ ^ 2 * (3 / 2) +
    z₃ ^ 2 * I ^ 2 * ↑√3 ^ 2 * (1 / 2) =
  0h:z₂ * z₃ * (1 / 2) + z₂ * z₃ * I ^ 2 * ↑√3 ^ 2 * (-1 / 2) + z₂ ^ 2 * (5 / 4) + z₂ ^ 2 * I * ↑√3 * (-1 / 2) +
          z₂ ^ 2 * I ^ 2 * ↑√3 ^ 2 * (1 / 4) +
        z₃ ^ 2 * (5 / 4) +
      z₃ ^ 2 * I * ↑√3 * (1 / 2) +
    z₃ ^ 2 * I ^ 2 * ↑√3 ^ 2 * (1 / 4) =
  z₂ * z₃ * 2 + z₂ ^ 2 * (1 / 2) + z₂ ^ 2 * I * ↑√3 * (-1 / 2) + z₃ ^ 2 * (1 / 2) + z₃ ^ 2 * I * ↑√3 * (1 / 2)⊢ ‖z₂ * (-1 / 2) + z₂ * I * ↑√3 * (-1 / 2) + z₃ * (1 / 2) + z₃ * I * ↑√3 * (1 / 2)‖ ^ 2 = ‖z₂ - z₃‖ ^ 2 ∧
  ‖z₂ - z₃‖ ^ 2 = ‖z₂ * (-1 / 2) + z₂ * I * ↑√3 * (1 / 2) + z₃ * (1 / 2) + z₃ * I * ↑√3 * (-1 / 2)‖ ^ 2
    norm_num [ Complex.normSq, Complex.sq_norm ] at *mpr.inrz₂:ℂz₃:ℂh_eq:-(z₂ * z₃ * 3) + z₂ * z₃ * ↑√3 ^ 2 + z₂ ^ 2 * (3 / 2) + -(z₂ ^ 2 * ↑√3 ^ 2 * (1 / 2)) + z₃ ^ 2 * (3 / 2) +
    -(z₃ ^ 2 * ↑√3 ^ 2 * (1 / 2)) =
  0h:z₂ * z₃ * (1 / 2) + z₂ * z₃ * ↑√3 ^ 2 * (1 / 2) + z₂ ^ 2 * (5 / 4) + -(z₂ ^ 2 * I * ↑√3 * (1 / 2)) +
          -(z₂ ^ 2 * ↑√3 ^ 2 * (1 / 4)) +
        z₃ ^ 2 * (5 / 4) +
      z₃ ^ 2 * I * ↑√3 * (1 / 2) +
    -(z₃ ^ 2 * ↑√3 ^ 2 * (1 / 4)) =
  z₂ * z₃ * 2 + z₂ ^ 2 * (1 / 2) + -(z₂ ^ 2 * I * ↑√3 * (1 / 2)) + z₃ ^ 2 * (1 / 2) + z₃ ^ 2 * I * ↑√3 * (1 / 2)⊢ (-(z₂.re * (1 / 2)) + z₂.im * √3 * (1 / 2) + z₃.re * (1 / 2) + -(z₃.im * √3 * (1 / 2))) *
        (-(z₂.re * (1 / 2)) + z₂.im * √3 * (1 / 2) + z₃.re * (1 / 2) + -(z₃.im * √3 * (1 / 2))) +
      (-(z₂.im * (1 / 2)) + -(z₂.re * √3 * (1 / 2)) + z₃.im * (1 / 2) + z₃.re * √3 * (1 / 2)) *
        (-(z₂.im * (1 / 2)) + -(z₂.re * √3 * (1 / 2)) + z₃.im * (1 / 2) + z₃.re * √3 * (1 / 2)) =
    (z₂.re - z₃.re) * (z₂.re - z₃.re) + (z₂.im - z₃.im) * (z₂.im - z₃.im) ∧
  (z₂.re - z₃.re) * (z₂.re - z₃.re) + (z₂.im - z₃.im) * (z₂.im - z₃.im) =
    (-(z₂.re * (1 / 2)) + -(z₂.im * √3 * (1 / 2)) + z₃.re * (1 / 2) + z₃.im * √3 * (1 / 2)) *
        (-(z₂.re * (1 / 2)) + -(z₂.im * √3 * (1 / 2)) + z₃.re * (1 / 2) + z₃.im * √3 * (1 / 2)) +
      (-(z₂.im * (1 / 2)) + z₂.re * √3 * (1 / 2) + z₃.im * (1 / 2) + -(z₃.re * √3 * (1 / 2))) *
        (-(z₂.im * (1 / 2)) + z₂.re * √3 * (1 / 2) + z₃.im * (1 / 2) + -(z₃.re * √3 * (1 / 2)));
    all_goals grindAll goals completed! 🐙