awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
A : Type uA
inst : AddCommGroup A
a : A
n : ℤ
hn : (HSMul.hSMul (β := ℚ) n 1).den = Rat.den (↑(if addOrderOf a = 0 then 2 else addOrderOf a) : ℚ)⁻¹
rw : ∀ (hn : 1 = if addOrderOf a = 0 then 2 else addOrderOf a), a = 0
rw₁ :
  ∀ (hn : 1 = Rat.den (↑(if addOrderOf a = 0 then 2 else addOrderOf a) : ℚ)⁻¹),
    0 < if addOrderOf a = 0 then 2 else addOrderOf a
⊢ a = 0

Tactic:
rw [zsmul_one, Rat.den_intCast, Rat.inv_natCast_den_of_pos] at hn

Premises used: Rat.den_intCast, Rat.inv_natCast_den_of_pos, zsmul_one
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
A : Type uA
inst : AddCommGroup A
a : A
n : ℤ
hn : 1 = if addOrderOf a = 0 then 2 else addOrderOf a
pos : addOrderOf a = 0 → ∀ (hn : Eq (α := ℕ) 1 2), a = 0
neg : ¬addOrderOf a = 0 → ∀ (hn : 1 = addOrderOf a), a = 0
⊢ a = 0

Tactic:
split_ifs at hn
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
A : Type uA
inst : AddCommGroup A
a : A
n : ℤ
h : addOrderOf a = 0
hn : Eq (α := ℕ) 1 2
⊢ a = 0

Tactic:
cases hn
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
A : Type uA
inst : AddCommGroup A
a : A
n : ℤ
h : ¬addOrderOf a = 0
hn : 1 = addOrderOf a
neg : ∀ (hn : addOrderOf a = 1), a = 0
neg₁ neg₂ neg₃ neg₄ : ∀ (hn : a = 0), a = 0
⊢ a = 0

Tactic:
rwa [eq_comm, AddMonoid.addOrderOf_eq_one_iff] at hn

Premises used: AddMonoid.addOrderOf_eq_one_iff, eq_comm
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
A : Type uA
inst : AddCommGroup A
a : A
n : ℤ
hn : 1 = Rat.den (↑(if addOrderOf a = 0 then 2 else addOrderOf a) : ℚ)⁻¹
⊢ 0 < if addOrderOf a = 0 then 2 else addOrderOf a

Tactic:
grind
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
A : Type uA
inst : AddCommGroup A
a : A
ne_zero : a ≠ 0
c : CharacterModule A
hc :
  Eq (α := CharacterModule ↥(ℤ ∙ a))
    ((dual (Submodule.subtype (ℤ ∙ a)) : (a_1 : CharacterModule A) → CharacterModule ↥(ℤ ∙ a)) c :
      CharacterModule ↥(ℤ ∙ a))
    (ofSpanSingleton a : CharacterModule ↥(ℤ ∙ a))
h : Eq (α := AddCircle (𝕜 := ℚ) 1) ((c : (a : A) → AddCircle 1) a : AddCircle (𝕜 := ℚ) 1) (0 : AddCircle (𝕜 := ℚ) 1)
rwa rwa₁ rwa₂ rwa₃ :
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((dual (Submodule.subtype (ℤ ∙ a)) : (a_1 : CharacterModule A) → CharacterModule ↥(ℤ ∙ a)) c :
            CharacterModule ↥(ℤ ∙ a)) :
          (a : ↥(ℤ ∙ a)) → AddCircle 1)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submodule ℤ A) (ℤ ∙ a) x) a ⋯) :
      AddCircle (𝕜 := ℚ) 1)
    (0 : AddCircle (𝕜 := ℚ) 1)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((ofSpanSingleton a : CharacterModule ↥(ℤ ∙ a)) : (a : ↥(ℤ ∙ a)) → AddCircle 1)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submodule ℤ A) (ℤ ∙ a) x) a ⋯) :
      AddCircle (𝕜 := ℚ) 1)
    (0 : AddCircle (𝕜 := ℚ) 1)

Tactic:
rwa [← hc]
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
A : Type uA
inst : AddCommGroup A
a : A
h :
  ∀ (c : CharacterModule A),
    Eq (α := AddCircle (𝕜 := ℚ) 1) ((c : (a : A) → AddCircle 1) a : AddCircle (𝕜 := ℚ) 1) (0 : AddCircle (𝕜 := ℚ) 1)
contrapose! :
  ∀ (h : a ≠ 0),
    ∃ (c : CharacterModule A),
      Ne (α := AddCircle (𝕜 := ℚ) 1) ((c : (a : A) → AddCircle 1) a : AddCircle (𝕜 := ℚ) 1) (0 : AddCircle (𝕜 := ℚ) 1)
⊢ a = 0

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
A : Type uA
inst : AddCommGroup A
a : A
h : a ≠ 0
⊢ ∃ (c : CharacterModule A),
    Ne (α := AddCircle (𝕜 := ℚ) 1) ((c : (a : A) → AddCircle 1) a : AddCircle (𝕜 := ℚ) 1) (0 : AddCircle (𝕜 := ℚ) 1)

Tactic:
exists_character_apply_ne_zero_of_ne_zero h

Premises used: CharacterModule.exists_character_apply_ne_zero_of_ne_zero
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
A : Type uA
inst : AddCommGroup A
a : A
h : a ≠ 0
⊢ ∃ (c : CharacterModule A),
    Ne (α := AddCircle (𝕜 := ℚ) 1) ((c : (a : A) → AddCircle 1) a : AddCircle (𝕜 := ℚ) 1) (0 : AddCircle (𝕜 := ℚ) 1)

Tactic:
exact exists_character_apply_ne_zero_of_ne_zero h

Premises used: CharacterModule.exists_character_apply_ne_zero_of_ne_zero
-- Module: Mathlib.Algebra.Module.CharacterModule
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'
h :
  Function.Surjective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
a : A
h0 : Eq.{u_1 + 1} (α := A') ((f : (a : A) → A') a : A') (0 : A')
c : CharacterModule A
obtain :
  ∀ (c : CharacterModule A'),
    Eq (α := AddCircle (𝕜 := ℚ) 1)
      ((((dual f : (a : CharacterModule A') → CharacterModule A) c : CharacterModule A) : (a : A) → AddCircle 1) a :
        AddCircle (𝕜 := ℚ) 1)
      (0 : AddCircle (𝕜 := ℚ) 1)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1) ((c : (a : A) → AddCircle 1) a : AddCircle (𝕜 := ℚ) 1) (0 : AddCircle (𝕜 := ℚ) 1)

Tactic:
obtain ⟨c, rfl⟩ := h c

Premises used: rfl
-- Module: Mathlib.Algebra.Module.CharacterModule
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'
h :
  Function.Surjective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
a : A
h0 : Eq.{u_1 + 1} (α := A') ((f : (a : A) → A') a : A') (0 : A')
c : CharacterModule A'
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((dual f : (a : CharacterModule A') → CharacterModule A) c : CharacterModule A) : (a : A) → AddCircle 1) a :
      AddCircle (𝕜 := ℚ) 1)
    (0 : AddCircle (𝕜 := ℚ) 1)

Tactic:
congr(c $h0).trans c.map_zero

Premises used: AddMonoidHom.map_zero, congrArg, id, DFunLike.coe, Eq.trans
-- Module: Mathlib.Algebra.Module.CharacterModule
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'
h :
  Function.Surjective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
a : A
h0 : Eq.{u_1 + 1} (α := A') ((f : (a : A) → A') a : A') (0 : A')
c : CharacterModule A'
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((dual f : (a : CharacterModule A') → CharacterModule A) c : CharacterModule A) : (a : A) → AddCircle 1) a :
      AddCircle (𝕜 := ℚ) 1)
    (0 : AddCircle (𝕜 := ℚ) 1)

Tactic:
exact congr(c $h0).trans c.map_zero

Premises used: AddMonoidHom.map_zero, congrArg, id, DFunLike.coe, Eq.trans
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
inst_4 : Module R A
inst_5 : Module R A'
inst_6 : Module R B
f : A →ₗ[R] A'
⊢ Function.Injective (α := TensorProduct R A B) (β := TensorProduct R A' B)
      (⇑(LinearMap.rTensor B f) : (a : TensorProduct R A B) → TensorProduct R A' B) ↔
    Function.Surjective (α := LinearMap.{uR, uR, u_1, uB} (RingHom.id R) A' (CharacterModule B)) (β :=
      LinearMap.{uR, uR, uA, uB} (RingHom.id R) A (CharacterModule B))
      (⇑(LinearMap.lcomp R (CharacterModule B) f) : (a : A' →ₗ[R] CharacterModule B) → A →ₗ[R] CharacterModule B)

Tactic:
simp [← dual_rTensor_conj_homEquiv, dual_surjective_iff_injective]

Premises used: CharacterModule.dual_rTensor_conj_homEquiv, CharacterModule.dual_surjective_iff_injective
-- Module: Mathlib.Algebra.Module.CharacterModule
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)
rw : Nonempty.{u_1 + 1} (Unique (A' ⧸ f.range))
⊢ Function.Surjective.{uA + 1, u_1 + 1} (α := A) (β := A') (⇑f : (a : A) → A')

Tactic:
rw [← LinearMap.range_eq_top, ← Submodule.unique_quotient_iff_eq_top]

Premises used: Submodule.unique_quotient_iff_eq_top, LinearMap.range_eq_top
-- Module: Mathlib.Algebra.Module.CharacterModule
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))

Tactic:
⟨Unique.mk inferInstance fun a ↦ eq_zero_of_character_apply fun c ↦ ?_⟩

Premises used: Unique.mk, inferInstance, Nonempty.intro, CharacterModule.eq_zero_of_character_apply
-- Module: Mathlib.Algebra.Module.CharacterModule
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)
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)
⊢ Nonempty.{u_1 + 1} (Unique (A' ⧸ f.range))

Tactic:
refine ⟨Unique.mk inferInstance fun a ↦ eq_zero_of_character_apply fun c ↦ ?_⟩
-- Module: Mathlib.Algebra.Module.CharacterModule
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)
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)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1) ((c : (a : A' ⧸ f.range) → AddCircle 1) a : AddCircle (𝕜 := ℚ) 1)
    (0 : AddCircle (𝕜 := ℚ) 1)

Tactic:
obtain ⟨b, rfl⟩ := QuotientAddGroup.mk'_surjective _ a

Premises used: QuotientAddGroup.mk'_surjective, rfl
-- Module: Mathlib.Algebra.Module.CharacterModule
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'
suffices :
  Eq (α := CharacterModule A')
    ((dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A') c : CharacterModule A')
    (0 : CharacterModule 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:
suffices eq : dual (Submodule.mkQ _) c = 0 from congr($eq b)
-- Module: Mathlib.Algebra.Module.CharacterModule
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')

Tactic:
hf ?_
-- Module: Mathlib.Algebra.Module.CharacterModule
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'
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)
⊢ Eq (α := CharacterModule A')
    ((dual f.range.mkQ : (a : CharacterModule (A' ⧸ f.range)) → CharacterModule A') c : CharacterModule A')
    (0 : CharacterModule A')

Tactic:
refine hf ?_
-- Module: Mathlib.Algebra.Module.CharacterModule
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)
rw₆ rw₇ : Eq.{uA + 1} (α := CharacterModule A) 0 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)

Tactic:
rw [← LinearMap.comp_apply, ← dual_comp, LinearMap.range_mkQ_comp, dual_zero,
    LinearMap.zero_apply, dual_apply, AddMonoidHom.zero_comp]

Premises used: LinearMap.zero_apply, LinearMap.range_mkQ_comp, CharacterModule.dual_comp, LinearMap.comp_apply, AddMonoidHom.zero_comp, CharacterModule.dual_zero, CharacterModule.dual_apply
-- Module: Mathlib.Algebra.Module.CharacterModule
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'
⊢ Function.Injective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
      (⇑(dual f) : (a : CharacterModule A') → CharacterModule A) ↔
    Function.Surjective.{uA + 1, u_1 + 1} (α := A) (β := A') (⇑f : (a : A) → A')

Tactic:
⟨fun h ↦ surjective_of_dual_injective f h, fun h ↦ dual_injective_of_surjective f h⟩

Premises used: CharacterModule.dual_injective_of_surjective, CharacterModule.surjective_of_dual_injective, Iff.intro
-- Module: Mathlib.Algebra.Module.CharacterModule
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'
⊢ Function.Bijective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
      (⇑(dual f) : (a : CharacterModule A') → CharacterModule A) ↔
    Function.Bijective.{uA + 1, u_1 + 1} (α := A) (β := A') (⇑f : (a : A) → A')

Tactic:
⟨fun h ↦ ⟨dual_surjective_iff_injective.mp h.2, dual_injective_iff_surjective.mp h.1⟩,
  fun h ↦ ⟨dual_injective_iff_surjective.mpr h.2, dual_surjective_iff_injective.mpr h.1⟩⟩

Premises used: Iff.mpr, And.right, And.left, And.intro, Iff.intro, Iff.mp, CharacterModule.dual_surjective_iff_injective, CharacterModule.dual_injective_iff_surjective
-- Module: Mathlib.Algebra.Module.Congruence.Defs
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : AddZeroClass M
inst_1 : DistribSMul S M
r : M → M → Prop
hr : ∀ (s : S) {m m' : M}, r m m' → r (s • m) (s • m')
s : S
x x_1 : M
h : ((addConGen r).toSetoid : M → M → Prop) x x_1
⊢ ∀ (x y : M),
    (DistribSMul.toAddMonoidHom M s : (a : M) → M) (x + y) =
      HAdd.hAdd (α := M) (β := M) ((DistribSMul.toAddMonoidHom M s : (a : M) → M) x : M)
        ((DistribSMul.toAddMonoidHom M s : (a : M) → M) y : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Congruence.Defs
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
⊢ 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 ⊢

Premises used: Setoid.ker_def
-- Module: Mathlib.Algebra.Module.Congruence.Defs
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)
simp_rw : HSMul.hSMul (β := N) (φ r) ((f : (a : M) → N) x : N) = HSMul.hSMul (β := N) (φ r) ((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)

Tactic:
simp_rw [map_smulₛₗ, h]

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.Algebra.Module.Congruence.Defs
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : Semiring S
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module S M
inst_4 : Module S N
f : M →ₗ[S] N
hf : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
s : S
x : ModuleCon.Quotient M (ker f.toDistribMulActionHom)
a : M
⊢ (AddCon.quotientKerEquivOfSurjective f.toAddMonoidHom hf).toFun
      (HSMul.hSMul (β := ModuleCon.Quotient M (ker f.toDistribMulActionHom)) s
        (Quot.mk (⇑(ker f.toDistribMulActionHom).toSetoid : M → M → Prop) a)) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S)
      ((AddCon.quotientKerEquivOfSurjective f.toAddMonoidHom hf).toFun
        (Quot.mk (⇑(ker f.toDistribMulActionHom).toSetoid : M → M → Prop) a))

Tactic:
apply map_smul f

Premises used: map_smul
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
⊢ ∀ (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)
-- Module: Mathlib.Algebra.Module.DedekindDomain
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)
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) ⊤
⊢ 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)

Tactic:
apply torsionBySet_isInternal (p := fun p => p ^ P.count p) _

Premises used: Submodule.torsionBySet_isInternal
-- Module: Mathlib.Algebra.Module.DedekindDomain
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 : Set R)

Tactic:
hM
-- Module: Mathlib.Algebra.Module.DedekindDomain
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 : ⨅ i ∈ (factors I).toFinset, i ^ Multiset.count i P = I
⊢ Module.IsTorsionBySet R M (↑(⨅ i ∈ (factors I).toFinset, i ^ Multiset.count i P) : Set R)

Tactic:
convert! hM
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
h₂ : ∀ i ∈ (factors I).toFinset, ∀ j ∈ (factors I).toFinset, i ≠ j → i ≠ j
⊢ ⨅ i ∈ (factors I).toFinset, i ^ Multiset.count i P = I

Tactic:
rw [← Finset.inf_eq_iInf, IsDedekindDomain.inf_pow_eq_prod_of_prime,
      ← Finset.prod_multiset_count, ← associated_iff_eq]

Premises used: IsDedekindDomain.inf_pow_eq_prod_of_prime, associated_iff_eq, Finset.inf_eq_iInf, Finset.prod_multiset_count
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
⊢ Associated (factors I).prod I

Tactic:
factors_prod hI

Premises used: UniqueFactorizationMonoid.factors_prod
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
⊢ Associated (factors I).prod I

Tactic:
exact factors_prod hI

Premises used: UniqueFactorizationMonoid.factors_prod
-- Module: Mathlib.Algebra.Module.DedekindDomain
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, Prime i

Tactic:
prime_of_mem

Premises used: Set.Mem, setOf
-- Module: Mathlib.Algebra.Module.DedekindDomain
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, Prime i

Tactic:
exact prime_of_mem
-- Module: Mathlib.Algebra.Module.DedekindDomain
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, ∀ j ∈ (factors I).toFinset, i ≠ j → i ≠ j

Tactic:
fun _ _ _ _ ij => ij