awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
B : Type u₄
inst_3 : Semiring B
inst_4 : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
g : AlgHom.{uS, uA, u₄} S (RingQuot s) B
h : g.comp (mkAlgHom S s) = f
w₁ :
  ∀ (x : A),
    Eq.{u₄ + 1} (α := B) ((g.comp (mkAlgHom S s) : (a : A) → B) x : B)
      ((AlgHom.comp
              ((liftAlgHom S (s := s) :
                  (a : { f : A →ₐ[S] B // ∀ ⦃x y : A⦄, s x y → (f : (a : A) → B) x = (f : (a : A) → B) y }) →
                    RingQuot s →ₐ[S] B)
                (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                  ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)) f w))
              (mkAlgHom S s) :
            (a : A) → B)
          x :
        B)
⊢ g =
    (liftAlgHom S (s := s) :
        (a : { f : A →ₐ[S] B // ∀ ⦃x y : A⦄, s x y → (f : (a : A) → B) x = (f : (a : A) → B) y }) → RingQuot s →ₐ[S] B)
      (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
        ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)) f w)

Tactic:
ext
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
B : Type u₄
inst_3 : Semiring B
inst_4 : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
g : AlgHom.{uS, uA, u₄} S (RingQuot s) B
h : g.comp (mkAlgHom S s) = f
x : A
⊢ Eq.{u₄ + 1} (α := B) ((g.comp (mkAlgHom S s) : (a : A) → B) x : B)
    ((AlgHom.comp
            ((liftAlgHom S (s := s) :
                (a : { f : A →ₐ[S] B // ∀ ⦃x y : A⦄, s x y → (f : (a : A) → B) x = (f : (a : A) → B) y }) →
                  RingQuot s →ₐ[S] B)
              (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)) f w))
            (mkAlgHom S s) :
          (a : A) → B)
        x :
      B)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
B : Type u₄
inst_3 : Semiring B
inst_4 : Algebra S B
s : A → A → Prop
f : AlgHom.{uS, uA, u₄} S (RingQuot s) B
⊢ f =
    (liftAlgHom S (s := s) :
        (a : { f : A →ₐ[S] B // ∀ ⦃x y : A⦄, s x y → (f : (a : A) → B) x = (f : (a : A) → B) y }) → RingQuot s →ₐ[S] B)
      (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
        ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B))
        (f.comp (mkAlgHom S s)) ⋯)

Tactic:
liftAlgHom_unique S (f.comp (mkAlgHom S s)) (fun _ _ h ↦ congr_arg (⇑f) (mkAlgHom_rel S h)) f rfl

Premises used: RingQuot.liftAlgHom_unique, RingQuot.mkAlgHom, congr_arg, RingQuot.mkAlgHom_rel, AlgHom.comp, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
f : SkewMonoidAlgebra k G
⊢ { toFinsupp := f.toFinsupp : SkewMonoidAlgebra k G } = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : SMulZeroClass S k
a : S
⊢ HSMul.hSMul (β := SkewMonoidAlgebra k G) a 0 = 0

Tactic:
congr_arg ofFinsupp (smul_zero a)

Premises used: smul_zero, SkewMonoidAlgebra.ofFinsupp, congr_arg, _private.0.SkewMonoidAlgebra.smul
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : SMulZeroClass S k
a : S
⊢ HSMul.hSMul (β := SkewMonoidAlgebra k G) a 0 = 0

Tactic:
exact congr_arg ofFinsupp (smul_zero a)

Premises used: smul_zero, SkewMonoidAlgebra.ofFinsupp, congr_arg
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
⊢ Eq (α := SkewMonoidAlgebra k G) { toFinsupp := 0 } 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a b : G →₀ k
rw rw₁ : { toFinsupp := a + b : SkewMonoidAlgebra k G } = { toFinsupp := a + b }
⊢ { toFinsupp := a + b : SkewMonoidAlgebra k G } = { toFinsupp := a }.add { toFinsupp := b }

Tactic:
rw [add]

Premises used: _private.0.SkewMonoidAlgebra.add
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : SMulZeroClass S k
a : S
b : G →₀ k
rw rw₁ : { toFinsupp := a • b : SkewMonoidAlgebra k G } = { toFinsupp := a • b }
⊢ { toFinsupp := a • b : SkewMonoidAlgebra k G } = smul a { toFinsupp := b }

Tactic:
rw [smul]

Premises used: _private.0.SkewMonoidAlgebra.smul
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
⊢ Eq (α := G →₀ k) (toFinsupp 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a b : SkewMonoidAlgebra k G
rw rw₁ : { toFinsupp := a.toFinsupp + b.toFinsupp : SkewMonoidAlgebra k G }.toFinsupp = a.toFinsupp + b.toFinsupp
⊢ (a + b).toFinsupp = a.toFinsupp + b.toFinsupp

Tactic:
rw [← ofFinsupp_add]

Premises used: SkewMonoidAlgebra.ofFinsupp_add
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : SMulZeroClass S k
a : S
b : SkewMonoidAlgebra k G
rw rw₁ : { toFinsupp := a • b.toFinsupp : SkewMonoidAlgebra k G }.toFinsupp = a • b.toFinsupp
⊢ (a • b).toFinsupp = a • b.toFinsupp

Tactic:
rw [← ofFinsupp_smul]

Premises used: SkewMonoidAlgebra.ofFinsupp_smul
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : Monoid S
inst_2 : DistribMulAction S k
a : S
ha : IsSMulRegular k a
toFinsupp toFinsupp_1 : G →₀ k
h :
  Eq (α := SkewMonoidAlgebra k G) ((fun (x : SkewMonoidAlgebra k G) ↦ a • x) { toFinsupp := toFinsupp })
    ((fun (x : SkewMonoidAlgebra k G) ↦ a • x) { toFinsupp := toFinsupp_1 })
⊢ { toFinsupp := toFinsupp : SkewMonoidAlgebra k G } = { toFinsupp := toFinsupp_1 }

Tactic:
congr_arg _ <| ha.finsupp (ofFinsupp.inj h)

Premises used: IsSMulRegular.finsupp, congr_arg, SkewMonoidAlgebra.ofFinsupp.inj
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : Monoid S
inst_2 : DistribMulAction S k
a : S
ha : IsSMulRegular k a
toFinsupp toFinsupp_1 : G →₀ k
h :
  Eq (α := SkewMonoidAlgebra k G) ((fun (x : SkewMonoidAlgebra k G) ↦ a • x) { toFinsupp := toFinsupp })
    ((fun (x : SkewMonoidAlgebra k G) ↦ a • x) { toFinsupp := toFinsupp_1 })
⊢ { toFinsupp := toFinsupp : SkewMonoidAlgebra k G } = { toFinsupp := toFinsupp_1 }

Tactic:
exact congr_arg _ <| ha.finsupp (ofFinsupp.inj h)

Premises used: IsSMulRegular.finsupp, congr_arg, SkewMonoidAlgebra.ofFinsupp.inj
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
⊢ Injective (α := SkewMonoidAlgebra k G) toFinsupp

Tactic:
fun ⟨_⟩ _ ↦ congr_arg _

Premises used: _private.0.SkewMonoidAlgebra.toFinsupp_injective.match_1, SkewMonoidAlgebra.ofFinsupp, congr_arg, Function.Injective
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a b : SkewMonoidAlgebra k G
⊢ a.toFinsupp = b.toFinsupp ↔ a = b

Tactic:
toFinsupp_injective.eq_iff

Premises used: Function.Injective.eq_iff, SkewMonoidAlgebra.toFinsupp_injective
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
⊢ Injective (α := G →₀ k) ofFinsupp

Tactic:
fun _ _ ↦ congr_arg toFinsupp

Premises used: SkewMonoidAlgebra.toFinsupp, congr_arg, Function.Injective
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a b : G →₀ k
⊢ { toFinsupp := a : SkewMonoidAlgebra k G } = { toFinsupp := b } ↔ a = b

Tactic:
ofFinsupp_injective.eq_iff

Premises used: Function.Injective.eq_iff, SkewMonoidAlgebra.ofFinsupp_injective
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a : SkewMonoidAlgebra k G
⊢ a.toFinsupp = 0 ↔ a = 0

Tactic:
toFinsupp_inj

Premises used: SkewMonoidAlgebra.toFinsupp_inj
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a : G →₀ k
⊢ { toFinsupp := a : SkewMonoidAlgebra k G } = 0 ↔ a = 0

Tactic:
ofFinsupp_inj

Premises used: SkewMonoidAlgebra.ofFinsupp_inj
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
inst_1 : Nontrivial k
inst_2 : Nonempty G
⊢ Nontrivial (SkewMonoidAlgebra k G)

Tactic:
Function.Injective.nontrivial ofFinsupp_injective

Premises used: Function.Injective.nontrivial, SkewMonoidAlgebra.ofFinsupp_injective
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
p : G →₀ k
rw rw₁ : { toFinsupp := p : SkewMonoidAlgebra k G }.toFinsupp.support = p.support
⊢ { toFinsupp := p : SkewMonoidAlgebra k G }.support = p.support

Tactic:
rw [support]

Premises used: SkewMonoidAlgebra.support
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
p : SkewMonoidAlgebra k G
rw rw₁ : p.toFinsupp.support = p.toFinsupp.support
⊢ p.toFinsupp.support = p.support

Tactic:
rw [support]

Premises used: SkewMonoidAlgebra.support
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
⊢ Eq.{u_2 + 1} (α := Finset G) (support.{u_1, u_2} (k := k) 0) ∅

Tactic:
rfl

Premises used: SkewMonoidAlgebra.support, rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
p : SkewMonoidAlgebra k G
rcases :
  ∀ (toFinsupp : G →₀ k),
    { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.support = ∅ ↔
      { toFinsupp := toFinsupp : SkewMonoidAlgebra k G } = 0
⊢ p.support = ∅ ↔ p = 0

Tactic:
rcases p
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
toFinsupp : G →₀ k
⊢ { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.support = ∅ ↔
    { toFinsupp := toFinsupp : SkewMonoidAlgebra k G } = 0

Tactic:
simp only [support, Finsupp.support_eq_empty, ofFinsupp_eq_zero]

Premises used: SkewMonoidAlgebra.ofFinsupp_eq_zero, SkewMonoidAlgebra.support, Finsupp.support_eq_empty
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
inst_1 : DecidableEq G
p q : SkewMonoidAlgebra k G
⊢ (p + q).support ⊆ p.support ∪ q.support

Tactic:
simpa [support] using Finsupp.support_add

Premises used: SkewMonoidAlgebra.support, Finsupp.support_add
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
p : G →₀ k
⊢ { toFinsupp := p : SkewMonoidAlgebra k G }.coeff = (⇑p : (a : G) → k)

Tactic:
rfl

Premises used: rfl, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
p q : G →₀ k
⊢ { toFinsupp := p : SkewMonoidAlgebra k G }.coeff = { toFinsupp := q : SkewMonoidAlgebra k G }.coeff →
    { toFinsupp := p : SkewMonoidAlgebra k G } = { toFinsupp := q }

Tactic:
simp only [coeff, DFunLike.coe_fn_eq, imp_self, ofFinsupp.injEq]

Premises used: SkewMonoidAlgebra.ofFinsupp.injEq, DFunLike.coe_fn_eq, imp_self, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
p q : SkewMonoidAlgebra k G
⊢ p.coeff = q.coeff ↔ p = q

Tactic:
coeff_injective.eq_iff

Premises used: Function.Injective.eq_iff, SkewMonoidAlgebra.coeff_injective
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
f : SkewMonoidAlgebra k G
g : G
⊢ (f.toFinsupp : (a : G) → k) g = f.coeff g

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
f : SkewMonoidAlgebra k G
a : G
rcases :
  ∀ (toFinsupp : G →₀ k),
    a ∈ { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.support ↔
      { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.coeff a ≠ 0
⊢ a ∈ f.support ↔ f.coeff a ≠ 0

Tactic:
rcases f with ⟨⟩
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a : G
toFinsupp : G →₀ k
⊢ a ∈ { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.support ↔
    { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.coeff a ≠ 0

Tactic:
simp only [coeff, support_ofFinsupp, Finsupp.mem_support_iff, ne_eq]

Premises used: Finsupp.mem_support_iff, ne_eq, SkewMonoidAlgebra.support_ofFinsupp, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
f : SkewMonoidAlgebra k G
a : G
⊢ a ∉ f.support ↔ f.coeff a = 0

Tactic:
simp only [mem_support_iff, ne_eq, not_not]

Premises used: Classical.not_not, ne_eq, SkewMonoidAlgebra.mem_support_iff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
p q : SkewMonoidAlgebra k G
rcases :
  ∀ (f : G →₀ k),
    { toFinsupp := f : SkewMonoidAlgebra k G } = q ↔
      ∀ (n : G), { toFinsupp := f : SkewMonoidAlgebra k G }.coeff n = q.coeff n
⊢ p = q ↔ ∀ (n : G), p.coeff n = q.coeff n

Tactic:
rcases p with ⟨f : G →₀ k⟩
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
q : SkewMonoidAlgebra k G
f : G →₀ k
rcases :
  ∀ (g : G →₀ k),
    { toFinsupp := f : SkewMonoidAlgebra k G } = { toFinsupp := g } ↔
      ∀ (n : G), { toFinsupp := f : SkewMonoidAlgebra k G }.coeff n = { toFinsupp := g : SkewMonoidAlgebra k G }.coeff n
⊢ { toFinsupp := f : SkewMonoidAlgebra k G } = q ↔
    ∀ (n : G), { toFinsupp := f : SkewMonoidAlgebra k G }.coeff n = q.coeff n

Tactic:
rcases q with ⟨g : G →₀ k⟩
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
f g : G →₀ k
⊢ { toFinsupp := f : SkewMonoidAlgebra k G } = { toFinsupp := g } ↔
    ∀ (n : G), { toFinsupp := f : SkewMonoidAlgebra k G }.coeff n = { toFinsupp := g : SkewMonoidAlgebra k G }.coeff n

Tactic:
simpa [coeff] using DFunLike.ext_iff (f := f) (g := g)

Premises used: DFunLike.ext_iff, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
p q : SkewMonoidAlgebra k G
⊢ (∀ (a : G), p.coeff a = q.coeff a) → p = q

Tactic:
ext_iff.2

Premises used: Iff.mpr, SkewMonoidAlgebra.ext_iff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
p q : SkewMonoidAlgebra k G
a : G
rcases :
  ∀ (toFinsupp : G →₀ k),
    ({ toFinsupp := toFinsupp : SkewMonoidAlgebra k G } + q).coeff a =
      { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.coeff a + q.coeff a
⊢ (p + q).coeff a = p.coeff a + q.coeff a

Tactic:
rcases p
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
q : SkewMonoidAlgebra k G
a : G
toFinsupp : G →₀ k
rcases :
  ∀ (toFinsupp_1 : G →₀ k),
    ({ toFinsupp := toFinsupp : SkewMonoidAlgebra k G } + { toFinsupp := toFinsupp_1 : SkewMonoidAlgebra k G }).coeff
        a =
      { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.coeff a +
        { toFinsupp := toFinsupp_1 : SkewMonoidAlgebra k G }.coeff a
⊢ ({ toFinsupp := toFinsupp : SkewMonoidAlgebra k G } + q).coeff a =
    { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.coeff a + q.coeff a

Tactic:
rcases q
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a : G
toFinsupp toFinsupp_1 : G →₀ k
simp_rw :
  (toFinsupp + toFinsupp_1 : (a : G) → k) a =
    HAdd.hAdd (α := k) (β := k) ((toFinsupp : (a : G) → k) a : k) ((toFinsupp_1 : (a : G) → k) a : k)
⊢ ({ toFinsupp := toFinsupp : SkewMonoidAlgebra k G } + { toFinsupp := toFinsupp_1 : SkewMonoidAlgebra k G }).coeff a =
    { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.coeff a +
      { toFinsupp := toFinsupp_1 : SkewMonoidAlgebra k G }.coeff a

Tactic:
simp_rw [← ofFinsupp_add, coeff]

Premises used: SkewMonoidAlgebra.ofFinsupp_add, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a : G
toFinsupp toFinsupp_1 : G →₀ k
⊢ (toFinsupp + toFinsupp_1 : (a : G) → k) a =
    HAdd.hAdd (α := k) (β := k) ((toFinsupp : (a : G) → k) a : k) ((toFinsupp_1 : (a : G) → k) a : k)

Tactic:
Finsupp.add_apply _ _ _

Premises used: Finsupp.add_apply
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a : G
toFinsupp toFinsupp_1 : G →₀ k
⊢ (toFinsupp + toFinsupp_1 : (a : G) → k) a =
    HAdd.hAdd (α := k) (β := k) ((toFinsupp : (a : G) → k) a : k) ((toFinsupp_1 : (a : G) → k) a : k)

Tactic:
exact Finsupp.add_apply _ _ _

Premises used: Finsupp.add_apply
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : SMulZeroClass S k
r : S
p : SkewMonoidAlgebra k G
a : G
⊢ (r • p).coeff a = r • p.coeff a

Tactic:
rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a : G
b : k
⊢ Eq (α := G →₀ k) (toFinsupp (single a b)) (Finsupp.single a b)

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a : G
b : k
⊢ Eq (α := SkewMonoidAlgebra k G) { toFinsupp := Finsupp.single a b } (single a b)

Tactic:
rfl

Premises used: SkewMonoidAlgebra.single, rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a : G
b : k
inst_1 : DecidableEq G
⊢ coeff (single a b) = Pi.single (M := fun (j : G) ↦ k) a b

Tactic:
simp [coeff, Finsupp.single_eq_pi_single]

Premises used: Finsupp.single_eq_pi_single, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a a' : G
b : k
inst_1 : Decidable (a = a')
⊢ coeff (single a b) a' = if a = a' then b else 0

Tactic:
simp [coeff, Finsupp.single_apply]

Premises used: Finsupp.single_apply, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a : G
⊢ Eq (α := SkewMonoidAlgebra k G) (single a 0) 0

Tactic:
simp [← toFinsupp_inj]

Premises used: SkewMonoidAlgebra.toFinsupp_inj
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a : G
b₁ b₂ : k
⊢ single a (b₁ + b₂) = HAdd.hAdd (α := SkewMonoidAlgebra k G) (single a b₁) (single a b₂)

Tactic:
simp [← toFinsupp_inj]

Premises used: SkewMonoidAlgebra.toFinsupp_inj
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a : G
b : k
⊢ Eq (α := SkewMonoidAlgebra k G) (single a b) 0 ↔ b = 0

Tactic:
simp [← toFinsupp_inj]

Premises used: SkewMonoidAlgebra.toFinsupp_inj
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : SMulZeroClass S k
s : S
a : G
b : k
⊢ (HSMul.hSMul (β := SkewMonoidAlgebra k G) s (single a b)).toFinsupp = toFinsupp (single a (s • b))

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a : G
⊢ Injective (α := k) (β := SkewMonoidAlgebra k G) (single a)

Tactic:
toFinsuppAddEquiv.symm.injective.comp (Finsupp.single_injective a)

Premises used: Finsupp.single_injective, SkewMonoidAlgebra.toFinsuppAddEquiv, Function.Injective.comp, AddEquiv.injective, SkewMonoidAlgebra.single, AddEquiv.symm
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a a' : G
b : k
h : b ≠ 0
rw : Eq (α := G →₀ k) (toFinsupp (single a b)) (toFinsupp (single a' b)) ↔ a = a'
⊢ Eq (α := SkewMonoidAlgebra k G) (single a b) (single a' b) ↔ a = a'

Tactic:
rw [← toFinsupp_inj]

Premises used: SkewMonoidAlgebra.toFinsupp_inj
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a a' : G
b : k
h : b ≠ 0
⊢ Eq (α := G →₀ k) (toFinsupp (single a b)) (toFinsupp (single a' b)) ↔ a = a'

Tactic:
Finsupp.single_left_inj h

Premises used: Finsupp.single_left_inj, Finsupp.single
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a a' : G
b : k
h : b ≠ 0
⊢ Eq (α := G →₀ k) (toFinsupp (single a b)) (toFinsupp (single a' b)) ↔ a = a'

Tactic:
exact Finsupp.single_left_inj h

Premises used: Finsupp.single_left_inj
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : Monoid S
inst_2 : DistribMulAction S k
a : S
inst_3 : Nonempty G
inhabit : ∀ (inhabited_h : Inhabited G), IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a
⊢ IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a

Tactic:
inhabit G
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : Monoid S
inst_2 : DistribMulAction S k
a : S
inst_3 : Nonempty G
inhabited_h : Inhabited G
⊢ IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a

Tactic:
⟨IsSMulRegular.skewMonoidAlgebra, fun ha b₁ b₂ inj ↦ ?_⟩

Premises used: IsSMulRegular.skewMonoidAlgebra, Iff.intro
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : Monoid S
inst_2 : DistribMulAction S k
a : S
inst_3 : Nonempty G
inhabited_h : Inhabited G
refine :
  ∀ (ha : IsSMulRegular (SkewMonoidAlgebra k G) a) (b₁ b₂ : k)
    (inj : Eq.{u_1 + 1} (α := k) ((fun (x : k) ↦ a • x) b₁) ((fun (x : k) ↦ a • x) b₂)), b₁ = b₂
⊢ IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a

Tactic:
refine ⟨IsSMulRegular.skewMonoidAlgebra, fun ha b₁ b₂ inj ↦ ?_⟩
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : Monoid S
inst_2 : DistribMulAction S k
a : S
inst_3 : Nonempty G
inhabited_h : Inhabited G
ha : IsSMulRegular (SkewMonoidAlgebra k G) a
b₁ b₂ : k
inj : Eq.{u_1 + 1} (α := k) ((fun (x : k) ↦ a • x) b₁) ((fun (x : k) ↦ a • x) b₂)
rw :
  ∀
    (inj :
      HSMul.hSMul (β := SkewMonoidAlgebra k G) a (single default b₁) =
        HSMul.hSMul (β := SkewMonoidAlgebra k G) a (single default b₂)),
    b₁ = b₂
rw₁ : Type u_2
⊢ b₁ = b₂

Tactic:
rw [← (single_injective _).eq_iff, ← smul_single, ← smul_single] at inj

Premises used: SkewMonoidAlgebra.single_injective, Function.Injective.eq_iff, SkewMonoidAlgebra.smul_single
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : Monoid S
inst_2 : DistribMulAction S k
a : S
inst_3 : Nonempty G
inhabited_h : Inhabited G
ha : IsSMulRegular (SkewMonoidAlgebra k G) a
b₁ b₂ : k
inj_1 : Eq.{u_1 + 1} (α := k) ((fun (x : k) ↦ a • x) b₁) ((fun (x : k) ↦ a • x) b₂)
inj :
  HSMul.hSMul (β := SkewMonoidAlgebra k G) a (single default b₁) =
    HSMul.hSMul (β := SkewMonoidAlgebra k G) a (single default b₂)
⊢ b₁ = b₂

Tactic:
single_injective default (ha inj)

Premises used: Inhabited.default, SkewMonoidAlgebra.single_injective
-- 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) { toFinsupp := Finsupp.single 1 1 } 1

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : One G
inst_1 : AddMonoidWithOne k
a : SkewMonoidAlgebra k G
⊢ a.toFinsupp = Finsupp.single 1 1 ↔ a = 1

Tactic:
simp [← toFinsupp_inj]

Premises used: SkewMonoidAlgebra.toFinsupp_inj