mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0 ∧
    (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1 ∧
      (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0 ∧ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
M : Matrix m n α
N : Matrix n l α
⊢ a • M * N = a • (M * N)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
i : m
j : n
a b : α
⊢ single i j (a + b) = single i j a + single i j b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
this : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ i ∈ s, I ≤ f i
⊢ ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : SMulCommClass R α α
M : Matrix m n α
a : R
N : Matrix n l α
⊢ M * a • N = a • (M * N)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝¹ : DecidableEq n
inst✝ : NegZeroClass α
i j : n
b : α
x y : n
⊢ of (-fun i' j' ↦ if i = i' ∧ j = j' then b else 0) x y = single i j (-b) x y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
M : Matrix m n α
⊢ M * 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
M : Matrix m n α
⊢ 0 * M = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
L : Matrix m n α
M N : Matrix n o α
⊢ L * (M + N) = L * M + L * N

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
L M : Matrix l m α
N : Matrix m n α
⊢ (L + M) * N = L * N + M * N

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
ι : Type u_3
inst✝ : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
⊢ ⋃ i ∈ s, ↑(f i) = ⋃ i ∈ t, ↑(f i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d : n → α
M : Matrix m n α
i : m
j : n
⊢ (M * diagonal d) i j = M i j * d j

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
⊢ diagonal d₁ * diagonal d₂ = diagonal fun i ↦ d₁ i * d₂ i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
α : Type u_10
inst✝² : NonUnitalNonAssocCommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
⊢ diagonal d₁ * diagonal d₂ = diagonal d₂ * diagonal d₁

Tactic:
diagonal_mul_diagonal,

Goal state after:
n : Type u_3
α : Type u_10
inst✝² : NonUnitalNonAssocCommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
⊢ (diagonal fun i ↦ d₁ i * d₂ i) = diagonal fun i ↦ d₂ i * d₁ i
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
⊢ single i j c *ᵥ x = Function.update 0 i (c * x j)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
α : Type u_10
inst✝² : NonUnitalNonAssocCommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
⊢ Commute (diagonal d₁) (diagonal d₂)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
a : α
⊢ a • M = (diagonal fun x ↦ a) * M

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
⊢ MulOpposite.op a • M = M * diagonal fun x ↦ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring α
i j : n
b : α
w : n → α
⊢ single i j b *ᵥ w = (b * w j) • Pi.single i 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
β : Type w
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : Fintype n
L : Matrix m n α
M : Matrix n o α
inst✝² : NonUnitalNonAssocSemiring β
F : Type u_10
inst✝¹ : FunLike F α β
inst✝ : NonUnitalRingHomClass F α β
f : F
⊢ (L * M).map ⇑f = L.map ⇑f * M.map ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
ι : Type u_3
inst✝ : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
⊢ ↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
⊢ 1 * M = M

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
⊢ M * 1 = M

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq m
a : α
⊢ a • 1 = diagonal fun x ↦ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq m
a : α
⊢ MulOpposite.op a • 1 = diagonal fun x ↦ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
L : Matrix l m α
M : Matrix m n α
N : Matrix n o α
⊢ L * M * N = L * (M * N)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
⊢ ∑ i, single i i (f i) = diagonal f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
⊢ -M * N = -(M * N)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
⊢ M * -N = -(M * N)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
⊢ M * -N = -(M * N)

Tactic:
by
  ext
  apply dotProduct_neg

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M M' : Matrix m n α
N : Matrix n o α
⊢ (M - M') * N = M * N - M' * N

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
hp : ∀ I ∈ S, I ≠ a → I ≠ b → I.IsPrime
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ ↑M ⊆ ⋃ I ∈ S, ↑I ↔ M ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
⊢ 0 * x + i ^ 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : m → n → α
⊢ ∑ i, ∑ j, single i j (x i j) = of x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N N' : Matrix n o α
⊢ M * (N - N') = M * N - M * N'

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
i : m
j : n
⊢ single i j 1 = vecMulVec (Pi.single i 1) (Pi.single j 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
α : Type v
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
k : ℕ
⊢ ∀ (i j : n), 0 ≤ (A ^ k) i j

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
⊢ a • M = M * diagonal fun x ↦ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R✝ : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
R : Type u_10
inst✝¹ : NonAssocSemiring R
inst✝ : IsStablyFiniteRing R
f : R →* Matrix (Fin 1) (Fin 1) R := { toFun := fun r ↦ diagonal fun x ↦ r, map_one' := ⋯, map_mul' := ⋯ }
x✝¹ x✝ : R
eq : f x✝¹ = f x✝
⊢ x✝¹ = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : Mul α
inst✝¹ : Zero α
inst✝ : NoZeroDivisors α
a b : n → α
ha : a ≠ 0
hb : b ≠ 0
⊢ vecMulVec a b ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
⊢ P M

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : MulZeroClass α
inst✝ : NoZeroDivisors α
a b : n → α
⊢ vecMulVec a b = 0 ↔ a = 0 ∨ b = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
⊢ 0 *ᵥ v = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
x y : Matrix m n α
⊢ (x + y) *ᵥ v = x *ᵥ v + y *ᵥ v

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : AddCommMonoid α
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
⊢ P 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ v ⬝ᵥ A *ᵥ w = v ᵥ* A ⬝ᵥ w

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
y i : R
hmem : i ∈ I
hi : y * x + i = 1
⊢ ∃ y, y * x + i ^ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
y i : R
hmem : i ∈ I
hi : y * x + i = 1
⊢ ∃ y, y * x + i ^ n = 1

Tactic:
by
    induction n with
    | zero => exact ⟨0, by simp⟩
    | succ n ih =>
      obtain ⟨z, hz⟩ := ih
      refine ⟨z * i + y, ?_⟩
      trans z * i * x + i * i ^ n + y * x
      · ring
      · rw [mul_comm z i, mul_assoc, ← mul_add, hz, add_comm]
        simpa

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ v ⬝ᵥ A *ᵥ w = ∑ j, ∑ i, v i * A i j * w j

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
⊢ ∃ y, ∃ i ∈ I ^ n, y * x + i = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
⊢ A *ᵥ 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
⊢ 0 ᵥ* A = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
⊢ 0 *ᵥ v = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
α : Type u_7
β : Type u_8
inst✝¹¹ : DecidableEq m
inst✝¹⁰ : DecidableEq n
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module R α
inst✝² : Module R β
inst✝¹ : Module S β
inst✝ : SMulCommClass R S β
f : m → n → α →ₗ[R] β
M : Matrix m n α
⊢ ((liftLinear S) f) M = ∑ i, ∑ j, (f i j) (M i j)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
v : m → α
⊢ v ᵥ* 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
α : Type u_7
β : Type u_8
inst✝¹¹ : DecidableEq m
inst✝¹⁰ : DecidableEq n
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module R α
inst✝² : Module R β
inst✝¹ : Module S β
inst✝ : SMulCommClass R S β
f : m → n → α →ₗ[R] β
i : m
j : n
a : α
⊢ ((liftLinear S) f) (single i j a) = (f i j) a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x y : n → α
⊢ A *ᵥ (x + y) = A *ᵥ x + A *ᵥ y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ∨ b ∈ I ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A B : Matrix m n α
x : n → α
⊢ (A + B) *ᵥ x = A *ᵥ x + B *ᵥ x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A B : Matrix m n α
x : m → α
⊢ x ᵥ* (A + B) = x ᵥ* A + x ᵥ* B

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
h : I = ⊤
⊢ ⊤ = I * ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
⊢ (single i i c).diag = Pi.single i c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x y : m → α
⊢ (x + y) ᵥ* A = x ᵥ* A + y ᵥ* A

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
b : n
M : Matrix m n α
⊢ (single i j c * M) i b = c * M j b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : m
j : n
a : l
M : Matrix l m α
⊢ (M * single i j c) a j = M a i * c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DistribSMul R α
inst✝ : SMulCommClass R α α
M : Matrix m n α
b : R
v : n → α
⊢ M *ᵥ b • v = b • M *ᵥ v

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
f : ι →₀ ↥I
⊢ (finsuppTotal ι M I v) f = f.sum fun i x ↦ ↑x • v i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
a : l
b : n
h : a ≠ i
M : Matrix m n α
⊢ (single i j c * M) a b = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : m
j : n
a : l
b : n
hbj : b ≠ j
M : Matrix l m α
⊢ (M * single i j c) a b = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DistribSMul R α
inst✝ : IsScalarTower R α α
b : R
M : Matrix m n α
v : n → α
⊢ (b • M) *ᵥ v = b • M *ᵥ v

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
v : ι → M
inst✝ : Fintype ι
f : ι →₀ ↥I
⊢ (finsuppTotal ι M I v) f = ∑ i, ↑(f i) • v i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype m
inst✝¹ : DistribSMul R α
inst✝ : IsScalarTower R α α
b : R
v : m → α
M : Matrix m n α
⊢ (b • v) ᵥ* M = b • v ᵥ* M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (if h : 0 ∈ I then ⟨0, h⟩ else 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype m
inst✝¹ : DistribSMul R α
inst✝ : SMulCommClass R α α
v : m → α
b : R
M : Matrix m n α
⊢ v ᵥ* (b • M) = b • v ᵥ* M

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonAssocSemiring R
M : Matrix m n R
j : n
⊢ M *ᵥ Pi.single j 1 = M.col j

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring R
i : m
M : Matrix m n R
⊢ Pi.single i 1 ᵥ* M = M.row i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
⊢ diagonal v *ᵥ Pi.single j x = Pi.single j (v j * x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
⊢ (finsuppTotal ι M I v).range = I • Submodule.span R (Set.range v)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
r : R
⊢ Associates.mk (Ideal.span {r}) ≠ 0 ↔ r ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
⊢ Pi.single j x ᵥ* diagonal v = Pi.single j (x * v j)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype m
v : m → α
M : Matrix m n α
N : Matrix n o α
⊢ v ᵥ* M ᵥ* N = v ᵥ* (M * N)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
⊢ M *ᵥ N *ᵥ v = (M * N) *ᵥ v

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
⊢ span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ (A * B * C) i j = A i ⬝ᵥ B *ᵥ Cᵀ j

Tactic:
by

Goal state after: