Chinese remainder theorem (coprime moduli)

import Mathlib

theorem crt {m n : ℕ} (h : Nat.Coprime m n) (a b : ℤ) : ∃ x : ℤ, x ≡ a [ZMOD m] ∧ x ≡ b [ZMOD n] :=by
  by_cases hm : m = 0
  · subst hm
    have hn : n = 1 := by rwa [Nat.Coprime, Nat.gcd_zero_left] at h
    subst hn
    use a
    exact ⟨rfl, Int.modEq_one⟩
  by_cases hn : n = 0
  · subst hn
    have hm' : m = 1 := by rwa [Nat.Coprime, Nat.gcd_zero_right] at h
    subst hm'
    use b
    exact ⟨Int.modEq_one, rfl⟩
  haveI : NeZero m := ⟨hm⟩
  haveI : NeZero n := ⟨hn⟩
  haveI : NeZero (m * n) := ⟨mul_ne_zero hm hn⟩
  let z : ZMod m × ZMod n := (a, b)
  let x_zmod := (ZMod.chineseRemainder h).symm z
  use (x_zmod.val : ℤ)
  have h_eq := RingEquiv.apply_symm_apply (ZMod.chineseRemainder h) z
  constructor
  · rw [← ZMod.intCast_eq_intCast_iff]
    simp only [Int.cast_natCast]
    rw [← ZMod.cast_eq_val]
    have h_fst := congr_arg Prod.fst h_eq
    have h_proj : (ZMod.chineseRemainder h x_zmod).1 = (ZMod.cast x_zmod : ZMod m) := by
      simp [ZMod.chineseRemainder]
    have h_fst_simp : (ZMod.cast x_zmod : ZMod m) = (a : ZMod m) := by
      rw [← h_proj]
      exact h_fst
    exact h_fst_simp
  · rw [← ZMod.intCast_eq_intCast_iff]
    simp only [Int.cast_natCast]
    rw [← ZMod.cast_eq_val]
    have h_snd := congr_arg Prod.snd h_eq
    have h_proj : (ZMod.chineseRemainder h x_zmod).2 = (ZMod.cast x_zmod : ZMod n) := by
      simp [ZMod.chineseRemainder]
    have h_snd_simp : (ZMod.cast x_zmod : ZMod n) = (b : ZMod n) := by
      rw [← h_proj]
      exact h_snd
    exact h_snd_simp