-- Mathlib/Algebra/Module/PID.lean
theorem exists_smul_eq_zero_and_mk_eq {z : M} (hz : Module.IsTorsionBy R M (p ^ pOrder hM z))
    {k : ℕ} (f : (R ⧸ R ∙ p ^ k) →ₗ[R] M ⧸ R ∙ z) :
    ∃ x : M, p ^ k • x = 0 ∧ Submodule.Quotient.mk (p := span R {z}) x = f 1

Proof state:
case 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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
this : p ^ k • f1.choose ∈ Submodule.span R {z}
a : R
ha : p ^ k • f1.choose = p ^ k • a • z
⊢ Submodule.Quotient.mk (f1.choose - a • z) = f 1

Tactic:
rw [mk_sub, mk_smul, (Quotient.mk_eq_zero _).mpr <| Submodule.mem_span_singleton_self _,
  smul_zero, sub_zero, f1.choose_spec]

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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
⊢ ∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1

Tactic:
have f1 := mk_surjective (R ∙ z) (f 1)

Result:
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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ ∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1

Proof state:
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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ p ^ k • Submodule.Quotient.mk 1 = 0

Tactic:
rw [← mk_smul, Quotient.mk_eq_zero, Algebra.id.smul_eq_mul, mul_one]

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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ p ^ k ∈ Submodule.span R {p ^ k}

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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
this : p ^ k • f1.choose ∈ Submodule.span R {z}
a : R
ha : p ^ k • f1.choose = p ^ k • a • z
⊢ p ^ k • (f1.choose - a • z) = 0

Tactic:
rw [smul_sub, sub_eq_zero, ha]

Result:
no goals

Proof state:
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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ p ^ k • 1 = 0

Tactic:
change _ • Submodule.Quotient.mk _ = _

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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ p ^ k • Submodule.Quotient.mk 1 = 0

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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ p ^ k • f1.choose ∈ Submodule.span R {z}

Tactic:
rw [← Quotient.mk_eq_zero, mk_smul, f1.choose_spec, ← f.map_smul]

Result:
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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ f (p ^ k • 1) = 0

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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ ∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1

Tactic:
have : p ^ k • f1.choose ∈ R ∙ z := by
  rw [← Quotient.mk_eq_zero, mk_smul, f1.choose_spec, ← f.map_smul]
  convert f.map_zero; change _ • Submodule.Quotient.mk _ = _
  rw [← mk_smul, Quotient.mk_eq_zero, Algebra.id.smul_eq_mul, mul_one]
  exact Submodule.mem_span_singleton_self _

Result:
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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
this : p ^ k • f1.choose ∈ Submodule.span R {z}
⊢ ∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1

Proof state:
case 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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
this : p ^ k • f1.choose ∈ Submodule.span R {z}
a : R
ha : p ^ k • f1.choose = p ^ k • a • z
⊢ ∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1

Tactic:
refine ⟨f1.choose - a • z, by rw [smul_sub, sub_eq_zero, ha], ?_⟩

Result:
case 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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
this : p ^ k • f1.choose ∈ Submodule.span R {z}
a : R
ha : p ^ k • f1.choose = p ^ k • a • z
⊢ Submodule.Quotient.mk (f1.choose - a • z) = f 1