Theorem: Imo1989P5.general_chinese_remainder (Compfiles/Imo1989P5.lean)

State before:
case nil
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) []
⊢ ∃ m, ∀ x ∈ [], m ≡ x.remainder [MOD x.modulus]
Tactic:
use 0
State after:
case h
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) []
⊢ ∀ x ∈ [], 0 ≡ x.remainder [MOD x.modulus]

State before:
case h
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) []
⊢ ∀ x ∈ [], 0 ≡ x.remainder [MOD x.modulus]
Tactic:
decide
State after:
no goals

State before:
case cons
x : ChinesePair
xs : List ChinesePair
ih : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs → ∃ m, ∀ x ∈ xs, m ≡ x.remainder [MOD x.modulus]
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) (x :: xs)
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
Tactic:
obtain ⟨b, hb⟩ := ih x_coprime.tail
State after:
case cons.intro
x : ChinesePair
xs : List ChinesePair
ih : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs → ∃ m, ∀ x ∈ xs, m ≡ x.remainder [MOD x.modulus]
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) (x :: xs)
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]

State before:
case cons.intro
x : ChinesePair
xs : List ChinesePair
ih : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs → ∃ m, ∀ x ∈ xs, m ≡ x.remainder [MOD x.modulus]
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) (x :: xs)
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
Tactic:
clear ih
State after:
case cons.intro
x : ChinesePair
xs : List ChinesePair
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) (x :: xs)
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]

State before:
case cons.intro
x : ChinesePair
xs : List ChinesePair
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) (x :: xs)
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
Tactic:
rw [List.pairwise_cons] at x_coprime
State after:
case cons.intro
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]

State before:
case cons.intro
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
Tactic:
obtain ⟨k, hk1, hk2⟩ := Nat.chineseRemainder h1 x.remainder b
State after:
case cons.intro.mk.intro
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]

State before:
case cons.intro.mk.intro
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
Tactic:
use k
State after:
case h
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
⊢ ∀ x_1 ∈ x :: xs, k ≡ x_1.remainder [MOD x_1.modulus]

State before:
case h
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
⊢ ∀ x_1 ∈ x :: xs, k ≡ x_1.remainder [MOD x_1.modulus]
Tactic:
intro z hz
State after:
case h
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
z : ChinesePair
hz : z ∈ x :: xs
⊢ k ≡ z.remainder [MOD z.modulus]

State before:
case h
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
z : ChinesePair
hz : z ∈ x :: xs
⊢ k ≡ z.remainder [MOD z.modulus]
Tactic:
cases hz with
| head => exact hk1
| tail w hw =>
  have h2 := hb z hw
  have h4 := modulus_of_product hk2 _ (List.mem_map_of_mem ChinesePair.modulus hw)
  exact Nat.ModEq.trans h4 h2
State after:
no goals

State before:
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
⊢ ∀ y ∈ List.map (fun x => x.modulus) xs, x.modulus.Coprime y
Tactic:
intro z hz
State after:
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
z : ℕ
hz : z ∈ List.map (fun x => x.modulus) xs
⊢ x.modulus.Coprime z

State before:
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
z : ℕ
hz : z ∈ List.map (fun x => x.modulus) xs
⊢ x.modulus.Coprime z
Tactic:
aesop
State after:
no goals

State before:
case h.head
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
⊢ k ≡ x.remainder [MOD x.modulus]
Tactic:
exact hk1
State after:
no goals

State before:
case h.tail
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
z : ChinesePair
hw : List.Mem z xs
⊢ k ≡ z.remainder [MOD z.modulus]
Tactic:
have h2 := hb z hw
State after:
case h.tail
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
z : ChinesePair
hw : List.Mem z xs
h2 : b ≡ z.remainder [MOD z.modulus]
⊢ k ≡ z.remainder [MOD z.modulus]

State before:
case h.tail
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
z : ChinesePair
hw : List.Mem z xs
h2 : b ≡ z.remainder [MOD z.modulus]
⊢ k ≡ z.remainder [MOD z.modulus]
Tactic:
have h4 := modulus_of_product hk2 _ (List.mem_map_of_mem ChinesePair.modulus hw)
State after:
case h.tail
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
z : ChinesePair
hw : List.Mem z xs
h2 : b ≡ z.remainder [MOD z.modulus]
h4 : k ≡ b [MOD z.modulus]
⊢ k ≡ z.remainder [MOD z.modulus]

State before:
case h.tail
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
z : ChinesePair
hw : List.Mem z xs
h2 : b ≡ z.remainder [MOD z.modulus]
h4 : k ≡ b [MOD z.modulus]
⊢ k ≡ z.remainder [MOD z.modulus]
Tactic:
exact Nat.ModEq.trans h4 h2
State after:
no goals