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
f : M →ₗ[R] A
h : IsSymmetricAlgebra f
A' : Type u_4
inst_5 : CommSemiring A'
inst_6 : Algebra R A'
g : M →ₗ[R] A'
⊢ (↑(h.lift g) :
        [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f =
    g

Tactic:
LinearMap.ext <| lift_eq h g

Premises used: IsSymmetricAlgebra.lift_eq, 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 : M →ₗ[R] A
A' : Type u_4
inst_5 : CommSemiring A'
inst_6 : Algebra R A'
h : IsSymmetricAlgebra f
F G : A →ₐ[R] A'
hFG :
  Eq (α := M →ₗ[R] A')
    ((↑F : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)
    ((↑G : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)
this : F.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A) = G.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A)
rw :
  ∀
    (this :
      Eq (α := (a : SymmetricAlgebra R M) → A')
        (⇑(F.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A)) : (a : SymmetricAlgebra R M) → A')
        (⇑(G.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A)) : (a : SymmetricAlgebra R M) → A')),
    Eq (α := (a : A) → A') (⇑F : (a : A) → A') (⇑G : (a : A) → A')
⊢ F = G

Tactic:
rw [DFunLike.ext'_iff] at this ⊢

Premises used: DFunLike.ext'_iff
-- 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' : Type u_4
inst_5 : CommSemiring A'
inst_6 : Algebra R A'
h : IsSymmetricAlgebra f
F G : A →ₐ[R] A'
hFG :
  Eq (α := M →ₗ[R] A')
    ((↑F : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)
    ((↑G : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)
this :
  Eq (α := (a : SymmetricAlgebra R M) → A')
    (⇑(F.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A)) : (a : SymmetricAlgebra R M) → A')
    (⇑(G.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A)) : (a : SymmetricAlgebra R M) → A')
⊢ Eq (α := (a : A) → A') (⇑F : (a : A) → A') (⇑G : (a : A) → A')

Tactic:
h.equiv.surjective.injective_comp_right this

Premises used: Function.Surjective.injective_comp_right, IsSymmetricAlgebra.equiv, AlgEquiv.surjective
-- 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' : Type u_4
inst_5 : CommSemiring A'
inst_6 : Algebra R A'
h : IsSymmetricAlgebra f
F G : A →ₐ[R] A'
hFG :
  Eq (α := M →ₗ[R] A')
    ((↑F : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)
    ((↑G : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)
this :
  Eq (α := (a : SymmetricAlgebra R M) → A')
    (⇑(F.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A)) : (a : SymmetricAlgebra R M) → A')
    (⇑(G.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A)) : (a : SymmetricAlgebra R M) → A')
⊢ Eq (α := (a : A) → A') (⇑F : (a : A) → A') (⇑G : (a : A) → A')

Tactic:
exact h.equiv.surjective.injective_comp_right this

Premises used: Function.Surjective.injective_comp_right, IsSymmetricAlgebra.equiv, AlgEquiv.surjective
-- 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' : Type u_4
inst_5 : CommSemiring A'
inst_6 : Algebra R A'
h : IsSymmetricAlgebra f
F G : A →ₐ[R] A'
hFG :
  Eq (α := M →ₗ[R] A')
    ((↑F : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)
    ((↑G : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)
suffices : F.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A) = G.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A)
⊢ F = G

Tactic:
suffices F.comp h.equiv.toAlgHom = G.comp h.equiv.toAlgHom by
    rw [DFunLike.ext'_iff] at this ⊢
    exact h.equiv.surjective.injective_comp_right this
-- 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' : Type u_4
inst_5 : CommSemiring A'
inst_6 : Algebra R A'
h : IsSymmetricAlgebra f
F G : A →ₐ[R] A'
hFG :
  Eq (α := M →ₗ[R] A')
    ((↑F : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)
    ((↑G : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)
⊢ F.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A) = G.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A)

Tactic:
SymmetricAlgebra.algHom_ext (LinearMap.ext fun x ↦ ?_)

Premises used: LinearMap.ext, 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
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
A' : Type u_4
inst_5 : CommSemiring A'
inst_6 : Algebra R A'
h : IsSymmetricAlgebra f
F G : A →ₐ[R] A'
hFG :
  Eq (α := M →ₗ[R] A')
    ((↑F : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)
    ((↑G : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)
refine :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := A')
      (((↑(F.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A)) :
                [inst_7 : 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')
      (((↑(G.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A)) :
                [inst_7 : 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')
⊢ F.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A) = G.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A)

Tactic:
refine SymmetricAlgebra.algHom_ext (LinearMap.ext fun x ↦ ?_)

Premises used: LinearMap.ext, 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
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
A' : Type u_4
inst_5 : CommSemiring A'
inst_6 : Algebra R A'
h : IsSymmetricAlgebra f
F G : A →ₐ[R] A'
hFG :
  Eq (α := M →ₗ[R] A')
    ((↑F : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)
    ((↑G : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)
x : M
⊢ Eq.{u_4 + 1} (α := A')
    (((↑(F.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A)) :
              [inst_7 : 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')
    (((↑(G.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A)) :
              [inst_7 : 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($hFG 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
h : IsSymmetricAlgebra f
A' : Type u_4
inst_5 : CommSemiring A'
inst_6 : Algebra R A'
g : M →ₗ[R] A'
F : A →ₐ[R] A'
hF :
  (↑F : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f =
    g
⊢ Eq (α := M →ₗ[R] A')
    ((↑F : [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)
    ((↑(h.lift g) :
        [inst_7 : FunLike (A →ₐ[R] A') A A'] → [SemilinearMapClass (A →ₐ[R] A') (RingHom.id R) A A'] → A →ₗ[R] A') ∘ₗ
      f)

Tactic:
simpa
-- 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
motive : A → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r)
ι : ∀ (x : M), motive ((f : (a : M) → A) x)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
add : ∀ (a b : A), motive a → motive b → motive (a + b)
a : A
rw : motive (h.equiv.toFun (h.equiv.invFun a))
⊢ motive a

Tactic:
rw [← h.equiv.right_inv a]

Premises used: Equiv.right_inv, IsSymmetricAlgebra.equiv, AlgEquiv.toEquiv
-- 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
motive : A → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r)
ι : ∀ (x : M), motive ((f : (a : M) → A) x)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
add : ∀ (a b : A), motive a → motive b → motive (a + b)
a : A
generalize : ∀ (y : SymmetricAlgebra R M), motive (h.equiv.toFun y)
⊢ motive (h.equiv.toFun (h.equiv.invFun a))

Tactic:
generalize h.equiv.invFun a = y

Premises used: IsSymmetricAlgebra.equiv, AlgEquiv.toEquiv, Equiv.invFun
-- 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
motive : A → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r)
ι : ∀ (x : M), motive ((f : (a : M) → A) x)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
add : ∀ (a b : A), motive a → motive b → motive (a + b)
a : A
y : SymmetricAlgebra R M
change :
  motive
    ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
        (a : SymmetricAlgebra R M) → A)
      y)
⊢ motive (h.equiv.toFun y)

Tactic:
change motive (SymmetricAlgebra.lift f y)

Premises used: SymmetricAlgebra.lift, 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 : M →ₗ[R] A
h : IsSymmetricAlgebra f
motive : A → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r)
ι : ∀ (x : M), motive ((f : (a : M) → A) x)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
add : ∀ (a b : A), motive a → motive b → motive (a + b)
a : A
r : R
⊢ motive
    ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
        (a : SymmetricAlgebra R M) → A)
      ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r : SymmetricAlgebra R M))

Tactic:
simpa using algebraMap r
-- 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
motive : A → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r)
ι : ∀ (x : M), motive ((f : (a : M) → A) x)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
add : ∀ (a b : A), motive a → motive b → motive (a + b)
a : A
y : M
⊢ motive
    ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
        (a : SymmetricAlgebra R M) → A)
      ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) y : SymmetricAlgebra R M))

Tactic:
simpa using ι y
-- 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
motive : A → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r)
ι : ∀ (x : M), motive ((f : (a : M) → A) x)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
add : ∀ (a b : A), motive a → motive b → motive (a + b)
a : A
a_1 b : SymmetricAlgebra R M
hx :
  motive
    ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
        (a : SymmetricAlgebra R M) → A)
      a_1)
hy :
  motive
    ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
        (a : SymmetricAlgebra R M) → A)
      b)
⊢ motive
    ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
        (a : SymmetricAlgebra R M) → A)
      (a_1 * b))

Tactic:
simpa using mul _ _ hx hy
-- 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
motive : A → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r)
ι : ∀ (x : M), motive ((f : (a : M) → A) x)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
add : ∀ (a b : A), motive a → motive b → motive (a + b)
a : A
a_1 b : SymmetricAlgebra R M
hx :
  motive
    ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
        (a : SymmetricAlgebra R M) → A)
      a_1)
hy :
  motive
    ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
        (a : SymmetricAlgebra R M) → A)
      b)
⊢ motive
    ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
        (a : SymmetricAlgebra R M) → A)
      (a_1 + b))

Tactic:
simpa using add _ _ hx hy
-- 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
motive : A → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A : (a : R) → A) r)
ι : ∀ (x : M), motive ((f : (a : M) → A) x)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
add : ∀ (a b : A), motive a → motive b → motive (a + b)
a : A
y : SymmetricAlgebra R M
algebraMap₁ :
  ∀ (r : R),
    motive
      ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
          (a : SymmetricAlgebra R M) → A)
        ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r : SymmetricAlgebra R M))
ι₁ :
  ∀ (y : M),
    motive
      ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
          (a : SymmetricAlgebra R M) → A)
        ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) y : SymmetricAlgebra R M))
mul₁ :
  ∀ (a b : SymmetricAlgebra R M)
    (hx :
      motive
        ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
            (a : SymmetricAlgebra R M) → A)
          a))
    (hy :
      motive
        ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
            (a : SymmetricAlgebra R M) → A)
          b)),
    motive
      ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
          (a : SymmetricAlgebra R M) → A)
        (a * b))
add₁ :
  ∀ (a b : SymmetricAlgebra R M)
    (hx :
      motive
        ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
            (a : SymmetricAlgebra R M) → A)
          a))
    (hy :
      motive
        ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
            (a : SymmetricAlgebra R M) → A)
          b)),
    motive
      ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
          (a : SymmetricAlgebra R M) → A)
        (a + b))
⊢ motive
    ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
        (a : SymmetricAlgebra R M) → A)
      y)

Tactic:
induction y using SymmetricAlgebra.induction with
  | algebraMap r => simpa using algebraMap r
  | ι y => simpa using ι y
  | mul _ _ hx hy => simpa using mul _ _ hx hy
  | add _ _ hx hy => simpa using add _ _ hx hy
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
Goal:
κ : Type uκ
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis κ R M
i : κ
⊢ Eq (α := MvPolynomial κ R)
    ((AlgHom.comp (B := SymmetricAlgebra R M)
            ((lift : (a : M →ₗ[R] MvPolynomial κ R) → SymmetricAlgebra R M →ₐ[R] MvPolynomial κ R)
              ((b.constr R : (a : κ → MvPolynomial κ R) → M →ₗ[R] MvPolynomial κ R) MvPolynomial.X))
            (MvPolynomial.aeval fun (i : κ) ↦ (ι R M : (a : M) → SymmetricAlgebra R M) ((b : (a : κ) → M) i)) :
          (a : MvPolynomial κ R) → MvPolynomial κ R)
        (MvPolynomial.X i) :
      MvPolynomial κ R)
    ((AlgHom.id R (MvPolynomial κ R) : (a : MvPolynomial κ R) → MvPolynomial κ R) (MvPolynomial.X i) : MvPolynomial κ R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
Goal:
κ : Type uκ
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis κ R M
i : κ
⊢ Eq (α := SymmetricAlgebra R M)
    (((↑(AlgHom.comp (B := MvPolynomial κ R)
                  (MvPolynomial.aeval fun (i : κ) ↦ (ι R M : (a : M) → SymmetricAlgebra R M) ((b : (a : κ) → M) i))
                  ((lift : (a : M →ₗ[R] MvPolynomial κ R) → SymmetricAlgebra R M →ₐ[R] MvPolynomial κ R)
                    ((b.constr R : (a : κ → MvPolynomial κ R) → M →ₗ[R] MvPolynomial κ R) MvPolynomial.X))) :
              [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)
        ((b : (a : κ) → M) i) :
      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)
        ((b : (a : κ) → M) i) :
      SymmetricAlgebra R M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
Goal:
κ : Type uκ
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis κ R M
i : κ
⊢ Eq (α := MvPolynomial κ R)
    ((((b.constr R : (a : κ → MvPolynomial κ R) → M →ₗ[R] MvPolynomial κ R) MvPolynomial.X : M →ₗ[R] MvPolynomial κ R) :
          (a : M) → MvPolynomial κ R)
        ((b : (a : κ) → M) i) :
      MvPolynomial κ R)
    (MvPolynomial.X i : MvPolynomial κ R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
Goal:
κ : Type uκ
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis κ R M
i : κ
⊢ Eq (α := SymmetricAlgebra R M)
    (((equivMvPolynomial b).symm : (a : MvPolynomial κ R) → SymmetricAlgebra R M) (MvPolynomial.X i) :
      SymmetricAlgebra R M)
    ((ι R M : (a : M) → SymmetricAlgebra R M) ((b : (a : κ) → M) i) : SymmetricAlgebra R M)

Tactic:
(equivMvPolynomial b).toEquiv.symm_apply_eq.mpr <| equivMvPolynomial_ι_apply b i |>.symm

Premises used: Iff.mpr, Equiv.symm_apply_eq, SymmetricAlgebra.equivMvPolynomial_ι_apply, AlgEquiv.toEquiv, Eq.symm, SymmetricAlgebra.equivMvPolynomial
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Type u_1
b : Basis I R M
⊢ IsSymmetricAlgebra (R := R) (M := M) (A := MvPolynomial I R)
    ((b.constr R : (a : I → MvPolynomial I R) → M →ₗ[R] MvPolynomial I R) MvPolynomial.X)

Tactic:
(SymmetricAlgebra.equivMvPolynomial b).bijective

Premises used: IsSymmetricAlgebra, AlgEquiv.bijective, SymmetricAlgebra.equivMvPolynomial
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
Goal:
κ : Type uκ
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
⊢ Free R (SymmetricAlgebra R M)

Tactic:
let ⟨⟨_I, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
  .of_basis b.symmetricAlgebra

Premises used: _private.0.SymmetricAlgebra.instModuleFree.match_1, SymmetricAlgebra, Module.Free, Module.Basis.symmetricAlgebra, Module.Free.of_basis, Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
Goal:
κ : Type uκ
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : NoZeroDivisors R
inst_4 : Free R M
⊢ NoZeroDivisors (SymmetricAlgebra R M)

Tactic:
have ⟨⟨_, b⟩⟩ := ‹Module.Free R M›
  (equivMvPolynomial b).toMulEquiv.noZeroDivisors

Premises used: SymmetricAlgebra, AlgEquiv.toMulEquiv, NoZeroDivisors, _private.0.SymmetricAlgebra.instNoZeroDivisors.match_1, MvPolynomial, MulEquiv.noZeroDivisors, SymmetricAlgebra.equivMvPolynomial
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
Goal:
κ : Type uκ
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : Free R M
⊢ IsDomain (SymmetricAlgebra R M)

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain