awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
r : R
h :
  Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
    ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
this : Module.{u_1, u_2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
⊢ IsCentralScalar R M

Tactic:
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
r : R
h :
  Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
    ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
this_1 : Module.{u_1, u_2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R M
⊢ Eq (α := TrivSqZeroExt R M)
    ((toTrivSqZeroExt : (a : TensorAlgebra R M) → TrivSqZeroExt R M) ((ι R : (a : M) → TensorAlgebra R M) x) :
      TrivSqZeroExt R M)
    ((0, x) : R × M)

Tactic:
have hf0 : toTrivSqZeroExt (ι R x) = (0, x) := lift_ι_apply _ _
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
r : R
h :
  Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
    ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
this_1 : Module.{u_1, u_2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R M
hf0 :
  Eq (α := TrivSqZeroExt R M)
    ((toTrivSqZeroExt : (a : TensorAlgebra R M) → TrivSqZeroExt R M) ((ι R : (a : M) → TensorAlgebra R M) x) :
      TrivSqZeroExt R M)
    ((0, x) : R × M)
⊢ Eq (α := TrivSqZeroExt R M) ((algebraMap R (TrivSqZeroExt R M) : (a : R) → TrivSqZeroExt R M) r : TrivSqZeroExt R M)
    ((0, x) : R × M)

Tactic:
rw [h, AlgHom.commutes] at hf0

Premises used: AlgHom.commutes
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
r : R
h :
  Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
    ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
this_1 : Module.{u_1, u_2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R M
hf0 :
  Eq (α := TrivSqZeroExt R M) ((algebraMap R (TrivSqZeroExt R M) : (a : R) → TrivSqZeroExt R M) r : TrivSqZeroExt R M)
    ((0, x) : R × M)
⊢ r = 0 ∧ 0 = x

Tactic:
have : r = 0 ∧ 0 = x := Prod.ext_iff.1 hf0
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
r : R
h :
  Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
    ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
this_1 : Module.{u_1, u_2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this_2 : IsCentralScalar R M
hf0 :
  Eq (α := TrivSqZeroExt R M) ((algebraMap R (TrivSqZeroExt R M) : (a : R) → TrivSqZeroExt R M) r : TrivSqZeroExt R M)
    ((0, x) : R × M)
this : r = 0 ∧ 0 = x
⊢ x = 0 ∧ r = 0

Tactic:
this.symm.imp_left Eq.symm

Premises used: And.imp_left, Eq.symm, And.symm
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
r : R
h :
  Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
    ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
this_1 : Module.{u_1, u_2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this_2 : IsCentralScalar R M
hf0 :
  Eq (α := TrivSqZeroExt R M) ((algebraMap R (TrivSqZeroExt R M) : (a : R) → TrivSqZeroExt R M) r : TrivSqZeroExt R M)
    ((0, x) : R × M)
this : r = 0 ∧ 0 = x
⊢ x = 0 ∧ r = 0

Tactic:
exact this.symm.imp_left Eq.symm

Premises used: And.imp_left, Eq.symm, And.symm
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
refine_2 : Eq (α := TensorAlgebra R M) 0 ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) 0)
refine_2₁ refine_2₂ : Eq (α := TensorAlgebra R M) 0 0
⊢ Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) 0)
    ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) 0)

Tactic:
rw [map_zero, map_zero]

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
x : M
rw : ¬(x = 0 ∧ Eq.{u_1 + 1} (α := R) 1 0)
⊢ Ne (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) (1 : TensorAlgebra R M)

Tactic:
rw [← (algebraMap R (TensorAlgebra R M)).map_one, Ne, ι_eq_algebraMap_iff]

Premises used: Algebra.algebraMap, RingHom.map_one, Ne, TensorAlgebra, TensorAlgebra.ι_eq_algebraMap_iff
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
x : M
⊢ ¬(x = 0 ∧ Eq.{u_1 + 1} (α := R) 1 0)

Tactic:
one_ne_zero ∘ And.right

Premises used: Function.comp, And.right, one_ne_zero, Not
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
x : M
⊢ ¬(x = 0 ∧ Eq.{u_1 + 1} (α := R) 1 0)

Tactic:
exact one_ne_zero ∘ And.right

Premises used: And.right, one_ne_zero
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw :
  ∀ (x : TensorAlgebra R M),
    Membership.mem (γ := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x →
      Membership.mem (γ := Submodule R (TensorAlgebra R M)) (LinearMap.range (Algebra.linearMap R (TensorAlgebra R M)))
          x →
        x = 0
⊢ Disjoint (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) 1

Tactic:
rw [Submodule.disjoint_def, Submodule.one_eq_range]

Premises used: Submodule.disjoint_def, Submodule.one_eq_range
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
r : R
hx :
  Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
    ((Algebra.linearMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
⊢ x = 0 ∧ r = 0

Tactic:
rw [Algebra.linearMap_apply, ι_eq_algebraMap_iff] at hx

Premises used: Algebra.linearMap_apply, TensorAlgebra.ι_eq_algebraMap_iff
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
r : R
hx : x = 0 ∧ r = 0
rw : Eq (α := TensorAlgebra R M) ((Algebra.linearMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) 0) 0
rw₁ rw₂ : Eq (α := TensorAlgebra R M) 0 0
⊢ Eq (α := TensorAlgebra R M)
    ((Algebra.linearMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
    (0 : TensorAlgebra R M)

Tactic:
rw [hx.2, map_zero]

Premises used: map_zero, And.right
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : Fin n → M
⊢ Eq (α := TensorAlgebra R M) ((tprod R M n : (a : (i : Fin n) → M) → TensorAlgebra R M) x : TensorAlgebra R M)
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → TensorAlgebra R M) (x i)) : TensorAlgebra R M)

Tactic:
rfl

Premises used: rfl, List.prod
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
⊢ Eq (α := TensorAlgebra R M) ((toTensor : (a : FreeAlgebra R M) → TensorAlgebra R M) (ι R m) : TensorAlgebra R M)
    ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)

Tactic:
simp [toTensor]

Premises used: FreeAlgebra.toTensor
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.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
w :
  ∀ (x : κ),
    Eq (α := FreeAlgebra R κ)
      (Function.comp (β := FreeAlgebra R κ)
        (⇑(AlgHom.comp (B := TensorAlgebra R M)
              ((lift R : (a : M →ₗ[R] FreeAlgebra R κ) → TensorAlgebra R M →ₐ[R] FreeAlgebra R κ)
                (Finsupp.linearCombination R (FreeAlgebra.ι R) ∘ₗ (↑b.repr : M →ₗ[R] κ →₀ R)))
              ((FreeAlgebra.lift R : (a : κ → TensorAlgebra R M) → FreeAlgebra R κ →ₐ[R] TensorAlgebra R M)
                (Function.comp (β := M) (⇑(ι R) : (a : M) → TensorAlgebra R M) (⇑b : (a : κ) → M)))) :
          (a : FreeAlgebra R κ) → FreeAlgebra R κ)
        (FreeAlgebra.ι R) x)
      (Function.comp (β := FreeAlgebra R κ) (⇑(AlgHom.id R (FreeAlgebra R κ)) : (a : FreeAlgebra R κ) → FreeAlgebra R κ)
        (FreeAlgebra.ι R) x)
⊢ Eq (α := FreeAlgebra R κ →ₐ[R] FreeAlgebra R κ)
    (AlgHom.comp (B := TensorAlgebra R M)
      ((lift R : (a : M →ₗ[R] FreeAlgebra R κ) → TensorAlgebra R M →ₐ[R] FreeAlgebra R κ)
        (Finsupp.linearCombination R (FreeAlgebra.ι R) ∘ₗ (↑b.repr : M →ₗ[R] κ →₀ R)))
      ((FreeAlgebra.lift R : (a : κ → TensorAlgebra R M) → FreeAlgebra R κ →ₐ[R] TensorAlgebra R M)
        (Function.comp (β := M) (⇑(ι R) : (a : M) → TensorAlgebra R M) (⇑b : (a : κ) → M))))
    (AlgHom.id R (FreeAlgebra R κ))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.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
x : κ
⊢ Eq (α := FreeAlgebra R κ)
    (Function.comp (β := FreeAlgebra R κ)
      (⇑(AlgHom.comp (B := TensorAlgebra R M)
            ((lift R : (a : M →ₗ[R] FreeAlgebra R κ) → TensorAlgebra R M →ₐ[R] FreeAlgebra R κ)
              (Finsupp.linearCombination R (FreeAlgebra.ι R) ∘ₗ (↑b.repr : M →ₗ[R] κ →₀ R)))
            ((FreeAlgebra.lift R : (a : κ → TensorAlgebra R M) → FreeAlgebra R κ →ₐ[R] TensorAlgebra R M)
              (Function.comp (β := M) (⇑(ι R) : (a : M) → TensorAlgebra R M) (⇑b : (a : κ) → M)))) :
        (a : FreeAlgebra R κ) → FreeAlgebra R κ)
      (FreeAlgebra.ι R) x)
    (Function.comp (β := FreeAlgebra R κ) (⇑(AlgHom.id R (FreeAlgebra R κ)) : (a : FreeAlgebra R κ) → FreeAlgebra R κ)
      (FreeAlgebra.ι R) x)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.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 (α := TensorAlgebra R M)
    ((AlgHom.toLinearMap
              (AlgHom.comp (B := FreeAlgebra R κ)
                ((FreeAlgebra.lift R : (a : κ → TensorAlgebra R M) → FreeAlgebra R κ →ₐ[R] TensorAlgebra R M)
                  (Function.comp (β := M) (⇑(ι R) : (a : M) → TensorAlgebra R M) (⇑b : (a : κ) → M)))
                ((lift R : (a : M →ₗ[R] FreeAlgebra R κ) → TensorAlgebra R M →ₐ[R] FreeAlgebra R κ)
                  (Finsupp.linearCombination R (FreeAlgebra.ι R) ∘ₗ (↑b.repr : M →ₗ[R] κ →₀ R)))) ∘ₗ
            ι R :
          (a : M) → TensorAlgebra R M)
        ((b : (a : κ) → M) i) :
      TensorAlgebra R M)
    ((AlgHom.toLinearMap (AlgHom.id R (TensorAlgebra R M)) ∘ₗ ι R : (a : M) → TensorAlgebra R M) ((b : (a : κ) → M) i) :
      TensorAlgebra R M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.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 (α := FreeAlgebra R κ)
    ((Finsupp.linearCombination R (FreeAlgebra.ι R) ∘ₗ (↑b.repr : M →ₗ[R] κ →₀ R) : (a : M) → FreeAlgebra R κ)
        ((b : (a : κ) → M) i) :
      FreeAlgebra R κ)
    (FreeAlgebra.ι R i : FreeAlgebra R κ)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.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 (α := TensorAlgebra R M)
    (((equivFreeAlgebra b).symm : (a : FreeAlgebra R κ) → TensorAlgebra R M) (FreeAlgebra.ι R i) : TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) ((b : (a : κ) → M) i) : TensorAlgebra R M)

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

Premises used: Iff.mpr, TensorAlgebra.equivFreeAlgebra_ι_apply, Equiv.symm_apply_eq, AlgEquiv.toEquiv, Eq.symm, TensorAlgebra.equivFreeAlgebra
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.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 (TensorAlgebra R M)

Tactic:
let ⟨⟨_κ, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
  .of_basis b.tensorAlgebra

Premises used: TensorAlgebra, Module.Free, Module.Basis.tensorAlgebra, Module.Free.of_basis, _private.0.TensorAlgebra.instModuleFree.match_1, Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.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 (TensorAlgebra R M)

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

Premises used: TensorAlgebra, AlgEquiv.toMulEquiv, FreeAlgebra, _private.0.TensorAlgebra.instNoZeroDivisors.match_1, NoZeroDivisors, MulEquiv.noZeroDivisors, TensorAlgebra.equivFreeAlgebra
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.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 (TensorAlgebra R M)

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basis
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Free R M
let :
  ∀ (κ : Type uM) (b : Basis κ R M),
    Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
⊢ Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)

Tactic:
let ⟨⟨κ, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basis
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Free R M
κ : Type uM
b : Basis κ R M
rw : Module.rank R (FreeAlgebra R κ) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
rw₁ : Cardinal.lift.{uR, uM} #(List κ) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
rw₂ : Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ #κ ^ n) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
rw₃ rw₄ :
  Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n) =
    Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
⊢ Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)

Tactic:
rw [(equivFreeAlgebra b).toLinearEquiv.rank_eq, FreeAlgebra.rank_eq, mk_list_eq_sum_pow,
    Basis.mk_eq_rank'' b]

Premises used: Cardinal.mk_list_eq_sum_pow, FreeAlgebra.rank_eq, LinearEquiv.rank_eq, AlgEquiv.toLinearEquiv, TensorAlgebra.equivFreeAlgebra, Module.Basis.mk_eq_rank''
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
⊢ Membership.mem (α := TensorAlgebra R M)
    (HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (TensorAlgebra.ι R)) 1)
    ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)

Tactic:
simpa only [pow_one] using LinearMap.mem_range_self _ m

Premises used: LinearMap.mem_range_self, pow_one
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
⊢ Eq (α := ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (TensorAlgebra.ι R)) i))
    ((ι R M : (a : M) → ⨁ (i : ℕ), ↥((TensorAlgebra.ι R).range ^ i)) m :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (TensorAlgebra.ι R)) i))
    (((DirectSum.of
              (fun (i : ℕ) ↦
                ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (TensorAlgebra.ι R)) i))
              1 :
            ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (TensorAlgebra.ι R)) 1) →+
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (TensorAlgebra.ι R)) i)) :
          (a : ↥((TensorAlgebra.ι R).range ^ 1)) → ⨁ (i : ℕ), ↥((TensorAlgebra.ι R).range ^ i))
        (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
          x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (TensorAlgebra.ι R)) 1)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m) ⋯) :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (TensorAlgebra.ι R)) i))

Tactic:
rfl

Premises used: Set.Mem, DFinsupp.single, rfl
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
w :
  ∀ (m : M),
    Eq (α := TensorAlgebra R M)
      ((AlgHom.toLinearMap
                (AlgHom.comp (B :=
                  ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
                  (DirectSum.coeAlgHom fun (x : ℕ) ↦
                    HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x)
                  ((lift R :
                      (a : M →ₗ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i)) →
                        TensorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i))
                    (GradedAlgebra.ι R M))) ∘ₗ
              ι R :
            (a : M) → TensorAlgebra R M)
          m :
        TensorAlgebra R M)
      ((AlgHom.toLinearMap (AlgHom.id R (TensorAlgebra R M)) ∘ₗ ι R : (a : M) → TensorAlgebra R M) m :
        TensorAlgebra R M)
⊢ Eq (α := TensorAlgebra R M →ₐ[R] TensorAlgebra R M)
    (AlgHom.comp (B := ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
      (DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x)
      ((lift R : (a : M →ₗ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (GradedAlgebra.ι R M)))
    (AlgHom.id R (TensorAlgebra R M))

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
w :
  Eq (α := TensorAlgebra R M)
    ((DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x :
          (a : ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M)
        ((GradedAlgebra.ι R M : (a : M) → ⨁ (i : ℕ), ↥((ι R).range ^ i)) m) :
      TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
w₁ :
  Eq (α := TensorAlgebra R M)
    ((DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x :
          (a : ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M)
        (((DirectSum.of (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
                1 :
              ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 1) →+
                ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
            (a : ↥((ι R).range ^ 1)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
          (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
            x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 1)
            ((ι R : (a : M) → TensorAlgebra R M) m) ⋯)) :
      TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
w₂ :
  Eq (α := TensorAlgebra R M)
    ((↑(Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
            x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 1)
            ((ι R : (a : M) → TensorAlgebra R M) m) ⋯) :
        TensorAlgebra R M) :
      TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
w₃ w₄ :
  Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
⊢ Eq (α := TensorAlgebra R M)
    ((DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x :
          (a : ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M)
        ((((lift R :
                  (a : M →ₗ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i))
                (GradedAlgebra.ι R M) :
              TensorAlgebra R M →ₐ[R]
                ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
            (a : TensorAlgebra R M) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
          ((ι R : (a : M) → TensorAlgebra R M) m)) :
      TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)

Tactic:
rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]

Premises used: Subtype.coe_mk, TensorAlgebra.lift_ι_apply, DirectSum.coeAlgHom_of, TensorAlgebra.GradedAlgebra.ι_apply