awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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)
        (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))
have 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
Tactic: convert! f.symm.map_zero
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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
⊢ p ^ (pOrder hM y - k) • Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ y) x) (p ^ k • x) h =
    0
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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
⊢ (↑(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)
have 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)
Tactic: rw [coe_smul_of_tower, coe_mk, coe_zero, smul_smul, ← pow_add, Nat.sub_add_cancel hk,
            @hM' x]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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) :
      M) =
    (↑0 : M)
have h₂ : p ^ (pOrder hM y - k) • p ^ k • x = (↑0 : M)
Tactic: rw [coe_smul_of_tower, coe_mk, coe_zero, smul_smul, ← pow_add, Nat.sub_add_cancel hk,
            @hM' x]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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)
⊢ (↑(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)
have h₃ : p ^ (pOrder hM y - k) • p ^ k • x = 0
Tactic: rw [coe_smul_of_tower, coe_mk, coe_zero, smul_smul, ← pow_add, Nat.sub_add_cancel hk,
            @hM' x]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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
⊢ (↑(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)
have h₄ : (p ^ (pOrder hM y - k) * p ^ k) • x = 0
Tactic: rw [coe_smul_of_tower, coe_mk, coe_zero, smul_smul, ← pow_add, Nat.sub_add_cancel hk,
            @hM' x]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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
⊢ (↑(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)
have h₅ : p ^ (pOrder hM y - k + k) • x = 0
Tactic: rw [coe_smul_of_tower, coe_mk, coe_zero, smul_smul, ← pow_add, Nat.sub_add_cancel hk,
            @hM' x]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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
⊢ (↑(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)
have h₆ : p ^ pOrder hM y • x = 0
Tactic: rw [coe_smul_of_tower, coe_mk, coe_zero, smul_smul, ← pow_add, Nat.sub_add_cancel hk,
            @hM' x]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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
⊢ (↑(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)
have h₇ : Eq.{v + 1} (α := M) 0 0
Tactic: rw [coe_smul_of_tower, coe_mk, coe_zero, smul_smul, ← pow_add, Nat.sub_add_cancel hk,
            @hM' x]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (hypothesis)
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), p ^ k • x = p ^ k • a • y
have 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))
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)
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (hypothesis)
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), p ^ k • x = p ^ k • a • y
have 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)
Tactic: rw [Submodule.mem_span_singleton] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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)
⊢ ∃ (a : R), p ^ k • x = p ^ k • a • y
have 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
Tactic: obtain ⟨a, ha⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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)
⊢ ∃ (a : R), p ^ k • x = p ^ k • a • y
have h₁ : p ^ k • x = p ^ k • a • y
Tactic: use a
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (hypothesis)
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)
⊢ p ^ k • x = p ^ k • a • y
have 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
Tactic: rw [f.eq_symm_apply, ← Ideal.Quotient.mk_eq_mk, ← Quotient.mk_smul] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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 = p ^ k • a • y
have h₁ : p ^ k • x = (a * p ^ k) • y
Tactic: rw [smul_smul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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 (α := Submodule R R) (R ∙ p ^ (pOrder hM y - k) * p ^ k) (torsionOf R M y)
have pos : Eq (α := Submodule R R) (torsionOf R M y) (R ∙ p ^ (pOrder hM y - k) * p ^ k)
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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 (α := Submodule R R) (torsionOf R M y) (R ∙ p ^ (pOrder hM y - k) * p ^ k)
have h₁ : p ^ (pOrder hM y - k) * p ^ k = p ^ pOrder hM y
Tactic: convert! Ideal.torsionOf_eq_span_pow_pOrder hp hM y
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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
⊢ p ^ (pOrder hM y - k) * p ^ k = p ^ pOrder hM y
have h₁ : p ^ (pOrder hM y - k + k) = p ^ pOrder hM y
Tactic: rw [← pow_add, Nat.sub_add_cancel hk]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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
⊢ p ^ (pOrder hM y - k) * p ^ k = p ^ pOrder hM y
have h₂ : p ^ pOrder hM y = p ^ pOrder hM y
Tactic: rw [← pow_add, Nat.sub_add_cancel hk]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
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
⊢ ∃ (a : R), p ^ k • x = p ^ k • a • y
have h₁ : p ^ k • x = p ^ k • HSMul.hSMul.{u, v, v} (α := R) 0 y
Tactic: use 0