-- Mathlib/Algebra/Module/PID.lean
theorem p_pow_smul_lift {x y : M} {k : ℕ} (hM' : Module.IsTorsionBy R M (p ^ pOrder hM y))
    (h : p ^ k • x ∈ R ∙ y) : ∃ a : R, p ^ k • x = p ^ k • a • y

Proof state:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ Submodule.span R {y}
hk : k ≤ pOrder hM y
f : (R ⧸ Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}) ≃ₗ[R] ↥(Submodule.span R {y}) :=
  (Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
a : R
ha : f (Submodule.Quotient.mk (a * p ^ k)) = ⟨p ^ k • x, h⟩
⊢ p ^ k • x = p ^ k • a • y

Tactic:
rw [smul_smul, mul_comm]

Result:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ Submodule.span R {y}
hk : k ≤ pOrder hM y
f : (R ⧸ Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}) ≃ₗ[R] ↥(Submodule.span R {y}) :=
  (Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
a : R
ha : f (Submodule.Quotient.mk (a * p ^ k)) = ⟨p ^ k • x, h⟩
⊢ p ^ k • x = (a * p ^ k) • y

Proof state:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ Submodule.span R {y}
hk : k ≤ pOrder hM y
f : (R ⧸ Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}) ≃ₗ[R] ↥(Submodule.span R {y}) :=
  (Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
⊢ f.symm (p ^ (pOrder hM y - k) • ⟨p ^ k • x, h⟩) = 0

Tactic:
convert f.symm.map_zero

Result:
case h.e'_2.h.e'_6
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ Submodule.span R {y}
hk : k ≤ pOrder hM y
f : (R ⧸ Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}) ≃ₗ[R] ↥(Submodule.span R {y}) :=
  (Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
⊢ p ^ (pOrder hM y - k) • ⟨p ^ k • x, h⟩ = 0

Proof state:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ Submodule.span R {y}
hk : k ≤ pOrder hM y
f : (R ⧸ Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}) ≃ₗ[R] ↥(Submodule.span R {y}) :=
  (Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
a : R
ha : f (Submodule.Quotient.mk (a • p ^ k)) = ⟨p ^ k • x, h⟩
⊢ p ^ k • x = p ^ k • a • y

Tactic:
dsimp only [smul_eq_mul, LinearEquiv.trans_apply, Submodule.quotEquivOfEq_mk,
  quotTorsionOfEquivSpanSingleton_apply_mk] at ha

Result:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ Submodule.span R {y}
hk : k ≤ pOrder hM y
f : (R ⧸ Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}) ≃ₗ[R] ↥(Submodule.span R {y}) :=
  (Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
a : R
ha : f (Submodule.Quotient.mk (a * p ^ k)) = ⟨p ^ k • x, h⟩
⊢ p ^ k • x = p ^ k • a • y

Proof state:
case pos.refine_2.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ Submodule.span R {y}
hk : k ≤ pOrder hM y
f : (R ⧸ Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}) ≃ₗ[R] ↥(Submodule.span R {y}) :=
  (Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
a : R
ha : a • (Ideal.Quotient.mk (Submodule.span R {p ^ (pOrder hM y - k) * p ^ k})) (p ^ k) = f.symm ⟨p ^ k • x, h⟩
⊢ ∃ a, p ^ k • x = p ^ k • a • y

Tactic:
use a

Result:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ Submodule.span R {y}
hk : k ≤ pOrder hM y
f : (R ⧸ Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}) ≃ₗ[R] ↥(Submodule.span R {y}) :=
  (Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
a : R
ha : a • (Ideal.Quotient.mk (Submodule.span R {p ^ (pOrder hM y - k) * p ^ k})) (p ^ k) = f.symm ⟨p ^ k • x, h⟩
⊢ p ^ k • x = p ^ k • a • y

Proof state:
case ha
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ Submodule.span R {y}
hk : k ≤ pOrder hM y
f : (R ⧸ Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}) ≃ₗ[R] ↥(Submodule.span R {y}) :=
  (Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
⊢ p ^ (pOrder hM y - k) ∈ nonZeroDivisors R

Tactic:
exact mem_nonZeroDivisors_of_ne_zero (pow_ne_zero _ hp.ne_zero)

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ Submodule.span R {y}
⊢ ∃ a, p ^ k • x = p ^ k • a • y

Tactic:
by_cases hk : k ≤ pOrder hM y

Result:
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ Submodule.span R {y}
hk : k ≤ pOrder hM y
⊢ ∃ a, p ^ k • x = p ^ k • a • y

case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ Submodule.span R {y}
hk : ¬k ≤ pOrder hM y
⊢ ∃ a, p ^ k • x = p ^ k • a • y