awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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
⊢ Eq.{u_3 + 1} (α := A) ((h : (a : TensorAlgebra R M) → A) x : A) ((h : (a : TensorAlgebra R M) → A) x_1 : A)
have 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)
Tactic: induction h' with | mul_comm x y => rw [map_mul, map_mul, mul_comm]
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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)
⊢ F = G
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module 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)
have 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)
Tactic: apply algHom_ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module 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)
have 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)
Tactic: rw [lift_comp_ι]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsSymmetricAlgebra (ι R M)
have rw : Function.Bijective (α := SymmetricAlgebra R M) (β := SymmetricAlgebra R M)
  (⇑(AlgHom.id R (SymmetricAlgebra R M)) : (a : SymmetricAlgebra R M) → SymmetricAlgebra R M)
Tactic: rw [IsSymmetricAlgebra, lift_ι]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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
⊢ IsSymmetricAlgebra f
have suffices : (↑e : SymmetricAlgebra R M →ₐ[R] A) = (SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f
Tactic: suffices h : e = SymmetricAlgebra.lift f by
    change Function.Bijective _
    exact h ▸ e.bijective
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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
⊢ (↑e : SymmetricAlgebra R M →ₐ[R] A) = (SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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)
⊢ F = G
have 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')
Tactic: rw [DFunLike.ext'_iff] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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 = G
have suffices : F.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A) = G.comp (↑h.equiv : SymmetricAlgebra R M →ₐ[R] A)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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)
have 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')
Tactic: refine SymmetricAlgebra.algHom_ext (LinearMap.ext fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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
⊢ motive a
have rw : motive (h.equiv.toFun (h.equiv.invFun a))
Tactic: rw [← h.equiv.right_inv a]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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
⊢ motive (h.equiv.toFun (h.equiv.invFun a))
have generalize : ∀ (y : SymmetricAlgebra R M), motive (h.equiv.toFun y)
Tactic: generalize h.equiv.invFun a = y
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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
⊢ motive (h.equiv.toFun y)
have 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)
Tactic: change motive (SymmetricAlgebra.lift f y)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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
⊢ motive
    ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
        (a : SymmetricAlgebra R M) → A)
      y)
have 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))
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
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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))
⊢ motive
    ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
        (a : SymmetricAlgebra R M) → A)
      y)
have ι₁ : ∀ (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: 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
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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))
⊢ motive
    ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
        (a : SymmetricAlgebra R M) → A)
      y)
have 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))
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
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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))
⊢ motive
    ((((SymmetricAlgebra.lift : (a : M →ₗ[R] A) → SymmetricAlgebra R M →ₐ[R] A) f : SymmetricAlgebra R M →ₐ[R] A) :
        (a : SymmetricAlgebra R M) → A)
      y)
have 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))
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
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basis (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : Free R M
⊢ Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)
have let : ∀ (κ : Type uM) (b : Basis κ R M),
  Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)
Tactic: let ⟨⟨κ, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basis (hypothesis)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : Free R M
κ : Type uM
b : Basis κ R M
⊢ Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)
have this : Nonempty κ
Tactic: have : Nonempty κ := Basis.index_nonempty b
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basis (hypothesis)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : Free R M
κ : Type uM
b : Basis κ R M
this : Nonempty κ
⊢ Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)
have this₁ : Nontrivial R
Tactic: have : Nontrivial R := Module.nontrivial R M