awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
a : α
b : β
c : α₂
⊢ ∀ (b_1 : α₂) (m₁ m₂ : β),
    single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) b_1)
        (b * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) (m₁ + m₂)) =
      HAdd.hAdd (α := SkewMonoidAlgebra β α₂)
        (single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) b_1)
          (b * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) m₁))
        (single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) b_1)
          (b * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) m₂))

Tactic:
simp [smul_add, mul_add, single_add]

Premises used: SkewMonoidAlgebra.single_add, mul_add, smul_add
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
a : α
b : β
c : α₂
e_g :
  Eq.{u_5 + 1} (α := β)
    (coeff
      (y.sum fun (a₂ : α) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
      c)
    (coeff
      (y.sum fun (a_1 : α) (m : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a_1 : α₂))
          (b * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) m))
      c)
⊢ Eq.{u_5 + 1} (α := β)
    (coeff
      (y.sum fun (a₂ : α) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
      c)
    (coeff
      (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) a₂)
          (b * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) b₂))
      c)

Tactic:
rw [sum_mapDomain_index (by simp) (by simp [smul_add, mul_add, single_add])]

Premises used: SkewMonoidAlgebra.sum_mapDomain_index
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
a : α
b : β
c : α₂
⊢ Eq.{u_5 + 1} (α := β)
    (coeff
      (y.sum fun (a₂ : α) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
      c)
    (coeff
      (y.sum fun (a_1 : α) (m : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a_1 : α₂))
          (b * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) m))
      c)

Tactic:
simp_rw [hf]
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
⊢ Eq (α := SkewMonoidAlgebra β α₂)
    (x.sum fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
          (single (a * a₂) (b * a • b₂)))
    (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x)
      fun (a₁ : α₂) (b₁ : β) ↦
      sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))

Tactic:
have : (sum x fun a b ↦ sum y fun a₂ b₂ ↦ mapDomain (↑f) (single (a * a₂) (b * a • b₂))) =
      sum (mapDomain (↑f) x) fun a₁ b₁ ↦
        sum (mapDomain (↑f) y) fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂) := by
    simp_rw [mapDomain_single, map_mul]
    rw [sum_mapDomain_index (by simp) (by simp [add_mul, single_add, sum_add])]
    congr
    ext a b c
    rw [sum_mapDomain_index (by simp) (by simp [smul_add, mul_add, single_add])]
    simp_rw [hf]
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
this :
  Eq (α := SkewMonoidAlgebra β α₂)
    (x.sum fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
          (single (a * a₂) (b * a • b₂)))
    (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x)
      fun (a₁ : α₂) (b₁ : β) ↦
      sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
⊢ Eq (α := SkewMonoidAlgebra β α₂)
    (x.sum fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
          (single (a * a₂) (b * a • b₂)))
    (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x)
      fun (a₁ : α₂) (b₁ : β) ↦
      sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))

Tactic:
this
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
this :
  Eq (α := SkewMonoidAlgebra β α₂)
    (x.sum fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
          (single (a * a₂) (b * a • b₂)))
    (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x)
      fun (a₁ : α₂) (b₁ : β) ↦
      sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
h :
  ∀ (x : α) (x_1 : β),
    Eq (α := SkewMonoidAlgebra β α₂)
      ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
        (y.sum fun (a₂ : α) (b₂ : β) ↦ single (x * a₂) (x_1 * x • b₂)))
      (y.sum fun (a₂ : α) (b₂ : β) ↦
        (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
          (single (x * a₂) (x_1 * x • b₂)))
⊢ (x.sum fun (a : α) (b : β) ↦
      (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
        (y.sum fun (a₂ : α) (b₂ : β) ↦ single (a * a₂) (b * a • b₂))) =
    HMul.hMul (α := SkewMonoidAlgebra β α₂) (β := SkewMonoidAlgebra β α₂)
      ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x :
        SkewMonoidAlgebra β α₂)
      ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y :
        SkewMonoidAlgebra β α₂)

Tactic:
convert! this using 4
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
this :
  Eq (α := SkewMonoidAlgebra β α₂)
    (x.sum fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
          (single (a * a₂) (b * a • b₂)))
    (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x)
      fun (a₁ : α₂) (b₁ : β) ↦
      sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
x_1 : α
x_2 : β
h h₁ :
  Eq (α := SkewMonoidAlgebra β α₂)
    (y.sum fun (a : α) (b : β) ↦
      (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
        (single (x_1 * a) (x_2 * x_1 • b)))
    (y.sum fun (a₂ : α) (b₂ : β) ↦
      (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
        (single (x_1 * a₂) (x_2 * x_1 • b₂)))
⊢ Eq (α := SkewMonoidAlgebra β α₂)
    ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
      (y.sum fun (a₂ : α) (b₂ : β) ↦ single (x_1 * a₂) (x_2 * x_1 • b₂)))
    (y.sum fun (a₂ : α) (b₂ : β) ↦
      (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
        (single (x_1 * a₂) (x_2 * x_1 • b₂)))

Tactic:
rw [map_sum]

Premises used: SkewMonoidAlgebra.map_sum
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
a b : G
⊢ single (a * b) 1 = HMul.hMul (α := SkewMonoidAlgebra k G) (single a 1) (single b 1)

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
a : G
⊢ Eq (α := SkewMonoidAlgebra k G) ((of k G : (a : G) → SkewMonoidAlgebra k G) a : SkewMonoidAlgebra k G)
    (single a 1 : SkewMonoidAlgebra k G)

Tactic:
simp [of, MonoidHom.coe_mk, OneHom.coe_mk]

Premises used: SkewMonoidAlgebra.of, OneHom.coe_mk, MonoidHom.coe_mk
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
g : G
r : k
rw : HSMul.hSMul (β := SkewMonoidAlgebra k G) r (single g 1) = single g r
rw₁ : Eq (α := SkewMonoidAlgebra k G) (single g (HSMul.hSMul (β := k) r 1)) (single g r)
rw₂ : Eq (α := SkewMonoidAlgebra k G) (single g (r * 1)) (single g r)
rw₃ rw₄ : Eq (α := SkewMonoidAlgebra k G) (single g r) (single g r)
⊢ HSMul.hSMul (β := SkewMonoidAlgebra k G) r ((of k G : (a : G) → SkewMonoidAlgebra k G) g : SkewMonoidAlgebra k G) =
    single g r

Tactic:
rw [of_apply, smul_single, smul_eq_mul, mul_one]

Premises used: SkewMonoidAlgebra.of_apply, SkewMonoidAlgebra.smul_single, smul_eq_mul, mul_one
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
inst_3 : Nontrivial k
a b : G
h :
  Eq (α := SkewMonoidAlgebra k G) ((of k G : (a : G) → SkewMonoidAlgebra k G) a : SkewMonoidAlgebra k G)
    ((of k G : (a : G) → SkewMonoidAlgebra k G) b : SkewMonoidAlgebra k G)
⊢ Eq (α := G →₀ k) (toFinsupp (single a 1)) (toFinsupp (single b 1))

Tactic:
simp_rw [of_apply, ← toFinsupp_inj] at h

Premises used: SkewMonoidAlgebra.of_apply, SkewMonoidAlgebra.toFinsupp_inj
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
inst_3 : Nontrivial k
a b : G
h : Eq (α := G →₀ k) (toFinsupp (single a 1)) (toFinsupp (single b 1))
⊢ a = b

Tactic:
simpa using (Finsupp.single_eq_single_iff _ _ _ _).mp h

Premises used: Finsupp.single_eq_single_iff, Iff.mp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
f g : SkewMonoidAlgebra k G →+* k
h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom
h_of :
  Eq (α := G →* k) (MonoidHom.comp (↑f : SkewMonoidAlgebra k G →* k) (of k G))
    (MonoidHom.comp (↑g : SkewMonoidAlgebra k G →* k) (of k G))
⊢ f = g

Tactic:
ringHom_ext (RingHom.congr_fun h₁) (DFunLike.congr_fun h_of)

Premises used: DFunLike.congr_fun, RingHom.congr_fun, SkewMonoidAlgebra.ringHom_ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : MulOneClass G
R : Type u_3
inst_2 : Semiring R
f : k →+* R
g : G →* R
c : k
φ : SkewMonoidAlgebra k G
this :
  Eq (α := SkewMonoidAlgebra k G →+ R)
    (AddMonoidHom.comp (N := SkewMonoidAlgebra k G) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R))
      ((smulAddHom k (SkewMonoidAlgebra k G) : (a : k) → SkewMonoidAlgebra k G →+ SkewMonoidAlgebra k G) c))
    (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : k) → R) c)) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R)))
⊢ (liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : SkewMonoidAlgebra k G) → R) (c • φ) =
    HMul.hMul (α := R) (β := R) ((f : (a : k) → R) c : R)
      ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : SkewMonoidAlgebra k G) → R) φ : R)

Tactic:
simpa using congr($this φ)
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : MulOneClass G
R : Type u_3
inst_2 : Semiring R
f : k →+* R
g : G →* R
c : k
φ : SkewMonoidAlgebra k G
suffices :
  Eq (α := SkewMonoidAlgebra k G →+ R)
    (AddMonoidHom.comp (N := SkewMonoidAlgebra k G) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R))
      ((smulAddHom k (SkewMonoidAlgebra k G) : (a : k) → SkewMonoidAlgebra k G →+ SkewMonoidAlgebra k G) c))
    (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : k) → R) c)) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R)))
⊢ (liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : SkewMonoidAlgebra k G) → R) (c • φ) =
    HMul.hMul (α := R) (β := R) ((f : (a : k) → R) c : R)
      ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : SkewMonoidAlgebra k G) → R) φ : R)

Tactic:
suffices this :
    (liftNC ↑f g).comp (smulAddHom k (SkewMonoidAlgebra k G) c) =
      (AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f g) by simpa using congr($this φ)
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : MulOneClass G
R : Type u_3
inst_2 : Semiring R
f : k →+* R
g : G →* R
c : k
φ : SkewMonoidAlgebra k G
⊢ Eq (α := SkewMonoidAlgebra k G →+ R)
    (AddMonoidHom.comp (N := SkewMonoidAlgebra k G) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R))
      ((smulAddHom k (SkewMonoidAlgebra k G) : (a : k) → SkewMonoidAlgebra k G →+ SkewMonoidAlgebra k G) c))
    (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : k) → R) c)) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R)))

Tactic:
addHom_ext' fun a => AddMonoidHom.ext fun b => ?_

Premises used: AddMonoidHom.ext, SkewMonoidAlgebra.addHom_ext'
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : MulOneClass G
R : Type u_3
inst_2 : Semiring R
f : k →+* R
g : G →* R
c : k
φ : SkewMonoidAlgebra k G
refine :
  ∀ (a : G) (b : k),
    Eq.{u_3 + 1} (α := R)
      ((AddMonoidHom.comp
              (AddMonoidHom.comp (N := SkewMonoidAlgebra k G) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R))
                ((smulAddHom k (SkewMonoidAlgebra k G) : (a : k) → SkewMonoidAlgebra k G →+ SkewMonoidAlgebra k G) c))
              (singleAddHom a) :
            (a : k) → R)
          b :
        R)
      (((AddMonoidHom.comp
                (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : k) → R) c))
                  (liftNC (↑f : k →+ R) (⇑g : (a : G) → R)))
                (singleAddHom a) :
              k →+ R) :
            (a : k) → R)
          b :
        R)
⊢ Eq (α := SkewMonoidAlgebra k G →+ R)
    (AddMonoidHom.comp (N := SkewMonoidAlgebra k G) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R))
      ((smulAddHom k (SkewMonoidAlgebra k G) : (a : k) → SkewMonoidAlgebra k G →+ SkewMonoidAlgebra k G) c))
    (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : k) → R) c)) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R)))

Tactic:
refine addHom_ext' fun a => AddMonoidHom.ext fun b => ?_

Premises used: AddMonoidHom.ext, SkewMonoidAlgebra.addHom_ext'
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : MulOneClass G
R : Type u_3
inst_2 : Semiring R
f : k →+* R
g : G →* R
c : k
φ : SkewMonoidAlgebra k G
a : G
b : k
⊢ Eq.{u_3 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := SkewMonoidAlgebra k G) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R))
              ((smulAddHom k (SkewMonoidAlgebra k G) : (a : k) → SkewMonoidAlgebra k G →+ SkewMonoidAlgebra k G) c))
            (singleAddHom a) :
          (a : k) → R)
        b :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : k) → R) c)) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R)))
              (singleAddHom a) :
            k →+ R) :
          (a : k) → R)
        b :
      R)

Tactic:
simp [smul_single, mul_assoc]

Premises used: mul_assoc, SkewMonoidAlgebra.smul_single
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
inst_3 : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
⊢ t • a * b = t • (a * b)

Tactic:
Eq.trans (sum_smul_index' (g := a) (b := t) ?_) ?_

Premises used: SkewMonoidAlgebra.sum_smul_index', Eq.trans
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
inst_3 : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
refine_1 : ∀ (i : G), Eq (α := SkewMonoidAlgebra k G) (b.sum fun (a₂ : G) (b₂ : k) ↦ single (i * a₂) (0 * i • b₂)) 0
refine_2 :
  (a.sum fun (x1 : G) (x2 : k) ↦ b.sum fun (a₂ : G) (b₂ : k) ↦ single (x1 * a₂) (t • x2 * x1 • b₂)) = t • (a * b)
⊢ t • a * b = t • (a * b)

Tactic:
refine Eq.trans (sum_smul_index' (g := a) (b := t) ?_) ?_

Premises used: SkewMonoidAlgebra.sum_smul_index', Eq.trans
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
inst_3 : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
⊢ ∀ (i : G), Eq (α := SkewMonoidAlgebra k G) (b.sum fun (a₂ : G) (b₂ : k) ↦ single (i * a₂) (0 * i • b₂)) 0

Tactic:
simp only [← smul_sum, smul_mul_assoc, ← smul_single,
        zero_mul, imp_true_iff, sum_zero, single_zero]

Premises used: MulZeroClass.zero_mul, SkewMonoidAlgebra.single_zero, smul_mul_assoc, SkewMonoidAlgebra.smul_single, imp_true_iff, SkewMonoidAlgebra.smul_sum, SkewMonoidAlgebra.sum_zero
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
inst_3 : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
refine_2 :
  HSMul.hSMul (β := SkewMonoidAlgebra k G) t
      (a.sum fun (a : G) (b_1 : k) ↦ b.sum fun (a_1 : G) (b : k) ↦ single (a * a_1) (b_1 * a • b)) =
    t • (a * b)
⊢ (a.sum fun (x1 : G) (x2 : k) ↦ b.sum fun (a₂ : G) (b₂ : k) ↦ single (x1 * a₂) (t • x2 * x1 • b₂)) = t • (a * b)

Tactic:
simp only [← smul_sum, smul_mul_assoc, ← smul_single,
        zero_mul, imp_true_iff, sum_zero, single_zero]

Premises used: MulZeroClass.zero_mul, SkewMonoidAlgebra.single_zero, smul_mul_assoc, SkewMonoidAlgebra.smul_single, imp_true_iff, SkewMonoidAlgebra.smul_sum, SkewMonoidAlgebra.sum_zero
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
inst_3 : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
⊢ HSMul.hSMul (β := SkewMonoidAlgebra k G) t
      (a.sum fun (a : G) (b_1 : k) ↦ b.sum fun (a_1 : G) (b : k) ↦ single (a * a_1) (b_1 * a • b)) =
    t • (a * b)

Tactic:
rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
inst_3 : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
simp : t • a * b = t • (a * b)
refine_2 refine_2₁ :
  HSMul.hSMul (β := SkewMonoidAlgebra k G) t
      (a.sum fun (a : G) (b_1 : k) ↦ b.sum fun (a_1 : G) (b : k) ↦ single (a * a_1) (b_1 * a • b)) =
    t • (a * b)
⊢ (t • a) • b = t • a • b

Tactic:
classical
    simp only [smul_eq_mul]
    refine Eq.trans (sum_smul_index' (g := a) (b := t) ?_) ?_ <;>
      simp only [← smul_sum, smul_mul_assoc, ← smul_single,
        zero_mul, imp_true_iff, sum_zero, single_zero]; rfl

Premises used: MulZeroClass.zero_mul, SkewMonoidAlgebra.sum_smul_index', SkewMonoidAlgebra.single_zero, smul_mul_assoc, SkewMonoidAlgebra.smul_single, imp_true_iff, SkewMonoidAlgebra.smul_sum, smul_eq_mul, SkewMonoidAlgebra.sum_zero, Eq.trans
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k_1 : Type u_1
G : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : DistribMulAction R M
α : Type u_6
a : α
k : R
m : M
⊢ ZeroHom.toFun (↑(singleAddHom a) : ZeroHom M (SkewMonoidAlgebra M α)) (k • m) =
    HSMul.hSMul (α := R) (β := SkewMonoidAlgebra M α) ((MonoidHom.id R : (a : R) → R) k : R)
      (ZeroHom.toFun (↑(singleAddHom a) : ZeroHom M (SkewMonoidAlgebra M α)) m)

Tactic:
simp [singleAddHom, smul_single, MonoidHom.id_apply]

Premises used: SkewMonoidAlgebra.smul_single, SkewMonoidAlgebra.singleAddHom, MonoidHom.id_apply
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : DistribMulAction R M
inst_4 : DistribMulAction R N
α : Type u_6
f g : SkewMonoidAlgebra M α →+[R] N
h :
  ∀ (a : α) (m : M),
    Eq.{u_5 + 1} (α := N) ((f : (a : SkewMonoidAlgebra M α) → N) (single a m) : N)
      ((g : (a : SkewMonoidAlgebra M α) → N) (single a m) : N)
⊢ f = g

Tactic:
DistribMulActionHom.toAddMonoidHom_injective <| addHom_ext h

Premises used: DistribMulActionHom.toAddMonoidHom_injective, SkewMonoidAlgebra.addHom_ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : DistribMulAction R M
inst_4 : DistribMulAction R N
α : Type u_6
f g : SkewMonoidAlgebra M α →+[R] N
h : ∀ (a : α), f.comp (DistribMulActionHom.single a) = g.comp (DistribMulActionHom.single a)
⊢ f = g

Tactic:
distribMulActionHom_ext fun a ↦ DistribMulActionHom.congr_fun (h a)

Premises used: DistribMulActionHom.congr_fun, SkewMonoidAlgebra.distribMulActionHom_ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
α : Type u_6
inst_3 : Module R M
inst_4 : Module R N
φ ψ : SkewMonoidAlgebra M α →ₗ[R] N
h :
  ∀ (a : α) (b : M),
    Eq.{u_5 + 1} (α := N) ((φ : (a : SkewMonoidAlgebra M α) → N) (single a b) : N)
      ((ψ : (a : SkewMonoidAlgebra M α) → N) (single a b) : N)
⊢ φ = ψ

Tactic:
LinearMap.toAddMonoidHom_injective <| addHom_ext h

Premises used: LinearMap.toAddMonoidHom_injective, SkewMonoidAlgebra.addHom_ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
α : Type u_6
inst_3 : Module R M
inst_4 : Module R N
φ ψ : SkewMonoidAlgebra M α →ₗ[R] N
h : ∀ (a : α), φ ∘ₗ lsingle a = ψ ∘ₗ lsingle a
⊢ φ = ψ

Tactic:
lhom_ext fun a ↦ LinearMap.congr_fun (h a)

Premises used: LinearMap.congr_fun, SkewMonoidAlgebra.lhom_ext