awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ HAdd.hAdd (α := M ⊗[R] N) ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) (x + y) : M ⊗[R] N) (x + y) =
    HAdd.hAdd (α := M ⊗[R] N) ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) x : M ⊗[R] N) x +
      HAdd.hAdd (α := M ⊗[R] N) ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) y : M ⊗[R] N) y
have rw : HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N) ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) x : M ⊗[R] N)
      ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) y : M ⊗[R] N) +
    (x + y) =
  HAdd.hAdd (α := M ⊗[R] N) ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) x : M ⊗[R] N) x +
    HAdd.hAdd (α := M ⊗[R] N) ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) y : M ⊗[R] N) y
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
⊢ -(x + y) + (x + y) = 0
have suffices : -x + x + (-y + y) = 0
Tactic: suffices -x + x + (-y + y) = 0 by
      rw [← this]
      unfold Neg.neg neg
      simp only
      rw [map_add]
      abel
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
⊢ -x + x + (-y + y) = 0
have rw : 0 + (-y + y) = 0
Tactic: rw [hx, hy, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
rw : 0 + (-y + y) = 0
⊢ -x + x + (-y + y) = 0
have rw₁ : HAdd.hAdd (α := M ⊗[R] N) 0 0 = 0
Tactic: rw [hx, hy, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
rw : 0 + (-y + y) = 0
rw₁ : HAdd.hAdd (α := M ⊗[R] N) 0 0 = 0
⊢ -x + x + (-y + y) = 0
have rw₂ : Eq (α := M ⊗[R] N) 0 0
Tactic: rw [hx, hy, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : AddCommGroup P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
n : ℕ
x : M ⊗[R] N
⊢ Int.negSucc n • x = -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) x
have change : HSMul.hSMul (α := ℤ) (-(↑n.succ : ℤ)) x = -(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 • x)
Tactic: change (-n.succ : ℤ) • x = -(((n : ℤ) + 1) • x)
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : AddCommGroup P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
n : ℕ
x : M ⊗[R] N
⊢ HSMul.hSMul (α := ℤ) (-(↑n.succ : ℤ)) x = -(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 • x)
have rw : -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) x = -(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 • x)
Tactic: rw [← zero_add (_ • x), ← TensorProduct.neg_add_cancel ((n.succ : ℤ) • x), add_assoc,
      ← add_smul, ← sub_eq_add_neg, sub_self, zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq κ
𝒞 : Basis κ R N
m : M
n : N
⊢ Eq (α := κ →₀ M) ((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) (m ⊗ₜ[R] n) : κ →₀ M)
    (Finsupp.mapRange (fun (x : R) ↦ x • m) ⋯ ((𝒞.repr : (a : N) → κ →₀ R) n) : κ →₀ M)
have h : ∀ (a : κ),
  Eq.{u_3 + 1} (α := M)
    ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) (m ⊗ₜ[R] n) : κ →₀ M) : (a : κ) → M) a : M)
    ((Finsupp.mapRange (fun (x : R) ↦ x • m) sorry ((𝒞.repr : (a : N) → κ →₀ R) n) : (a : κ) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq κ
𝒞 : Basis κ R N
⊢ Eq (α := (κ →₀ M) →ₗ[R] M ⊗[R] N) (↑(LinearEquiv.symm (equivFinsuppOfBasisRight 𝒞)) : (κ →₀ M) →ₗ[R] M ⊗[R] N)
    ((Finsupp.lsum R : (a : κ → M →ₗ[R] M ⊗[R] N) → (κ →₀ M) →ₗ[R] M ⊗[R] N) fun (i : κ) ↦
      (LinearMap.flip (mk R M N) : (a : N) → M →ₗ[R] M ⊗[R] N) ((𝒞 : (a : κ) → N) i))
have h : ∀ (a : κ) (x : M),
  Eq (α := M ⊗[R] N)
    (((↑(LinearEquiv.symm (equivFinsuppOfBasisRight 𝒞)) : (κ →₀ M) →ₗ[R] M ⊗[R] N) ∘ₗ Finsupp.lsingle a :
          (a : M) → M ⊗[R] N)
        x :
      M ⊗[R] N)
    ((((Finsupp.lsum R : (a : κ → M →ₗ[R] M ⊗[R] N) → (κ →₀ M) →ₗ[R] M ⊗[R] N) fun (i : κ) ↦
              (LinearMap.flip (mk R M N) : (a : N) → M →ₗ[R] M ⊗[R] N) ((𝒞 : (a : κ) → N) i)) ∘ₗ
            Finsupp.lsingle a :
          (a : M) → M ⊗[R] N)
        x :
      M ⊗[R] N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq κ
𝒞 : Basis κ R N
x : M ⊗[R] N
i : κ
⊢ Eq.{u_3 + 1} (α := M) ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) x : κ →₀ M) : (a : κ) → M) i : M)
    ((TensorProduct.rid R M : (a : M ⊗[R] R) → M) ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) x : M ⊗[R] R) :
      M)
have zero : Eq.{u_3 + 1} (α := M) (((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) 0 : (a : κ) → M) i : M)
  ((TensorProduct.rid R M : (a : M ⊗[R] R) → M) ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) 0) : M)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq κ
𝒞 : Basis κ R N
x : M ⊗[R] N
i : κ
zero :
  Eq.{u_3 + 1} (α := M) (((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) 0 : (a : κ) → M) i : M)
    ((TensorProduct.rid R M : (a : M ⊗[R] R) → M) ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) 0) : M)
⊢ Eq.{u_3 + 1} (α := M) ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) x : κ →₀ M) : (a : κ) → M) i : M)
    ((TensorProduct.rid R M : (a : M ⊗[R] R) → M) ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) x : M ⊗[R] R) :
      M)
have tmul : ∀ (x : M) (y : N),
  Eq.{u_3 + 1} (α := M)
    ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) (x ⊗ₜ[R] y) : κ →₀ M) : (a : κ) → M) i : M)
    ((TensorProduct.rid R M : (a : M ⊗[R] R) → M)
        ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) (x ⊗ₜ[R] y) : M ⊗[R] R) :
      M)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq κ
𝒞 : Basis κ R N
x : M ⊗[R] N
i : κ
zero :
  Eq.{u_3 + 1} (α := M) (((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) 0 : (a : κ) → M) i : M)
    ((TensorProduct.rid R M : (a : M ⊗[R] R) → M) ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) 0) : M)
tmul :
  ∀ (x : M) (y : N),
    Eq.{u_3 + 1} (α := M)
      ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) (x ⊗ₜ[R] y) : κ →₀ M) : (a : κ) → M) i : M)
      ((TensorProduct.rid R M : (a : M ⊗[R] R) → M)
          ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) (x ⊗ₜ[R] y) : M ⊗[R] R) :
        M)
⊢ Eq.{u_3 + 1} (α := M) ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) x : κ →₀ M) : (a : κ) → M) i : M)
    ((TensorProduct.rid R M : (a : M ⊗[R] R) → M) ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) x : M ⊗[R] R) :
      M)
have add : ∀ (x y : M ⊗[R] N),
  Eq.{u_3 + 1} (α := M) ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) x : κ →₀ M) : (a : κ) → M) i : M)
      ((TensorProduct.rid R M : (a : M ⊗[R] R) → M) ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) x : M ⊗[R] R) :
        M) →
    Eq.{u_3 + 1} (α := M) ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) y : κ →₀ M) : (a : κ) → M) i : M)
        ((TensorProduct.rid R M : (a : M ⊗[R] R) → M)
            ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) y : M ⊗[R] R) :
          M) →
      Eq.{u_3 + 1} (α := M)
        ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) (x + y) : κ →₀ M) : (a : κ) → M) i : M)
        ((TensorProduct.rid R M : (a : M ⊗[R] R) → M)
            ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) (x + y) : M ⊗[R] R) :
          M)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
ℬ : Basis ι R M
x : M ⊗[R] N
i : ι
⊢ Eq.{u_4 + 1} (α := N) ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) x : ι →₀ N) : (a : ι) → N) i : N)
    ((TensorProduct.lid R N : (a : R ⊗[R] N) → N) ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) x : R ⊗[R] N) :
      N)
have zero : Eq.{u_4 + 1} (α := N) (((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) 0 : (a : ι) → N) i : N)
  ((TensorProduct.lid R N : (a : R ⊗[R] N) → N) ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) 0) : N)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
ℬ : Basis ι R M
x : M ⊗[R] N
i : ι
zero :
  Eq.{u_4 + 1} (α := N) (((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) 0 : (a : ι) → N) i : N)
    ((TensorProduct.lid R N : (a : R ⊗[R] N) → N) ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) 0) : N)
⊢ Eq.{u_4 + 1} (α := N) ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) x : ι →₀ N) : (a : ι) → N) i : N)
    ((TensorProduct.lid R N : (a : R ⊗[R] N) → N) ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) x : R ⊗[R] N) :
      N)
have tmul : ∀ (x : M) (y : N),
  Eq.{u_4 + 1} (α := N)
    ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) (x ⊗ₜ[R] y) : ι →₀ N) : (a : ι) → N) i : N)
    ((TensorProduct.lid R N : (a : R ⊗[R] N) → N)
        ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) (x ⊗ₜ[R] y) : R ⊗[R] N) :
      N)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
ℬ : Basis ι R M
x : M ⊗[R] N
i : ι
zero :
  Eq.{u_4 + 1} (α := N) (((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) 0 : (a : ι) → N) i : N)
    ((TensorProduct.lid R N : (a : R ⊗[R] N) → N) ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) 0) : N)
tmul :
  ∀ (x : M) (y : N),
    Eq.{u_4 + 1} (α := N)
      ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) (x ⊗ₜ[R] y) : ι →₀ N) : (a : ι) → N) i : N)
      ((TensorProduct.lid R N : (a : R ⊗[R] N) → N)
          ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) (x ⊗ₜ[R] y) : R ⊗[R] N) :
        N)
⊢ Eq.{u_4 + 1} (α := N) ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) x : ι →₀ N) : (a : ι) → N) i : N)
    ((TensorProduct.lid R N : (a : R ⊗[R] N) → N) ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) x : R ⊗[R] N) :
      N)
have add : ∀ (x y : M ⊗[R] N),
  Eq.{u_4 + 1} (α := N) ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) x : ι →₀ N) : (a : ι) → N) i : N)
      ((TensorProduct.lid R N : (a : R ⊗[R] N) → N) ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) x : R ⊗[R] N) :
        N) →
    Eq.{u_4 + 1} (α := N) ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) y : ι →₀ N) : (a : ι) → N) i : N)
        ((TensorProduct.lid R N : (a : R ⊗[R] N) → N)
            ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) y : R ⊗[R] N) :
          N) →
      Eq.{u_4 + 1} (α := N)
        ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) (x + y) : ι →₀ N) : (a : ι) → N) i : N)
        ((TensorProduct.lid R N : (a : R ⊗[R] N) → N)
            ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) (x + y) : R ⊗[R] N) :
          N)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
ℬ : Basis ι R M
⊢ Eq (α := (ι →₀ N) →ₗ[R] M ⊗[R] N) (↑(LinearEquiv.symm (equivFinsuppOfBasisLeft ℬ)) : (ι →₀ N) →ₗ[R] M ⊗[R] N)
    ((Finsupp.lsum R : (a : ι → N →ₗ[R] M ⊗[R] N) → (ι →₀ N) →ₗ[R] M ⊗[R] N) fun (i : ι) ↦
      (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) ((ℬ : (a : ι) → M) i))
have h : ∀ (a : ι) (x : N),
  Eq (α := M ⊗[R] N)
    (((↑(LinearEquiv.symm (equivFinsuppOfBasisLeft ℬ)) : (ι →₀ N) →ₗ[R] M ⊗[R] N) ∘ₗ Finsupp.lsingle a :
          (a : N) → M ⊗[R] N)
        x :
      M ⊗[R] N)
    ((((Finsupp.lsum R : (a : ι → N →ₗ[R] M ⊗[R] N) → (ι →₀ N) →ₗ[R] M ⊗[R] N) fun (i : ι) ↦
              (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) ((ℬ : (a : ι) → M) i)) ∘ₗ
            Finsupp.lsingle a :
          (a : N) → M ⊗[R] N)
        x :
      M ⊗[R] N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
ℬ : Basis ι R M
x : M ⊗[R] N
⊢ ∃ (c : ι →₀ N), (c.sum fun (i : ι) (n : N) ↦ (ℬ : (a : ι) → M) i ⊗ₜ[R] n) = x
have obtain : ∀ (c : ι →₀ N),
  ∃ (c_1 : ι →₀ N),
    Eq (α := M ⊗[R] N) (c_1.sum fun (i : ι) (n : N) ↦ (ℬ : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
      ((LinearEquiv.symm (equivFinsuppOfBasisLeft ℬ) : (a : ι →₀ N) → M ⊗[R] N) c : M ⊗[R] N)
Tactic: obtain ⟨c, rfl⟩ := (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
ℬ : Basis ι R M
x : M ⊗[R] N
⊢ ∃ (c : ι →₀ N), (c.sum fun (i : ι) (n : N) ↦ (ℬ : (a : ι) → M) i ⊗ₜ[R] n) = x
have classical : ∀ (c : ι →₀ N),
  ∃ (c_1 : ι →₀ N),
    Eq (α := M ⊗[R] N) (c_1.sum fun (i : ι) (n : N) ↦ (ℬ : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
      ((LinearEquiv.symm (equivFinsuppOfBasisLeft ℬ) : (a : ι →₀ N) → M ⊗[R] N) c : M ⊗[R] N)
Tactic: classical obtain ⟨c, rfl⟩ := (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Decomposition (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
⊢ Decomposition (σ := Submodule S (S ⊗[R] M)) fun (i : ι) ↦ Submodule.baseChange S (ℳ i)
have refine_1 : Eq (α := S ⊗[R] M →ₗ[S] S ⊗[R] M)
  ((coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
    (lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
          ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
        (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) ∘ₗ
      (((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
              (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
            (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) ∘ₗ
          ((↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) :
              S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
            S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
        S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)))
  LinearMap.id
Tactic: refine .ofLinearMap _ (lmap (ℳ · |>.toBaseChange S) ∘ₗ
    (directSumRight R S S fun i ↦ ℳ i).toLinearMap ∘ₗ
    ((decomposeLinearEquiv ℳ).baseChange R S)) ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Decomposition (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
refine_1 :
  Eq (α := S ⊗[R] M →ₗ[S] S ⊗[R] M)
    ((coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
      (lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
            ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
          (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) ∘ₗ
        (((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
                (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
              (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) ∘ₗ
            ((↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) :
                S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
              S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
          S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)))
    LinearMap.id
⊢ Decomposition (σ := Submodule S (S ⊗[R] M)) fun (i : ι) ↦ Submodule.baseChange S (ℳ i)
have refine_2 : Eq (α := (⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
  (((lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
          ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
        (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) ∘ₗ
      (((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
              (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
            (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) ∘ₗ
          ((↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) :
              S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
            S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
        S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i))) ∘ₗ
    coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i))
  LinearMap.id
Tactic: refine .ofLinearMap _ (lmap (ℳ · |>.toBaseChange S) ∘ₗ
    (directSumRight R S S fun i ↦ ℳ i).toLinearMap ∘ₗ
    ((decomposeLinearEquiv ℳ).baseChange R S)) ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Decomposition (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
⊢ Eq (α := S ⊗[R] M →ₗ[S] S ⊗[R] M)
    ((((coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
              lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
                ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
            (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] S ⊗[R] M) ∘ₗ
          ((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
              (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
            (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
        (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M) ∘ₗ
      ((↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) :
          S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
        S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)))
    LinearMap.id
have refine_1 : Eq (α := (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M)
  (((coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
          lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
            ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
        (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] S ⊗[R] M) ∘ₗ
      ((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
          (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
        (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
    (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M)
  (LinearMap.id ∘ₗ
      (↑(LinearEquiv.symm (LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ))) :
        (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M) :
    (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M)
Tactic: rw [← LinearEquiv.eq_comp_toLinearMap_symm]