mathlib-initiative/mathlib-tactics huggingface dataset:
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:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
i✝ : m
j✝ : n
⊢ (a • M) i✝ j✝ = (M * diagonal fun x ↦ a) i✝ j✝
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:
ext

Goal state after:
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✝ : m
⊢ (0 *ᵥ v) x✝ = 0 x✝
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:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x✝ : m
⊢ (A *ᵥ 0) x✝ = 0 x✝
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:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x✝ : n
⊢ (0 ᵥ* A) x✝ = 0 x✝
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:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
x✝ : m
⊢ (0 *ᵥ v) x✝ = 0 x✝
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:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
v : m → α
x✝ : n
⊢ (v ᵥ* 0) x✝ = 0 x✝
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:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x y : n → α
x✝ : m
⊢ (A *ᵥ (x + y)) x✝ = (A *ᵥ x + A *ᵥ y) x✝
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:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A B : Matrix m n α
x : n → α
x✝ : m
⊢ ((A + B) *ᵥ x) x✝ = (A *ᵥ x + B *ᵥ x) x✝
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:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A B : Matrix m n α
x : m → α
x✝ : n
⊢ (x ᵥ* (A + B)) x✝ = (x ᵥ* A + x ᵥ* B) x✝
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:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x y : m → α
x✝ : n
⊢ ((x + y) ᵥ* A) x✝ = (x ᵥ* A + y ᵥ* A) x✝
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:
ext

Goal state after:
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 → α
x✝ : m
⊢ (M *ᵥ b • v) x✝ = (b • M *ᵥ v) x✝
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:
ext

Goal state after:
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 → α
x✝ : m
⊢ ((b • M) *ᵥ v) x✝ = (b • M *ᵥ v) x✝
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:
ext

Goal state after:
ι : 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
x✝ : M
⊢ x✝ ∈ (finsuppTotal ι M I v).range ↔ x✝ ∈ I • Submodule.span R (Set.range v)
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:
ext

Goal state after:
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 α
x✝ : n
⊢ ((b • v) ᵥ* M) x✝ = (b • v ᵥ* M) x✝
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:
ext

Goal state after:
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 α
x✝ : n
⊢ (v ᵥ* (b • M)) x✝ = (b • v ᵥ* M) x✝
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:
ext

Goal state after:
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
x✝ : m
⊢ (M *ᵥ Pi.single j 1) x✝ = M.col j x✝
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:
ext

Goal state after:
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
x✝ : n
⊢ (Pi.single i 1 ᵥ* M) x✝ = M.row i x✝
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:
ext

Goal state after:
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 α
x✝ : o
⊢ (v ᵥ* M ᵥ* N) x✝ = (v ᵥ* (M * N)) x✝
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:
ext

Goal state after:
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 α
x✝ : m
⊢ (M *ᵥ N *ᵥ v) x✝ = ((M * N) *ᵥ v) x✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
M : Matrix l m α
x : m → α
y : n → α
⊢ M * vecMulVec x y = vecMulVec (M *ᵥ x) y

Tactic:
ext

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
M : Matrix l m α
x : m → α
y : n → α
i✝ : l
j✝ : n
⊢ (M * vecMulVec x y) i✝ j✝ = vecMulVec (M *ᵥ x) y i✝ j✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
x : l → α
y : m → α
M : Matrix m n α
⊢ vecMulVec x y * M = vecMulVec x (y ᵥ* M)

Tactic:
ext

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
x : l → α
y : m → α
M : Matrix m n α
i✝ : l
j✝ : n
⊢ (vecMulVec x y * M) i✝ j✝ = vecMulVec x (y ᵥ* M) i✝ j✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Nonempty l
inst✝ : Fintype m
A : Matrix m n α
⊢ (Function.Injective fun B ↦ B * A) ↔ Function.Injective fun v ↦ v ᵥ* A

Tactic:
refine ⟨fun ha v w hvw => ?_, fun ha B C hBC => ext_row fun i => ha congr(($hBC).row i)⟩

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Nonempty l
inst✝ : Fintype m
A : Matrix m n α
ha : Function.Injective fun B ↦ B * A
v w : m → α
hvw : (fun v ↦ v ᵥ* A) v = (fun v ↦ v ᵥ* A) w
⊢ v = w
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
⊢ A *ᵥ 1 = ∑ j, Aᵀ j

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x✝ : m
⊢ (A *ᵥ 1) x✝ = (∑ j, Aᵀ j) x✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
⊢ 1 ᵥ* A = ∑ i, A i

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x✝ : n
⊢ (1 ᵥ* A) x✝ = (∑ i, A i) x✝
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
b : ι → S
ι' : Type u_6
c : ι' → A
hb : LinearIndependent R b
hc : LinearIndependent S c
⊢ LinearIndependent R fun p ↦ b p.2 • c p.1

Tactic:
LinearIndependent,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
b : ι → S
ι' : Type u_6
c : ι' → A
hb : LinearIndependent R b
hc : LinearIndependent S c
⊢ Function.Injective ⇑(linearCombination R fun p ↦ b p.2 • c p.1)
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
A B : Matrix m n α
h : A.mulVec = B.mulVec
i : m
j : n
⊢ A i j = B i j

Tactic:
classical
  simpa using congrFun₂ h (Pi.single j 1) i

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
⊢ 1 *ᵥ v = v

Tactic:
ext

Goal state after:
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
x✝ : m
⊢ (1 *ᵥ v) x✝ = v x✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
⊢ v ᵥ* 1 = v

Tactic:
ext

Goal state after:
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
x✝ : m
⊢ (v ᵥ* 1) x✝ = v x✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x : α
v : m → α
⊢ (diagonal fun x_1 ↦ x) *ᵥ v = x • v

Tactic:
ext

Goal state after:
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x : α
v : m → α
x✝ : m
⊢ ((diagonal fun x_1 ↦ x) *ᵥ v) x✝ = (x • v) x✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x : α
v : m → α
⊢ (v ᵥ* diagonal fun x_1 ↦ x) = MulOpposite.op x • v

Tactic:
ext

Goal state after:
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x : α
v : m → α
x✝ : m
⊢ (v ᵥ* diagonal fun x_1 ↦ x) x✝ = (MulOpposite.op x • v) x✝
Module: Mathlib.Data.Matrix.Mul

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

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
x✝ : n
⊢ (-v ᵥ* A) x✝ = (-(v ᵥ* A)) x✝
Module: Mathlib.Data.Matrix.Mul

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

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
x✝ : n
⊢ (v ᵥ* -A) x✝ = (-(v ᵥ* A)) x✝
Module: Mathlib.Data.Matrix.Mul

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

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
x✝ : m
⊢ (-A *ᵥ v) x✝ = (-(A *ᵥ v)) x✝
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f✝ f : C →ₐ[A] D
⊢ AlgHom.restrictScalars A (AlgHom.extendScalars B f) = f

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f✝ f : C →ₐ[A] D
x✝ : C
⊢ (AlgHom.restrictScalars A (AlgHom.extendScalars B f)) x✝ = f x✝
Module: Mathlib.Data.Matrix.Mul

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

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
x✝ : m
⊢ (A *ᵥ -v) x✝ = (-(A *ᵥ v)) x✝
Module: Mathlib.Data.Matrix.Mul

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

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
A : Matrix m n α
x y : n → α
x✝ : m
⊢ (A *ᵥ (x - y)) x✝ = (A *ᵥ x - A *ᵥ y) x✝
Module: Mathlib.Data.Matrix.Mul

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

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
A : Matrix m n α
x y : m → α
x✝ : n
⊢ ((x - y) ᵥ* A) x✝ = (x ᵥ* A - y ᵥ* A) x✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype m
A : Matrix m n α
x : m → α
⊢ Aᵀ *ᵥ x = x ᵥ* A

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype m
A : Matrix m n α
x : m → α
x✝ : n
⊢ (Aᵀ *ᵥ x) x✝ = (x ᵥ* A) x✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype n
A : Matrix m n α
x : n → α
⊢ x ᵥ* Aᵀ = A *ᵥ x

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype n
A : Matrix m n α
x : n → α
x✝ : m
⊢ (x ᵥ* Aᵀ) x✝ = (A *ᵥ x) x✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : AddCommMonoid α
inst✝¹ : CommMagma α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n l α
⊢ (M * N)ᵀ = Nᵀ * Mᵀ

Tactic:
ext

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : AddCommMonoid α
inst✝¹ : CommMagma α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n l α
i✝ : l
j✝ : m
⊢ (M * N)ᵀ i✝ j✝ = (Nᵀ * Mᵀ) i✝ j✝
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✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → m
e₂ : n ≃ o
⊢ M.submatrix e₁ id * N.submatrix (⇑e₂) id = M.submatrix e₁ ⇑e₂.symm * N

Tactic:
ext

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → m
e₂ : n ≃ o
i✝ : l
j✝ : p
⊢ (M.submatrix e₁ id * N.submatrix (⇑e₂) id) i✝ j✝ = (M.submatrix e₁ ⇑e₂.symm * N) i✝ j✝
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✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → p
e₂ : o ≃ n
⊢ M.submatrix id ⇑e₂ * N.submatrix id e₁ = M * N.submatrix (⇑e₂.symm) e₁

Tactic:
ext

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → p
e₂ : o ≃ n
i✝ : m
j✝ : l
⊢ (M.submatrix id ⇑e₂ * N.submatrix id e₁) i✝ j✝ = (M * N.submatrix (⇑e₂.symm) e₁) i✝ j✝
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : LinearOrder M
inst✝⁴ : CanonicallyOrderedAdd M
inst✝³ : Sub M
inst✝² : AddLeftReflectLE M
inst✝¹ : OrderedSub M
s : Finset ι
t : Finset κ
inst✝ : OrderBot M
hs : s.Nonempty
ht : t.Nonempty
f : ι → M
g : κ → M
⊢ s.sup f + t.sup g = (s ×ˢ t).sup fun ij ↦ f ij.1 + g ij.2

Tactic:
simp only [Finset.sup_add hs, Finset.add_sup ht, Finset.sup_product_left]

Goal state after:
Module: Mathlib.Order.Preorder.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : Lattice M
f g : ι →₀ M
inst✝ : DecidableEq ι
⊢ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ = (↑(f.support ∪ g.support))ᶜ

Tactic:
ext

Goal state after:
ι : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : Lattice M
f g : ι →₀ M
inst✝ : DecidableEq ι
x✝ : ι
⊢ x✝ ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ ↔ x✝ ∈ (↑(f.support ∪ g.support))ᶜ
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : ↑T
⊢ iUnionLift S f hf T hT x ∈ t ↔ ∃ i x_1, f i x_1 ∈ t ∧ inclusion ⋯ x_1 = inclusion hT x

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : ↑T
⊢ iUnionLift S f hf T hT x ∈ t → ∃ i x_1, f i x_1 ∈ t ∧ inclusion ⋯ x_1 = inclusion hT x

case mpr
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : ↑T
⊢ (∃ i x_1, f i x_1 ∈ t ∧ inclusion ⋯ x_1 = inclusion hT x) → iUnionLift S f hf T hT x ∈ t
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
this : x = inclusion ⋯ ⟨↑x, hi⟩
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = f i (ui i ⟨↑x, hi⟩)

Tactic:
conv_lhs => rw [this, hui, iUnionLift_inclusion]

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n ↦ a ^ n
⊢ ({a}.prod ^ n * f.prod fun a n ↦ a ^ n) = a ^ n * f.prod HPow.hPow

pp: case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n ↦ a ^ n
⊢ a ^ 0 = 1

Tactic:
Multiset.prod_singleton

Goal state after:
case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n ↦ a ^ n
⊢ (a ^ n * f.prod fun a n ↦ a ^ n) = a ^ n * f.prod HPow.hPow

case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n ↦ a ^ n
⊢ a ^ 0 = 1
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 → (toMultiset f).toFinset = f.support → (toMultiset (single a b + f)).toFinset = (single a b + f).support

Tactic:
intro a n f ha hn ih

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : (toMultiset f).toFinset = f.support
⊢ (toMultiset (single a n + f)).toFinset = (single a n + f).support
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
hS : iUnion S = univ
t : Set β
⊢ (fun a ↦ ⟨a, ⋯⟩) ⁻¹' inclusion ⋯ ⁻¹' ⋃ i, inclusion ⋯ '' f i ⁻¹' t = ⋃ i, Subtype.val '' f i ⁻¹' t

Tactic:
ext

Goal state after:
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
hS : iUnion S = univ
t : Set β
x✝ : α
⊢ x✝ ∈ (fun a ↦ ⟨a, ⋯⟩) ⁻¹' inclusion ⋯ ⁻¹' ⋃ i, inclusion ⋯ '' f i ⁻¹' t ↔ x✝ ∈ ⋃ i, Subtype.val '' f i ⁻¹' t