awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬Eq (α := Ideal S) (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 (S := S) (LinearEquiv.coord S S f hf)
dsimp :
  ∀ (x : S),
    Eq (α := S)
      ((((Matrix.toLin b' b' : (a : Matrix ι ι R) → S →ₗ[R] S) (Matrix.diagonal (smithCoeffs b (span {f}) ⋯)) :
              S →ₗ[R] S) :
            (a : S) → S)
          x :
        S)
      (((((↑(AlgHom.toRingHom (Algebra.lmul R S)) : S →* End R S) : (a : S) → S →ₗ[R] S) f : S →ₗ[R] S) : (a : S) → S)
          (((LinearEquiv.restrictScalars R (S := S) (LinearEquiv.coord S S f hf) : ↥(S ∙ f) ≃ₗ[R] S) :
                (a : ↥(span {f})) → S)
              ((b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) : (a : S) → ↥(span {f})) x : ↥(span {f})) :
            S) :
        S)
⊢ ∀ (x : S),
    Eq (α := S)
      ((((Matrix.toLin b' b' : (a : Matrix ι ι R) → S →ₗ[R] S) (Matrix.diagonal (smithCoeffs b (span {f}) ⋯)) :
              S →ₗ[R] S) :
            (a : S) → S)
          x :
        S)
      (((((↑(AlgHom.toRingHom (Algebra.lmul R S)) : S →* End R S) : (a : S) → S →ₗ[R] S) f : S →ₗ[R] S) : (a : S) → S)
          ((e : (a : S) → S) x : S) :
        S)

Tactic:
dsimp only [e, LinearEquiv.trans_apply]

Premises used: LinearEquiv.trans_apply
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬Eq (α := Ideal S) (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 (S := S) (LinearEquiv.coord S S f hf)
simp_rw :
  Eq.{u_2 + 1} (α := S →ₗ[R] S)
    (((↑(Matrix.toLin b' b') : Matrix ι ι R →ₗ[R] S →ₗ[R] S) : (a : Matrix ι ι R) → S →ₗ[R] S)
        (Matrix.diagonal (smithCoeffs b (span {f}) ⋯)) :
      S →ₗ[R] S)
    (((↑(AlgHom.toRingHom (Algebra.lmul R S)) : S →* End R S) : (a : S) → S →ₗ[R] S) f ∘ₗ
        (↑(LinearEquiv.restrictScalars R (S := S) (LinearEquiv.coord S S f hf)) : ↥(span {f}) →ₗ[R] S) ∘ₗ
          (↑(b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)) : S →ₗ[R] ↥(span {f})) :
      S →ₗ[R] S)
⊢ ∀ (x : S),
    Eq (α := S)
      ((((Matrix.toLin b' b' : (a : Matrix ι ι R) → S →ₗ[R] S) (Matrix.diagonal (smithCoeffs b (span {f}) ⋯)) :
              S →ₗ[R] S) :
            (a : S) → S)
          x :
        S)
      (((((↑(AlgHom.toRingHom (Algebra.lmul R S)) : S →* End R S) : (a : S) → S →ₗ[R] S) f : S →ₗ[R] S) : (a : S) → S)
          (((LinearEquiv.restrictScalars R (S := S) (LinearEquiv.coord S S f hf) : ↥(S ∙ f) ≃ₗ[R] S) :
                (a : ↥(span {f})) → S)
              ((b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) : (a : S) → ↥(span {f})) x : ↥(span {f})) :
            S) :
        S)

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

Premises used: LinearMap.comp_apply, LinearMap.ext_iff, LinearEquiv.coe_toLinearMap
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬Eq (α := Ideal S) (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 (S := S) (LinearEquiv.coord S S f hf)
⊢ Eq.{u_2 + 1} (α := S →ₗ[R] S)
    (((↑(Matrix.toLin b' b') : Matrix ι ι R →ₗ[R] S →ₗ[R] S) : (a : Matrix ι ι R) → S →ₗ[R] S)
        (Matrix.diagonal (smithCoeffs b (span {f}) ⋯)) :
      S →ₗ[R] S)
    (((↑(AlgHom.toRingHom (Algebra.lmul R S)) : S →* End R S) : (a : S) → S →ₗ[R] S) f ∘ₗ
        (↑(LinearEquiv.restrictScalars R (S := S) (LinearEquiv.coord S S f hf)) : ↥(span {f}) →ₗ[R] S) ∘ₗ
          (↑(b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)) : S →ₗ[R] ↥(span {f})) :
      S →ₗ[R] S)

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

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬Eq (α := Ideal S) (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 (S := S) (LinearEquiv.coord S S f hf)
refine :
  ∀ (i : ι),
    Eq (α := S)
      (((((↑(Matrix.toLin b' b') : Matrix ι ι R →ₗ[R] S →ₗ[R] S) : (a : Matrix ι ι R) → S →ₗ[R] S)
                (Matrix.diagonal (smithCoeffs b (span {f}) ⋯)) :
              S →ₗ[R] S) :
            (a : S) → S)
          ((b' : (a : ι) → S) i : S) :
        S)
      ((((↑(AlgHom.toRingHom (Algebra.lmul R S)) : S →* End R S) : (a : S) → S →ₗ[R] S) f ∘ₗ
              (↑(LinearEquiv.restrictScalars R (S := S) (LinearEquiv.coord S S f hf)) : ↥(span {f}) →ₗ[R] S) ∘ₗ
                (↑(b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)) : S →ₗ[R] ↥(span {f})) :
            (a : S) → S)
          ((b' : (a : ι) → S) i : S) :
        S)
⊢ Eq.{u_2 + 1} (α := S →ₗ[R] S)
    (((↑(Matrix.toLin b' b') : Matrix ι ι R →ₗ[R] S →ₗ[R] S) : (a : Matrix ι ι R) → S →ₗ[R] S)
        (Matrix.diagonal (smithCoeffs b (span {f}) ⋯)) :
      S →ₗ[R] S)
    (((↑(AlgHom.toRingHom (Algebra.lmul R S)) : S →* End R S) : (a : S) → S →ₗ[R] S) f ∘ₗ
        (↑(LinearEquiv.restrictScalars R (S := S) (LinearEquiv.coord S S f hf)) : ↥(span {f}) →ₗ[R] S) ∘ₗ
          (↑(b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)) : S →ₗ[R] ↥(span {f})) :
      S →ₗ[R] S)

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

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬Eq (α := Ideal S) (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 (S := S) (LinearEquiv.coord S S f hf)
i : ι
simp_rw :
  HSMul.hSMul (β := S) (smithCoeffs b (span {f}) ⋯ i) ((b' : (a : ι) → S) i : S) =
    ((((↑(AlgHom.toRingHom (Algebra.lmul R S)) : S →* End R S) : (a : S) → S →ₗ[R] S) f : S →ₗ[R] S) : (a : S) → S)
      (((LinearEquiv.restrictScalars R (S := S) (LinearEquiv.coord S S f hf) : ↥(S ∙ f) ≃ₗ[R] S) :
            (a : ↥(span {f})) → S)
          ((selfBasis b (span {f}) hI : (a : ι) → ↥(span {f})) ((Equiv.refl ι : (a : ι) → ι) i) : ↥(span {f})) :
        S)
⊢ Eq (α := S)
    (((((↑(Matrix.toLin b' b') : Matrix ι ι R →ₗ[R] S →ₗ[R] S) : (a : Matrix ι ι R) → S →ₗ[R] S)
              (Matrix.diagonal (smithCoeffs b (span {f}) ⋯)) :
            S →ₗ[R] S) :
          (a : S) → S)
        ((b' : (a : ι) → S) i : S) :
      S)
    ((((↑(AlgHom.toRingHom (Algebra.lmul R S)) : S →* End R S) : (a : S) → S →ₗ[R] S) f ∘ₗ
            (↑(LinearEquiv.restrictScalars R (S := S) (LinearEquiv.coord S S f hf)) : ↥(span {f}) →ₗ[R] S) ∘ₗ
              (↑(b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)) : S →ₗ[R] ↥(span {f})) :
          (a : S) → S)
        ((b' : (a : ι) → S) i : S) :
      S)

Tactic:
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]

Premises used: Finset.mem_univ, Module.Basis.equiv_apply, Finset.sum_ite_eq', Pi.single_apply, LinearMap.comp_apply, if_pos, Matrix.toLin_apply, zero_smul, Matrix.diagonal_mulVec_single, LinearEquiv.coe_toLinearMap, ite_smul, mul_one, Finsupp.single_eq_pi_single, Module.Basis.repr_self
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬Eq (α := Ideal S) (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 (S := S) (LinearEquiv.coord S S f hf)
i : ι
change :
  HSMul.hSMul (β := S) (smithCoeffs b (span {f}) ⋯ i) ((b' : (a : ι) → S) i : S) =
    HMul.hMul (β := S) f
      (((LinearEquiv.restrictScalars R (S := S) (LinearEquiv.coord S S f hf) : ↥(S ∙ f) ≃ₗ[R] S) :
            (a : ↥(span {f})) → S)
          ((selfBasis b (span {f}) hI : (a : ι) → ↥(span {f})) ((Equiv.refl ι : (a : ι) → ι) i) : ↥(span {f})) :
        S)
⊢ HSMul.hSMul (β := S) (smithCoeffs b (span {f}) ⋯ i) ((b' : (a : ι) → S) i : S) =
    ((((↑(AlgHom.toRingHom (Algebra.lmul R S)) : S →* End R S) : (a : S) → S →ₗ[R] S) f : S →ₗ[R] S) : (a : S) → S)
      (((LinearEquiv.restrictScalars R (S := S) (LinearEquiv.coord S S f hf) : ↥(S ∙ f) ≃ₗ[R] S) :
            (a : ↥(span {f})) → S)
          ((selfBasis b (span {f}) hI : (a : ι) → ↥(span {f})) ((Equiv.refl ι : (a : ι) → ι) i) : ↥(span {f})) :
        S)

Tactic:
change _ = f * _
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬Eq (α := Ideal S) (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 (S := S) (LinearEquiv.coord S S f hf)
i : ι
rw :
  HSMul.hSMul (β := S) (smithCoeffs b (span {f}) ⋯ i) ((b' : (a : ι) → S) i : S) =
    (↑((selfBasis b (span {f}) hI : (a : ι) → ↥(span {f})) ((Equiv.refl ι : (a : ι) → ι) i)) : S)
⊢ HSMul.hSMul (β := S) (smithCoeffs b (span {f}) ⋯ i) ((b' : (a : ι) → S) i : S) =
    HMul.hMul (β := S) f
      (((LinearEquiv.restrictScalars R (S := S) (LinearEquiv.coord S S f hf) : ↥(S ∙ f) ≃ₗ[R] S) :
            (a : ↥(span {f})) → S)
          ((selfBasis b (span {f}) hI : (a : ι) → ↥(span {f})) ((Equiv.refl ι : (a : ι) → ι) i) : ↥(span {f})) :
        S)

Tactic:
rw [mul_comm, ← smul_eq_mul, LinearEquiv.restrictScalars_apply, LinearEquiv.coord_apply_smul]

Premises used: LinearEquiv.restrictScalars_apply, mul_comm, LinearEquiv.coord_apply_smul, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬Eq (α := Ideal S) (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 (S := S) (LinearEquiv.coord S S f hf)
i : ι
⊢ HSMul.hSMul (β := S) (smithCoeffs b (span {f}) ⋯ i) ((b' : (a : ι) → S) i : S) =
    (↑((selfBasis b (span {f}) hI : (a : ι) → ↥(span {f})) ((Equiv.refl ι : (a : ι) → ι) i)) : S)

Tactic:
grind [Ideal.selfBasis_def]

Premises used: Ideal.selfBasis_def
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
F : Type u_4
inst_6 : Field F
inst_7 : Algebra.{u_4, u_2} F[X] S
inst_8 : Finite ι
b : Basis.{u_3, u_4, u_2} ι F[X] S
I : Ideal S
hI : I ≠ ⊥
i : ι
⊢ FiniteDimensional F (HasQuotient.Quotient F[X] (B := Ideal F[X]) (span {smithCoeffs b I hI i}))

Tactic:
PowerBasis.finite <| AdjoinRoot.powerBasis <| I.smithCoeffs_ne_zero b hI i

Premises used: PowerBasis.finite, Ideal.smithCoeffs_ne_zero, AdjoinRoot.powerBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
S : Type u_2
ι : Type u_3
inst : CommRing S
inst_1 : IsDomain S
F : Type u_4
inst_2 : Field F
inst_3 : Algebra.{u_4, u_2} F[X] S
inst_4 : Finite ι
inst_5 : Algebra F S
inst_6 : IsScalarTower F F[X] S
b : Basis.{u_3, u_4, u_2} ι F[X] S
f : S
hf : f ≠ 0
haveI :
  ∀ (this : Fintype ι),
    finrank.{u_4, u_2} F (HasQuotient.Quotient S (B := Ideal S) (span {f})) =
      natDegree.{u_4} (R := F) ((Algebra.norm F[X] : (a : S) → F[X]) f)
⊢ finrank.{u_4, u_2} F (HasQuotient.Quotient S (B := Ideal S) (span {f})) =
    natDegree.{u_4} (R := F) ((Algebra.norm F[X] : (a : S) → F[X]) f)

Tactic:
haveI := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
S : Type u_2
ι : Type u_3
inst : CommRing S
inst_1 : IsDomain S
F : Type u_4
inst_2 : Field F
inst_3 : Algebra.{u_4, u_2} F[X] S
inst_4 : Finite ι
inst_5 : Algebra F S
inst_6 : IsScalarTower F F[X] S
b : Basis.{u_3, u_4, u_2} ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
⊢ ¬Eq (α := Ideal S) (span {f}) ⊥

Tactic:
have h := span_singleton_eq_bot.not.2 hf
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
S : Type u_2
ι : Type u_3
inst : CommRing S
inst_1 : IsDomain S
F : Type u_4
inst_2 : Field F
inst_3 : Algebra.{u_4, u_2} F[X] S
inst_4 : Finite ι
inst_5 : Algebra F S
inst_6 : IsScalarTower F F[X] S
b : Basis.{u_3, u_4, u_2} ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬Eq (α := Ideal S) (span {f}) ⊥
rw :
  finrank.{u_4, u_2} F (HasQuotient.Quotient S (B := Ideal S) (span {f})) =
    natDegree.{u_4} (R := F) (∏ i : ι, smithCoeffs b (span {f}) ⋯ i)
⊢ finrank.{u_4, u_2} F (HasQuotient.Quotient S (B := Ideal S) (span {f})) =
    natDegree.{u_4} (R := F) ((Algebra.norm F[X] : (a : S) → F[X]) f)

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

Premises used: Polynomial.degree_eq_degree_of_associated, associated_norm_prod_smith, Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
S : Type u_2
ι : Type u_3
inst : CommRing S
inst_1 : IsDomain S
F : Type u_4
inst_2 : Field F
inst_3 : Algebra.{u_4, u_2} F[X] S
inst_4 : Finite ι
inst_5 : Algebra F S
inst_6 : IsScalarTower F F[X] S
b : Basis.{u_3, u_4, u_2} ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬Eq (α := Ideal S) (span {f}) ⊥
rw :
  Eq (α := ℕ) (∑ i : ι, finrank F (HasQuotient.Quotient F[X] (B := Ideal F[X]) (span {smithCoeffs b (span {f}) h i})))
    (∑ i : ι, (smithCoeffs b (span {f}) h i).natDegree)
⊢ finrank.{u_4, u_2} F (HasQuotient.Quotient S (B := Ideal S) (span {f})) =
    natDegree.{u_4} (R := F) (∏ i : ι, smithCoeffs b (span {f}) ⋯ i)

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

Premises used: Polynomial.natDegree_prod, Ideal.finrank_quotient_eq_sum, Ideal.span, Singleton.singleton, Ideal.smithCoeffs_ne_zero
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
S : Type u_2
ι : Type u_3
inst : CommRing S
inst_1 : IsDomain S
F : Type u_4
inst_2 : Field F
inst_3 : Algebra.{u_4, u_2} F[X] S
inst_4 : Finite ι
inst_5 : Algebra F S
inst_6 : IsScalarTower F F[X] S
b : Basis.{u_3, u_4, u_2} ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬Eq (α := Ideal S) (span {f}) ⊥
e_f :
  ∀ (i : ι),
    finrank F (HasQuotient.Quotient F[X] (B := Ideal F[X]) (span {smithCoeffs b (span {f}) h i})) =
      (smithCoeffs b (span {f}) h i).natDegree
⊢ Eq (α := ℕ) (∑ i : ι, finrank F (HasQuotient.Quotient F[X] (B := Ideal F[X]) (span {smithCoeffs b (span {f}) h i})))
    (∑ i : ι, (smithCoeffs b (span {f}) h i).natDegree)

Tactic:
congr with i
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
S : Type u_2
ι : Type u_3
inst : CommRing S
inst_1 : IsDomain S
F : Type u_4
inst_2 : Field F
inst_3 : Algebra.{u_4, u_2} F[X] S
inst_4 : Finite ι
inst_5 : Algebra F S
inst_6 : IsScalarTower F F[X] S
b : Basis.{u_3, u_4, u_2} ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬Eq (α := Ideal S) (span {f}) ⊥
i : ι
⊢ finrank F (HasQuotient.Quotient F[X] (B := Ideal F[X]) (span {smithCoeffs b (span {f}) h i})) =
    (smithCoeffs b (span {f}) h i).natDegree

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

Premises used: AdjoinRoot, PowerBasis.finrank, WithBot.recBotCoe, Polynomial.natDegree, Ideal.smithCoeffs_ne_zero, WithBot.unbotD, AdjoinRoot.powerBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
S : Type u_2
ι : Type u_3
inst : CommRing S
inst_1 : IsDomain S
F : Type u_4
inst_2 : Field F
inst_3 : Algebra.{u_4, u_2} F[X] S
inst_4 : Finite ι
inst_5 : Algebra F S
inst_6 : IsScalarTower F F[X] S
b : Basis.{u_3, u_4, u_2} ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬Eq (α := Ideal S) (span {f}) ⊥
i : ι
⊢ finrank F (HasQuotient.Quotient F[X] (B := Ideal 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

Premises used: PowerBasis.finrank, Ideal.smithCoeffs_ne_zero, AdjoinRoot.powerBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬Submodule.map ϕ N < Submodule.map ψ N
inst_3 : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
rw : ∀ x ∈ N, x = 0
⊢ N = ⊥

Tactic:
rw [Submodule.eq_bot_iff]

Premises used: Submodule.eq_bot_iff
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬Submodule.map ϕ N < Submodule.map ψ N
inst_3 : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
⊢ x = 0

Tactic:
b.ext_elem fun i ↦ ?_

Premises used: Module.Basis.ext_elem
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬Submodule.map ϕ N < Submodule.map ψ N
inst_3 : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
refine :
  ∀ (i : ι),
    Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
      (((b.repr : (a : M) → ι →₀ R) 0 : (a : ι) → R) i : R)
⊢ x = 0

Tactic:
refine b.ext_elem fun i ↦ ?_

Premises used: Module.Basis.ext_elem
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬Submodule.map ϕ N < Submodule.map ψ N
inst_3 : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
rw :
  ∀ (hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < Submodule.map ψ N) [inst_4 : (Submodule.map ϕ N).IsPrincipal]
    (hgen : generator (Submodule.map ϕ N) = 0) (x : M) (hx : x ∈ N) (i : ι),
    Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
      (((b.repr : (a : M) → ι →₀ R) 0 : (a : ι) → R) i : R)
⊢ Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
    (((b.repr : (a : M) → ι →₀ R) 0 : (a : ι) → R) i : R)

Tactic:
rw [(eq_bot_iff_generator_eq_zero _).mpr hgen] at hϕ

Premises used: Iff.mpr, Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < Submodule.map ψ N
inst_3 : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
rw : Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
⊢ Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
    (((b.repr : (a : M) → ι →₀ R) 0 : (a : ι) → R) i : R)

Tactic:
rw [map_zero, Finsupp.zero_apply]

Premises used: map_zero, Finsupp.zero_apply
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < Submodule.map ψ N
inst_3 : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) (0 : R)

Tactic:
(Submodule.eq_bot_iff _).mp (not_bot_lt_iff.1 <| hϕ (Finsupp.lapply i ∘ₗ ↑b.repr)) _
      ⟨x, hx, rfl⟩

Premises used: Module.Basis.repr, LinearMap.comp, LinearEquiv.toLinearMap, And.intro, Exists.intro, Iff.mp, not_bot_lt_iff, Submodule.eq_bot_iff, Finsupp.lapply, rfl
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < Submodule.map ψ N
inst_3 : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) (0 : R)

Tactic:
exact
    (Submodule.eq_bot_iff _).mp (not_bot_lt_iff.1 <| hϕ (Finsupp.lapply i ∘ₗ ↑b.repr)) _
      ⟨x, hx, rfl⟩

Premises used: Module.Basis.repr, LinearMap.comp, LinearEquiv.toLinearMap, And.intro, Exists.intro, Iff.mp, not_bot_lt_iff, Submodule.eq_bot_iff, Finsupp.lapply, rfl
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis.{u_1, u, v} ι R ↥O
hNO : N ≤ O
ϕ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_3 : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
rw : ∀ x ∈ N, x = 0
⊢ N = ⊥

Tactic:
rw [Submodule.eq_bot_iff]

Premises used: Submodule.eq_bot_iff
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis.{u_1, u, v} ι R ↥O
hNO : N ≤ O
ϕ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_3 : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
⊢ x = 0

Tactic:
(mk_eq_zero _ _).mp (show (⟨x, hNO hx⟩ : O) = 0 from b.ext_elem fun i ↦ ?_)

Premises used: Module.Basis.ext_elem, Iff.mp, Submodule.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis.{u_1, u, v} ι R ↥O
hNO : N ≤ O
ϕ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_3 : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
refine :
  ∀ (i : ι),
    Eq.{u + 1} (α := R)
      ((((b.repr : (a : ↥O) → ι →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯) : ι →₀ R) : (a : ι) → R) i : R)
      (((b.repr : (a : ↥O) → ι →₀ R) 0 : (a : ι) → R) i : R)
⊢ x = 0

Tactic:
refine (mk_eq_zero _ _).mp (show (⟨x, hNO hx⟩ : O) = 0 from b.ext_elem fun i ↦ ?_)

Premises used: Module.Basis.ext_elem, Iff.mp, Submodule.mk_eq_zero