Theorem: Usa2003P1.lemma2 (Compfiles/Usa2003P1.lean)

State before:
a b c : ℕ
hb : 0 < b
h : a.Coprime b
⊢ ∃ k < b, a * k ≡ c [MOD b]
Tactic:
let ⟨N, HN1, HN2⟩ := Nat.chineseRemainder h 0 c
State after:
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
⊢ ∃ k < b, a * k ≡ c [MOD b]

State before:
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
⊢ ∃ k < b, a * k ≡ c [MOD b]
Tactic:
have ⟨x, hx⟩ : a ∣ N := Nat.modEq_zero_iff_dvd.mp HN1
State after:
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ ∃ k < b, a * k ≡ c [MOD b]

State before:
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ ∃ k < b, a * k ≡ c [MOD b]
Tactic:
use x % b
State after:
case h
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ x % b < b ∧ a * (x % b) ≡ c [MOD b]

State before:
case h
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ x % b < b ∧ a * (x % b) ≡ c [MOD b]
Tactic:
constructor
State after:
case h.left
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ x % b < b

case h.right
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ a * (x % b) ≡ c [MOD b]

State before:
case h.left
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ x % b < b
Tactic:
exact Nat.mod_lt _ hb
State after:
no goals

State before:
case h.right
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ a * (x % b) ≡ c [MOD b]
Tactic:
change N % b = c % b at HN2
State after:
case h.right
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
x : ℕ
hx : N = a * x
HN2 : N % b = c % b
⊢ a * (x % b) ≡ c [MOD b]

State before:
case h.right
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
x : ℕ
hx : N = a * x
HN2 : N % b = c % b
⊢ a * (x % b) ≡ c [MOD b]
Tactic:
change (a * (x % b)) % b = c % b
State after:
case h.right
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
x : ℕ
hx : N = a * x
HN2 : N % b = c % b
⊢ a * (x % b) % b = c % b

State before:
case h.right
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
x : ℕ
hx : N = a * x
HN2 : N % b = c % b
⊢ a * (x % b) % b = c % b
Tactic:
rw [← HN2, hx, Nat.mul_mod, Nat.mod_mod, ←Nat.mul_mod]
State after:
no goals