mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
⊢ (toLinAlgEquiv v₁) ((toMatrixAlgEquiv v₁) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
y z : OreLocalization S R
x : OreLocalization S X
⊢ (y + z) • x = y • x + z • x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
⊢ (toMatrixAlgEquiv v₁) ((toLinAlgEquiv v₁) M) = M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝⁸ : Semiring R
S : Submonoid R
inst✝⁷ : OreSet S
X : Type u_2
inst✝⁶ : AddCommMonoid X
inst✝⁵ : Module R X
R₀ : Type ?u.16
inst✝⁴ : Semiring R₀
inst✝³ : Module R₀ X
inst✝² : Module R₀ R
inst✝¹ : IsScalarTower R₀ R X
inst✝ : IsScalarTower R₀ R R
r s : R₀
x : OreLocalization S X
⊢ (r + s) • x = r • x + s • x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
i j : n
⊢ (toMatrixAlgEquiv v₁) f i j = (v₁.repr (f (v₁ j))) i

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝⁸ : Semiring R
S : Submonoid R
inst✝⁷ : OreSet S
X : Type u_2
inst✝⁶ : AddCommMonoid X
inst✝⁵ : Module R X
R₀ : Type ?u.16
inst✝⁴ : Semiring R₀
inst✝³ : Module R₀ X
inst✝² : Module R₀ R
inst✝¹ : IsScalarTower R₀ R X
inst✝ : IsScalarTower R₀ R R
x : OreLocalization S X
⊢ 0 • x = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
n : ℕ
x : OreLocalization S X
⊢ n • x = n • x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
⊢ (↑numeratorHom).toFun 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
⊢ (toMatrixAlgEquiv v₁) id = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
⊢ (toLinAlgEquiv v₁) 1 = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
S : Submonoid R
inst✝⁴ : OreSet S
X : Type u_2
inst✝³ : AddCommMonoid X
inst✝² : Module R X
R₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
x : OreLocalization S R
⊢ (numeratorRingHom.comp (algebraMap R₀ R)) r * x = x * (numeratorRingHom.comp (algebraMap R₀ R)) r

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
⊢ ∃ y ∈ M,
    ∃ a,
      a • y ∈ N ∧
        ∃ M' ≤ M,
          ∃ N' ≤ N,
            N' ≤ M' ∧
              (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧
                (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧
                  ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'),
                    ∃ bN,
                      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'),
                        ∃ (hnm : n' + 1 ≤ m' + 1),
                          ∃ bM,
                            ∀ (as : Fin n' → R),
                              (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
                                ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
S : Submonoid R
inst✝⁴ : OreSet S
X : Type u_2
inst✝³ : AddCommMonoid X
inst✝² : Module R X
R₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
x : OreLocalization S R
⊢ r • x = (numeratorRingHom.comp (algebraMap R₀ R)) r * x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
M₁ : Type u_5
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R M₁
v₁ : Basis n R M₁
inst✝ : DecidableEq M₁
f : M₁ →ₗ[R] M₁
k i : n
⊢ (toMatrixAlgEquiv v₁.reindexRange) f ⟨v₁ k, ⋯⟩ ⟨v₁ i, ⋯⟩ = (toMatrixAlgEquiv v₁) f k i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
⊢ (toMatrixAlgEquiv v₁) (f ∘ₗ g) = (toMatrixAlgEquiv v₁) f * (toMatrixAlgEquiv v₁) g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
⊢ (↑(universalMulHom (↑f) fS hf)).toFun 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
⊢ (toMatrixAlgEquiv v₁) (f * g) = (toMatrixAlgEquiv v₁) f * (toMatrixAlgEquiv v₁) g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
A B : Matrix n n R
⊢ (toLinAlgEquiv v₁) (A * B) = (toLinAlgEquiv v₁) A ∘ₗ (toLinAlgEquiv v₁) B

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b c d : R
x : R × R
⊢ ((toLin (Basis.finTwoProd R) (Basis.finTwoProd R)) !![a, b; c, d]) x = (a * x.1 + b * x.2, c * x.1 + d * x.2)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
x : R
⊢ (toMatrix v₁ v₁) (DistribSMul.toLinearMap R M₁ x) = Matrix.diagonal fun x_1 ↦ x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
⊢ (toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) = fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x : S
i j : m
⊢ (toMatrix b b) ((lmul R S) x) i j = (b.repr (x * b j)) i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
⊢ (toMatrix b b) ((lmul R S) 1) = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
N : Submodule R M
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x y : S
⊢ (toMatrix b b) ((lmul R S) (x * y)) = (toMatrix b b) ((lmul R S) x) * (toMatrix b b) ((lmul R S) y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
⊢ (toMatrix b b) ((lmul R S) 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R ↥⊥
e : Fin n ≃ Fin 0 := b'.indexEquiv (Basis.empty ↥⊥)
⊢ n = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x y : S
⊢ (toMatrix b b) ((lmul R S) (x + y)) = (toMatrix b b) ((lmul R S) x) + (toMatrix b b) ((lmul R S) y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
⊢ basisOfPid b ⊥ = ⟨0, Basis.empty ↥⊥⟩

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
r : R
⊢ (toMatrix b b) ((lmul R S) ((algebraMap R S) r)) = (algebraMap R (Matrix m m R)) r

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
x y : OreLocalization S R
⊢ (↑(universalMulHom (↑f) fS hf)).toFun (x + y) =
    (↑(universalMulHom (↑f) fS hf)).toFun x + (↑(universalMulHom (↑f) fS hf)).toFun y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r : R
⊢ (universalHom f fS hf) (numeratorHom r) = f r

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x : S
i j : m
⊢ (leftMulMatrix b) x i j = (b.repr (x * b j)) i

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommGroup X
inst✝ : Module R X
n : ℤ
x : OreLocalization S X
⊢ n • x = n • x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x x' : S
h : (leftMulMatrix b) x = (leftMulMatrix b) x'
⊢ ((lmul R S) x) 1 = ((lmul R S) x') 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
h : numeratorHom r₁ = numeratorHom r₂
⊢ r₁ = r₂

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring S
inst✝⁶ : Algebra R S
m : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
b : Basis m R S
G : Type u_4
inst✝³ : Group G
inst✝² : DistribMulAction G S
inst✝¹ : SMulCommClass G R S
inst✝ : SMulCommClass G S S
g : G
x : S
⊢ (leftMulMatrix (g • b)) x = (leftMulMatrix b) x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq m
A : Type u_4
M : Type u_5
n : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : CommSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
bA : Basis m R A
bM : Basis n A M
f : M →ₗ[A] M
⊢ (toMatrix (bA.smulTower' bM) (bA.smulTower' bM)) (↑R f) =
    (Matrix.comp n n m m R) (((toMatrix bM bM) f).map ⇑(leftMulMatrix bA))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : T
ik jk : m × n
⊢ (leftMulMatrix (b.smulTower c)) x ik jk = (leftMulMatrix b) ((leftMulMatrix c) x ik.2 jk.2) ik.1 jk.1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this.choose
indepI : LinearIndependent (ι := ↑I) R (s ∘ fun x ↦ ↑x)
hI : ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
N : Submodule R M := span R (range (s ∘ fun x ↦ ↑x))
_sI : ↑I → ↥N := fun i ↦ ⟨s ↑i, ⋯⟩
sI_basis : Basis (↑I) R ↥N := Basis.span indepI
⊢ ∀ (i : ι), ∃ a, a ≠ 0 ∧ a • s i ∈ N

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
⊢ (leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) = blockDiagonal fun x_1 ↦ (leftMulMatrix b) x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this.choose
indepI : LinearIndependent (ι := ↑I) R (s ∘ fun x ↦ ↑x)
hI : ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
N : Submodule R M := span R (range (s ∘ fun x ↦ ↑x))
_sI : ↑I → ↥N := fun i ↦ ⟨s ↑i, ⋯⟩
sI_basis : Basis (↑I) R ↥N := Basis.span indepI
a : ι → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i, a i
⊢ A ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i j : m
k : n
⊢ (leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k) = (leftMulMatrix b) x i j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i j : m
k k' : n
h : k ≠ k'
⊢ (leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k') = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
ι₁ : Type u_6
ι₂ : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Fintype ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
ij : ι₂ × ι₁
⊢ (b₁.linearMap b₂) ij = (toLin b₁ b₂) ((stdBasis R ι₂ ι₁) ij)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this✝¹ : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this✝¹.choose
indepI : LinearIndependent (ι := ↑I) R (s ∘ fun x ↦ ↑x)
hI : ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
N : Submodule R M := span R (range (s ∘ fun x ↦ ↑x))
_sI : ↑I → ↥N := fun i ↦ ⟨s ↑i, ⋯⟩
sI_basis : Basis (↑I) R ↥N := Basis.span indepI
a : ι → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i, a i
hA : A ≠ 0
φ : M →ₗ[R] M := (LinearMap.lsmul R M) A
this✝ : φ.ker = ⊥
ψ : M ≃ₗ[R] ↥φ.range := LinearEquiv.ofInjective φ ⋯
this : ∀ (i : ι), φ (s i) ∈ N
⊢ φ.range ≤ N

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
ι₁ : Type u_6
ι₂ : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Fintype ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
ij : ι₂ × ι₁
k : ι₁
⊢ ((b₁.linearMap b₂) ij) (b₁ k) = if ij.2 = k then b₂ ij.1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_5
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
R : Type u_8
M : Type u_9
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : Basis ι R M
a : ι → R
s : End R M
hs : ∀ (k : ι), s (b k) = a k • b k
i j : ι
⊢ ⁅s, b.end (i, j)⁆ = (a i - a j) • b.end (i, j)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
f : End A (ι → M)
i j : ι
x y : M
⊢ f (Pi.single j (x + y)) i = f (Pi.single j x) i + f (Pi.single j y) i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
f : End A (ι → M)
i j : ι
x : A
y : M
⊢ f (Pi.single j (x • y)) i = (RingHom.id A) x • f (Pi.single j y) i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this✝ : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this✝.choose
indepI : LinearIndependent (ι := ↑I) R (s ∘ fun x ↦ ↑x)
hI : ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
N : Submodule R M := span R (range (s ∘ fun x ↦ ↑x))
_sI : ↑I → ↥N := fun i ↦ ⟨s ↑i, ⋯⟩
sI_basis : Basis (↑I) R ↥N := Basis.span indepI
a : ι → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i, a i
hA : A ≠ 0
φ : M →ₗ[R] M := (LinearMap.lsmul R M) A
this : φ.ker = ⊥
ψ : M ≃ₗ[R] ↥φ.range := LinearEquiv.ofInjective φ ⋯
i : ι
⊢ (∏ j ∈ {i}ᶜ, a j) • a i • s i = (∏ j, a j) • s i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this✝ : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this✝.choose
indepI : LinearIndependent (ι := ↑I) R (s ∘ fun x ↦ ↑x)
hI : ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
N : Submodule R M := span R (range (s ∘ fun x ↦ ↑x))
_sI : ↑I → ↥N := fun i ↦ ⟨s ↑i, ⋯⟩
sI_basis : Basis (↑I) R ↥N := Basis.span indepI
a : ι → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i, a i
hA : A ≠ 0
φ : M →ₗ[R] M := (LinearMap.lsmul R M) A
this : φ.ker = ⊥
ψ : M ≃ₗ[R] ↥φ.range := LinearEquiv.ofInjective φ ⋯
⊢ φ.range ≤ N

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : Matrix ι ι (End A M)
⊢ ∀ (x y : ι → M), (fun i ↦ ∑ j, (m i j) ((x + y) j)) = (fun i ↦ ∑ j, (m i j) (x j)) + fun i ↦ ∑ j, (m i j) (y j)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
⊢ (n : ℕ) × Basis (Fin n) R M

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Finite ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
⊢ Free R M

Tactic:
by

Goal state after: