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 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 :
  (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
h₁ : p ^ k • x = (a * p ^ k) • y
⊢ p ^ k • x = p ^ k • a • y

Tactic:
rw [smul_smul, mul_comm]

Premises used: smul_smul, mul_comm
-- 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 :
  (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
⊢ p ^ k • x = (a * p ^ k) • y

Tactic:
congr_arg ((↑) : _ → M) ha.symm

Premises used: Quotient.liftOn', AddCon.liftOn, congr_arg, Eq.symm
-- 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 :
  (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
⊢ p ^ k • x = (a * p ^ k) • y

Tactic:
exact congr_arg ((↑) : _ → M) ha.symm

Premises used: congr_arg, Eq.symm
-- 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 : Eq (α := Submodule R R) (torsionOf R M y) (R ∙ p ^ (pOrder hM y - k) * p ^ k)
⊢ Eq (α := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k) (torsionOf R M y)

Tactic:
symm
-- 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
⊢ Eq (α := Ideal R) (torsionOf R M y) (Ideal.span {p ^ pOrder hM y})

Tactic:
Ideal.torsionOf_eq_span_pow_pOrder hp hM y

Premises used: Ideal.torsionOf_eq_span_pow_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
h₁ : p ^ (pOrder hM y - k) * p ^ k = p ^ pOrder hM y
⊢ Eq (α := Submodule R R) (torsionOf R M y) (R ∙ p ^ (pOrder hM y - k) * p ^ k)

Tactic:
convert! Ideal.torsionOf_eq_span_pow_pOrder hp hM y

Premises used: Ideal.torsionOf_eq_span_pow_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
h₁ : p ^ (pOrder hM y - k + k) = p ^ pOrder hM y
h₂ h₃ : p ^ pOrder hM y = p ^ pOrder hM y
⊢ p ^ (pOrder hM y - k) * p ^ k = p ^ pOrder hM y

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

Premises used: pow_add, Nat.sub_add_cancel
-- 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 : pOrder hM y < k
h₁ : p ^ k • x = p ^ k • HSMul.hSMul.{u, v, v} (α := R) 0 y
⊢ ∃ (a : R), p ^ k • x = p ^ k • a • y

Tactic:
use 0
-- 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 : pOrder hM y < k
h₁ : p ^ k • x = HSMul.hSMul (β := M) (p ^ k) 0
h₂ : p ^ k • x = 0
h₃ : p ^ (k - pOrder hM y + pOrder hM y) • x = 0
h₄ : (p ^ (k - pOrder hM y) * p ^ pOrder hM y) • x = 0
h₅ : p ^ (k - pOrder hM y) • p ^ pOrder hM y • x = 0
h₆ : HSMul.hSMul (β := M) (p ^ (k - pOrder hM y)) 0 = 0
h₇ h₈ : Eq.{v + 1} (α := M) 0 0
⊢ p ^ k • x = p ^ k • HSMul.hSMul.{u, v, v} (α := R) 0 y

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

Premises used: pow_add, smul_zero, LT.lt.le, zero_smul, Nat.sub_add_cancel, SemigroupAction.mul_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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f :
  LinearMap.{u, u, u, v} (RingHom.id R) (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k))
    (HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
⊢ ∃ (a : M),
    Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
      ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)

Tactic:
have f1 := mk_surjective (R ∙ z) (f 1)
-- 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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f :
  LinearMap.{u, u, u, v} (RingHom.id R) (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k))
    (HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
f1 :
  ∃ (a : M),
    Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
      ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)
rw :
  Eq.{v + 1} (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
    ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z)
        (HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k)) (p ^ k) 1) :
      HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
    (0 : HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
⊢ Membership.mem (γ := Submodule R M) (R ∙ z)
    (p ^ k •
      f1.choose (p := fun (a : M) ↦
        Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
          ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)))

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

Premises used: Exists.choose_spec, Submodule.Quotient.mk_smul, LinearMap.map_smul, Submodule.Quotient.mk_eq_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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f :
  LinearMap.{u, u, u, v} (RingHom.id R) (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k))
    (HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
f1 :
  ∃ (a : M),
    Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
      ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)
⊢ Eq.{v + 1} (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 0) 0

Tactic:
f.map_zero

Premises used: LinearMap.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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f :
  LinearMap.{u, u, u, v} (RingHom.id R) (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k))
    (HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
f1 :
  ∃ (a : M),
    Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
      ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)
h : HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k)) (p ^ k) 1 = 0
⊢ Eq.{v + 1} (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
    ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z)
        (HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k)) (p ^ k) 1) :
      HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
    (0 : HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))

Tactic:
convert! f.map_zero

Premises used: LinearMap.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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f :
  LinearMap.{u, u, u, v} (RingHom.id R) (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k))
    (HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
f1 :
  ∃ (a : M),
    Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
      ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)
h : Membership.mem (γ := Submodule R R) (R ∙ p ^ k) (p ^ k)
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k)) (p ^ k) (Submodule.Quotient.mk 1) = 0

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

Premises used: Submodule.Quotient.mk_smul, smul_eq_mul, mul_one, Submodule.Quotient.mk_eq_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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f :
  LinearMap.{u, u, u, v} (RingHom.id R) (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k))
    (HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
f1 :
  ∃ (a : M),
    Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
      ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)
⊢ Membership.mem (γ := Submodule R R) (R ∙ p ^ k) (p ^ k)

Tactic:
Submodule.mem_span_singleton_self _

Premises used: Set.Mem, Submodule.mem_span_singleton_self
-- 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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f :
  LinearMap.{u, u, u, v} (RingHom.id R) (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k))
    (HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
f1 :
  ∃ (a : M),
    Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
      ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)
⊢ Membership.mem (γ := Submodule R R) (R ∙ p ^ k) (p ^ k)

Tactic:
exact Submodule.mem_span_singleton_self _

Premises used: Submodule.mem_span_singleton_self
-- 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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f :
  LinearMap.{u, u, u, v} (RingHom.id R) (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k))
    (HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
f1 :
  ∃ (a : M),
    Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
      ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)
⊢ Membership.mem (γ := Submodule R M) (R ∙ z)
    (p ^ k •
      f1.choose (p := fun (a : M) ↦
        Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
          ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 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, smul_eq_mul, mul_one]
    exact Submodule.mem_span_singleton_self _
-- 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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f :
  LinearMap.{u, u, u, v} (RingHom.id R) (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k))
    (HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
f1 :
  ∃ (a : M),
    Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
      ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)
this :
  Membership.mem (γ := Submodule R M) (R ∙ z)
    (p ^ k •
      f1.choose (p := fun (a : M) ↦
        Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
          ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)))
obtain :
  ∀ (a : R)
    (ha :
      p ^ k •
          f1.choose (p := fun (a : M) ↦
            Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
              ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)) =
        p ^ k • a • z),
    ∃ (x : M),
      p ^ k • x = 0 ∧
        Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk x)
          ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)
⊢ ∃ (x : M),
    p ^ k • x = 0 ∧
      Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk x)
        ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)

Tactic:
obtain ⟨a, ha⟩ := p_pow_smul_lift hp hM hz this

Premises used: Module.p_pow_smul_lift
-- 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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f :
  LinearMap.{u, u, u, v} (RingHom.id R) (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k))
    (HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
f1 :
  ∃ (a : M),
    Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
      ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)
this :
  Membership.mem (γ := Submodule R M) (R ∙ z)
    (p ^ k •
      f1.choose (p := fun (a : M) ↦
        Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
          ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)))
a : R
ha :
  p ^ k •
      f1.choose (p := fun (a : M) ↦
        Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
          ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)) =
    p ^ k • a • z
rw :
  p ^ k •
        f1.choose (p := fun (a : M) ↦
          Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
            ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)) -
      p ^ k • a • z =
    0
rw₁ :
  p ^ k •
      f1.choose (p := fun (a : M) ↦
        Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
          ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)) =
    p ^ k • a • z
rw₂ rw₃ : p ^ k • a • z = p ^ k • a • z
⊢ p ^ k •
      (f1.choose (p := fun (a : M) ↦
          Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
            ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)) -
        a • z) =
    0

Tactic:
rw [smul_sub, sub_eq_zero, ha]

Premises used: sub_eq_zero, smul_sub
-- 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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f :
  LinearMap.{u, u, u, v} (RingHom.id R) (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k))
    (HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
f1 :
  ∃ (a : M),
    Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
      ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)
this :
  Membership.mem (γ := Submodule R M) (R ∙ z)
    (p ^ k •
      f1.choose (p := fun (a : M) ↦
        Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
          ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)))
a : R
ha :
  p ^ k •
      f1.choose (p := fun (a : M) ↦
        Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
          ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)) =
    p ^ k • a • z
refine :
  Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
    (Submodule.Quotient.mk
      (f1.choose (p := fun (a : M) ↦
          Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
            ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)) -
        a • z))
    ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)
⊢ ∃ (x : M),
    p ^ k • x = 0 ∧
      Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk x)
        ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)

Tactic:
refine ⟨f1.choose - a • z, by rw [smul_sub, sub_eq_zero, ha], ?_⟩
-- 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)
h' : Module.Finite R M
obtain :
  ∀ (d : ℕ) (s : Fin d → M) (hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤),
    ∃ (d : ℕ) (k : Fin d → ℕ),
      Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
⊢ ∃ (d : ℕ) (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))

Tactic:
obtain ⟨d, s, hs⟩ := @Module.Finite.exists_fin _ _ _ _ _ h'

Premises used: Module.Finite.exists_fin
-- 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)
h' : Module.Finite R M
d : ℕ
s : Fin d → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
h : ∃ (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
⊢ ∃ (d : ℕ) (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))

Tactic:
use d
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin 0 → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
h :
  Nonempty
    (M ≃ₗ[R]
      ⨁ (i : Fin 0),
        HasQuotient.Quotient R (B := Submodule R R)
          (R ∙ HPow.hPow (β := ℕ) p (finZeroElim (α := fun (a : Fin 0) ↦ ℕ) i : ℕ)))
⊢ ∃ (k : Fin 0 → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin 0), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))

Tactic:
use finZeroElim

Premises used: finZeroElim
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin 0 → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
⊢ Eq.{v + 1} (α := Submodule R M) ⊥ ⊤

Tactic:
rw [Set.range_eq_empty, Submodule.span_empty] at hs

Premises used: Submodule.span_empty, Set.range_eq_empty
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin 0 → M
hs : Eq.{v + 1} (α := Submodule R M) ⊥ ⊤
x : M
dsimp : x = 0
⊢ x = default

Tactic:
dsimp
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin 0 → M
hs : Eq.{v + 1} (α := Submodule R M) ⊥ ⊤
x : M
rw : Membership.mem (γ := Submodule R M) ⊤ x
⊢ x = 0

Tactic:
rw [← Submodule.mem_bot R, hs]

Premises used: Submodule.mem_bot
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin 0 → M
hs : Eq.{v + 1} (α := Submodule R M) ⊥ ⊤
x : M
⊢ Membership.mem (γ := Submodule R M) ⊤ x

Tactic:
Submodule.mem_top

Premises used: Submodule.mem_top