-- Mathlib/Data/Nat/ChineseRemainder.lean
theorem chineseRemainderOfList_lt_prod (l : List ι)
    (co : l.Pairwise (Coprime on s)) (hs : ∀ i ∈ l, s i ≠ 0) :
    chineseRemainderOfList a s l co < (l.map s).prod

Proof state:
case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
⊢ ∀ x ∈ l, ¬s x = 0

Tactic:
intro j hj

Result:
case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
j : ι
hj : j ∈ l
⊢ ¬s j = 0

Proof state:
case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
⊢ ↑(chineseRemainder ⋯ (a i) ↑(chineseRemainderOfList a s l ⋯)) < s i * (List.map s l).prod

Tactic:
refine chineseRemainder_lt_mul this (a i) (chineseRemainderOfList a s l co.of_cons)
  (hs i (List.mem_cons_self _ l)) ?_

Result:
case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
⊢ (List.map s l).prod ≠ 0

Proof state:
case nil
ι : Type u_1
a s : ι → ℕ
co : List.Pairwise (Coprime on s) []
hs : ∀ i ∈ [], s i ≠ 0
⊢ ↑(chineseRemainderOfList a s [] co) < (List.map s []).prod

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
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 : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
⊢ (List.map s l).prod ≠ 0

Tactic:
simp only [ne_eq, List.prod_eq_zero_iff, List.mem_map, not_exists, not_and]

Result:
case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
⊢ ∀ x ∈ l, ¬s x = 0

Proof state:
case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
⊢ ↑(chineseRemainder ⋯ (a i) ↑(chineseRemainderOfList a s l ⋯)) < 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 : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
⊢ ↑(chineseRemainder ⋯ (a i) ↑(chineseRemainderOfList a s l ⋯)) < s i * (List.map s l).prod

Proof state:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
⊢ ∀ a ∈ l, (s i).Coprime (s a)

Tactic:
intro j hj

Result:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
j : ι
hj : j ∈ l
⊢ (s i).Coprime (s j)

Proof state:
case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
⊢ ↑(chineseRemainderOfList a s (i :: l) co) < (List.map s (i :: l)).prod

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

Result:
case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
⊢ ↑(chineseRemainder ⋯ (a i) ↑(chineseRemainderOfList a s l ⋯)) < s i * (List.map s l).prod

Proof state:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
⊢ (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 : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
⊢ ∀ a ∈ l, (s i).Coprime (s a)

Proof state:
case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
j : ι
hj : j ∈ l
⊢ ¬s j = 0

Tactic:
exact hs j (List.mem_cons_of_mem _ hj)

Result:
no goals

Proof state:
ι : Type u_1
a s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
hs : ∀ i ∈ l, s i ≠ 0
⊢ ↑(chineseRemainderOfList a s l co) < (List.map s l).prod

Tactic:
cases l with
| nil => simp
| cons i l =>
  simp only [chineseRemainderOfList, List.map_cons, List.prod_cons]
  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
  refine chineseRemainder_lt_mul this (a i) (chineseRemainderOfList a s l co.of_cons)
    (hs i (List.mem_cons_self _ l)) ?_
  simp only [ne_eq, List.prod_eq_zero_iff, List.mem_map, not_exists, not_and]
  intro j hj
  exact hs j (List.mem_cons_of_mem _ hj)

Result:
no goals