-- Mathlib/Data/Nat/ChineseRemainder.lean
theorem chineseRemainderOfList_modEq_unique (l : List ι)
    (co : l.Pairwise (Coprime on s)) {z} (hz : ∀ i ∈ l, z ≡ a i [MOD s i]) :
    z ≡ chineseRemainderOfList a s l co [MOD (l.map s).prod]

Proof state:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ ∀ a ∈ l, (s i).Coprime (s a)

Tactic:
intro j hj

Result:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
j : ι
hj : j ∈ l
⊢ (s i).Coprime (s j)

Proof state:
case cons
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ z ≡ ↑(chineseRemainder ⋯ (a i) ↑(chineseRemainderOfList a s l ⋯)) [MOD s i * (List.map s l).prod]

Tactic:
have : Coprime (s i) (l.map s).prod := by
  simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂]
  intro j hj
  exact (List.pairwise_cons.mp co).1 j hj

Result:
case cons
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
this : (s i).Coprime (List.map s l).prod
⊢ z ≡ ↑(chineseRemainder ⋯ (a i) ↑(chineseRemainderOfList a s l ⋯)) [MOD s i * (List.map s l).prod]

Proof state:
case cons
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
this : (s i).Coprime (List.map s l).prod
⊢ z ≡ ↑(chineseRemainder ⋯ (a i) ↑(chineseRemainderOfList a s l ⋯)) [MOD s i * (List.map s l).prod]

Tactic:
exact chineseRemainder_modEq_unique this
  (hz i (List.mem_cons_self _ _)) (ih co.of_cons (fun j hj => hz j (List.mem_cons_of_mem _ hj)))

Result:
no goals

Proof state:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
j : ι
hj : j ∈ l
⊢ (s i).Coprime (s j)

Tactic:
exact (List.pairwise_cons.mp co).1 j hj

Result:
no goals

Proof state:
case cons
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ z ≡ ↑(chineseRemainderOfList a s (i :: l) co) [MOD (List.map s (i :: l)).prod]

Tactic:
simp only [List.map_cons, List.prod_cons, chineseRemainderOfList]

Result:
case cons
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ z ≡ ↑(chineseRemainder ⋯ (a i) ↑(chineseRemainderOfList a s l ⋯)) [MOD s i * (List.map s l).prod]

Proof state:
ι : Type u_1
a s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
z : ℕ
hz : ∀ i ∈ l, z ≡ a i [MOD s i]
⊢ z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]

Tactic:
induction' l with i l ih

Result:
case nil
ι : Type u_1
a s : ι → ℕ
z : ℕ
co : List.Pairwise (Coprime on s) []
hz : ∀ i ∈ [], z ≡ a i [MOD s i]
⊢ z ≡ ↑(chineseRemainderOfList a s [] co) [MOD (List.map s []).prod]

case cons
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ z ≡ ↑(chineseRemainderOfList a s (i :: l) co) [MOD (List.map s (i :: l)).prod]

Proof state:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ (s i).Coprime (List.map s l).prod

Tactic:
simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂]

Result:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ ∀ a ∈ l, (s i).Coprime (s a)

Proof state:
case nil
ι : Type u_1
a s : ι → ℕ
z : ℕ
co : List.Pairwise (Coprime on s) []
hz : ∀ i ∈ [], z ≡ a i [MOD s i]
⊢ z ≡ ↑(chineseRemainderOfList a s [] co) [MOD (List.map s []).prod]

Tactic:
simp [modEq_one]

Result:
no goals