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 : pOrder hM y < k
⊢ p ^ k • x = p ^ k • HSMul.hSMul.{u, v, v} (α := R) 0 y
have h₁ : p ^ k • x = HSMul.hSMul (β := M) (p ^ k) 0
Tactic: rw [zero_smul, smul_zero, ← Nat.sub_add_cancel hk.le, pow_add, mul_smul, hM',
      smul_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 : pOrder hM y < k
h₁ : p ^ k • x = HSMul.hSMul (β := M) (p ^ k) 0
⊢ p ^ k • x = p ^ k • HSMul.hSMul.{u, v, v} (α := R) 0 y
have h₂ : p ^ k • x = 0
Tactic: rw [zero_smul, smul_zero, ← Nat.sub_add_cancel hk.le, pow_add, mul_smul, hM',
      smul_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 : pOrder hM y < k
h₁ : p ^ k • x = HSMul.hSMul (β := M) (p ^ k) 0
h₂ : p ^ k • x = 0
⊢ p ^ k • x = p ^ k • HSMul.hSMul.{u, v, v} (α := R) 0 y
have h₃ : p ^ (k - pOrder hM y + pOrder hM y) • x = 0
Tactic: rw [zero_smul, smul_zero, ← Nat.sub_add_cancel hk.le, pow_add, mul_smul, hM',
      smul_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 : 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
⊢ p ^ k • x = p ^ k • HSMul.hSMul.{u, v, v} (α := R) 0 y
have h₄ : (p ^ (k - pOrder hM y) * p ^ pOrder hM y) • x = 0
Tactic: rw [zero_smul, smul_zero, ← Nat.sub_add_cancel hk.le, pow_add, mul_smul, hM',
      smul_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 : 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
⊢ p ^ k • x = p ^ k • HSMul.hSMul.{u, v, v} (α := R) 0 y
have h₅ : p ^ (k - pOrder hM y) • p ^ pOrder hM y • x = 0
Tactic: rw [zero_smul, smul_zero, ← Nat.sub_add_cancel hk.le, pow_add, mul_smul, hM',
      smul_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 : 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
⊢ p ^ k • x = p ^ k • HSMul.hSMul.{u, v, v} (α := R) 0 y
have h₆ : HSMul.hSMul (β := M) (p ^ (k - pOrder hM y)) 0 = 0
Tactic: rw [zero_smul, smul_zero, ← Nat.sub_add_cancel hk.le, pow_add, mul_smul, hM',
      smul_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 : 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
⊢ p ^ k • x = p ^ k • HSMul.hSMul.{u, v, v} (α := R) 0 y
have h₇ : Eq.{v + 1} (α := M) 0 0
Tactic: rw [zero_smul, smul_zero, ← Nat.sub_add_cancel hk.le, pow_add, mul_smul, hM',
      smul_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)
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))
⊢ ∃ (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)
have 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)
Tactic: have f1 := mk_surjective (R ∙ z) (f 1)
-- 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)
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)))
have 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))
Tactic: rw [← Quotient.mk_eq_zero, mk_smul, f1.choose_spec, ← f.map_smul]
-- 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)
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)
        (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))
have h : HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k)) (p ^ k) 1 = 0
Tactic: convert! f.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)
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)
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k)) (p ^ k) (Submodule.Quotient.mk 1) = 0
have h : Membership.mem (γ := Submodule R R) (R ∙ p ^ k) (p ^ k)
Tactic: rw [← mk_smul, Quotient.mk_eq_zero, smul_eq_mul, mul_one]
-- 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)
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)
⊢ ∃ (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)
have 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)))
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 _
-- 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)
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)))
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨a, ha⟩ := p_pow_smul_lift hp hM hz 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)
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
⊢ 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
have 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
Tactic: rw [smul_sub, sub_eq_zero, 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)
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
⊢ 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
have rw₂ : p ^ k • a • z = p ^ k • a • z
Tactic: rw [smul_sub, sub_eq_zero, 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)
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
⊢ ∃ (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)
have 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)
Tactic: refine ⟨f1.choose - a • z, by rw [smul_sub, sub_eq_zero, 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)
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
⊢ 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)
have rw : HSub.hSub (α := 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))))
    (Submodule.Quotient.mk (a • z)) =
  (f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1
Tactic: rw [mk_sub, mk_smul, (Quotient.mk_eq_zero _).mpr <| Submodule.mem_span_singleton_self _,
    smul_zero, sub_zero, f1.choose_spec]
-- 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)
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 :
  HSub.hSub (α := 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))))
      (Submodule.Quotient.mk (a • z)) =
    (f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1
⊢ 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)
have rw₁ : 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))) -
    HSMul.hSMul (β := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) a (Submodule.Quotient.mk z) =
  (f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1
Tactic: rw [mk_sub, mk_smul, (Quotient.mk_eq_zero _).mpr <| Submodule.mem_span_singleton_self _,
    smul_zero, sub_zero, f1.choose_spec]