awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.ZMod (goal)
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
⊢ c • x ∈ K
have rw : HSMul.hSMul (α := ℤ) c.cast x ∈ K
Tactic: rw [← ZMod.intCast_zmod_cast c, Int.cast_smul_eq_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZMod (goal)
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₁
⊢ toZModLinearMap n (f₁ + f₂) =
    HAdd.hAdd (α := LinearMap (R := ZMod n) (RingHom.id (ZMod n)) M M₁) (toZModLinearMap n f₁) (toZModLinearMap n f₂)
have 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₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.ZMod (goal)
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' : Submodule (ZMod p) G), Nat.card.{u_5} ↥H' ≤ k ∧ k < p * Nat.card.{u_5} ↥H' ∧ H' ≤ H
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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]
⊢ (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))
have 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)))
Tactic: rw [Finsupp.smul_sum, sum_smul_index']
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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)))
⊢ (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))
have rw₁ : ∀ (i : M), HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := A) 0 ((f : (a : M) → A) i : A) = 0
Tactic: rw [Finsupp.smul_sum, sum_smul_index']
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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]
⊢ 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)))
have 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)))
Tactic: simp_rw [smul_assoc, MonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (hypothesis)
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)
⊢ (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))
have h₁ : ∀ (m : M), g m 0 = 0
Tactic: have h₁ : ∀ m, g m 0 = 0 := by
          intro m
          exact zero_smul R (f m)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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₂
have rw : g m (t₁ + t₂) = HSMul.hSMul (β := A) (t₁ + t₂) ((f : (a : M) → A) m : A)
Tactic: rw [← add_smul]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (hypothesis)
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
⊢ (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))
have h₂ : ∀ (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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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₂
⊢ (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))
have 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))
Tactic: simp_rw [Finsupp.mul_sum, Finsupp.sum_mul, smul_mul_smul_comm, ← f.map_mul, mul_def,
          sum_comm a₂ a₁]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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₂
⊢ 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))
have rw : Eq.{u_4 + 1} (α := A) (sum a₁ fun (a : M) (b : R) ↦ sum (sum a₂ fun (m₂ : M) (r₂ : R) ↦ single (a * m₂) (b * r₂)) g)
  (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))
Tactic: rw [sum_sum_index h₁ h₂]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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₂
⊢ Eq.{u_4 + 1} (α := A) (sum a₁ fun (a : M) (b : R) ↦ sum (sum a₂ fun (m₂ : M) (r₂ : R) ↦ single (a * m₂) (b * r₂)) g)
    (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))
have e_g : Eq (α := M → R → A) (fun (a : M) (b : R) ↦ sum (sum a₂ fun (m₂ : M) (r₂ : R) ↦ single (a * m₂) (b * r₂)) g)
  fun (x' : M) (v' : R) ↦ sum a₂ fun (x : M) (v : R) ↦ HSMul.hSMul (β := A) (v' * v) ((f : (a : M) → A) (x' * x) : A)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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₂
⊢ Eq (α := M → R → A) (fun (a : M) (b : R) ↦ sum (sum a₂ fun (m₂ : M) (r₂ : R) ↦ single (a * m₂) (b * r₂)) g)
    fun (x' : M) (v' : R) ↦ sum a₂ fun (x : M) (v : R) ↦ HSMul.hSMul (β := A) (v' * v) ((f : (a : M) → A) (x' * x) : A)
have e_g : ∀ (x : M) (x_1 : R),
  sum (sum a₂ fun (m₂ : M) (r₂ : R) ↦ single (x * m₂) (x_1 * r₂)) g =
    sum a₂ fun (x_2 : M) (v : R) ↦ HSMul.hSMul (β := A) (x_1 * v) ((f : (a : M) → A) (x * x_2) : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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₂
x : M
x_1 : R
⊢ sum (sum a₂ fun (m₂ : M) (r₂ : R) ↦ single (x * m₂) (x_1 * r₂)) g =
    sum a₂ fun (x_2 : M) (v : R) ↦ HSMul.hSMul (β := A) (x_1 * v) ((f : (a : M) → A) (x * x_2) : A)
have e_g : Eq.{u_4 + 1} (α := A) (sum a₂ fun (a : M) (b : R) ↦ sum (single (x * a) (x_1 * b)) g)
  (sum a₂ fun (x_2 : M) (v : R) ↦ HSMul.hSMul (β := A) (x_1 * v) ((f : (a : M) → A) (x * x_2) : A))
Tactic: rw [sum_sum_index h₁ h₂]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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₂
x : M
x_1 : R
⊢ Eq.{u_4 + 1} (α := A) (sum a₂ fun (a : M) (b : R) ↦ sum (single (x * a) (x_1 * b)) g)
    (sum a₂ fun (x_2 : M) (v : R) ↦ HSMul.hSMul (β := A) (x_1 * v) ((f : (a : M) → A) (x * x_2) : A))
have e_g : Eq (α := M → R → A) (fun (a : M) (b : R) ↦ sum (single (x * a) (x_1 * b)) g) fun (x_2 : M) (v : R) ↦
  HSMul.hSMul (β := A) (x_1 * v) ((f : (a : M) → A) (x * x_2) : A)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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₂
x : M
x_1 : R
⊢ Eq (α := M → R → A) (fun (a : M) (b : R) ↦ sum (single (x * a) (x_1 * b)) g) fun (x_2 : M) (v : R) ↦
    HSMul.hSMul (β := A) (x_1 * v) ((f : (a : M) → A) (x * x_2) : A)
have e_g : ∀ (x_2 : M) (x_3 : R),
  sum (single (x * x_2) (x_1 * x_3)) g = HSMul.hSMul (β := A) (x_1 * x_3) ((f : (a : M) → A) (x * x_2) : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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₂
x : M
x_1 : R
x_2 : M
x_3 : R
⊢ sum (single (x * x_2) (x_1 * x_3)) g = HSMul.hSMul (β := A) (x_1 * x_3) ((f : (a : M) → A) (x * x_2) : A)
have e_g : g (x * x_2) (x_1 * x_3) = HSMul.hSMul (β := A) (x_1 * x_3) ((f : (a : M) → A) (x * x_2) : A)
Tactic: rw [sum_single_index (h₁ _)]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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
⊢ (fun (F : R[M] →ₙₐ[R] A) ↦ F.toMulHom.comp (ofMagma R M))
      ((fun (f : M →ₙ* A) ↦
          let __src : (M →₀ R) →+ A :=
            (liftAddHom : (a : M → R →+ A) → (M →₀ R) →+ A) fun (x : M) ↦
              (AddMonoidHom.flip (smulAddHom R A) : (a : A) → R →+ A) ((f : (a : M) → A) x);
          ({ toFun := fun (a : R[M]) ↦ sum a fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A),
              map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ } :
            R[M] →ₙₐ[R] A))
        f) =
    f
have h : ∀ (x : M),
  Eq.{u_4 + 1} (α := A)
    (((fun (F : R[M] →ₙₐ[R] A) ↦ F.toMulHom.comp (ofMagma R M))
            ((fun (f : M →ₙ* A) ↦
                let __src : (M →₀ R) →+ A :=
                  (liftAddHom : (a : M → R →+ A) → (M →₀ R) →+ A) fun (x : M) ↦
                    (AddMonoidHom.flip (smulAddHom R A) : (a : A) → R →+ A) ((f : (a : M) → A) x);
                ({
                    toFun := fun (a : R[M]) ↦
                      sum a fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A),
                    map_smul' := sorry, map_zero' := sorry, map_add' := sorry, map_mul' := sorry } :
                  R[M] →ₙₐ[R] A))
              f) :
          (a : M) → A)
        x :
      A)
    ((f : (a : M) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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 : R[M] →ₙₐ[R] A
⊢ (fun (f : M →ₙ* A) ↦
        let __src : (M →₀ R) →+ A :=
          (liftAddHom : (a : M → R →+ A) → (M →₀ R) →+ A) fun (x : M) ↦
            (AddMonoidHom.flip (smulAddHom R A) : (a : A) → R →+ A) ((f : (a : M) → A) x);
        ({ toFun := fun (a : R[M]) ↦ sum a fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A),
            map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ } :
          R[M] →ₙₐ[R] A))
      ((fun (F : R[M] →ₙₐ[R] A) ↦ F.toMulHom.comp (ofMagma R M)) F) =
    F
have h : ∀ (x : M),
  Eq.{u_4 + 1} (α := A)
    ((MulHom.comp (N := R[M])
            (NonUnitalAlgHom.toMulHom (R := R) (S := R) (φ := MonoidHom.id R)
              ((fun (f : M →ₙ* A) ↦
                  let __src : (M →₀ R) →+ A :=
                    (liftAddHom : (a : M → R →+ A) → (M →₀ R) →+ A) fun (x : M) ↦
                      (AddMonoidHom.flip (smulAddHom R A) : (a : A) → R →+ A) ((f : (a : M) → A) x);
                  ({
                      toFun := fun (a : R[M]) ↦
                        sum a fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A),
                      map_smul' := sorry, map_zero' := sorry, map_add' := sorry, map_mul' := sorry } :
                    R[M] →ₙₐ[R] A))
                ((fun (F : R[M] →ₙₐ[R] A) ↦ F.toMulHom.comp (ofMagma R M)) F)))
            (ofMagma R M) :
          (a : M) → A)
        x :
      A)
    ((F.toMulHom.comp (ofMagma R M) : (a : M) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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 : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
f : A[M]
⊢ HMul.hMul (α := A[M]) (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M]) f =
    HMul.hMul (β := A[M]) f (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M])
have hfg : ∀ (m : M),
  Eq.{u_4 + 1} (α := A)
    ((HMul.hMul (α := A[M]) (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M])
            f :
          (a : M) → A)
        m :
      A)
    ((HMul.hMul (β := A[M]) f
            (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M]) :
          (a : M) → A)
        m :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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 : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
f : A[M]
m : M
⊢ Eq.{u_4 + 1} (α := A)
    ((HMul.hMul (α := A[M]) (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M])
            f :
          (a : M) → A)
        m :
      A)
    ((HMul.hMul (β := A[M]) f
            (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M]) :
          (a : M) → A)
        m :
      A)
have hfg : Eq.{u_4 + 1} (α := A)
  ((HMul.hMul (α := A[M]) (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) f : (a : M) → A) m : A)
  ((HMul.hMul (β := A[M]) f (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) : (a : M) → A) m : A)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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 : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
f : A[M]
m : M
⊢ Eq.{u_4 + 1} (α := A)
    ((HMul.hMul (α := A[M]) (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) f : (a : M) → A) m : A)
    ((HMul.hMul (β := A[M]) f (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) : (a : M) → A) m : A)
have hfg : HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((f : (a : M) → A) m : A) =
  (HMul.hMul (β := A[M]) f (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) : (a : M) → A) m
Tactic: rw [single_one_mul_apply, mul_single_one_apply, Algebra.commutes]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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 : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
f : A[M]
m : M
hfg :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((f : (a : M) → A) m : A) =
    (HMul.hMul (β := A[M]) f (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) : (a : M) → A) m
⊢ Eq.{u_4 + 1} (α := A)
    ((HMul.hMul (α := A[M]) (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) f : (a : M) → A) m : A)
    ((HMul.hMul (β := A[M]) f (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) : (a : M) → A) m : A)
have hfg₁ : HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((f : (a : M) → A) m : A) =
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((algebraMap R A : (a : R) → A) r : A)
Tactic: rw [single_one_mul_apply, mul_single_one_apply, Algebra.commutes]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
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 : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
f : A[M]
m : M
hfg :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((f : (a : M) → A) m : A) =
    (HMul.hMul (β := A[M]) f (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) : (a : M) → A) m
hfg₁ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((f : (a : M) → A) m : A) =
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((algebraMap R A : (a : R) → A) r : A)
⊢ Eq.{u_4 + 1} (α := A)
    ((HMul.hMul (α := A[M]) (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) f : (a : M) → A) m : A)
    ((HMul.hMul (β := A[M]) f (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) : (a : M) → A) m : A)
have hfg₂ : HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((algebraMap R A : (a : R) → A) r : A) =
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((algebraMap R A : (a : R) → A) r : A)
Tactic: rw [single_one_mul_apply, mul_single_one_apply, Algebra.commutes]