awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : TensorAlgebra R M
algebraMap :
  ∀ (r : R),
    Membership.mem (α := TensorAlgebra R M) (γ := Subalgebra R (TensorAlgebra R M))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M)))
      ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
add :
  ∀ (x y : TensorAlgebra R M)
    (hx :
      Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) x)
    (hy :
      Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) y),
    Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) (x + y)
⊢ Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) x
have mul : ∀ (x y : TensorAlgebra R M)
  (hx :
    Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) x)
  (hy :
    Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) y),
  Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) (x * y)
Tactic: induction x using induction with
  | algebraMap => exact algebraMap_mem _ _
  | add x y hx hy => exact add_mem hx hy
  | mul x y hx hy => exact mul_mem hx hy
  | ι x => exact Algebra.subset_adjoin (Set.mem_range_self _)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : TensorAlgebra R M
algebraMap :
  ∀ (r : R),
    Membership.mem (α := TensorAlgebra R M) (γ := Subalgebra R (TensorAlgebra R M))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M)))
      ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
add :
  ∀ (x y : TensorAlgebra R M)
    (hx :
      Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) x)
    (hy :
      Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) y),
    Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) (x + y)
mul :
  ∀ (x y : TensorAlgebra R M)
    (hx :
      Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) x)
    (hy :
      Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) y),
    Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) (x * y)
⊢ Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) x
have ι : ∀ (x : M),
  Membership.mem (α := TensorAlgebra R M) (γ := Subalgebra R (TensorAlgebra R M))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M)))
    ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
Tactic: induction x using induction with
  | algebraMap => exact algebraMap_mem _ _
  | add x y hx hy => exact add_mem hx hy
  | mul x y hx hy => exact mul_mem hx hy
  | ι x => exact Algebra.subset_adjoin (Set.mem_range_self _)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
⊢ Eq.{u_3 + 1} (α := Subalgebra R A)
    (AlgHom.range (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
have simp_rw : Eq.{u_3 + 1} (α := Subalgebra R A)
  (Subalgebra.map (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f) ⊤)
  (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
Tactic: simp_rw [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, lift_ι_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
simp_rw :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Subalgebra.map (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f) ⊤)
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
⊢ Eq.{u_3 + 1} (α := Subalgebra R A)
    (AlgHom.range (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
have simp_rw₁ : Eq.{u_3 + 1} (α := Subalgebra R A)
  (Subalgebra.map (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f)
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))))
  (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
Tactic: simp_rw [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, lift_ι_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
simp_rw :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Subalgebra.map (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f) ⊤)
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
simp_rw₁ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Subalgebra.map (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f)
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
⊢ Eq.{u_3 + 1} (α := Subalgebra R A)
    (AlgHom.range (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
have simp_rw₂ : Eq.{u_3 + 1} (α := Subalgebra R A)
  (Algebra.adjoin R
    (Set.image (α := TensorAlgebra R M)
      (⇑((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f : TensorAlgebra R M →ₐ[R] A) :
        (a : TensorAlgebra R M) → A)
      (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))))
  (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
Tactic: simp_rw [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, lift_ι_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
simp_rw :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Subalgebra.map (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f) ⊤)
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
simp_rw₁ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Subalgebra.map (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f)
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
simp_rw₂ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Algebra.adjoin R
      (Set.image (α := TensorAlgebra R M)
        (⇑((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f : TensorAlgebra R M →ₐ[R] A) :
          (a : TensorAlgebra R M) → A)
        (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
⊢ Eq.{u_3 + 1} (α := Subalgebra R A)
    (AlgHom.range (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
have simp_rw₃ : Eq.{u_3 + 1} (α := Subalgebra R A)
  (Algebra.adjoin R
    (Set.range.{u_3, u_2 + 1} (ι := M)
      (Function.comp (β := TensorAlgebra R M)
        (⇑((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f : TensorAlgebra R M →ₐ[R] A) :
          (a : TensorAlgebra R M) → A)
        (⇑(ι R) : (a : M) → TensorAlgebra R M))))
  (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
Tactic: simp_rw [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, lift_ι_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
simp_rw :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Subalgebra.map (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f) ⊤)
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
simp_rw₁ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Subalgebra.map (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f)
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
simp_rw₂ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Algebra.adjoin R
      (Set.image (α := TensorAlgebra R M)
        (⇑((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f : TensorAlgebra R M →ₐ[R] A) :
          (a : TensorAlgebra R M) → A)
        (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
simp_rw₃ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Algebra.adjoin R
      (Set.range.{u_3, u_2 + 1} (ι := M)
        (Function.comp (β := TensorAlgebra R M)
          (⇑((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f : TensorAlgebra R M →ₐ[R] A) :
            (a : TensorAlgebra R M) → A)
          (⇑(ι R) : (a : M) → TensorAlgebra R M))))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
⊢ Eq.{u_3 + 1} (α := Subalgebra R A)
    (AlgHom.range (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
have simp_rw₄ : Eq.{u_3 + 1} (α := Subalgebra R A)
  (Algebra.adjoin R
    (Set.range fun (x : M) ↦
      (((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f : TensorAlgebra R M →ₐ[R] A) :
          (a : TensorAlgebra R M) → A)
        ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)))
  (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
Tactic: simp_rw [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, lift_ι_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
this : Module.{u_1, u_2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
⊢ TensorAlgebra R M →ₗ[R] M
have this₁ : IsCentralScalar R M
Tactic: haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) (0 : TensorAlgebra R M) ↔
    x = 0
have rw : Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) (0 : TensorAlgebra R M) ↔
  Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) 0 : TensorAlgebra R M)
Tactic: rw [← ι_inj R x 0, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
rw :
  Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) (0 : TensorAlgebra R M) ↔
    Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
      ((ι R : (a : M) → TensorAlgebra R M) 0 : TensorAlgebra R M)
⊢ Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) (0 : TensorAlgebra R M) ↔
    x = 0
have rw₁ : Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) (0 : TensorAlgebra R M) ↔
  Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) (0 : TensorAlgebra R M)
Tactic: rw [← ι_inj R x 0, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
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
⊢ 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) ↔
    x = 0 ∧ r = 0
have refine_1 : ∀
  (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)),
  x = 0 ∧ r = 0
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
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
refine_1 :
  ∀
    (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)),
    x = 0 ∧ r = 0
⊢ 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) ↔
    x = 0 ∧ r = 0
have refine_2 : x = 0 ∧ r = 0 →
  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)
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (hypothesis)
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) ⋯)
⊢ x = 0 ∧ r = 0
have this₁ : IsCentralScalar R M
Tactic: haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (hypothesis)
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
⊢ x = 0 ∧ r = 0
have 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)
Tactic: have hf0 : toTrivSqZeroExt (ι R x) = (0, x) := lift_ι_apply _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (hypothesis)
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)
⊢ x = 0 ∧ r = 0
have hf0₁ : 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
Cleared hypotheses: hf0
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (hypothesis)
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)
⊢ x = 0 ∧ r = 0
have this₁ : r = 0 ∧ 0 = x
Tactic: have : r = 0 ∧ 0 = x := Prod.ext_iff.1 hf0
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) 0)
    ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) 0)
have refine_2 : Eq (α := TensorAlgebra R M) 0 ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) 0)
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
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)
⊢ Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) 0)
    ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) 0)
have refine_2₁ : Eq (α := TensorAlgebra R M) 0 0
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
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
⊢ Ne (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) (1 : TensorAlgebra R M)
have rw : ¬(x = 0 ∧ Eq.{u_1 + 1} (α := R) 1 0)
Tactic: rw [← (algebraMap R (TensorAlgebra R M)).map_one, Ne, ι_eq_algebraMap_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Disjoint (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) 1
have 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
Tactic: rw [Submodule.disjoint_def, Submodule.one_eq_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (hypothesis)
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)
⊢ Eq (α := TensorAlgebra R M)
    ((Algebra.linearMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
    (0 : TensorAlgebra R M)
have hx₁ : x = 0 ∧ r = 0
Tactic: rw [Algebra.linearMap_apply, ι_eq_algebraMap_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
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
⊢ Eq (α := TensorAlgebra R M)
    ((Algebra.linearMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
    (0 : TensorAlgebra R M)
have rw : Eq (α := TensorAlgebra R M) ((Algebra.linearMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) 0) 0
Tactic: rw [hx.2, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
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
⊢ Eq (α := TensorAlgebra R M)
    ((Algebra.linearMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
    (0 : TensorAlgebra R M)
have rw₁ : Eq (α := TensorAlgebra R M) 0 0
Tactic: rw [hx.2, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basis (goal)
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
⊢ 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 κ))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basis (goal)
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
⊢ Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
have 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)
Tactic: let ⟨⟨κ, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)