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

Goal state before:
pp: 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) α
⊢ (blockDiagonal' fun k ↦ M k * N k) = blockDiagonal' M * blockDiagonal' N

Tactic:
by

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
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:
by

Goal state after:
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 l
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
i : l
r : m → α
j : n
c : m → α
⊢ updateRow 0 i r * updateCol 0 j c = single i j (r ⬝ᵥ c)

Tactic:
by

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

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
⊢ (diagonal d).blockDiag' k i j = diagonal (fun i ↦ d ⟨k, i⟩) i j

Tactic:
by

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

Goal state before:
pp: R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k → Prop
A : Matrix m n R
B : Matrix n k R
⊢ (A * B).toBlock p q = A.toBlock p ⊤ * B.toBlock ⊤ q

Tactic:
by

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

Goal state before:
pp: R : Type u_10
inst✝² : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst✝¹ : Fintype n
p : m → Prop
q : n → Prop
inst✝ : DecidablePred q
r : k → Prop
A : Matrix m n R
B : Matrix n k R
⊢ (A * B).toBlock p r = A.toBlock p q * B.toBlock q r + (A.toBlock p fun i ↦ ¬q i) * B.toBlock (fun i ↦ ¬q i) r

Tactic:
by

Goal state after:
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:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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:
by

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

Goal state before:
pp: α : Type u
inst✝ : Zero α
d : Fin 1 → α
⊢ diagonal d = !![d 0]

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Zero α
d : Fin 2 → α
⊢ diagonal d = !![d 0, 0; 0, d 1]

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Zero α
d : Fin 3 → α
⊢ diagonal d = !![d 0, 0, 0; 0, d 1, 0; 0, 0, d 2]

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

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

Tactic:
by

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

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

Tactic:
by

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:
by

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

Goal state before:
pp: α : Type u
m : ℕ
n' : Type uₙ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
⊢ of (vecCons v A) *ᵥ w = vecCons (v ⬝ᵥ w) (of A *ᵥ w)

Tactic:
by

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

Goal state before:
pp: n : ℕ
m' : Type uₘ
α : Type u_1
inst✝ : NonUnitalCommSemiring α
A : m' → Fin n.succ → α
x : α
v : Fin n → α
⊢ of A *ᵥ vecCons x v = x • vecHead ∘ A + of (vecTail ∘ A) *ᵥ v

Tactic:
by

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

Goal state before:
pp: α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
⊢ vecMulVec (vecCons x v) w = vecCons (x • w) (vecMulVec v w)

Tactic:
by

Goal state after:
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:
by

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✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : DistribMulAction R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : DistribMulAction R C
inst✝³ : Star C
inst✝² : NonUnitalNonAssocSemiring D
inst✝¹ : DistribMulAction R D
inst✝ : Star D
⊢ Function.Injective fun f ↦ f.toFun

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : Star A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : DistribMulAction R B
inst✝ : Star B
f : A →⋆ₙₐ[R] B
h₁ : ∀ (m : R) (x : A), f (m • x) = (MonoidHom.id R) m • f x
h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y
h₄ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) =
      { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x *
        { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y
h₅ :
  ∀ (a : A),
    { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun (star a) =
      star ({ toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun a)
⊢ { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄, map_star' := h₅ } = f

Tactic:
by

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✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : DistribMulAction R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : DistribMulAction R C
inst✝³ : Star C
inst✝² : NonUnitalNonAssocSemiring D
inst✝¹ : DistribMulAction R D
inst✝ : Star D
f : B →⋆ₙₐ[R] C
g : A →⋆ₙₐ[R] B
⊢ ∀ (a : A), (f.comp g.toNonUnitalAlgHom).toFun (star a) = star ((f.comp g.toNonUnitalAlgHom).toFun a)

Tactic:
by

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:
by

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
D : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Star A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R B
inst✝⁶ : Star B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Star C
inst✝² : Semiring D
inst✝¹ : Algebra R D
inst✝ : Star D
⊢ Function.Injective fun f ↦ (↑↑f.toRingHom).toFun

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Star A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Star B
f : A →⋆ₐ[R] B
h₁ : f 1 = 1
h₂ :
  ∀ (x y : A),
    { toFun := ⇑f, map_one' := h₁ }.toFun (x * y) =
      { toFun := ⇑f, map_one' := h₁ }.toFun x * { toFun := ⇑f, map_one' := h₁ }.toFun y
h₃ : (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0
h₄ :
  ∀ (x y : A),
    (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) =
      (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun x +
        (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun y
h₅ :
  ∀ (r : R),
    (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) =
      (algebraMap R B) r
h₆ :
  ∀ (x : A),
    (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                  commutes' := h₅ }.toRingHom).toFun
        (star x) =
      star
        ((↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                    commutes' := h₅ }.toRingHom).toFun
          x)
⊢ { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_star' := h₆ } = f

Tactic:
by

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
D : Type u_6
inst✝¹⁸ : CommSemiring R✝
inst✝¹⁷ : Semiring A✝
inst✝¹⁶ : Algebra R✝ A✝
inst✝¹⁵ : Star A✝
inst✝¹⁴ : Semiring B
inst✝¹³ : Algebra R✝ B
inst✝¹² : Star B
inst✝¹¹ : Semiring C
inst✝¹⁰ : Algebra R✝ C
inst✝⁹ : Star C
inst✝⁸ : Semiring D
inst✝⁷ : Algebra R✝ D
inst✝⁶ : Star D
R : Type u_7
A : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarMul A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
⊢ ∀ (x : R), (algebraMap R A) (star x) = star ((algebraMap R A) x)

Tactic:
by

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
D : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Star A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R B
inst✝⁶ : Star B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Star C
inst✝² : Semiring D
inst✝¹ : Algebra R D
inst✝ : Star D
f : B →⋆ₐ[R] C
g : A →⋆ₐ[R] B
⊢ ∀ (x : A), (↑↑((↑f).comp ↑g).toRingHom).toFun (star x) = star ((↑↑((↑f).comp ↑g).toRingHom).toFun x)

Tactic:
by

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
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x : A
⊢ (f.prod g.toNonUnitalAlgHom).toFun (star x) = star ((f.prod g.toNonUnitalAlgHom).toFun x)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

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
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
⊢ (fst R B C).comp (f.prod g) = f

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

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
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
⊢ (snd R B C).comp (f.prod g) = g

Tactic:
by

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
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x : A
⊢ (↑↑((↑f).prod ↑g).toRingHom).toFun (star x) = star ((↑↑((↑f).prod ↑g).toRingHom).toFun x)

Tactic:
by

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
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
⊢ (fst R B C).comp (f.prod g) = f

Tactic:
by

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
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
⊢ (snd R B C).comp (f.prod g) = g

Tactic:
by

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
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : EquivLike F A B
inst✝ : NonUnitalAlgEquivClass F R A B
f : F
r : R
⊢ f ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
by

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
f g : A ≃⋆ₐ[R] B
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
by

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
e : A ≃⋆ₐ[R] B
r : R
b : B
⊢ e.symm.toFun (r • b) = r • e.symm.toFun b

Tactic:
by

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
⊢ f.toFun ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁵ : CommSemiring R
inst✝²⁴ : Semiring A
inst✝²³ : Semiring B
inst✝²² : Algebra R A
inst✝²¹ : Algebra R B
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
inst✝¹⁸ : Module A M
inst✝¹⁷ : IsScalarTower R A M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
inst✝¹² : Module A P
inst✝¹¹ : IsScalarTower R A P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R Q
inst✝⁸ : AddCommMonoid P'
inst✝⁷ : Module R P'
inst✝⁶ : Module A P'
inst✝⁵ : Module B P'
inst✝⁴ : IsScalarTower R A P'
inst✝³ : IsScalarTower R B P'
inst✝² : SMulCommClass A B P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
f : M →ₗ[A] N →ₗ[R] P
c : A
x : M
y : N
⊢ (TensorProduct.lift (↑R f) ∘ₗ (Algebra.lsmul R R (M ⊗[R] N)) c) (x ⊗ₜ[R] y) =
    ((Algebra.lsmul R R P) c ∘ₗ TensorProduct.lift (↑R f)) (x ⊗ₜ[R] y)

Tactic:
by

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₂
⊢ (fun f ↦ (e₂.symm.toNonUnitalStarAlgHom.comp f).comp e₁.toNonUnitalStarAlgHom)
      ((fun f ↦ (e₂.toNonUnitalStarAlgHom.comp f).comp e₁.symm.toNonUnitalStarAlgHom) f) =
    f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁸ : CommSemiring R
inst✝²⁷ : Semiring A
inst✝²⁶ : Semiring B
inst✝²⁵ : Algebra R A
inst✝²⁴ : Algebra R B
inst✝²³ : AddCommMonoid M
inst✝²² : Module R M
inst✝²¹ : Module A M
inst✝²⁰ : IsScalarTower R A M
inst✝¹⁹ : AddCommMonoid N
inst✝¹⁸ : Module R N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : Module R P
inst✝¹⁵ : Module A P
inst✝¹⁴ : IsScalarTower R A P
inst✝¹³ : AddCommMonoid Q
inst✝¹² : Module R Q
inst✝¹¹ : AddCommMonoid P'
inst✝¹⁰ : Module R P'
inst✝⁹ : Module A P'
inst✝⁸ : Module B P'
inst✝⁷ : IsScalarTower R A P'
inst✝⁶ : IsScalarTower R B P'
inst✝⁵ : SMulCommClass A B P'
inst✝⁴ : AddCommMonoid Q'
inst✝³ : Module R Q'
inst✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
x✝¹ x✝ : M →ₗ[A] N →ₗ[R] P
x : M
y : N
⊢ (lift (x✝¹ + x✝)) (x ⊗ₜ[R] y) = (lift x✝¹ + lift x✝) (x ⊗ₜ[R] y)

Tactic:
by

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₂'
⊢ (fun f ↦ (e₂.toNonUnitalStarAlgHom.comp f).comp e₁.symm.toNonUnitalStarAlgHom)
      ((fun f ↦ (e₂.symm.toNonUnitalStarAlgHom.comp f).comp e₁.toNonUnitalStarAlgHom) f) =
    f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁸ : CommSemiring R
inst✝²⁷ : Semiring A
inst✝²⁶ : Semiring B
inst✝²⁵ : Algebra R A
inst✝²⁴ : Algebra R B
inst✝²³ : AddCommMonoid M
inst✝²² : Module R M
inst✝²¹ : Module A M
inst✝²⁰ : IsScalarTower R A M
inst✝¹⁹ : AddCommMonoid N
inst✝¹⁸ : Module R N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : Module R P
inst✝¹⁵ : Module A P
inst✝¹⁴ : IsScalarTower R A P
inst✝¹³ : AddCommMonoid Q
inst✝¹² : Module R Q
inst✝¹¹ : AddCommMonoid P'
inst✝¹⁰ : Module R P'
inst✝⁹ : Module A P'
inst✝⁸ : Module B P'
inst✝⁷ : IsScalarTower R A P'
inst✝⁶ : IsScalarTower R B P'
inst✝⁵ : SMulCommClass A B P'
inst✝⁴ : AddCommMonoid Q'
inst✝³ : Module R Q'
inst✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
x✝¹ : B
x✝ : M →ₗ[A] N →ₗ[R] P
x : M
y : N
⊢ (lift (x✝¹ • x✝)) (x ⊗ₜ[R] y) = ((RingHom.id B) x✝¹ • lift x✝) (x ⊗ₜ[R] y)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

Goal state after: