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

Goal state before:
pp: case pos
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
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₁'
m : M₁'
n✝ : ⨁ (i : ι₂), M₂ i
j : ι₂
n : M₂ j
⊢ ((↑R (component S ι₂ (fun i ↦ M₁' ⊗[R] M₂ i) j) ∘ₗ
          ↑R ↑(directSumRight R S M₁' M₂) ∘ₗ (mk R M₁' (⨁ (i : ι₂), M₂ i)) m) ∘ₗ
        lof R ι₂ M₂ j)
      n =
    (((mk R M₁' (M₂ j)) m ∘ₗ component R ι₂ M₂ j) ∘ₗ lof R ι₂ M₂ j) n

Tactic:
simp

Goal state after:
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 * ⅟r) * ⅟(star r) = ⅟(star r)

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝³ : DivisionSemiring R
inst✝² : MulAction R M
inst✝¹ : MulAction ℚ≥0 M
inst✝ : IsScalarTower ℚ≥0 R M
q : ℚ≥0
x : M
⊢ (↑q • 1) • x = (q • 1) • x

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝³ : DivisionRing R
inst✝² : MulAction R M
inst✝¹ : MulAction ℚ M
inst✝ : IsScalarTower ℚ R M
q : ℚ
x : M
⊢ (↑q • 1) • x = (q • 1) • x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : StarMul R
x : Rˣ
inst✝ : IsStarNormal ↑x
⊢ Commute (star ↑x⁻¹) ↑x⁻¹

Tactic:
by simpa [← Units.coe_star_inv, -Commute.units_val_iff] using star_comm_self

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : StarAddMonoid A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : StarAddMonoid B
⊢ ∀ (a : A), (NonUnitalRingHom.toMulHom 0).toFun (star a) = star ((NonUnitalRingHom.toMulHom 0).toFun a)

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
i : m
j : n
a : α
⊢ (single i j a)ᵀ.map ⇑starAddEquiv = single j i (star a)

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝ : InvolutiveStar α
M : Matrix m n α
⊢ ∀ (i : m) (j : n), Mᴴᴴ i j = M i j

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : AddCommMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : Module R A
inst✝ : StarModule R A
x : A
⊢ (starLinearEquiv R).symm x = starAddEquiv.invFun x

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
⊢ ∀ (i : n) (j : m), 0ᴴ i j = 0 i j

Tactic:
simp

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
⊢ ⅟2 • (x + star x) ∈ selfAdjoint A

Tactic:
selfAdjoint.mem_iff,

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
⊢ star (⅟2 • (x + star x)) = ⅟2 • (x + star x)
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
M : Matrix n n α
⊢ M = map 1 star ↔ M = 1

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M N : Matrix m n α
⊢ ∀ (i : n) (j : m), (M + N)ᴴ i j = (Mᴴ + Nᴴ) i j

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
M N : Matrix m n α
⊢ ∀ (i : n) (j : m), (M - N)ᴴ i j = (Mᴴ - Nᴴ) i j

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
c : ℕ
M : Matrix m n α
⊢ (c • M)ᴴ = c • Mᴴ

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
c : ℤ
M : Matrix m n α
⊢ (c • M)ᴴ = c • Mᴴ

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℕ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (↑c • M)ᴴ i j = (↑c • Mᴴ) i j

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℤ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (↑c • M)ᴴ i j = (↑c • Mᴴ) i j

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommMonoid α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℕ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), ((↑c)⁻¹ • M)ᴴ i j = ((↑c)⁻¹ • Mᴴ) i j

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℤ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), ((↑c)⁻¹ • M)ᴴ i j = ((↑c)⁻¹ • Mᴴ) i j

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℚ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (↑c • M)ᴴ i j = (↑c • Mᴴ) i j

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module ℚ α
c : ℚ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (c • M)ᴴ i j = (c • Mᴴ) i j

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (-M)ᴴ i j = (-Mᴴ) i j

Tactic:
simp

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

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✝⁷ : Fintype n
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TrivialStar R
inst✝³ : Semiring α
inst✝² : StarRing α
inst✝¹ : Algebra R α
inst✝ : StarModule R α
r : R
M : Matrix n n α
⊢ (conjTransposeRingEquiv n α) (r • M) = r • (conjTransposeRingEquiv n α) M

Tactic:
simp

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

Goal state before:
pp: case hl.fst
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 : ↥(selfAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑x + ↑0)).1 = ↑x

Tactic:
simp

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

Goal state before:
pp: case hl.snd
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 : ↥(selfAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑x + ↑0)).2 = 0

Tactic:
simp

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

Goal state before:
pp: case hr.fst
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 : ↥(skewAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑0 + ↑x)).1 = 0

Tactic:
simp

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

Goal state before:
pp: case hr.snd
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 : ↥(skewAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑0 + ↑x)).2 = ↑x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Fin

Goal state before:
pp: R : Type u_3
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
b : Basis (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ ⇑(have span_b := ⋯;
      Basis.mk ⋯ ⋯) =
    Fin.snoc (Subtype.val ∘ ⇑b) y

Tactic:
exact coe_mk (v := Fin.snoc (N.subtype ∘ b) y) _ _

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

Goal state before:
pp: l : Type u_14
m : Type u_15
n : Type u_16
o : Type u_17
α : Type u_18
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ (fromBlocks A B C D).submatrix Sum.swap Sum.swap = fromBlocks D C B A

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.SMul

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_5
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
⊢ ⊤ ≤ span R (range (w • v))

Tactic:
intro j

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_5
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
⊢ j ∈ ⊤ → j ∈ span R (range (w • v))
Module: Mathlib.LinearAlgebra.Basis.SMul

Goal state before:
pp: ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i : ι
⊢ ∀ (i_1 : ι), ((e.unitsSMul w).coord i) (e i_1) = ((w i)⁻¹ • e.coord i) (e i_1)

Tactic:
intro j

Goal state after:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ ((e.unitsSMul w).coord i) (e j) = ((w i)⁻¹ • e.coord i) (e 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
β : 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
⊢ (if i✝.2 = j✝.2 then f (M i✝.2 i✝.1 j✝.1) else f 0) = if i✝.2 = j✝.2 then f (M i✝.2 i✝.1 j✝.1) else 0

Tactic:
hf

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
⊢ (if i✝.2 = j✝.2 then f (M i✝.2 i✝.1 j✝.1) else 0) = if i✝.2 = j✝.2 then f (M i✝.2 i✝.1 j✝.1) else 0
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case pos
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
h✝ : i✝.2 = j✝.2
⊢ M i✝.2 i✝.1 j✝.1 + N i✝.2 i✝.1 j✝.1 = M i✝.2 i✝.1 j✝.1 + N i✝.2 i✝.1 j✝.1

Tactic:
simp

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

Goal state before:
pp: case neg
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
h✝ : ¬i✝.2 = j✝.2
⊢ 0 = 0 + 0

Tactic:
simp

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

Goal state before:
pp: case pos
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
h✝ : i✝.2 = j✝.2
⊢ x • M i✝.2 i✝.1 j✝.1 = x • M i✝.2 i✝.1 j✝.1

Tactic:
simp

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

Goal state before:
pp: case neg
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
h✝ : ¬i✝.2 = j✝.2
⊢ 0 = x • 0

Tactic:
simp

Goal state after:
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
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ (if h : i✝.fst = j✝.fst then f (M i✝.fst i✝.snd (cast ⋯ j✝.snd)) else f 0) =
    if h : i✝.fst = j✝.fst then f (M i✝.fst i✝.snd (cast ⋯ j✝.snd)) else 0

Tactic:
hf

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
⊢ (if h : i✝.fst = j✝.fst then f (M i✝.fst i✝.snd (cast ⋯ j✝.snd)) else 0) =
    if h : i✝.fst = j✝.fst then f (M i✝.fst i✝.snd (cast ⋯ j✝.snd)) else 0
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k k' : m' i
⊢ (if h : i = i then of (fun i_1 j ↦ if i_1 = j then d i i_1 else 0) k (cast ⋯ k') else 0) =
    of (fun i j ↦ if i = j then d i.fst i.snd else 0) ⟨i, k⟩ ⟨i, k'⟩

Tactic:
simp

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

Goal state before:
pp: case pos
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
h✝ : i✝.fst = j✝.fst
⊢ M i✝.fst i✝.snd (cast ⋯ j✝.snd) + N i✝.fst i✝.snd (cast ⋯ j✝.snd) =
    M i✝.fst i✝.snd (cast ⋯ j✝.snd) + N i✝.fst i✝.snd (cast ⋯ j✝.snd)

Tactic:
simp

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

Goal state before:
pp: case neg
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
h✝ : ¬i✝.fst = j✝.fst
⊢ 0 = 0 + 0

Tactic:
simp

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

Goal state before:
pp: case pos
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
h✝ : k = k'
⊢ ∑ j_1, M k i j_1 * N k j_1 (cast ⋯ j) = ∑ x, M k i (cast ⋯ x) * N k x (cast ⋯ j)

Tactic:
simp

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

Goal state before:
pp: case neg
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
h✝ : ¬k = k'
⊢ 0 = ∑ x, M k i (cast ⋯ x) * 0

Tactic:
simp

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

Goal state before:
pp: case pos
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
h✝ : i✝.fst = j✝.fst
⊢ x • M i✝.fst i✝.snd (cast ⋯ j✝.snd) = x • M i✝.fst i✝.snd (cast ⋯ j✝.snd)

Tactic:
simp

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

Goal state before:
pp: case neg
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
h✝ : ¬i✝.fst = j✝.fst
⊢ 0 = x • 0

Tactic:
simp

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

Goal state before:
pp: case refine_1
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
B : Fin m → n' → α
i : Fin m.succ
j : n'
⊢ vecCons v B 0 j = vecCons (v j) (fun i ↦ B i j) 0

Tactic:
simp

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

Goal state before:
pp: case refine_2
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
B : Fin m → n' → α
i : Fin m.succ
j : n'
⊢ ∀ (i : Fin m), vecCons v B i.succ j = vecCons (v j) (fun i ↦ B i j) i.succ

Tactic:
simp

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

Goal state before:
pp: α : Type u
n : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v ⬝ᵥ vecCons y w = x * y + v ⬝ᵥ w

Tactic:
simp

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

Goal state before:
pp: case refine_1
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
i : Fin m.succ
j : ι
⊢ replicateCol ι (vecCons x u) 0 j = of (vecCons (fun x_1 ↦ x) (replicateCol ι u)) 0 j

Tactic:
simp

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

Goal state before:
pp: case refine_2
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
i : Fin m.succ
j : ι
⊢ ∀ (i : Fin m), replicateCol ι (vecCons x u) i.succ j = of (vecCons (fun x_1 ↦ x) (replicateCol ι u)) i.succ j

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case refine_2
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
⊢ ∀ (i_1 : Fin m), (of (vecCons v A))ᵀ i i_1.succ = of (fun i ↦ vecCons (v i) (Aᵀ i)) i i_1.succ

Tactic:
simp

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

Goal state before:
pp: α : Type u
n : ℕ
o' : Type uₒ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
w : o' → α
B : Fin n → o' → α
⊢ vecCons x v ᵥ* of (vecCons w B) = x • w + v ᵥ* of B

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : StarAddMonoid A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : DistribMulAction R B
inst✝ : StarAddMonoid B
⊢ ∀ (a : A),
    (NonUnitalAlgHom.toDistribMulActionHom 0).toFun (star a) = star ((NonUnitalAlgHom.toDistribMulActionHom 0).toFun a)

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
R✝ : Type u_2
A✝ : Type u_3
B✝ : Type u_4
C : Type u_5
inst✝¹⁸ : Add A✝
inst✝¹⁷ : Add B✝
inst✝¹⁶ : Mul A✝
inst✝¹⁵ : Mul B✝
inst✝¹⁴ : SMul R✝ A✝
inst✝¹³ : SMul R✝ B✝
inst✝¹² : Star A✝
inst✝¹¹ : Star B✝
inst✝¹⁰ : Add C
inst✝⁹ : Mul C
inst✝⁸ : SMul R✝ C
inst✝⁷ : Star C
R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Star A
inst✝ : Star B
f : A ≃⋆ₐ[R] B
r : R
⊢ r • f.toFun 1 = r • 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : Monoid R
inst✝¹⁷ : NonUnitalNonAssocSemiring A₁
inst✝¹⁶ : DistribMulAction R A₁
inst✝¹⁵ : Star A₁
inst✝¹⁴ : NonUnitalNonAssocSemiring A₂
inst✝¹³ : DistribMulAction R A₂
inst✝¹² : Star A₂
inst✝¹¹ : NonUnitalNonAssocSemiring A₃
inst✝¹⁰ : DistribMulAction R A₃
inst✝⁹ : Star A₃
inst✝⁸ : NonUnitalNonAssocSemiring A₁'
inst✝⁷ : DistribMulAction R A₁'
inst✝⁶ : Star A₁'
inst✝⁵ : NonUnitalNonAssocSemiring A₂'
inst✝⁴ : DistribMulAction R A₂'
inst✝³ : Star A₂'
inst✝² : NonUnitalNonAssocSemiring A₃'
inst✝¹ : DistribMulAction R A₃'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁ →⋆ₙₐ[R] A₂
x✝ : A₁
⊢ ((fun f ↦ (e₂.symm.toNonUnitalStarAlgHom.comp f).comp e₁.toNonUnitalStarAlgHom)
        ((fun f ↦ (e₂.toNonUnitalStarAlgHom.comp f).comp e₁.symm.toNonUnitalStarAlgHom) f))
      x✝ =
    f x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : Monoid R
inst✝¹⁷ : NonUnitalNonAssocSemiring A₁
inst✝¹⁶ : DistribMulAction R A₁
inst✝¹⁵ : Star A₁
inst✝¹⁴ : NonUnitalNonAssocSemiring A₂
inst✝¹³ : DistribMulAction R A₂
inst✝¹² : Star A₂
inst✝¹¹ : NonUnitalNonAssocSemiring A₃
inst✝¹⁰ : DistribMulAction R A₃
inst✝⁹ : Star A₃
inst✝⁸ : NonUnitalNonAssocSemiring A₁'
inst✝⁷ : DistribMulAction R A₁'
inst✝⁶ : Star A₁'
inst✝⁵ : NonUnitalNonAssocSemiring A₂'
inst✝⁴ : DistribMulAction R A₂'
inst✝³ : Star A₂'
inst✝² : NonUnitalNonAssocSemiring A₃'
inst✝¹ : DistribMulAction R A₃'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁' →⋆ₙₐ[R] A₂'
x✝ : A₁'
⊢ ((fun f ↦ (e₂.toNonUnitalStarAlgHom.comp f).comp e₁.symm.toNonUnitalStarAlgHom)
        ((fun f ↦ (e₂.symm.toNonUnitalStarAlgHom.comp f).comp e₁.toNonUnitalStarAlgHom) f))
      x✝ =
    f x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : Monoid R
inst✝¹⁷ : NonUnitalNonAssocSemiring A₁
inst✝¹⁶ : DistribMulAction R A₁
inst✝¹⁵ : Star A₁
inst✝¹⁴ : NonUnitalNonAssocSemiring A₂
inst✝¹³ : DistribMulAction R A₂
inst✝¹² : Star A₂
inst✝¹¹ : NonUnitalNonAssocSemiring A₃
inst✝¹⁰ : DistribMulAction R A₃
inst✝⁹ : Star A₃
inst✝⁸ : NonUnitalNonAssocSemiring A₁'
inst✝⁷ : DistribMulAction R A₁'
inst✝⁶ : Star A₁'
inst✝⁵ : NonUnitalNonAssocSemiring A₂'
inst✝⁴ : DistribMulAction R A₂'
inst✝³ : Star A₂'
inst✝² : NonUnitalNonAssocSemiring A₃'
inst✝¹ : DistribMulAction R A₃'
inst✝ : Star A₃'
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
e₃ : A₃ ≃⋆ₐ[R] A₃'
f : A₁ →⋆ₙₐ[R] A₂
g : A₂ →⋆ₙₐ[R] A₃
x✝ : A₁'
⊢ ((e₁.arrowCongr' e₃) (g.comp f)) x✝ = (((e₂.arrowCongr' e₃) g).comp ((e₁.arrowCongr' e₂) f)) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Semiring A₁
inst✝¹⁶ : Semiring A₂
inst✝¹⁵ : Semiring A₃
inst✝¹⁴ : Semiring A₁'
inst✝¹³ : Semiring A₂'
inst✝¹² : Semiring A₃'
inst✝¹¹ : Algebra R A₁
inst✝¹⁰ : Algebra R A₂
inst✝⁹ : Algebra R A₃
inst✝⁸ : Algebra R A₁'
inst✝⁷ : Algebra R A₂'
inst✝⁶ : Algebra R A₃'
inst✝⁵ : Star A₁
inst✝⁴ : Star A₂
inst✝³ : Star A₃
inst✝² : Star A₁'
inst✝¹ : Star A₂'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁ →⋆ₐ[R] A₂
x✝ : A₁
⊢ ((fun f ↦ (e₂.symm.toStarAlgHom.comp f).comp e₁.toStarAlgHom)
        ((fun f ↦ (e₂.toStarAlgHom.comp f).comp e₁.symm.toStarAlgHom) f))
      x✝ =
    f x✝

Tactic:
simp

Goal state after: