awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this_1 : 0 < finrank.{0, u_1} ℤ ↥L
this_2 : ‖(↑t : E) - x‖ < 2⁻¹ * ‖t‖
this : ‖(↑t : E)‖ - 2⁻¹ * ‖(↑t : E)‖ < ‖x‖
⊢ Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t

Tactic:
simpa using show ‖t.1‖ ≤ 2 * ‖x‖ by linarith
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
n : ℤ
hn : n < -(↑(finrank.{0, u_1} ℤ ↥L) : ℤ)
x : E
⊢ Summable (α := ℝ) fun (z : ↥L) ↦ ‖(↑z : E) - x‖ ^ n

Tactic:
mod_cast summable_norm_sub_rpow L n (mod_cast hn) x

Premises used: Norm.norm, Int.cast, congrArg, Int.cast_neg_natCast._simp_1, HSub.hSub, cast, Membership.mem, Subtype, Int, funext, ZLattice.summable_norm_sub_rpow, LT.lt, Int.cast_lt._simp_1, congrFun', Summable, Eq.symm, Subtype.val, Real.rpow_intCast, Module.finrank, SummationFilter.unconditional, Eq.trans
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
n : ℤ
hn : n < -(↑(finrank.{0, u_1} ℤ ↥L) : ℤ)
⊢ Summable (α := ℝ) fun (z : ↥L) ↦ ‖z‖ ^ n

Tactic:
simpa using summable_norm_sub_zpow L n hn 0

Premises used: ZLattice.summable_norm_sub_zpow, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
n : ℕ
hn : finrank.{0, u_1} ℤ ↥L < n
x : E
⊢ LT.lt (α := ℤ) (-(↑n : ℤ)) (-(↑(finrank.{0, u_1} ℤ ↥L) : ℤ))

Tactic:
gcongr
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
n : ℕ
hn : finrank.{0, u_1} ℤ ↥L < n
x : E
⊢ Summable (α := ℝ) fun (z : ↥L) ↦ ‖(↑z : E) - x‖⁻¹ ^ n

Tactic:
simpa using summable_norm_sub_zpow L (-n) (by gcongr) x

Premises used: Nat.cast, ZLattice.summable_norm_sub_zpow, Neg.neg
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
n : ℕ
hn : finrank.{0, u_1} ℤ ↥L < n
⊢ Summable (α := ℝ) fun (z : ↥L) ↦ ‖z‖⁻¹ ^ n

Tactic:
simpa using summable_norm_sub_inv_pow L n hn 0

Premises used: ZLattice.summable_norm_sub_inv_pow, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : NeZero n
inst_1 : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
this : (c % n + c / n * n) • x = c • x
rwa : ∀ (this : (c % n) • x + (c / n * n) • x = c • x), (c % n) • x = c • x
rwa₁ : ∀ (this : (c % n) • x + n • (c / n) • x = c • x), (c % n) • x = c • x
rwa₂ : ∀ (this : (c % n) • x + 0 = c • x), (c % n) • x = c • x
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : (c % n) • x = c • x), (c % n) • x = c • x
⊢ (c % n) • x = c • x

Tactic:
rwa [add_nsmul, mul_nsmul, h, add_zero] at this

Premises used: mul_nsmul, add_zero, add_nsmul
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : NeZero n
inst_1 : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
suffices : (c % n + c / n * n) • x = c • x
⊢ (c % n) • x = c • x

Tactic:
suffices (c % n + c / n * n) • x = c • x by rwa [add_nsmul, mul_nsmul, h, add_zero] at this
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : NeZero n
inst_1 : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
rw rw₁ : c • x = c • x
⊢ (c % n + c / n * n) • x = c • x

Tactic:
rw [Nat.mod_add_div']

Premises used: Nat.mod_add_div'
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : NeZero n
inst_1 : AddCommMonoid M
h : ∀ (x : M), n • x = 0
⊢ ∀ (c : ℕ) (x : M), (c % n) • x = c • x

Tactic:
have h_mod (c : ℕ) (x : M) : (c % n) • x = c • x := by
    suffices (c % n + c / n * n) • x = c • x by rwa [add_nsmul, mul_nsmul, h, add_zero] at this
    rw [Nat.mod_add_div']
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : NeZero n
inst_1 : AddCommMonoid M
h : ∀ (x : M), n • x = 0
h_mod : ∀ (c : ℕ) (x : M), (c % n) • x = c • x
⊢ n ≠ 0

Tactic:
have := NeZero.ne n
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n_1 : ℕ
M : Type u_1
M₁ : Type u_2
inst : NeZero n_1
inst_1 : AddCommMonoid M
n : ℕ
h : ∀ (x : M), (n + 1) • x = 0
h_mod : ∀ (c : ℕ) (x : M), (c % (n + 1)) • x = c • x
this : n + 1 ≠ 0
⊢ Module (ZMod (n + 1)) M

Tactic:
exact {
    smul := fun (c : Fin _) x ↦ c.val • x
    smul_zero := fun _ ↦ nsmul_zero _
    zero_smul := fun _ ↦ zero_nsmul _
    smul_add := fun _ _ _ ↦ nsmul_add _ _ _
    one_smul := fun _ ↦ (h_mod _ _).trans <| one_nsmul _
    add_smul := fun _ _ _ ↦ (h_mod _ _).trans <| add_nsmul _ _ _
    mul_smul := fun _ _ _ ↦ (h_mod _ _).trans <| mul_nsmul' _ _ _
  }
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : NeZero n
inst_1 : AddCommMonoid M
h : ∀ (x : M), n • x = 0
h_mod : ∀ (c : ℕ) (x : M), (c % n) • x = c • x
this : n ≠ 0
⊢ Module (ZMod n) M

Tactic:
match n with
  | n + 1 => exact {
    smul := fun (c : Fin _) x ↦ c.val • x
    smul_zero := fun _ ↦ nsmul_zero _
    zero_smul := fun _ ↦ zero_nsmul _
    smul_add := fun _ _ _ ↦ nsmul_add _ _ _
    one_smul := fun _ ↦ (h_mod _ _).trans <| one_nsmul _
    add_smul := fun _ _ _ ↦ (h_mod _ _).trans <| add_nsmul _ _ _
    mul_smul := fun _ _ _ ↦ (h_mod _ _).trans <| mul_nsmul' _ _ _
  }
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
G : Type u_3
inst : AddCommGroup G
H : AddSubgroup G
hH : ∀ (x : G), n • x ∈ H
⊢ ∀ (x : G ⧸ H), n • x = 0

Tactic:
simpa [QuotientAddGroup.forall_mk, ← QuotientAddGroup.mk_nsmul]

Premises used: QuotientAddGroup.forall_mk, QuotientAddGroup.mk_nsmul
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
inst : AddCommGroup M
inst_1 : AddCommGroup M₁
inst_2 : FunLike F M M₁
inst_3 : AddMonoidHomClass F M M₁
inst_4 : Module (ZMod n) M
inst_5 : Module (ZMod n) M₁
f : F
c : ZMod n
x : M
rw :
  (f : (a : M) → M₁) (HSMul.hSMul (α := ZMod n) (↑c.cast : ZMod n) x) =
    HSMul.hSMul (α := ZMod n) (β := M₁) (↑c.cast : ZMod n) ((f : (a : M) → M₁) x : M₁)
⊢ (f : (a : M) → M₁) (c • x) = HSMul.hSMul (β := M₁) c ((f : (a : M) → M₁) x : M₁)

Tactic:
rw [← ZMod.intCast_zmod_cast c]

Premises used: ZMod.intCast_zmod_cast
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
inst : AddCommGroup M
inst_1 : AddCommGroup M₁
inst_2 : FunLike F M M₁
inst_3 : AddMonoidHomClass F M M₁
inst_4 : Module (ZMod n) M
inst_5 : Module (ZMod n) M₁
f : F
c : ZMod n
x : M
⊢ (f : (a : M) → M₁) (HSMul.hSMul (α := ZMod n) (↑c.cast : ZMod n) x) =
    HSMul.hSMul (α := ZMod n) (β := M₁) (↑c.cast : ZMod n) ((f : (a : M) → M₁) x : M₁)

Tactic:
map_intCast_smul f _ _ (cast c) x

Premises used: ZMod.cast, map_intCast_smul
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
inst : AddCommGroup M
inst_1 : AddCommGroup M₁
inst_2 : FunLike F M M₁
inst_3 : AddMonoidHomClass F M M₁
inst_4 : Module (ZMod n) M
inst_5 : Module (ZMod n) M₁
f : F
c : ZMod n
x : M
⊢ (f : (a : M) → M₁) (HSMul.hSMul (α := ZMod n) (↑c.cast : ZMod n) x) =
    HSMul.hSMul (α := ZMod n) (β := M₁) (↑c.cast : ZMod n) ((f : (a : M) → M₁) x : M₁)

Tactic:
exact map_intCast_smul f _ _ (cast c) x

Premises used: ZMod.cast, map_intCast_smul
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
S : Type u_4
inst : AddCommGroup M
inst_1 : Module (ZMod n) M
inst_2 : SetLike S M
inst_3 : AddSubgroupClass S M
x : M
K : S
hx : x ∈ K
c : ZMod n
rw : HSMul.hSMul (α := ℤ) c.cast x ∈ K
⊢ c • x ∈ K

Tactic:
rw [← ZMod.intCast_zmod_cast c, Int.cast_smul_eq_zsmul]

Premises used: ZMod.intCast_zmod_cast, Int.cast_smul_eq_zsmul
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
S : Type u_4
inst : AddCommGroup M
inst_1 : Module (ZMod n) M
inst_2 : SetLike S M
inst_3 : AddSubgroupClass S M
x : M
K : S
hx : x ∈ K
c : ZMod n
⊢ HSMul.hSMul (α := ℤ) c.cast x ∈ K

Tactic:
zsmul_mem hx (cast c)

Premises used: zsmul_mem, ZMod.cast
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
S : Type u_4
inst : AddCommGroup M
inst_1 : Module (ZMod n) M
inst_2 : SetLike S M
inst_3 : AddSubgroupClass S M
x : M
K : S
hx : x ∈ K
c : ZMod n
⊢ HSMul.hSMul (α := ℤ) c.cast x ∈ K

Tactic:
exact zsmul_mem hx (cast c)

Premises used: zsmul_mem, ZMod.cast
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : AddCommGroup M
inst_1 : AddCommGroup M₁
inst_2 : Module (ZMod n) M
inst_3 : Module (ZMod n) M₁
⊢ Function.Injective (α := M →+ M₁) (β := LinearMap (R := ZMod n) (RingHom.id (ZMod n)) M M₁) (toZModLinearMap n)

Tactic:
fun _ _ h ↦ ext fun x ↦ congr($h x)

Premises used: congrArg, id, AddMonoidHom.ext, Function.Injective, DFunLike.coe
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : AddCommGroup M
inst_1 : AddCommGroup M₁
inst_2 : Module (ZMod n) M
inst_3 : Module (ZMod n) M₁
f : M →+ M₁
⊢ Eq (α := (a : M) → M₁) (⇑(toZModLinearMap n f) : (a : M) → M₁) (⇑f : (a : M) → M₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
S : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₁
inst_2 : FunLike F M M₁
inst_3 : AddMonoidHomClass F M M₁
inst_4 : Module (ZMod n) M
inst_5 : Module (ZMod n) M₁
inst_6 : SetLike S M
inst_7 : AddSubgroupClass S M
x : M
K : S
f₁ f₂ : M →+ M₁
h :
  ∀ (x : M),
    Eq.{u_2 + 1} (α := M₁) ((toZModLinearMap n (f₁ + f₂) : (a : M) → M₁) x : M₁)
      ((HAdd.hAdd (α := LinearMap (R := ZMod n) (RingHom.id (ZMod n)) M M₁) (toZModLinearMap n f₁)
              (toZModLinearMap n f₂) :
            (a : M) → M₁)
          x :
        M₁)
⊢ toZModLinearMap n (f₁ + f₂) =
    HAdd.hAdd (α := LinearMap (R := ZMod n) (RingHom.id (ZMod n)) M M₁) (toZModLinearMap n f₁) (toZModLinearMap n f₂)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
S : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₁
inst_2 : FunLike F M M₁
inst_3 : AddMonoidHomClass F M M₁
inst_4 : Module (ZMod n) M
inst_5 : Module (ZMod n) M₁
inst_6 : SetLike S M
inst_7 : AddSubgroupClass S M
x : M
K : S
f₁ f₂ : M →+ M₁
x_1 : M
⊢ Eq.{u_2 + 1} (α := M₁) ((toZModLinearMap n (f₁ + f₂) : (a : M) → M₁) x_1 : M₁)
    ((HAdd.hAdd (α := LinearMap (R := ZMod n) (RingHom.id (ZMod n)) M M₁) (toZModLinearMap n f₁)
            (toZModLinearMap n f₂) :
          (a : M) → M₁)
        x_1 :
      M₁)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
inst : AddCommGroup M
inst_1 : Module (ZMod n) M
⊢ Eq.{u_1 + 1} (α := (a : Submodule (ZMod n) M) → AddSubgroup M)
    (⇑(OrderIso.symm (toZModSubmodule n)) : (a : Submodule (ZMod n) M) → AddSubgroup M) Submodule.toAddSubgroup

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
inst : AddCommGroup M
inst_1 : Module (ZMod n) M
S : AddSubgroup M
⊢ (↑((toZModSubmodule n : (a : AddSubgroup M) → Submodule (ZMod n) M) S : Submodule (ZMod n) M) : Set M) = (↑S : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
inst : AddCommGroup M
inst_1 : Module (ZMod n) M
x : M
S : AddSubgroup M
⊢ Membership.mem (γ := Submodule (ZMod n) M)
      ((toZModSubmodule n : (a : AddSubgroup M) → Submodule (ZMod n) M) S : Submodule (ZMod n) M) x ↔
    x ∈ S

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
inst : AddCommGroup M
inst_1 : Module (ZMod n) M
S : AddSubgroup M
⊢ Submodule.toAddSubgroup (R := ZMod n) (module_M := inst_1)
      ((toZModSubmodule n : (a : AddSubgroup M) → Submodule (ZMod n) M) S) =
    S

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
n : ℕ
M : Type u_1
inst : AddCommGroup M
inst_1 : Module (ZMod n) M
S : Submodule (ZMod n) M
⊢ (toZModSubmodule n : (a : AddSubgroup M) → Submodule (ZMod n) M) S.toAddSubgroup = S

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
p : ℕ
G : Type u_5
inst : AddCommGroup G
hp : Nat.Prime p
inst_1 : Module (ZMod p) G
H : Submodule (ZMod p) G
k : ℕ
hk : k ≤ Nat.card.{u_5} ↥H
h'k : k ≠ 0
obtain :
  ∀ (H'm : Subgroup (Multiplicative G))
    (H'mHm :
      H'm ≤
        (AddSubgroup.toSubgroup : (a : AddSubgroup G) → Subgroup (Multiplicative G))
          ((OrderIso.symm (AddSubgroup.toZModSubmodule p) : (a : Submodule (ZMod p) G) → AddSubgroup G) H))
    (H'mk : Nat.card.{u_5} ↥H'm ≤ k) (kH'm : k < p * Nat.card.{u_5} ↥H'm),
    ∃ (H' : Submodule (ZMod p) G), Nat.card.{u_5} ↥H' ≤ k ∧ k < p * Nat.card.{u_5} ↥H' ∧ H' ≤ H
⊢ ∃ (H' : Submodule (ZMod p) G), Nat.card.{u_5} ↥H' ≤ k ∧ k < p * Nat.card.{u_5} ↥H' ∧ H' ≤ H

Tactic:
obtain ⟨H'm, H'mHm, H'mk, kH'm⟩ := Sylow.exists_subgroup_le_card_le
    (H := AddSubgroup.toSubgroup ((AddSubgroup.toZModSubmodule _).symm H)) hp
      isPGroup_multiplicative hk h'k

Premises used: ZModModule.isPGroup_multiplicative, Sylow.exists_subgroup_le_card_le
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
p : ℕ
G : Type u_5
inst : AddCommGroup G
hp : Nat.Prime p
inst_1 : Module (ZMod p) G
H : Submodule (ZMod p) G
k : ℕ
hk : k ≤ Nat.card.{u_5} ↥H
h'k : k ≠ 0
H'm : Subgroup (Multiplicative G)
H'mHm :
  H'm ≤
    (AddSubgroup.toSubgroup : (a : AddSubgroup G) → Subgroup (Multiplicative G))
      ((OrderIso.symm (AddSubgroup.toZModSubmodule p) : (a : Submodule (ZMod p) G) → AddSubgroup G) H)
H'mk : Nat.card.{u_5} ↥H'm ≤ k
kH'm : k < p * Nat.card.{u_5} ↥H'm
⊢ ∃ (H' : Submodule (ZMod p) G), Nat.card.{u_5} ↥H' ≤ k ∧ k < p * Nat.card.{u_5} ↥H' ∧ H' ≤ H

Tactic:
⟨AddSubgroup.toZModSubmodule _ (AddSubgroup.toSubgroup.symm H'm), H'mk, kH'm, H'mHm⟩

Premises used: OrderIso.symm, AddSubgroup.toSubgroup, And.intro, Exists.intro, AddSubgroup.toZModSubmodule, DFunLike.coe
-- Module: Mathlib.Algebra.Module.ZMod
Goal:
p : ℕ
G : Type u_5
inst : AddCommGroup G
hp : Nat.Prime p
inst_1 : Module (ZMod p) G
H : Submodule (ZMod p) G
k : ℕ
hk : k ≤ Nat.card.{u_5} ↥H
h'k : k ≠ 0
H'm : Subgroup (Multiplicative G)
H'mHm :
  H'm ≤
    (AddSubgroup.toSubgroup : (a : AddSubgroup G) → Subgroup (Multiplicative G))
      ((OrderIso.symm (AddSubgroup.toZModSubmodule p) : (a : Submodule (ZMod p) G) → AddSubgroup G) H)
H'mk : Nat.card.{u_5} ↥H'm ≤ k
kH'm : k < p * Nat.card.{u_5} ↥H'm
⊢ ∃ (H' : Submodule (ZMod p) G), Nat.card.{u_5} ↥H' ≤ k ∧ k < p * Nat.card.{u_5} ↥H' ∧ H' ≤ H

Tactic:
exact ⟨AddSubgroup.toZModSubmodule _ (AddSubgroup.toSubgroup.symm H'm), H'mk, kH'm, H'mHm⟩
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
φ₁ φ₂ : R[M] →ₙₐ[R] A
h : ∀ (x : M), Eq.{u_4 + 1} (α := A) ((φ₁ : (a : R[M]) → A) (single x 1) : A) ((φ₂ : (a : R[M]) → A) (single x 1) : A)
⊢ φ₁ = φ₂

Tactic:
NonUnitalAlgHom.to_distribMulActionHom_injective <|
    Finsupp.distribMulActionHom_ext' fun a => DistribMulActionHom.ext_ring (h a)

Premises used: Finsupp.distribMulActionHom_ext', NonUnitalAlgHom.to_distribMulActionHom_injective, DistribMulActionHom.ext_ring
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
φ₁ φ₂ : R[M] →ₙₐ[R] A
h : φ₁.toMulHom.comp (ofMagma R M) = φ₂.toMulHom.comp (ofMagma R M)
⊢ φ₁ = φ₂

Tactic:
nonUnitalAlgHom_ext R <| DFunLike.congr_fun h

Premises used: DFunLike.congr_fun, MonoidAlgebra.nonUnitalAlgHom_ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
t' : R
a : R[M]
rw :
  Eq.{u_4 + 1} (α := A) (sum a fun (i : M) (c : R) ↦ HSMul.hSMul (β := A) (t' • c) ((f : (a : M) → A) i : A))
    (sum a fun (a : M) (b : R) ↦
      HSMul.hSMul (α := R) ((MonoidHom.id R : (a : R) → R) t' : R) (HSMul.hSMul (β := A) b ((f : (a : M) → A) a : A)))
rw₁ : ∀ (i : M), HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := A) 0 ((f : (a : M) → A) i : A) = 0
⊢ (sum (t' • a) fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A)) =
    HSMul.hSMul (α := R) (β := A) ((MonoidHom.id R : (a : R) → R) t' : R)
      (sum a fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A))

Tactic:
rw [Finsupp.smul_sum, sum_smul_index']

Premises used: Finsupp.sum_smul_index', Finsupp.smul_sum
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
t' : R
a : R[M]
simp_rw :
  Eq.{u_4 + 1} (α := A) (sum a fun (i : M) (c : R) ↦ t' • HSMul.hSMul (β := A) c ((f : (a : M) → A) i : A))
    (sum a fun (a : M) (b : R) ↦
      HSMul.hSMul (α := R) ((MonoidHom.id R : (a : R) → R) t' : R) (HSMul.hSMul (β := A) b ((f : (a : M) → A) a : A)))
⊢ Eq.{u_4 + 1} (α := A) (sum a fun (i : M) (c : R) ↦ HSMul.hSMul (β := A) (t' • c) ((f : (a : M) → A) i : A))
    (sum a fun (a : M) (b : R) ↦
      HSMul.hSMul (α := R) ((MonoidHom.id R : (a : R) → R) t' : R) (HSMul.hSMul (β := A) b ((f : (a : M) → A) a : A)))

Tactic:
simp_rw [smul_assoc, MonoidHom.id_apply]

Premises used: smul_assoc, MonoidHom.id_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
t' : R
a : R[M]
m : M
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := A) 0 ((f : (a : M) → A) m : A) = 0

Tactic:
zero_smul R (f m)

Premises used: zero_smul, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
t' : R
a : R[M]
m : M
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := A) 0 ((f : (a : M) → A) m : A) = 0

Tactic:
exact zero_smul R (f m)

Premises used: zero_smul, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
g : M → R → A := fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A)
m : M
⊢ g m 0 = 0

Tactic:
zero_smul R (f m)

Premises used: zero_smul, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
g : M → R → A := fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A)
m : M
⊢ g m 0 = 0

Tactic:
exact zero_smul R (f m)

Premises used: zero_smul, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
g : M → R → A := fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A)
⊢ ∀ (m : M), g m 0 = 0

Tactic:
have h₁ : ∀ m, g m 0 = 0 := by
          intro m
          exact zero_smul R (f m)
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
g : M → R → A := fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A)
h₁ : ∀ (m : M), g m 0 = 0
m : M
t₁ t₂ : R
rw rw₁ : g m (t₁ + t₂) = HSMul.hSMul (β := A) (t₁ + t₂) ((f : (a : M) → A) m : A)
⊢ g m (t₁ + t₂) = g m t₁ + g m t₂

Tactic:
rw [← add_smul]

Premises used: add_smul
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
g : M → R → A := fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A)
h₁ : ∀ (m : M), g m 0 = 0
⊢ ∀ (m : M) (t₁ t₂ : R), g m (t₁ + t₂) = g m t₁ + g m t₂

Tactic:
have h₂ : ∀ (m) (t₁ t₂ : R), g m (t₁ + t₂) = g m t₁ + g m t₂ := by
          intros
          rw [← add_smul]
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
g : M → R → A := fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A)
h₁ : ∀ (m : M), g m 0 = 0
h₂ : ∀ (m : M) (t₁ t₂ : R), g m (t₁ + t₂) = g m t₁ + g m t₂
simp_rw :
  Eq.{u_4 + 1} (α := A)
    (sum (sum a₁ fun (m₁ : M) (r₁ : R) ↦ sum a₂ fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
      fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A))
    (sum a₁ fun (x' : M) (v' : R) ↦
      sum a₂ fun (x : M) (v : R) ↦ HSMul.hSMul (β := A) (v' * v) ((f : (a : M) → A) (x' * x) : A))
⊢ (sum (a₁ * a₂) fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A)) =
    HMul.hMul (α := A) (sum a₁ fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A))
      (sum a₂ fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A))

Tactic:
simp_rw [Finsupp.mul_sum, Finsupp.sum_mul, smul_mul_smul_comm, ← f.map_mul, mul_def,
          sum_comm a₂ a₁]

Premises used: MonoidAlgebra.mul_def, Finsupp.sum_comm, smul_mul_smul_comm, Finsupp.mul_sum, MulHom.map_mul, Finsupp.sum_mul