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

Goal state after:
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ * diagonal d₂) i j = diagonal (fun i ↦ d₁ i * d₂ i) i j
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:
ext i j

Goal state after:
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 : m
j : n
⊢ (∑ i, ∑ j, single i j (x i j)) i j = of x i j
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:
simp_rw [dotProduct_mulVec, dotProduct, vecMul_eq_sum, Finset.sum_apply, Pi.smul_apply,
    smul_eq_mul, Finset.sum_mul]

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✝¹ : DecidableEq n
inst✝ : Fintype n
M N : Matrix m n α
h : ∀ (i : n), M *ᵥ Pi.single i 1 = N *ᵥ Pi.single i 1
⊢ M = N

Tactic:
ext i j

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M N : Matrix m n α
h : ∀ (i : n), M *ᵥ Pi.single i 1 = N *ᵥ Pi.single i 1
i : m
j : n
⊢ M i j = N i j
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
M N : Matrix m n α
h : ∀ (i : m), Pi.single i 1 ᵥ* M = Pi.single i 1 ᵥ* N
⊢ M = N

Tactic:
ext i j

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
M N : Matrix m n α
h : ∀ (i : m), Pi.single i 1 ᵥ* M = Pi.single i 1 ᵥ* N
i : m
j : n
⊢ M i j = N i j
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
⊢ A = B

Tactic:
ext i j

Goal state after:
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
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 B : Matrix m n α
h : (fun x v ↦ v ᵥ* x) A = (fun x v ↦ v ᵥ* x) B
⊢ A = B

Tactic:
ext i j

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
A B : Matrix m n α
h : (fun x v ↦ v ᵥ* x) A = (fun x v ↦ v ᵥ* x) B
i : m
j : n
⊢ A i j = B i j
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 → α
x✝ : m
⊢ (v ᵥ* diagonal fun x_1 ↦ x) x✝ = (MulOpposite.op x • v) x✝

Tactic:
simp [vecMul_diagonal]

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✝ : Semiring α
M : Matrix n n α
⊢ M ∈ Set.range ⇑(scalar n) ↔ ∀ (i j : n), i ≠ j → Commute (single i j 1) M

Tactic:
by
  refine ⟨fun ⟨r, hr⟩ i j _ => hr ▸ Commute.symm ?_, mem_range_scalar_of_commute_single⟩
  rw [scalar_commute_iff]
  simp

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✝ : Semiring α
x✝ : Nonempty n
i : n
x : α
hx : ∀ (g : Matrix n n α), g * (scalar n) x = (scalar n) x * g
⊢ ∃ x_1, (∀ (g : α), g * x_1 = x_1 * g) ∧ (scalar n) x_1 = (scalar n) x

Tactic:
exact ⟨x, by simpa using fun r ↦ congr($(hx (single i i r)) i i)⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
⊢ lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)

Tactic:
let c := Module.Free.chooseBasis K A

Goal state after:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon x y
⊢ I.ringCon (x - y) 0

Tactic:
convert! I.ringCon.sub h (I.ringCon.refl y)

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon x y
⊢ 0 = y - y
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
ι : Type u_2
b : Basis ι R M
d1 : finrank R M = 1
this : Nontrivial R
⊢ Nonempty (Unique ι)

Tactic:
have : Module.Finite R M :=
    Module.finite_of_finrank_pos (Nat.lt_of_sub_eq_succ d1)

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
ι : Type u_2
b : Basis ι R M
d1 : finrank R M = 1
this✝ : Nontrivial R
this : Module.Finite R M
⊢ Nonempty (Unique ι)
Module: Mathlib.Algebra.Algebra.Subalgebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
U V : Subalgebra S A
H : restrictScalars R U = restrictScalars R V
x : A
⊢ x ∈ U ↔ x ∈ V

Tactic:
← mem_restrictScalars R,

Goal state after:
R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
U V : Subalgebra S A
H : restrictScalars R U = restrictScalars R V
x : A
⊢ x ∈ restrictScalars R U ↔ x ∈ V
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case refine_1
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
a : A
ha : a ∈ s
⊢ ⟨a, ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

pp: case refine_2
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
r : R
⊢ ⟨(algebraMap R A) r, ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

pp: case refine_3
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ + x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

pp: case refine_4
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ * x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

Tactic:
· exact subset_adjoin ha

Goal state after:
case refine_2
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
r : R
⊢ ⟨(algebraMap R A) r, ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

case refine_3
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ + x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

case refine_4
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ * x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ ∀ {x : A}, x ∈ T → x ∈ S ⊔ T

Tactic:
rw [← SetLike.le_def]
  exact le_sup_right

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
s : Set A
hb : b ∈ adjoin R s
h : ∀ b ∈ s, Commute a b
⊢ a ∈ centralizer R s

Tactic:
simpa only [Commute.symm_iff (a := a)] using! h

Goal state after:
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
hM : Projective R M
hN : Projective R₀ N
⊢ Projective R (M ⊗[R₀] N)

Tactic:
obtain ⟨sM, hsM⟩ := hM
  obtain ⟨sN, hsN⟩ := hN
  have : Module.Projective R (M ⊗[R₀] (N →₀ R₀)) := by
    fapply Projective.of_split (R := R) (M := ((M →₀ R) ⊗[R₀] (N →₀ R₀)))
    · exact (AlgebraTensorModule.map sM (LinearMap.id (R := R₀) (M := N →₀ R₀)))
    · exact (AlgebraTensorModule.map
        (Finsupp.linearCombination R id) (LinearMap.id (R := R₀) (M := N →₀ R₀)))
    · ext; simp [hsM _]
  fapply Projective.of_split (R := R) (M := (M ⊗[R₀] (N →₀ R₀)))
  · exact (AlgebraTensorModule.map (LinearMap.id (R := R) (M := M)) sN)
  · exact (AlgebraTensorModule.map (LinearMap.id (R := R) (M := M)) (linearCombination R₀ id))
  · ext; simp [hsN _]

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

Goal state before:
pp: case inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
hi : i ≠ i'
⊢ single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')

Tactic:
single_apply_of_row_ne hi,

Goal state after:
case inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
hi : i ≠ i'
⊢ 0 k' l' = single (i, k) (j, l) r (i', k') (j', l')
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
S : Type v
f : R → S
𝕜 : Type u_1
inst✝⁵ : Star 𝕜
inst✝⁴ : SMul 𝕜 R
inst✝³ : Star R
inst✝² : SMul 𝕜 S
inst✝¹ : Star S
inst✝ : StarModule 𝕜 S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
smul : ∀ (r : 𝕜) (x : R), f (r • x) = r • f x
r : 𝕜
x : R
⊢ f (Star.star (r • x)) = f (Star.star r • Star.star x)

Tactic:
by rw [star, smul, star_smul, smul, star]

Goal state after:
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ ⅟2 • (x + x) = x

Tactic:
smul_add,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ ⅟2 • x + ⅟2 • x = x
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
⊢ IsIdempotentElem (star a) ↔ IsIdempotentElem a

Tactic:
by
  simp [IsIdempotentElem, ← star_mul]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ = M

Tactic:
ext i j

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
i : n ⊕ o
j : l ⊕ m
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ i j = M i j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
⊢ (fromBlocks A B C D).map f = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f)

Tactic:
ext i j

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
i : n ⊕ o
j : l ⊕ m
⊢ (fromBlocks A B C D).map f i j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) i j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ (fromBlocks A B C D)ᵀ = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ

Tactic:
ext i j

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : l ⊕ m
j : n ⊕ o
⊢ (fromBlocks A B C D)ᵀ i j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ i j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
⊢ (fromBlocks A B C D).submatrix Sum.swap f = (fromBlocks C D A B).submatrix id f

Tactic:
ext i j

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
i : o ⊕ n
j : p
⊢ (fromBlocks A B C D).submatrix Sum.swap f i j = (fromBlocks C D A B).submatrix id f i j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
⊢ (fromBlocks A B C D).submatrix f Sum.swap = (fromBlocks B A D C).submatrix f id

Tactic:
ext i j

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
j : m ⊕ l
⊢ (fromBlocks A B C D).submatrix f Sum.swap i j = (fromBlocks B A D C).submatrix f id i j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ x • fromBlocks A B C D = fromBlocks (x • A) (x • B) (x • C) (x • D)

Tactic:
ext i j

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (x • fromBlocks A B C D) i j = fromBlocks (x • A) (x • B) (x • C) (x • D) i j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
⊢ -fromBlocks A B C D = fromBlocks (-A) (-B) (-C) (-D)

Tactic:
ext i j

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
i : n ⊕ o
j : l ⊕ m
⊢ (-fromBlocks A B C D) i j = fromBlocks (-A) (-B) (-C) (-D) i j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
⊢ fromBlocks 0 0 0 0 = 0

Tactic:
ext i j

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
i : n ⊕ o
j : l ⊕ m
⊢ fromBlocks 0 0 0 0 i j = 0 i j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
⊢ fromBlocks A B C D + fromBlocks A' B' C' D' = fromBlocks (A + A') (B + B') (C + C') (D + D')

Tactic:
ext i j

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') i j = fromBlocks (A + A') (B + B') (C + C') (D + D') i j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
⊢ fromBlocks A B C D * fromBlocks A' B' C' D' =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D')

Tactic:
ext i j

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
i : n ⊕ o
j : p ⊕ q
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') i j =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') i j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
⊢ (diagonal d).toBlock p p = diagonal fun i ↦ d ↑i

Tactic:
ext i j

Goal state after:
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
⊢ (diagonal d).toBlock p p i j = diagonal (fun i ↦ d ↑i) i j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) = diagonal (Sum.elim d₁ d₂)

Tactic:
ext i j

Goal state after:
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
i j : l ⊕ m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) i j = diagonal (Sum.elim d₁ d₂) i j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
⊢ fromBlocks 1 0 0 1 = 1

Tactic:
ext i j

Goal state after:
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
i j : l ⊕ m
⊢ fromBlocks 1 0 0 1 i j = 1 i j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : m
j : n
r : α
⊢ updateCol 0 j (A *ᵥ Pi.single i r) = updateCol 0 j (A.col i <• r)

Tactic:
mulVec_single

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : m
j : n
r : α
⊢ updateCol 0 j (A.col i <• r) = updateCol 0 j (A.col i <• r)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
⊢ replicateCol ι (vecCons x u) = of (vecCons (fun x_1 ↦ x) (replicateCol ι u))

Tactic:
ext i j

Goal state after:
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
i : Fin m.succ
j : ι
⊢ replicateCol ι (vecCons x u) i j = of (vecCons (fun x_1 ↦ x) (replicateCol ι u)) i j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
⊢ (of (vecCons v A))ᵀ = of fun i ↦ vecCons (v i) (Aᵀ i)

Tactic:
ext i j

Goal state after:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
⊢ (of (vecCons v A))ᵀ i j = of (fun i ↦ vecCons (v i) (Aᵀ i)) i j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
n : ℕ
m' : Type uₘ
A : Matrix m' (Fin n.succ) α
⊢ vecTail (of.symm Aᵀ) = (vecTail ∘ A)ᵀ

Tactic:
ext i j

Goal state after:
α : Type u
n : ℕ
m' : Type uₘ
A : Matrix m' (Fin n.succ) α
i : Fin n
j : m'
⊢ vecTail (of.symm Aᵀ) i j = (vecTail ∘ A)ᵀ i j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
⊢ of (vecCons v A) * B = of (vecCons (v ᵥ* B) (of.symm (of A * B)))

Tactic:
ext i j

Goal state after:
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
⊢ (of (vecCons v A) * B) i j = of (vecCons (v ᵥ* B) (of.symm (of A * B))) i j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i : m'
row : Fin m → m'
col : o' → n'
⊢ A.submatrix (vecCons i row) col = vecCons (fun j ↦ A i (col j)) (A.submatrix row col)

Tactic:
ext i j

Goal state after:
α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i✝ : m'
row : Fin m → m'
col : o' → n'
i : Fin m.succ
j : o'
⊢ A.submatrix (vecCons i✝ row) col i j = vecCons (fun j ↦ A i✝ (col j)) (A.submatrix row col) i j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 = !![1, 0; 0, 1]

Tactic:
ext i j

Goal state after:
α : Type u
inst✝¹ : Zero α
inst✝ : One α
i j : Fin 2
⊢ 1 i j = !![1, 0; 0, 1] i j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 = !![1, 0, 0; 0, 1, 0; 0, 0, 1]

Tactic:
ext i j

Goal state after:
α : Type u
inst✝¹ : Zero α
inst✝ : One α
i j : Fin 3
⊢ 1 i j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] i j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n = !![↑n, 0; 0, ↑n]

Tactic:
ext i j

Goal state after:
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
i j : Fin 2
⊢ ↑n i j = !![↑n, 0; 0, ↑n] i j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n]

Tactic:
ext i j

Goal state after:
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
i j : Fin 3
⊢ ↑n i j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] i j