1.4. Quadratic equation🔗

Verify the formula for solving quadratic equation.
The first theorem consider the simplified version x^2=c.
The second theorem verify the quadratic formula for monic polynomial x^2 +bx +c
/-- Solve equation x^2=c for some constant compelx number c
 The two solutions are ±d, where d is a complex number
 satisfying d^2 = c.
-/
theorem solve_square_eq_constant
   {c d x : ℂ} (h : d^2 = c) (h₁: x^2 = c) :
    x=d ∨ x=-d := byc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = c⊢ x = d ∨ x = -d

  have h₂ : (x-d)*(x+d) = 0 := calc
  (x-d)*(x+d) = x^2 - d^2 := byc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = c⊢ (x - d) * (x + d) = x ^ 2 - d ^ 2 ringAll goals completed! 🐙
   _ = c - c := byc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = c⊢ x ^ 2 - d ^ 2 = c - c rw [h, h₁]All goals completed! 🐙
   _ = 0 := byc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = c⊢ c - c = 0 ringAll goals completed! 🐙
  have h₃ : x - d = 0 ∨  x + d = 0
    := eq_zero_or_eq_zero_of_mul_eq_zero h₂c:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = ch₂:(x - d) * (x + d) = 0h₃:x - d = 0 ∨ x + d = 0⊢ x = d ∨ x = -d
  obtain h₄ | h₅ := h₃inlc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = ch₂:(x - d) * (x + d) = 0h₄:x - d = 0⊢ x = d ∨ x = -dinrc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = ch₂:(x - d) * (x + d) = 0h₅:x + d = 0⊢ x = d ∨ x = -d
  ·inlc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = ch₂:(x - d) * (x + d) = 0h₄:x - d = 0⊢ x = d ∨ x = -d leftinl.hc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = ch₂:(x - d) * (x + d) = 0h₄:x - d = 0⊢ x = d
    calc
    x = (x-d)+d := byc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = ch₂:(x - d) * (x + d) = 0h₄:x - d = 0⊢ x = x - d + d ringAll goals completed! 🐙
    _ = 0 + d := byc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = ch₂:(x - d) * (x + d) = 0h₄:x - d = 0⊢ x - d + d = 0 + d rw [h₄]All goals completed! 🐙
    _ = d := byc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = ch₂:(x - d) * (x + d) = 0h₄:x - d = 0⊢ 0 + d = d ringAll goals completed! 🐙
  ·inrc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = ch₂:(x - d) * (x + d) = 0h₅:x + d = 0⊢ x = d ∨ x = -d rightinr.hc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = ch₂:(x - d) * (x + d) = 0h₅:x + d = 0⊢ x = -d
    calc
    x = (x+d)-d := byc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = ch₂:(x - d) * (x + d) = 0h₅:x + d = 0⊢ x = x + d - d ringAll goals completed! 🐙
    _ = 0 - d := byc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = ch₂:(x - d) * (x + d) = 0h₅:x + d = 0⊢ x + d - d = 0 - d rw [h₅]All goals completed! 🐙
    _ = - d := byc:ℂd:ℂx:ℂh:d ^ 2 = ch₁:x ^ 2 = ch₂:(x - d) * (x + d) = 0h₅:x + d = 0⊢ 0 - d = -d ringAll goals completed! 🐙

/-- Prove that the roots of polynomial
    x^2+bx+c are -b/2 ± (√disc)/2
 where disc is the discriminant b^2-4c

 Reduce the problem to the case with zero degree-1 term
 and apply the previous theorem
-/
theorem solve_quadratic_equation
  (b c d x : ℂ)
  (h: d^2 = b^2/4-c)
  (h₁ : x^2+b*x+c=0) :
    x=-b/2+d ∨ x = -b/2-d := byb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0⊢ x = -b / 2 + d ∨ x = -b / 2 - d

  let y:ℂ := x+b/2b:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2⊢ x = -b / 2 + d ∨ x = -b / 2 - d
  have h₂: y^2 + c - b^2/4 = 0 :=
  calc
    y^2 + c - b^2/4 = y^2 +c + b^2/4- b^2/2 := byb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2⊢ y ^ 2 + c - b ^ 2 / 4 = y ^ 2 + c + b ^ 2 / 4 - b ^ 2 / 2 ringAll goals completed! 🐙
    _   = (y-b/2)^2 +b*(y- b/2) +c := byb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2⊢ y ^ 2 + c + b ^ 2 / 4 - b ^ 2 / 2 = (y - b / 2) ^ 2 + b * (y - b / 2) + c ringAll goals completed! 🐙
    _   = x ^2 + b*x+c
           := byb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2⊢ (y - b / 2) ^ 2 + b * (y - b / 2) + c = x ^ 2 + b * x + c simp only [add_sub_cancel_right, y]All goals completed! 🐙
    _   = 0 := h₁
  have h₃ : y^2 = b^2/4 - c :=
  calc
    y^2 = (y^2 +c - b^2/4) + b^2/4 -c := byb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2h₂:y ^ 2 + c - b ^ 2 / 4 = 0⊢ y ^ 2 = y ^ 2 + c - b ^ 2 / 4 + b ^ 2 / 4 - c ringAll goals completed! 🐙
      _ = 0 + b^2/4 - c := byb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2h₂:y ^ 2 + c - b ^ 2 / 4 = 0⊢ y ^ 2 + c - b ^ 2 / 4 + b ^ 2 / 4 - c = 0 + b ^ 2 / 4 - c rw [h₂]All goals completed! 🐙
      _ = b^2/4 - c := byb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2h₂:y ^ 2 + c - b ^ 2 / 4 = 0⊢ 0 + b ^ 2 / 4 - c = b ^ 2 / 4 - c ringAll goals completed! 🐙
  have h₄ : y = d ∨ y = -d := solve_square_eq_constant h h₃b:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2h₂:y ^ 2 + c - b ^ 2 / 4 = 0h₃:y ^ 2 = b ^ 2 / 4 - ch₄:y = d ∨ y = -d⊢ x = -b / 2 + d ∨ x = -b / 2 - d
  obtain h₅ | h₆ := h₄inlb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2h₂:y ^ 2 + c - b ^ 2 / 4 = 0h₃:y ^ 2 = b ^ 2 / 4 - ch₅:y = d⊢ x = -b / 2 + d ∨ x = -b / 2 - dinrb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2h₂:y ^ 2 + c - b ^ 2 / 4 = 0h₃:y ^ 2 = b ^ 2 / 4 - ch₆:y = -d⊢ x = -b / 2 + d ∨ x = -b / 2 - d
  ·inlb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2h₂:y ^ 2 + c - b ^ 2 / 4 = 0h₃:y ^ 2 = b ^ 2 / 4 - ch₅:y = d⊢ x = -b / 2 + d ∨ x = -b / 2 - d leftinl.hb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2h₂:y ^ 2 + c - b ^ 2 / 4 = 0h₃:y ^ 2 = b ^ 2 / 4 - ch₅:y = d⊢ x = -b / 2 + d
    calc
      x = y-b/2 := eq_sub_of_add_eq rfl
      _ = -b/2 +y := byb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2h₂:y ^ 2 + c - b ^ 2 / 4 = 0h₃:y ^ 2 = b ^ 2 / 4 - ch₅:y = d⊢ y - b / 2 = -b / 2 + y ringAll goals completed! 🐙
      _ = - b/2+d:= byb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2h₂:y ^ 2 + c - b ^ 2 / 4 = 0h₃:y ^ 2 = b ^ 2 / 4 - ch₅:y = d⊢ -b / 2 + y = -b / 2 + d rw [h₅]All goals completed! 🐙
  ·inrb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2h₂:y ^ 2 + c - b ^ 2 / 4 = 0h₃:y ^ 2 = b ^ 2 / 4 - ch₆:y = -d⊢ x = -b / 2 + d ∨ x = -b / 2 - d rightinr.hb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2h₂:y ^ 2 + c - b ^ 2 / 4 = 0h₃:y ^ 2 = b ^ 2 / 4 - ch₆:y = -d⊢ x = -b / 2 - d
    calc
      x = y-b/2 := eq_sub_of_add_eq rfl
      _ = -b/2 +y := byb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2h₂:y ^ 2 + c - b ^ 2 / 4 = 0h₃:y ^ 2 = b ^ 2 / 4 - ch₆:y = -d⊢ y - b / 2 = -b / 2 + y ringAll goals completed! 🐙
      _ = -b/2 + (-d) := byb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2h₂:y ^ 2 + c - b ^ 2 / 4 = 0h₃:y ^ 2 = b ^ 2 / 4 - ch₆:y = -d⊢ -b / 2 + y = -b / 2 + -d rw [h₆]All goals completed! 🐙
      _ = -b/2 - d := byb:ℂc:ℂd:ℂx:ℂh:d ^ 2 = b ^ 2 / 4 - ch₁:x ^ 2 + b * x + c = 0y:ℂ := x + b / 2h₂:y ^ 2 + c - b ^ 2 / 4 = 0h₃:y ^ 2 = b ^ 2 / 4 - ch₆:y = -d⊢ -b / 2 + -d = -b / 2 - d ringAll goals completed! 🐙