-- 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.e'_2.h.e'_6.a
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

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

Result:
no goals

Proof state:
case pos.refine_2
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
this :
  f.symm ⟨p ^ k • x, h⟩ ∈
    Submodule.span R {(Ideal.Quotient.mk (Submodule.span R {p ^ (pOrder hM y - k) * p ^ k})) (p ^ k)}
⊢ ∃ a, p ^ k • x = p ^ k • a • y

Tactic:
rw [Submodule.mem_span_singleton] at this

Result:
case pos.refine_2
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
this : ∃ a, 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

Proof state:
case pos.refine_1
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
⊢ torsionOf R M y = Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}

Tactic:
convert Ideal.torsionOf_eq_span_pow_pOrder hp hM y

Result:
case h.e'_3.h.e'_1.h.e'_4
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
⊢ p ^ (pOrder hM y - k) * p ^ k = p ^ pOrder hM 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 : 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

Tactic:
rw [f.eq_symm_apply, ← Ideal.Quotient.mk_eq_mk, ← Quotient.mk_smul] 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 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

Tactic:
use 0

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
⊢ p ^ k • x = p ^ k • 0 • 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
⊢ p ^ k • x = p ^ k • 0 • y

Tactic:
rw [zero_smul, smul_zero, ← Nat.sub_add_cancel (le_of_not_le hk), pow_add, mul_smul, hM',
  smul_zero]

Result:
no goals

Proof state:
case pos.refine_1
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
⊢ Submodule.span R {p ^ (pOrder hM y - k) * p ^ k} = torsionOf R M y

Tactic:
symm

Result:
case pos.refine_1
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
⊢ torsionOf R M y = Submodule.span R {p ^ (pOrder hM y - k) * p ^ k}

Proof state:
case h.e'_3.h.e'_1.h.e'_4
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
⊢ p ^ (pOrder hM y - k) * p ^ k = p ^ pOrder hM y

Tactic:
rw [← pow_add, Nat.sub_add_cancel hk]

Result:
no goals