awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x : M
prop :
  Eq (α := (n : ℕ) → Prop) (fun (n : ℕ) ↦ p ^ n • x = 0) fun (n : ℕ) ↦
    Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n
this : ∃ (n : ℕ), Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n
⊢ Associates.mk (generator (torsionOf R M x)) =
    HPow.hPow (α := Associates R) (Associates.mk p)
      (Nat.find (p := fun (n : ℕ) ↦
        Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n) ⋯)

Tactic:
Associates.eq_pow_find_of_dvd_irreducible_pow (Associates.irreducible_mk.mpr hp)
      this.choose_spec

Premises used: Iff.mpr, Exists.choose_spec, Associates.irreducible_mk, Associates.eq_pow_find_of_dvd_irreducible_pow
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x : M
prop :
  Eq (α := (n : ℕ) → Prop) (fun (n : ℕ) ↦ p ^ n • x = 0) fun (n : ℕ) ↦
    Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n
this : ∃ (n : ℕ), Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n
⊢ Associates.mk (generator (torsionOf R M x)) =
    HPow.hPow (α := Associates R) (Associates.mk p) (Nat.find (p := fun (n : ℕ) ↦ p ^ n • x = 0) ⋯)

Tactic:
convert!
    Associates.eq_pow_find_of_dvd_irreducible_pow (Associates.irreducible_mk.mpr hp)
      this.choose_spec

Premises used: Iff.mpr, Exists.choose_spec, Associates.irreducible_mk, Associates.eq_pow_find_of_dvd_irreducible_pow
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x : M
dsimp : Eq (α := Ideal R) (torsionOf R M x) (Ideal.span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n • x = 0) ⋯})
dsimp₁ :
  Associates.mk (generator (torsionOf R M x)) =
    HPow.hPow (α := Associates R) (Associates.mk p) (Nat.find (p := fun (n : ℕ) ↦ p ^ n • x = 0) ⋯)
dsimp₂ :
  ∀
    (prop :
      Eq (α := (n : ℕ) → Prop) (fun (n : ℕ) ↦ p ^ n • x = 0) fun (n : ℕ) ↦
        Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n),
    Associates.mk (generator (torsionOf R M x)) =
      HPow.hPow (α := Associates R) (Associates.mk p) (Nat.find (p := fun (n : ℕ) ↦ p ^ n • x = 0) ⋯)
dsimp₃ dsimp₄ :
  ∀
    (prop :
      Eq (α := (n : ℕ) → Prop) (fun (n : ℕ) ↦ p ^ n • x = 0) fun (n : ℕ) ↦
        Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n)
    (this : ∃ (n : ℕ), p ^ n • x = 0),
    Associates.mk (generator (torsionOf R M x)) =
      HPow.hPow (α := Associates R) (Associates.mk p) (Nat.find (p := fun (n : ℕ) ↦ p ^ n • x = 0) ⋯)
dsimp₅ :
  ∀
    (prop :
      Eq (α := (n : ℕ) → Prop) (fun (n : ℕ) ↦ p ^ n • x = 0) fun (n : ℕ) ↦
        Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n)
    (this : ∃ (n : ℕ), Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n),
    Associates.mk (generator (torsionOf R M x)) =
      HPow.hPow (α := Associates R) (Associates.mk p) (Nat.find (p := fun (n : ℕ) ↦ p ^ n • x = 0) ⋯)
⊢ Eq (α := Ideal R) (torsionOf R M x) (Ideal.span {p ^ pOrder hM x})

Tactic:
classical
  dsimp only [pOrder]
  rw [← (torsionOf R M x).span_singleton_generator, Ideal.span_singleton_eq_span_singleton, ←
    Associates.mk_eq_mk_iff_associated, Associates.mk_pow]
  have prop :
    (fun n : ℕ => p ^ n • x = 0) = fun n : ℕ =>
      (Associates.mk <| generator <| torsionOf R M x) ∣ Associates.mk p ^ n := by
    ext n; rw [← Associates.mk_pow, Associates.mk_dvd_mk, ← mem_iff_generator_dvd]; rfl
  have := (isTorsion'_powers_iff p).mp hM x; rw [prop] at this
  convert!
    Associates.eq_pow_find_of_dvd_irreducible_pow (Associates.irreducible_mk.mpr hp)
      this.choose_spec

Premises used: Associates.mk_eq_mk_iff_associated, Ideal.span_singleton_eq_span_singleton, Ideal.span_singleton_generator, Associates.mk_pow, Ideal.torsionOf, Submodule.pOrder
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : Membership.mem (γ := Submodule R M) (R ∙ y) (p ^ k • x)
pos : ∀ (hk : k ≤ pOrder hM y), ∃ (a : R), p ^ k • x = p ^ k • a • y
neg : ∀ (hk : pOrder hM y < k), ∃ (a : R), p ^ k • x = p ^ k • a • y
⊢ ∃ (a : R), p ^ k • x = p ^ k • a • y

Tactic:
by_cases! hk : k ≤ pOrder hM y

Premises used: Submodule.pOrder
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : Membership.mem (γ := Submodule R M) (R ∙ y) (p ^ k • x)
hk : k ≤ pOrder hM y
pos : ∃ (a : R), p ^ k • x = p ^ k • a • y
pos₁ : Eq (α := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k) (torsionOf R M y)
⊢ ∃ (a : R), p ^ k • x = p ^ k • a • y

Tactic:
let f :=
      ((R ∙ p ^ (pOrder hM y - k) * p ^ k).quotEquivOfEq _ ?_).trans
        (quotTorsionOfEquivSpanSingleton R M y)
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : Membership.mem (γ := Submodule R M) (R ∙ y) (p ^ k • x)
hk : k ≤ pOrder hM y
f : LinearEquiv.{u, u, u, v} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) ↥(R ∙ y) :=
  Submodule.quotEquivOfEq (R ∙ p ^ (pOrder hM y - k) * p ^ k) (torsionOf R M y) ⋯ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
rw :
  Eq.{u + 1} (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))
    ((f.symm : (a : ↥(R ∙ y)) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
        (p ^ (pOrder hM y - k) •
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h) :
      HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))
    (0 : HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (p ^ (pOrder hM y - k))
⊢ Membership.mem (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) (γ :=
    Submodule R (HasQuotient.Quotient R (B := Ideal R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)))
    (Submodule.span R
      (singleton (α := HasQuotient.Quotient R (B := Ideal R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))
        ((Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k) : (a : R) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
            (p ^ k) :
          HasQuotient.Quotient R (B := Ideal R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))))
    ((f.symm : (a : ↥(R ∙ y)) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h) :
      HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))

Tactic:
rw [← Quotient.torsionBy_eq_span_singleton, mem_torsionBy_iff, ← f.symm.map_smul]

Premises used: LinearEquiv.symm, Ideal.Quotient.torsionBy_eq_span_singleton, Submodule.mem_torsionBy_iff, LinearEquiv.map_smul
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : Membership.mem (γ := Submodule R M) (R ∙ y) (p ^ k • x)
hk : k ≤ pOrder hM y
f : LinearEquiv.{u, u, u, v} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) ↥(R ∙ y) :=
  Submodule.quotEquivOfEq (R ∙ p ^ (pOrder hM y - k) * p ^ k) (torsionOf R M y) ⋯ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
⊢ Eq.{u + 1} (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))
    ((f.symm : (a : ↥(R ∙ y)) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k) 0) 0

Tactic:
f.symm.map_zero

Premises used: LinearEquiv.symm, LinearEquiv.map_zero
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : Membership.mem (γ := Submodule R M) (R ∙ y) (p ^ k • x)
hk : k ≤ pOrder hM y
f : LinearEquiv.{u, u, u, v} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) ↥(R ∙ y) :=
  Submodule.quotEquivOfEq (R ∙ p ^ (pOrder hM y - k) * p ^ k) (torsionOf R M y) ⋯ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
h₁ :
  p ^ (pOrder hM y - k) • Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h =
    0
⊢ Eq.{u + 1} (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))
    ((f.symm : (a : ↥(R ∙ y)) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
        (p ^ (pOrder hM y - k) •
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h) :
      HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))
    (0 : HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))

Tactic:
convert! f.symm.map_zero

Premises used: LinearEquiv.symm, LinearEquiv.map_zero
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : Membership.mem (γ := Submodule R M) (R ∙ y) (p ^ k • x)
hk : k ≤ pOrder hM y
f : LinearEquiv.{u, u, u, v} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) ↥(R ∙ y) :=
  Submodule.quotEquivOfEq (R ∙ p ^ (pOrder hM y - k) * p ^ k) (torsionOf R M y) ⋯ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
h₁ :
  (↑(p ^ (pOrder hM y - k) •
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h) :
      M) =
    (↑0 : M)
⊢ p ^ (pOrder hM y - k) • Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h =
    0

Tactic:
ext
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : Membership.mem (γ := Submodule R M) (R ∙ y) (p ^ k • x)
hk : k ≤ pOrder hM y
f : LinearEquiv.{u, u, u, v} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) ↥(R ∙ y) :=
  Submodule.quotEquivOfEq (R ∙ p ^ (pOrder hM y - k) * p ^ k) (torsionOf R M y) ⋯ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
h₁ :
  p ^ (pOrder hM y - k) •
      (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h) : M) =
    (↑0 : M)
h₂ : p ^ (pOrder hM y - k) • p ^ k • x = (↑0 : M)
h₃ : p ^ (pOrder hM y - k) • p ^ k • x = 0
h₄ : (p ^ (pOrder hM y - k) * p ^ k) • x = 0
h₅ : p ^ (pOrder hM y - k + k) • x = 0
h₆ : p ^ pOrder hM y • x = 0
h₇ h₈ : Eq.{v + 1} (α := M) 0 0
⊢ (↑(p ^ (pOrder hM y - k) •
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h) :
      M) =
    (↑0 : M)

Tactic:
rw [coe_smul_of_tower, coe_mk, coe_zero, smul_smul, ← pow_add, Nat.sub_add_cancel hk,
            @hM' x]

Premises used: pow_add, Submodule.coe_mk, smul_smul, Submodule.coe_zero, Nat.sub_add_cancel, Submodule.coe_smul_of_tower
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : Membership.mem (γ := Submodule R M) (R ∙ y) (p ^ k • x)
hk : k ≤ pOrder hM y
f : LinearEquiv.{u, u, u, v} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) ↥(R ∙ y) :=
  Submodule.quotEquivOfEq (R ∙ p ^ (pOrder hM y - k) * p ^ k) (torsionOf R M y) ⋯ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (p ^ (pOrder hM y - k))

Tactic:
mem_nonZeroDivisors_of_ne_zero (pow_ne_zero _ hp.ne_zero)

Premises used: pow_ne_zero, mem_nonZeroDivisors_of_ne_zero, Irreducible.ne_zero
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : Membership.mem (γ := Submodule R M) (R ∙ y) (p ^ k • x)
hk : k ≤ pOrder hM y
f : LinearEquiv.{u, u, u, v} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) ↥(R ∙ y) :=
  Submodule.quotEquivOfEq (R ∙ p ^ (pOrder hM y - k) * p ^ k) (torsionOf R M y) ⋯ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (p ^ (pOrder hM y - k))

Tactic:
exact mem_nonZeroDivisors_of_ne_zero (pow_ne_zero _ hp.ne_zero)

Premises used: pow_ne_zero, mem_nonZeroDivisors_of_ne_zero, Irreducible.ne_zero
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : Membership.mem (γ := Submodule R M) (R ∙ y) (p ^ k • x)
hk : k ≤ pOrder hM y
f : LinearEquiv.{u, u, u, v} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) ↥(R ∙ y) :=
  Submodule.quotEquivOfEq (R ∙ p ^ (pOrder hM y - k) * p ^ k) (torsionOf R M y) ⋯ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
⊢ Membership.mem (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) (γ :=
    Submodule R (HasQuotient.Quotient R (B := Ideal R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)))
    (Submodule.span R
      (singleton (α := HasQuotient.Quotient R (B := Ideal R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))
        ((Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k) : (a : R) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
            (p ^ k) :
          HasQuotient.Quotient R (B := Ideal R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))))
    ((f.symm : (a : ↥(R ∙ y)) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h) :
      HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))

Tactic:
have : f.symm ⟨p ^ k • x, h⟩ ∈
          R ∙ Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k) (p ^ k) := by
        rw [← Quotient.torsionBy_eq_span_singleton, mem_torsionBy_iff, ← f.symm.map_smul]
        · convert! f.symm.map_zero; ext
          rw [coe_smul_of_tower, coe_mk, coe_zero, smul_smul, ← pow_add, Nat.sub_add_cancel hk,
            @hM' x]
        · exact mem_nonZeroDivisors_of_ne_zero (pow_ne_zero _ hp.ne_zero)
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : Membership.mem (γ := Submodule R M) (R ∙ y) (p ^ k • x)
hk : k ≤ pOrder hM y
f : LinearEquiv.{u, u, u, v} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) ↥(R ∙ y) :=
  Submodule.quotEquivOfEq (R ∙ p ^ (pOrder hM y - k) * p ^ k) (torsionOf R M y) ⋯ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
this :
  Membership.mem (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) (γ :=
    Submodule R (HasQuotient.Quotient R (B := Ideal R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)))
    (Submodule.span R
      (singleton (α := HasQuotient.Quotient R (B := Ideal R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))
        ((Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k) : (a : R) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
            (p ^ k) :
          HasQuotient.Quotient R (B := Ideal R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))))
    ((f.symm : (a : ↥(R ∙ y)) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h) :
      HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k))
⊢ ∃ (a : R),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) a
        ((Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k) : (a : R) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
            (p ^ k) :
          HasQuotient.Quotient R (B := Ideal R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) =
      (f.symm : (a : ↥(R ∙ y)) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h)

Tactic:
rw [Submodule.mem_span_singleton] at this

Premises used: Submodule.mem_span_singleton
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : Membership.mem (γ := Submodule R M) (R ∙ y) (p ^ k • x)
hk : k ≤ pOrder hM y
f : LinearEquiv.{u, u, u, v} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) ↥(R ∙ y) :=
  Submodule.quotEquivOfEq (R ∙ p ^ (pOrder hM y - k) * p ^ k) (torsionOf R M y) ⋯ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
this :
  ∃ (a : R),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) a
        ((Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k) : (a : R) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
            (p ^ k) :
          HasQuotient.Quotient R (B := Ideal R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) =
      (f.symm : (a : ↥(R ∙ y)) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h)
pos :
  ∀ (a : R)
    (ha :
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) a
          ((Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k) : (a : R) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
              (p ^ k) :
            HasQuotient.Quotient R (B := Ideal R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) =
        (f.symm : (a : ↥(R ∙ y)) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h)),
    ∃ (a : R), p ^ k • x = p ^ k • a • y
⊢ ∃ (a : R), p ^ k • x = p ^ k • a • y

Tactic:
obtain ⟨a, ha⟩ := this
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : Membership.mem (γ := Submodule R M) (R ∙ y) (p ^ k • x)
hk : k ≤ pOrder hM y
f : LinearEquiv.{u, u, u, v} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) ↥(R ∙ y) :=
  Submodule.quotEquivOfEq (R ∙ p ^ (pOrder hM y - k) * p ^ k) (torsionOf R M y) ⋯ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
a : R
ha :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) a
      ((Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k) : (a : R) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
          (p ^ k) :
        HasQuotient.Quotient R (B := Ideal R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) =
    (f.symm : (a : ↥(R ∙ y)) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h)
h₁ : p ^ k • x = p ^ k • a • y
⊢ ∃ (a : R), p ^ k • x = p ^ k • a • y

Tactic:
use a
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : Membership.mem (γ := Submodule R M) (R ∙ y) (p ^ k • x)
hk : k ≤ pOrder hM y
f : LinearEquiv.{u, u, u, v} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) ↥(R ∙ y) :=
  Submodule.quotEquivOfEq (R ∙ p ^ (pOrder hM y - k) * p ^ k) (torsionOf R M y) ⋯ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
a : R
ha :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) a
      ((Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k) : (a : R) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
          (p ^ k) :
        HasQuotient.Quotient R (B := Ideal R) (R ∙ p ^ (pOrder hM y - k) * p ^ k)) =
    (f.symm : (a : ↥(R ∙ y)) → R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k)
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h)
⊢ (f : (a : R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k) → ↥(R ∙ y)) (Submodule.Quotient.mk (a • p ^ k)) =
    Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h

Tactic:
rw [f.eq_symm_apply, ← Ideal.Quotient.mk_eq_mk, ← Quotient.mk_smul] at ha

Premises used: LinearEquiv.eq_symm_apply, Submodule.Quotient.mk_smul, Ideal.Quotient.mk_eq_mk