awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
inst_3 : Module R A
inst_4 : Module R A'
f : A →ₗ[R] A'
hf :
  Function.Injective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
⊢ Nonempty.{u_1 + 1} (Unique (A' ⧸ f.range))
have refine : ∀ (a : A' ⧸ f.range) (c : CharacterModule (A' ⧸ f.range)),
  Eq (α := AddCircle (𝕜 := ℚ) 1) ((c : (a : A' ⧸ f.range) → AddCircle 1) a : AddCircle (𝕜 := ℚ) 1)
    (0 : AddCircle (𝕜 := ℚ) 1)
Tactic: refine ⟨Unique.mk inferInstance fun a ↦ eq_zero_of_character_apply fun c ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
inst_3 : Module R A
inst_4 : Module R A'
f : A →ₗ[R] A'
hf :
  Function.Injective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
a : A' ⧸ f.range
c : CharacterModule (A' ⧸ f.range)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1) ((c : (a : A' ⧸ f.range) → AddCircle 1) a : AddCircle (𝕜 := ℚ) 1)
    (0 : AddCircle (𝕜 := ℚ) 1)
have obtain : ∀ (b : A'),
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((c : (a : A' ⧸ f.range) → AddCircle 1)
        ((QuotientAddGroup.mk' f.range.toAddSubgroup : (a : A') → A' ⧸ f.range.toAddSubgroup) b) :
      AddCircle (𝕜 := ℚ) 1)
    (0 : AddCircle (𝕜 := ℚ) 1)
Tactic: obtain ⟨b, rfl⟩ := QuotientAddGroup.mk'_surjective _ a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
inst_3 : Module R A
inst_4 : Module R A'
f : A →ₗ[R] A'
hf :
  Function.Injective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
c : CharacterModule (A' ⧸ f.range)
b : A'
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((c : (a : A' ⧸ f.range) → AddCircle 1)
        ((QuotientAddGroup.mk' f.range.toAddSubgroup : (a : A') → A' ⧸ f.range.toAddSubgroup) b) :
      AddCircle (𝕜 := ℚ) 1)
    (0 : AddCircle (𝕜 := ℚ) 1)
have suffices : Eq (α := CharacterModule A')
  ((dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A') c : CharacterModule A')
  (0 : CharacterModule A')
Tactic: suffices eq : dual (Submodule.mkQ _) c = 0 from congr($eq b)
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
inst_3 : Module R A
inst_4 : Module R A'
f : A →ₗ[R] A'
hf :
  Function.Injective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
c : CharacterModule (A' ⧸ f.range)
b : A'
⊢ Eq (α := CharacterModule A')
    ((dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A') c : CharacterModule A')
    (0 : CharacterModule A')
have refine : Eq.{uA + 1} (α := CharacterModule A)
  ((dual f : (a : CharacterModule A') → CharacterModule A)
      ((dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A') c) :
    CharacterModule A)
  ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
Tactic: refine hf ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
inst_3 : Module R A
inst_4 : Module R A'
f : A →ₗ[R] A'
hf :
  Function.Injective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
c : CharacterModule (A' ⧸ f.range)
b : A'
⊢ Eq.{uA + 1} (α := CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A)
        ((dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A') c) :
      CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
have rw : Eq.{uA + 1} (α := CharacterModule A)
  ((dual f ∘ₗ dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
  ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
Tactic: rw [← LinearMap.comp_apply, ← dual_comp, LinearMap.range_mkQ_comp, dual_zero,
    LinearMap.zero_apply, dual_apply, AddMonoidHom.zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
inst_3 : Module R A
inst_4 : Module R A'
f : A →ₗ[R] A'
hf :
  Function.Injective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
c : CharacterModule (A' ⧸ f.range)
b : A'
rw :
  Eq.{uA + 1} (α := CharacterModule A)
    ((dual f ∘ₗ dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
⊢ Eq.{uA + 1} (α := CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A)
        ((dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A') c) :
      CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
have rw₁ : Eq.{uA + 1} (α := CharacterModule A)
  ((dual (f.range.mkQ ∘ₗ f) : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
  ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
Tactic: rw [← LinearMap.comp_apply, ← dual_comp, LinearMap.range_mkQ_comp, dual_zero,
    LinearMap.zero_apply, dual_apply, AddMonoidHom.zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
inst_3 : Module R A
inst_4 : Module R A'
f : A →ₗ[R] A'
hf :
  Function.Injective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
c : CharacterModule (A' ⧸ f.range)
b : A'
rw :
  Eq.{uA + 1} (α := CharacterModule A)
    ((dual f ∘ₗ dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
rw₁ :
  Eq.{uA + 1} (α := CharacterModule A)
    ((dual (f.range.mkQ ∘ₗ f) : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
⊢ Eq.{uA + 1} (α := CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A)
        ((dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A') c) :
      CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
have rw₂ : Eq.{uA + 1} (α := CharacterModule A)
  ((dual 0 : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
  ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
Tactic: rw [← LinearMap.comp_apply, ← dual_comp, LinearMap.range_mkQ_comp, dual_zero,
    LinearMap.zero_apply, dual_apply, AddMonoidHom.zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
inst_3 : Module R A
inst_4 : Module R A'
f : A →ₗ[R] A'
hf :
  Function.Injective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
c : CharacterModule (A' ⧸ f.range)
b : A'
rw :
  Eq.{uA + 1} (α := CharacterModule A)
    ((dual f ∘ₗ dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
rw₁ :
  Eq.{uA + 1} (α := CharacterModule A)
    ((dual (f.range.mkQ ∘ₗ f) : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
rw₂ :
  Eq.{uA + 1} (α := CharacterModule A)
    ((dual 0 : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
⊢ Eq.{uA + 1} (α := CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A)
        ((dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A') c) :
      CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
have rw₃ : Eq.{uA + 1} (α := CharacterModule A)
  (((0 : LinearMap.{uR, uR, u_1, uA} (RingHom.id R) (CharacterModule (A' ⧸ f.range)) (CharacterModule A)) :
        (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A)
      c :
    CharacterModule A)
  ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
Tactic: rw [← LinearMap.comp_apply, ← dual_comp, LinearMap.range_mkQ_comp, dual_zero,
    LinearMap.zero_apply, dual_apply, AddMonoidHom.zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
inst_3 : Module R A
inst_4 : Module R A'
f : A →ₗ[R] A'
hf :
  Function.Injective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
c : CharacterModule (A' ⧸ f.range)
b : A'
rw :
  Eq.{uA + 1} (α := CharacterModule A)
    ((dual f ∘ₗ dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
rw₁ :
  Eq.{uA + 1} (α := CharacterModule A)
    ((dual (f.range.mkQ ∘ₗ f) : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
rw₂ :
  Eq.{uA + 1} (α := CharacterModule A)
    ((dual 0 : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
rw₃ :
  Eq.{uA + 1} (α := CharacterModule A)
    (((0 : LinearMap.{uR, uR, u_1, uA} (RingHom.id R) (CharacterModule (A' ⧸ f.range)) (CharacterModule A)) :
          (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A)
        c :
      CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
⊢ Eq.{uA + 1} (α := CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A)
        ((dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A') c) :
      CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
have rw₄ : Eq.{uA + 1} (α := CharacterModule A) 0 ((dual f : (a : CharacterModule A') → CharacterModule A) 0)
Tactic: rw [← LinearMap.comp_apply, ← dual_comp, LinearMap.range_mkQ_comp, dual_zero,
    LinearMap.zero_apply, dual_apply, AddMonoidHom.zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
inst_3 : Module R A
inst_4 : Module R A'
f : A →ₗ[R] A'
hf :
  Function.Injective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
c : CharacterModule (A' ⧸ f.range)
b : A'
rw :
  Eq.{uA + 1} (α := CharacterModule A)
    ((dual f ∘ₗ dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
rw₁ :
  Eq.{uA + 1} (α := CharacterModule A)
    ((dual (f.range.mkQ ∘ₗ f) : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
rw₂ :
  Eq.{uA + 1} (α := CharacterModule A)
    ((dual 0 : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
rw₃ :
  Eq.{uA + 1} (α := CharacterModule A)
    (((0 : LinearMap.{uR, uR, u_1, uA} (RingHom.id R) (CharacterModule (A' ⧸ f.range)) (CharacterModule A)) :
          (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A)
        c :
      CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
rw₄ : Eq.{uA + 1} (α := CharacterModule A) 0 ((dual f : (a : CharacterModule A') → CharacterModule A) 0)
⊢ Eq.{uA + 1} (α := CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A)
        ((dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A') c) :
      CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
have rw₅ : Eq (α := CharacterModule A) 0 (AddMonoidHom.comp 0 f.toAddMonoidHom)
Tactic: rw [← LinearMap.comp_apply, ← dual_comp, LinearMap.range_mkQ_comp, dual_zero,
    LinearMap.zero_apply, dual_apply, AddMonoidHom.zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
inst_3 : Module R A
inst_4 : Module R A'
f : A →ₗ[R] A'
hf :
  Function.Injective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
c : CharacterModule (A' ⧸ f.range)
b : A'
rw :
  Eq.{uA + 1} (α := CharacterModule A)
    ((dual f ∘ₗ dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
rw₁ :
  Eq.{uA + 1} (α := CharacterModule A)
    ((dual (f.range.mkQ ∘ₗ f) : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
rw₂ :
  Eq.{uA + 1} (α := CharacterModule A)
    ((dual 0 : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A) c : CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
rw₃ :
  Eq.{uA + 1} (α := CharacterModule A)
    (((0 : LinearMap.{uR, uR, u_1, uA} (RingHom.id R) (CharacterModule (A' ⧸ f.range)) (CharacterModule A)) :
          (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A)
        c :
      CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
rw₄ : Eq.{uA + 1} (α := CharacterModule A) 0 ((dual f : (a : CharacterModule A') → CharacterModule A) 0)
rw₅ : Eq (α := CharacterModule A) 0 (AddMonoidHom.comp 0 f.toAddMonoidHom)
⊢ Eq.{uA + 1} (α := CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A)
        ((dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A') c) :
      CharacterModule A)
    ((dual f : (a : CharacterModule A') → CharacterModule A) 0 : CharacterModule A)
have rw₆ : Eq.{uA + 1} (α := CharacterModule A) 0 0
Tactic: rw [← LinearMap.comp_apply, ← dual_comp, LinearMap.range_mkQ_comp, dual_zero,
    LinearMap.zero_apply, dual_apply, AddMonoidHom.zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.Congruence.Defs (hypothesis)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : SMul R M
inst_1 : SMul S N
φ : R → S
f : M →ₑ[φ] N
r : R
x x_1 : M
h : (Setoid.ker (⇑f : (a : M) → N) : M → M → Prop) x x_1
⊢ (Setoid.ker (⇑f : (a : M) → N) : M → M → Prop) (r • x) (r • x_1)
have h₁ : Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) x_1 : N)
Tactic: rw [Setoid.ker_def] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Congruence.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : SMul R M
inst_1 : SMul S N
φ : R → S
f : M →ₑ[φ] N
r : R
x x_1 : M
h : Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) x_1 : N)
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) (r • x) : N) ((f : (a : M) → N) (r • x_1) : N)
have simp_rw : HSMul.hSMul (β := N) (φ r) ((f : (a : M) → N) x : N) = HSMul.hSMul (β := N) (φ r) ((f : (a : M) → N) x_1 : N)
Tactic: simp_rw [map_smulₛₗ, h]
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
⊢ DirectSum.IsInternal (S := Submodule R M) fun (p : ↥(factors I).toFinset) ↦
    torsionBySet R M (↑((↑p : Ideal R) ^ Multiset.count (↑p : Ideal R) (factors I)) : Set R)
have prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
Tactic: have prime_of_mem := fun p (hp : p ∈ P.toFinset) =>
    prime_of_factor p (Multiset.mem_toFinset.mp hp)
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
⊢ DirectSum.IsInternal (S := Submodule R M) fun (p : ↥(factors I).toFinset) ↦
    torsionBySet R M (↑((↑p : Ideal R) ^ Multiset.count (↑p : Ideal R) (factors I)) : Set R)
have apply : Module.IsTorsionBySet R M (↑(⨅ i ∈ (factors I).toFinset, i ^ Multiset.count i P) : Set R)
Tactic: apply torsionBySet_isInternal (p := fun p => p ^ P.count p) _
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
apply : Module.IsTorsionBySet R M (↑(⨅ i ∈ (factors I).toFinset, i ^ Multiset.count i P) : Set R)
⊢ DirectSum.IsInternal (S := Submodule R M) fun (p : ↥(factors I).toFinset) ↦
    torsionBySet R M (↑((↑p : Ideal R) ^ Multiset.count (↑p : Ideal R) (factors I)) : Set R)
have apply₁ : (↑(factors I).toFinset : Set (Ideal R)).Pairwise fun (i j : Ideal R) ↦
  Eq.{u + 1} (α := Ideal R)
    ((fun (p : Ideal R) ↦ p ^ Multiset.count p P) i ⊔ (fun (p : Ideal R) ↦ p ^ Multiset.count p P) j) ⊤
Tactic: apply torsionBySet_isInternal (p := fun p => p ^ P.count p) _
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
⊢ Module.IsTorsionBySet R M (↑(⨅ i ∈ (factors I).toFinset, i ^ Multiset.count i P) : Set R)
have h : ⨅ i ∈ (factors I).toFinset, i ^ Multiset.count i P = I
Tactic: convert! hM
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
⊢ ⨅ i ∈ (factors I).toFinset, i ^ Multiset.count i P = I
have h : Associated (factors I).prod I
Tactic: rw [← Finset.inf_eq_iInf, IsDedekindDomain.inf_pow_eq_prod_of_prime,
      ← Finset.prod_multiset_count, ← associated_iff_eq]
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
h : Associated (factors I).prod I
h₁ : ∀ i ∈ (factors I).toFinset, Prime i
⊢ ⨅ i ∈ (factors I).toFinset, i ^ Multiset.count i P = I
have h₂ : ∀ i ∈ (factors I).toFinset, ∀ j ∈ (factors I).toFinset, i ≠ j → i ≠ j
Tactic: rw [← Finset.inf_eq_iInf, IsDedekindDomain.inf_pow_eq_prod_of_prime,
      ← Finset.prod_multiset_count, ← associated_iff_eq]
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
p : Ideal R
hp : p ∈ (↑(factors I).toFinset : Set (Ideal R))
q : Ideal R
hq : q ∈ (↑(factors I).toFinset : Set (Ideal R))
pq : p ≠ q
⊢ p ^ Multiset.count p P ⊔ q ^ Multiset.count q P = ⊤
have rw : p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q P))) (Multiset.count p P) = ⊤
Tactic: rw [Ideal.irreducible_pow_sup]
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
p : Ideal R
hp : p ∈ (↑(factors I).toFinset : Set (Ideal R))
q : Ideal R
hq : q ∈ (↑(factors I).toFinset : Set (Ideal R))
pq : p ≠ q
rw : p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q P))) (Multiset.count p P) = ⊤
⊢ p ^ Multiset.count p P ⊔ q ^ Multiset.count q P = ⊤
have hI₁ : q ^ Multiset.count q P ≠ ⊥
Tactic: rw [Ideal.irreducible_pow_sup]
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
p : Ideal R
hp : p ∈ (↑(factors I).toFinset : Set (Ideal R))
q : Ideal R
hq : q ∈ (↑(factors I).toFinset : Set (Ideal R))
pq : p ≠ q
rw : p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q P))) (Multiset.count p P) = ⊤
hI₁ : q ^ Multiset.count q P ≠ ⊥
⊢ p ^ Multiset.count p P ⊔ q ^ Multiset.count q P = ⊤
have hJ : Irreducible p
Tactic: rw [Ideal.irreducible_pow_sup]
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
p : Ideal R
hp : p ∈ (↑(factors I).toFinset : Set (Ideal R))
q : Ideal R
hq : q ∈ (↑(factors I).toFinset : Set (Ideal R))
pq : p ≠ q
this : Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) = 0
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q P))) (Multiset.count p P) = ⊤
have rw : p ^ min 0 (Multiset.count p P) = ⊤
Tactic: rw [this, zero_min, pow_zero, Ideal.one_eq_top]