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
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
i : Fin d
fi : LinearMap.{u, u, u, v} (RingHom.id R) (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
  (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)) :=
  (↑f.symm : (⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) →ₗ[R] M ⧸ R ∙ s j) ∘ₗ
    DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i
x : M
h0 : p ^ k i • x = 0
h1 :
  Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)) (Submodule.Quotient.mk x)
    ((fi : (a : R ⧸ R ∙ p ^ k i) → M ⧸ R ∙ s j) 1)
⊢ Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
    ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
      ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
    (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
            HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
              ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
          (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
        1 :
      ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
have rw : Eq (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
  ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) ((fi : (a : R ⧸ R ∙ p ^ k i) → M ⧸ R ∙ s j) 1) :
    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
  (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
          HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
        (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
      1 :
    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
Tactic: rw [h1]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
⊢ ∃ (k : Fin (d + 1) → ℕ),
    Nonempty (M ≃ₗ[R] ⨁ (i : Fin (d + 1)), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
have this₁ : ∀ (i : Fin d),
  ∃ (x : M),
    p ^ k i • x = 0 ∧
      Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
        ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
          ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
        (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                  ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
              (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
            1 :
          ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
Tactic: have : ∀ i : Fin d,
          ∃ x : M, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = DirectSum.lof R _ _ i 1 := by
        intro i
        let fi := f.symm.toLinearMap.comp (DirectSum.lof _ _ _ i)
        obtain ⟨x, h0, h1⟩ := exists_smul_eq_zero_and_mk_eq hp hM hj fi; refine ⟨x, h0, ?_⟩; rw [h1]
        simp only [fi, LinearMap.coe_comp, f.symm.coe_toLinearMap, f.apply_symm_apply,
          Function.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this_1 : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
this :
  ∀ (i : Fin d),
    ∃ (x : M),
      p ^ k i • x = 0 ∧
        Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
              1 :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
⊢ ∃ (k : Fin (d + 1) → ℕ),
    Nonempty (M ≃ₗ[R] ⨁ (i : Fin (d + 1)), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
have h : Fin (d + 1) → ℕ
Tactic: refine ⟨?_, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this_1 : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
this :
  ∀ (i : Fin d),
    ∃ (x : M),
      p ^ k i • x = 0 ∧
        Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
              1 :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
h : Fin (d + 1) → ℕ
⊢ ∃ (k : Fin (d + 1) → ℕ),
    Nonempty (M ≃ₗ[R] ⨁ (i : Fin (d + 1)), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
have h₁ : M ≃ₗ[R]
  ⨁ (i : Fin (d + 1)),
    HasQuotient.Quotient R (B := Submodule R R)
      (R ∙
        HPow.hPow (β := ℕ) p
          ((fun (i : Option (Fin d)) ↦ (Option.rec (motive := fun (x : Option (Fin d)) ↦ ℕ) (pOrder hM (s j)) k i : ℕ))
            ((finSuccEquiv d : (a : Fin (d + 1)) → Option (Fin d)) i)))
Tactic: refine ⟨?_, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this_1 : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
this :
  ∀ (i : Fin d),
    ∃ (x : M),
      p ^ k i • x = 0 ∧
        Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
              1 :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
⊢ M ≃ₗ[R]
    ⨁ (i : Fin (d + 1)),
      HasQuotient.Quotient R (B := Submodule R R)
        (R ∙
          HPow.hPow (β := ℕ) p
            ((fun (i : Option (Fin d)) ↦
                (Option.rec (motive := fun (x : Option (Fin d)) ↦ ℕ) (pOrder hM (s j)) k i : ℕ))
              ((finSuccEquiv d : (a : Fin (d + 1)) → Option (Fin d)) i)))
have h : LinearMap.range (M := ↥(R ∙ s j)) (Submodule.subtype (R ∙ s j)) =
  ((↑f : M ⧸ R ∙ s j →ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) ∘ₗ mkQ (R ∙ s j)).ker
Tactic: refine
          (lequivProdOfRightSplitExact
            (g := f.toLinearMap.comp <| mkQ _)
            (f := (DirectSum.toModule _ _ _ fun i => (liftQSpanSingleton (p ^ k i)
                (LinearMap.toSpanSingleton _ _ _) (this i).choose_spec.left : R ⧸ _ →ₗ[R] _)))
              (R ∙ s j).injective_subtype ?_ ?_).symm ≪≫ₗ
          (((quotTorsionOfEquivSpanSingleton R M (s j)).symm ≪≫ₗ
            (quotEquivOfEq (torsionOf R M (s j)) _
              (Ideal.torsionOf_eq_span_pow_pOrder hp hM (s j)))).prodCongr (.refl _ _)) ≪≫ₗ
          (@DirectSum.lequivProdDirectSum R _ _
            (fun i => R ⧸ R ∙ p ^ @Option.rec _ (fun _ => ℕ) (pOrder hM <| s j) k i) _ _).symm ≪≫ₗ
          (DirectSum.lequivCongrLeft R (finSuccEquiv d).symm)
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this_1 : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
this :
  ∀ (i : Fin d),
    ∃ (x : M),
      p ^ k i • x = 0 ∧
        Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
              1 :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
⊢ LinearMap.range (M := ↥(R ∙ s j)) (Submodule.subtype (R ∙ s j)) =
    ((↑f : M ⧸ R ∙ s j →ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) ∘ₗ mkQ (R ∙ s j)).ker
have h : R ∙ s j = ((↑f : M ⧸ R ∙ s j →ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) ∘ₗ mkQ (R ∙ s j)).ker
Tactic: rw [range_subtype, LinearEquiv.ker_comp, ker_mkQ]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this_1 : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
this :
  ∀ (i : Fin d),
    ∃ (x : M),
      p ^ k i • x = 0 ∧
        Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
              1 :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
h : R ∙ s j = ((↑f : M ⧸ R ∙ s j →ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) ∘ₗ mkQ (R ∙ s j)).ker
⊢ LinearMap.range (M := ↥(R ∙ s j)) (Submodule.subtype (R ∙ s j)) =
    ((↑f : M ⧸ R ∙ s j →ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) ∘ₗ mkQ (R ∙ s j)).ker
have h₁ : Eq (α := Submodule R M) (R ∙ s j)
  (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)) (mkQ (R ∙ s j)))
Tactic: rw [range_subtype, LinearEquiv.ker_comp, ker_mkQ]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this_1 : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
this :
  ∀ (i : Fin d),
    ∃ (x : M),
      p ^ k i • x = 0 ∧
        Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
              1 :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
h : R ∙ s j = ((↑f : M ⧸ R ∙ s j →ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) ∘ₗ mkQ (R ∙ s j)).ker
h₁ :
  Eq (α := Submodule R M) (R ∙ s j)
    (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)) (mkQ (R ∙ s j)))
⊢ LinearMap.range (M := ↥(R ∙ s j)) (Submodule.subtype (R ∙ s j)) =
    ((↑f : M ⧸ R ∙ s j →ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) ∘ₗ mkQ (R ∙ s j)).ker
have h₂ : Eq (α := Submodule R M) (R ∙ s j) (R ∙ s j)
Tactic: rw [range_subtype, LinearEquiv.ker_comp, ker_mkQ]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst_5 : AddCommGroup M] [inst_6 : Module R M] (hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p))
    (s : Fin d → M) (hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤),
    ∃ (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
x : M
⊢ HSMul.hSMul (β := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
      (Exists.choose (p := fun (a : ↥(Submonoid.powers p)) ↦ a • x = 0) ⋯) (Submodule.Quotient.mk x) =
    0
have rw : Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
  (Submodule.Quotient.mk (Exists.choose (p := fun (a : ↥(Submonoid.powers p)) ↦ a • x = 0) sorry • x)) 0
Tactic: rw [← Quotient.mk_smul, (@hM x).choose_spec, Quotient.mk_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst_5 : AddCommGroup M] [inst_6 : Module R M] (hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p))
    (s : Fin d → M) (hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤),
    ∃ (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
x : M
rw :
  Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (Submodule.Quotient.mk (Exists.choose (p := fun (a : ↥(Submonoid.powers p)) ↦ a • x = 0) ⋯ • x)) 0
⊢ HSMul.hSMul (β := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
      (Exists.choose (p := fun (a : ↥(Submonoid.powers p)) ↦ a • x = 0) ⋯) (Submodule.Quotient.mk x) =
    0
have rw₁ : Eq.{v + 1} (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)) (Submodule.Quotient.mk 0) 0
Tactic: rw [← Quotient.mk_smul, (@hM x).choose_spec, Quotient.mk_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst_5 : AddCommGroup M] [inst_6 : Module R M] (hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p))
    (s : Fin d → M) (hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤),
    ∃ (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
x : M
rw :
  Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (Submodule.Quotient.mk (Exists.choose (p := fun (a : ↥(Submonoid.powers p)) ↦ a • x = 0) ⋯ • x)) 0
rw₁ : Eq.{v + 1} (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)) (Submodule.Quotient.mk 0) 0
⊢ HSMul.hSMul (β := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
      (Exists.choose (p := fun (a : ↥(Submonoid.powers p)) ↦ a • x = 0) ⋯) (Submodule.Quotient.mk x) =
    0
have rw₂ : Eq.{v + 1} (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)) 0 0
Tactic: rw [← Quotient.mk_smul, (@hM x).choose_spec, Quotient.mk_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst_5 : AddCommGroup M] [inst_6 : Module R M] (hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p))
    (s : Fin d → M) (hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤),
    ∃ (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
⊢ Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))) (Submodule.span R (Set.range s')) ⊤
have hs' : Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
  (Submodule.map (mkQ (R ∙ s j)) (Submodule.span R (Set.range s))) (Submodule.map (mkQ (R ∙ s j)) ⊤)
Tactic: have hs' := congr_arg (Submodule.map <| mkQ <| R ∙ s j) hs