awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
a b : k[G]
rw :
  support.{u₂, u₁} (M := k) (sum a fun (m₁ : G) (r₁ : k) ↦ sum b fun (m₂ : G) (r₂ : k) ↦ single (m₁ * m₂) (r₁ * r₂)) ⊆
    a.support * b.support
⊢ (a * b).support ⊆ a.support * b.support

Tactic:
rw [MonoidAlgebra.mul_def]

Premises used: MonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
a b : k[G]
⊢ support.{u₂, u₁} (M := k) (sum a fun (m₁ : G) (r₁ : k) ↦ sum b fun (m₂ : G) (r₂ : k) ↦ single (m₁ * m₂) (r₁ * r₂)) ⊆
    a.support * b.support

Tactic:
support_sum.trans <| biUnion_subset.2 fun _x hx ↦
    support_sum.trans <| biUnion_subset.2 fun _y hy ↦
      support_single_subset.trans <| singleton_subset_iff.2 <| mem_image₂_of_mem hx hy

Premises used: Iff.mpr, Set.Mem, setOf, Finset.singleton_subset_iff, HasSubset.Subset.trans, Finsupp.support_sum, Finset.mem_image₂_of_mem, MonoidAlgebra, Finset.biUnion_subset, Finsupp.support_single_subset
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
a b : k[G]
⊢ support.{u₂, u₁} (M := k) (sum a fun (m₁ : G) (r₁ : k) ↦ sum b fun (m₂ : G) (r₂ : k) ↦ single (m₁ * m₂) (r₁ * r₂)) ⊆
    a.support * b.support

Tactic:
exact support_sum.trans <| biUnion_subset.2 fun _x hx ↦
    support_sum.trans <| biUnion_subset.2 fun _y hy ↦
      support_single_subset.trans <| singleton_subset_iff.2 <| mem_image₂_of_mem hx hy

Premises used: Iff.mpr, Finset.singleton_subset_iff, HasSubset.Subset.trans, Finsupp.support_sum, Finset.mem_image₂_of_mem, Finset.biUnion_subset, Finsupp.support_single_subset
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
a : G
rw rw₁ : Subset (α := Finset G) (image (fun (b : G) ↦ a * b) f.support) (image (fun (b : G) ↦ a * b) f.support)
⊢ Subset (α := Finset G) (image₂ (fun (x1 x2 : G) ↦ x1 * x2) {a} f.support) (image (fun (x : G) ↦ a * x) f.support)

Tactic:
rw [Finset.image₂_singleton_left]

Premises used: Finset.image₂_singleton_left
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
a : G
rw rw₁ : Subset (α := Finset G) (image (fun (a_1 : G) ↦ a_1 * a) f.support) (image (fun (a_1 : G) ↦ a_1 * a) f.support)
⊢ Subset (α := Finset G) (image₂ (fun (x1 x2 : G) ↦ x1 * x2) f.support {a}) (image (fun (x : G) ↦ x * a) f.support)

Tactic:
rw [Finset.image₂_singleton_right]

Premises used: Finset.image₂_singleton_right
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
⊢ (single x r * f).support = image (fun (x_1 : G) ↦ x * x_1) f.support

Tactic:
subset_antisymm (support_single_mul_subset f _ _) fun y hy => ?_

Premises used: subset_antisymm, MonoidAlgebra.support_single_mul_subset
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
refine :
  ∀ (y : G) (hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x * x_1) f.support) y),
    y ∈ (single x r * f).support
⊢ (single x r * f).support = image (fun (x_1 : G) ↦ x * x_1) f.support

Tactic:
refine subset_antisymm (support_single_mul_subset f _ _) fun y hy => ?_

Premises used: subset_antisymm, MonoidAlgebra.support_single_mul_subset
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x * x_1) f.support) y
⊢ ∃ a ∈ f.support, x * a = y

Tactic:
grind
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x * x_1) f.support) y
obtain :
  ∀ (y : G) (yf : y ∈ f.support)
    (hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x * x_1) f.support) (x * y)),
    x * y ∈ (single x r * f).support
⊢ y ∈ (single x r * f).support

Tactic:
obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ x * a = y := by grind

Premises used: Finsupp.support, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
yf : y ∈ f.support
hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x * x_1) f.support) (x * y)
⊢ x * y ∈ (single x r * f).support

Tactic:
simp [mul_apply, mem_support_iff.mp yf, hr, lx.eq_iff]

Premises used: Finsupp.mem_support_iff, Function.Injective.eq_iff, MonoidAlgebra.mul_apply, Iff.mp
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
⊢ (f * single x r).support = image (fun (x_1 : G) ↦ x_1 * x) f.support

Tactic:
subset_antisymm (support_mul_single_subset f _ _) fun y hy => ?_

Premises used: subset_antisymm, MonoidAlgebra.support_mul_single_subset
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
refine :
  ∀ (y : G) (hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x_1 * x) f.support) y),
    y ∈ (f * single x r).support
⊢ (f * single x r).support = image (fun (x_1 : G) ↦ x_1 * x) f.support

Tactic:
refine subset_antisymm (support_mul_single_subset f _ _) fun y hy => ?_

Premises used: subset_antisymm, MonoidAlgebra.support_mul_single_subset
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x_1 * x) f.support) y
⊢ ∃ a ∈ f.support, a * x = y

Tactic:
grind
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x_1 * x) f.support) y
obtain :
  ∀ (y : G) (yf : y ∈ f.support)
    (hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x_1 * x) f.support) (y * x)),
    y * x ∈ (f * single x r).support
⊢ y ∈ (f * single x r).support

Tactic:
obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ a * x = y := by grind

Premises used: Finsupp.support, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
yf : y ∈ f.support
hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x_1 * x) f.support) (y * x)
⊢ y * x ∈ (f * single x r).support

Tactic:
simp only [mul_apply, mem_support_iff.mp yf, hr, mem_support_iff, sum_single_index,
    Finsupp.sum_ite_eq', Ne, not_false_iff, if_true, mul_zero, ite_self, rx.eq_iff]

Premises used: Finsupp.mem_support_iff, if_true, ite_self, Function.Injective.eq_iff, Finsupp.sum_ite_eq', Ne, MulZeroClass.mul_zero, MonoidAlgebra.mul_apply, Iff.mp, not_false_iff, MonoidAlgebra.sum_single_index
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : IsRightCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
h : ∀ (a : G), a ∈ (f * single x r).support ↔ a ∈ map (mulRightEmbedding x) f.support
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : IsRightCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x a : G
⊢ a ∈ (f * single x r).support ↔ a ∈ map (mulRightEmbedding x) f.support

Tactic:
simp only [support_mul_single_eq_image f hr (IsRightRegular.all x),
      mem_image, mem_map, mulRightEmbedding_apply]

Premises used: IsRightRegular.all, Finset.mem_image, MonoidAlgebra.support_mul_single_eq_image, mulRightEmbedding_apply, Finset.mem_map
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : IsRightCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
h : ∀ (a : G), a ∈ (f * single x r).support ↔ a ∈ map (mulRightEmbedding x) f.support
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support

Tactic:
classical
    ext
    simp only [support_mul_single_eq_image f hr (IsRightRegular.all x),
      mem_image, mem_map, mulRightEmbedding_apply]

Premises used: Finset.mem_image, mulRightEmbedding_apply, Finset.mem_map
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : IsLeftCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
h : ∀ (a : G), a ∈ (single x r * f).support ↔ a ∈ map (mulLeftEmbedding x) f.support
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : IsLeftCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x a : G
⊢ a ∈ (single x r * f).support ↔ a ∈ map (mulLeftEmbedding x) f.support

Tactic:
simp only [support_single_mul_eq_image f hr (IsLeftRegular.all x), mem_image,
      mem_map, mulLeftEmbedding_apply]

Premises used: Finset.mem_image, IsLeftRegular.all, MonoidAlgebra.support_single_mul_eq_image, Finset.mem_map, mulLeftEmbedding_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : IsLeftCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
h : ∀ (a : G), a ∈ (single x r * f).support ↔ a ∈ map (mulLeftEmbedding x) f.support
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support

Tactic:
classical
    ext
    simp only [support_single_mul_eq_image f hr (IsLeftRegular.all x), mem_image,
      mem_map, mulLeftEmbedding_apply]

Premises used: Finset.mem_image, Finset.mem_map, mulLeftEmbedding_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : One G
⊢ Subset.{u₂} (α := Finset G) (support.{u₂, u₁} (M := k) 1) 1

Tactic:
Finsupp.support_single_subset

Premises used: Set.Mem, setOf, Finsupp.support_single_subset
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : One G
inst_2 : NeZero.{u₁} (R := k) 1
⊢ Eq.{u₂ + 1} (α := Finset G) (support.{u₂, u₁} (M := k) 1) 1

Tactic:
Finsupp.support_single _ one_ne_zero

Premises used: Finsupp.support_single, one_ne_zero
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : MulOneClass G
f : k[G]
rw : Membership.mem (γ := Submodule k k[G]) (Finsupp.supported k k (↑f.support : Set G)) f
rw₁ rw₂ : (↑f.support : Set G) ⊆ (↑f.support : Set G)
⊢ Membership.mem (γ := Submodule k k[G]) (Submodule.span k ((fun (m : G) ↦ single m 1) '' (↑f.support : Set G))) f

Tactic:
rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported]

Premises used: Finsupp.mem_supported, Finsupp.supported_eq_span_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Support
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
f : k[G]
rw : Membership.mem (γ := Submodule k k[G]) (Finsupp.supported k k (↑f.support : Set G)) f
rw₁ rw₂ : (↑f.support : Set G) ⊆ (↑f.support : Set G)
⊢ Membership.mem (γ := Submodule k k[G]) (Submodule.span k ((fun (a : G) ↦ single a 1) '' (↑f.support : Set G))) f

Tactic:
rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported]

Premises used: Finsupp.mem_supported, Finsupp.supported_eq_span_single
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Semiring M
i : ι
m : M
⊢ Eq (α := ⨁ (x : ι), M) (toDirectSum (single i m))
    (((DirectSum.of.{u_1, u_3} (fun (x : ι) ↦ M) i : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) m)

Tactic:
Finsupp.toDFinsupp_single i m

Premises used: DFinsupp.single, Finsupp.toDFinsupp_single, AddMonoidAlgebra.toDirectSum, DirectSum
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Semiring M
inst_2 : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
⊢ Eq (α := AddMonoidAlgebra M ι)
    (toAddMonoidAlgebra (((of.{u_1, u_3} (fun (x : ι) ↦ M) i : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) m))
    (AddMonoidAlgebra.single i m)

Tactic:
DFinsupp.toFinsupp_single i m

Premises used: DFinsupp.single, DFinsupp.toFinsupp_single, DirectSum.toAddMonoidAlgebra, AddMonoidAlgebra
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Semiring M
inst_2 : (m : M) → Decidable (m ≠ 0)
f : M[ι]
⊢ f.toDirectSum.toAddMonoidAlgebra = f

Tactic:
Finsupp.toDFinsupp_toFinsupp f

Premises used: DirectSum.toAddMonoidAlgebra, Finsupp.toDFinsupp_toFinsupp, AddMonoidAlgebra, AddMonoidAlgebra.toDirectSum
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Semiring M
inst_2 : (m : M) → Decidable (m ≠ 0)
f : ⨁ (x : ι), M
⊢ f.toAddMonoidAlgebra.toDirectSum = f

Tactic:
(DFinsupp.toFinsupp_toDFinsupp (show Π₀ _ : ι, M from f) :)

Premises used: DFinsupp.toFinsupp_toDFinsupp, DirectSum.toAddMonoidAlgebra, AddMonoidAlgebra.toDirectSum, DirectSum
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : Semiring M
⊢ Eq (α := ⨁ (x : ι), M) (toDirectSum 0) 0

Tactic:
Finsupp.toDFinsupp_zero

Premises used: Finsupp.toDFinsupp_zero, AddMonoidAlgebra.toDirectSum, DirectSum
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : Semiring M
f g : M[ι]
⊢ (f + g).toDirectSum = f.toDirectSum + g.toDirectSum

Tactic:
Finsupp.toDFinsupp_add _ _

Premises used: Finsupp.toDFinsupp_add, AddMonoidAlgebra.toDirectSum, DirectSum
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
n : ℕ
⊢ Eq (α := ⨁ (x : ι), M) (toDirectSum (↑n : M[ι])) (↑n : ⨁ (x : ι), M)

Tactic:
Finsupp.toDFinsupp_single _ _

Premises used: DFinsupp.single, Finsupp.toDFinsupp_single, AddMonoidAlgebra.toDirectSum, DirectSum, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
n : ℕ
inst_3 : n.AtLeastTwo
⊢ Eq (α := ⨁ (x : ι), M) (toDirectSum (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
Finsupp.toDFinsupp_single _ _

Premises used: DFinsupp.single, Finsupp.toDFinsupp_single, AddMonoidAlgebra.toDirectSum, DirectSum, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : Ring M
f g : M[ι]
⊢ (f - g).toDirectSum = f.toDirectSum - g.toDirectSum

Tactic:
Finsupp.toDFinsupp_sub _ _

Premises used: Finsupp.toDFinsupp_sub, AddMonoidAlgebra.addAddCommGroup._aux_3, AddMonoidAlgebra.toDirectSum, DirectSum
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : Ring M
f : M[ι]
⊢ (-f).toDirectSum = -f.toDirectSum

Tactic:
Finsupp.toDFinsupp_neg _

Premises used: AddMonoidAlgebra.addAddCommGroup._aux_1, Finsupp.toDFinsupp_neg, AddMonoidAlgebra.toDirectSum, DirectSum
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Ring M
z : ℤ
⊢ Eq (α := ⨁ (x : ι), M) (toDirectSum (↑z : M[ι])) (↑z : ⨁ (x : ι), M)

Tactic:
Finsupp.toDFinsupp_single _ _

Premises used: DFinsupp.single, Finsupp.toDFinsupp_single, AddMonoidAlgebra.toDirectSum, DirectSum, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero ι
inst_2 : Semiring M
⊢ Eq (α := ⨁ (x : ι), M) (toDirectSum 1) 1

Tactic:
Finsupp.toDFinsupp_single _ _

Premises used: DFinsupp.single, Finsupp.toDFinsupp_single, AddMonoidAlgebra.toDirectSum, DirectSum, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
f g : M[ι]
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
change :
  (to_hom : (a : M[ι]) → ⨁ (x : ι), M) (f * g) =
    HMul.hMul (α := ⨁ (x : ι), M) (β := ⨁ (x : ι), M) ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) f : ⨁ (x : ι), M)
      ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) g : ⨁ (x : ι), M)
⊢ (f * g).toDirectSum = f.toDirectSum * g.toDirectSum

Tactic:
change to_hom (f * g) = to_hom f * to_hom g

Premises used: HMul.hMul, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
f g : M[ι]
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
revert :
  ∀ (f g : M[ι]),
    (to_hom : (a : M[ι]) → ⨁ (x : ι), M) (f * g) =
      HMul.hMul (α := ⨁ (x : ι), M) (β := ⨁ (x : ι), M) ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) f : ⨁ (x : ι), M)
        ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) g : ⨁ (x : ι), M)
⊢ (to_hom : (a : M[ι]) → ⨁ (x : ι), M) (f * g) =
    HMul.hMul (α := ⨁ (x : ι), M) (β := ⨁ (x : ι), M) ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) f : ⨁ (x : ι), M)
      ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) g : ⨁ (x : ι), M)

Tactic:
revert f g
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
rw : AddMonoidHom.compr₂ AddMonoidHom.mul to_hom = (AddMonoidHom.comp AddMonoidHom.mul to_hom).compl₂ to_hom
⊢ ∀ (f g : M[ι]),
    (to_hom : (a : M[ι]) → ⨁ (x : ι), M) (f * g) =
      HMul.hMul (α := ⨁ (x : ι), M) (β := ⨁ (x : ι), M) ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) f : ⨁ (x : ι), M)
        ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) g : ⨁ (x : ι), M)

Tactic:
rw [AddMonoidHom.map_mul_iff]

Premises used: AddMonoidHom.map_mul_iff
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
hfg :
  ∀ (xi : ι) (xv : M) (yi : ι) (yv : M),
    Eq (α := ⨁ (x : ι), M)
      ((AddMonoidHom.comp
              (((AddMonoidHom.compr₂ AddMonoidHom.mul to_hom).comp (singleAddHom xi) : (a : M) → M[ι] →+ ⨁ (x : ι), M)
                xv)
              (singleAddHom yi) :
            (a : M) → ⨁ (x : ι), M)
          yv :
        ⨁ (x : ι), M)
      ((AddMonoidHom.comp
              ((((AddMonoidHom.comp AddMonoidHom.mul to_hom).compl₂ to_hom).comp (singleAddHom xi) :
                  (a : M) → M[ι] →+ ⨁ (x : ι), M)
                xv)
              (singleAddHom yi) :
            (a : M) → ⨁ (x : ι), M)
          yv :
        ⨁ (x : ι), M)
⊢ AddMonoidHom.compr₂ AddMonoidHom.mul to_hom = (AddMonoidHom.comp AddMonoidHom.mul to_hom).compl₂ to_hom

Tactic:
ext xi xv yi yv : 4
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
xi : ι
xv : M
yi : ι
yv : M
⊢ Eq (α := ⨁ (x : ι), M)
    ((AddMonoidHom.comp
            (((AddMonoidHom.compr₂ AddMonoidHom.mul to_hom).comp (singleAddHom xi) : (a : M) → M[ι] →+ ⨁ (x : ι), M) xv)
            (singleAddHom yi) :
          (a : M) → ⨁ (x : ι), M)
        yv :
      ⨁ (x : ι), M)
    ((AddMonoidHom.comp
            ((((AddMonoidHom.comp AddMonoidHom.mul to_hom).compl₂ to_hom).comp (singleAddHom xi) :
                (a : M) → M[ι] →+ ⨁ (x : ι), M)
              xv)
            (singleAddHom yi) :
          (a : M) → ⨁ (x : ι), M)
        yv :
      ⨁ (x : ι), M)

Tactic:
simp [to_hom, AddMonoidAlgebra.single_mul_single, DirectSum.of_mul_of]

Premises used: DirectSum.of_mul_of, AddMonoidAlgebra.single_mul_single
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Semiring M
inst_2 : (m : M) → Decidable (m ≠ 0)
⊢ Eq (α := AddMonoidAlgebra M ι) (toAddMonoidAlgebra 0) 0

Tactic:
DFinsupp.toFinsupp_zero

Premises used: DirectSum.toAddMonoidAlgebra, AddMonoidAlgebra, DFinsupp.toFinsupp_zero
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Semiring M
inst_2 : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (f + g).toAddMonoidAlgebra = f.toAddMonoidAlgebra + g.toAddMonoidAlgebra

Tactic:
DFinsupp.toFinsupp_add _ _

Premises used: DFinsupp.toFinsupp_add, DirectSum.toAddMonoidAlgebra, AddMonoidAlgebra
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
inst_3 : (m : M) → Decidable (m ≠ 0)
n : ℕ
⊢ Eq (α := AddMonoidAlgebra M ι) (toAddMonoidAlgebra (↑n : ⨁ (x : ι), M)) (↑n : AddMonoidAlgebra M ι)

Tactic:
DFinsupp.toFinsupp_single _ _

Premises used: DFinsupp.single, DFinsupp.toFinsupp_single, DirectSum.toAddMonoidAlgebra, AddMonoidAlgebra, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
inst_3 : (m : M) → Decidable (m ≠ 0)
n : ℕ
inst_4 : n.AtLeastTwo
⊢ Eq (α := AddMonoidAlgebra M ι) (toAddMonoidAlgebra (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
DFinsupp.toFinsupp_single _ _

Premises used: DFinsupp.single, DFinsupp.toFinsupp_single, DirectSum.toAddMonoidAlgebra, AddMonoidAlgebra, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Ring M
inst_2 : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (f - g).toAddMonoidAlgebra = f.toAddMonoidAlgebra - g.toAddMonoidAlgebra

Tactic:
DFinsupp.toFinsupp_sub _ _

Premises used: DFinsupp.toFinsupp_sub, DirectSum.toAddMonoidAlgebra, AddMonoidAlgebra, AddMonoidAlgebra.addAddCommGroup._aux_3
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Ring M
inst_2 : (m : M) → Decidable (m ≠ 0)
f : ⨁ (x : ι), M
⊢ (-f).toAddMonoidAlgebra = -f.toAddMonoidAlgebra

Tactic:
DFinsupp.toFinsupp_neg _

Premises used: AddMonoidAlgebra.addAddCommGroup._aux_1, DirectSum.toAddMonoidAlgebra, AddMonoidAlgebra, DFinsupp.toFinsupp_neg
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Ring M
inst_3 : (m : M) → Decidable (m ≠ 0)
z : ℤ
⊢ Eq (α := AddMonoidAlgebra M ι) (toAddMonoidAlgebra (↑z : ⨁ (x : ι), M)) (↑z : AddMonoidAlgebra M ι)

Tactic:
DFinsupp.toFinsupp_single _ _

Premises used: DFinsupp.single, DFinsupp.toFinsupp_single, DirectSum.toAddMonoidAlgebra, AddMonoidAlgebra, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero ι
inst_2 : Semiring M
inst_3 : (m : M) → Decidable (m ≠ 0)
⊢ Eq (α := AddMonoidAlgebra M ι) (toAddMonoidAlgebra 1) 1

Tactic:
DFinsupp.toFinsupp_single _ _

Premises used: DFinsupp.single, DFinsupp.toFinsupp_single, DirectSum.toAddMonoidAlgebra, AddMonoidAlgebra, Finsupp.single