awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
ι : Type u_4
b : Basis ι ℤ G
i : ι
⊢ Eq.{u_1 + 1} (α := ModN G n)
    (((basis b : Basis.{u_4, 0, u_1} ι (ZMod n) (ModN G n)) : (a : ι) → ModN G n) i : ModN G n)
    ((mkQ n : (a : G) → ModN G n) ((b : (a : ι) → G) i) : ModN G n)
have rw : Eq.{max (u_4 + 1) 1} (α := ι →₀ ZMod n)
  (((Basis.repr (basis b) : LinearEquiv.{0, 0, u_1, u_4} (RingHom.id (ZMod n)) (ModN G n) (ι →₀ ZMod n)) :
        (a : ModN G n) → ι →₀ ZMod n)
      ((mkQ n : (a : G) → ModN G n) ((b : (a : ι) → G) i)) :
    ι →₀ ZMod n)
  (single i 1 : ι →₀ ZMod n)
Tactic: rw [Basis.apply_eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Norm (hypothesis)
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
⊢ Associated.{u_1} (M := R) ((Algebra.norm R : (a : S) → R) f : R) (∏ i : ι, smithCoeffs b (span {f}) ⋯ i : R)
have hI : ¬Eq (α := Ideal S) (span {f}) ⊥
Tactic: have hI := span_singleton_eq_bot.not.2 hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Norm (goal)
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
⊢ Associated.{u_1} (M := R) ((Algebra.norm R : (a : S) → R) f : R) (∏ i : ι, smithCoeffs b (span {f}) ⋯ i : R)
have rw : Associated.{u_1} (M := R) ((Algebra.norm R : (a : S) → R) f : R)
  (((LinearMap.det.{u_2, u_1} (M := S) (A := R) : MonoidHom.{u_2, u_1} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
      ((Matrix.toLin b' b' : (a : Matrix ι ι R) → S →ₗ[R] S) (Matrix.diagonal (smithCoeffs b (span {f}) sorry)) :
        S →ₗ[R] S) :
    R)
Tactic: rw [← Matrix.det_diagonal, ← LinearMap.det_toLin b']
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Norm (goal)
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)
⊢ Associated.{u_1} (M := R) ((Algebra.norm R : (a : S) → R) f : R)
    (((LinearMap.det.{u_2, u_1} (M := S) (A := R) : MonoidHom.{u_2, u_1} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
        ((Matrix.toLin b' b' : (a : Matrix ι ι R) → S →ₗ[R] S) (Matrix.diagonal (smithCoeffs b (span {f}) ⋯)) :
          S →ₗ[R] S) :
      R)
have refine : ∀ (x : S),
  Eq (α := S)
    ((((Matrix.toLin b' b' : (a : Matrix ι ι R) → S →ₗ[R] S) (Matrix.diagonal (smithCoeffs b (span {f}) sorry)) :
            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: refine (LinearMap.associated_det_of_eq_comp e _ _ ?_).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Norm (goal)
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)
⊢ ∀ (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)
have dsimp : ∀ (x : S),
  Eq (α := S)
    ((((Matrix.toLin b' b' : (a : Matrix ι ι R) → S →ₗ[R] S) (Matrix.diagonal (smithCoeffs b (span {f}) sorry)) :
            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: dsimp only [e, LinearEquiv.trans_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Norm (goal)
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)
⊢ ∀ (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)
have 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}) sorry)) :
    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: simp_rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.comp_apply, ← LinearMap.ext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Norm (goal)
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)
have 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}) sorry)) :
            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: refine b'.ext fun i => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Norm (goal)
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 : ι
⊢ 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)
have simp_rw : HSMul.hSMul (β := S) (smithCoeffs b (span {f}) sorry 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: 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Norm (goal)
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) =
    ((((↑(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)
have change : HSMul.hSMul (β := S) (smithCoeffs b (span {f}) sorry 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: change _ = f * _
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Norm (goal)
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) =
    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)
have rw : HSMul.hSMul (β := S) (smithCoeffs b (span {f}) sorry i) ((b' : (a : ι) → S) i : S) =
  (↑((selfBasis b (span {f}) hI : (a : ι) → ↥(span {f})) ((Equiv.refl ι : (a : ι) → ι) i)) : S)
Tactic: rw [mul_comm, ← smul_eq_mul, LinearEquiv.restrictScalars_apply, LinearEquiv.coord_apply_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Norm (goal)
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
⊢ 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)
have 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)
Tactic: haveI := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Norm (hypothesis)
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 ι
⊢ 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)
have h : ¬Eq (α := Ideal S) (span {f}) ⊥
Tactic: have h := span_singleton_eq_bot.not.2 hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Norm (goal)
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}) ⊥
⊢ 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)
have 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}) sorry i)
Tactic: rw [natDegree_eq_of_degree_eq
      (degree_eq_degree_of_associated <| associated_norm_prod_smith b hf)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Norm (goal)
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}) ⊥
⊢ 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)
have 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)
Tactic: rw [natDegree_prod _ _ fun i _ => smithCoeffs_ne_zero b _ h i, finrank_quotient_eq_sum F h b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Norm (goal)
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}) ⊥
⊢ 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)
have 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
Tactic: congr with i
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
⊢ N = ⊥
have rw : ∀ x ∈ N, x = 0
Tactic: rw [Submodule.eq_bot_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
have 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)
Tactic: refine b.ext_elem fun i ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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 : ι
⊢ 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)
have 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)
Tactic: rw [(eq_bot_iff_generator_eq_zero _).mpr hgen] at hϕ
Cleared hypotheses: hϕ, inst_3, hgen, x, hx, i
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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)
    (((b.repr : (a : M) → ι →₀ R) 0 : (a : ι) → R) i : R)
have rw : Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
Tactic: rw [map_zero, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
⊢ N = ⊥
have rw : ∀ x ∈ N, x = 0
Tactic: rw [Submodule.eq_bot_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
have refine : ∀ (i : ι),
  Eq.{u + 1} (α := R)
    ((((b.repr : (a : ↥O) → ι →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x sorry) : ι →₀ R) : (a : ι) → R) i : R)
    (((b.repr : (a : ↥O) → ι →₀ R) 0 : (a : ι) → R) i : R)
Tactic: refine (mk_eq_zero _ _).mp (show (⟨x, hNO hx⟩ : O) = 0 from b.ext_elem fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
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)
have rw : ∀ (hϕ : ∀ (ψ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R), ¬⊥ < ψ.submoduleImage N)
  [inst_4 : (ϕ.submoduleImage N).IsPrincipal] (hgen : generator (ϕ.submoduleImage N) = 0) (x : M) (hx : x ∈ N) (i : ι),
  Eq.{u + 1} (α := R)
    ((((b.repr : (a : ↥O) → ι →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x sorry) : ι →₀ R) : (a : ι) → R) i : R)
    (((b.repr : (a : ↥O) → ι →₀ R) 0 : (a : ι) → R) i : R)
Tactic: rw [(eq_bot_iff_generator_eq_zero _).mpr hgen] at hϕ
Cleared hypotheses: hϕ, inst_3, hgen, x, hx, i
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
inst_3 : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
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)
have rw : Eq.{u + 1} (α := R)
  ((((b.repr : (a : ↥O) → ι →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x sorry) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
Tactic: rw [map_zero, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
inst_3 : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ Eq.{u + 1} (α := R)
    ((((b.repr : (a : ↥O) → ι →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
have refine : Membership.mem (α := R) ((Finsupp.lapply i ∘ₗ (↑b.repr : ↥O →ₗ[R] ι →₀ R)).submoduleImage N)
  ((((b.repr : (a : ↥O) → ι →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x sorry) : ι →₀ R) : (a : ι) → R) i : R)
Tactic: refine (Submodule.eq_bot_iff _).mp (not_bot_lt_iff.1 <| hϕ (Finsupp.lapply i ∘ₗ ↑b.repr)) _ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Submodule.IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ I = Ideal.span {x}
have simp_rw : Membership.mem (γ := Ideal R) (Ideal.span {x}) (generator I) ↔ I ≤ Ideal.span {x}
Tactic: simp_rw [le_antisymm_iff, I.span_singleton_le_iff_mem.2 hx, and_true, ← Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Submodule.IsPrincipal I
x : R
hx : x ∈ I
| I ≤ Ideal.span {x}
have rw : Membership.mem (γ := Submodule R R) (Ideal.span {x}) (generator I)
Tactic: rw [← span_singleton_generator I, Submodule.span_singleton_le_iff_mem]