awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst_3 : DecidableEq ι'
x : M
i' : ι
k : ι'
h : k = j
pos :
  Eq.{u_5 + 1} (α := R)
    ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x j) : ι →₀ R) : (a : ι) → R) i' : R)
    ((((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' : R)
⊢ Eq.{u_5 + 1} (α := R)
    ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x k) : ι →₀ R) : (a : ι) → R) i' : R)
    ((((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' : R)
have pos₁ : Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' : R)
  ((((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' : R)
Tactic: rw [h, update_self j x v]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst_3 : DecidableEq ι'
x : M
i' : ι
k : ι'
h : ¬k = j
⊢ Eq.{u_5 + 1} (α := R)
    ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x k) : ι →₀ R) : (a : ι) → R) i' : R)
    ((((e.repr : (a : M) → ι →₀ R) (v k) : ι →₀ R) : (a : ι) → R) i' : R)
have neg : Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) (v k) : ι →₀ R) : (a : ι) → R) i' : R)
  ((((e.repr : (a : M) → ι →₀ R) (v k) : ι →₀ R) : (a : ι) → R) i' : R)
Tactic: rw [update_of_ne h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
⊢ e.toMatrix (⇑(e.unitsSMul w) : (a : ι) → M₂) = Matrix.diagonal (Units.val ∘ w)
have a : ∀ (i j : ι), e.toMatrix (⇑(e.unitsSMul w) : (a : ι) → M₂) i j = Matrix.diagonal (Units.val ∘ w) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
⊢ e.toMatrix (⇑(e.unitsSMul w) : (a : ι) → M₂) i j = Matrix.diagonal (Units.val ∘ w) i j
have pos : ∀ (h : i = j), e.toMatrix (⇑(e.unitsSMul w) : (a : ι) → M₂) i j = Matrix.diagonal (Units.val ∘ w) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
pos : ∀ (h : i = j), e.toMatrix (⇑(e.unitsSMul w) : (a : ι) → M₂) i j = Matrix.diagonal (Units.val ∘ w) i j
⊢ e.toMatrix (⇑(e.unitsSMul w) : (a : ι) → M₂) i j = Matrix.diagonal (Units.val ∘ w) i j
have neg : ∀ (h : ¬i = j), e.toMatrix (⇑(e.unitsSMul w) : (a : ι) → M₂) i j = Matrix.diagonal (Units.val ∘ w) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst_3 : Fintype ι
⊢ ∑ i : ι, HSMul.hSMul (β := M) (e.toMatrix v i j) ((e : (a : ι) → M) i : M) = v j
have simp_rw : ∑ x : ι,
    HSMul.hSMul.{u_5, u_6, u_6} (α := R) (β := M) ((((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) x : R)
      ((e : (a : ι) → M) x : M) =
  v j
Tactic: simp_rw [e.toMatrix_apply, e.sum_repr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst : CommSemiring R₁
inst_1 : Semiring S
inst_2 : Algebra R₁ S
inst_3 : Fintype ι
inst_4 : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
⊢ b.toMatrix (x • w) =
    HMul.hMul (α := Matrix ι ι R₁) ((Algebra.leftMulMatrix b : (a : S) → Matrix ι ι R₁) x : Matrix ι ι R₁)
      (b.toMatrix w)
have a : ∀ (i j : ι),
  b.toMatrix (x • w) i j =
    HMul.hMul (α := Matrix ι ι R₁) ((Algebra.leftMulMatrix b : (a : S) → Matrix ι ι R₁) x : Matrix ι ι R₁)
      (b.toMatrix w) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst : CommSemiring R₁
inst_1 : Semiring S
inst_2 : Algebra R₁ S
inst_3 : Fintype ι
inst_4 : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
i j : ι
⊢ b.toMatrix (x • w) i j =
    HMul.hMul (α := Matrix ι ι R₁) ((Algebra.leftMulMatrix b : (a : S) → Matrix ι ι R₁) x : Matrix ι ι R₁)
      (b.toMatrix w) i j
have a : mulVec (n := ι) ((Algebra.leftMulMatrix b : (a : S) → Matrix ι ι R₁) x)
    (⇑((b.repr : (a : S) → ι →₀ R₁) (w j) : ι →₀ R₁) : (a : ι) → R₁) i =
  HMul.hMul (α := Matrix ι ι R₁) ((Algebra.leftMulMatrix b : (a : S) → Matrix ι ι R₁) x : Matrix ι ι R₁) (b.toMatrix w)
    i j
Tactic: rw [Basis.toMatrix_apply, Pi.smul_apply, smul_eq_mul, ← Algebra.leftMulMatrix_mulVec_repr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
inst : CommSemiring R
S : Type u_9
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Fintype ι
b : Basis ι R S
v : ι' → S
⊢ (⇑b : (a : ι) → S) ᵥ* (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S) = v
have h : ∀ (i : ι'), ((⇑b : (a : ι) → S) ᵥ* (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S)) i = v i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
inst : CommSemiring R
S : Type u_9
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Fintype ι
b : Basis ι R S
v : ι' → S
i : ι'
⊢ ((⇑b : (a : ι) → S) ᵥ* (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S)) i = v i
have h : ((⇑b : (a : ι) → S) ⬝ᵥ fun (i_1 : ι) ↦ (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S) i_1 i) = v i
Tactic: simp_rw [vecMul, dotProduct, Matrix.map_apply, ← Algebra.commutes, ← Algebra.smul_def,
    sum_toMatrix_smul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
inst : CommSemiring R
S : Type u_9
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Fintype ι
b : Basis ι R S
v : ι' → S
i : ι'
h : ((⇑b : (a : ι) → S) ⬝ᵥ fun (i_1 : ι) ↦ (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S) i_1 i) = v i
⊢ ((⇑b : (a : ι) → S) ᵥ* (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S)) i = v i
have h₁ : ∑ x : ι,
    HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) x : S)
      ((b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S) x i : S) =
  v i
Tactic: simp_rw [vecMul, dotProduct, Matrix.map_apply, ← Algebra.commutes, ← Algebra.smul_def,
    sum_toMatrix_smul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
inst : CommSemiring R
S : Type u_9
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Fintype ι
b : Basis ι R S
v : ι' → S
i : ι'
h : ((⇑b : (a : ι) → S) ⬝ᵥ fun (i_1 : ι) ↦ (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S) i_1 i) = v i
h₁ :
  ∑ x : ι,
      HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) x : S)
        ((b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S) x i : S) =
    v i
⊢ ((⇑b : (a : ι) → S) ᵥ* (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S)) i = v i
have h₂ : ∑ x : ι, HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) x : S) ((algebraMap R S : (a : R) → S) (b.toMatrix v x i) : S) =
  v i
Tactic: simp_rw [vecMul, dotProduct, Matrix.map_apply, ← Algebra.commutes, ← Algebra.smul_def,
    sum_toMatrix_smul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
inst : CommSemiring R
S : Type u_9
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Fintype ι
b : Basis ι R S
v : ι' → S
i : ι'
h : ((⇑b : (a : ι) → S) ⬝ᵥ fun (i_1 : ι) ↦ (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S) i_1 i) = v i
h₁ :
  ∑ x : ι,
      HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) x : S)
        ((b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S) x i : S) =
    v i
h₂ :
  ∑ x : ι,
      HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) x : S) ((algebraMap R S : (a : R) → S) (b.toMatrix v x i) : S) =
    v i
⊢ ((⇑b : (a : ι) → S) ᵥ* (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S)) i = v i
have h₃ : ∑ x : ι, HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (b.toMatrix v x i) : S) ((b : (a : ι) → S) x : S) =
  v i
Tactic: simp_rw [vecMul, dotProduct, Matrix.map_apply, ← Algebra.commutes, ← Algebra.smul_def,
    sum_toMatrix_smul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
inst : CommSemiring R
S : Type u_9
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Fintype ι
b : Basis ι R S
v : ι' → S
i : ι'
h : ((⇑b : (a : ι) → S) ⬝ᵥ fun (i_1 : ι) ↦ (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S) i_1 i) = v i
h₁ :
  ∑ x : ι,
      HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) x : S)
        ((b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S) x i : S) =
    v i
h₂ :
  ∑ x : ι,
      HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) x : S) ((algebraMap R S : (a : R) → S) (b.toMatrix v x i) : S) =
    v i
h₃ :
  ∑ x : ι,
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (b.toMatrix v x i) : S) ((b : (a : ι) → S) x : S) =
    v i
⊢ ((⇑b : (a : ι) → S) ᵥ* (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S)) i = v i
have h₄ : ∑ x : ι, HSMul.hSMul (β := S) (b.toMatrix v x i) ((b : (a : ι) → S) x : S) = v i
Tactic: simp_rw [vecMul, dotProduct, Matrix.map_apply, ← Algebra.commutes, ← Algebra.smul_def,
    sum_toMatrix_smul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : Finite ι
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
v : Basis ι' R M
i : ι'
⊢ Eq.{u_6 + 1} (α := M)
    ((((toLin v e : (a : Matrix ι ι' R) → M →ₗ[R] M) (e.toMatrix (⇑v : (a : ι') → M)) : M →ₗ[R] M) : (a : M) → M)
        ((v : (a : ι') → M) i : M) :
      M)
    ((LinearMap.id : (a : M) → M) ((v : (a : ι') → M) i : M) : M)
have intro : ∀ (val : Fintype ι),
  Eq.{u_6 + 1} (α := M)
    ((((toLin v e : (a : Matrix ι ι' R) → M →ₗ[R] M) (e.toMatrix (⇑v : (a : ι') → M)) : M →ₗ[R] M) : (a : M) → M)
        ((v : (a : ι') → M) i : M) :
      M)
    ((LinearMap.id : (a : M) → M) ((v : (a : ι') → M) i : M) : M)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : Finite ι
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
v : Basis ι' R M
i : ι'
val : Fintype ι
⊢ Eq.{u_6 + 1} (α := M)
    ((((toLin v e : (a : Matrix ι ι' R) → M →ₗ[R] M) (e.toMatrix (⇑v : (a : ι') → M)) : M →ₗ[R] M) : (a : M) → M)
        ((v : (a : ι') → M) i : M) :
      M)
    ((LinearMap.id : (a : M) → M) ((v : (a : ι') → M) i : M) : M)
have intro : Eq.{u_6 + 1} (α := M) (∑ j : ι, HSMul.hSMul (β := M) (e.toMatrix (⇑v : (a : ι') → M) j i) ((e : (a : ι) → M) j : M) : M)
  ((LinearMap.id : (a : M) → M) ((v : (a : ι') → M) i : M) : M)
Tactic: rw [toLin_self, id_apply, e.sum_toMatrix_smul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : Finite ι
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
v : Basis ι' R M
i : ι'
val : Fintype ι
intro :
  Eq.{u_6 + 1} (α := M)
    (∑ j : ι, HSMul.hSMul (β := M) (e.toMatrix (⇑v : (a : ι') → M) j i) ((e : (a : ι) → M) j : M) : M)
    ((LinearMap.id : (a : M) → M) ((v : (a : ι') → M) i : M) : M)
⊢ Eq.{u_6 + 1} (α := M)
    ((((toLin v e : (a : Matrix ι ι' R) → M →ₗ[R] M) (e.toMatrix (⇑v : (a : ι') → M)) : M →ₗ[R] M) : (a : M) → M)
        ((v : (a : ι') → M) i : M) :
      M)
    ((LinearMap.id : (a : M) → M) ((v : (a : ι') → M) i : M) : M)
have intro₁ : Eq.{u_6 + 1} (α := M) (∑ j : ι, HSMul.hSMul (β := M) (e.toMatrix (⇑v : (a : ι') → M) j i) ((e : (a : ι) → M) j : M) : M)
  ((v : (a : ι') → M) i : M)
Tactic: rw [toLin_self, id_apply, e.sum_toMatrix_smul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : Finite ι
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
v : Basis ι' R M
i : ι'
val : Fintype ι
intro :
  Eq.{u_6 + 1} (α := M)
    (∑ j : ι, HSMul.hSMul (β := M) (e.toMatrix (⇑v : (a : ι') → M) j i) ((e : (a : ι) → M) j : M) : M)
    ((LinearMap.id : (a : M) → M) ((v : (a : ι') → M) i : M) : M)
intro₁ :
  Eq.{u_6 + 1} (α := M)
    (∑ j : ι, HSMul.hSMul (β := M) (e.toMatrix (⇑v : (a : ι') → M) j i) ((e : (a : ι) → M) j : M) : M)
    ((v : (a : ι') → M) i : M)
⊢ Eq.{u_6 + 1} (α := M)
    ((((toLin v e : (a : Matrix ι ι' R) → M →ₗ[R] M) (e.toMatrix (⇑v : (a : ι') → M)) : M →ₗ[R] M) : (a : M) → M)
        ((v : (a : ι') → M) i : M) :
      M)
    ((LinearMap.id : (a : M) → M) ((v : (a : ι') → M) i : M) : M)
have intro₂ : Eq.{u_6 + 1} (α := M) ((v : (a : ι') → M) i : M) ((v : (a : ι') → M) i : M)
Tactic: rw [toLin_self, id_apply, e.sum_toMatrix_smul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v_1 : ι' → M
i : ι
j : ι'
inst_6 : Fintype ι
e : Basis ι R M
v w : ι → M
⊢ e.toMatrix (v + w) = e.toMatrix v + e.toMatrix w
have a : ∀ (i j : ι), e.toMatrix (v + w) i j = (e.toMatrix v + e.toMatrix w) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v_1 : ι' → M
i_1 : ι
j_1 : ι'
inst_6 : Fintype ι
e : Basis ι R M
v w : ι → M
i j : ι
⊢ e.toMatrix (v + w) i j = (e.toMatrix v + e.toMatrix w) i j
have a : (HAdd.hAdd (α := ι →₀ R) (β := ι →₀ R) ((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R)
        ((e.repr : (a : M) → ι →₀ R) (w j) : ι →₀ R) :
      (a : ι) → R)
    i =
  e.toMatrix v i j + e.toMatrix w i j
Tactic: rw [Matrix.add_apply, e.toMatrix_apply, Pi.add_apply, map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v_1 : ι' → M
i : ι
j : ι'
inst_6 : Fintype ι
e : Basis ι R M
c : R
v : ι → M
⊢ e.toMatrix (c • v) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (e.toMatrix v)
have a : ∀ (i j : ι), e.toMatrix (c • v) i j = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (e.toMatrix v) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v_1 : ι' → M
i_1 : ι
j_1 : ι'
inst_6 : Fintype ι
e : Basis ι R M
c : R
v : ι → M
i j : ι
⊢ e.toMatrix (c • v) i j = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (e.toMatrix v) i j
have a : (HSMul.hSMul (β := ι →₀ R) c ((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) i =
  HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (e.toMatrix v) i j
Tactic: rw [e.toMatrix_apply, Pi.smul_apply, map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v_1 : ι' → M
i : ι
j : ι'
inst_6 : Fintype ι
e : Basis ι R M
v : ι → M
⊢ (fun (m : Matrix ι ι R) (j : ι) ↦ (∑ i : ι, HSMul.hSMul (β := M) (m i j) ((e : (a : ι) → M) i : M) : M))
      (e.toMatrix v) =
    v
have h : ∀ (j : ι),
  (fun (m : Matrix ι ι R) (j : ι) ↦ (∑ i : ι, HSMul.hSMul (β := M) (m i j) ((e : (a : ι) → M) i : M) : M))
      (e.toMatrix v) j =
    v j
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst_6 : Fintype ι
e : Basis ι R M
m : Matrix ι ι R
⊢ e.toMatrix
      ((fun (m : Matrix ι ι R) (j : ι) ↦ (∑ i : ι, HSMul.hSMul (β := M) (m i j) ((e : (a : ι) → M) i : M) : M)) m) =
    m
have a : ∀ (k l : ι),
  e.toMatrix
      ((fun (m : Matrix ι ι R) (j : ι) ↦ (∑ i : ι, HSMul.hSMul (β := M) (m i j) ((e : (a : ι) → M) i : M) : M)) m) k l =
    m k l
Tactic: ext k l
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : Fintype ι
inst_4 : DecidableEq ι
S : Type u_9
inst_5 : CommRing S
inst_6 : Nontrivial S
inst_7 : Algebra R₂ S
inst_8 : Module S M₂
inst_9 : IsScalarTower R₂ S M₂
inst_10 : IsDomain R₂
inst_11 : IsTorsionFree R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range.{u_8, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M₂)))
⊢ Eq (α := Matrix ι ι S)
    ((RingHom.mapMatrix (algebraMap R₂ S) : (a : Matrix ι ι R₂) → Matrix ι ι S) (toMatrix (restrictScalars R₂ b) v) :
      Matrix ι ι S)
    (b.toMatrix fun (i : ι) ↦ (↑(v i) : M₂) : Matrix ι ι S)
have a : ∀ (i j : ι),
  (RingHom.mapMatrix (algebraMap R₂ S) : (a : Matrix ι ι R₂) → Matrix ι ι S) (toMatrix (restrictScalars R₂ b) v) i j =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : Fintype ι
inst_4 : DecidableEq ι
S : Type u_9
inst_5 : CommRing S
inst_6 : Nontrivial S
inst_7 : Algebra R₂ S
inst_8 : Module S M₂
inst_9 : IsScalarTower R₂ S M₂
inst_10 : IsDomain R₂
inst_11 : IsTorsionFree R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range.{u_8, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M₂)))
i j : ι
⊢ (RingHom.mapMatrix (algebraMap R₂ S) : (a : Matrix ι ι R₂) → Matrix ι ι S) (toMatrix (restrictScalars R₂ b) v) i j =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
have a : (toMatrix (restrictScalars R₂ b) v).map (⇑(algebraMap R₂ S) : (a : R₂) → S) i j =
  b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
Tactic: rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
    Basis.restrictScalars_repr_apply, Basis.toMatrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : Fintype ι
inst_4 : DecidableEq ι
S : Type u_9
inst_5 : CommRing S
inst_6 : Nontrivial S
inst_7 : Algebra R₂ S
inst_8 : Module S M₂
inst_9 : IsScalarTower R₂ S M₂
inst_10 : IsDomain R₂
inst_11 : IsTorsionFree R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range.{u_8, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M₂)))
i j : ι
a :
  (toMatrix (restrictScalars R₂ b) v).map (⇑(algebraMap R₂ S) : (a : R₂) → S) i j =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
⊢ (RingHom.mapMatrix (algebraMap R₂ S) : (a : Matrix ι ι R₂) → Matrix ι ι S) (toMatrix (restrictScalars R₂ b) v) i j =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
have a₁ : (algebraMap R₂ S : (a : R₂) → S) (toMatrix (restrictScalars R₂ b) v i j) = b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
Tactic: rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
    Basis.restrictScalars_repr_apply, Basis.toMatrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : Fintype ι
inst_4 : DecidableEq ι
S : Type u_9
inst_5 : CommRing S
inst_6 : Nontrivial S
inst_7 : Algebra R₂ S
inst_8 : Module S M₂
inst_9 : IsScalarTower R₂ S M₂
inst_10 : IsDomain R₂
inst_11 : IsTorsionFree R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range.{u_8, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M₂)))
i j : ι
a :
  (toMatrix (restrictScalars R₂ b) v).map (⇑(algebraMap R₂ S) : (a : R₂) → S) i j =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
a₁ :
  (algebraMap R₂ S : (a : R₂) → S) (toMatrix (restrictScalars R₂ b) v i j) =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
⊢ (RingHom.mapMatrix (algebraMap R₂ S) : (a : Matrix ι ι R₂) → Matrix ι ι S) (toMatrix (restrictScalars R₂ b) v) i j =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
have a₂ : (algebraMap R₂ S : (a : R₂) → S)
    ((((repr (restrictScalars R₂ b) : (a : ↥(span R₂ (Set.range (⇑b : (a : ι) → M₂)))) → ι →₀ R₂) (v j) : ι →₀ R₂) :
          (a : ι) → R₂)
        i :
      R₂) =
  b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
Tactic: rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
    Basis.restrictScalars_repr_apply, Basis.toMatrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : Fintype ι
inst_4 : DecidableEq ι
S : Type u_9
inst_5 : CommRing S
inst_6 : Nontrivial S
inst_7 : Algebra R₂ S
inst_8 : Module S M₂
inst_9 : IsScalarTower R₂ S M₂
inst_10 : IsDomain R₂
inst_11 : IsTorsionFree R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range.{u_8, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M₂)))
i j : ι
a :
  (toMatrix (restrictScalars R₂ b) v).map (⇑(algebraMap R₂ S) : (a : R₂) → S) i j =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
a₁ :
  (algebraMap R₂ S : (a : R₂) → S) (toMatrix (restrictScalars R₂ b) v i j) =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
a₂ :
  (algebraMap R₂ S : (a : R₂) → S)
      ((((repr (restrictScalars R₂ b) : (a : ↥(span R₂ (Set.range (⇑b : (a : ι) → M₂)))) → ι →₀ R₂) (v j) : ι →₀ R₂) :
            (a : ι) → R₂)
          i :
        R₂) =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
⊢ (RingHom.mapMatrix (algebraMap R₂ S) : (a : Matrix ι ι R₂) → Matrix ι ι S) (toMatrix (restrictScalars R₂ b) v) i j =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
have a₃ : (((b.repr : (a : M₂) → ι →₀ S) (↑(v j) : M₂) : ι →₀ S) : (a : ι) → S) i = b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
Tactic: rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
    Basis.restrictScalars_repr_apply, Basis.toMatrix_apply]