awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : One G
inst_1 : AddMonoidWithOne k
a : G →₀ k
⊢ { toFinsupp := a : SkewMonoidAlgebra k G } = 1 ↔ a = Finsupp.single 1 1

Tactic:
simp [← toFinsupp_inj]

Premises used: SkewMonoidAlgebra.toFinsupp_inj
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : One G
inst_1 : AddMonoidWithOne k
⊢ Eq (α := SkewMonoidAlgebra k G) (single 1 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : One G
inst_1 : AddMonoidWithOne k
⊢ Eq (α := SkewMonoidAlgebra k G) 1 (single 1 1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : One G
inst_1 : AddMonoidWithOne k
⊢ Eq.{u_1 + 1} (α := k) (coeff.{u_1, u_2} (G := G) 1 1) 1

Tactic:
simp only [coeff, toFinsupp_single, Finsupp.single_eq_same]

Premises used: Finsupp.single_eq_same, SkewMonoidAlgebra.toFinsupp_single, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : One G
inst_1 : AddMonoidWithOne k
a : G
inst_2 : Decidable (a = 1)
⊢ Eq.{u_1 + 1} (α := k) (coeff 1 a) (if a = 1 then 1 else 0)

Tactic:
simpa [eq_comm (a := a)] using coeff_single_apply

Premises used: eq_comm, SkewMonoidAlgebra.coeff_single_apply
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : One G
inst_1 : AddMonoidWithOne k
a : G
inst_2 : Decidable (a = 1)
⊢ Eq.{u_1 + 1} (α := k) (coeff 1 a) (if a = 1 then 1 else 0)

Tactic:
classical
  simpa [eq_comm (a := a)] using coeff_single_apply

Premises used: eq_comm, SkewMonoidAlgebra.coeff_single_apply
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : One G
inst_1 : AddMonoidWithOne k
n : ℕ
zero : Eq (α := SkewMonoidAlgebra k G) (↑0 : SkewMonoidAlgebra k G) (single 1 (↑0 : k))
succ :
  ∀ (n : ℕ),
    Eq (α := SkewMonoidAlgebra k G) (↑n : SkewMonoidAlgebra k G) (single 1 (↑n : k)) →
      Eq (α := SkewMonoidAlgebra k G) (↑(n + 1) : SkewMonoidAlgebra k G) (single 1 (↑(n + 1) : k))
⊢ Eq (α := SkewMonoidAlgebra k G) (↑n : SkewMonoidAlgebra k G) (single 1 (↑n : k))

Tactic:
induction n
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : One G
inst_1 : AddMonoidWithOne k
⊢ Eq (α := SkewMonoidAlgebra k G) (↑0 : SkewMonoidAlgebra k G) (single 1 (↑0 : k))

Tactic:
simp_all
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : One G
inst_1 : AddMonoidWithOne k
n : ℕ
h : Eq (α := SkewMonoidAlgebra k G) (↑n : SkewMonoidAlgebra k G) (single 1 (↑n : k))
⊢ Eq (α := SkewMonoidAlgebra k G) (↑(n + 1) : SkewMonoidAlgebra k G) (single 1 (↑(n + 1) : k))

Tactic:
simp_all
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : One G
inst_1 : AddMonoidWithOne k
n : ℕ
⊢ Eq (α := SkewMonoidAlgebra k G) (single 1 (↑n : k)) (↑n : SkewMonoidAlgebra k G)

Tactic:
(natCast_def _).symm

Premises used: SkewMonoidAlgebra.natCast_def, Eq.symm
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
N : Type u_3
inst_1 : AddCommMonoid N
f : SkewMonoidAlgebra k G
g : G → k → N
⊢ f.sum g = f.toFinsupp.sum g

Tactic:
rfl

Premises used: SkewMonoidAlgebra.sum, rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
N : Type u_3
inst_1 : AddCommMonoid N
f : SkewMonoidAlgebra k G
g : G → k → N
⊢ f.sum g = ∑ a ∈ f.support, g a (f.coeff a)

Tactic:
rfl

Premises used: Finsupp.sum, SkewMonoidAlgebra.support, SkewMonoidAlgebra.sum, rfl, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
N : Type u_3
inst_1 : AddCommMonoid N
a : G
b : k
h : G → k → N
h_zero : h a 0 = 0
⊢ sum (single a b) h = h a b

Tactic:
Finsupp.sum_single_index h_zero

Premises used: Finsupp.sum_single_index, SkewMonoidAlgebra.sum, Finsupp.single
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
N : Type u_3
P : Type u_4
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
H : Type u_5
inst_3 : FunLike H N P
inst_4 : AddMonoidHomClass H N P
h : H
f : SkewMonoidAlgebra k G
g : G → k → N
⊢ Eq.{u_4 + 1} (α := P) ((h : (a : N) → P) (f.sum g) : P) (f.sum fun (a : G) (b : k) ↦ (h : (a : N) → P) (g a b) : P)

Tactic:
_root_.map_sum h _ _

Premises used: Finsupp.sum, map_sum, SkewMonoidAlgebra.sum
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst_1 : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
⊢ (f.sum g).toFinsupp = f.toFinsupp.sum fun (x1 : G) (x2 : k) ↦ (g x1 x2).toFinsupp

Tactic:
_root_.map_sum toFinsuppAddEquiv (fun a ↦ g a (f.coeff a)) f.toFinsupp.support

Premises used: SkewMonoidAlgebra.toFinsuppAddEquiv, Finsupp.sum, Finsupp.support, map_sum, SkewMonoidAlgebra.toFinsupp, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst_1 : AddCommMonoid k'
f : G →₀ k
g : G → k → G' →₀ k'
a :
  { toFinsupp := f.sum g : SkewMonoidAlgebra k' G' }.toFinsupp =
    toFinsupp ({ toFinsupp := f : SkewMonoidAlgebra k G }.sum fun (x1 : G) (x2 : k) ↦ { toFinsupp := g x1 x2 })
⊢ { toFinsupp := f.sum g : SkewMonoidAlgebra k' G' } =
    { toFinsupp := f : SkewMonoidAlgebra k G }.sum fun (x1 : G) (x2 : k) ↦ { toFinsupp := g x1 x2 }

Tactic:
apply toFinsupp_injective

Premises used: SkewMonoidAlgebra.toFinsupp_injective
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst_1 : AddCommMonoid k'
f : G →₀ k
g : G → k → G' →₀ k'
⊢ { toFinsupp := f.sum g : SkewMonoidAlgebra k' G' }.toFinsupp =
    toFinsupp ({ toFinsupp := f : SkewMonoidAlgebra k G }.sum fun (x1 : G) (x2 : k) ↦ { toFinsupp := g x1 x2 })

Tactic:
simp only [toFinsupp_sum']

Premises used: SkewMonoidAlgebra.toFinsupp_sum'
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
f : SkewMonoidAlgebra k G
a : toFinsupp (f.sum single) = f.toFinsupp
⊢ f.sum single = f

Tactic:
apply toFinsupp_injective

Premises used: SkewMonoidAlgebra.toFinsupp_injective
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
f : SkewMonoidAlgebra k G
⊢ toFinsupp (f.sum single) = f.toFinsupp

Tactic:
simp only [toFinsupp_sum', toFinsupp_single, Finsupp.sum_single]

Premises used: SkewMonoidAlgebra.toFinsupp_single, Finsupp.sum_single, SkewMonoidAlgebra.toFinsupp_sum'
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
rw : f + g = { toFinsupp := f.toFinsupp : SkewMonoidAlgebra k G } + { toFinsupp := g.toFinsupp : SkewMonoidAlgebra k G }
rw₁ rw₂ : f + g = f + { toFinsupp := g.toFinsupp : SkewMonoidAlgebra k G }
⊢ f + g = { toFinsupp := f.toFinsupp + g.toFinsupp }

Tactic:
rw [ofFinsupp_add, eta]

Premises used: SkewMonoidAlgebra.eta, SkewMonoidAlgebra.ofFinsupp_add
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
rw : { toFinsupp := f.toFinsupp + g.toFinsupp : SkewMonoidAlgebra k G }.sum h = f.sum h + g.sum h
⊢ (f + g).sum h = f.sum h + g.sum h

Tactic:
rw [show f + g = ⟨f.toFinsupp + g.toFinsupp⟩ by rw [ofFinsupp_add, eta]]
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ { toFinsupp := f.toFinsupp + g.toFinsupp : SkewMonoidAlgebra k G }.sum h = f.sum h + g.sum h

Tactic:
Finsupp.sum_add_index' hf h_add

Premises used: Finsupp.sum_add_index', SkewMonoidAlgebra.sum
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ { toFinsupp := f.toFinsupp + g.toFinsupp : SkewMonoidAlgebra k G }.sum h = f.sum h + g.sum h

Tactic:
exact Finsupp.sum_add_index' hf h_add

Premises used: Finsupp.sum_add_index'
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : DecidableEq G
inst_2 : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
rw : f + g = { toFinsupp := f.toFinsupp : SkewMonoidAlgebra k G } + { toFinsupp := g.toFinsupp : SkewMonoidAlgebra k G }
rw₁ rw₂ : f + g = f + { toFinsupp := g.toFinsupp : SkewMonoidAlgebra k G }
⊢ f + g = { toFinsupp := f.toFinsupp + g.toFinsupp }

Tactic:
rw [ofFinsupp_add, eta]

Premises used: SkewMonoidAlgebra.eta, SkewMonoidAlgebra.ofFinsupp_add
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : DecidableEq G
inst_2 : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
rw : { toFinsupp := f.toFinsupp + g.toFinsupp : SkewMonoidAlgebra k G }.sum h = f.sum h + g.sum h
⊢ (f + g).sum h = f.sum h + g.sum h

Tactic:
rw [show f + g = ⟨f.toFinsupp + g.toFinsupp⟩ by rw [ofFinsupp_add, eta]]
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : DecidableEq G
inst_2 : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ { toFinsupp := f.toFinsupp + g.toFinsupp : SkewMonoidAlgebra k G }.sum h = f.sum h + g.sum h

Tactic:
Finsupp.sum_add_index h_zero h_add

Premises used: Finsupp.sum_add_index, SkewMonoidAlgebra.sum
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : DecidableEq G
inst_2 : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ { toFinsupp := f.toFinsupp + g.toFinsupp : SkewMonoidAlgebra k G }.sum h = f.sum h + g.sum h

Tactic:
exact Finsupp.sum_add_index h_zero h_add

Premises used: Finsupp.sum_add_index
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : AddCommMonoid S
p : SkewMonoidAlgebra k G
f g : G → k → S
⊢ (p.sum fun (n : G) (x : k) ↦ f n x + g n x) = p.sum f + p.sum g

Tactic:
Finsupp.sum_add

Premises used: Finsupp.sum_add, SkewMonoidAlgebra.sum
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : AddCommMonoid S
f : G → k → S
⊢ sum 0 f = 0

Tactic:
simp [sum]

Premises used: SkewMonoidAlgebra.sum
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
N : Type u_3
inst_1 : AddCommMonoid N
f : SkewMonoidAlgebra k G
⊢ Eq.{u_3 + 1} (α := N) (f.sum fun (x : G) (x_1 : k) ↦ 0) 0

Tactic:
Finset.sum_const_zero

Premises used: Finsupp.sum, Finset.sum_const_zero, SkewMonoidAlgebra.sum
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
f : SkewMonoidAlgebra M α
g : α → M → SkewMonoidAlgebra N β
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 0
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂
rw :
  Eq.{u_7 + 1} (α := P) (f.toFinsupp.sum fun (a : α) (b : M) ↦ (g a b).toFinsupp.sum h)
    (f.sum fun (a : α) (b : M) ↦ (g a b).sum h)
⊢ (f.sum g).sum h = f.sum fun (a : α) (b : M) ↦ (g a b).sum h

Tactic:
rw [sum_def, toFinsupp_sum' f g, Finsupp.sum_sum_index h_zero h_add]

Premises used: SkewMonoidAlgebra.sum_def, SkewMonoidAlgebra.toFinsupp_sum', Finsupp.sum_sum_index
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
f : SkewMonoidAlgebra M α
g : α → M → SkewMonoidAlgebra N β
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 0
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ Eq.{u_7 + 1} (α := P) (f.toFinsupp.sum fun (a : α) (b : M) ↦ (g a b).toFinsupp.sum h)
    (f.sum fun (a : α) (b : M) ↦ (g a b).sum h)

Tactic:
simp [sum_def]

Premises used: SkewMonoidAlgebra.sum_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst_1 : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
a₂ : G'
simp_rw :
  Eq.{u_3 + 1} (α := k') (((f.sum g).toFinsupp : (a : G') → k') a₂ : k')
    (f.sum fun (a₁ : G) (b : k) ↦ ((g a₁ b).toFinsupp : (a : G') → k') a₂ : k')
simp_rw₁ :
  Eq.{u_3 + 1} (α := k') ((f.toFinsupp.sum fun (x1 : G) (x2 : k) ↦ (g x1 x2).toFinsupp : (a : G') → k') a₂ : k')
    (f.sum fun (a₁ : G) (b : k) ↦ ((g a₁ b).toFinsupp : (a : G') → k') a₂ : k')
simp_rw₂ :
  Eq.{u_3 + 1} (α := k') ((f.toFinsupp.sum fun (x1 : G) (x2 : k) ↦ (g x1 x2).toFinsupp : (a : G') → k') a₂ : k')
    (f.toFinsupp.sum fun (a₁ : G) (b : k) ↦ ((g a₁ b).toFinsupp : (a : G') → k') a₂ : k')
⊢ (f.sum g).coeff a₂ = f.sum fun (a₁ : G) (b : k) ↦ (g a₁ b).coeff a₂

Tactic:
simp_rw [coeff, toFinsupp_sum', sum_def, Finsupp.sum_apply]

Premises used: SkewMonoidAlgebra.sum_def, Finsupp.sum_apply, SkewMonoidAlgebra.toFinsupp_sum', SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : NonUnitalNonAssocSemiring S
b : S
s : SkewMonoidAlgebra k G
f : G → k → S
⊢ s.sum f * b = s.sum fun (a : G) (c : k) ↦ f a c * b

Tactic:
simp only [sum, Finsupp.sum, Finset.sum_mul]

Premises used: Finsupp.sum, SkewMonoidAlgebra.sum, Finset.sum_mul
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : NonUnitalNonAssocSemiring S
b : S
s : SkewMonoidAlgebra k G
f : G → k → S
⊢ b * s.sum f = s.sum fun (a : G) (c : k) ↦ b * f a c

Tactic:
simp only [sum, Finsupp.sum, Finset.mul_sum]

Premises used: Finset.mul_sum, Finsupp.sum, SkewMonoidAlgebra.sum
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
N : Type u_3
inst_1 : AddCommMonoid N
inst_2 : DecidableEq G
f : SkewMonoidAlgebra k G
a : G
b : G → k → N
⊢ (f.sum fun (x : G) (v : k) ↦ if x = a then b x v else 0) = if a ∈ f.support then b a (f.coeff a) else 0

Tactic:
simp only [sum_def', f.toFinsupp.support.sum_ite_eq', support]

Premises used: SkewMonoidAlgebra.sum_def', Finset.sum_ite_eq', Finsupp.support, SkewMonoidAlgebra.toFinsupp, SkewMonoidAlgebra.support
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
M : Type u_3
R : Type u_4
inst_1 : AddCommMonoid M
inst_2 : DistribSMul R M
v : SkewMonoidAlgebra k G
c : R
h : G → k → M
⊢ c • v.sum h = v.sum fun (a : G) (b : k) ↦ c • h a b

Tactic:
Finsupp.smul_sum

Premises used: Finsupp.smul_sum, SkewMonoidAlgebra.sum
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
f : SkewMonoidAlgebra k G
M : Type u_3
inst_1 : AddCommMonoid M
g₁ g₂ : G → k → M
h : ∀ x ∈ f.support, g₁ x (f.coeff x) = g₂ x (f.coeff x)
⊢ f.sum g₁ = f.sum g₂

Tactic:
Finset.sum_congr rfl h

Premises used: Finsupp.sum, SkewMonoidAlgebra.sum, Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
p : SkewMonoidAlgebra k G → Prop
f : SkewMonoidAlgebra k G
zero : p 0
single : ∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)
add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)
rw : p (∑ a ∈ f.support, SkewMonoidAlgebra.single a (f.coeff a))
⊢ p f

Tactic:
rw [← sum_single f, sum_def']

Premises used: SkewMonoidAlgebra.sum_def', SkewMonoidAlgebra.sum_single
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
p : SkewMonoidAlgebra k G → Prop
f : SkewMonoidAlgebra k G
zero : p 0
single : ∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)
add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)
⊢ ∀ x ∈ f.support, p (SkewMonoidAlgebra.single x (f.coeff x))

Tactic:
simp_all
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
p : SkewMonoidAlgebra k G → Prop
f : SkewMonoidAlgebra k G
zero : p 0
single : ∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)
add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)
⊢ p (∑ a ∈ f.support, SkewMonoidAlgebra.single a (f.coeff a))

Tactic:
exact Finset.sum_induction _ _ add zero (by simp_all)

Premises used: Finset.sum_induction
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
instNonempty : Nonempty G
p : SkewMonoidAlgebra k G → Prop
f : SkewMonoidAlgebra k G
single : ∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)
add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)
⊢ p 0

Tactic:
simpa using single (Classical.choice instNonempty) 0

Premises used: Classical.choice, OfNat.ofNat
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
M : Type u_3
inst_1 : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h :
  ∀ (a : G) (b : k),
    Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
      ((g : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
h₁ :
  ∀ (p : SkewMonoidAlgebra k G),
    Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) p : M) ((g : (a : SkewMonoidAlgebra k G) → M) p : M)
⊢ f = g

Tactic:
ext p
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
M : Type u_3
inst_1 : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h :
  ∀ (a : G) (b : k),
    Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
      ((g : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
p : SkewMonoidAlgebra k G
h₁ : Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) 0 : M) ((g : (a : SkewMonoidAlgebra k G) → M) 0 : M)
h₂ :
  ∀ (g_1 : G) (a : k),
    Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) (single g_1 a) : M)
      ((g : (a : SkewMonoidAlgebra k G) → M) (single g_1 a) : M)
h₃ :
  ∀ (f_1 g_1 : SkewMonoidAlgebra k G),
    Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) f_1 : M)
        ((g : (a : SkewMonoidAlgebra k G) → M) f_1 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) g_1 : M)
          ((g : (a : SkewMonoidAlgebra k G) → M) g_1 : M) →
        Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) (f_1 + g_1) : M)
          ((g : (a : SkewMonoidAlgebra k G) → M) (f_1 + g_1) : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) p : M) ((g : (a : SkewMonoidAlgebra k G) → M) p : M)

Tactic:
induction p using SkewMonoidAlgebra.induction_on
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
M : Type u_3
inst_1 : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h :
  ∀ (a : G) (b : k),
    Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
      ((g : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) 0 : M) ((g : (a : SkewMonoidAlgebra k G) → M) 0 : M)

Tactic:
simp_all
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
M : Type u_3
inst_1 : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h :
  ∀ (a : G) (b : k),
    Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
      ((g : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
g_1 : G
a : k
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) (single g_1 a) : M)
    ((g : (a : SkewMonoidAlgebra k G) → M) (single g_1 a) : M)

Tactic:
simp_all
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
M : Type u_3
inst_1 : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h :
  ∀ (a : G) (b : k),
    Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
      ((g : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
f_1 g_1 : SkewMonoidAlgebra k G
h_1 :
  Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) f_1 : M) ((g : (a : SkewMonoidAlgebra k G) → M) f_1 : M)
h_2 :
  Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) g_1 : M) ((g : (a : SkewMonoidAlgebra k G) → M) g_1 : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) (f_1 + g_1) : M)
    ((g : (a : SkewMonoidAlgebra k G) → M) (f_1 + g_1) : M)

Tactic:
simp_all
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
G' : Type u_3
f : G → G'
v : SkewMonoidAlgebra k G
simp_rw : toFinsupp (v.sum fun (a : G) ↦ single (f a)) = Finsupp.mapDomain f v.toFinsupp
simp_rw₁ :
  Eq (α := G' →₀ k) (toFinsupp (v.sum fun (a : G) ↦ single (f a))) (v.toFinsupp.sum fun (a : G) ↦ Finsupp.single (f a))
simp_rw₂ :
  Eq (α := G' →₀ k) (v.toFinsupp.sum fun (x1 : G) (x2 : k) ↦ toFinsupp (single (f x1) x2))
    (v.toFinsupp.sum fun (a : G) ↦ Finsupp.single (f a))
⊢ toFinsupp ((mapDomain f : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k G') v) = Finsupp.mapDomain f v.toFinsupp

Tactic:
simp_rw [mapDomain_apply, Finsupp.mapDomain, toFinsupp_sum', single]

Premises used: Finsupp.mapDomain, SkewMonoidAlgebra.single, SkewMonoidAlgebra.mapDomain_apply, SkewMonoidAlgebra.toFinsupp_sum'
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
v : SkewMonoidAlgebra k G
⊢ (mapDomain id : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k G) v = v

Tactic:
sum_single _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, SkewMonoidAlgebra.sum_single, SkewMonoidAlgebra.sum, Finset.sum
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
G' : Type u_3
G'' : Type u_4
f : G → G'
g : G' → G''
v : SkewMonoidAlgebra k G
⊢ Eq (α := SkewMonoidAlgebra k G'')
    ((mapDomain (g ∘ f) : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k G'') v : SkewMonoidAlgebra k G'')
    ((mapDomain g : (a : SkewMonoidAlgebra k G') → SkewMonoidAlgebra k G'')
        ((mapDomain f : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k G') v) :
      SkewMonoidAlgebra k G'')

Tactic:
((sum_sum_index (single_zero <| g ·) (single_add <| g ·)).trans
    (sum_congr fun _ _ ↦ sum_single_index (single_zero _))).symm

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, SkewMonoidAlgebra.single_zero, SkewMonoidAlgebra.single_add, SkewMonoidAlgebra.sum_sum_index, SkewMonoidAlgebra.sum_congr, Eq.symm, SkewMonoidAlgebra.sum, Finset.sum, Eq.trans, SkewMonoidAlgebra.sum_single_index