-- Mathlib/LinearAlgebra/FreeModule/Norm.lean
theorem associated_norm_prod_smith [Fintype ι] (b : Basis ι R S) {f : S} (hf : f ≠ 0) :
    Associated (Algebra.norm R f) (∏ i, smithCoeffs b _ (span_singleton_eq_bot.not.2 hf) i)

Proof state:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
⊢ ∀ (x : S),
    ((Matrix.toLin b' b') (Matrix.diagonal (smithCoeffs b (span {f}) ⋯))) x =
      (↑(Algebra.lmul R S).toRingHom f)
        ((LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
          ((b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)) x))

Tactic:
simp_rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.comp_apply, ← LinearMap.ext_iff]

Result:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
⊢ ↑(Matrix.toLin b' b') (Matrix.diagonal (smithCoeffs b (span {f}) ⋯)) =
    ↑(Algebra.lmul R S).toRingHom f ∘ₗ
      ↑(LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)) ∘ₗ
        ↑(b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι))

Proof state:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
⊢ Associated ((Algebra.norm R) f) (LinearMap.det ((Matrix.toLin b' b') (Matrix.diagonal (smithCoeffs b (span {f}) ⋯))))

Tactic:
refine (LinearMap.associated_det_of_eq_comp e _ _ ?_).symm

Result:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
⊢ ∀ (x : S),
    ((Matrix.toLin b' b') (Matrix.diagonal (smithCoeffs b (span {f}) ⋯))) x = (↑(Algebra.lmul R S).toRingHom f) (e x)

Proof state:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ smithCoeffs b (span {f}) ⋯ i • b' i =
    (LinearEquiv.coord S S f hf) ((selfBasis b (span {f}) hI) ((Equiv.refl ι) i)) • f

Tactic:
erw [LinearEquiv.coord_apply_smul]

Result:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ smithCoeffs b (span {f}) ⋯ i • b' i = ↑((selfBasis b (span {f}) hI) ((Equiv.refl ι) i))

Proof state:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ smithCoeffs b (span {f}) ⋯ i • b' i = ↑((selfBasis b (span {f}) hI) ((Equiv.refl ι) i))

Tactic:
rw [Ideal.selfBasis_def]

Result:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ smithCoeffs b (span {f}) ⋯ i • b' i =
    smithCoeffs b (span {f}) hI ((Equiv.refl ι) i) • (ringBasis b (span {f}) hI) ((Equiv.refl ι) i)

Proof state:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
⊢ Associated ((Algebra.norm R) f) (LinearMap.det ((Matrix.toLin b' b') (Matrix.diagonal (smithCoeffs b (span {f}) ⋯))))

Tactic:
let e :=
  (b'.equiv ((span {f}).selfBasis b hI) <| Equiv.refl _).trans
    ((LinearEquiv.coord S S f hf).restrictScalars R)

Result:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
⊢ Associated ((Algebra.norm R) f) (LinearMap.det ((Matrix.toLin b' b') (Matrix.diagonal (smithCoeffs b (span {f}) ⋯))))

Proof state:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
⊢ Associated ((Algebra.norm R) f) (∏ i : ι, smithCoeffs b (span {f}) ⋯ i)

Tactic:
classical
rw [← Matrix.det_diagonal, ← LinearMap.det_toLin b']
let e :=
  (b'.equiv ((span {f}).selfBasis b hI) <| Equiv.refl _).trans
    ((LinearEquiv.coord S S f hf).restrictScalars R)
refine (LinearMap.associated_det_of_eq_comp e _ _ ?_).symm
dsimp only [e, LinearEquiv.trans_apply]
simp_rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.comp_apply, ← LinearMap.ext_iff]
refine b'.ext fun i => ?_
simp_rw [LinearMap.comp_apply, LinearEquiv.coe_toLinearMap, Matrix.toLin_apply, Basis.repr_self,
  Finsupp.single_eq_pi_single, Matrix.diagonal_mulVec_single, Pi.single_apply, ite_smul,
  zero_smul, Finset.sum_ite_eq', mul_one, if_pos (Finset.mem_univ _), b'.equiv_apply]
change _ = f * _
rw [mul_comm, ← smul_eq_mul, LinearEquiv.restrictScalars_apply]
erw [LinearEquiv.coord_apply_smul]
rw [Ideal.selfBasis_def]
rfl

Result:
no goals