-- Mathlib/Data/Nat/ChineseRemainder.lean
theorem chineseRemainderOfList_perm {l l' : List ι} (hl : l.Perm l')
    (hs : ∀ i ∈ l, s i ≠ 0) (co : l.Pairwise (Coprime on s)) :
    (chineseRemainderOfList a s l co : ℕ) =
    chineseRemainderOfList a s l' (co.perm hl coprime_comm.mpr)

Proof state:
ι : 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:
rw [hlp]

Result:
ι : 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

Proof state:
ι : 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' ⋯
⊢ ↑(chineseRemainderOfList a s l co) = ↑(chineseRemainderOfList a s l' ⋯)

Tactic:
have hlp : (l.map s).prod = (l'.map s).prod := List.Perm.prod_eq (List.Perm.map s hl)

Result:
ι : 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' ⋯)

Proof state:
ι : 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)

Result:
no goals

Proof state:
ι : 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))

Result:
no goals

Proof state:
ι : 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
⊢ ↑(chineseRemainderOfList a s l co) = ↑(chineseRemainderOfList a s l' ⋯)

Tactic:
let z := chineseRemainderOfList a s l' (co.perm hl coprime_comm.mpr)

Result:
ι : 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' ⋯
⊢ ↑(chineseRemainderOfList a s l co) = ↑(chineseRemainderOfList a s l' ⋯)

Proof state:
ι : 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

Result:
no goals