awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x y : Associates R
rw :
  (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
          (HMul.hMul (α := Associates R) (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x))
            (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) y)))) :
      Ideal R) =
    HMul.hMul (α := Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
            (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x))) :
        Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
            (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) y))) :
        Ideal R)
⊢ (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) (x * y)) : Ideal R) =
    HMul.hMul (α := Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) x) : Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) y) : Ideal R)

Tactic:
rw [← quot_out x, ← quot_out y]

Premises used: Associates.quot_out
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x y : Associates R
simp_rw :
  (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
          (Associates.mk
            (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x *
              Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) y))) :
      Ideal R) =
    HMul.hMul (α := Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
            (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x))) :
        Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
            (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) y))) :
        Ideal R)
simp_rw₁ :
  span
      {Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x *
          Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) y} =
    HMul.hMul (α := Ideal R) (span {Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x})
      (span {Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) y})
⊢ (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
          (HMul.hMul (α := Associates R) (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x))
            (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) y)))) :
      Ideal R) =
    HMul.hMul (α := Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
            (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x))) :
        Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
            (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) y))) :
        Ideal R)

Tactic:
simp_rw [mk_mul_mk, associatesEquivIsPrincipal_apply, span_singleton_mul_span_singleton]

Premises used: Ideal.span_singleton_mul_span_singleton, Associates.mk_mul_mk, Ideal.associatesEquivIsPrincipal_apply
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
rw :
  Eq.{u_1 + 1} (α := Ideal R)
    (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) (Associates.mk 0)) :
      Ideal R)
    0
rw₁ : Eq (α := Ideal R) (span {0}) 0
rw₂ : Eq (α := Ideal R) (span {0}) ⊥
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq (α := Ideal R)
    (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) 0) : Ideal R) 0

Tactic:
rw [← mk_zero, associatesEquivIsPrincipal_apply, Submodule.zero_eq_bot, span_singleton_eq_bot]

Premises used: Ideal.span_singleton_eq_bot, Associates.mk_zero, Ideal.associatesEquivIsPrincipal_apply, Submodule.zero_eq_bot
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
rw :
  Eq.{u_1 + 1} (α := Ideal R)
    (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) (Associates.mk 1)) :
      Ideal R)
    1
rw₁ : Eq (α := Ideal R) (span {1}) 1
rw₂ : Eq.{u_1 + 1} (α := Ideal R) ⊤ 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := Ideal R) ⊤ ⊤
⊢ Eq (α := Ideal R)
    (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) 1) : Ideal R) 1

Tactic:
rw [one_eq_mk_one, associatesEquivIsPrincipal_apply, span_singleton_one, one_eq_top]

Premises used: Ideal.one_eq_top, Ideal.span_singleton_one, Associates.one_eq_mk_one, Ideal.associatesEquivIsPrincipal_apply
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x x_1 : Associates R
rw :
  (↑(Equiv.toFun (associatesEquivIsPrincipal R) (x * x_1)) : Ideal R) =
    (↑(Equiv.toFun (associatesEquivIsPrincipal R) x * Equiv.toFun (associatesEquivIsPrincipal R) x_1) : Ideal R)
⊢ Equiv.toFun (associatesEquivIsPrincipal R) (x * x_1) =
    Equiv.toFun (associatesEquivIsPrincipal R) x * Equiv.toFun (associatesEquivIsPrincipal R) x_1

Tactic:
rw [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x x_1 : Associates R
erw :
  HMul.hMul (α := Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) x) : Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) x_1) : Ideal R) =
    (↑(Equiv.toFun (associatesEquivIsPrincipal R) x * Equiv.toFun (associatesEquivIsPrincipal R) x_1) : Ideal R)
⊢ (↑(Equiv.toFun (associatesEquivIsPrincipal R) (x * x_1)) : Ideal R) =
    (↑(Equiv.toFun (associatesEquivIsPrincipal R) x * Equiv.toFun (associatesEquivIsPrincipal R) x_1) : Ideal R)

Tactic:
erw [associatesEquivIsPrincipal_mul]

Premises used: Ideal.associatesEquivIsPrincipal_mul
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x x_1 : Associates R
⊢ HMul.hMul (α := Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) x) : Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) x_1) : Ideal R) =
    (↑(Equiv.toFun (associatesEquivIsPrincipal R) x * Equiv.toFun (associatesEquivIsPrincipal R) x_1) : Ideal R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x : Associates R
rw :
  Membership.mem (γ := Submonoid (Associates R)) (Associates R)⁰
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x)) ↔
    Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
            (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x))) :
        Ideal R)
rw₁ :
  Membership.mem (γ := Submonoid R) R⁰ (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x) ↔
    Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
            (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x))) :
        Ideal R)
rw₂ :
  Membership.mem (γ := Submonoid R) R⁰ (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x) ↔
    Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰
      (span {Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x})
rw₃ rw₄ :
  Membership.mem (γ := Submonoid R) R⁰ (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x) ↔
    Membership.mem (γ := Submonoid R) R⁰ (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x)
⊢ Membership.mem (γ := Submonoid (Associates R)) (Associates R)⁰ x ↔
    Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) x) : Ideal R)

Tactic:
rw [← quot_out x, mk_mem_nonZeroDivisors_associates,
          associatesEquivIsPrincipal_apply, span_singleton_nonZeroDivisors]

Premises used: Ideal.span_singleton_nonZeroDivisors, mk_mem_nonZeroDivisors_associates, Ideal.associatesEquivIsPrincipal_apply, Associates.quot_out
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
⊢ Eq.{max 1 (u_1 + 1)} (α := Ideal R → Prop)
    (fun (I : Ideal R) ↦ IsPrincipal I ∧ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ I) fun (I : Ideal R) ↦
    Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ I ∧ IsPrincipal I

Tactic:
simp_rw [and_comm]

Premises used: and_comm
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x : ↥R⁰
⊢ Eq (α := Ideal R)
    (↑(↑((associatesNonZeroDivisorsEquivIsPrincipal R :
                (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
              (Associates.mk x)) :
          ↥(Ideal R)⁰) :
      Ideal R)
    (span {(↑x : R)})

Tactic:
rfl

Premises used: Set.Mem, setOf, Submodule.span, rfl
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x : Associates ↥R⁰
⊢ Eq (α := Ideal R)
    (↑(↑((associatesNonZeroDivisorsEquivIsPrincipal R :
                (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
              x) :
          ↥(Ideal R)⁰) :
      Ideal R)
    (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
          (↑((MulEquiv.symm associatesNonZeroDivisorsEquiv : (a : Associates ↥R⁰) → ↥(Associates R)⁰) x) :
            Associates R)) :
      Ideal R)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, rfl
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
rw :
  Eq (α := Ideal R)
    (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
          (↑((MulEquiv.symm associatesNonZeroDivisorsEquiv : (a : Associates ↥R⁰) → ↥(Associates R)⁰) 1) :
            Associates R)) :
      Ideal R)
    1
rw₁ :
  Eq (α := Ideal R)
    (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) (↑1 : Associates R)) :
      Ideal R)
    1
rw₂ :
  Eq (α := Ideal R)
    (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) 1) : Ideal R) 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := Ideal R) 1 1
⊢ Eq (α := Ideal R)
    (↑(↑((associatesNonZeroDivisorsEquivIsPrincipal R :
                (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
              1) :
          ↥(Ideal R)⁰) :
      Ideal R)
    1

Tactic:
rw [associatesNonZeroDivisorsEquivIsPrincipal_coe, map_one, OneMemClass.coe_one,
    associatesEquivIsPrincipal_map_one]

Premises used: OneMemClass.coe_one, map_one, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_coe, Ideal.associatesEquivIsPrincipal_map_one
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x x_1 : Associates ↥R⁰
rw :
  HMul.hMul (α := Ideal R)
      (↑(↑((associatesNonZeroDivisorsEquivIsPrincipal R :
                  (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
                x) :
            ↥(Ideal R)⁰) :
        Ideal R)
      (↑(↑((associatesNonZeroDivisorsEquivIsPrincipal R :
                  (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
                x_1) :
            ↥(Ideal R)⁰) :
        Ideal R) =
    (↑(↑(HMul.hMul (α := ↥(isPrincipalNonZeroDivisorsSubmonoid R)) (β := ↥(isPrincipalNonZeroDivisorsSubmonoid R))
              ((associatesNonZeroDivisorsEquivIsPrincipal R :
                    (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
                  x :
                { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
              ((associatesNonZeroDivisorsEquivIsPrincipal R :
                    (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
                  x_1 :
                { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })) :
          ↥(Ideal R)⁰) :
      Ideal R)
⊢ Equiv.toFun (associatesNonZeroDivisorsEquivIsPrincipal R) (x * x_1) =
    Equiv.toFun (associatesNonZeroDivisorsEquivIsPrincipal R) x *
      Equiv.toFun (associatesNonZeroDivisorsEquivIsPrincipal R) x_1

Tactic:
rw [Subtype.ext_iff, Subtype.ext_iff, Equiv.toFun_as_coe,
      associatesNonZeroDivisorsEquivIsPrincipal_mul]

Premises used: Equiv.toFun_as_coe, Subtype.ext_iff, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_mul
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x x_1 : Associates ↥R⁰
⊢ HMul.hMul (α := Ideal R)
      (↑(↑((associatesNonZeroDivisorsEquivIsPrincipal R :
                  (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
                x) :
            ↥(Ideal R)⁰) :
        Ideal R)
      (↑(↑((associatesNonZeroDivisorsEquivIsPrincipal R :
                  (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
                x_1) :
            ↥(Ideal R)⁰) :
        Ideal R) =
    (↑(↑(HMul.hMul (α := ↥(isPrincipalNonZeroDivisorsSubmonoid R)) (β := ↥(isPrincipalNonZeroDivisorsSubmonoid R))
              ((associatesNonZeroDivisorsEquivIsPrincipal R :
                    (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
                  x :
                { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
              ((associatesNonZeroDivisorsEquivIsPrincipal R :
                    (a : Associates ↥R⁰) → { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })
                  x_1 :
                { I : ↥(Ideal R)⁰ // IsPrincipal (↑I : Ideal R) })) :
          ↥(Ideal R)⁰) :
      Ideal R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
hprinc : IsPrincipal I
hI : I ≠ ⊥
x : R := IsPrincipal.generator I
rwa : ¬x = 0
rwa₁ rwa₂ rwa₃ rwa₄ : ¬I = ⊥
⊢ x ≠ 0

Tactic:
rwa [Ne, ← IsPrincipal.eq_bot_iff_generator_eq_zero]

Premises used: Ne, Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
hprinc : IsPrincipal I
hI : I ≠ ⊥
x : R
⊢ (↑((isoBaseOfIsPrincipal hI : (a : R) → ↥I) x) : R) = x * IsPrincipal.generator I

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
hprinc : IsPrincipal I
h : I ≠ ⊥
h₁ :
  Eq (α := R) ((Submodule.subtype I ∘ₗ (↑(isoBaseOfIsPrincipal h) : R →ₗ[R] ↥I) : (a : R) → R) 1 : R)
    ((((LinearMap.mul R R : (a : R) → R →ₗ[R] R) (IsPrincipal.generator I) : R →ₗ[R] R) : (a : R) → R) 1 : R)
⊢ Submodule.subtype I ∘ₗ (↑(isoBaseOfIsPrincipal h) : R →ₗ[R] ↥I) =
    (LinearMap.mul R R : (a : R) → R →ₗ[R] R) (IsPrincipal.generator I)

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
hprinc : IsPrincipal I
h : I ≠ ⊥
⊢ Eq (α := R) ((Submodule.subtype I ∘ₗ (↑(isoBaseOfIsPrincipal h) : R →ₗ[R] ↥I) : (a : R) → R) 1 : R)
    ((((LinearMap.mul R R : (a : R) → R →ₗ[R] R) (IsPrincipal.generator I) : R →ₗ[R] R) : (a : R) → R) 1 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
⊢ I = span {ϖ}

Tactic:
have hI : I = Ideal.span {ϖ} := h.principal.choose_spec
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
⊢ ϖ ^ n ∈ I ^ n

Tactic:
have hϖ : ϖ ^ n ∈ I ^ n := hI ▸ (Ideal.pow_mem_pow (Ideal.mem_span_singleton_self _) n)
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
x : R
simp : x * ϖ ^ n ∈ I ^ n
⊢ Membership.mem (α := R) (I ^ n) ((HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n : (a : R) → R) x : R)

Tactic:
simp only [LinearMap.pow_mulRight, LinearMap.mulRight_apply]

Premises used: LinearMap.pow_mulRight, LinearMap.mulRight_apply
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
x : R
⊢ x * ϖ ^ n ∈ I ^ n

Tactic:
Ideal.mul_mem_left _ _ hϖ

Premises used: Set.Mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
x : R
⊢ x * ϖ ^ n ∈ I ^ n

Tactic:
exact Ideal.mul_mem_left _ _ hϖ

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
h₁ : ∀ (x : R), x ∈ I ↔ x ∈ (f ∘ₗ g).ker
⊢ I = (f ∘ₗ g).ker

Tactic:
ext x
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x : R
h₁ : x ∈ I ↔ x * ϖ ^ n ∈ I * I ^ n
⊢ x ∈ I ↔ x ∈ (f ∘ₗ g).ker

Tactic:
simp only [LinearMap.codRestrict, LinearMap.pow_mulRight, LinearMap.mulRight_apply,
      LinearMap.mem_ker, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
      Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, Submodule.mem_smul_top_iff, smul_eq_mul,
      f, g]

Premises used: LinearMap.coe_mk, LinearMap.pow_mulRight, Submodule.mkQ_apply, LinearMap.mem_ker, LinearMap.coe_comp, Submodule.mem_smul_top_iff, LinearMap.mulRight_apply, LinearMap.codRestrict, Function.comp_apply, smul_eq_mul, AddHom.coe_mk, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x : R
h₁ : x ∈ I → x * ϖ ^ n ∈ I * I ^ n
h₂ : x * ϖ ^ n ∈ I * I ^ n → x ∈ I
⊢ x ∈ I ↔ x * ϖ ^ n ∈ I * I ^ n

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x : R
hx : x ∈ I
⊢ x * ϖ ^ n ∈ I * I ^ n

Tactic:
Submodule.mul_mem_mul hx hϖ

Premises used: Submodule.mul_mem_mul, Set.Mem
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x : R
hx : x ∈ I
⊢ x * ϖ ^ n ∈ I * I ^ n

Tactic:
exact Submodule.mul_mem_mul hx hϖ

Premises used: Submodule.mul_mem_mul
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x : R
hx : x * ϖ ^ n ∈ I * I ^ n
⊢ ϖ ^ (n + 1) ∣ x * ϖ ^ n

Tactic:
rw [← pow_succ', hI, Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hx

Premises used: Ideal.mem_span_singleton, pow_succ', Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x : R
hx : ϖ ^ (n + 1) ∣ x * ϖ ^ n
h₁ : ∀ (y : R) (hy : x * ϖ ^ n = ϖ ^ (n + 1) * y), x ∈ I
⊢ x ∈ I

Tactic:
obtain ⟨y, hy⟩ := hx
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x y : R
hy : x * ϖ ^ n = ϖ ^ (n + 1) * y
h₁ : ∀ (hy : x = ϖ * y), x ∈ I
rw : ∀ (hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)), ϖ ≠ 0
⊢ x ∈ I

Tactic:
rw [mul_comm, pow_succ, mul_assoc, mul_right_inj' (pow_ne_zero _ _)] at hy

Premises used: pow_succ, mul_assoc, pow_ne_zero, mul_comm, mul_right_inj'