awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
φ₁ : AlgHom.{u_1, u_1, u_2} R p.ResidueField
  (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)) :=
  Ideal.quotientMapₐ (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)
    (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :=
  TensorProduct.lift φ₁
    (IsScalarTower.toAlgHom R S
      (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)))
    ⋯
φ₃ : Localization.AtPrime (R := p.Fiber S) Q →ₐ[R]
  HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :=
  IsLocalization.liftAlgHom (R := p.Fiber S) (M := Q.primeCompl) (f := φ₂) ⋯
this :
  Function.Surjective (α := Localization.AtPrime (R := p.Fiber S) Q) (β :=
    HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
    (⇑φ₃ : (a : Localization.AtPrime Q) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
⊢ QuasiFiniteAt R (S := p.Fiber S) Q

Tactic:
have inst : QuasiFiniteAt R Q := .trans _ p.ResidueField _
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
q : Ideal S
inst_4 : q.IsPrime
Sq : Type u_2 := Localization.AtPrime q
inst_5 : Ideal.IsPrime (Ideal.under R q)
inst_6 : q.LiesOver (Ideal.under R q)
Q : Ideal (Ideal.Fiber (Ideal.under R q) S)
inst_7 : Q.IsPrime
hQ :
  Ideal.comap (F := S →+* TensorProduct R (Ideal.ResidueField (Ideal.under R q)) S)
      (AlgHom.toRingHom TensorProduct.includeRight) Q =
    q
inst_8 : QuasiFiniteAt (Ideal.ResidueField (Ideal.under R q)) (S := Ideal.Fiber (Ideal.under R q) S) Q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R q)) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R q) q
φ₁ : AlgHom.{u_1, u_1, u_2} R (Ideal.ResidueField (Ideal.under R q))
  (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) (Ideal.under R q))) :=
  Ideal.quotientMapₐ (Ideal.map (F := R →+* Sq) (algebraMap R Sq) (Ideal.under R q))
    (IsScalarTower.toAlgHom R (Localization.AtPrime (Ideal.under R q)) Sq) ⋯
φ₂ : Ideal.Fiber (Ideal.under R q) S →ₐ[R]
  HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) (Ideal.under R q)) :=
  TensorProduct.lift φ₁
    (IsScalarTower.toAlgHom R S
      (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) (Ideal.under R q))))
    ⋯
φ₃ : Localization.AtPrime (R := Ideal.Fiber (Ideal.under R q) S) Q →ₐ[R]
  HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) (Ideal.under R q)) :=
  IsLocalization.liftAlgHom (R := Ideal.Fiber (Ideal.under R q) S) (M := Q.primeCompl) (f := φ₂) ⋯
this :
  Function.Surjective (α := Localization.AtPrime (R := Ideal.Fiber (Ideal.under R q) S) Q) (β :=
    HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) (Ideal.under R q)))
    (⇑φ₃ : (a : Localization.AtPrime Q) → Sq ⧸ Ideal.map (algebraMap R Sq) (Ideal.under R q))
inst : QuasiFiniteAt R (S := Ideal.Fiber (Ideal.under R q) S) Q
⊢ QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
        (Ideal.under R q)))

Tactic:
.of_surjective_algHom φ₃ this

Premises used: Algebra.QuasiFinite.of_surjective_algHom
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
r : R
M : Type u_1
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
inst_5 : AddCommGroup M''
inst_6 : Module R M''
e : M' ≃ₗ[R] M''
⊢ r • Submodule.map (↑e : M' →ₗ[R] M'') ⊤ = HSMul.hSMul (β := Submodule R M'') r ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
x : M
⊢ Eq.{u_3 + 1} (α := QuotSMulTop r M')
    ((((map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f :
            LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (QuotSMulTop r M) (QuotSMulTop r M')) :
          (a : QuotSMulTop r M) → QuotSMulTop r M')
        (Submodule.Quotient.mk x) :
      QuotSMulTop r M')
    (Submodule.Quotient.mk ((f : (a : M) → M') x) : M' ⧸ HSMul.hSMul (β := Submodule R M') r ⊤)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
h :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := QuotSMulTop r M')
      (((map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f ∘ₗ
              (HSMul.hSMul (β := Submodule R M) r ⊤).mkQ :
            (a : M) → QuotSMulTop r M')
          x :
        QuotSMulTop r M')
      (((HSMul.hSMul (β := Submodule R M') r ⊤).mkQ ∘ₗ f : (a : M) → QuotSMulTop r M') x : QuotSMulTop r M')
⊢ (map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f ∘ₗ (HSMul.hSMul (β := Submodule R M) r ⊤).mkQ =
    (HSMul.hSMul (β := Submodule R M') r ⊤).mkQ ∘ₗ f

Tactic:
ext
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
x : M
⊢ Eq.{u_3 + 1} (α := QuotSMulTop r M')
    (((map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f ∘ₗ
            (HSMul.hSMul (β := Submodule R M) r ⊤).mkQ :
          (a : M) → QuotSMulTop r M')
        x :
      QuotSMulTop r M')
    (((HSMul.hSMul (β := Submodule R M') r ⊤).mkQ ∘ₗ f : (a : M) → QuotSMulTop r M') x : QuotSMulTop r M')

Tactic:
rfl
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
r : R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq.{u_1 + 1} (α := QuotSMulTop r M →ₗ[R] QuotSMulTop r M)
    ((map r : (a : M →ₗ[R] M) → QuotSMulTop r M →ₗ[R] QuotSMulTop r M) LinearMap.id :
      QuotSMulTop r M →ₗ[R] QuotSMulTop r M)
    (LinearMap.id : QuotSMulTop r M →ₗ[R] QuotSMulTop r M)

Tactic:
DFunLike.ext _ _ <| (mkQ_surjective _).forall.mpr fun _ => rfl

Premises used: Iff.mpr, Function.Surjective.forall, DFunLike.ext, Submodule.mkQ_surjective, rfl
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
r : R
M : Type u_1
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
inst_5 : AddCommGroup M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
f : M →ₗ[R] M'
⊢ Eq (α := LinearMap.{u_2, u_2, u_1, u_4} (RingHom.id R) (QuotSMulTop r M) (QuotSMulTop r M''))
    ((map r : (a : M →ₗ[R] M'') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M'') (g ∘ₗ f) :
      LinearMap.{u_2, u_2, u_1, u_4} (RingHom.id R) (QuotSMulTop r M) (QuotSMulTop r M''))
    ((map r : (a : M' →ₗ[R] M'') → QuotSMulTop r M' →ₗ[R] QuotSMulTop r M'') g ∘ₗ
        (map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f :
      LinearMap.{u_2, u_2, u_1, u_4} (RingHom.id R) (QuotSMulTop r M) (QuotSMulTop r M''))

Tactic:
DFunLike.ext _ _ <| (mkQ_surjective _).forall.mpr fun _ => rfl

Premises used: Iff.mpr, Function.Surjective.forall, DFunLike.ext, Submodule.mkQ_surjective, rfl
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
x : M
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}) ⊗[R] M')
    ((equivQuotTensor r M' : (a : QuotSMulTop r M') → (R ⧸ Ideal.span {r}) ⊗[R] M')
        ((((map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f :
              LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (QuotSMulTop r M) (QuotSMulTop r M')) :
            (a : QuotSMulTop r M) → QuotSMulTop r M')
          (Submodule.Quotient.mk x)) :
      HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}) ⊗[R] M')
    ((LinearMap.lTensor (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) f :
          (a : (R ⧸ Ideal.span {r}) ⊗[R] M) → (R ⧸ Ideal.span {r}) ⊗[R] M')
        ((equivQuotTensor r M : (a : QuotSMulTop r M) → (R ⧸ Ideal.span {r}) ⊗[R] M) (Submodule.Quotient.mk x)) :
      HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}) ⊗[R] M')

Tactic:
(LinearMap.lTensor_tmul (R ⧸ Ideal.span {r}) f 1 x).symm

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, List.foldl, HasQuotient.Quotient, Ideal.span, TensorProduct.tmul, Singleton.singleton, OfNat.ofNat, Eq.symm, AddCon.toQuotient, FreeAddMonoid.sumAux, LinearMap.lTensor_tmul
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
⊢ (↑(equivQuotTensor r M') : QuotSMulTop r M' →ₗ[R] (R ⧸ Ideal.span {r}) ⊗[R] M') ∘ₗ
      (map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f =
    LinearMap.lTensor (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) f ∘ₗ
      (↑(equivQuotTensor r M) : QuotSMulTop r M →ₗ[R] (R ⧸ Ideal.span {r}) ⊗[R] M)

Tactic:
quot_hom_ext _ _ _ (equivQuotTensor_naturality_mk r f)

Premises used: QuotSMulTop.equivQuotTensor_naturality_mk, Submodule.quot_hom_ext
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
x : M
⊢ Eq (α := M' ⊗[R] HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
    ((equivTensorQuot r M' : (a : QuotSMulTop r M') → M' ⊗[R] (R ⧸ Ideal.span {r}))
        ((((map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f :
              LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (QuotSMulTop r M) (QuotSMulTop r M')) :
            (a : QuotSMulTop r M) → QuotSMulTop r M')
          (Submodule.Quotient.mk x)) :
      M' ⊗[R] HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
    ((LinearMap.rTensor (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) f :
          (a : M ⊗[R] (R ⧸ Ideal.span {r})) → M' ⊗[R] (R ⧸ Ideal.span {r}))
        ((equivTensorQuot r M : (a : QuotSMulTop r M) → M ⊗[R] (R ⧸ Ideal.span {r})) (Submodule.Quotient.mk x)) :
      M' ⊗[R] HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))

Tactic:
(LinearMap.rTensor_tmul (R ⧸ Ideal.span {r}) f 1 x).symm

Premises used: Quotient.liftOn', LinearMap.rTensor_tmul, AddCon.liftOn, Submodule.Quotient.mk, List.foldl, HasQuotient.Quotient, Ideal.span, TensorProduct.tmul, Singleton.singleton, OfNat.ofNat, Eq.symm, AddCon.toQuotient, FreeAddMonoid.sumAux
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
⊢ (↑(equivTensorQuot r M') : QuotSMulTop r M' →ₗ[R] M' ⊗[R] (R ⧸ Ideal.span {r})) ∘ₗ
      (map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f =
    LinearMap.rTensor (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) f ∘ₗ
      (↑(equivTensorQuot r M) : QuotSMulTop r M →ₗ[R] M ⊗[R] (R ⧸ Ideal.span {r}))

Tactic:
quot_hom_ext _ _ _ (equivTensorQuot_naturality_mk r f)

Premises used: QuotSMulTop.equivTensorQuot_naturality_mk, Submodule.quot_hom_ext
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
H₁ :
  Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M' ⧸ HSMul.hSMul (β := Submodule R M') r ⊤)
    (comp (β := M') (⇑(HSMul.hSMul (β := Submodule R M') r ⊤).mkQ : (a : M') → M' ⧸ r • ⊤) (⇑f : (a : M) → M'))
rwa :
  Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := QuotSMulTop r M')
    (⇑((map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f ∘ₗ
          (HSMul.hSMul (β := Submodule R M) r ⊤).mkQ) :
      (a : M) → QuotSMulTop r M')
rwa₁ :
  Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := QuotSMulTop r M')
    (⇑((HSMul.hSMul (β := Submodule R M') r ⊤).mkQ ∘ₗ f) : (a : M) → QuotSMulTop r M')
rwa₂ rwa₃ rwa₄ rwa₅ :
  Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := QuotSMulTop r M')
    (comp (β := M') (⇑(HSMul.hSMul (β := Submodule R M') r ⊤).mkQ : (a : M') → M' ⧸ r • ⊤) (⇑f : (a : M) → M'))
⊢ Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := QuotSMulTop r M')
    (comp (β := QuotSMulTop r M)
      (⇑((map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f :
            LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (QuotSMulTop r M) (QuotSMulTop r M')) :
        (a : QuotSMulTop r M) → QuotSMulTop r M')
      (⇑(HSMul.hSMul (β := Submodule R M) r ⊤).mkQ : (a : M) → M ⧸ r • ⊤))

Tactic:
rwa [← LinearMap.coe_comp, map_comp_mkQ, LinearMap.coe_comp]

Premises used: QuotSMulTop.map_comp_mkQ, LinearMap.coe_comp
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
r : R
M : Type u_1
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
inst_5 : AddCommGroup M''
inst_6 : Module R M''
f : M →ₗ[R] M'
g : M' →ₗ[R] M''
hfg : Exact.{u_1, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
hg : Surjective.{u_3 + 1, u_4 + 1} (α := M') (β := M'') (⇑g : (a : M') → M'')
⊢ Exact.{u_1, u_3, u_4} (M := QuotSMulTop r M) (N := QuotSMulTop r M') (P := QuotSMulTop r M'')
    (⇑((map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f :
          LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (QuotSMulTop r M) (QuotSMulTop r M')) :
      (a : QuotSMulTop r M) → QuotSMulTop r M')
    (⇑((map r : (a : M' →ₗ[R] M'') → QuotSMulTop r M' →ₗ[R] QuotSMulTop r M'') g :
          LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) (QuotSMulTop r M') (QuotSMulTop r M'')) :
      (a : QuotSMulTop r M') → QuotSMulTop r M'')

Tactic:
(Exact.iff_of_ladder_linearEquiv (equivQuotTensor_naturality r f).symm
                             (equivQuotTensor_naturality r g).symm).mp
    (lTensor_exact (R ⧸ Ideal.span {r}) hfg hg)

Premises used: Function.Exact.iff_of_ladder_linearEquiv, lTensor_exact, QuotSMulTop.equivQuotTensor_naturality, HasQuotient.Quotient, Iff.mp, Ideal.span, Singleton.singleton, Eq.symm
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_3
inst : CommRing R
r : R
M : Type u_1
M' : Type ?u.313736
M'' : Type ?u.314002
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
inst_5 : AddCommGroup M''
inst_6 : Module R M''
S : Type u_2
inst_7 : CommRing S
inst_8 : Algebra R S
⊢ HSMul.hSMul (α := S) (β := Submodule S (S ⊗[R] M)) ((algebraMap R S : (a : R) → S) r : S) ⊤ =
    HSMul.hSMul (α := Ideal S) (β := Submodule S (S ⊗[R] M))
      (Ideal.map (R := R) (F := R →+* S) (algebraMap R S) (Ideal.span {r})) ⊤

Tactic:
simp [Ideal.map_span, ideal_span_singleton_smul]

Premises used: Submodule.ideal_span_singleton_smul, Ideal.map_span
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
x : R
⊢ Membership.mem (γ := Ideal R) (Module.annihilator.{u_2, u_1} R (QuotSMulTop x M)) x

Tactic:
Module.mem_annihilator.mpr (fun m ↦ ?_)

Premises used: Iff.mpr, Module.mem_annihilator
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
x : R
refine : ∀ (m : QuotSMulTop x M), x • m = 0
⊢ Membership.mem (γ := Ideal R) (Module.annihilator.{u_2, u_1} R (QuotSMulTop x M)) x

Tactic:
refine Module.mem_annihilator.mpr (fun m ↦ ?_)

Premises used: Iff.mpr, Module.mem_annihilator
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
x : R
m : QuotSMulTop x M
rcases : ∀ (m' : M) (hm' : Submodule.Quotient.mk m' = m), x • m = 0
⊢ x • m = 0

Tactic:
rcases Submodule.Quotient.mk_surjective _ m with ⟨m', hm'⟩

Premises used: Submodule.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.QuotSMulTop
Goal:
R : Type u_2
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
x : R
m : QuotSMulTop x M
m' : M
hm' : Submodule.Quotient.mk m' = m
⊢ x • m = 0

Tactic:
simpa [← hm', ← Submodule.Quotient.mk_smul] using Submodule.smul_mem_pointwise_smul m' x ⊤ trivial

Premises used: trivial, Submodule.smul_mem_pointwise_smul, Submodule.Quotient.mk_smul, Top.top
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
⊢ a ∈ primeFactors b ↔ a ∈ normalizedFactors b

Tactic:
simp only [primeFactors, Multiset.mem_toFinset]

Premises used: UniqueFactorizationMonoid.primeFactors, Multiset.mem_toFinset
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
h : Associated a b
rw rw₁ : (normalizedFactors b).toFinset = (normalizedFactors b).toFinset
⊢ (normalizedFactors a).toFinset = (normalizedFactors b).toFinset

Tactic:
rw [h.normalizedFactors_eq]

Premises used: Associated.normalizedFactors_eq
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
⊢ Eq.{u_1 + 1} (α := Finset M) (primeFactors 0) ∅

Tactic:
simp [primeFactors]

Premises used: UniqueFactorizationMonoid.primeFactors
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
⊢ Eq.{u_1 + 1} (α := Finset M) (primeFactors 1) ∅

Tactic:
simp [primeFactors]

Premises used: UniqueFactorizationMonoid.primeFactors
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
inl : (↑(primeFactors 0) : Set M).Pairwise IsRelPrime
inr : ∀ (ha₀ : a ≠ 0), (↑(primeFactors a) : Set M).Pairwise IsRelPrime
⊢ (↑(primeFactors a) : Set M).Pairwise IsRelPrime

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
⊢ (↑(primeFactors 0) : Set M).Pairwise IsRelPrime

Tactic:
simp
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x : M
hx : x ∈ (↑(primeFactors a) : Set M)
y : M
hy : y ∈ (↑(primeFactors a) : Set M)
hxy : x ≠ y
⊢ Irreducible x ∧ (normalize : (a : M) → M) x = x ∧ x ∣ a

Tactic:
simp only [Finset.mem_coe, mem_primeFactors, mem_normalizedFactors_iff' ha₀] at hx hy

Premises used: UniqueFactorizationMonoid.mem_primeFactors, UniqueFactorizationMonoid.mem_normalizedFactors_iff', Finset.mem_coe
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x : M
hx : x ∈ (↑(primeFactors a) : Set M)
y : M
hy : y ∈ (↑(primeFactors a) : Set M)
hxy : x ≠ y
hx₁ : Irreducible x ∧ (normalize : (a : M) → M) x = x ∧ x ∣ a
⊢ Irreducible y ∧ (normalize : (a : M) → M) y = y ∧ y ∣ a

Tactic:
simp only [Finset.mem_coe, mem_primeFactors, mem_normalizedFactors_iff' ha₀] at hx hy

Premises used: UniqueFactorizationMonoid.mem_primeFactors, UniqueFactorizationMonoid.mem_normalizedFactors_iff', Finset.mem_coe
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x y : M
hxy : x ≠ y
hx : Irreducible x ∧ (normalize : (a : M) → M) x = x ∧ x ∣ a
hy : Irreducible y ∧ (normalize : (a : M) → M) y = y ∧ y ∣ a
inr : ¬x ∣ y
⊢ IsRelPrime x y

Tactic:
rw [hx.1.isRelPrime_iff_not_dvd]

Premises used: Irreducible.isRelPrime_iff_not_dvd, And.left
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x y : M
hxy : x ≠ y
hx : Irreducible x ∧ (normalize : (a : M) → M) x = x ∧ x ∣ a
hy : Irreducible y ∧ (normalize : (a : M) → M) y = y ∧ y ∣ a
inr : ∀ (hxy : x ∣ y), x = y
⊢ ¬x ∣ y

Tactic:
contrapose hxy
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x y : M
hx : Irreducible x ∧ (normalize : (a : M) → M) x = x ∧ x ∣ a
hy : Irreducible y ∧ (normalize : (a : M) → M) y = y ∧ y ∣ a
hxy : x ∣ y
⊢ Associated x y

Tactic:
have : Associated x y := hx.1.associated_of_dvd hy.1 hxy
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x y : M
hx : Irreducible x ∧ (normalize : (a : M) → M) x = x ∧ x ∣ a
hy : Irreducible y ∧ (normalize : (a : M) → M) y = y ∧ y ∣ a
hxy : x ∣ y
this : Associated x y
⊢ x = y

Tactic:
this.eq_of_normalized hx.2.1 hy.2.1

Premises used: Associated.eq_of_normalized, And.right, And.left
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x y : M
hx : Irreducible x ∧ (normalize : (a : M) → M) x = x ∧ x ∣ a
hy : Irreducible y ∧ (normalize : (a : M) → M) y = y ∧ y ∣ a
hxy : x ∣ y
this : Associated x y
⊢ x = y

Tactic:
exact this.eq_of_normalized hx.2.1 hy.2.1

Premises used: Associated.eq_of_normalized, And.right, And.left
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
n : ℕ
hn : n ≠ 0
simp_rw : (normalizedFactors (a ^ n)).toFinset = (normalizedFactors a).toFinset
simp_rw₁ : (n • normalizedFactors a).toFinset = (normalizedFactors a).toFinset
⊢ primeFactors (a ^ n) = primeFactors a

Tactic:
simp_rw [primeFactors, normalizedFactors_pow, Multiset.toFinset_nsmul _ _ hn]

Premises used: Multiset.toFinset_nsmul, UniqueFactorizationMonoid.primeFactors, UniqueFactorizationMonoid.normalizedFactors_pow
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
n : ℕ
inst_3 : NeZero n
⊢ primeFactors (a ^ n) = primeFactors a

Tactic:
primeFactors_pow a NeZero.out

Premises used: UniqueFactorizationMonoid.primeFactors_pow, NeZero.out
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
inl : ∀ (ha : IsRadical.{u_1} (R := M) 0), Multiset.Nodup.{u_1} (α := M) (normalizedFactors 0)
inr : ∀ (ha₀ : a ≠ 0), (normalizedFactors a).Nodup
⊢ (normalizedFactors a).Nodup

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl