[GOAL]
m n a b c d : ℕ
⊢ a ≡ 0 [MOD n] ↔ n ∣ a
[PROOFSTEP]
rw [ModEq, zero_mod, dvd_iff_mod_eq_zero]
[GOAL]
m n a b c d : ℕ
⊢ a ≡ b [MOD n] ↔ ↑n ∣ ↑b - ↑a
[PROOFSTEP]
rw [ModEq, eq_comm, ← Int.coe_nat_inj', Int.coe_nat_mod, Int.coe_nat_mod, Int.emod_eq_emod_iff_emod_sub_eq_zero,
  Int.dvd_iff_emod_eq_zero]
[GOAL]
m n a b c d : ℕ
h : a ≤ b
⊢ a ≡ b [MOD n] ↔ n ∣ b - a
[PROOFSTEP]
rw [modEq_iff_dvd, ← Int.coe_nat_dvd, Int.ofNat_sub h]
[GOAL]
m n a b c✝ d c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD c * n]
[PROOFSTEP]
unfold ModEq at *
[GOAL]
m n a b c✝ d c : ℕ
h : a % n = b % n
⊢ c * a % (c * n) = c * b % (c * n)
[PROOFSTEP]
rw [mul_mod_mul_left, mul_mod_mul_left, h]
[GOAL]
m n a b c✝ d c : ℕ
h : a ≡ b [MOD n]
⊢ a * c ≡ b * c [MOD n * c]
[PROOFSTEP]
rw [mul_comm a, mul_comm b, mul_comm n]
[GOAL]
m n a b c✝ d c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD c * n]
[PROOFSTEP]
exact h.mul_left' c
[GOAL]
m n a b c✝ d c : ℕ
h : a ≡ b [MOD n]
⊢ a * c ≡ b * c [MOD n]
[PROOFSTEP]
rw [mul_comm a, mul_comm b]
[GOAL]
m n a b c✝ d c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD n]
[PROOFSTEP]
exact h.mul_left c
[GOAL]
m✝ n a b c d m : ℕ
h : a ≡ b [MOD n]
⊢ a ^ m ≡ b ^ m [MOD n]
[PROOFSTEP]
induction m with
| zero => rfl
| succ d hd =>
  rw [pow_succ, pow_succ]
  exact hd.mul h
[GOAL]
m✝ n a b c d m : ℕ
h : a ≡ b [MOD n]
⊢ a ^ m ≡ b ^ m [MOD n]
[PROOFSTEP]
induction m with
| zero => rfl
| succ d hd =>
  rw [pow_succ, pow_succ]
  exact hd.mul h
[GOAL]
case zero
m n a b c d : ℕ
h : a ≡ b [MOD n]
⊢ a ^ zero ≡ b ^ zero [MOD n]
[PROOFSTEP]

| zero => rfl
[GOAL]
case zero
m n a b c d : ℕ
h : a ≡ b [MOD n]
⊢ a ^ zero ≡ b ^ zero [MOD n]
[PROOFSTEP]
rfl
[GOAL]
case succ
m n a b c d✝ : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ succ d ≡ b ^ succ d [MOD n]
[PROOFSTEP]

| succ d hd =>
  rw [pow_succ, pow_succ]
  exact hd.mul h
[GOAL]
case succ
m n a b c d✝ : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ succ d ≡ b ^ succ d [MOD n]
[PROOFSTEP]
rw [pow_succ, pow_succ]
[GOAL]
case succ
m n a b c d✝ : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ d * a ≡ b ^ d * b [MOD n]
[PROOFSTEP]
exact hd.mul h
[GOAL]
m n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : c ≡ d [MOD n]
⊢ a + c ≡ b + d [MOD n]
[PROOFSTEP]
rw [modEq_iff_dvd, Int.ofNat_add, Int.ofNat_add, add_sub_add_comm]
[GOAL]
m n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : c ≡ d [MOD n]
⊢ ↑n ∣ ↑b - ↑a + (↑d - ↑c)
[PROOFSTEP]
exact dvd_add h₁.dvd h₂.dvd
[GOAL]
m n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : a + c ≡ b + d [MOD n]
⊢ c ≡ d [MOD n]
[PROOFSTEP]
simp only [modEq_iff_dvd, Int.ofNat_add] at *
[GOAL]
m n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b + ↑d - (↑a + ↑c)
⊢ ↑n ∣ ↑d - ↑c
[PROOFSTEP]
rw [add_sub_add_comm] at h₂
[GOAL]
m n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b - ↑a + (↑d - ↑c)
⊢ ↑n ∣ ↑d - ↑c
[PROOFSTEP]
convert _root_.dvd_sub h₂ h₁ using 1
[GOAL]
case h.e'_4
m n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b - ↑a + (↑d - ↑c)
⊢ ↑d - ↑c = ↑b - ↑a + (↑d - ↑c) - (↑b - ↑a)
[PROOFSTEP]
rw [add_sub_cancel']
[GOAL]
m n a b c d : ℕ
h₁ : c ≡ d [MOD n]
h₂ : a + c ≡ b + d [MOD n]
⊢ a ≡ b [MOD n]
[PROOFSTEP]
rw [add_comm a, add_comm b] at h₂
[GOAL]
m n a b c d : ℕ
h₁ : c ≡ d [MOD n]
h₂ : c + a ≡ d + b [MOD n]
⊢ a ≡ b [MOD n]
[PROOFSTEP]
exact h₁.add_left_cancel h₂
[GOAL]
m✝ n a✝ b✝ c✝ d a b c m : ℕ
hc : c ≠ 0
⊢ c * a ≡ c * b [MOD c * m] → a ≡ b [MOD m]
[PROOFSTEP]
simp [modEq_iff_dvd, ← mul_sub, mul_dvd_mul_iff_left (by simp [hc] : (c : ℤ) ≠ 0)]
[GOAL]
m✝ n a✝ b✝ c✝ d a b c m : ℕ
hc : c ≠ 0
⊢ ↑c ≠ 0
[PROOFSTEP]
simp [hc]
[GOAL]
m✝ n a✝ b✝ c✝ d a b c m : ℕ
hc : c ≠ 0
⊢ a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m]
[PROOFSTEP]
simp [modEq_iff_dvd, ← sub_mul, mul_dvd_mul_iff_right (by simp [hc] : (c : ℤ) ≠ 0)]
[GOAL]
m✝ n a✝ b✝ c✝ d a b c m : ℕ
hc : c ≠ 0
⊢ ↑c ≠ 0
[PROOFSTEP]
simp [hc]
[GOAL]
m✝ n a b c d m : ℕ
h : a ≡ b [MOD m * n]
⊢ a ≡ b [MOD n]
[PROOFSTEP]
rw [modEq_iff_dvd] at *
[GOAL]
m✝ n a b c d m : ℕ
h : ↑(m * n) ∣ ↑b - ↑a
⊢ ↑n ∣ ↑b - ↑a
[PROOFSTEP]
exact (dvd_mul_left (n : ℤ) (m : ℤ)).trans h
[GOAL]
m n a b c d : ℕ
h : a / c ≡ b / c [MOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a ≡ b [MOD m]
[PROOFSTEP]
convert h.mul_left' c
[GOAL]
case h.e'_1
m n a b c d : ℕ
h : a / c ≡ b / c [MOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ m = c * (m / c)
[PROOFSTEP]
rwa [Nat.mul_div_cancel']
[GOAL]
case h.e'_2
m n a b c d : ℕ
h : a / c ≡ b / c [MOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a = c * (a / c)
[PROOFSTEP]
rwa [Nat.mul_div_cancel']
[GOAL]
case h.e'_3
m n a b c d : ℕ
h : a / c ≡ b / c [MOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ b = c * (b / c)
[PROOFSTEP]
rwa [Nat.mul_div_cancel']
[GOAL]
m n a b c d : ℕ
h : b ≤ a
⊢ ↑(a - b) ∣ ↑a - ↑b
[PROOFSTEP]
rw [Int.ofNat_sub h]
[GOAL]
m n a b c d : ℕ
⊢ a ≡ b [MOD 0] ↔ a = b
[PROOFSTEP]
rw [ModEq, mod_zero, mod_zero]
[GOAL]
m n a b c d : ℕ
⊢ n + a ≡ a [MOD n]
[PROOFSTEP]
rw [ModEq, add_mod_left]
[GOAL]
m n a b c d : ℕ
⊢ a + n ≡ a [MOD n]
[PROOFSTEP]
rw [ModEq, add_mod_right]
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ d ∣ a ↔ d ∣ b
[PROOFSTEP]
simp only [← modEq_zero_iff_dvd]
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]
[PROOFSTEP]
replace h := h.of_dvd hdm
[GOAL]
m n a b c d : ℕ
hdm : d ∣ m
h : a ≡ b [MOD d]
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]
[PROOFSTEP]
exact ⟨h.symm.trans, h.trans⟩
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD m]
⊢ gcd a m = gcd b m
[PROOFSTEP]
have h1 := gcd_dvd_right a m
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD m]
h1 : gcd a m ∣ m
⊢ gcd a m = gcd b m
[PROOFSTEP]
have h2 := gcd_dvd_right b m
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD m]
h1 : gcd a m ∣ m
h2 : gcd b m ∣ m
⊢ gcd a m = gcd b m
[PROOFSTEP]
exact
  dvd_antisymm (dvd_gcd ((h.dvd_iff h1).mp (gcd_dvd_left a m)) h1) (dvd_gcd ((h.dvd_iff h2).mpr (gcd_dvd_left b m)) h2)
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD m]
h2 : |↑b - ↑a| < ↑m
⊢ a = b
[PROOFSTEP]
apply Int.ofNat.inj
[GOAL]
case x
m n a b c d : ℕ
h : a ≡ b [MOD m]
h2 : |↑b - ↑a| < ↑m
⊢ Int.ofNat a = Int.ofNat b
[PROOFSTEP]
rw [eq_comm, ← sub_eq_zero]
[GOAL]
case x
m n a b c d : ℕ
h : a ≡ b [MOD m]
h2 : |↑b - ↑a| < ↑m
⊢ Int.ofNat b - Int.ofNat a = 0
[PROOFSTEP]
exact Int.eq_zero_of_abs_lt_dvd h.dvd h2
[GOAL]
m n a b c d : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
⊢ a ≡ b [MOD m / gcd m c]
[PROOFSTEP]
let d := gcd m c
[GOAL]
m n a b c d✝ : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := gcd m c
⊢ a ≡ b [MOD m / gcd m c]
[PROOFSTEP]
have hmd := gcd_dvd_left m c
[GOAL]
m n a b c d✝ : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := gcd m c
hmd : gcd m c ∣ m
⊢ a ≡ b [MOD m / gcd m c]
[PROOFSTEP]
have hcd := gcd_dvd_right m c
[GOAL]
m n a b c d✝ : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := gcd m c
hmd : gcd m c ∣ m
hcd : gcd m c ∣ c
⊢ a ≡ b [MOD m / gcd m c]
[PROOFSTEP]
rw [modEq_iff_dvd]
[GOAL]
m n a b c d✝ : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := gcd m c
hmd : gcd m c ∣ m
hcd : gcd m c ∣ c
⊢ ↑(m / gcd m c) ∣ ↑b - ↑a
[PROOFSTEP]
refine' @Int.dvd_of_dvd_mul_right_of_gcd_one (m / d) (c / d) (b - a) _ _
[GOAL]
case refine'_1
m n a b c d✝ : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := gcd m c
hmd : gcd m c ∣ m
hcd : gcd m c ∣ c
⊢ ↑m / ↑d ∣ ↑c / ↑d * (↑b - ↑a)
case refine'_2
m n a b c d✝ : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := gcd m c
hmd : gcd m c ∣ m
hcd : gcd m c ∣ c
⊢ Int.gcd (↑m / ↑d) (↑c / ↑d) = 1
[PROOFSTEP]
show (m / d : ℤ) ∣ c / d * (b - a)
[GOAL]
case refine'_1
m n a b c d✝ : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := gcd m c
hmd : gcd m c ∣ m
hcd : gcd m c ∣ c
⊢ ↑m / ↑d ∣ ↑c / ↑d * (↑b - ↑a)
[PROOFSTEP]
rw [mul_comm, ← Int.mul_ediv_assoc (b - a) (Int.coe_nat_dvd.mpr hcd), mul_comm]
[GOAL]
case refine'_1
m n a b c d✝ : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := gcd m c
hmd : gcd m c ∣ m
hcd : gcd m c ∣ c
⊢ ↑m / ↑d ∣ ↑c * (↑b - ↑a) / ↑(gcd m c)
[PROOFSTEP]
apply Int.ediv_dvd_ediv (Int.coe_nat_dvd.mpr hmd)
[GOAL]
case refine'_1
m n a b c d✝ : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := gcd m c
hmd : gcd m c ∣ m
hcd : gcd m c ∣ c
⊢ ↑m ∣ ↑c * (↑b - ↑a)
[PROOFSTEP]
rw [mul_sub]
[GOAL]
case refine'_1
m n a b c d✝ : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := gcd m c
hmd : gcd m c ∣ m
hcd : gcd m c ∣ c
⊢ ↑m ∣ ↑c * ↑b - ↑c * ↑a
[PROOFSTEP]
exact modEq_iff_dvd.mp h
[GOAL]
case refine'_2
m n a b c d✝ : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := gcd m c
hmd : gcd m c ∣ m
hcd : gcd m c ∣ c
⊢ Int.gcd (↑m / ↑d) (↑c / ↑d) = 1
[PROOFSTEP]
show Int.gcd (m / d) (c / d) = 1
[GOAL]
case refine'_2
m n a b c d✝ : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := gcd m c
hmd : gcd m c ∣ m
hcd : gcd m c ∣ c
⊢ Int.gcd (↑m / ↑d) (↑c / ↑d) = 1
[PROOFSTEP]
simp only [← Int.coe_nat_div, Int.coe_nat_gcd (m / d) (c / d), gcd_div hmd hcd, Nat.div_self (gcd_pos_of_pos_left c hm)]
[GOAL]
m n a b c d : ℕ
hm : 0 < m
h : a * c ≡ b * c [MOD m]
⊢ a ≡ b [MOD m / gcd m c]
[PROOFSTEP]
apply cancel_left_div_gcd hm
[GOAL]
m n a b c d : ℕ
hm : 0 < m
h : a * c ≡ b * c [MOD m]
⊢ c * a ≡ c * b [MOD m]
[PROOFSTEP]
simpa [mul_comm] using h
[GOAL]
m n a b c d : ℕ
hmc : gcd m c = 1
h : c * a ≡ c * b [MOD m]
⊢ a ≡ b [MOD m]
[PROOFSTEP]
rcases m.eq_zero_or_pos with (rfl | hm)
[GOAL]
case inl
n a b c d : ℕ
hmc : gcd 0 c = 1
h : c * a ≡ c * b [MOD 0]
⊢ a ≡ b [MOD 0]
[PROOFSTEP]
simp only [gcd_zero_left] at hmc
[GOAL]
case inl
n a b c d : ℕ
hmc : c = 1
h : c * a ≡ c * b [MOD 0]
⊢ a ≡ b [MOD 0]
[PROOFSTEP]
simp only [gcd_zero_left, hmc, one_mul, modEq_zero_iff] at h
[GOAL]
case inl
n a b c d : ℕ
hmc : c = 1
h : a = b
⊢ a ≡ b [MOD 0]
[PROOFSTEP]
subst h
[GOAL]
case inl
n a c d : ℕ
hmc : c = 1
⊢ a ≡ a [MOD 0]
[PROOFSTEP]
rfl
[GOAL]
case inr
m n a b c d : ℕ
hmc : gcd m c = 1
h : c * a ≡ c * b [MOD m]
hm : m > 0
⊢ a ≡ b [MOD m]
[PROOFSTEP]
simpa [hmc] using h.cancel_left_div_gcd hm
[GOAL]
m n a b c d : ℕ
hmc : gcd m c = 1
h : a * c ≡ b * c [MOD m]
⊢ c * a ≡ c * b [MOD m]
[PROOFSTEP]
simpa [mul_comm] using h
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : n = 0
⊢ a ≡ a [MOD n] ∧ a ≡ b [MOD m]
[PROOFSTEP]
rw [hn, gcd_zero_left] at h
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
⊢ a ≡ a [MOD n] ∧ a ≡ b [MOD m]
[PROOFSTEP]
constructor
[GOAL]
case left
m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
⊢ a ≡ a [MOD n]
case right m n a b c d : ℕ h : a ≡ b [MOD m] hn : n = 0 ⊢ a ≡ b [MOD m]
[PROOFSTEP]
rfl
[GOAL]
case right
m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
⊢ a ≡ b [MOD m]
[PROOFSTEP]
exact h
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ a [MOD n] ∧ b ≡ b [MOD m]
[PROOFSTEP]
rw [hm, gcd_zero_right] at h
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ a [MOD n] ∧ b ≡ b [MOD m]
[PROOFSTEP]
constructor
[GOAL]
case left
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ a [MOD n]
case right m n a b c d : ℕ h : a ≡ b [MOD n] hn : ¬n = 0 hm : m = 0 ⊢ b ≡ b [MOD m]
[PROOFSTEP]
exact h.symm
[GOAL]
case right
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ b [MOD m]
[PROOFSTEP]
rfl
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
⊢ (match xgcd n m with
      | (c, d) => Int.toNat ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(gcd n m) % ↑(lcm n m))) ≡
      a [MOD n] ∧
    (match xgcd n m with
      | (c, d) => Int.toNat ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(gcd n m) % ↑(lcm n m))) ≡
      b [MOD m]
[PROOFSTEP]
rw [xgcd_val]
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
⊢ (match (gcdA n m, gcdB n m) with
      | (c, d) => Int.toNat ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(gcd n m) % ↑(lcm n m))) ≡
      a [MOD n] ∧
    (match (gcdA n m, gcdB n m) with
      | (c, d) => Int.toNat ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(gcd n m) % ↑(lcm n m))) ≡
      b [MOD m]
[PROOFSTEP]
dsimp
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
⊢ Int.toNat ((↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) % ↑(lcm n m)) ≡ a [MOD n] ∧
    Int.toNat ((↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) % ↑(lcm n m)) ≡ b [MOD m]
[PROOFSTEP]
rw [modEq_iff_dvd, modEq_iff_dvd, Int.toNat_of_nonneg (Int.emod_nonneg _ (Int.coe_nat_ne_zero.2 (lcm_ne_zero hn hm)))]
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
⊢ ↑n ∣ ↑a - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) % ↑(lcm n m) ∧
    ↑m ∣ ↑b - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) % ↑(lcm n m)
[PROOFSTEP]
have hnonzero : (gcd n m : ℤ) ≠ 0 := by
  norm_cast
  rw [Nat.gcd_eq_zero_iff, not_and]
  exact fun _ => hm
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
⊢ ↑(gcd n m) ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
⊢ ¬gcd n m = 0
[PROOFSTEP]
rw [Nat.gcd_eq_zero_iff, not_and]
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
⊢ n = 0 → ¬m = 0
[PROOFSTEP]
exact fun _ => hm
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
⊢ ↑n ∣ ↑a - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) % ↑(lcm n m) ∧
    ↑m ∣ ↑b - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) % ↑(lcm n m)
[PROOFSTEP]
have hcoedvd : ∀ t, (gcd n m : ℤ) ∣ t * (b - a) := fun t => h.dvd.mul_left _
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
⊢ ↑n ∣ ↑a - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) % ↑(lcm n m) ∧
    ↑m ∣ ↑b - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) % ↑(lcm n m)
[PROOFSTEP]
have := gcd_eq_gcd_ab n m
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ ↑n ∣ ↑a - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) % ↑(lcm n m) ∧
    ↑m ∣ ↑b - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) % ↑(lcm n m)
[PROOFSTEP]
constructor
[GOAL]
case left
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ ↑n ∣ ↑a - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) % ↑(lcm n m)
[PROOFSTEP]
rw [Int.emod_def, ← sub_add]
[GOAL]
case right
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ ↑m ∣ ↑b - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) % ↑(lcm n m)
[PROOFSTEP]
rw [Int.emod_def, ← sub_add]
[GOAL]
case left
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ ↑n ∣
    ↑a - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) +
      ↑(lcm n m) * ((↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) / ↑(lcm n m))
[PROOFSTEP]
refine' dvd_add _ (dvd_mul_of_dvd_left _ _)
[GOAL]
case right
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ ↑m ∣
    ↑b - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) +
      ↑(lcm n m) * ((↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m) / ↑(lcm n m))
[PROOFSTEP]
refine' dvd_add _ (dvd_mul_of_dvd_left _ _)
[GOAL]
case left.refine'_1
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ ↑n ∣ ↑a - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m)
[PROOFSTEP]
try norm_cast
[GOAL]
case left.refine'_1
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ ↑n ∣ ↑a - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m)
[PROOFSTEP]
norm_cast
[GOAL]
case left.refine'_2
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ ↑n ∣ ↑(lcm n m)
[PROOFSTEP]
try norm_cast
[GOAL]
case left.refine'_2
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ ↑n ∣ ↑(lcm n m)
[PROOFSTEP]
norm_cast
[GOAL]
case right.refine'_1
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ ↑m ∣ ↑b - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m)
[PROOFSTEP]
try norm_cast
[GOAL]
case right.refine'_1
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ ↑m ∣ ↑b - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m)
[PROOFSTEP]
norm_cast
[GOAL]
case right.refine'_2
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ ↑m ∣ ↑(lcm n m)
[PROOFSTEP]
try norm_cast
[GOAL]
case right.refine'_2
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ ↑m ∣ ↑(lcm n m)
[PROOFSTEP]
norm_cast
[GOAL]
case left.refine'_1
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ ↑n ∣ ↑a - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m)
[PROOFSTEP]
rw [← sub_eq_iff_eq_add'] at this
[GOAL]
case left.refine'_1
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) - ↑n * gcdA n m = ↑m * gcdB n m
⊢ ↑n ∣ ↑a - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m)
[PROOFSTEP]
rw [← this, sub_mul, ← add_sub_assoc, add_comm, add_sub_assoc, ← mul_sub, Int.add_ediv_of_dvd_left,
  Int.mul_ediv_cancel_left _ hnonzero, Int.mul_ediv_assoc _ h.dvd, ← sub_sub, sub_self, zero_sub, dvd_neg, mul_assoc]
[GOAL]
case left.refine'_1
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) - ↑n * gcdA n m = ↑m * gcdB n m
⊢ ↑n ∣ ↑n * (gcdA n m * ((↑b - ↑a) / ↑(gcd n m)))
case left.refine'_1
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) - ↑n * gcdA n m = ↑m * gcdB n m
⊢ ↑(gcd n m) ∣ ↑(gcd n m) * ↑a
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
case left.refine'_1
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) - ↑n * gcdA n m = ↑m * gcdB n m
⊢ ↑(gcd n m) ∣ ↑(gcd n m) * ↑a
[PROOFSTEP]
norm_cast
[GOAL]
case left.refine'_1
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) - ↑n * gcdA n m = ↑m * gcdB n m
⊢ gcd n m ∣ gcd n m * a
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
case left.refine'_2
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ n ∣ lcm n m
[PROOFSTEP]
exact dvd_lcm_left n m
[GOAL]
case right.refine'_1
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ ↑m ∣ ↑b - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m)
[PROOFSTEP]
rw [← sub_eq_iff_eq_add] at this
[GOAL]
case right.refine'_1
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) - ↑m * gcdB n m = ↑n * gcdA n m
⊢ ↑m ∣ ↑b - (↑n * gcdA n m * ↑b + ↑m * gcdB n m * ↑a) / ↑(gcd n m)
[PROOFSTEP]
rw [← this, sub_mul, sub_add, ← mul_sub, Int.sub_ediv_of_dvd, Int.mul_ediv_cancel_left _ hnonzero,
  Int.mul_ediv_assoc _ h.dvd, ← sub_add, sub_self, zero_add, mul_assoc]
[GOAL]
case right.refine'_1
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) - ↑m * gcdB n m = ↑n * gcdA n m
⊢ ↑m ∣ ↑m * (gcdB n m * ((↑b - ↑a) / ↑(gcd n m)))
case right.refine'_1.hcb
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) - ↑m * gcdB n m = ↑n * gcdA n m
⊢ ↑(gcd n m) ∣ ↑m * gcdB n m * (↑b - ↑a)
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
case right.refine'_1.hcb
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) - ↑m * gcdB n m = ↑n * gcdA n m
⊢ ↑(gcd n m) ∣ ↑m * gcdB n m * (↑b - ↑a)
[PROOFSTEP]
exact hcoedvd _
[GOAL]
case right.refine'_2
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(gcd n m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(gcd n m) ∣ t * (↑b - ↑a)
this : ↑(gcd n m) = ↑n * gcdA n m + ↑m * gcdB n m
⊢ m ∣ lcm n m
[PROOFSTEP]
exact dvd_lcm_right n m
[GOAL]
m n a✝ b✝ c d : ℕ
co : coprime n m
a b : ℕ
⊢ a ≡ b [MOD gcd n m]
[PROOFSTEP]
convert @modEq_one a b
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ↑(chineseRemainder' h) < lcm n m
[PROOFSTEP]
dsimp only [chineseRemainder']
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ↑(if hn : n = 0 then { val := a, property := (_ : a ≡ a [MOD n] ∧ a ≡ b [MOD m]) }
      else
        if hm : m = 0 then { val := b, property := (_ : b ≡ a [MOD n] ∧ b ≡ b [MOD m]) }
        else
          { val := Int.toNat ((↑n * (xgcd n m).fst * ↑b + ↑m * (xgcd n m).snd * ↑a) / ↑(gcd n m) % ↑(lcm n m)),
            property :=
              (_ :
                (match xgcd n m with
                    | (c, d) => Int.toNat ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(gcd n m) % ↑(lcm n m))) ≡
                    a [MOD n] ∧
                  (match xgcd n m with
                    | (c, d) => Int.toNat ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(gcd n m) % ↑(lcm n m))) ≡
                    b [MOD m]) }) <
    lcm n m
[PROOFSTEP]
rw [dif_neg hn, dif_neg hm, Subtype.coe_mk, xgcd_val, ← Int.toNat_coe_nat (lcm n m)]
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : n ≠ 0
hm : m ≠ 0
⊢ Int.toNat
      ((↑n * (gcdA n m, gcdB n m).fst * ↑b + ↑m * (gcdA n m, gcdB n m).snd * ↑a) / ↑(gcd n m) %
        ↑(Int.toNat ↑(lcm n m))) <
    Int.toNat ↑(lcm n m)
[PROOFSTEP]
have lcm_pos := Int.coe_nat_pos.mpr (Nat.pos_of_ne_zero (lcm_ne_zero hn hm))
[GOAL]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : n ≠ 0
hm : m ≠ 0
lcm_pos : 0 < ↑(lcm n m)
⊢ Int.toNat
      ((↑n * (gcdA n m, gcdB n m).fst * ↑b + ↑m * (gcdA n m, gcdB n m).snd * ↑a) / ↑(gcd n m) %
        ↑(Int.toNat ↑(lcm n m))) <
    Int.toNat ↑(lcm n m)
[PROOFSTEP]
exact (Int.toNat_lt_toNat lcm_pos).mpr (Int.emod_lt_of_pos _ lcm_pos)
[GOAL]
m✝ n✝ a✝ b✝ c d a b m n : ℕ
hmn : coprime m n
h : a ≡ b [MOD m] ∧ a ≡ b [MOD n]
⊢ a ≡ b [MOD m * n]
[PROOFSTEP]
rw [Nat.modEq_iff_dvd, Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.coe_nat_dvd, ← Int.dvd_natAbs, Int.coe_nat_dvd] at h
[GOAL]
m✝ n✝ a✝ b✝ c d a b m n : ℕ
hmn : coprime m n
h : m ∣ Int.natAbs (↑b - ↑a) ∧ n ∣ Int.natAbs (↑b - ↑a)
⊢ a ≡ b [MOD m * n]
[PROOFSTEP]
rw [Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.coe_nat_dvd]
[GOAL]
m✝ n✝ a✝ b✝ c d a b m n : ℕ
hmn : coprime m n
h : m ∣ Int.natAbs (↑b - ↑a) ∧ n ∣ Int.natAbs (↑b - ↑a)
⊢ m * n ∣ Int.natAbs (↑b - ↑a)
[PROOFSTEP]
exact hmn.mul_dvd_of_dvd_of_dvd h.1 h.2
[GOAL]
m n✝ a✝ b✝ c d b a n : ℕ
h : a * b ≡ 1 [MOD n]
⊢ coprime a n
[PROOFSTEP]
obtain ⟨g, hh⟩ := Nat.gcd_dvd_right a n
[GOAL]
case intro
m n✝ a✝ b✝ c d b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = gcd a n * g
⊢ coprime a n
[PROOFSTEP]
rw [Nat.coprime_iff_gcd_eq_one, ← Nat.dvd_one, ← Nat.modEq_zero_iff_dvd]
[GOAL]
case intro
m n✝ a✝ b✝ c d b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = gcd a n * g
⊢ 1 ≡ 0 [MOD gcd a n]
[PROOFSTEP]
calc
  1 ≡ a * b [MOD a.gcd n] := (hh ▸ h).symm.of_mul_right g
  _ ≡ 0 * b [MOD a.gcd n] := ((Nat.modEq_zero_iff_dvd.mpr (Nat.gcd_dvd_left _ _)).mul_right b)
  _ = 0 := by rw [zero_mul]
[GOAL]
m n✝ a✝ b✝ c d b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = gcd a n * g
⊢ 0 * b = 0
[PROOFSTEP]
rw [zero_mul]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hb0 : b = 0
⊢ a / b % c = a % (b * c) / b
[PROOFSTEP]
simp [hb0]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hb0 : ¬b = 0
⊢ a / b % c = a % (b * c) / b
[PROOFSTEP]
rw [← @add_right_cancel_iff _ _ _ (c * (a / b / c)), mod_add_div, Nat.div_div_eq_div_mul, ← mul_right_inj' hb0, ←
  @add_left_cancel_iff _ _ _ (a % b), mod_add_div, mul_add, ← @add_left_cancel_iff _ _ _ (a % (b * c) % b),
  add_left_comm, ← add_assoc (a % (b * c) % b), mod_add_div, ← mul_assoc, mod_add_div, mod_mul_right_mod]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : c = 0
⊢ ((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c
[PROOFSTEP]
simp [hc0, Nat.mod_zero]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
⊢ ((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c
[PROOFSTEP]
rw [this]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
⊢ ((a % c + b % c) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
m n a✝ b✝ c✝ d a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
⊢ (a % c + b % c) % c + c = a % c + b % c
[PROOFSTEP]
have h2 : (a % c + b % c) / c < 2 :=
  Nat.div_lt_of_lt_mul
    (by
      rw [mul_two]
      exact add_lt_add (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0)) (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0)))
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
⊢ a % c + b % c < c * 2
[PROOFSTEP]
rw [mul_two]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
⊢ a % c + b % c < c + c
[PROOFSTEP]
exact add_lt_add (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0)) (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0))
[GOAL]
case pos
m n a✝ b✝ c✝ d a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
⊢ (a % c + b % c) % c + c = a % c + b % c
[PROOFSTEP]
have h0 : 0 < (a % c + b % c) / c := Nat.div_pos h (Nat.pos_of_ne_zero hc0)
[GOAL]
case pos
m n a✝ b✝ c✝ d a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
h0 : 0 < (a % c + b % c) / c
⊢ (a % c + b % c) % c + c = a % c + b % c
[PROOFSTEP]
rw [← @add_right_cancel_iff _ _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc, mod_add_div,
  le_antisymm (le_of_lt_succ h2) h0, mul_one, add_comm]
[GOAL]
case neg
m n a✝ b✝ c✝ d a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : ¬c ≤ a % c + b % c
⊢ (a % c + b % c) % c + 0 = a % c + b % c
[PROOFSTEP]
rw [Nat.mod_eq_of_lt (lt_of_not_ge h), add_zero]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc : a % c + b % c < c
⊢ (a + b) % c = a % c + b % c
[PROOFSTEP]
rw [← add_mod_add_ite, if_neg (not_le_of_lt hc), add_zero]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc : c ≤ a % c + b % c
⊢ (a + b) % c + c = a % c + b % c
[PROOFSTEP]
rw [← add_mod_add_ite, if_pos hc]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ (a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0
[PROOFSTEP]
rw [← mul_right_inj' hc0.ne', ← @add_left_cancel_iff _ _ _ ((a + b) % c + a % c + b % c)]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ (a + b) % c + a % c + b % c + c * ((a + b) / c) =
    (a + b) % c + a % c + b % c + c * (a / c + b / c + if c ≤ a % c + b % c then 1 else 0)
[PROOFSTEP]
suffices
  (a + b) % c + c * ((a + b) / c) + a % c + b % c =
    (a % c + c * (a / c) + (b % c + c * (b / c)) + c * if c ≤ a % c + b % c then 1 else 0) + (a + b) % c
  by simpa only [mul_add, add_comm, add_left_comm, add_assoc]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
this :
  (a + b) % c + c * ((a + b) / c) + a % c + b % c =
    (a % c + c * (a / c) + (b % c + c * (b / c)) + c * if c ≤ a % c + b % c then 1 else 0) + (a + b) % c
⊢ (a + b) % c + a % c + b % c + c * ((a + b) / c) =
    (a + b) % c + a % c + b % c + c * (a / c + b / c + if c ≤ a % c + b % c then 1 else 0)
[PROOFSTEP]
simpa only [mul_add, add_comm, add_left_comm, add_assoc]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ (a + b) % c + c * ((a + b) / c) + a % c + b % c =
    (a % c + c * (a / c) + (b % c + c * (b / c)) + c * if c ≤ a % c + b % c then 1 else 0) + (a + b) % c
[PROOFSTEP]
rw [mod_add_div, mod_add_div, mod_add_div, mul_ite, add_assoc, add_assoc]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ a + (b + (a % c + b % c)) = (a + b + if c ≤ a % c + b % c then c * 1 else c * 0) + (a + b) % c
[PROOFSTEP]
conv_lhs => rw [← add_mod_add_ite]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
| a + (b + (a % c + b % c))
[PROOFSTEP]
rw [← add_mod_add_ite]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
| a + (b + (a % c + b % c))
[PROOFSTEP]
rw [← add_mod_add_ite]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
| a + (b + (a % c + b % c))
[PROOFSTEP]
rw [← add_mod_add_ite]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ a + (b + ((a + b) % c + if c ≤ a % c + b % c then c else 0)) =
    (a + b + if c ≤ a % c + b % c then c * 1 else c * 0) + (a + b) % c
[PROOFSTEP]
simp
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : 0 < c
⊢ a + (b + ((a + b) % c + if c ≤ a % c + b % c then c else 0)) =
    (a + b + if c ≤ a % c + b % c then c else 0) + (a + b) % c
[PROOFSTEP]
ac_rfl
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc : a % c + b % c < c
hc0 : c = 0
⊢ (a + b) / c = a / c + b / c
[PROOFSTEP]
simp [hc0]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc : a % c + b % c < c
hc0 : ¬c = 0
⊢ (a + b) / c = a / c + b / c
[PROOFSTEP]
rw [add_div (Nat.pos_of_ne_zero hc0), if_neg (not_le_of_lt hc), add_zero]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hca : c ∣ a
h : c = 0
⊢ (a + b) / c = a / c + b / c
[PROOFSTEP]
simp [h]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hca : c ∣ a
h : ¬c = 0
⊢ a % c + b % c < c
[PROOFSTEP]
rw [Nat.mod_eq_zero_of_dvd hca, zero_add]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hca : c ∣ a
h : ¬c = 0
⊢ b % c < c
[PROOFSTEP]
exact Nat.mod_lt _ (pos_iff_ne_zero.mpr h)
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hca : c ∣ b
⊢ (a + b) / c = a / c + b / c
[PROOFSTEP]
rwa [add_comm, Nat.add_div_of_dvd_right, add_comm]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc : c ≤ a % c + b % c
hc0 : 0 < c
⊢ (a + b) / c = a / c + b / c + 1
[PROOFSTEP]
rw [add_div hc0, if_pos hc]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : c = 0
⊢ a / c + b / c ≤ (a + b) / c
[PROOFSTEP]
simp [hc0]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : ¬c = 0
⊢ a / c + b / c ≤ (a + b) / c
[PROOFSTEP]
rw [Nat.add_div (Nat.pos_of_ne_zero hc0)]
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
hc0 : ¬c = 0
⊢ a / c + b / c ≤ a / c + b / c + if c ≤ a % c + b % c then 1 else 0
[PROOFSTEP]
exact Nat.le_add_right _ _
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
h : c ∣ a + b
ha : ¬c ∣ a
hc : ¬c ≤ a % c + b % c
⊢ False
[PROOFSTEP]
have : (a + b) % c = a % c + b % c := add_mod_of_add_mod_lt (lt_of_not_ge hc)
[GOAL]
m n a✝ b✝ c✝ d a b c : ℕ
h : c ∣ a + b
ha : ¬c ∣ a
hc : ¬c ≤ a % c + b % c
this : (a + b) % c = a % c + b % c
⊢ False
[PROOFSTEP]
simp_all [dvd_iff_mod_eq_zero]
[GOAL]
m✝ n✝ a b c d n m : ℕ
⊢ n % 2 = 1 → m % 2 = 1 → n * m % 2 = 1
[PROOFSTEP]
simpa [Nat.ModEq] using @ModEq.mul 2 n 1 m 1
[GOAL]
m✝ n✝ a b c d m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
h : m = 0
⊢ False
[PROOFSTEP]
simp_all
[GOAL]
m✝ n✝ a b c d m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hm0 : 0 < m
h : n = 0
⊢ False
[PROOFSTEP]
simp_all
[GOAL]
m✝ n✝ a b c d m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hm0 : 0 < m
hn0 : 0 < n
⊢ (fun x x_1 => x * x_1) 2 (m * n / 2) = (fun x x_1 => x * x_1) 2 (m * (n / 2) + m / 2)
[PROOFSTEP]
dsimp
[GOAL]
m✝ n✝ a b c d m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hm0 : 0 < m
hn0 : 0 < n
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)
[PROOFSTEP]
rw [mul_add, two_mul_odd_div_two hm1, mul_left_comm, two_mul_odd_div_two hn1,
  two_mul_odd_div_two (Nat.odd_mul_odd hm1 hn1), mul_tsub, mul_one, ← add_tsub_assoc_of_le (succ_le_of_lt hm0),
  tsub_add_cancel_of_le (le_mul_of_one_le_right (Nat.zero_le _) hn0)]
[GOAL]
m n✝ a b c d n : ℕ
⊢ n % 4 = 1 → n % 2 = 1
[PROOFSTEP]
simpa [ModEq, show 2 * 2 = 4 by norm_num] using @ModEq.of_mul_left 2 n 1 2
[GOAL]
m n✝ a b c d n : ℕ
⊢ 2 * 2 = 4
[PROOFSTEP]
norm_num
[GOAL]
m n✝ a b c d n : ℕ
⊢ n % 4 = 3 → n % 2 = 1
[PROOFSTEP]
simpa [ModEq, show 2 * 2 = 4 by norm_num, show 3 % 4 = 3 by norm_num] using @ModEq.of_mul_left 2 n 3 2
[GOAL]
m n✝ a b c d n : ℕ
⊢ 2 * 2 = 4
[PROOFSTEP]
norm_num
[GOAL]
m n✝ a b c d n : ℕ
⊢ 3 % 4 = 3
[PROOFSTEP]
norm_num
[GOAL]
m n✝ a b c d n : ℕ
⊢ ∀ (m : ℕ), m < 4 → m % 2 = 1 → m = 1 ∨ m = 3
[PROOFSTEP]
decide
[GOAL]
m n✝ a b c d n : ℕ
help : ∀ (m : ℕ), m < 4 → m % 2 = 1 → m = 1 ∨ m = 3
hn : n % 2 = 1
⊢ 4 > 0
[PROOFSTEP]
norm_num
[GOAL]
m n✝ a b c d n : ℕ
help : ∀ (m : ℕ), m < 4 → m % 2 = 1 → m = 1 ∨ m = 3
hn : n % 2 = 1
⊢ 2 ∣ 4
[PROOFSTEP]
norm_num


[GOAL]
n k : ℕ
⊢ List.toFinset (factors (n ^ (k + 1))) = List.toFinset (factors n)
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
k : ℕ
⊢ List.toFinset (factors (0 ^ (k + 1))) = List.toFinset (factors 0)
[PROOFSTEP]
simp
[GOAL]
case inr
n k : ℕ
hn : n ≠ 0
⊢ List.toFinset (factors (n ^ (k + 1))) = List.toFinset (factors n)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case inr.zero
n : ℕ
hn : n ≠ 0
⊢ List.toFinset (factors (n ^ (zero + 1))) = List.toFinset (factors n)
[PROOFSTEP]
simp
[GOAL]
case inr.succ
n : ℕ
hn : n ≠ 0
k : ℕ
ih : List.toFinset (factors (n ^ (k + 1))) = List.toFinset (factors n)
⊢ List.toFinset (factors (n ^ (succ k + 1))) = List.toFinset (factors n)
[PROOFSTEP]
rw [pow_succ', factors_mul_toFinset hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]
[GOAL]
n k : ℕ
hk : k ≠ 0
⊢ List.toFinset (factors (n ^ k)) = List.toFinset (factors n)
[PROOFSTEP]
cases k
[GOAL]
case zero
n : ℕ
hk : zero ≠ 0
⊢ List.toFinset (factors (n ^ zero)) = List.toFinset (factors n)
[PROOFSTEP]
simp at hk
[GOAL]
case succ
n n✝ : ℕ
hk : succ n✝ ≠ 0
⊢ List.toFinset (factors (n ^ succ n✝)) = List.toFinset (factors n)
[PROOFSTEP]
rw [pow_succ_factors_toFinset]
[GOAL]
p k : ℕ
hk : k ≠ 0
hp : Prime p
⊢ List.toFinset (factors (p ^ k)) = {p}
[PROOFSTEP]
simp [pow_factors_toFinset p hk, factors_prime hp]


[GOAL]
⊢ {0} ∪ range succ = univ
[PROOFSTEP]
ext n
[GOAL]
case h
n : ℕ
⊢ n ∈ {0} ∪ range succ ↔ n ∈ univ
[PROOFSTEP]
cases n
[GOAL]
case h.zero
⊢ zero ∈ {0} ∪ range succ ↔ zero ∈ univ
[PROOFSTEP]
simp
[GOAL]
case h.succ
n✝ : ℕ
⊢ succ n✝ ∈ {0} ∪ range succ ↔ succ n✝ ∈ univ
[PROOFSTEP]
simp
[GOAL]
⊢ range succ = {i | 0 < i}
[PROOFSTEP]
ext (_ | i)
[GOAL]
case h.zero
⊢ zero ∈ range succ ↔ zero ∈ {i | 0 < i}
[PROOFSTEP]
simp [succ_pos, succ_ne_zero, Set.mem_setOf]
[GOAL]
case h.succ
i : ℕ
⊢ succ i ∈ range succ ↔ succ i ∈ {i | 0 < i}
[PROOFSTEP]
simp [succ_pos, succ_ne_zero, Set.mem_setOf]
[GOAL]
α : Type u_1
f : ℕ → α
⊢ {f 0} ∪ range (f ∘ succ) = range f
[PROOFSTEP]
rw [← image_singleton, range_comp, ← image_union, zero_union_range_succ, image_univ]
[GOAL]
α✝ : Type u_1
α : Type u_2
x : α
f : ℕ → α → α
⊢ (range fun n => rec x f n) = {x} ∪ range fun n => rec (f 0 x) (f ∘ succ) n
[PROOFSTEP]
convert (range_of_succ (fun n => Nat.rec x f n : ℕ → α)).symm using 4
[GOAL]
case h.e'_3.h.e'_4.h.e'_3.h
α✝ : Type u_1
α : Type u_2
x : α
f : ℕ → α → α
x✝ : ℕ
⊢ rec (f 0 x) (f ∘ succ) x✝ = ((fun n => rec x f n) ∘ succ) x✝
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_3.h.e'_4.h.e'_3.h
α✝ : Type u_1
α : Type u_2
x : α
f : ℕ → α → α
x✝ : ℕ
⊢ rec (f 0 x) (f ∘ succ) x✝ = f x✝ (rec x f x✝)
[PROOFSTEP]
rename_i n
[GOAL]
case h.e'_3.h.e'_4.h.e'_3.h
α✝ : Type u_1
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
⊢ rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case h.e'_3.h.e'_4.h.e'_3.h.zero
α✝ : Type u_1
α : Type u_2
x : α
f : ℕ → α → α
⊢ rec (f 0 x) (f ∘ succ) zero = f zero (rec x f zero)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3.h.e'_4.h.e'_3.h.succ
α✝ : Type u_1
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ rec (f 0 x) (f ∘ succ) (succ n) = f (succ n) (rec x f (succ n))
[PROOFSTEP]
dsimp at ihn ⊢
[GOAL]
case h.e'_3.h.e'_4.h.e'_3.h.succ
α✝ : Type u_1
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ f (succ n) (rec (f 0 x) (f ∘ succ) n) = f (succ n) (f n (rec x f n))
[PROOFSTEP]
rw [ihn]


[GOAL]
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ HEq (evenOddRec h0 h_even h_odd (bit false n)) (h_even n (evenOddRec h0 h_even h_odd n))
[PROOFSTEP]
rw [evenOddRec, binaryRec_eq]
[GOAL]
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ HEq
    (match false, n,
      binaryRec h0
        (fun x x_1 x_2 =>
          match x, x_1, x_2 with
          | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
          | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
        n with
    | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
    | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
    (h_even n (evenOddRec h0 h_even h_odd n))
case h
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ (match false, 0, h0 with
    | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
    | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =
    h0
[PROOFSTEP]
apply eq_rec_heq
[GOAL]
case h
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ (match false, 0, h0 with
    | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
    | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =
    h0
[PROOFSTEP]
exact H
[GOAL]
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ HEq (evenOddRec h0 h_even h_odd (bit true n)) (h_odd n (evenOddRec h0 h_even h_odd n))
[PROOFSTEP]
rw [evenOddRec, binaryRec_eq]
[GOAL]
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ HEq
    (match true, n,
      binaryRec h0
        (fun x x_1 x_2 =>
          match x, x_1, x_2 with
          | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
          | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
        n with
    | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
    | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
    (h_odd n (evenOddRec h0 h_even h_odd n))
case h
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ (match false, 0, h0 with
    | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
    | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =
    h0
[PROOFSTEP]
apply eq_rec_heq
[GOAL]
case h
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ (match false, 0, h0 with
    | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
    | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =
    h0
[PROOFSTEP]
exact H