awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
A : Type u_6
inst : NonUnitalNonAssocSemiring A
inst_1 : Monoid G
inst_2 : Semiring k
inst_3 : MulSemiringAction G k
inst_4 : DistribMulAction k A
φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A
h :
  ∀ (x : G),
    Eq.{u_6 + 1} (α := A) ((φ₁ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
      ((φ₂ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
h₁ : Eq (α := SkewMonoidAlgebra k G →+[k] A) (↑φ₁ : SkewMonoidAlgebra k G →+[k] A) (↑φ₂ : SkewMonoidAlgebra k G →+[k] A)
⊢ φ₁ = φ₂

Tactic:
apply NonUnitalAlgHom.to_distribMulActionHom_injective

Premises used: NonUnitalAlgHom.to_distribMulActionHom_injective
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
A : Type u_6
inst : NonUnitalNonAssocSemiring A
inst_1 : Monoid G
inst_2 : Semiring k
inst_3 : MulSemiringAction G k
inst_4 : DistribMulAction k A
φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A
h :
  ∀ (x : G),
    Eq.{u_6 + 1} (α := A) ((φ₁ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
      ((φ₂ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
h₁ :
  ∀ (a : G),
    Eq (α := k →+[k] A) (DistribMulActionHom.comp (↑φ₁ : SkewMonoidAlgebra k G →+[k] A) (DistribMulActionHom.single a))
      (DistribMulActionHom.comp (↑φ₂ : SkewMonoidAlgebra k G →+[k] A) (DistribMulActionHom.single a))
⊢ Eq (α := SkewMonoidAlgebra k G →+[k] A) (↑φ₁ : SkewMonoidAlgebra k G →+[k] A) (↑φ₂ : SkewMonoidAlgebra k G →+[k] A)

Tactic:
apply distribMulActionHom_ext'

Premises used: SkewMonoidAlgebra.distribMulActionHom_ext'
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
A : Type u_6
inst : NonUnitalNonAssocSemiring A
inst_1 : Monoid G
inst_2 : Semiring k
inst_3 : MulSemiringAction G k
inst_4 : DistribMulAction k A
φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A
h :
  ∀ (x : G),
    Eq.{u_6 + 1} (α := A) ((φ₁ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
      ((φ₂ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
a : G
h₁ :
  Eq.{u_6 + 1} (α := A)
    ((DistribMulActionHom.comp (↑φ₁ : SkewMonoidAlgebra k G →+[k] A) (DistribMulActionHom.single a) : (a : k) → A) 1 :
      A)
    ((DistribMulActionHom.comp (↑φ₂ : SkewMonoidAlgebra k G →+[k] A) (DistribMulActionHom.single a) : (a : k) → A) 1 :
      A)
⊢ Eq (α := k →+[k] A) (DistribMulActionHom.comp (↑φ₁ : SkewMonoidAlgebra k G →+[k] A) (DistribMulActionHom.single a))
    (DistribMulActionHom.comp (↑φ₂ : SkewMonoidAlgebra k G →+[k] A) (DistribMulActionHom.single a))

Tactic:
ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
A : Type u_6
inst : NonUnitalNonAssocSemiring A
inst_1 : Monoid G
inst_2 : Semiring k
inst_3 : MulSemiringAction G k
inst_4 : DistribMulAction k A
φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A
h :
  ∀ (x : G),
    Eq.{u_6 + 1} (α := A) ((φ₁ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
      ((φ₂ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
a : G
⊢ Eq.{u_6 + 1} (α := A)
    ((DistribMulActionHom.comp (↑φ₁ : SkewMonoidAlgebra k G →+[k] A) (DistribMulActionHom.single a) : (a : k) → A) 1 :
      A)
    ((DistribMulActionHom.comp (↑φ₂ : SkewMonoidAlgebra k G →+[k] A) (DistribMulActionHom.single a) : (a : k) → A) 1 :
      A)

Tactic:
simp [singleAddHom_apply, h]

Premises used: SkewMonoidAlgebra.singleAddHom_apply
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
A : Type u_6
inst : NonUnitalNonAssocSemiring A
inst_1 : Monoid G
inst_2 : Semiring k
inst_3 : MulSemiringAction G k
inst_4 : DistribMulAction k A
φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A
h :
  φ₁.toMulHom.comp (↑(of k G) : G →ₙ* SkewMonoidAlgebra k G) =
    φ₂.toMulHom.comp (↑(of k G) : G →ₙ* SkewMonoidAlgebra k G)
⊢ φ₁ = φ₂

Tactic:
nonUnitalAlgHom_ext <| DFunLike.congr_fun h

Premises used: DFunLike.congr_fun, SkewMonoidAlgebra.nonUnitalAlgHom_ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : CommSemiring k
A : Type u_3
inst_2 : Semiring A
inst_3 : Algebra k A
inst_4 : MulSemiringAction G A
inst_5 : SMulCommClass G k A
r : k
f : SkewMonoidAlgebra A G
a :
  ∀ (a : G),
    (HMul.hMul (α := SkewMonoidAlgebra A G)
            ((RingHom.comp singleOneRingHom (algebraMap k A) : (a : k) → SkewMonoidAlgebra A G) r :
              SkewMonoidAlgebra A G)
            f).coeff
        a =
      (HMul.hMul (β := SkewMonoidAlgebra A G) f
            ((RingHom.comp singleOneRingHom (algebraMap k A) : (a : k) → SkewMonoidAlgebra A G) r :
              SkewMonoidAlgebra A G)).coeff
        a
⊢ HMul.hMul (α := SkewMonoidAlgebra A G)
      ((RingHom.comp singleOneRingHom (algebraMap k A) : (a : k) → SkewMonoidAlgebra A G) r : SkewMonoidAlgebra A G) f =
    HMul.hMul (β := SkewMonoidAlgebra A G) f
      ((RingHom.comp singleOneRingHom (algebraMap k A) : (a : k) → SkewMonoidAlgebra A G) r : SkewMonoidAlgebra A G)

Tactic:
ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : CommSemiring k
A : Type u_3
inst_2 : Semiring A
inst_3 : Algebra k A
inst_4 : MulSemiringAction G A
inst_5 : SMulCommClass G k A
r : k
f : SkewMonoidAlgebra A G
a : G
⊢ (HMul.hMul (α := SkewMonoidAlgebra A G)
          ((RingHom.comp singleOneRingHom (algebraMap k A) : (a : k) → SkewMonoidAlgebra A G) r : SkewMonoidAlgebra A G)
          f).coeff
      a =
    (HMul.hMul (β := SkewMonoidAlgebra A G) f
          ((RingHom.comp singleOneRingHom (algebraMap k A) : (a : k) → SkewMonoidAlgebra A G) r :
            SkewMonoidAlgebra A G)).coeff
      a

Tactic:
simp only [singleOneRingHom, singleAddHom, ZeroHom.toFun_eq_coe, ZeroHom.coe_mk, RingHom.coe_mk,
      MonoidHom.coe_mk, OneHom.coe_mk, coeff_single_one_mul, Algebra.commutes, coeff_mul_single_one,
      smul_algebraMap, RingHom.coe_comp, comp_apply]

Premises used: SkewMonoidAlgebra.coeff_single_one_mul, OneHom.coe_mk, SkewMonoidAlgebra.singleOneRingHom, smul_algebraMap, SkewMonoidAlgebra.singleAddHom, ZeroHom.coe_mk, MonoidHom.coe_mk, SkewMonoidAlgebra.coeff_mul_single_one, RingHom.coe_mk, RingHom.coe_comp, Function.comp_apply, Algebra.commutes, ZeroHom.toFun_eq_coe
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : CommSemiring k
A : Type u_3
inst_2 : Semiring A
inst_3 : Algebra k A
inst_4 : MulSemiringAction G A
inst_5 : SMulCommClass G k A
r : k
a : SkewMonoidAlgebra A G
a₁ :
  ∀ (a_1 : G),
    (r • a).coeff a_1 =
      (HMul.hMul (α := SkewMonoidAlgebra A G)
            ((RingHom.comp singleOneRingHom (algebraMap k A) : (a : k) → SkewMonoidAlgebra A G) r :
              SkewMonoidAlgebra A G)
            a).coeff
        a_1
⊢ r • a =
    HMul.hMul (α := SkewMonoidAlgebra A G)
      ((RingHom.comp singleOneRingHom (algebraMap k A) : (a : k) → SkewMonoidAlgebra A G) r : SkewMonoidAlgebra A G) a

Tactic:
ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : CommSemiring k
A : Type u_3
inst_2 : Semiring A
inst_3 : Algebra k A
inst_4 : MulSemiringAction G A
inst_5 : SMulCommClass G k A
r : k
a : SkewMonoidAlgebra A G
a_1 : G
⊢ (r • a).coeff a_1 =
    (HMul.hMul (α := SkewMonoidAlgebra A G)
          ((RingHom.comp singleOneRingHom (algebraMap k A) : (a : k) → SkewMonoidAlgebra A G) r : SkewMonoidAlgebra A G)
          a).coeff
      a_1

Tactic:
simp only [RingHom.coe_comp, comp_apply, coeff_smul, Algebra.smul_def, singleOneRingHom,
      singleAddHom, ZeroHom.toFun_eq_coe, ZeroHom.coe_mk, RingHom.coe_mk, MonoidHom.coe_mk,
      OneHom.coe_mk, coeff_single_one_mul]

Premises used: SkewMonoidAlgebra.coeff_single_one_mul, OneHom.coe_mk, SkewMonoidAlgebra.singleOneRingHom, SkewMonoidAlgebra.singleAddHom, ZeroHom.coe_mk, MonoidHom.coe_mk, RingHom.coe_mk, RingHom.coe_comp, Algebra.smul_def, Function.comp_apply, SkewMonoidAlgebra.coeff_smul, ZeroHom.toFun_eq_coe
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : CommSemiring k
A : Type u_3
inst_2 : Semiring A
inst_3 : Algebra k A
inst_4 : MulSemiringAction G A
inst_5 : SMulCommClass G k A
⊢ Eq (α := (a : k) → SkewMonoidAlgebra A G) (⇑(algebraMap k (SkewMonoidAlgebra A G)) : (a : k) → SkewMonoidAlgebra A G)
    (single 1 ∘ (⇑(algebraMap k A) : (a : k) → A))

Tactic:
rfl

Premises used: SkewMonoidAlgebra.single, rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : CommSemiring k
inst_2 : MulSemiringAction G k
inst_3 : SMulCommClass G k k
a : G
b : k
⊢ single a b =
    HMul.hMul (α := SkewMonoidAlgebra k G) (β := SkewMonoidAlgebra k G)
      ((algebraMap k (SkewMonoidAlgebra k G) : (a : k) → SkewMonoidAlgebra k G) b : SkewMonoidAlgebra k G)
      ((of k G : (a : G) → SkewMonoidAlgebra k G) a : SkewMonoidAlgebra k G)

Tactic:
simp [coe_algebraMap, comp_apply, of_apply, single_mul_single, one_mul, smul_one, mul_one]

Premises used: SkewMonoidAlgebra.of_apply, SkewMonoidAlgebra.single_mul_single, SkewMonoidAlgebra.coe_algebraMap, MulDistribMulAction.smul_one, Function.comp_apply, mul_one, one_mul
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : CommSemiring k
A : Type u_3
inst_2 : Semiring A
inst_3 : Algebra k A
a : G
b : k
inst_4 : MulSemiringAction G A
inst_5 : SMulCommClass G k A
⊢ single a ((algebraMap k A : (a : k) → A) b) =
    HMul.hMul (α := SkewMonoidAlgebra A G) (β := SkewMonoidAlgebra A G)
      ((algebraMap k (SkewMonoidAlgebra A G) : (a : k) → SkewMonoidAlgebra A G) b : SkewMonoidAlgebra A G)
      ((of A G : (a : G) → SkewMonoidAlgebra A G) a : SkewMonoidAlgebra A G)

Tactic:
simp [coe_algebraMap, comp_apply, of_apply, single_mul_single, one_mul, smul_one, mul_one]

Premises used: SkewMonoidAlgebra.of_apply, SkewMonoidAlgebra.single_mul_single, SkewMonoidAlgebra.coe_algebraMap, MulDistribMulAction.smul_one, Function.comp_apply, mul_one, one_mul
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : CommSemiring k
A : Type u_3
inst_2 : Semiring A
inst_3 : Algebra k A
inst_4 : MulSemiringAction G k
inst_5 : SMulCommClass G k k
φ₁ φ₂ : SkewMonoidAlgebra k G →ₐ[k] A
h :
  ∀ (x : G),
    Eq.{u_3 + 1} (α := A) ((φ₁ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
      ((φ₂ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
⊢ φ₁ = φ₂

Tactic:
AlgHom.toLinearMap_injective (lhom_ext' fun a ↦ (LinearMap.ext_ring (h a)))

Premises used: SkewMonoidAlgebra.lhom_ext', AlgHom.toLinearMap_injective, LinearMap.ext_ring
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : CommSemiring k
A : Type u_3
inst_2 : Semiring A
inst_3 : Algebra k A
inst_4 : MulSemiringAction G k
inst_5 : SMulCommClass G k k
φ₁ φ₂ : SkewMonoidAlgebra k G →ₐ[k] A
h :
  Eq (α := G →* A) (MonoidHom.comp (↑φ₁ : SkewMonoidAlgebra k G →* A) (of k G))
    (MonoidHom.comp (↑φ₂ : SkewMonoidAlgebra k G →* A) (of k G))
⊢ φ₁ = φ₂

Tactic:
algHom_ext <| DFunLike.congr_fun h

Premises used: DFunLike.congr_fun, SkewMonoidAlgebra.algHom_ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : Monoid H
A : Type u_4
B : Type u_5
inst_3 : Semiring A
inst_4 : Algebra k A
inst_5 : Semiring B
inst_6 : Algebra k B
inst_7 : MulSemiringAction G A
inst_8 : SMulCommClass G k A
f : A →ₐ[k] B
g : G →* B
h_comm :
  ∀ {x : A} {y : G},
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (y • x) : B) ((g : (a : G) → B) y : B) =
      HMul.hMul (α := B) (β := B) ((g : (a : G) → B) y : B) ((f : (a : A) → B) x : B)
⊢ ∀ (r : k),
    OneHom.toFun (M := SkewMonoidAlgebra A G)
        (↑(↑(liftNCRingHom (↑f : A →+* B) g ⋯) : SkewMonoidAlgebra A G →* B) : OneHom (SkewMonoidAlgebra A G) B)
        ((algebraMap k (SkewMonoidAlgebra A G) : (a : k) → SkewMonoidAlgebra A G) r) =
      (algebraMap k B : (a : k) → B) r

Tactic:
simp [liftNCRingHom]

Premises used: SkewMonoidAlgebra.liftNCRingHom
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : Monoid H
A : Type u_4
B : Type u_5
inst_3 : Semiring A
inst_4 : Algebra k A
inst_5 : Semiring B
inst_6 : Algebra k B
inst_7 : MulSemiringAction G k
inst_8 : SMulCommClass G k k
F : G →* A
apply :
  ∀ {x : k} {y : G},
    HMul.hMul (α := A) (β := A) ((Algebra.ofId k A : (a : k) → A) (y • x) : A) ((F : (a : G) → A) y : A) =
      HMul.hMul (α := A) (β := A) ((F : (a : G) → A) y : A) ((Algebra.ofId k A : (a : k) → A) x : A)
⊢ SkewMonoidAlgebra k G →ₐ[k] A

Tactic:
apply liftNCAlgHom (Algebra.ofId k A) F

Premises used: SkewMonoidAlgebra.liftNCAlgHom, Algebra.ofId
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : Monoid H
A : Type u_4
B : Type u_5
inst_3 : Semiring A
inst_4 : Algebra k A
inst_5 : Semiring B
inst_6 : Algebra k B
inst_7 : MulSemiringAction G k
inst_8 : SMulCommClass G k k
F : G →* A
⊢ ∀ (g : G) (r : k), g • r = r

Tactic:
fun _ _ ↦ smul_algebraMap _ (algebraMap k k _)

Premises used: Algebra.algebraMap, smul_algebraMap, DFunLike.coe
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : Monoid H
A : Type u_4
B : Type u_5
inst_3 : Semiring A
inst_4 : Algebra k A
inst_5 : Semiring B
inst_6 : Algebra k B
inst_7 : MulSemiringAction G k
inst_8 : SMulCommClass G k k
F : G →* A
⊢ ∀ (g : G) (r : k), g • r = r

Tactic:
exact fun _ _ ↦ smul_algebraMap _ (algebraMap k k _)

Premises used: Algebra.algebraMap, smul_algebraMap, DFunLike.coe
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : Monoid H
A : Type u_4
B : Type u_5
inst_3 : Semiring A
inst_4 : Algebra k A
inst_5 : Semiring B
inst_6 : Algebra k B
inst_7 : MulSemiringAction G k
inst_8 : SMulCommClass G k k
F : G →* A
simp_rw :
  ∀ {x : k} {y : G},
    HMul.hMul (α := A) (β := A) ((Algebra.ofId k A : (a : k) → A) x : A) ((F : (a : G) → A) y : A) =
      HMul.hMul (α := A) (β := A) ((F : (a : G) → A) y : A) ((Algebra.ofId k A : (a : k) → A) x : A)
⊢ ∀ {x : k} {y : G},
    HMul.hMul (α := A) (β := A) ((Algebra.ofId k A : (a : k) → A) (y • x) : A) ((F : (a : G) → A) y : A) =
      HMul.hMul (α := A) (β := A) ((F : (a : G) → A) y : A) ((Algebra.ofId k A : (a : k) → A) x : A)

Tactic:
simp_rw [show ∀ (g : G) (r : k), g • r = r by
        exact fun _ _ ↦ smul_algebraMap _ (algebraMap k k _)]
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : Monoid H
A : Type u_4
B : Type u_5
inst_3 : Semiring A
inst_4 : Algebra k A
inst_5 : Semiring B
inst_6 : Algebra k B
inst_7 : MulSemiringAction G k
inst_8 : SMulCommClass G k k
F : G →* A
x : k
y : G
⊢ HMul.hMul (α := A) (β := A) ((Algebra.ofId k A : (a : k) → A) x : A) ((F : (a : G) → A) y : A) =
    HMul.hMul (α := A) (β := A) ((F : (a : G) → A) y : A) ((Algebra.ofId k A : (a : k) → A) x : A)

Tactic:
Algebra.commutes _ _

Premises used: Algebra.commutes
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : Monoid H
A : Type u_4
B : Type u_5
inst_3 : Semiring A
inst_4 : Algebra k A
inst_5 : Semiring B
inst_6 : Algebra k B
inst_7 : MulSemiringAction G k
inst_8 : SMulCommClass G k k
F : G →* A
⊢ ∀ {x : k} {y : G},
    HMul.hMul (α := A) (β := A) ((Algebra.ofId k A : (a : k) → A) x : A) ((F : (a : G) → A) y : A) =
      HMul.hMul (α := A) (β := A) ((F : (a : G) → A) y : A) ((Algebra.ofId k A : (a : k) → A) x : A)

Tactic:
exact Algebra.commutes _ _

Premises used: Algebra.commutes
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : Monoid H
A : Type u_4
B : Type u_5
inst_3 : Semiring A
inst_4 : Algebra k A
inst_5 : Semiring B
inst_6 : Algebra k B
inst_7 : MulSemiringAction G k
inst_8 : SMulCommClass G k k
f : G →* A
h :
  ∀ (x : G),
    Eq.{u_4 + 1} (α := A)
      (((fun (f : SkewMonoidAlgebra k G →ₐ[k] A) ↦ (MonoidHom.comp (↑f : SkewMonoidAlgebra k G →* A) (of k G) : G →* A))
              ((fun (F : G →* A) ↦ (liftNCAlgHom (Algebra.ofId k A) F ⋯ : SkewMonoidAlgebra k G →ₐ[k] A)) f) :
            (a : G) → A)
          x :
        A)
      ((f : (a : G) → A) x : A)
⊢ (fun (f : SkewMonoidAlgebra k G →ₐ[k] A) ↦ (MonoidHom.comp (↑f : SkewMonoidAlgebra k G →* A) (of k G) : G →* A))
      ((fun (F : G →* A) ↦ (liftNCAlgHom (Algebra.ofId k A) F ⋯ : SkewMonoidAlgebra k G →ₐ[k] A)) f) =
    f

Tactic:
ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : Monoid H
A : Type u_4
B : Type u_5
inst_3 : Semiring A
inst_4 : Algebra k A
inst_5 : Semiring B
inst_6 : Algebra k B
inst_7 : MulSemiringAction G k
inst_8 : SMulCommClass G k k
f : G →* A
x : G
⊢ Eq.{u_4 + 1} (α := A)
    (((fun (f : SkewMonoidAlgebra k G →ₐ[k] A) ↦ (MonoidHom.comp (↑f : SkewMonoidAlgebra k G →* A) (of k G) : G →* A))
            ((fun (F : G →* A) ↦ (liftNCAlgHom (Algebra.ofId k A) F ⋯ : SkewMonoidAlgebra k G →ₐ[k] A)) f) :
          (a : G) → A)
        x :
      A)
    ((f : (a : G) → A) x : A)

Tactic:
simp [liftNCAlgHom, liftNCRingHom]

Premises used: SkewMonoidAlgebra.liftNCRingHom, SkewMonoidAlgebra.liftNCAlgHom
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : Monoid H
A : Type u_4
B : Type u_5
inst_3 : Semiring A
inst_4 : Algebra k A
inst_5 : Semiring B
inst_6 : Algebra k B
inst_7 : MulSemiringAction G k
inst_8 : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
h :
  ∀ (x : G),
    Eq.{u_4 + 1} (α := A)
      ((MonoidHom.comp
              (↑((fun (F : G →* A) ↦ (liftNCAlgHom (Algebra.ofId k A) F ⋯ : SkewMonoidAlgebra k G →ₐ[k] A))
                    ((fun (f : SkewMonoidAlgebra k G →ₐ[k] A) ↦
                        (MonoidHom.comp (↑f : SkewMonoidAlgebra k G →* A) (of k G) : G →* A))
                      F)) :
                SkewMonoidAlgebra k G →* A)
              (of k G) :
            (a : G) → A)
          x :
        A)
      ((MonoidHom.comp (↑F : SkewMonoidAlgebra k G →* A) (of k G) : (a : G) → A) x : A)
⊢ (fun (F : G →* A) ↦ (liftNCAlgHom (Algebra.ofId k A) F ⋯ : SkewMonoidAlgebra k G →ₐ[k] A))
      ((fun (f : SkewMonoidAlgebra k G →ₐ[k] A) ↦ (MonoidHom.comp (↑f : SkewMonoidAlgebra k G →* A) (of k G) : G →* A))
        F) =
    F

Tactic:
ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : Monoid H
A : Type u_4
B : Type u_5
inst_3 : Semiring A
inst_4 : Algebra k A
inst_5 : Semiring B
inst_6 : Algebra k B
inst_7 : MulSemiringAction G k
inst_8 : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
x : G
⊢ Eq.{u_4 + 1} (α := A)
    ((MonoidHom.comp
            (↑((fun (F : G →* A) ↦ (liftNCAlgHom (Algebra.ofId k A) F ⋯ : SkewMonoidAlgebra k G →ₐ[k] A))
                  ((fun (f : SkewMonoidAlgebra k G →ₐ[k] A) ↦
                      (MonoidHom.comp (↑f : SkewMonoidAlgebra k G →* A) (of k G) : G →* A))
                    F)) :
              SkewMonoidAlgebra k G →* A)
            (of k G) :
          (a : G) → A)
        x :
      A)
    ((MonoidHom.comp (↑F : SkewMonoidAlgebra k G →* A) (of k G) : (a : G) → A) x : A)

Tactic:
simp [liftNCAlgHom, liftNCRingHom]

Premises used: SkewMonoidAlgebra.liftNCRingHom, SkewMonoidAlgebra.liftNCAlgHom
-- 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
f : SkewMonoidAlgebra k G
⊢ Eq.{u_4 + 1} (α := A)
    ((((lift k G A : (a : G →* A) → SkewMonoidAlgebra k G →ₐ[k] A) F : SkewMonoidAlgebra k G →ₐ[k] A) :
          (a : SkewMonoidAlgebra k G) → A)
        f :
      A)
    (f.sum fun (a : G) (b : k) ↦
        HMul.hMul (α := A) (β := A) ((algebraMap k A : (a : k) → A) b : A) ((F : (a : G) → A) a : A) :
      A)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, SkewMonoidAlgebra.sum, Finset.sum, rfl
-- 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
f : SkewMonoidAlgebra k G
⊢ Eq.{u_4 + 1} (α := A)
    ((((lift k G A : (a : G →* A) → SkewMonoidAlgebra k G →ₐ[k] A) F : SkewMonoidAlgebra k G →ₐ[k] A) :
          (a : SkewMonoidAlgebra k G) → A)
        f :
      A)
    (f.sum fun (a : G) (b : k) ↦ HSMul.hSMul (β := A) b ((F : (a : G) → A) a : A) : A)

Tactic:
simp [lift_apply', Algebra.smul_def]

Premises used: SkewMonoidAlgebra.lift_apply', Algebra.smul_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 : G →* A
⊢ Eq (α := (a : SkewMonoidAlgebra k G) → A)
    (⇑((lift k G A : (a : G →* A) → SkewMonoidAlgebra k G →ₐ[k] A) F : SkewMonoidAlgebra k G →ₐ[k] A) :
      (a : SkewMonoidAlgebra k G) → A)
    (⇑(liftNC (↑(algebraMap k A) : k →+ A) (⇑F : (a : G) → A)) : (a : SkewMonoidAlgebra k G) → A)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, rfl
-- 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
x : G
⊢ Eq.{u_4 + 1} (α := A)
    ((((Equiv.symm (lift k G A) : (a : SkewMonoidAlgebra k G →ₐ[k] A) → G →* A) F : G →* A) : (a : G) → A) x : A)
    ((F : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)

Tactic:
rfl

Premises used: SkewMonoidAlgebra.single, rfl
-- 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
x : G
rw :
  Eq.{u_4 + 1} (α := 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 x 1) :
      A)
    ((F : (a : G) → A) x : A)
rw₁ :
  Eq.{u_4 + 1} (α := A)
    ((((Equiv.symm (lift k G A) : (a : SkewMonoidAlgebra k G →ₐ[k] A) → G →* A)
              ((lift k G A : (a : G →* A) → SkewMonoidAlgebra k G →ₐ[k] A) F) :
            G →* A) :
          (a : G) → A)
        x :
      A)
    ((F : (a : G) → A) x : A)
rw₂ rw₃ : Eq.{u_4 + 1} (α := A) ((F : (a : G) → A) x : A) ((F : (a : G) → A) x : A)
⊢ Eq.{u_4 + 1} (α := A)
    ((((lift k G A : (a : G →* A) → SkewMonoidAlgebra k G →ₐ[k] A) F : SkewMonoidAlgebra k G →ₐ[k] A) :
          (a : SkewMonoidAlgebra k G) → A)
        ((of k G : (a : G) → SkewMonoidAlgebra k G) x : SkewMonoidAlgebra k G) :
      A)
    ((F : (a : G) → A) x : A)

Tactic:
rw [of_apply, ← lift_symm_apply, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, SkewMonoidAlgebra.of_apply, SkewMonoidAlgebra.lift_symm_apply