awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
h : TensorAlgebra R M →ₐ[R] A
x x_1 : TensorAlgebra R M
h' : SymRel R M x x_1
mul_comm :
  ∀ (x y : M),
    Eq.{u_3 + 1} (α := A)
      ((h : (a : TensorAlgebra R M) → A)
          (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
            ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
            ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M)) :
        A)
      ((h : (a : TensorAlgebra R M) → A)
          (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
            ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M)
            ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)) :
        A)
⊢ Eq.{u_3 + 1} (α := A) ((h : (a : TensorAlgebra R M) → A) x : A) ((h : (a : TensorAlgebra R M) → A) x_1 : A)

Tactic:
induction h' with | mul_comm x y => rw [map_mul, map_mul, mul_comm]

Premises used: map_mul, mul_comm
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
equiv : (TensorAlgebra R M →ₐ[R] A) ≃
  { f : TensorAlgebra R M →ₐ[R] A //
    ∀ {x y : TensorAlgebra R M},
      SymRel R M x y →
        Eq.{u_3 + 1} (α := A) ((f : (a : TensorAlgebra R M) → A) x : A) ((f : (a : TensorAlgebra R M) → A) y : A) } :=
  Equiv.symm
    (Equiv.subtypeUnivEquiv (p := fun (h : TensorAlgebra R M →ₐ[R] A) ↦
      ∀ (x x_1 : TensorAlgebra R M) (h' : SymRel R M x x_1),
        Eq.{u_3 + 1} (α := A) ((h : (a : TensorAlgebra R M) → A) x : A) ((h : (a : TensorAlgebra R M) → A) x_1 : A))
      ⋯)
⊢ (M →ₗ[R] A) ≃ (SymmetricAlgebra R M →ₐ[R] A)

Tactic:
exact (TensorAlgebra.lift R).trans <| equiv.trans <| RingQuot.liftAlgHom R

Premises used: Equiv.trans, TensorAlgebra.lift, RingQuot.liftAlgHom
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
a : M
⊢ Eq.{u_3 + 1} (α := A)
    ((((lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
          (a : SymmetricAlgebra R M) → A)
        ((ι R M : (a : M) → SymmetricAlgebra R M) a : SymmetricAlgebra R M) :
      A)
    ((f : (a : M) → A) a : A)

Tactic:
simp [lift, ι, algHom]

Premises used: SymmetricAlgebra.lift, SymmetricAlgebra.algHom, SymmetricAlgebra.ι
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
⊢ (↑((lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
        [inst_5 : FunLike (SymmetricAlgebra R M →ₐ[R] A) (SymmetricAlgebra R M) A] →
          [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] A) (RingHom.id R) (SymmetricAlgebra R M) A] →
            SymmetricAlgebra R M →ₗ[R] A) ∘ₗ
      ι R M =
    f

Tactic:
LinearMap.ext <| lift_ι_apply f

Premises used: SymmetricAlgebra.lift_ι_apply, LinearMap.ext
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
F G : SymmetricAlgebra R M →ₐ[R] A
h :
  Eq (α := M →ₗ[R] A)
    ((↑F :
        [inst_5 : FunLike (SymmetricAlgebra R M →ₐ[R] A) (SymmetricAlgebra R M) A] →
          [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] A) (RingHom.id R) (SymmetricAlgebra R M) A] →
            SymmetricAlgebra R M →ₗ[R] A) ∘ₗ
      ι R M)
    ((↑G :
        [inst_5 : FunLike (SymmetricAlgebra R M →ₐ[R] A) (SymmetricAlgebra R M) A] →
          [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] A) (RingHom.id R) (SymmetricAlgebra R M) A] →
            SymmetricAlgebra R M →ₗ[R] A) ∘ₗ
      ι R M)
w :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := A)
      (((F.comp (RingQuot.mkAlgHom R (SymRel R M))).toLinearMap ∘ₗ TensorAlgebra.ι R : (a : M) → A) x : A)
      (((G.comp (RingQuot.mkAlgHom R (SymRel R M))).toLinearMap ∘ₗ TensorAlgebra.ι R : (a : M) → A) x : A)
⊢ F = G

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
F G : SymmetricAlgebra R M →ₐ[R] A
h :
  Eq (α := M →ₗ[R] A)
    ((↑F :
        [inst_5 : FunLike (SymmetricAlgebra R M →ₐ[R] A) (SymmetricAlgebra R M) A] →
          [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] A) (RingHom.id R) (SymmetricAlgebra R M) A] →
            SymmetricAlgebra R M →ₗ[R] A) ∘ₗ
      ι R M)
    ((↑G :
        [inst_5 : FunLike (SymmetricAlgebra R M →ₐ[R] A) (SymmetricAlgebra R M) A] →
          [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] A) (RingHom.id R) (SymmetricAlgebra R M) A] →
            SymmetricAlgebra R M →ₗ[R] A) ∘ₗ
      ι R M)
x : M
⊢ Eq.{u_3 + 1} (α := A)
    (((F.comp (RingQuot.mkAlgHom R (SymRel R M))).toLinearMap ∘ₗ TensorAlgebra.ι R : (a : M) → A) x : A)
    (((G.comp (RingQuot.mkAlgHom R (SymRel R M))).toLinearMap ∘ₗ TensorAlgebra.ι R : (a : M) → A) x : A)

Tactic:
congr($h x)

Premises used: congrArg, id, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
F G : SymmetricAlgebra R M →ₐ[R] A
h :
  Eq (α := M →ₗ[R] A)
    ((↑F :
        [inst_5 : FunLike (SymmetricAlgebra R M →ₐ[R] A) (SymmetricAlgebra R M) A] →
          [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] A) (RingHom.id R) (SymmetricAlgebra R M) A] →
            SymmetricAlgebra R M →ₗ[R] A) ∘ₗ
      ι R M)
    ((↑G :
        [inst_5 : FunLike (SymmetricAlgebra R M →ₐ[R] A) (SymmetricAlgebra R M) A] →
          [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] A) (RingHom.id R) (SymmetricAlgebra R M) A] →
            SymmetricAlgebra R M →ₗ[R] A) ∘ₗ
      ι R M)
x : M
⊢ Eq.{u_3 + 1} (α := A)
    (((F.comp (RingQuot.mkAlgHom R (SymRel R M))).toLinearMap ∘ₗ TensorAlgebra.ι R : (a : M) → A) x : A)
    (((G.comp (RingQuot.mkAlgHom R (SymRel R M))).toLinearMap ∘ₗ TensorAlgebra.ι R : (a : M) → A) x : A)

Tactic:
exact congr($h x)
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  Eq (α := M →ₗ[R] SymmetricAlgebra R M)
    ((↑((lift : (a : M →ₗ[R] SymmetricAlgebra R M) → SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (ι R M) :
            SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) :
        [inst_3 :
            FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (SymmetricAlgebra R M) (SymmetricAlgebra R M)] →
          [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (RingHom.id R) (SymmetricAlgebra R M)
                (SymmetricAlgebra R M)] →
            SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M) ∘ₗ
      ι R M)
    ((↑(AlgHom.id R (SymmetricAlgebra R M)) :
        [inst_3 :
            FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (SymmetricAlgebra R M) (SymmetricAlgebra R M)] →
          [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (RingHom.id R) (SymmetricAlgebra R M)
                (SymmetricAlgebra R M)] →
            SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M) ∘ₗ
      ι R M)
⊢ Eq (α := SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M)
    ((lift : (a : M →ₗ[R] SymmetricAlgebra R M) → SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (ι R M) :
      SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M)
    (AlgHom.id R (SymmetricAlgebra R M) : SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M)

Tactic:
apply algHom_ext

Premises used: SymmetricAlgebra.algHom_ext
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  Eq (α := M →ₗ[R] SymmetricAlgebra R M) (ι R M)
    ((↑(AlgHom.id R (SymmetricAlgebra R M)) :
        [inst_3 :
            FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (SymmetricAlgebra R M) (SymmetricAlgebra R M)] →
          [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (RingHom.id R) (SymmetricAlgebra R M)
                (SymmetricAlgebra R M)] →
            SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M) ∘ₗ
      ι R M)
⊢ Eq (α := M →ₗ[R] SymmetricAlgebra R M)
    ((↑((lift : (a : M →ₗ[R] SymmetricAlgebra R M) → SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (ι R M) :
            SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) :
        [inst_3 :
            FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (SymmetricAlgebra R M) (SymmetricAlgebra R M)] →
          [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (RingHom.id R) (SymmetricAlgebra R M)
                (SymmetricAlgebra R M)] →
            SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M) ∘ₗ
      ι R M)
    ((↑(AlgHom.id R (SymmetricAlgebra R M)) :
        [inst_3 :
            FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (SymmetricAlgebra R M) (SymmetricAlgebra R M)] →
          [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (RingHom.id R) (SymmetricAlgebra R M)
                (SymmetricAlgebra R M)] →
            SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M) ∘ₗ
      ι R M)

Tactic:
rw [lift_comp_ι]

Premises used: SymmetricAlgebra.lift_comp_ι
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  ∀ (x : M),
    Eq (α := SymmetricAlgebra R M) ((ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)
      (((↑(AlgHom.id R (SymmetricAlgebra R M)) :
                [inst_3 :
                    FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (SymmetricAlgebra R M)
                      (SymmetricAlgebra R M)] →
                  [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (RingHom.id R)
                        (SymmetricAlgebra R M) (SymmetricAlgebra R M)] →
                    SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M) ∘ₗ
              ι R M :
            (a : M) → SymmetricAlgebra R M)
          x :
        SymmetricAlgebra R M)
⊢ Eq (α := M →ₗ[R] SymmetricAlgebra R M) (ι R M)
    ((↑(AlgHom.id R (SymmetricAlgebra R M)) :
        [inst_3 :
            FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (SymmetricAlgebra R M) (SymmetricAlgebra R M)] →
          [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (RingHom.id R) (SymmetricAlgebra R M)
                (SymmetricAlgebra R M)] →
            SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M) ∘ₗ
      ι R M)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Eq (α := SymmetricAlgebra R M) ((ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)
    (((↑(AlgHom.id R (SymmetricAlgebra R M)) :
              [inst_3 :
                  FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (SymmetricAlgebra R M)
                    (SymmetricAlgebra R M)] →
                [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M) (RingHom.id R)
                      (SymmetricAlgebra R M) (SymmetricAlgebra R M)] →
                  SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M) ∘ₗ
            ι R M :
          (a : M) → SymmetricAlgebra R M)
        x :
      SymmetricAlgebra R M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Eq.{u_1 + 1} (α := R)
    ((algebraMapInv : (a : SymmetricAlgebra R M) → R)
        ((ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M) :
      R)
    (0 : R)

Tactic:
lift_ι_apply 0 x

Premises used: SymmetricAlgebra.lift_ι_apply, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : R
⊢ (algebraMapInv : (a : SymmetricAlgebra R M) → R)
      ((algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) x : SymmetricAlgebra R M) =
    x

Tactic:
simp [algebraMapInv]

Premises used: SymmetricAlgebra.algebraMapInv
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : R
⊢ Eq (α := SymmetricAlgebra R M)
      ((algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)
      ((algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) y : SymmetricAlgebra R M) ↔
    x = y

Tactic:
(algebraMap_leftInverse M).injective.eq_iff

Premises used: Function.LeftInverse.injective, Function.Injective.eq_iff, SymmetricAlgebra.algebraMap_leftInverse
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : R
⊢ Eq (α := SymmetricAlgebra R M)
      ((algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)
      (0 : SymmetricAlgebra R M) ↔
    x = 0

Tactic:
map_eq_zero_iff (algebraMap _ _) (algebraMap_leftInverse _).injective

Premises used: Function.LeftInverse.injective, Algebra.algebraMap, map_eq_zero_iff, SymmetricAlgebra.algebraMap_leftInverse
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : R
⊢ Eq (α := SymmetricAlgebra R M)
      ((algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)
      (1 : SymmetricAlgebra R M) ↔
    x = 1

Tactic:
map_eq_one_iff (algebraMap _ _) (algebraMap_leftInverse _).injective

Premises used: Function.LeftInverse.injective, Algebra.algebraMap, map_eq_one_iff, SymmetricAlgebra.algebraMap_leftInverse
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
inst_5 : Nontrivial R
⊢ Nontrivial (SymmetricAlgebra R M)

Tactic:
(algebraMap_leftInverse M).injective.nontrivial

Premises used: Function.LeftInverse.injective, Function.Injective.nontrivial, SymmetricAlgebra.algebraMap_leftInverse
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw :
  Function.Bijective (α := SymmetricAlgebra R M) (β := SymmetricAlgebra R M)
    (⇑(AlgHom.id R (SymmetricAlgebra R M)) : (a : SymmetricAlgebra R M) → SymmetricAlgebra R M)
⊢ IsSymmetricAlgebra (ι R M)

Tactic:
rw [IsSymmetricAlgebra, lift_ι]

Premises used: IsSymmetricAlgebra, SymmetricAlgebra.lift_ι
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Function.Bijective (α := SymmetricAlgebra R M) (β := SymmetricAlgebra R M)
    (⇑(AlgHom.id R (SymmetricAlgebra R M)) : (a : SymmetricAlgebra R M) → SymmetricAlgebra R M)

Tactic:
Function.Involutive.bijective (congrFun rfl)

Premises used: congrFun, Function.Involutive.bijective, rfl
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Function.Bijective (α := SymmetricAlgebra R M) (β := SymmetricAlgebra R M)
    (⇑(AlgHom.id R (SymmetricAlgebra R M)) : (a : SymmetricAlgebra R M) → SymmetricAlgebra R M)

Tactic:
exact Function.Involutive.bijective (congrFun rfl)

Premises used: congrFun, Function.Involutive.bijective, rfl
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
h : IsSymmetricAlgebra f
a : SymmetricAlgebra R M
⊢ Eq.{u_3 + 1} (α := A) ((h.equiv : (a : SymmetricAlgebra R M) → A) a : A)
    ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
          (a : SymmetricAlgebra R M) → A)
        a :
      A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
h : IsSymmetricAlgebra f
⊢ (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A) = (SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, rfl
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
h : IsSymmetricAlgebra f
a : M
⊢ Eq.{u_3 + 1} (α := A)
    ((h.equiv : (a : SymmetricAlgebra R M) → A)
        ((h.equiv.symm : (a : A) → SymmetricAlgebra R M) ((f : (a : M) → A) a) : SymmetricAlgebra R M) :
      A)
    ((h.equiv : (a : SymmetricAlgebra R M) → A)
        ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) a : SymmetricAlgebra R M) :
      A)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
h : IsSymmetricAlgebra f
⊢ (↑(↑h.equiv : SymmetricAlgebra R M ≃ₗ[R] A).symm : A →ₗ[R] SymmetricAlgebra R M) ∘ₗ f = SymmetricAlgebra.ι R M

Tactic:
LinearMap.ext fun x ↦ equiv_symm_apply h x

Premises used: LinearMap.ext, IsSymmetricAlgebra.equiv_symm_apply
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
e : SymmetricAlgebra R M ≃ₐ[R] A
he : (↑(↑e : SymmetricAlgebra R M ≃ₗ[R] A) : SymmetricAlgebra R M →ₗ[R] A) ∘ₗ SymmetricAlgebra.ι R M = f
h : (↑e : SymmetricAlgebra R M →ₐ[R] A) = (SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f
⊢ Function.Bijective (α := SymmetricAlgebra R M) (β := A)
    (⇑((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
      (a : SymmetricAlgebra R M) → A)

Tactic:
h ▸ e.bijective

Premises used: Eq.rec, AlgEquiv.bijective
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
e : SymmetricAlgebra R M ≃ₐ[R] A
he : (↑(↑e : SymmetricAlgebra R M ≃ₗ[R] A) : SymmetricAlgebra R M →ₗ[R] A) ∘ₗ SymmetricAlgebra.ι R M = f
h : (↑e : SymmetricAlgebra R M →ₐ[R] A) = (SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f
⊢ Function.Bijective (α := SymmetricAlgebra R M) (β := A)
    (⇑((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
      (a : SymmetricAlgebra R M) → A)

Tactic:
exact h ▸ e.bijective
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
e : SymmetricAlgebra R M ≃ₐ[R] A
he : (↑(↑e : SymmetricAlgebra R M ≃ₗ[R] A) : SymmetricAlgebra R M →ₗ[R] A) ∘ₗ SymmetricAlgebra.ι R M = f
suffices :
  (↑e : SymmetricAlgebra R M →ₐ[R] A) = (SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f
⊢ IsSymmetricAlgebra f

Tactic:
suffices h : e = SymmetricAlgebra.lift f by
    change Function.Bijective _
    exact h ▸ e.bijective
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
e : SymmetricAlgebra R M ≃ₐ[R] A
he : (↑(↑e : SymmetricAlgebra R M ≃ₗ[R] A) : SymmetricAlgebra R M →ₗ[R] A) ∘ₗ SymmetricAlgebra.ι R M = f
h :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := A)
      (((↑(↑e : SymmetricAlgebra R M →ₐ[R] A) :
                [inst_5 : FunLike (SymmetricAlgebra R M →ₐ[R] A) (SymmetricAlgebra R M) A] →
                  [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] A) (RingHom.id R) (SymmetricAlgebra R M) A] →
                    SymmetricAlgebra R M →ₗ[R] A) ∘ₗ
              SymmetricAlgebra.ι R M :
            (a : M) → A)
          x :
        A)
      (((↑((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
                [inst_5 : FunLike (SymmetricAlgebra R M →ₐ[R] A) (SymmetricAlgebra R M) A] →
                  [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] A) (RingHom.id R) (SymmetricAlgebra R M) A] →
                    SymmetricAlgebra R M →ₗ[R] A) ∘ₗ
              SymmetricAlgebra.ι R M :
            (a : M) → A)
          x :
        A)
⊢ (↑e : SymmetricAlgebra R M →ₐ[R] A) = (SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
e : SymmetricAlgebra R M ≃ₐ[R] A
he : (↑(↑e : SymmetricAlgebra R M ≃ₗ[R] A) : SymmetricAlgebra R M →ₗ[R] A) ∘ₗ SymmetricAlgebra.ι R M = f
x : M
⊢ Eq.{u_3 + 1} (α := A)
    (((↑(↑e : SymmetricAlgebra R M →ₐ[R] A) :
              [inst_5 : FunLike (SymmetricAlgebra R M →ₐ[R] A) (SymmetricAlgebra R M) A] →
                [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] A) (RingHom.id R) (SymmetricAlgebra R M) A] →
                  SymmetricAlgebra R M →ₗ[R] A) ∘ₗ
            SymmetricAlgebra.ι R M :
          (a : M) → A)
        x :
      A)
    (((↑((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
              [inst_5 : FunLike (SymmetricAlgebra R M →ₐ[R] A) (SymmetricAlgebra R M) A] →
                [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] A) (RingHom.id R) (SymmetricAlgebra R M) A] →
                  SymmetricAlgebra R M →ₗ[R] A) ∘ₗ
            SymmetricAlgebra.ι R M :
          (a : M) → A)
        x :
      A)

Tactic:
simpa using congr($he x)
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
e : SymmetricAlgebra R M ≃ₐ[R] A
⊢ IsSymmetricAlgebra (e.toLinearMap ∘ₗ SymmetricAlgebra.ι R M)

Tactic:
.of_equiv e rfl

Premises used: IsSymmetricAlgebra.of_equiv, rfl
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
h : IsSymmetricAlgebra f
A' : Type u_4
inst_5 : CommSemiring A'
inst_6 : Algebra R A'
g : M →ₗ[R] A'
a : M
⊢ Eq.{u_4 + 1} (α := A') ((h.lift g : (a : A) → A') ((f : (a : M) → A) a : A) : A') ((g : (a : M) → A') a : A')

Tactic:
simp [lift]

Premises used: IsSymmetricAlgebra.lift