-- Mathlib/LinearAlgebra/FreeModule/Norm.lean
theorem finrank_quotient_span_eq_natDegree_norm [Algebra F S] [IsScalarTower F F[X] S]
    (b : Basis ι F[X] S) {f : S} (hf : f ≠ 0) :
    Module.finrank F (S ⧸ span ({f} : Set S)) = (Algebra.norm F[X] f).natDegree

Proof state:
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
⊢ Module.finrank F (S ⧸ span {f}) = ((Algebra.norm F[X]) f).natDegree

Tactic:
have h := span_singleton_eq_bot.not.2 hf

Result:
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ Module.finrank F (S ⧸ span {f}) = ((Algebra.norm F[X]) f).natDegree

Proof state:
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
⊢ Module.finrank F (S ⧸ span {f}) = ((Algebra.norm F[X]) f).natDegree

Tactic:
haveI := Fintype.ofFinite ι

Result:
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
⊢ Module.finrank F (S ⧸ span {f}) = ((Algebra.norm F[X]) f).natDegree

Proof state:
case e_f.h
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
i : ι
⊢ Module.finrank F (F[X] ⧸ span {smithCoeffs b (span {f}) h i}) = (smithCoeffs b (span {f}) h i).natDegree

Tactic:
exact (AdjoinRoot.powerBasis <| smithCoeffs_ne_zero b _ h i).finrank

Result:
no goals

Proof state:
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ ∑ i : ι, Module.finrank F (F[X] ⧸ span {smithCoeffs b (span {f}) h i}) =
    ∑ i : ι, (smithCoeffs b (span {f}) h i).natDegree

Tactic:
congr with i

Result:
case e_f.h
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
i : ι
⊢ Module.finrank F (F[X] ⧸ span {smithCoeffs b (span {f}) h i}) = (smithCoeffs b (span {f}) h i).natDegree

Proof state:
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ Module.finrank F (S ⧸ span {f}) = (∏ i : ι, smithCoeffs b (span {f}) ⋯ i).natDegree

Tactic:
rw [natDegree_prod _ _ fun i _ => smithCoeffs_ne_zero b _ h i, finrank_quotient_eq_sum F h b]

Result:
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ ∑ i : ι, Module.finrank F (F[X] ⧸ span {smithCoeffs b (span {f}) h i}) =
    ∑ i : ι, (smithCoeffs b (span {f}) h i).natDegree

Proof state:
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ Module.finrank F (S ⧸ span {f}) = ((Algebra.norm F[X]) f).natDegree

Tactic:
rw [natDegree_eq_of_degree_eq
    (degree_eq_degree_of_associated <| associated_norm_prod_smith b hf)]

Result:
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ Module.finrank F (S ⧸ span {f}) = (∏ i : ι, smithCoeffs b (span {f}) ⋯ i).natDegree