awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
A : Type u_4
inst_2 : Semiring A
inst_3 : Algebra k A
inst_4 : MulSemiringAction G k
inst_5 : SMulCommClass G k k
F : G →* A
a : G
b : k
rw :
  (liftNC (↑(algebraMap k A) : k →+ A) (⇑F : (a : G) → A) : (a : SkewMonoidAlgebra k G) → A) (single a b) =
    HSMul.hSMul (β := A) b ((F : (a : G) → A) a : A)
rw₁ :
  HMul.hMul (α := A) (β := A) (((↑(algebraMap k A) : k →+ A) : (a : k) → A) b : A) ((F : (a : G) → A) a : A) =
    HSMul.hSMul (β := A) b ((F : (a : G) → A) a : A)
rw₂ :
  HMul.hMul (α := A) (β := A) (((↑(algebraMap k A) : k →+ A) : (a : k) → A) b : A) ((F : (a : G) → A) a : A) =
    HMul.hMul (α := A) (β := A) ((algebraMap k A : (a : k) → A) b : A) ((F : (a : G) → A) a : A)
rw₃ rw₄ :
  HMul.hMul (α := A) (β := A) ((algebraMap k A : (a : k) → A) b : A) ((F : (a : G) → A) a : A) =
    HMul.hMul (α := A) (β := A) ((algebraMap k A : (a : k) → A) b : A) ((F : (a : G) → A) a : A)
⊢ (((lift k G A : (a : G →* A) → SkewMonoidAlgebra k G →ₐ[k] A) F : SkewMonoidAlgebra k G →ₐ[k] A) :
        (a : SkewMonoidAlgebra k G) → A)
      (single a b) =
    HSMul.hSMul (β := A) b ((F : (a : G) → A) a : A)

Tactic:
rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]

Premises used: AddMonoidHom.coe_coe, SkewMonoidAlgebra.liftNC_single, Algebra.smul_def, SkewMonoidAlgebra.lift_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
A : Type u_4
inst_2 : Semiring A
inst_3 : Algebra k A
inst_4 : MulSemiringAction G k
inst_5 : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
⊢ F =
    (lift k G A : (a : G →* A) → SkewMonoidAlgebra k G →ₐ[k] A)
      (MonoidHom.comp (↑F : SkewMonoidAlgebra k G →* A) (of k G))

Tactic:
((lift k G A).apply_symm_apply F).symm

Premises used: Equiv.apply_symm_apply, Eq.symm, SkewMonoidAlgebra.lift
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
A : Type u_4
inst_2 : Semiring A
inst_3 : Algebra k A
inst_4 : MulSemiringAction G k
inst_5 : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
f : SkewMonoidAlgebra k G
rw :
  ((((lift k G A : (a : G →* A) → SkewMonoidAlgebra k G →ₐ[k] A)
            (MonoidHom.comp (↑F : SkewMonoidAlgebra k G →* A) (of k G)) :
          SkewMonoidAlgebra k G →ₐ[k] A) :
        (a : SkewMonoidAlgebra k G) → A)
      f :
    A)
| ((F : (a : SkewMonoidAlgebra k G) → A) f : A)

Tactic:
rw [lift_unique' F]

Premises used: SkewMonoidAlgebra.lift_unique'
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
A : Type u_4
inst_2 : Semiring A
inst_3 : Algebra k A
inst_4 : MulSemiringAction G k
inst_5 : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
f : SkewMonoidAlgebra k G
simp : f.sum fun (a : G) (b : k) ↦ HSMul.hSMul (β := A) b ((F : (a : SkewMonoidAlgebra k G) → A) (single a 1) : A)
| ((((lift k G A : (a : G →* A) → SkewMonoidAlgebra k G →ₐ[k] A)
            (MonoidHom.comp (↑F : SkewMonoidAlgebra k G →* A) (of k G)) :
          SkewMonoidAlgebra k G →ₐ[k] A) :
        (a : SkewMonoidAlgebra k G) → A)
      f :
    A)

Tactic:
simp [lift_apply]

Premises used: SkewMonoidAlgebra.lift_apply
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
A : Type u_4
inst_2 : Semiring A
inst_3 : Algebra k A
inst_4 : MulSemiringAction G k
inst_5 : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
f : SkewMonoidAlgebra k G
rw : f.sum fun (a : G) (b : k) ↦ HSMul.hSMul (β := A) b ((F : (a : SkewMonoidAlgebra k G) → A) (single a 1) : A)
| ((F : (a : SkewMonoidAlgebra k G) → A) f : A)

Tactic:
rw [lift_unique' F]
    simp [lift_apply]

Premises used: SkewMonoidAlgebra.lift_apply, SkewMonoidAlgebra.lift_unique'
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
A : Type u_4
inst_2 : Semiring A
inst_3 : Algebra k A
inst_4 : MulSemiringAction G k
inst_5 : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
f : SkewMonoidAlgebra k G
conv_lhs :
  Eq.{u_4 + 1} (α := A) ((F : (a : SkewMonoidAlgebra k G) → A) f : A)
    (f.sum fun (a : G) (b : k) ↦ HSMul.hSMul (β := A) b ((F : (a : SkewMonoidAlgebra k G) → A) (single a 1) : A) : A)
conv_lhs₁ :
  Eq.{u_4 + 1} (α := A)
    (f.sum fun (a : G) (b : k) ↦ HSMul.hSMul (β := A) b ((F : (a : SkewMonoidAlgebra k G) → A) (single a 1) : A))
    (f.sum fun (a : G) (b : k) ↦ HSMul.hSMul (β := A) b ((F : (a : SkewMonoidAlgebra k G) → A) (single a 1) : A))
⊢ Eq.{u_4 + 1} (α := A) ((F : (a : SkewMonoidAlgebra k G) → A) f : A)
    (f.sum fun (a : G) (b : k) ↦ HSMul.hSMul (β := A) b ((F : (a : SkewMonoidAlgebra k G) → A) (single a 1) : A) : A)

Tactic:
conv_lhs =>
    rw [lift_unique' F]
    simp [lift_apply]

Premises used: SkewMonoidAlgebra.lift_apply, SkewMonoidAlgebra.lift_unique'
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k_1 : Type u_1
G : Type u_2
H_1 : Type u_3
inst : CommSemiring k_1
inst_1 : Monoid G
inst_2 : Monoid H_1
A_1 : Type u_4
B : Type u_5
inst_3 : Semiring A_1
inst_4 : Algebra k_1 A_1
inst_5 : Semiring B
inst_6 : Algebra k_1 B
inst_7 : MulSemiringAction G k_1
inst_8 : SMulCommClass G k_1 k_1
k : Type u_6
A : Type u_7
inst_9 : CommSemiring k
inst_10 : Semiring A
inst_11 : Algebra k A
H : Type u_8
F : Type u_9
inst_12 : Monoid H
inst_13 : FunLike F G H
inst_14 : MonoidHomClass F G H
inst_15 : MulSemiringAction G A
inst_16 : MulSemiringAction H A
inst_17 : SMulCommClass G k A
inst_18 : SMulCommClass H k A
f : F
hf : ∀ (a : G) (x : A), a • x = HSMul.hSMul.{u_8, u_7, u_7} (α := H) ((f : (a : G) → H) a : H) x
⊢ ∀ (r : k),
    (↑(↑(mapDomainRingHom hf) : SkewMonoidAlgebra A G →* SkewMonoidAlgebra A H) :
            OneHom (SkewMonoidAlgebra A G) (SkewMonoidAlgebra A H)).toFun
        ((algebraMap k (SkewMonoidAlgebra A G) : (a : k) → SkewMonoidAlgebra A G) r) =
      (algebraMap k (SkewMonoidAlgebra A H) : (a : k) → SkewMonoidAlgebra A H) r

Tactic:
simp [mapDomainRingHom]

Premises used: SkewMonoidAlgebra.mapDomainRingHom
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : AddCommMonoid k
f : G ≃ H
l : SkewMonoidAlgebra k G
⊢ ∀ (a : H),
    a ∈ Finset.map f.toEmbedding l.support ↔
      Ne.{u_1 + 1} (α := k) ((fun (a : H) ↦ l.coeff ((f.symm : (a : H) → G) a)) a) 0

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : AddCommMonoid k
f : G ≃ H
l : SkewMonoidAlgebra k G
b : H
⊢ (equivMapDomain f l).coeff b = l.coeff ((f.symm : (a : H) → G) b)

Tactic:
rfl

Premises used: SkewMonoidAlgebra.equivMapDomain, rfl, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : AddCommMonoid k
f : G ≃ H
l : SkewMonoidAlgebra k G
⊢ (equivMapDomain f l).toFinsupp = Finsupp.equivMapDomain f l.toFinsupp

Tactic:
rfl

Premises used: Finsupp.equivMapDomain, SkewMonoidAlgebra.support, rfl, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : AddCommMonoid k
f : G ≃ H
l : SkewMonoidAlgebra k G
a :
  (equivMapDomain f l).toFinsupp =
    toFinsupp ((mapDomain (⇑f : (a : G) → H) : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k H) l)
⊢ equivMapDomain f l = (mapDomain (⇑f : (a : G) → H) : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k H) l

Tactic:
apply toFinsupp_injective

Premises used: SkewMonoidAlgebra.toFinsupp_injective
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : AddCommMonoid k
f : G ≃ H
l : SkewMonoidAlgebra k G
a :
  ∀ (x : H),
    Eq.{u_1 + 1} (α := k) (((equivMapDomain f l).toFinsupp : (a : H) → k) x : k)
      ((toFinsupp ((mapDomain (⇑f : (a : G) → H) : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k H) l) :
            (a : H) → k)
          x :
        k)
⊢ (equivMapDomain f l).toFinsupp =
    toFinsupp ((mapDomain (⇑f : (a : G) → H) : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k H) l)

Tactic:
ext x
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : AddCommMonoid k
f : G ≃ H
l : SkewMonoidAlgebra k G
x : H
a :
  Eq.{u_1 + 1} (α := k) ((Finsupp.equivMapDomain f l.toFinsupp : (a : H) → k) x : k)
    ((toFinsupp ((mapDomain (⇑f : (a : G) → H) : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k H) l) : (a : H) → k)
        x :
      k)
a₁ :
  Eq.{u_1 + 1} (α := k) ((l.toFinsupp : (a : G) → k) ((f.symm : (a : H) → G) x : G) : k)
    ((toFinsupp ((mapDomain (⇑f : (a : G) → H) : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k H) l) : (a : H) → k)
        x :
      k)
a₂ :
  Eq.{u_1 + 1} (α := k) ((l.toFinsupp : (a : G) → k) ((f.symm : (a : H) → G) x : G) : k)
    ((Finsupp.mapDomain (⇑f : (a : G) → H) l.toFinsupp : (a : H) → k) x : k)
⊢ Eq.{u_1 + 1} (α := k) (((equivMapDomain f l).toFinsupp : (a : H) → k) x : k)
    ((toFinsupp ((mapDomain (⇑f : (a : G) → H) : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k H) l) : (a : H) → k)
        x :
      k)

Tactic:
simp_rw [toFinsupp_equivMapDomain, Finsupp.equivMapDomain_apply, toFinsupp_mapDomain,
    Finsupp.mapDomain_equiv_apply]

Premises used: SkewMonoidAlgebra.toFinsupp_equivMapDomain, Finsupp.equivMapDomain_apply, SkewMonoidAlgebra.toFinsupp_mapDomain, Finsupp.mapDomain_equiv_apply
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
G' : Type u_4
G'' : Type u_5
f : G ≃ G'
g : G' ≃ G''
l : SkewMonoidAlgebra k G
a : ∀ (x : G''), (equivMapDomain (f.trans g) l).coeff x = (equivMapDomain g (equivMapDomain f l)).coeff x
⊢ equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l)

Tactic:
ext x
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
G' : Type u_4
G'' : Type u_5
f : G ≃ G'
g : G' ≃ G''
l : SkewMonoidAlgebra k G
x : G''
⊢ (equivMapDomain (f.trans g) l).coeff x = (equivMapDomain g (equivMapDomain f l)).coeff x

Tactic:
rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
l : SkewMonoidAlgebra k G
a : ∀ (x : G), (equivMapDomain (Equiv.refl G) l).coeff x = l.coeff x
⊢ equivMapDomain (Equiv.refl G) l = l

Tactic:
ext x
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
l : SkewMonoidAlgebra k G
x : G
⊢ (equivMapDomain (Equiv.refl G) l).coeff x = l.coeff x

Tactic:
rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : AddCommMonoid k
f : G ≃ H
a : G
b : k
a₁ : Eq (α := H →₀ k) (toFinsupp (equivMapDomain f (single a b))) (toFinsupp (single ((f : (a : G) → H) a) b))
⊢ Eq (α := SkewMonoidAlgebra k H) (equivMapDomain f (single a b)) (single ((f : (a : G) → H) a) b)

Tactic:
apply toFinsupp_injective

Premises used: SkewMonoidAlgebra.toFinsupp_injective
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : AddCommMonoid k
f : G ≃ H
a : G
b : k
a₁ : Eq (α := H →₀ k) (Finsupp.equivMapDomain f (toFinsupp (single a b))) (toFinsupp (single ((f : (a : G) → H) a) b))
a₂ : Eq (α := H →₀ k) (Finsupp.equivMapDomain f (Finsupp.single a b)) (Finsupp.single ((f : (a : G) → H) a) b)
⊢ Eq (α := H →₀ k) (toFinsupp (equivMapDomain f (single a b))) (toFinsupp (single ((f : (a : G) → H) a) b))

Tactic:
simp_rw [toFinsupp_equivMapDomain, single, Finsupp.equivMapDomain_single]

Premises used: Finsupp.equivMapDomain_single, SkewMonoidAlgebra.toFinsupp_equivMapDomain, SkewMonoidAlgebra.single
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : AddCommMonoid k
f : G ≃ H
a : G
b : k
a₁ : Eq (α := H →₀ k) (toFinsupp (equivMapDomain f (single a b))) (toFinsupp (single ((f : (a : G) → H) a) b))
⊢ Eq (α := SkewMonoidAlgebra k H) (equivMapDomain f (single a b)) (single ((f : (a : G) → H) a) b)

Tactic:
classical
  apply toFinsupp_injective
  simp_rw [toFinsupp_equivMapDomain, single, Finsupp.equivMapDomain_single]

Premises used: Finsupp.equivMapDomain_single, SkewMonoidAlgebra.toFinsupp_injective, SkewMonoidAlgebra.toFinsupp_equivMapDomain, SkewMonoidAlgebra.single
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst : AddCommMonoid A
e : G ≃ H
v : SkewMonoidAlgebra A G
⊢ equivMapDomain e.symm (equivMapDomain e v) = v

Tactic:
simp [← equivMapDomain_trans]

Premises used: SkewMonoidAlgebra.equivMapDomain_trans
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst : AddCommMonoid A
e : G ≃ H
v : SkewMonoidAlgebra A H
⊢ equivMapDomain e (equivMapDomain e.symm v) = v

Tactic:
simp [← equivMapDomain_trans]

Premises used: SkewMonoidAlgebra.equivMapDomain_trans
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst : AddCommMonoid A
e : G ≃ H
a b : SkewMonoidAlgebra A G
⊢ equivMapDomain e (a + b) = equivMapDomain e a + equivMapDomain e b

Tactic:
simp [equivMapDomain_eq_mapDomain, map_add]

Premises used: map_add, SkewMonoidAlgebra.equivMapDomain_eq_mapDomain
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst : Semiring k
inst_1 : AddCommMonoid A
inst_2 : Module k A
e : G ≃ H
c : k
x : SkewMonoidAlgebra A G
simp_rw :
  (mapDomain (⇑e : (a : G) → H) : (a : SkewMonoidAlgebra A G) → SkewMonoidAlgebra A H) (c • x) =
    HSMul.hSMul (β := SkewMonoidAlgebra A H) c
      ((mapDomain (⇑e : (a : G) → H) : (a : SkewMonoidAlgebra A G) → SkewMonoidAlgebra A H) x : SkewMonoidAlgebra A H)
⊢ equivMapDomain e (c • x) = c • equivMapDomain e x

Tactic:
simp_rw [equivMapDomain_eq_mapDomain, mapDomain_smul]

Premises used: SkewMonoidAlgebra.mapDomain_smul, SkewMonoidAlgebra.equivMapDomain_eq_mapDomain
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst : Monoid G
inst_1 : Monoid H
inst_2 : Semiring A
inst_3 : CommSemiring k
inst_4 : Algebra k A
inst_5 : MulSemiringAction G A
inst_6 : MulSemiringAction H A
inst_7 : SMulCommClass G k A
inst_8 : SMulCommClass H k A
e : G ≃* H
he : ∀ (a : G) (x : A), a • x = HSMul.hSMul.{u_3, u_4, u_4} (α := H) ((e : (a : G) → H) a : H) x
⊢ Eq (α := SkewMonoidAlgebra A G →ₐ[k] SkewMonoidAlgebra A H)
    (↑(domCongrAlg k A he) : SkewMonoidAlgebra A G →ₐ[k] SkewMonoidAlgebra A H) (mapDomainAlgHom k A he)

Tactic:
AlgHom.ext <| fun _ ↦ equivMapDomain_eq_mapDomain _ _

Premises used: AlgHom.ext, EquivLike.toEquiv, SkewMonoidAlgebra.equivMapDomain_eq_mapDomain
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst : Monoid G
inst_1 : Monoid H
inst_2 : Semiring A
inst_3 : CommSemiring k
inst_4 : Algebra k A
inst_5 : MulSemiringAction G A
inst_6 : MulSemiringAction H A
inst_7 : SMulCommClass G k A
inst_8 : SMulCommClass H k A
e : G ≃* H
he : ∀ (a : G) (x : A), a • x = HSMul.hSMul.{u_3, u_4, u_4} (α := H) ((e : (a : G) → H) a : H) x
f : SkewMonoidAlgebra A G
h : H
⊢ coeff ((domCongrAlg k A he : (a : SkewMonoidAlgebra A G) → SkewMonoidAlgebra A H) f) h =
    f.coeff ((e.symm : (a : H) → G) h)

Tactic:
rfl

Premises used: SkewMonoidAlgebra.equivMapDomain, rfl, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst : Monoid G
inst_1 : Monoid H
inst_2 : Semiring A
inst_3 : CommSemiring k
inst_4 : Algebra k A
inst_5 : MulSemiringAction G A
inst_6 : MulSemiringAction H A
inst_7 : SMulCommClass G k A
inst_8 : SMulCommClass H k A
e : G ≃* H
he : ∀ (a : G) (x : A), a • x = HSMul.hSMul.{u_3, u_4, u_4} (α := H) ((e : (a : G) → H) a : H) x
f : SkewMonoidAlgebra A G
⊢ support.{u_4, u_3} (k := A) ((domCongrAlg k A he : (a : SkewMonoidAlgebra A G) → SkewMonoidAlgebra A H) f) =
    Finset.map (↑e : G ≃ H).toEmbedding f.support

Tactic:
rfl

Premises used: Finset.map, SkewMonoidAlgebra.support, rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst : Monoid G
inst_1 : Monoid H
inst_2 : Semiring A
inst_3 : CommSemiring k
inst_4 : Algebra k A
inst_5 : MulSemiringAction G A
inst_6 : MulSemiringAction H A
inst_7 : SMulCommClass G k A
inst_8 : SMulCommClass H k A
e : G ≃* H
he : ∀ (a : G) (x : A), a • x = HSMul.hSMul.{u_3, u_4, u_4} (α := H) ((e : (a : G) → H) a : H) x
g : G
a : A
⊢ Eq (α := SkewMonoidAlgebra A H)
    ((domCongrAlg k A he : (a : SkewMonoidAlgebra A G) → SkewMonoidAlgebra A H) (single g a) : SkewMonoidAlgebra A H)
    (single ((e : (a : G) → H) g) a : SkewMonoidAlgebra A H)

Tactic:
equivMapDomain_single ..

Premises used: SkewMonoidAlgebra.equivMapDomain, SkewMonoidAlgebra.equivMapDomain_single
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
A : Type u_4
inst : Monoid G
inst_1 : Semiring A
inst_2 : CommSemiring k
inst_3 : Algebra k A
inst_4 : MulSemiringAction G A
inst_5 : SMulCommClass G k A
h :
  ∀ (a : SkewMonoidAlgebra A G),
    Eq (α := SkewMonoidAlgebra A G)
      ((domCongrAlg k A (e := MulEquiv.refl G) ⋯ : (a : SkewMonoidAlgebra A G) → SkewMonoidAlgebra A G) a :
        SkewMonoidAlgebra A G)
      ((AlgEquiv.refl : (a : SkewMonoidAlgebra A G) → SkewMonoidAlgebra A G) a : SkewMonoidAlgebra A G)
⊢ Eq (α := SkewMonoidAlgebra A G ≃ₐ[k] SkewMonoidAlgebra A G) (domCongrAlg k A (e := MulEquiv.refl G) ⋯) AlgEquiv.refl

Tactic:
apply AlgEquiv.ext

Premises used: AlgEquiv.ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
A : Type u_4
inst : Monoid G
inst_1 : Semiring A
inst_2 : CommSemiring k
inst_3 : Algebra k A
inst_4 : MulSemiringAction G A
inst_5 : SMulCommClass G k A
⊢ ∀ (a : SkewMonoidAlgebra A G),
    Eq (α := SkewMonoidAlgebra A G)
      ((domCongrAlg k A (e := MulEquiv.refl G) ⋯ : (a : SkewMonoidAlgebra A G) → SkewMonoidAlgebra A G) a :
        SkewMonoidAlgebra A G)
      ((AlgEquiv.refl : (a : SkewMonoidAlgebra A G) → SkewMonoidAlgebra A G) a : SkewMonoidAlgebra A G)

Tactic:
aesop
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst : Monoid G
inst_1 : Monoid H
inst_2 : Semiring A
inst_3 : CommSemiring k
inst_4 : Algebra k A
inst_5 : MulSemiringAction G A
inst_6 : MulSemiringAction H A
inst_7 : SMulCommClass G k A
inst_8 : SMulCommClass H k A
e : G ≃* H
he : ∀ (a : G) (x : A), a • x = HSMul.hSMul.{u_3, u_4, u_4} (α := H) ((e : (a : G) → H) a : H) x
a : H
x : A
rw : a • x = HSMul.hSMul.{u_3, u_4, u_4} (α := H) ((e : (a : G) → H) ((e.symm : (a : H) → G) a : G) : H) x
rw₁ rw₂ : a • x = a • x
⊢ a • x = HSMul.hSMul.{u_2, u_4, u_4} (α := G) ((e.symm : (a : H) → G) a : G) x

Tactic:
rw [he, MulEquiv.apply_symm_apply]

Premises used: MulEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst : Monoid G
inst_1 : Monoid H
inst_2 : Semiring A
inst_3 : CommSemiring k
inst_4 : Algebra k A
inst_5 : MulSemiringAction G A
inst_6 : MulSemiringAction H A
inst_7 : SMulCommClass G k A
inst_8 : SMulCommClass H k A
e : G ≃* H
he : ∀ (a : G) (x : A), a • x = HSMul.hSMul.{u_3, u_4, u_4} (α := H) ((e : (a : G) → H) a : H) x
⊢ Eq (α := SkewMonoidAlgebra A H ≃ₐ[k] SkewMonoidAlgebra A G) (AlgEquiv.symm (domCongrAlg k A he))
    (domCongrAlg k A (e := e.symm) ⋯)

Tactic:
rfl

Premises used: SkewMonoidAlgebra.equivMapDomain, AlgEquiv.symm, SkewMonoidAlgebra.domCongrAlg, AlgEquiv.ofLinearEquiv, Equiv.symm, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
V : Type u_4
inst_3 : AddCommMonoid V
inst_4 : Module k V
inst_5 : Module (SkewMonoidAlgebra k G) V
inst_6 : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h :
  ∀ (g : G),
    ∀ v ∈ W,
      HSMul.hSMul (α := SkewMonoidAlgebra k G) ((of k G : (a : G) → SkewMonoidAlgebra k G) g : SkewMonoidAlgebra k G)
          v ∈
        W
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ (↑W : Set V)
rw :
  ∑ i ∈ f.toFinsupp.support,
      HSMul.hSMul (α := SkewMonoidAlgebra k G) (single i ((f.toFinsupp : (a : G) → k) i) : SkewMonoidAlgebra k G) v ∈
    (↑W : Set V)
⊢ f • v ∈ (↑W : Set V)

Tactic:
rw [← sum_single f, sum_def, Finsupp.sum, Finset.sum_smul]

Premises used: Finset.sum_smul, SkewMonoidAlgebra.sum_def, Finsupp.sum, SkewMonoidAlgebra.sum_single
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
V : Type u_4
inst_3 : AddCommMonoid V
inst_4 : Module k V
inst_5 : Module (SkewMonoidAlgebra k G) V
inst_6 : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h :
  ∀ (g : G),
    ∀ v ∈ W,
      HSMul.hSMul (α := SkewMonoidAlgebra k G) ((of k G : (a : G) → SkewMonoidAlgebra k G) g : SkewMonoidAlgebra k G)
          v ∈
        W
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ (↑W : Set V)
simp_rw :
  ∑ x ∈ f.toFinsupp.support,
      HSMul.hSMul.{u_1, u_4, u_4} (α := k) ((f.toFinsupp : (a : G) → k) x : k)
        (HSMul.hSMul (α := SkewMonoidAlgebra k G) ((of k G : (a : G) → SkewMonoidAlgebra k G) x : SkewMonoidAlgebra k G)
          v) ∈
    (↑W : Set V)
⊢ ∑ i ∈ f.toFinsupp.support,
      HSMul.hSMul (α := SkewMonoidAlgebra k G) (single i ((f.toFinsupp : (a : G) → k) i) : SkewMonoidAlgebra k G) v ∈
    (↑W : Set V)

Tactic:
simp_rw [← smul_of, smul_assoc]

Premises used: SkewMonoidAlgebra.smul_of, smul_assoc
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
V : Type u_4
inst_3 : AddCommMonoid V
inst_4 : Module k V
inst_5 : Module (SkewMonoidAlgebra k G) V
inst_6 : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h :
  ∀ (g : G),
    ∀ v ∈ W,
      HSMul.hSMul (α := SkewMonoidAlgebra k G) ((of k G : (a : G) → SkewMonoidAlgebra k G) g : SkewMonoidAlgebra k G)
          v ∈
        W
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ (↑W : Set V)
⊢ ∑ x ∈ f.toFinsupp.support,
      HSMul.hSMul.{u_1, u_4, u_4} (α := k) ((f.toFinsupp : (a : G) → k) x : k)
        (HSMul.hSMul (α := SkewMonoidAlgebra k G) ((of k G : (a : G) → SkewMonoidAlgebra k G) x : SkewMonoidAlgebra k G)
          v) ∈
    (↑W : Set V)

Tactic:
Submodule.sum_smul_mem W _ fun g _ ↦ h g v hv

Premises used: Submodule.sum_smul_mem
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
V : Type u_4
inst_3 : AddCommMonoid V
inst_4 : Module k V
inst_5 : Module (SkewMonoidAlgebra k G) V
inst_6 : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h :
  ∀ (g : G),
    ∀ v ∈ W,
      HSMul.hSMul (α := SkewMonoidAlgebra k G) ((of k G : (a : G) → SkewMonoidAlgebra k G) g : SkewMonoidAlgebra k G)
          v ∈
        W
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ (↑W : Set V)
⊢ ∑ x ∈ f.toFinsupp.support,
      HSMul.hSMul.{u_1, u_4, u_4} (α := k) ((f.toFinsupp : (a : G) → k) x : k)
        (HSMul.hSMul (α := SkewMonoidAlgebra k G) ((of k G : (a : G) → SkewMonoidAlgebra k G) x : SkewMonoidAlgebra k G)
          v) ∈
    (↑W : Set V)

Tactic:
exact Submodule.sum_smul_mem W _ fun g _ ↦ h g v hv

Premises used: Submodule.sum_smul_mem
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a a' : α
b : M
f : SkewMonoidAlgebra M α
⊢ Eq (α := SkewMonoidAlgebra M α) { toFinsupp := Finsupp.erase a (toFinsupp 0) } 0

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Single
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a a' : α
b : M
f : SkewMonoidAlgebra M α
⊢ ∀ (x y : SkewMonoidAlgebra M α),
    { toFinsupp := Finsupp.erase a (x + y).toFinsupp : SkewMonoidAlgebra M α } =
      { toFinsupp := Finsupp.erase a x.toFinsupp : SkewMonoidAlgebra M α } +
        { toFinsupp := Finsupp.erase a y.toFinsupp : SkewMonoidAlgebra M α }

Tactic:
simp