awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)) ⊤)
⊢ 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.span R ((⇑(mkQ (R ∙ s j)) : (a : M) → M ⧸ R ∙ s j) '' Set.range s)) ⊤
Tactic: rw [Submodule.map_span, Submodule.map_top, range_mkQ] at hs'
Cleared hypotheses: hs'
-- 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
hs' :
  Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R ((⇑(mkQ (R ∙ s j)) : (a : M) → M ⧸ R ∙ s j) '' Set.range s)) ⊤
⊢ 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.span R ((fun (a : M) ↦ Submodule.Quotient.mk a) '' Set.range s)) ⊤
Tactic: simp only [mkQ_apply] at hs'
Cleared hypotheses: hs'
-- 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
hs' :
  Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R ((fun (a : M) ↦ Submodule.Quotient.mk a) '' Set.range s)) ⊤
⊢ Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R (Set.range (Submodule.Quotient.mk ∘ s ∘ j.succAbove))) ⊤
have h : Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
  (Submodule.span R (Submodule.Quotient.mk ∘ s '' {j}ᶜ)) ⊤
Tactic: rw [← Function.comp_assoc, Set.range_comp (_ ∘ s), Fin.range_succAbove]
-- 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
h' : Module.Finite R M
hM : IsTorsion R M
⊢ ∃ (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ),
    Nonempty (M ≃ₗ[R] ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))
have obtain : ∀ (I : Type u) (fI : Fintype I) (w : DecidableEq I) (p : I → R) (hp : ∀ (i : I), Irreducible (p i)) (e : I → ℕ)
  (h : DirectSum.IsInternal (S := Submodule R M) fun (i : I) ↦ torsionBy R M (p i ^ e i)),
  ∃ (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ),
    Nonempty (M ≃ₗ[R] ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))
Tactic: obtain ⟨I, fI, _, p, hp, e, h⟩ := Submodule.exists_isInternal_prime_power_torsion_of_pid hM
-- 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
h' : Module.Finite R M
hM : IsTorsion R M
I : Type u
fI : Fintype I
w : DecidableEq I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : DirectSum.IsInternal (S := Submodule R M) fun (i : I) ↦ torsionBy R M (p i ^ e i)
⊢ ∃ (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ),
    Nonempty (M ≃ₗ[R] ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))
have this : ∀ (i : I),
  ∃ (d : ℕ) (k : Fin d → ℕ),
    Nonempty
      (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
        (⨁ (j : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ k j)))
Tactic: have :
    ∀ i,
      ∃ (d : ℕ) (k : Fin d → ℕ),
        Nonempty <| torsionBy R M (p i ^ e i) ≃ₗ[R] ⨁ j, R ⧸ R ∙ p i ^ k j := by
    exact fun i =>
      torsion_by_prime_power_decomposition.{u, v} (hp i)
        ((isTorsion'_powers_iff <| p i).mpr fun x => ⟨e i, smul_torsionBy _ _⟩)
-- 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
h' : Module.Finite R M
⊢ ∃ (n : ℕ) (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ),
    Nonempty (M ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))
have obtain : ∀ (I : Type u) (fI : Fintype I) (p : I → R) (hp : ∀ (i : I), Irreducible (p i)) (e : I → ℕ)
  (h :
    LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsion R M))
      (⨁ (i : I), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))),
  ∃ (n : ℕ) (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ),
    Nonempty (M ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))
Tactic: obtain ⟨I, fI, p, hp, e, ⟨h⟩⟩ :=
    equiv_directSum_of_isTorsion.{u, v} (@torsion_isTorsion R M _ _ _)
-- 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
h' : Module.Finite R M
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsion R M))
    (⨁ (i : I), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))
⊢ ∃ (n : ℕ) (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ),
    Nonempty (M ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))
have obtain : ∀ (n : ℕ)
  (g :
    LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (torsion R M)) (Fin n →₀ R)),
  ∃ (n : ℕ) (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ),
    Nonempty (M ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))
Tactic: obtain ⟨n, ⟨g⟩⟩ := @Module.basisOfFiniteTypeTorsionFree' R _ (M ⧸ torsion R M) _ _ _ _ _ _
-- 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
h' : Module.Finite R M
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsion R M))
    (⨁ (i : I), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))
n : ℕ
g : LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (torsion R M)) (Fin n →₀ R)
⊢ ∃ (n : ℕ) (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ),
    Nonempty (M ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))
have obtain : ∀ (f : HasQuotient.Quotient M (B := Submodule R M) (torsion R M) →ₗ[R] M) (hf : mkQ (torsion R M) ∘ₗ f = LinearMap.id),
  ∃ (n : ℕ) (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ),
    Nonempty (M ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))
Tactic: obtain ⟨f, hf⟩ := Module.projective_lifting_property _ LinearMap.id (torsion R M).mkQ_surjective
-- 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
h' : Module.Finite R M
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsion R M))
    (⨁ (i : I), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))
n : ℕ
g : LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (torsion R M)) (Fin n →₀ R)
f : HasQuotient.Quotient M (B := Submodule R M) (torsion R M) →ₗ[R] M
hf : mkQ (torsion R M) ∘ₗ f = LinearMap.id
⊢ ∃ (n : ℕ) (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ),
    Nonempty (M ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))
have R₁ : Eq (α := Submodule R M)
  (LinearMap.range (R := R) (M := ↥(torsion R M)) (τ₁₂ := RingHom.id R) (Submodule.subtype (torsion R M)))
  (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (torsion R M)) (mkQ (torsion R M)))
Tactic: refine
    ⟨n, I, fI, p, hp, e,
      ⟨(lequivProdOfRightSplitExact (torsion R M).injective_subtype ?_ hf).symm.trans <|
          (h.prodCongr g).trans <| LinearEquiv.prodComm.{u, u} R _ (Fin n →₀ R) ⟩⟩
-- 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
h' : Module.Finite R M
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsion R M))
    (⨁ (i : I), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))
n : ℕ
g : LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (torsion R M)) (Fin n →₀ R)
f : HasQuotient.Quotient M (B := Submodule R M) (torsion R M) →ₗ[R] M
hf : mkQ (torsion R M) ∘ₗ f = LinearMap.id
⊢ Eq (α := Submodule R M)
    (LinearMap.range (R := R) (M := ↥(torsion R M)) (τ₁₂ := RingHom.id R) (Submodule.subtype (torsion R M)))
    (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (torsion R M)) (mkQ (torsion R M)))
have rw : Eq (α := Submodule R M) (torsion R M)
  (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (torsion R M)) (mkQ (torsion R M)))
Tactic: rw [range_subtype, ker_mkQ]
-- 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
h' : Module.Finite R M
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsion R M))
    (⨁ (i : I), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ e i))
n : ℕ
g : LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (torsion R M)) (Fin n →₀ R)
f : HasQuotient.Quotient M (B := Submodule R M) (torsion R M) →ₗ[R] M
hf : mkQ (torsion R M) ∘ₗ f = LinearMap.id
rw :
  Eq (α := Submodule R M) (torsion R M)
    (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (torsion R M)) (mkQ (torsion R M)))
⊢ Eq (α := Submodule R M)
    (LinearMap.range (R := R) (M := ↥(torsion R M)) (τ₁₂ := RingHom.id R) (Submodule.subtype (torsion R M)))
    (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (torsion R M)) (mkQ (torsion R M)))
have rw₁ : Eq (α := Submodule R M) (torsion R M) (torsion R M)
Tactic: rw [range_subtype, ker_mkQ]
-- 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
inst_5 : Module.Finite R M
⊢ ∃ (x : M), Eq (α := Submodule R R) (ker (toSpanSingleton R M x)) (annihilator R M)
have have : ∀ (m : ℕ) (ι : Type u) (w : Fintype ι) (p : ι → R) (irr : ∀ (i : ι), Irreducible (p i)) (n : ι → ℕ)
  (e : M ≃ₗ[R] (Fin m →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)),
  ∃ (x : M), Eq (α := Submodule R R) (ker (toSpanSingleton R M x)) (annihilator R M)
Tactic: have ⟨m, ι, _, p, irr, n, ⟨e⟩⟩ := equiv_free_prod_directSum (R := R) (M := M)
-- 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
inst_5 : Module.Finite R M
m : ℕ
ι : Type u
w : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
e : M ≃ₗ[R] (Fin m →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)
⊢ ∃ (x : M), Eq (α := Submodule R R) (ker (toSpanSingleton R M x)) (annihilator R M)
have refine : ∀ (x : R)
  (h :
    Membership.mem (γ := Submodule R R)
      (ker
        (toSpanSingleton R M
          ((e.symm : (a : (Fin m →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ n i) → M)
            ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin m → R) → Fin m →₀ R) fun (x : Fin m) ↦ 1,
              (Equiv.symm
                    (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                      HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                  (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1))))
      x),
  Membership.mem (γ := Submodule R R) (annihilator R M) x
Tactic: refine ⟨e.symm (Finsupp.equivFunOnFinite.symm fun _ ↦ 1, DFinsupp.equivFunOnFintype.symm
    fun _ ↦ mkQ _ 1), le_antisymm (fun x h ↦ ?_) fun x h ↦ mem_annihilator.mp h _⟩
-- 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
inst_5 : Module.Finite R M
m : ℕ
ι : Type u
w : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
e : M ≃ₗ[R] (Fin m →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)
x : R
h :
  Membership.mem (γ := Submodule R R)
    (ker
      (toSpanSingleton R M
        ((e.symm : (a : (Fin m →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ n i) → M)
          ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin m → R) → Fin m →₀ R) fun (x : Fin m) ↦ 1,
            (Equiv.symm
                  (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                    HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
              fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1))))
    x
⊢ Membership.mem (γ := Submodule R R) (annihilator R M) x
have h₁ : (∀ (a : Fin m),
    Eq (α := R)
      (((HSMul.hSMul (β := (Fin m →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin m → R) → Fin m →₀ R) fun (x : Fin m) ↦ 1,
                  (Equiv.symm
                        (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                          HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                      (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                    fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).1 :
            (a : Fin m) → R)
          a :
        R)
      ((0.1 : (a : Fin m) → R) a : R)) ∧
  ∀ (i : ι),
    ((HSMul.hSMul (β := (Fin m →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
              ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin m → R) → Fin m →₀ R) fun (x : Fin m) ↦ 1,
                (Equiv.symm
                      (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                        HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                    (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                  fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).2 :
          (a : ι) → R ⧸ R ∙ p a ^ n a)
        i =
      (0.2 : (a : ι) → R ⧸ R ∙ p a ^ n a) i
Tactic: rw [mem_ker, toSpanSingleton_apply, ← map_smul,
    e.symm.map_eq_zero_iff, Prod.ext_iff, Finsupp.ext_iff, DFinsupp.ext_iff] at h
Cleared hypotheses: h
-- 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
inst_5 : Module.Finite R M
ι : Type u
w : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
e : M ≃ₗ[R] (Fin 0 →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)
h :
  (∀ (a : Fin 0),
      Eq (α := R)
        (((HSMul.hSMul (β := (Fin 0 →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                  ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 0 → R) → Fin 0 →₀ R) fun (x : Fin 0) ↦ 1,
                    (Equiv.symm
                          (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                            HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                        (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                      fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).1 :
              (a : Fin 0) → R)
            a :
          R)
        ((0.1 : (a : Fin 0) → R) a : R)) ∧
    ∀ (i : ι),
      ((HSMul.hSMul (β := (Fin 0 →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 0 → R) → Fin 0 →₀ R) fun (x : Fin 0) ↦ 1,
                  (Equiv.symm
                        (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                          HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                      (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                    fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).2 :
            (a : ι) → R ⧸ R ∙ p a ^ n a)
          i =
        (0.2 : (a : ι) → R ⧸ R ∙ p a ^ n a) i
⊢ Membership.mem (γ := Submodule R R) (annihilator R M) x
have zero : Membership.mem (γ := Submodule R R)
  (annihilator R (Fin 0 →₀ R) ⊓ annihilator R (⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)))
  (HSMul.hSMul (β := R) x 1)
Tactic: rw [← mul_one x, ← smul_eq_mul, e.annihilator_eq, annihilator_prod]
-- 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
inst_5 : Module.Finite R M
ι : Type u
w : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
e : M ≃ₗ[R] (Fin 0 →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)
h :
  (∀ (a : Fin 0),
      Eq (α := R)
        (((HSMul.hSMul (β := (Fin 0 →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                  ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 0 → R) → Fin 0 →₀ R) fun (x : Fin 0) ↦ 1,
                    (Equiv.symm
                          (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                            HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                        (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                      fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).1 :
              (a : Fin 0) → R)
            a :
          R)
        ((0.1 : (a : Fin 0) → R) a : R)) ∧
    ∀ (i : ι),
      ((HSMul.hSMul (β := (Fin 0 →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 0 → R) → Fin 0 →₀ R) fun (x : Fin 0) ↦ 1,
                  (Equiv.symm
                        (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                          HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                      (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                    fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).2 :
            (a : ι) → R ⧸ R ∙ p a ^ n a)
          i =
        (0.2 : (a : ι) → R ⧸ R ∙ p a ^ n a) i
⊢ Membership.mem (γ := Submodule R R)
    (annihilator R (Fin 0 →₀ R) ⊓
      annihilator R (⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)))
    (HSMul.hSMul (β := R) x 1)
have zero : ∀ (i : ι),
  Eq (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))
    (Submodule.Quotient.mk (HSMul.hSMul (β := R) x 1)) 0
Tactic: simp_rw [annihilator_eq_top_iff.mpr inferInstance, DirectSum, annihilator_dfinsupp,
      top_inf_eq, mem_iInf, Ideal.annihilator_quotient, ← Quotient.mk_eq_zero]