awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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
⊢ SkewMonoidAlgebra k G →ₐ[k] A
have 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)
Tactic: apply liftNCAlgHom (Algebra.ofId k A) F
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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) (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)
have 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)
Tactic: simp_rw [show ∀ (g : G) (r : k), g • r = r by
        exact fun _ _ ↦ smul_algebraMap _ (algebraMap k k _)]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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
⊢ (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
have 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 sorry : SkewMonoidAlgebra k G →ₐ[k] A)) f) :
          (a : G) → A)
        x :
      A)
    ((f : (a : G) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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
⊢ (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
have h : ∀ (x : G),
  Eq.{u_4 + 1} (α := A)
    ((MonoidHom.comp
            (↑((fun (F : G →* A) ↦ (liftNCAlgHom (Algebra.ofId k A) F sorry : 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: ext
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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
⊢ 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)
have 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)
Tactic: rw [of_apply, ← lift_symm_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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)
⊢ 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)
have 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)
Tactic: rw [of_apply, ← lift_symm_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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)
⊢ 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)
have rw₂ : Eq.{u_4 + 1} (α := A) ((F : (a : G) → A) x : A) ((F : (a : G) → A) x : A)
Tactic: rw [of_apply, ← lift_symm_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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
⊢ (((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)
have 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)
Tactic: rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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)
⊢ (((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)
have 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)
Tactic: rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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)
⊢ (((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)
have 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)
Tactic: rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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)
⊢ (((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)
have 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)
Tactic: rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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
| ((F : (a : SkewMonoidAlgebra k G) → A) f : A)
have 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)
Tactic: rw [lift_unique' F]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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
| ((((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)
have simp : f.sum fun (a : G) (b : k) ↦ HSMul.hSMul (β := A) b ((F : (a : SkewMonoidAlgebra k G) → A) (single a 1) : A)
Tactic: simp [lift_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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
| ((F : (a : SkewMonoidAlgebra k G) → A) f : A)
have rw : f.sum fun (a : G) (b : k) ↦ HSMul.hSMul (β := A) b ((F : (a : SkewMonoidAlgebra k G) → A) (single a 1) : A)
Tactic: rw [lift_unique' F]
    simp [lift_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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
⊢ 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)
have 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)
Tactic: conv_lhs =>
    rw [lift_unique' F]
    simp [lift_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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)
⊢ 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)
have 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))
Tactic: conv_lhs =>
    rw [lift_unique' F]
    simp [lift_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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 = (mapDomain (⇑f : (a : G) → H) : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k H) l
have a : (equivMapDomain f l).toFinsupp =
  toFinsupp ((mapDomain (⇑f : (a : G) → H) : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k H) l)
Tactic: apply toFinsupp_injective
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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 =
    toFinsupp ((mapDomain (⇑f : (a : G) → H) : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k H) l)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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
⊢ 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)
have 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)
Tactic: simp_rw [toFinsupp_equivMapDomain, Finsupp.equivMapDomain_apply, toFinsupp_mapDomain,
    Finsupp.mapDomain_equiv_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [toFinsupp_equivMapDomain, Finsupp.equivMapDomain_apply, toFinsupp_mapDomain,
    Finsupp.mapDomain_equiv_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [toFinsupp_equivMapDomain, Finsupp.equivMapDomain_apply, toFinsupp_mapDomain,
    Finsupp.mapDomain_equiv_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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
⊢ equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l)
have a : ∀ (x : G''), (equivMapDomain (f.trans g) l).coeff x = (equivMapDomain g (equivMapDomain f l)).coeff x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
l : SkewMonoidAlgebra k G
⊢ equivMapDomain (Equiv.refl G) l = l
have a : ∀ (x : G), (equivMapDomain (Equiv.refl G) l).coeff x = l.coeff x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : AddCommMonoid k
f : G ≃ H
a : G
b : k
⊢ Eq (α := SkewMonoidAlgebra k H) (equivMapDomain f (single a b)) (single ((f : (a : G) → H) a) b)
have a₁ : Eq (α := H →₀ k) (toFinsupp (equivMapDomain f (single a b))) (toFinsupp (single ((f : (a : G) → H) a) b))
Tactic: apply toFinsupp_injective
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : AddCommMonoid k
f : G ≃ H
a : G
b : k
⊢ Eq (α := H →₀ k) (toFinsupp (equivMapDomain f (single a b))) (toFinsupp (single ((f : (a : G) → H) a) b))
have a₁ : Eq (α := H →₀ k) (Finsupp.equivMapDomain f (toFinsupp (single a b))) (toFinsupp (single ((f : (a : G) → H) a) b))
Tactic: simp_rw [toFinsupp_equivMapDomain, single, Finsupp.equivMapDomain_single]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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))
⊢ Eq (α := H →₀ k) (toFinsupp (equivMapDomain f (single a b))) (toFinsupp (single ((f : (a : G) → H) a) b))
have a₂ : Eq (α := H →₀ k) (Finsupp.equivMapDomain f (Finsupp.single a b)) (Finsupp.single ((f : (a : G) → H) a) b)
Tactic: simp_rw [toFinsupp_equivMapDomain, single, Finsupp.equivMapDomain_single]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : AddCommMonoid k
f : G ≃ H
a : G
b : k
⊢ Eq (α := SkewMonoidAlgebra k H) (equivMapDomain f (single a b)) (single ((f : (a : G) → H) a) b)
have a₁ : Eq (α := H →₀ k) (toFinsupp (equivMapDomain f (single a b))) (toFinsupp (single ((f : (a : G) → H) a) b))
Tactic: classical
  apply toFinsupp_injective
  simp_rw [toFinsupp_equivMapDomain, single, Finsupp.equivMapDomain_single]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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
⊢ equivMapDomain e (c • x) = c • equivMapDomain e x
have 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)
Tactic: simp_rw [equivMapDomain_eq_mapDomain, mapDomain_smul]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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
⊢ Eq (α := SkewMonoidAlgebra A G ≃ₐ[k] SkewMonoidAlgebra A G) (domCongrAlg k A (e := MulEquiv.refl G) ⋯) AlgEquiv.refl
have h : ∀ (a : SkewMonoidAlgebra A G),
  Eq (α := SkewMonoidAlgebra A G)
    ((domCongrAlg k A (e := MulEquiv.refl G) sorry : (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: apply AlgEquiv.ext
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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
⊢ a • x = HSMul.hSMul.{u_2, u_4, u_4} (α := G) ((e.symm : (a : H) → G) a : G) x
have 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
Tactic: rw [he, MulEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
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
⊢ a • x = HSMul.hSMul.{u_2, u_4, u_4} (α := G) ((e.symm : (a : H) → G) a : G) x
have rw₁ : a • x = a • x
Tactic: rw [he, MulEquiv.apply_symm_apply]