-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem absNorm_span_singleton (r : S) :
    absNorm (span ({r} : Set S)) = (Algebra.norm ℤ r).natAbs

Proof state:
case neg
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
this : Fintype (S ⧸ span {r}) := (span {r}).fintypeQuotientOfFreeOfNeBot ⋯
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ (LinearMap.det
        (↑ℤ (Submodule.subtype (span {r})) ∘ₗ
          (↑(b.equiv (basisSpanSingleton b hr)
                (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S)))).toIntLinearMap)).natAbs =
    (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs

Tactic:
congr

Result:
case neg.e_m.h.e_6.h
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
this : Fintype (S ⧸ span {r}) := (span {r}).fintypeQuotientOfFreeOfNeBot ⋯
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ ↑ℤ (Submodule.subtype (span {r})) ∘ₗ
      (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S)))).toIntLinearMap =
    (Algebra.lmul ℤ S) r

Proof state:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
⊢ absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs

Tactic:
by_cases hr : r = 0

Result:
case pos
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : r = 0
⊢ absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs

case neg
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
⊢ absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs

Proof state:
case pos
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : r = 0
⊢ absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs

Tactic:
simp only [hr, Ideal.span_zero, Algebra.coe_lmul_eq_mul, eq_self_iff_true, Ideal.absNorm_bot,
  LinearMap.det_zero'', Set.singleton_zero, _root_.map_zero, Int.natAbs_zero]

Result:
no goals

Proof state:
case neg
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
⊢ absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs

Tactic:
letI := Ideal.fintypeQuotientOfFreeOfNeBot (span {r}) (mt span_singleton_eq_bot.mp hr)

Result:
case neg
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
this : Fintype (S ⧸ span {r}) := (span {r}).fintypeQuotientOfFreeOfNeBot ⋯
⊢ absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs

Proof state:
case neg.e_m.h.e_6.h
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
this : Fintype (S ⧸ span {r}) := (span {r}).fintypeQuotientOfFreeOfNeBot ⋯
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : Module.Free.ChooseBasisIndex ℤ S
⊢ (↑ℤ (Submodule.subtype (span {r})) ∘ₗ
        (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S)))).toIntLinearMap)
      (b i) =
    ((Algebra.lmul ℤ S) r) (b i)

Tactic:
simp

Result:
no goals

Proof state:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
⊢ absNorm (span {r}) = ((Algebra.norm ℤ) r).natAbs

Tactic:
rw [Algebra.norm_apply]

Result:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
⊢ absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs

Proof state:
case neg
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
this : Fintype (S ⧸ span {r}) := (span {r}).fintypeQuotientOfFreeOfNeBot ⋯
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs

Tactic:
rw [← natAbs_det_equiv _ (b.equiv (basisSpanSingleton b hr) (Equiv.refl _))]

Result:
case neg
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
this : Fintype (S ⧸ span {r}) := (span {r}).fintypeQuotientOfFreeOfNeBot ⋯
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ (LinearMap.det
        (↑ℤ (Submodule.subtype (span {r})) ∘ₗ
          (↑(b.equiv (basisSpanSingleton b hr)
                (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S)))).toIntLinearMap)).natAbs =
    (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs

Proof state:
case neg.e_m.h.e_6.h
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
this : Fintype (S ⧸ span {r}) := (span {r}).fintypeQuotientOfFreeOfNeBot ⋯
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ ↑ℤ (Submodule.subtype (span {r})) ∘ₗ
      (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S)))).toIntLinearMap =
    (Algebra.lmul ℤ S) r

Tactic:
refine b.ext fun i => ?_

Result:
case neg.e_m.h.e_6.h
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
this : Fintype (S ⧸ span {r}) := (span {r}).fintypeQuotientOfFreeOfNeBot ⋯
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : Module.Free.ChooseBasisIndex ℤ S
⊢ (↑ℤ (Submodule.subtype (span {r})) ∘ₗ
        (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S)))).toIntLinearMap)
      (b i) =
    ((Algebra.lmul ℤ S) r) (b i)

Proof state:
case neg
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
this : Fintype (S ⧸ span {r}) := (span {r}).fintypeQuotientOfFreeOfNeBot ⋯
⊢ absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs

Tactic:
let b := Module.Free.chooseBasis ℤ S

Result:
case neg
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
this : Fintype (S ⧸ span {r}) := (span {r}).fintypeQuotientOfFreeOfNeBot ⋯
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs