mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: R : Type u
inst✝¹⁵ : CommSemiring R
S : Type u_2
inst✝¹⁴ : Semiring S
inst✝¹³ : Algebra R S
ι₂ : Type v₂
inst✝¹² : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝¹¹ : AddCommMonoid M₁'
inst✝¹⁰ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝⁹ : Module R M₁'
inst✝⁸ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝⁷ : Module S M₁'
inst✝⁶ : IsScalarTower R S M₁'
S₀ : Type u_1
inst✝⁵ : CommSemiring S₀
inst✝⁴ : Algebra R S₀
inst✝³ : Algebra S₀ S
inst✝² : Module S₀ M₁'
inst✝¹ : IsScalarTower R S₀ M₁'
inst✝ : IsScalarTower S₀ S M₁'
⊢ ↑(LinearEquiv.restrictScalars R (LinearEquiv.restrictScalars S₀ (directSumRight R S M₁' M₂))) =
    ↑(LinearEquiv.restrictScalars R (directSumRight R S₀ M₁' M₂))

Tactic:
ext

Goal state after:
R : Type u
inst✝¹⁵ : CommSemiring R
S : Type u_2
inst✝¹⁴ : Semiring S
inst✝¹³ : Algebra R S
ι₂ : Type v₂
inst✝¹² : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝¹¹ : AddCommMonoid M₁'
inst✝¹⁰ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝⁹ : Module R M₁'
inst✝⁸ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝⁷ : Module S M₁'
inst✝⁶ : IsScalarTower R S M₁'
S₀ : Type u_1
inst✝⁵ : CommSemiring S₀
inst✝⁴ : Algebra R S₀
inst✝³ : Algebra S₀ S
inst✝² : Module S₀ M₁'
inst✝¹ : IsScalarTower R S₀ M₁'
inst✝ : IsScalarTower S₀ S M₁'
x✝¹ : M₁'
i✝¹ : ι₂
x✝ : M₂ i✝¹
i✝ : ι₂
⊢ (((AlgebraTensorModule.curry
              ↑(LinearEquiv.restrictScalars R (LinearEquiv.restrictScalars S₀ (directSumRight R S M₁' M₂))))
            x✝¹ ∘ₗ
          lof R ι₂ M₂ i✝¹)
        x✝)
      i✝ =
    (((AlgebraTensorModule.curry ↑(LinearEquiv.restrictScalars R (directSumRight R S₀ M₁' M₂))) x✝¹ ∘ₗ lof R ι₂ M₂ i✝¹)
        x✝)
      i✝
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → MulOneClass (R i)
inst✝ : (i : ι) → StarMul (R i)
i : ι
r : R i
⊢ star (mulSingle i r) = mulSingle i (star r)

Tactic:
ext

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → MulOneClass (R i)
inst✝ : (i : ι) → StarMul (R i)
i : ι
r : R i
x✝ : ι
⊢ star (mulSingle i r) x✝ = mulSingle i (star r) x✝
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddMonoid (R i)
inst✝ : (i : ι) → StarAddMonoid (R i)
i : ι
r : R i
⊢ star (single i r) = single i (star r)

Tactic:
ext

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddMonoid (R i)
inst✝ : (i : ι) → StarAddMonoid (R i)
i : ι
r : R i
x✝ : ι
⊢ star (single i r) x✝ = single i (star r) x✝
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
inst✝¹ : StarRing R
S : Type u_1
inst✝ : NonAssocSemiring S
x✝ : S →+* R
⊢ (fun f ↦ (starRingEnd R).comp f) ((fun f ↦ (starRingEnd R).comp f) x✝) = x✝

Tactic:
ext

Goal state after:
R : Type u
inst✝² : CommSemiring R
inst✝¹ : StarRing R
S : Type u_1
inst✝ : NonAssocSemiring S
x✝¹ : S →+* R
x✝ : S
⊢ ((fun f ↦ (starRingEnd R).comp f) ((fun f ↦ (starRingEnd R).comp f) x✝¹)) x✝ = x✝¹ x✝
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
inst✝² : StarMul R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
⊢ star ⅟r = ⅟(star r)

Tactic:
rw [← mul_one (star (⅟r)), ← mul_invOf_self (star r), ← mul_assoc, ← star_mul]
  simp

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
M : Type u_3
inst✝² : Zero M
inst✝¹ : AddCommMonoid R
inst✝ : StarAddMonoid R
s : ι →₀ M
f : ι → M → R
⊢ star (s.sum f) = s.sum fun i m ↦ star f i m

Tactic:
by
  simp [Finsupp.sum]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Star A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : Star B
f : A →⋆ₙ+* B
h₁ : ∀ (x y : A), f (x * y) = f x * f y
h₂ : { toFun := ⇑f, map_mul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_mul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_mul' := h₁ }.toFun x + { toFun := ⇑f, map_mul' := h₁ }.toFun y
h₄ :
  ∀ (a : A),
    { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (star a) =
      star ({ toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun a)
⊢ { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃, map_star' := h₄ } = f

Tactic:
ext

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Star A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : Star B
f : A →⋆ₙ+* B
h₁ : ∀ (x y : A), f (x * y) = f x * f y
h₂ : { toFun := ⇑f, map_mul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_mul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_mul' := h₁ }.toFun x + { toFun := ⇑f, map_mul' := h₁ }.toFun y
h₄ :
  ∀ (a : A),
    { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (star a) =
      star ({ toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun a)
x✝ : A
⊢ { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃, map_star' := h₄ } x✝ = f x✝
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 y : A
⊢ ⟨⅟2 • (x + y + star (x + y)), ⋯⟩ = ⟨⅟2 • (x + star x), ⋯⟩ + ⟨⅟2 • (y + star y), ⋯⟩

Tactic:
ext

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 y : A
⊢ ↑⟨⅟2 • (x + y + star (x + y)), ⋯⟩ = ↑(⟨⅟2 • (x + star x), ⋯⟩ + ⟨⅟2 • (y + star y), ⋯⟩)
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
r : R
x : A
⊢ ⟨⅟2 • (r • x + star (r • x)), ⋯⟩ = (RingHom.id R) r • ⟨⅟2 • (x + star x), ⋯⟩

Tactic:
ext

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
r : R
x : A
⊢ ↑⟨⅟2 • (r • x + star (r • x)), ⋯⟩ = ↑((RingHom.id R) r • ⟨⅟2 • (x + star x), ⋯⟩)
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 y : A
⊢ ⟨⅟2 • (x + y - star (x + y)), ⋯⟩ = ⟨⅟2 • (x - star x), ⋯⟩ + ⟨⅟2 • (y - star y), ⋯⟩

Tactic:
ext

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 y : A
⊢ ↑⟨⅟2 • (x + y - star (x + y)), ⋯⟩ = ↑(⟨⅟2 • (x - star x), ⋯⟩ + ⟨⅟2 • (y - star y), ⋯⟩)
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
r : R
x : A
⊢ ⟨⅟2 • (r • x - star (r • x)), ⋯⟩ = (RingHom.id R) r • ⟨⅟2 • (x - star x), ⋯⟩

Tactic:
ext

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
r : R
x : A
⊢ ↑⟨⅟2 • (r • x - star (r • x)), ⋯⟩ = ↑((RingHom.id R) r • ⟨⅟2 • (x - star x), ⋯⟩)
Module: Mathlib.LinearAlgebra.Basis.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ (b.prod b') i = Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i

Tactic:
ext

Goal state after:
case fst
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ ((b.prod b') i).1 = (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i).1

case snd
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ ((b.prod b') i).2 = (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i).2
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 α
v : l ⊕ m → α
⊢ (diagonal v).toBlocks₁₁ = diagonal fun i ↦ v (Sum.inl i)

Tactic:
unfold toBlocks₁₁

Goal state after:
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
⊢ (of fun i j ↦ diagonal v (Sum.inl i) (Sum.inl j)) = diagonal fun i ↦ v (Sum.inl i)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
⊢ (blockDiagonal M).map f = blockDiagonal fun k ↦ (M k).map f

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i✝ : m × o
j✝ : n × o
⊢ (blockDiagonal M).map f i✝ j✝ = blockDiagonal (fun k ↦ (M k).map f) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : MulOneClass R
x : n → R
⊢ vecMulVec x 1 = replicateCol m x

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : MulOneClass R
x : n → R
i✝ : n
j✝ : m
⊢ vecMulVec x 1 i✝ j✝ = replicateCol m x i✝ j✝
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
⊢ (blockDiagonal M)ᵀ = blockDiagonal fun k ↦ (M k)ᵀ

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
⊢ (blockDiagonal M)ᵀ i✝ j✝ = blockDiagonal (fun k ↦ (M k)ᵀ) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : MulOneClass R
x : n → R
⊢ vecMulVec 1 x = replicateRow m x

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : MulOneClass R
x : n → R
i✝ : m
j✝ : n
⊢ vecMulVec 1 x i✝ j✝ = replicateRow m x i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Add α
v w : m → α
⊢ replicateCol ι (v + w) = replicateCol ι v + replicateCol ι w

Tactic:
ext

Goal state after:
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Add α
v w : m → α
i✝ : m
j✝ : ι
⊢ replicateCol ι (v + w) i✝ j✝ = (replicateCol ι v + replicateCol ι w) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst✝ : SMul R α
x : R
v : m → α
⊢ replicateCol ι (x • v) = x • replicateCol ι v

Tactic:
ext

Goal state after:
m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst✝ : SMul R α
x : R
v : m → α
i✝ : m
j✝ : ι
⊢ replicateCol ι (x • v) i✝ j✝ = (x • replicateCol ι v) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Add α
v w : m → α
⊢ replicateRow ι (v + w) = replicateRow ι v + replicateRow ι w

Tactic:
ext

Goal state after:
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Add α
v w : m → α
i✝ : ι
j✝ : m
⊢ replicateRow ι (v + w) i✝ j✝ = (replicateRow ι v + replicateRow ι w) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst✝ : SMul R α
x : R
v : m → α
⊢ replicateRow ι (x • v) = x • replicateRow ι v

Tactic:
ext

Goal state after:
m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst✝ : SMul R α
x : R
v : m → α
i✝ : ι
j✝ : m
⊢ replicateRow ι (x • v) i✝ j✝ = (x • replicateRow ι v) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
v : m → α
⊢ (replicateCol ι v)ᵀ = replicateRow ι v

Tactic:
ext

Goal state after:
m : Type u_2
α : Type v
ι : Type u_6
v : m → α
i✝ : ι
j✝ : m
⊢ (replicateCol ι v)ᵀ i✝ j✝ = replicateRow ι v i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
v : m → α
⊢ (replicateRow ι v)ᵀ = replicateCol ι v

Tactic:
ext

Goal state after:
m : Type u_2
α : Type v
ι : Type u_6
v : m → α
i✝ : m
j✝ : ι
⊢ (replicateRow ι v)ᵀ i✝ j✝ = replicateCol ι v i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Star α
v : m → α
⊢ (replicateCol ι v)ᴴ = replicateRow ι (star v)

Tactic:
ext

Goal state after:
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Star α
v : m → α
i✝ : ι
j✝ : m
⊢ (replicateCol ι v)ᴴ i✝ j✝ = replicateRow ι (star v) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Star α
v : m → α
⊢ (replicateRow ι v)ᴴ = replicateCol ι (star v)

Tactic:
ext

Goal state after:
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Star α
v : m → α
i✝ : m
j✝ : ι
⊢ (replicateRow ι v)ᴴ i✝ j✝ = replicateCol ι (star v) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
⊢ replicateRow ι (v ᵥ* M) = replicateRow ι v * M

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
i✝ : ι
j✝ : n
⊢ replicateRow ι (v ᵥ* M) i✝ j✝ = (replicateRow ι v * M) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
⊢ replicateCol ι (v ᵥ* M) = (replicateRow ι v * M)ᵀ

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
i✝ : n
j✝ : ι
⊢ replicateCol ι (v ᵥ* M) i✝ j✝ = (replicateRow ι v * M)ᵀ i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
⊢ replicateCol ι (M *ᵥ v) = M * replicateCol ι v

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
i✝ : m
j✝ : ι
⊢ replicateCol ι (M *ᵥ v) i✝ j✝ = (M * replicateCol ι v) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
⊢ replicateRow ι (M *ᵥ v) = (M * replicateCol ι v)ᵀ

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
i✝ : ι
j✝ : m
⊢ replicateRow ι (M *ᵥ v) i✝ j✝ = (M * replicateCol ι v)ᵀ i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: n : Type u_3
α : Type v
ι : Type u_6
inst✝² : Mul α
inst✝¹ : AddCommMonoid α
inst✝ : Unique ι
a b : n → α
⊢ (replicateCol ι a * replicateRow ι b).diag = a * b

Tactic:
ext

Goal state after:
n : Type u_3
α : Type v
ι : Type u_6
inst✝² : Mul α
inst✝¹ : AddCommMonoid α
inst✝ : Unique ι
a b : n → α
x✝ : n
⊢ (replicateCol ι a * replicateRow ι b).diag x✝ = (a * b) x✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝² : Mul α
inst✝¹ : AddCommMonoid α
inst✝ : Unique ι
w : m → α
v : n → α
⊢ vecMulVec w v = replicateCol ι w * replicateRow ι v

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝² : Mul α
inst✝¹ : AddCommMonoid α
inst✝ : Unique ι
w : m → α
v : n → α
i✝ : m
j✝ : n
⊢ vecMulVec w v i✝ j✝ = (replicateCol ι w * replicateRow ι v) i✝ j✝
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
⊢ blockDiagonal 0 = 0

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
i✝ : m × o
j✝ : n × o
⊢ blockDiagonal 0 i✝ j✝ = 0 i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
f : α → β
⊢ (M.updateRow i b).map f = (M.map f).updateRow i (f ∘ b)

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
j✝ : n
⊢ (M.updateRow i b).map f i✝ j✝ = (M.map f).updateRow i (f ∘ b) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
⊢ (M.updateCol j c).map f = (M.map f).updateCol j (f ∘ c)

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
j✝ : n
⊢ (M.updateCol j c).map f i✝ j✝ = (M.map f).updateCol j (f ∘ c) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
⊢ Mᵀ.updateRow j c = (M.updateCol j c)ᵀ

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
i✝ : n
j✝ : m
⊢ Mᵀ.updateRow j c i✝ j✝ = (M.updateCol j c)ᵀ i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
⊢ Mᵀ.updateCol i b = (M.updateRow i b)ᵀ

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
i✝ : n
j✝ : m
⊢ Mᵀ.updateCol i b i✝ j✝ = (M.updateRow i b)ᵀ i✝ j✝
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
⊢ blockDiagonal (M + N) = blockDiagonal M + blockDiagonal N

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
j✝ : n × o
⊢ blockDiagonal (M + N) i✝ j✝ = (blockDiagonal M + blockDiagonal N) i✝ j✝
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
R : Type u_14
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
x : R
M : o → Matrix m n α
⊢ blockDiagonal (x • M) = x • blockDiagonal M

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
R : Type u_14
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
x : R
M : o → Matrix m n α
i✝ : m × o
j✝ : n × o
⊢ blockDiagonal (x • M) i✝ j✝ = (x • blockDiagonal M) i✝ j✝
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
⊢ (blockDiagonal' M).map f = blockDiagonal' fun k ↦ (M k).map f

Tactic:
ext

Goal state after:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ (blockDiagonal' M).map f i✝ j✝ = blockDiagonal' (fun k ↦ (M k).map f) i✝ j✝
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
⊢ blockDiagonal' 0 = 0

Tactic:
ext

Goal state after:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ blockDiagonal' 0 i✝ j✝ = 0 i✝ j✝
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
⊢ blockDiagonal' (M + N) = blockDiagonal' M + blockDiagonal' N

Tactic:
ext

Goal state after:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ blockDiagonal' (M + N) i✝ j✝ = (blockDiagonal' M + blockDiagonal' N) i✝ j✝
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝² : DecidableEq o
R : Type u_14
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
⊢ blockDiagonal' (x • M) = x • blockDiagonal' M

Tactic:
ext

Goal state after:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝² : DecidableEq o
R : Type u_14
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ blockDiagonal' (x • M) i✝ j✝ = (x • blockDiagonal' M) i✝ j✝
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_14
inst✝¹ : Zero R
inst✝ : DecidableEq m
d : m → Matrix n n R
⊢ (comp m m n n R) (diagonal d) = (reindex (Equiv.prodComm n m) (Equiv.prodComm n m)) (blockDiagonal d)

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_14
inst✝¹ : Zero R
inst✝ : DecidableEq m
d : m → Matrix n n R
i✝ j✝ : m × n
⊢ (comp m m n n R) (diagonal d) i✝ j✝ = (reindex (Equiv.prodComm n m) (Equiv.prodComm n m)) (blockDiagonal d) 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
  fin_cases i <;> fin_cases j <;> rfl

Goal state after: