awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
change : Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔ x ∈ RHS
⊢ Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔
    ∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'

Tactic:
change _ ↔ x ∈ RHS
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
mp : Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x → x ∈ RHS
mpr : x ∈ RHS → Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x
⊢ Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔ x ∈ RHS

Tactic:
constructor
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
mp : Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s) ≤ RHS
⊢ Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x → x ∈ RHS

Tactic:
suffices Ideal.span (⇑(of k G) '' s) ≤ RHS from @this x
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
mp : (⇑(of k G) : (a : G) → k[G]) '' s ⊆ (↑RHS : Set k[G])
⊢ Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s) ≤ RHS

Tactic:
rw [Ideal.span_le]

Premises used: Ideal.span_le
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
i : G
hi : i ∈ s
m : G
hm : Membership.mem (γ := Finset G) (Finsupp.support.{u_3, u_1} (M := k) ((of k G : (a : G) → k[G]) i)) m
⊢ ∃ m' ∈ s, ∃ (d : G), m = d * m'

Tactic:
⟨_, hi, 1, ?_⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
i : G
hi : i ∈ s
m : G
hm : Membership.mem (γ := Finset G) (Finsupp.support.{u_3, u_1} (M := k) ((of k G : (a : G) → k[G]) i)) m
mp : m = 1 * i
⊢ ∃ m' ∈ s, ∃ (d : G), m = d * m'

Tactic:
refine ⟨_, hi, 1, ?_⟩
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
i : G
hi : i ∈ s
m : G
hm : Membership.mem (γ := Finset G) (Finsupp.support.{u_3, u_1} (M := k) ((of k G : (a : G) → k[G]) i)) m
⊢ m = 1 * i

Tactic:
simpa using Finsupp.support_single_subset hm

Premises used: Finsupp.support_single_subset
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
hx : x ∈ RHS
mpr : Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) (Finsupp.sum x Finsupp.single)
⊢ Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x

Tactic:
rw [← Finsupp.sum_single x]

Premises used: Finsupp.sum_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
hx : x ∈ RHS
apply :
  ∀ (i : G) (hi : i ∈ x.support),
    Membership.mem (α := k[G]) (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s))
      (Finsupp.single i ((x : (a : G) → k) i) : G →₀ k)
⊢ Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) (Finsupp.sum x Finsupp.single)

Tactic:
apply Ideal.sum_mem _ fun i hi ↦ ?_

Premises used: Ideal.sum_mem
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
hx : x ∈ RHS
i : G
hi : i ∈ x.support
obtain :
  ∀ (d : G) (hd : d ∈ s) (d2 : G) (hi : d2 * d ∈ x.support),
    Membership.mem (α := k[G]) (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s))
      (Finsupp.single (d2 * d) ((x : (a : G) → k) (d2 * d)) : G →₀ k)
⊢ Membership.mem (α := k[G]) (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s))
    (Finsupp.single i ((x : (a : G) → k) i) : G →₀ k)

Tactic:
obtain ⟨d, hd, d2, rfl⟩ := hx _ hi

Premises used: rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
hx : x ∈ RHS
d : G
hd : d ∈ s
d2 : G
hi : d2 * d ∈ x.support
⊢ Membership.mem (α := k[G]) (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s))
    (Finsupp.single (d2 * d) ((x : (a : G) → k) (d2 * d)) : G →₀ k)

Tactic:
simpa using Ideal.mul_mem_left _ (.single d2 <| x (d2 * d)) (b := of k G d)
      (Ideal.subset_span <| Set.mem_image_of_mem _ hd)

Premises used: Ideal.subset_span, Set.mem_image_of_mem, Ideal.mul_mem_left
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
let let₁ let₂ :
  Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔
    ∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'
let₃ :
  let RHS : Ideal k[G] :=
    { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
      smul_mem' := ⋯ };
  Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔ x ∈ RHS
mp :
  let RHS : Ideal k[G] :=
    { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
      smul_mem' := ⋯ };
  Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x → x ∈ RHS
mpr mpr₁ :
  let RHS : Ideal k[G] :=
    { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
      smul_mem' := ⋯ };
  x ∈ RHS → Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x
⊢ Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔
    ∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'

Tactic:
classical
  let RHS : Ideal (MonoidAlgebra k G) :=
    { carrier := { p | ∀ m : G, m ∈ p.support → ∃ m' ∈ s, ∃ d, m = d * m' }
      add_mem' {x y} hx hy m hm := (Finset.mem_union.1 <| Finsupp.support_add hm).elim (hx m) (hy m)
      zero_mem' := by simp
      smul_mem' x y hy m hm := by
        simp only [smul_eq_mul, mul_def] at hm
        obtain ⟨xm, -, hm⟩ := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
        obtain ⟨ym, hym, hm⟩ := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
        obtain rfl := Finset.mem_singleton.mp (Finsupp.support_single_subset hm)
        refine (hy _ hym).imp fun sm p => And.imp_right ?_ p
        rintro ⟨d, rfl⟩
        exact ⟨xm * d, (mul_assoc _ _ _).symm⟩ }
  change _ ↔ x ∈ RHS
  constructor
  · suffices Ideal.span (⇑(of k G) '' s) ≤ RHS from @this x
    rw [Ideal.span_le]
    rintro _ ⟨i, hi, rfl⟩ m hm
    refine ⟨_, hi, 1, ?_⟩
    simpa using Finsupp.support_single_subset hm
  · intro hx
    rw [← Finsupp.sum_single x]
    apply Ideal.sum_mem _ fun i hi ↦ ?_
    obtain ⟨d, hd, d2, rfl⟩ := hx _ hi
    simpa using Ideal.mul_mem_left _ (.single d2 <| x (d2 * d)) (b := of k G d)
      (Ideal.subset_span <| Set.mem_image_of_mem _ hd)

Premises used: Ideal.span_le, Ideal.sum_mem, Finsupp.sum_single, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
A : Type u_2
inst : AddMonoid A
inst_1 : Semiring k
s : Set A
x : k[A]
⊢ Membership.mem (γ := Ideal k[A]) (Ideal.span (of' k A '' s)) x ↔ ∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : A), m = d + m'

Tactic:
@MonoidAlgebra.mem_ideal_span_of_image k (Multiplicative A) _ _ _ _

Premises used: Set.Mem, setOf, Multiplicative, MonoidAlgebra.mem_ideal_span_of_image, AddMonoidAlgebra, AddMonoidAlgebra.of', Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Lift
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : NonUnitalNonAssocSemiring R
f : k →+ R
g : G → R
a : G
b : k
⊢ (liftNC f g : (a : k[G]) → R) (single a b) = HMul.hMul (α := R) ((f : (a : k) → R) b : R) (g a)

Tactic:
liftAddHom_apply_single _ _ _

Premises used: Finsupp.liftAddHom_apply_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Lift
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : Semiring R
g_hom : Type u_6
inst_3 : FunLike g_hom G R
inst_4 : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm :
  ∀ {x y : G},
    y ∈ a.support → Commute.{u_2} (S := R) ((f : (a : k) → R) ((b : (a : G) → k) x : k) : R) ((g : (a : G) → R) y : R)
rw :
  HMul.hMul (α := R) (β := R) ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (sum a single) : R)
    ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (sum b single) : R)
| HMul.hMul (α := R) (β := R) ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) a : R)
    ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) b : R)

Tactic:
rw [← sum_single a, ← sum_single b]

Premises used: MonoidAlgebra.sum_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Lift
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : Semiring R
g_hom : Type u_6
inst_3 : FunLike g_hom G R
inst_4 : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm :
  ∀ {x y : G},
    y ∈ a.support → Commute.{u_2} (S := R) ((f : (a : k) → R) ((b : (a : G) → k) x : k) : R) ((g : (a : G) → R) y : R)
conv_rhs :
  (liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (a * b) =
    HMul.hMul (α := R) (β := R) ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (sum a single) : R)
      ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (sum b single) : R)
⊢ (liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (a * b) =
    HMul.hMul (α := R) (β := R) ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) a : R)
      ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) b : R)

Tactic:
conv_rhs => rw [← sum_single a, ← sum_single b]

Premises used: MonoidAlgebra.sum_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Lift
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : Semiring R
g_hom : Type u_6
inst_3 : FunLike g_hom G R
inst_4 : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm :
  ∀ {x y : G},
    y ∈ a.support → Commute.{u_2} (S := R) ((f : (a : k) → R) ((b : (a : G) → k) x : k) : R) ((g : (a : G) → R) y : R)
simp_rw :
  Eq.{u_2 + 1} (α := R)
    (sum a fun (a : G) (b_1 : k) ↦
      sum b fun (a_1 : G) (b : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (b_1 * b) : R) ((g : (a : G) → R) (a * a_1) : R))
    (sum a fun (a : G) (c : k) ↦
      sum b fun (a_1 : G) (c_1 : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c : R) ((g : (a : G) → R) a : R) *
          HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c_1 : R) ((g : (a : G) → R) a_1 : R))
⊢ (liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (a * b) =
    HMul.hMul (α := R) (β := R) ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (sum a single) : R)
      ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (sum b single) : R)

Tactic:
simp_rw [mul_def, map_finsuppSum, liftNC_single, Finsupp.sum_mul, Finsupp.mul_sum]

Premises used: MonoidAlgebra.mul_def, MonoidAlgebra.liftNC_single, map_finsuppSum, Finsupp.mul_sum, Finsupp.sum_mul
-- Module: Mathlib.Algebra.MonoidAlgebra.Lift
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : Semiring R
g_hom : Type u_6
inst_3 : FunLike g_hom G R
inst_4 : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm :
  ∀ {x y : G},
    y ∈ a.support → Commute.{u_2} (S := R) ((f : (a : k) → R) ((b : (a : G) → k) x : k) : R) ((g : (a : G) → R) y : R)
⊢ Eq.{u_2 + 1} (α := R)
    (sum a fun (a : G) (b_1 : k) ↦
      sum b fun (a_1 : G) (b : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (b_1 * b) : R) ((g : (a : G) → R) (a * a_1) : R))
    (sum a fun (a : G) (c : k) ↦
      sum b fun (a_1 : G) (c_1 : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c : R) ((g : (a : G) → R) a : R) *
          HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c_1 : R) ((g : (a : G) → R) a_1 : R))

Tactic:
Finset.sum_congr rfl fun y hy => Finset.sum_congr rfl fun x _hx => ?_

Premises used: Finsupp.sum, Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Lift
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : Semiring R
g_hom : Type u_6
inst_3 : FunLike g_hom G R
inst_4 : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm :
  ∀ {x y : G},
    y ∈ a.support → Commute.{u_2} (S := R) ((f : (a : k) → R) ((b : (a : G) → k) x : k) : R) ((g : (a : G) → R) y : R)
refine :
  ∀ (y : G) (hy : y ∈ a.support) (x : G) (_hx : x ∈ b.support),
    Eq.{u_2 + 1} (α := R)
      ((fun (a_1 : G) (b : k) ↦
          HMul.hMul (α := R) (β := R)
            (((↑f : k →+ R) : (a : k) → R) (HMul.hMul (α := k) ((a : (a : G) → k) y : k) b) : R)
            ((g : (a : G) → R) (y * a_1) : R))
        x ((b : (a : G) → k) x))
      ((fun (a_1 : G) (c : k) ↦
          HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) ((a : (a : G) → k) y : k) : R)
              ((g : (a : G) → R) y : R) *
            HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c : R) ((g : (a : G) → R) a_1 : R))
        x ((b : (a : G) → k) x))
⊢ Eq.{u_2 + 1} (α := R)
    (sum a fun (a : G) (b_1 : k) ↦
      sum b fun (a_1 : G) (b : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (b_1 * b) : R) ((g : (a : G) → R) (a * a_1) : R))
    (sum a fun (a : G) (c : k) ↦
      sum b fun (a_1 : G) (c_1 : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c : R) ((g : (a : G) → R) a : R) *
          HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c_1 : R) ((g : (a : G) → R) a_1 : R))

Tactic:
refine Finset.sum_congr rfl fun y hy => Finset.sum_congr rfl fun x _hx => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Lift
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : Semiring R
g_hom : Type u_6
inst_3 : FunLike g_hom G R
inst_4 : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm :
  ∀ {x y : G},
    y ∈ a.support → Commute.{u_2} (S := R) ((f : (a : k) → R) ((b : (a : G) → k) x : k) : R) ((g : (a : G) → R) y : R)
y : G
hy : y ∈ a.support
x : G
_hx : x ∈ b.support
⊢ Eq.{u_2 + 1} (α := R)
    ((fun (a_1 : G) (b : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (HMul.hMul (α := k) ((a : (a : G) → k) y : k) b) : R)
          ((g : (a : G) → R) (y * a_1) : R))
      x ((b : (a : G) → k) x))
    ((fun (a_1 : G) (c : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) ((a : (a : G) → k) y : k) : R)
            ((g : (a : G) → R) y : R) *
          HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c : R) ((g : (a : G) → R) a_1 : R))
      x ((b : (a : G) → k) x))

Tactic:
simp [mul_assoc, (h_comm hy).left_comm]

Premises used: Commute.left_comm, mul_assoc
-- Module: Mathlib.Algebra.MonoidAlgebra.Lift
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Semiring k
inst_2 : One G
g_hom : Type u_6
inst_3 : FunLike g_hom G R
inst_4 : OneHomClass g_hom G R
f : k →+* R
g : g_hom
⊢ Eq.{u_2 + 1} (α := R) ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) 1 : R) (1 : R)

Tactic:
simp [one_def]

Premises used: MonoidAlgebra.one_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Lift
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : Semiring R
f : k →+* R
g : G →* R
h_comm : ∀ (x : k) (y : G), Commute.{u_2} (S := R) ((f : (a : k) → R) x : R) ((g : (a : G) → R) y : R)
a : G
b : k
⊢ (liftNCRingHom f g h_comm : (a : k[G]) → R) (single a b) =
    HMul.hMul (α := R) (β := R) ((f : (a : k) → R) b : R) ((g : (a : G) → R) a : R)

Tactic:
liftNC_single _ _ _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MonoidAlgebra.liftNC_single, Finset.sum
-- Module: Mathlib.Algebra.MonoidAlgebra.Lift
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : NonUnitalNonAssocSemiring R
f : k →+ R
g : Multiplicative G → R
a : G
b : k
⊢ (liftNC f g : (a : k[G]) → R) (single a b) =
    HMul.hMul (α := R) ((f : (a : k) → R) b : R) (g ((Multiplicative.ofAdd : (a : G) → Multiplicative G) a))

Tactic:
liftAddHom_apply_single _ _ _

Premises used: Finsupp.liftAddHom_apply_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Lift
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : Add G
inst_2 : Semiring R
g_hom : Type u_6
inst_3 : FunLike.{u_6 + 1, u₂ + 1, u_2 + 1} g_hom (Multiplicative G) R
inst_4 : MulHomClass.{u_6, u₂, u_2} g_hom (Multiplicative G) R
f : k →+* R
g : g_hom
a b : k[G]
h_comm :
  ∀ {x y : G},
    y ∈ a.support →
      Commute.{u_2} (S := R) ((f : (a : k) → R) ((b : (a : G) → k) x : k) : R)
        ((g : (a : Multiplicative G) → R) ((Multiplicative.ofAdd : (a : G) → Multiplicative G) y : Multiplicative G) :
          R)
⊢ (liftNC (↑f : k →+ R) (⇑g : (a : Multiplicative G) → R) : (a : k[G]) → R) (a * b) =
    HMul.hMul (α := R) (β := R) ((liftNC (↑f : k →+ R) (⇑g : (a : Multiplicative G) → R) : (a : k[G]) → R) a : R)
      ((liftNC (↑f : k →+ R) (⇑g : (a : Multiplicative G) → R) : (a : k[G]) → R) b : R)

Tactic:
MonoidAlgebra.liftNC_mul f g _ _ @h_comm

Premises used: MonoidAlgebra.liftNC_mul, Multiplicative
-- Module: Mathlib.Algebra.MonoidAlgebra.Lift
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : Zero G
inst_2 : NonAssocSemiring R
g_hom : Type u_6
inst_3 : FunLike.{u_6 + 1, u₂ + 1, u_2 + 1} g_hom (Multiplicative G) R
inst_4 : OneHomClass.{u_6, u₂, u_2} g_hom (Multiplicative G) R
f : k →+* R
g : g_hom
⊢ Eq.{u_2 + 1} (α := R) ((liftNC (↑f : k →+ R) (⇑g : (a : Multiplicative G) → R) : (a : k[G]) → R) 1 : R) (1 : R)

Tactic:
MonoidAlgebra.liftNC_one f g

Premises used: Multiplicative, MonoidAlgebra.liftNC_one
-- Module: Mathlib.Algebra.MonoidAlgebra.Lift
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : AddMonoid G
inst_2 : Semiring R
f : k →+* R
g : MonoidHom.{u₂, u_2} (Multiplicative G) R
h_comm :
  ∀ (x : k) (y : Multiplicative G),
    Commute.{u_2} (S := R) ((f : (a : k) → R) x : R) ((g : (a : Multiplicative G) → R) y : R)
a : G
b : k
⊢ (liftNCRingHom f g h_comm : (a : k[G]) → R) (single a b) =
    HMul.hMul (α := R) (β := R) ((f : (a : k) → R) b : R)
      ((g : (a : Multiplicative G) → R) ((Multiplicative.ofAdd : (a : G) → Multiplicative G) a : Multiplicative G) : R)

Tactic:
liftNC_single _ _ _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, AddMonoidAlgebra.liftNC_single, Finset.sum
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
f : M → N
x : R[M]
⊢ (mapDomain f x).coeff = Finsupp.mapDomain f x.coeff

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.mapDomain, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
f : M → N
x : M →₀ R
⊢ ofCoeff (Finsupp.mapDomain f x) = mapDomain f (ofCoeff x)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, MonoidAlgebra.ofCoeff, Finsupp.mapDomain, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
f : M → N
⊢ Eq (α := R[N]) (mapDomain f 0) 0

Tactic:
Finsupp.mapDomain_zero ..

Premises used: Finsupp.mapDomain_zero, MonoidAlgebra
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
f : M → N
x y : R[M]
⊢ mapDomain f (x + y) = mapDomain f x + mapDomain f y

Tactic:
Finsupp.mapDomain_add ..

Premises used: MonoidAlgebra, Finsupp.mapDomain_add
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
N : Type u_7
inst : Semiring R
inst_1 : Semiring S
f : M → N
x : S[M]
v : M → S → R[M]
⊢ mapDomain f (sum x v) = sum x fun (a : M) (b : S) ↦ mapDomain f (v a b)

Tactic:
Finsupp.mapDomain_sum

Premises used: MonoidAlgebra, Finsupp.mapDomain_sum
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
f : M → N
a : M
r : R
hfg :
  ∀ (m : N),
    Eq.{u_3 + 1} (α := R) ((mapDomain f (single a r) : (a : N) → R) m : R) ((single (f a) r : (a : N) → R) m : R)
⊢ Eq (α := R[N]) (mapDomain f (single a r)) (single (f a) r)

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
f : M → N
a : M
r : R
m : N
⊢ Eq.{u_3 + 1} (α := R) ((mapDomain f (single a r) : (a : N) → R) m : R) ((single (f a) r : (a : N) → R) m : R)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
f : M → N
hf : Injective f
⊢ Injective (α := R[M]) (mapDomain f)

Tactic:
Finsupp.mapDomain_injective hf

Premises used: MonoidAlgebra, Finsupp.mapDomain_injective
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
inst_1 : One M
inst_2 : One N
F : Type u_9
inst_3 : FunLike F M N
inst_4 : OneHomClass F M N
f : F
⊢ Eq (α := R[N]) (mapDomain.{u_3, u_6, u_7} (M := M) (⇑f : (a : M) → N) 1) 1

Tactic:
simp [one_def]

Premises used: MonoidAlgebra.one_def
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
x : R[M]
⊢ (map f x).coeff = mapRange (⇑f : (a : R) → S) ⋯ x.coeff

Tactic:
rfl

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, Finsupp.onFinset, MonoidAlgebra.map, Finsupp.mapRange, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
x : M →₀ R
⊢ ofCoeff (mapRange (⇑f : (a : R) → S) ⋯ x) = map f (ofCoeff x)

Tactic:
rfl

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, MonoidAlgebra.map, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
⊢ Eq (α := S[M]) (map f 0) 0

Tactic:
mapRange_zero (hf := f.map_zero)

Premises used: MonoidAlgebra.ofCoeff, Finsupp.onFinset, MonoidAlgebra.map, Finsupp.mapRange_zero, MonoidAlgebra, Finsupp.mapRange