提交 #22

import Mathlib.Data.Int.GCD
import Mathlib.Tactic.Convert
import Mathlib.Tactic.Ring

local notation " ( " a " ≡ " b " mod " n " ) " => n ∣ a - b

theorem modulo_tran (a b c n : ℤ) (hab : (a ≡ b mod n)) (hbc : (b ≡ c mod n)) : (a ≡ c mod n) := by
  convert Int.dvd_add hab hbc using 1
  ring

theorem Int.dvd_mul_of_dvd_left {a b c : Int} (h : a ∣ b) : a ∣ b * c :=
  Int.dvd_trans h (Int.dvd_mul_right b c)

theorem modulo_mult_subst (a b c n : ℤ) (hab : (a ≡ b mod n)) : (a * c ≡ b * c mod n) := by
  convert Int.dvd_mul_of_dvd_left hab (c := c) using 1
  ring

theorem modulo_inv (m n : ℤ) (p : m.gcd n = 1) : ∃ x : ℤ, (m * x ≡ 1 mod n) := by
  refine ⟨m.gcdA n, ?_⟩
  have h := m.gcd_eq_gcd_ab n
  rw [p, Nat.cast_one] at h
  rw [h]
  simp

theorem SimpleChineseRemainder (m n : ℤ) (p : m.gcd n = 1) (a b : ℤ) : ∃ x : ℤ, (x ≡ a mod m) ∧ (x ≡ b mod n) := by
  refine ⟨m * m.gcdA n * b + n * m.gcdB n * a, ?_, ?_⟩
  · refine modulo_tran _ (m * m.gcdA n * a + n * m.gcdB n * a) _ m ?_ ?_
    · ring
      apply Int.dvd_sub <;> simp [Int.mul_assoc]
    · rw [← Int.add_mul, ← m.gcd_eq_gcd_ab n, p]
      simp
  · refine modulo_tran _ (m * m.gcdA n * b + n * m.gcdB n * b) _ n ?_ ?_
    · ring
      apply Int.dvd_add
      · simp
        rw [Int.mul_right_comm]
        simp
      · simp [Int.mul_assoc]
    · rw [← Int.add_mul, ← m.gcd_eq_gcd_ab n, p]
      simp

theorem P₅₀₅ :
  (∀ (a b c n : ℤ), (a ≡ b mod n) → (b ≡ c mod n) → (a ≡ c mod n)) ∧
  (∀ (a b c n : ℤ), (a ≡ b mod n) → (a * c ≡ b * c mod n)) ∧
  (∀ (m n : ℤ), m.gcd n = 1 → ∃ x : ℤ, (m * x ≡ 1 mod n)) ∧
  (∀ (m n : ℤ), m.gcd n = 1 → ∀ (a b : ℤ), ∃ x : ℤ, (x ≡ a mod m) ∧ (x ≡ b mod n)) :=
  ⟨modulo_tran, modulo_mult_subst, modulo_inv, SimpleChineseRemainder⟩