awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
inst_1 : DecidableEq α
h :
  ∀ (a_1 : α),
    Membership.mem (γ := Finset α)
        (support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)) a_1 ↔
      a_1 ∈ f.support.erase a
⊢ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) = f.support.erase a

Tactic:
ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
inst_1 : DecidableEq α
a_1 : α
⊢ Membership.mem (γ := Finset α)
      (support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)) a_1 ↔
    a_1 ∈ f.support.erase a

Tactic:
simp [erase]

Premises used: SkewMonoidAlgebra.erase
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
⊢ Eq.{u_4 + 1} (α := M) (coeff ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) a) 0

Tactic:
simp [erase]

Premises used: SkewMonoidAlgebra.erase
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a a' : α
f : SkewMonoidAlgebra M α
h : a' ≠ a
⊢ coeff ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) a' = f.coeff a'

Tactic:
simp [erase, h]

Premises used: SkewMonoidAlgebra.erase
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
b : M
⊢ Eq (α := SkewMonoidAlgebra M α)
    ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) (single a b) : SkewMonoidAlgebra M α)
    (0 : SkewMonoidAlgebra M α)

Tactic:
simp [erase]

Premises used: SkewMonoidAlgebra.erase
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a a' : α
f : SkewMonoidAlgebra M α
inst_1 : DecidableEq α
⊢ coeff ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) a' = if a' = a then 0 else f.coeff a'

Tactic:
ite_congr rfl (fun _ ↦ rfl) (fun _ ↦ rfl)

Premises used: ite_congr, rfl, SkewMonoidAlgebra.coeff, ite
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
a₁ :
  (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp
⊢ HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α) =
    f

Tactic:
apply toFinsupp_injective

Premises used: SkewMonoidAlgebra.toFinsupp_injective
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
a₁ :
  (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
        { toFinsupp := Finsupp.single a (f.coeff a) : SkewMonoidAlgebra M α }
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp
a₂ :
  (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
        ({ toFinsupp := Finsupp.single a ((f.toFinsupp : (a : α) → M) a) } : SkewMonoidAlgebra M α)
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp
a₃ :
  HAdd.hAdd (α := α →₀ M) (β := α →₀ M)
      (toFinsupp { toFinsupp := Finsupp.single a ((f.toFinsupp : (a : α) → M) a) : SkewMonoidAlgebra M α } : α →₀ M)
      (toFinsupp ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) : α →₀ M) =
    f.toFinsupp
a₄ :
  HAdd.hAdd (α := α →₀ M)
      (toFinsupp { toFinsupp := Finsupp.single a ((f.toFinsupp : (a : α) → M) a) : SkewMonoidAlgebra M α } : α →₀ M)
      (Finsupp.erase a f.toFinsupp) =
    f.toFinsupp
a₅ a₆ : f.toFinsupp = f.toFinsupp
⊢ (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp

Tactic:
rw [single, ← toFinsupp_apply, toFinsupp_add, erase_apply_toFinsupp,
    Finsupp.single_add_erase]

Premises used: SkewMonoidAlgebra.toFinsupp_apply, SkewMonoidAlgebra.erase_apply_toFinsupp, SkewMonoidAlgebra.toFinsupp_add, Finsupp.single_add_erase, SkewMonoidAlgebra.single
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s : Finset α
f : SkewMonoidAlgebra M α
hf : f.support = ∅
rwa rwa₁ rwa₂ rwa₃ : p 0
⊢ p f

Tactic:
rwa [support_eq_empty.1 hf]

Premises used: SkewMonoidAlgebra.support_eq_empty, Iff.mp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
this :
  p
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α))
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : p f), p f
⊢ p f

Tactic:
rwa [single_add_erase] at this

Premises used: SkewMonoidAlgebra.single_add_erase
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
suffices :
  p
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α))
⊢ p f

Tactic:
suffices p (single a (f.coeff a) + f.erase a) by rwa [single_add_erase] at this
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
a₁ : a ∉ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)
a₂ : f.coeff a ≠ 0
a₃ : p ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)
⊢ p
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α))

Tactic:
apply ha
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
a₁ : ¬(a ≠ a ∧ a ∈ f.support)
⊢ a ∉ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)

Tactic:
rw [support_erase, Finset.mem_erase]

Premises used: Finset.mem_erase, SkewMonoidAlgebra.support_erase
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ ¬(a ≠ a ∧ a ∈ f.support)

Tactic:
fun H ↦ H.1 rfl

Premises used: And.left, Not, rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ ¬(a ≠ a ∧ a ∈ f.support)

Tactic:
exact fun H ↦ H.1 rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ f.coeff a ≠ 0

Tactic:
simp only [← mem_support_iff, hf, Finset.mem_cons_self]

Premises used: SkewMonoidAlgebra.mem_support_iff, Finset.mem_cons_self
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
a₁ : support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) = s
⊢ p ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)

Tactic:
apply ih
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
a₁ : f.support.erase a = s
a₂ : (Finset.cons a s has).erase a = s
a₃ a₄ : s = s
⊢ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) = s

Tactic:
rw [support_erase, hf, Finset.erase_cons]

Premises used: Finset.erase_cons, SkewMonoidAlgebra.support_erase
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
a₁ : a ∉ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)
a₂ : f.coeff a ≠ 0
a₃ : p ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)
a₄ : f.coeff a ≠ 0
a₅ a₆ : p ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)
⊢ p
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α))

Tactic:
classical
    apply ha
    · rw [support_erase, Finset.mem_erase]
      exact fun H ↦ H.1 rfl
    · simp only [← mem_support_iff, hf, Finset.mem_cons_self]
    · apply ih
      rw [support_erase, hf, Finset.erase_cons]

Premises used: Finset.erase_cons, SkewMonoidAlgebra.mem_support_iff, Finset.mem_erase, Finset.mem_cons_self, SkewMonoidAlgebra.support_erase
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
rcases :
  ∀ (f : α →₀ M),
    { toFinsupp := f : SkewMonoidAlgebra M α }.update a ({ toFinsupp := f : SkewMonoidAlgebra M α }.coeff a) =
      { toFinsupp := f }
⊢ f.update a (f.coeff a) = f

Tactic:
rcases f with ⟨f⟩
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
f : α →₀ M
a₁ :
  ({ toFinsupp := f : SkewMonoidAlgebra M α }.update a ({ toFinsupp := f : SkewMonoidAlgebra M α }.coeff a)).toFinsupp =
    { toFinsupp := f }.toFinsupp
⊢ { toFinsupp := f : SkewMonoidAlgebra M α }.update a ({ toFinsupp := f : SkewMonoidAlgebra M α }.coeff a) =
    { toFinsupp := f }

Tactic:
apply toFinsupp_injective

Premises used: SkewMonoidAlgebra.toFinsupp_injective
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
f : α →₀ M
⊢ ({ toFinsupp := f : SkewMonoidAlgebra M α }.update a ({ toFinsupp := f : SkewMonoidAlgebra M α }.coeff a)).toFinsupp =
    { toFinsupp := f }.toFinsupp

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
b : M
⊢ Eq (α := SkewMonoidAlgebra M α) (update 0 a b) (single a b)

Tactic:
simp [update]

Premises used: SkewMonoidAlgebra.update
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
inst_1 : DecidableEq α
inst_2 : DecidableEq M
⊢ (f.update a b).support = if b = 0 then f.support.erase a else insert a f.support

Tactic:
aesop (add norm [update, Finsupp.support_update_ne_zero])

Premises used: Finsupp.support_update_ne_zero, SkewMonoidAlgebra.update
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
inst_1 : DecidableEq α
simp :
  Eq (α := α → M) (Function.update (β := fun (a : α) ↦ M) (⇑f.toFinsupp : (a : α) → M) a b)
    (Function.update (β := fun (a : α) ↦ M) (⇑f.toFinsupp : (a : α) → M) a b)
⊢ (f.update a b).coeff = Function.update (β := fun (a : α) ↦ M) f.coeff a b

Tactic:
simp only [coeff, update, Finsupp.update, Finsupp.coe_mk]

Premises used: Finsupp.update, SkewMonoidAlgebra.update, Finsupp.coe_mk, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
inst_1 : DecidableEq α
⊢ Eq (α := α → M) (Function.update (β := fun (a : α) ↦ M) (⇑f.toFinsupp : (a : α) → M) a b)
    (Function.update (β := fun (a : α) ↦ M) (⇑f.toFinsupp : (a : α) → M) a b)

Tactic:
congr!
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a' : α
b : M
inst_1 : DecidableEq α
rw : Function.update (β := fun (a : α) ↦ M) f.coeff a b a' = if a' = a then b else f.coeff a'
rw₁ rw₂ : (if a' = a then b else f.coeff a') = if a' = a then b else f.coeff a'
⊢ (f.update a b).coeff a' = if a' = a then b else f.coeff a'

Tactic:
rw [coeff_update, Function.update_apply]

Premises used: Function.update_apply, SkewMonoidAlgebra.coeff_update
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
rw : (if a = a then b else f.coeff a) = b
rw₁ rw₂ : b = b
⊢ (f.update a b).coeff a = b

Tactic:
rw [f.coeff_update_apply, if_pos rfl]

Premises used: if_pos, SkewMonoidAlgebra.coeff_update_apply, rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
rw : (if a = a then b else f.coeff a) = b
rw₁ rw₂ : b = b
⊢ (f.update a b).coeff a = b

Tactic:
classical
  rw [f.coeff_update_apply, if_pos rfl]

Premises used: if_pos, SkewMonoidAlgebra.coeff_update_apply, rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a' : α
b : M
h : a' ≠ a
rw : (if a' = a then b else f.coeff a') = f.coeff a'
rw₁ rw₂ : f.coeff a' = f.coeff a'
⊢ (f.update a b).coeff a' = f.coeff a'

Tactic:
rw [f.coeff_update_apply, if_neg h]

Premises used: SkewMonoidAlgebra.coeff_update_apply, if_neg
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a' : α
b : M
h : a' ≠ a
rw : (if a' = a then b else f.coeff a') = f.coeff a'
rw₁ rw₂ : f.coeff a' = f.coeff a'
⊢ (f.update a b).coeff a' = f.coeff a'

Tactic:
classical
  rw [f.coeff_update_apply, if_neg h]

Premises used: SkewMonoidAlgebra.coeff_update_apply, if_neg
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
a₁ :
  ∀ (x : α),
    (f.update a b).coeff x =
      (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
            ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)
            (single a b)).coeff
        x
⊢ f.update a b =
    HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α) (single a b)

Tactic:
ext x
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
x : α
pos :
  ∀ (hx : x = a),
    (f.update a b).coeff x =
      (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
            ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)
            (single a b)).coeff
        x
neg :
  ∀ (hx : ¬x = a),
    (f.update a b).coeff x =
      (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
            ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)
            (single a b)).coeff
        x
⊢ (f.update a b).coeff x =
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
          ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)
          (single a b)).coeff
      x

Tactic:
by_cases hx : x = a
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
x : α
hx : x = a
⊢ (f.update a b).coeff x =
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
          ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)
          (single a b)).coeff
      x

Tactic:
aesop (add norm coeff_single_apply)

Premises used: SkewMonoidAlgebra.coeff_single_apply
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
x : α
hx : ¬x = a
⊢ (f.update a b).coeff x =
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
          ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)
          (single a b)).coeff
      x

Tactic:
aesop (add norm coeff_single_apply)

Premises used: SkewMonoidAlgebra.coeff_single_apply
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
a₁ a₂ :
  ∀ (x : α),
    (f.update a b).coeff x =
      (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
            ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)
            (single a b)).coeff
        x
⊢ f.update a b =
    HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α) (single a b)

Tactic:
classical ext x; by_cases hx : x = a <;> aesop (add norm coeff_single_apply)

Premises used: SkewMonoidAlgebra.coeff_single_apply
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
a₁ :
  ∀ (a_1 : α), (f.update a 0).coeff a_1 = coeff ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) a_1
⊢ f.update a 0 = (erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f

Tactic:
ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a_1 : α
⊢ (f.update a 0).coeff a_1 = coeff ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) a_1

Tactic:
simp [coeff_update_apply, coeff_erase_apply]

Premises used: SkewMonoidAlgebra.coeff_update_apply, SkewMonoidAlgebra.coeff_erase_apply
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
a₁ a₂ :
  ∀ (a_1 : α), (f.update a 0).coeff a_1 = coeff ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) a_1
⊢ f.update a 0 = (erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f

Tactic:
classical ext; simp [coeff_update_apply, coeff_erase_apply]

Premises used: SkewMonoidAlgebra.coeff_update_apply, SkewMonoidAlgebra.coeff_erase_apply
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
b : k
a : G
h : b ≠ 0
⊢ support (single a b) = {a}

Tactic:
Finsupp.support_single _ h

Premises used: Finsupp.support_single, SkewMonoidAlgebra.support
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
a : G
b : k
⊢ support (single a b) ⊆ {a}

Tactic:
Finsupp.support_single_subset

Premises used: Set.Mem, setOf, Finsupp.support_single_subset
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst_1 : DecidableEq G'
inst_2 : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
simp_rw :
  Subset.{u_4} (α := Finset G')
    (Finsupp.support.{u_4, u_3} (M := k') (f.toFinsupp.sum fun (x1 : G) (x2 : k) ↦ (g x1 x2).toFinsupp))
    (f.toFinsupp.support.biUnion fun (a : G) ↦ (g a (f.coeff a)).toFinsupp.support)
⊢ (f.sum g).support ⊆ f.support.biUnion fun (a : G) ↦ (g a (f.coeff a)).support

Tactic:
simp_rw [support, toFinsupp_sum']

Premises used: SkewMonoidAlgebra.support, SkewMonoidAlgebra.toFinsupp_sum'
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst_1 : DecidableEq G'
inst_2 : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
⊢ Subset.{u_4} (α := Finset G')
    (Finsupp.support.{u_4, u_3} (M := k') (f.toFinsupp.sum fun (x1 : G) (x2 : k) ↦ (g x1 x2).toFinsupp))
    (f.toFinsupp.support.biUnion fun (a : G) ↦ (g a (f.coeff a)).toFinsupp.support)

Tactic:
apply Finsupp.support_sum

Premises used: Finsupp.support_sum
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
Goal:
k : Type u_1
G : Type u_2
inst : AddCommGroup k
p : SkewMonoidAlgebra k G
rw : (-p).toFinsupp.support = p.support
rw₁ : (-p.toFinsupp).support = p.support
rw₂ : p.toFinsupp.support = p.support
rw₃ rw₄ : p.support = p.support
⊢ (-p).support = p.support

Tactic:
rw [support, toFinsupp_neg, Finsupp.support_neg, support_toFinsupp]

Premises used: SkewMonoidAlgebra.support_toFinsupp, SkewMonoidAlgebra.toFinsupp_neg, SkewMonoidAlgebra.support, Finsupp.support_neg
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
Goal:
k : Type u_1
G : Type u_2
inst : One G
inst_1 : AddCommMonoidWithOne k
⊢ Subset.{u_2} (α := Finset G) (support.{u_1, u_2} (k := k) 1) 1

Tactic:
Finsupp.support_single_subset

Premises used: Set.Mem, setOf, Finsupp.support_single_subset