Using coercions

Stream: new members

[Janitha]

import Mathlib

example (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
    (h : ∃ q : ℚ, (a * Real.sqrt 2023 + b) / (a + c * Real.sqrt 2023) = q) :
    (a + b + c) ∣ (a^2 + b^2 + c^2) := by

      --Express q as m / n . This could go as a lemma; so left with a sorry.
      have rat : ∃ m n : ℤ , (a * Real.sqrt 2023 + b) / (a + c * Real.sqrt 2023) = m / n ∧ n ≠ 0 := by sorry
      rcases rat with ⟨m, n, hmn⟩

      --The first goal is to show (n * a - m * c) * Real.sqrt 2023 = m * a - n * b.
      have h1 : a + c * Real.sqrt 2023 ≠ 0 := by positivity
      have h2 : n ≠ 0 := by exact hmn.2

      --Simplifying...
      have h3 : n * ( (a * Real.sqrt 2023 + b) / (a + c * Real.sqrt 2023) ) = m := by
        calc
            n * ( (a * Real.sqrt 2023 + b) / (a + c * Real.sqrt 2023) ) = n * (m / n) := by rw [hmn.1]
          _ = m := by field_simp

      --Simplifying...
      have h4 : n * ( (a * Real.sqrt 2023 + b) / (a + c * Real.sqrt 2023) ) =  (n * (a * Real.sqrt 2023 + b)) / (a + c * Real.sqrt 2023) := by
        exact Eq.symm (mul_div_assoc (↑n) (↑a * √2023 + ↑b) (↑a + ↑c * √2023))

      rw [h4] at h3

      --Simplifying...
      have h5' : m * (a + c * Real.sqrt 2023) = n * (a * Real.sqrt 2023 + b) := by
        exact (eq_mul_inv_iff_mul_eq₀ h1).mp (id (Eq.symm h3))

      --Simplifying...
      have h5 : n * (a * Real.sqrt 2023 + b) = m * (a + c * Real.sqrt 2023) := by exact h5'.symm

      --Obtain, (n * a - m * c) * Real.sqrt 2023 = m * a - n * b.
      have h6 : (n * a - m * c) * Real.sqrt 2023 = m * a - n * b := by linarith

      --Now, the second goal is to show n * a - m * c = 0.
      --The idea is to use the fact that Real.sqrt 2023 is irrational.
      have h7 : n * a - m * c = 0 := by
        --Prove this by contradiction.
        sorry

      --Next, show that m * a - n * b = 0.
      have h8 : m * a - n * b = 0 := by
          rify at h6 h7 ⊢
          rw [h7, zero_mul] at h6
          exact h6.symm

      --Show  a = m * c / n.
      have h9 : a = m * c / n := by
        refine Int.eq_ediv_of_mul_eq_right h2 ?_
        exact Int.eq_of_sub_eq_zero h7

      have h9' : (a : ℚ) = (m / n) * c := by
        rify at h9 ⊢
        rw [h9]
        field_simp
        sorry

      have h9' : a = (m / n) * c := by
        rw [h9]
        ring_nf
        sorry

      --Show b = m * a / n.
      have h10 : b = m * a / n := by
        refine Int.eq_ediv_of_mul_eq_right h2 ?_
        exact Eq.symm (Int.eq_of_sub_eq_zero h8)

      --Show b = (m^2 / n^2) * c using h9 and h10.
      have h11 : b = (m^2 / n^2) * c := by
        calc
          b = m * a / n := by exact h10
          _ = (m / n) * a := by sorry
          _ = (m / n) * (m * c / n) := by rw [h9]
          _ = (m / n) * (m / n) * c := by sorry
          _ = (m^2 / n^2) * c := by sorry

      --Show that a + b + c = (m / n) * c + (m^2 / n^2) * c + c.
      have h12 : a + b + c = (m / n) * c + (m^2 / n^2) * c + c := by
        rw [h9', h11]

      --Show that a + b + c = c * (m^2 / n^2 + m / n + 1).
      have h13 : a + b + c = c * (m^2 / n^2 + m / n + 1) := by linarith

      --Show that a^2 = (m^2 / n^2) * c^2.
      have h14 : a^2 = (m^2 / n^2) * c^2 := by
        rify at h9 ⊢
        rw [pow_two]
        rw [h9]
        field_simp [pow_succ', mul_pow]
        sorry

      --Show that b^2 = (m^4 / n^4) * c^2.
      have h15 : b^2 = (m^4 / n^4) * c^2 := by sorry


      have h16 : (a^2 + b^2 + c^2 : ℝ) = (a + b + c) * (b - a + c) := by
        rify at h9' h11 h13 h14 h15 ⊢
        calc
          (a^2 + b^2 + c^2 : ℝ) = (m^2 / n^2) * c^2 + (m^4 / n^4) * c^2 + c^2 := by sorry
          _ = c^2 * (m^4 / n^4 + m^2 / n^2 + 1) := by ring
          _ = c^2 * (m^2 / n^2 + m/n + 1) * (m^2 / n^2 - m/n + 1) := by
            sorry
          _ = (c * (m^2 / n^2 + m/n + 1)) * (c * (m^2 / n^2 - m/n + 1)) := by ring
          _ = (a + b + c) * (b - a + c) := by
            sorry

      use b - a + c

I am unable to figure out how to close the goal using h16. Can someone help? Thanks!

[Edward van de Meent]

you will be delighted to learn about rify, read $\mathbb{R}$-ify

[Janitha]

zify
      use (b - a + c )
      --exact h16 ; why doesn't `exact h16` work?

I used zify. And I don't see why exact h16 shouldn't close the goal.

[Edward van de Meent]

because h16 is about equality of reals

[Edward van de Meent]

not integers

[Edward van de Meent]

for what it's worth, zify; use (b - a + c); rify; exact h16 seems to close the goal