awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
ih : { k : ℕ // ∀ i ∈ l, k ≡ a i [MOD s i] }
k : { k : ℕ // k ≡ a i [MOD s i] ∧ k ≡ (↑ih : ℕ) [MOD (List.map s l).prod] }
property : ∀ a_1 ∈ l, (↑k : ℕ) ≡ a a_1 [MOD s a_1]
⊢ ∀ i_1 ∈ i :: l, (↑k : ℕ) ≡ a i_1 [MOD s i_1]

Tactic:
simp only [List.mem_cons, forall_eq_or_imp, k.prop.1, true_and]

Premises used: forall_eq_or_imp, And.left, Subtype.prop, List.mem_cons, true_and
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
ih : { k : ℕ // ∀ i ∈ l, k ≡ a i [MOD s i] }
k : { k : ℕ // k ≡ a i [MOD s i] ∧ k ≡ (↑ih : ℕ) [MOD (List.map s l).prod] }
j : ι
hj : j ∈ l
⊢ (↑k : ℕ) ≡ a j [MOD s j]

Tactic:
((modEq_list_map_prod_iff co.of_cons).mp k.prop.2 j hj).trans (ih.prop j hj)

Premises used: Nat.modEq_list_map_prod_iff, And.right, Subtype.prop, Iff.mp, List.Pairwise.of_cons, Nat.ModEq.trans
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
ih : { k : ℕ // ∀ i ∈ l, k ≡ a i [MOD s i] }
k : { k : ℕ // k ≡ a i [MOD s i] ∧ k ≡ (↑ih : ℕ) [MOD (List.map s l).prod] }
j : ι
hj : j ∈ l
⊢ (↑k : ℕ) ≡ a j [MOD s j]

Tactic:
exact ((modEq_list_map_prod_iff co.of_cons).mp k.prop.2 j hj).trans (ih.prop j hj)

Premises used: Nat.modEq_list_map_prod_iff, And.right, Subtype.prop, Iff.mp, List.Pairwise.of_cons, Nat.ModEq.trans
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
⊢ (↑(chineseRemainderOfList a s [] ⋯) : ℕ) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
co : List.Pairwise (Coprime on s) []
hs : ∀ (i : ι), Membership.mem (γ := List ι) [] i → s i ≠ 0
⊢ (↑(chineseRemainderOfList a s [] co) : ℕ) < (List.map s []).prod

Tactic:
simp
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : 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
cons : (↑(chineseRemainder ⋯ (a i) (↑(chineseRemainderOfList a s l ⋯) : ℕ)) : ℕ) < s i * (List.map s l).prod
⊢ (↑(chineseRemainderOfList a s (i :: l) co) : ℕ) < (List.map s (i :: l)).prod

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

Premises used: List.map_cons, Nat.chineseRemainderOfList, List.prod_cons
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : 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
simp : ∀ a ∈ l, (s i).Coprime (s a)
⊢ (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₂]

Premises used: and_imp, forall_exists_index, List.mem_map, Nat.coprime_list_prod_right_iff, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : 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:
(List.pairwise_cons.mp co).1 j hj

Premises used: List.pairwise_cons, And.left, Iff.mp
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : 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

Premises used: List.pairwise_cons, And.left, Iff.mp
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : 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:
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
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : 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:
chineseRemainder_lt_mul this (a i) (chineseRemainderOfList a s l co.of_cons)
      (hs i List.mem_cons_self) ?_

Premises used: Nat.chineseRemainderOfList, Nat.chineseRemainder_lt_mul, List.mem_cons_self, Subtype.val, List.Pairwise.of_cons
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : 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
cons : (List.map s l).prod ≠ 0
⊢ (↑(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) ?_

Premises used: Nat.chineseRemainderOfList, Nat.chineseRemainder_lt_mul, List.mem_cons_self, Subtype.val, List.Pairwise.of_cons
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : 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
cons : ∀ x ∈ l, ¬s x = 0
⊢ (List.map s l).prod ≠ 0

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

Premises used: not_exists, ne_eq, List.prod_eq_zero_iff, List.mem_map, not_and
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : 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:
hs j (List.mem_cons_of_mem _ hj)

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : 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)

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
hs : ∀ i ∈ l, s i ≠ 0
nil :
  ∀ (co : List.Pairwise (Coprime on s) []) (hs : ∀ (i : ι), Membership.mem (γ := List ι) [] i → s i ≠ 0),
    (↑(chineseRemainderOfList a s [] co) : ℕ) < (List.map s []).prod
cons :
  ∀ (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
⊢ (↑(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) ?_
    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)

Premises used: List.map_cons, not_exists, Nat.chineseRemainderOfList, ne_eq, List.prod_eq_zero_iff, List.mem_map, List.prod_cons, not_and
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
z : ℕ
co : List.Pairwise (Coprime on s) []
hz : ∀ (i : ι), Membership.mem (γ := List ι) [] i → z ≡ a i [MOD s i]
⊢ z ≡ (↑(chineseRemainderOfList a s [] co) : ℕ) [MOD (List.map s []).prod]

Tactic:
simp [modEq_one]

Premises used: Nat.modEq_one
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l) (hz : ∀ 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]
cons : z ≡ (↑(chineseRemainder ⋯ (a i) (↑(chineseRemainderOfList a s l ⋯) : ℕ)) : ℕ) [MOD s i * (List.map s l).prod]
⊢ z ≡ (↑(chineseRemainderOfList a s (i :: l) co) : ℕ) [MOD (List.map s (i :: l)).prod]

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

Premises used: List.map_cons, Nat.chineseRemainderOfList, List.prod_cons
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l) (hz : ∀ 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]
simp : ∀ a ∈ l, (s i).Coprime (s a)
⊢ (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₂]

Premises used: and_imp, forall_exists_index, List.mem_map, Nat.coprime_list_prod_right_iff, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l) (hz : ∀ 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:
(List.pairwise_cons.mp co).1 j hj

Premises used: List.pairwise_cons, And.left, Iff.mp
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l) (hz : ∀ 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

Premises used: List.pairwise_cons, And.left, Iff.mp
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l) (hz : ∀ 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:
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
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l) (hz : ∀ 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:
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)))

Premises used: Nat.chineseRemainder_modEq_unique, List.mem_cons_of_mem, List.mem_cons_self, List.Pairwise.of_cons
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l) (hz : ∀ 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)))

Premises used: Nat.chineseRemainder_modEq_unique, List.mem_cons_of_mem, List.mem_cons_self, List.Pairwise.of_cons
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
z : ℕ
hz : ∀ i ∈ l, z ≡ a i [MOD s i]
nil :
  ∀ (co : List.Pairwise (Coprime on s) []) (hz : ∀ (i : ι), Membership.mem (γ := List ι) [] i → z ≡ a i [MOD s i]),
    z ≡ (↑(chineseRemainderOfList a s [] co) : ℕ) [MOD (List.map s []).prod]
cons :
  ∀ (i : ι) (l : List ι)
    (ih :
      ∀ (co : List.Pairwise (Coprime on s) l) (hz : ∀ 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]
⊢ z ≡ (↑(chineseRemainderOfList a s l co) : ℕ) [MOD (List.map s l).prod]

Tactic:
induction l with
  | nil => simp [modEq_one]
  | cons i l ih =>
    simp only [List.map_cons, List.prod_cons, chineseRemainderOfList]
    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
    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)))

Premises used: Nat.modEq_one, List.map_cons, Nat.chineseRemainderOfList, List.prod_cons
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
z : { k : ℕ // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
⊢ (List.map s l).prod = (List.map s l').prod

Tactic:
have hlp : (l.map s).prod = (l'.map s).prod := List.Perm.prod_eq (List.Perm.map s hl)
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
z : { k : ℕ // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
hlp : (List.map s l).prod = (List.map s l').prod
rw : (↑z : ℕ) < (List.map s l').prod
⊢ (↑z : ℕ) < (List.map s l).prod

Tactic:
rw [hlp]
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
z : { k : ℕ // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
hlp : (List.map s l).prod = (List.map s l').prod
⊢ ∀ i ∈ l', s i ≠ 0

Tactic:
simpa [List.Perm.mem_iff hl.symm] using hs

Premises used: List.Perm.symm, List.Perm.mem_iff
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
z : { k : ℕ // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
hlp : (List.map s l).prod = (List.map s l').prod
⊢ (↑z : ℕ) < (List.map s l').prod

Tactic:
exact chineseRemainderOfList_lt_prod _ _ _ _
            (by simpa [List.Perm.mem_iff hl.symm] using hs)

Premises used: Nat.chineseRemainderOfList_lt_prod
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
z : { k : ℕ // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
hlp : (List.map s l).prod = (List.map s l').prod
⊢ (↑(chineseRemainderOfList a s l co) : ℕ) = (↑(chineseRemainderOfList a s l' ⋯) : ℕ)

Tactic:
exact (chineseRemainderOfList_modEq_unique a s l co (z := z)
    (fun i hi => z.prop i (hl.symm.mem_iff.mpr hi))).symm.eq_of_lt_of_lt
      (chineseRemainderOfList_lt_prod _ _ _ _ hs)
      (by rw [hlp]
          exact chineseRemainderOfList_lt_prod _ _ _ _
            (by simpa [List.Perm.mem_iff hl.symm] using hs))

Premises used: Iff.mpr, Nat.chineseRemainderOfList_modEq_unique, Nat.ModEq.eq_of_lt_of_lt, Nat.ModEq.symm, Subtype.prop, List.Perm.symm, Nat.chineseRemainderOfList_lt_prod, List.Perm.mem_iff
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
⊢ ∀ i ∈ l, s i ≠ 0

Tactic:
simpa [List.Perm.mem_iff pp] using hs'

Premises used: List.Perm.mem_iff
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
hs : ∀ i ∈ l, s i ≠ 0
co' : Set.Pairwise {x : ι | x ∈ l'} (Coprime on s)
⊢ Set.Pairwise {x : ι | x ∈ l} (Coprime on s)

Tactic:
simpa [List.Perm.mem_iff pp] using co'

Premises used: List.Perm.mem_iff
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
hs : ∀ i ∈ l, s i ≠ 0
co' : Set.Pairwise {x : ι | x ∈ l'} (Coprime on s)
co : Set.Pairwise {x : ι | x ∈ l} (Coprime on s)
lco : List.Pairwise (Coprime on s) l
nod'' : (↑l : Multiset ι).Nodup
hs'' : ∀ i ∈ (↑l : Multiset ι), s i ≠ 0
co'' : Set.Pairwise {x : ι | x ∈ (↑l : Multiset ι)} (Coprime on s)
⊢ (↑(Eq.ndrec (motive := fun (m : Multiset ι) ↦
          m.Nodup →
            (∀ i ∈ m, s i ≠ 0) → Set.Pairwise {x : ι | x ∈ m} (Coprime on s) → { k : ℕ // ∀ i ∈ m, k ≡ a i [MOD s i] })
          (fun (nod : (↑l : Multiset ι).Nodup) (x : ∀ i ∈ (↑l : Multiset ι), s i ≠ 0)
              (co : Set.Pairwise {x : ι | x ∈ (↑l : Multiset ι)} (Coprime on s)) ↦
            chineseRemainderOfList a s l ⋯)
          ⋯ nod'' hs'' co'') :
      ℕ) =
    (↑(chineseRemainderOfList a s l lco) : ℕ)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
hs : ∀ i ∈ l, s i ≠ 0
co' : Set.Pairwise {x : ι | x ∈ l'} (Coprime on s)
co : Set.Pairwise {x : ι | x ∈ l} (Coprime on s)
lco : List.Pairwise (Coprime on s) l
this :
  ∀ {m' : Multiset ι} {e : (↑l : Multiset ι) = m'} {nod'' : m'.Nodup} {hs'' : ∀ i ∈ m', s i ≠ 0}
    {co'' : Set.Pairwise {x : ι | x ∈ m'} (Coprime on s)},
    (↑(Eq.ndrec (motive := fun (m : Multiset ι) ↦
            m.Nodup →
              (∀ i ∈ m, s i ≠ 0) →
                Set.Pairwise {x : ι | x ∈ m} (Coprime on s) → { k : ℕ // ∀ i ∈ m, k ≡ a i [MOD s i] })
            (fun (nod : (↑l : Multiset ι).Nodup) (x : ∀ i ∈ (↑l : Multiset ι), s i ≠ 0)
                (co : Set.Pairwise {x : ι | x ∈ (↑l : Multiset ι)} (Coprime on s)) ↦
              chineseRemainderOfList a s l ⋯)
            e nod'' hs'' co'') :
        ℕ) =
      (↑(chineseRemainderOfList a s l lco) : ℕ)
a₁ :
  (↑(Eq.ndrec (a := ⟦l⟧) (motive := fun (x : Multiset ι) ↦
          x.Nodup →
            (∀ i ∈ x, s i ≠ 0) →
              Set.Pairwise {x_1 : ι | x_1 ∈ x} (Coprime on s) → { k : ℕ // ∀ i ∈ x, k ≡ a i [MOD s i] })
          fun (nod : Multiset.Nodup ⟦l⟧) (x : ∀ i ∈ ⟦l⟧, s i ≠ 0) (co : Set.Pairwise {x : ι | x ∈ ⟦l⟧} (Coprime on s)) ↦
          chineseRemainderOfList a s l ⋯ (b := ⟦l'⟧) ⋯ nod' hs' co') :
      ℕ) =
    (↑(chineseRemainderOfList a s l' ⋯) : ℕ)
⊢ Eq.ndrec (a := ⟦l⟧) (motive := fun (x : Multiset ι) ↦
      x.Nodup →
        (∀ i ∈ x, s i ≠ 0) → Set.Pairwise {x_1 : ι | x_1 ∈ x} (Coprime on s) → { k : ℕ // ∀ i ∈ x, k ≡ a i [MOD s i] })
      fun (nod : Multiset.Nodup ⟦l⟧) (x : ∀ i ∈ ⟦l⟧, s i ≠ 0) (co : Set.Pairwise {x : ι | x ∈ ⟦l⟧} (Coprime on s)) ↦
      chineseRemainderOfList a s l ⋯ (b := ⟦l'⟧) ⋯ nod' hs' co' =
    chineseRemainderOfList a s l' ⋯

Tactic:
ext
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
hs : ∀ i ∈ l, s i ≠ 0
co' : Set.Pairwise {x : ι | x ∈ l'} (Coprime on s)
co : Set.Pairwise {x : ι | x ∈ l} (Coprime on s)
lco : List.Pairwise (Coprime on s) l
this :
  ∀ {m' : Multiset ι} {e : (↑l : Multiset ι) = m'} {nod'' : m'.Nodup} {hs'' : ∀ i ∈ m', s i ≠ 0}
    {co'' : Set.Pairwise {x : ι | x ∈ m'} (Coprime on s)},
    (↑(Eq.ndrec (motive := fun (m : Multiset ι) ↦
            m.Nodup →
              (∀ i ∈ m, s i ≠ 0) →
                Set.Pairwise {x : ι | x ∈ m} (Coprime on s) → { k : ℕ // ∀ i ∈ m, k ≡ a i [MOD s i] })
            (fun (nod : (↑l : Multiset ι).Nodup) (x : ∀ i ∈ (↑l : Multiset ι), s i ≠ 0)
                (co : Set.Pairwise {x : ι | x ∈ (↑l : Multiset ι)} (Coprime on s)) ↦
              chineseRemainderOfList a s l ⋯)
            e nod'' hs'' co'') :
        ℕ) =
      (↑(chineseRemainderOfList a s l lco) : ℕ)
⊢ (↑(Eq.ndrec (a := ⟦l⟧) (motive := fun (x : Multiset ι) ↦
          x.Nodup →
            (∀ i ∈ x, s i ≠ 0) →
              Set.Pairwise {x_1 : ι | x_1 ∈ x} (Coprime on s) → { k : ℕ // ∀ i ∈ x, k ≡ a i [MOD s i] })
          fun (nod : Multiset.Nodup ⟦l⟧) (x : ∀ i ∈ ⟦l⟧, s i ≠ 0) (co : Set.Pairwise {x : ι | x ∈ ⟦l⟧} (Coprime on s)) ↦
          chineseRemainderOfList a s l ⋯ (b := ⟦l'⟧) ⋯ nod' hs' co') :
      ℕ) =
    (↑(chineseRemainderOfList a s l' ⋯) : ℕ)

Tactic:
this.trans <| chineseRemainderOfList_perm a s pp hs lco

Premises used: setOf, Multiset, Multiset.ofList, Eq.trans, Nat.chineseRemainderOfList_perm
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
hs : ∀ i ∈ l, s i ≠ 0
co' : Set.Pairwise {x : ι | x ∈ l'} (Coprime on s)
co : Set.Pairwise {x : ι | x ∈ l} (Coprime on s)
lco : List.Pairwise (Coprime on s) l
this :
  ∀ {m' : Multiset ι} {e : (↑l : Multiset ι) = m'} {nod'' : m'.Nodup} {hs'' : ∀ i ∈ m', s i ≠ 0}
    {co'' : Set.Pairwise {x : ι | x ∈ m'} (Coprime on s)},
    (↑(Eq.ndrec (motive := fun (m : Multiset ι) ↦
            m.Nodup →
              (∀ i ∈ m, s i ≠ 0) →
                Set.Pairwise {x : ι | x ∈ m} (Coprime on s) → { k : ℕ // ∀ i ∈ m, k ≡ a i [MOD s i] })
            (fun (nod : (↑l : Multiset ι).Nodup) (x : ∀ i ∈ (↑l : Multiset ι), s i ≠ 0)
                (co : Set.Pairwise {x : ι | x ∈ (↑l : Multiset ι)} (Coprime on s)) ↦
              chineseRemainderOfList a s l ⋯)
            e nod'' hs'' co'') :
        ℕ) =
      (↑(chineseRemainderOfList a s l lco) : ℕ)
⊢ (↑(Eq.ndrec (a := ⟦l⟧) (motive := fun (x : Multiset ι) ↦
          x.Nodup →
            (∀ i ∈ x, s i ≠ 0) →
              Set.Pairwise {x_1 : ι | x_1 ∈ x} (Coprime on s) → { k : ℕ // ∀ i ∈ x, k ≡ a i [MOD s i] })
          fun (nod : Multiset.Nodup ⟦l⟧) (x : ∀ i ∈ ⟦l⟧, s i ≠ 0) (co : Set.Pairwise {x : ι | x ∈ ⟦l⟧} (Coprime on s)) ↦
          chineseRemainderOfList a s l ⋯ (b := ⟦l'⟧) ⋯ nod' hs' co') :
      ℕ) =
    (↑(chineseRemainderOfList a s l' ⋯) : ℕ)

Tactic:
exact this.trans <| chineseRemainderOfList_perm a s pp hs lco

Premises used: Eq.trans, Nat.chineseRemainderOfList_perm
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
m : Multiset ι
nod : m.Nodup
hs : ∀ i ∈ m, s i ≠ 0
pp : Set.Pairwise {x : ι | x ∈ m} (Coprime on s)
mk :
  ∀ (l : List ι) (nod : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l))
    (hs :
      ∀ (i : ι), Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i → s i ≠ 0)
    (pp :
      Set.Pairwise
        {x : ι | Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) x}
        (Coprime on s)),
    (↑(chineseRemainderOfMultiset a s nod hs pp) : ℕ) <
      (Multiset.map s (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod
⊢ (↑(chineseRemainderOfMultiset a s nod hs pp) : ℕ) < (Multiset.map s m).prod

Tactic:
induction m using Quot.ind with | _ l

Premises used: Quot.ind