-- Mathlib/Data/Nat/ChineseRemainder.lean
lemma modEq_list_prod_iff' {a b} {s : ι → ℕ} {l : List ι} (co : l.Pairwise (Coprime on s)) :
    a ≡ b [MOD (l.map s).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i]

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

Tactic:
simp [← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co)]

Result:
no goals

Proof state:
ι : Type u_1
a b : ℕ
s : ι → ℕ
i : ι
l : List ι
ih : List.Pairwise (Coprime on s) l → (a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i])
co : List.Pairwise (Coprime on s) (i :: l)
⊢ (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 b : ℕ
s : ι → ℕ
i : ι
l : List ι
ih : List.Pairwise (Coprime on s) l → (a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i])
co : List.Pairwise (Coprime on s) (i :: l)
⊢ ∀ a ∈ l, (s i).Coprime (s a)

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

Tactic:
simp [modEq_one]

Result:
no goals

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

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 b : ℕ
s : ι → ℕ
i : ι
l : List ι
ih : List.Pairwise (Coprime on s) l → (a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i])
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
⊢ a ≡ b [MOD (List.map s (i :: l)).prod] ↔ ∀ i_1 ∈ i :: l, a ≡ b [MOD s i_1]

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

Tactic:
intro j hj

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

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

Tactic:
induction' l with i l ih

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

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

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

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

Result:
no goals