mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.StarRingHom

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝⁸ : Add A
inst✝⁷ : Add B
inst✝⁶ : Mul A
inst✝⁵ : Mul B
inst✝⁴ : Star A
inst✝³ : Star B
inst✝² : Add C
inst✝¹ : Mul C
inst✝ : Star C
f g : A ≃⋆+* B
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
by

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✝⁸ : Add A
inst✝⁷ : Add B
inst✝⁶ : Mul A
inst✝⁵ : Mul B
inst✝⁴ : Star A
inst✝³ : Star B
inst✝² : Add C
inst✝¹ : Mul C
inst✝ : Star C
e : A ≃⋆+* B
b : B
⊢ e.symm.toFun (star b) = star (e.symm.toFun b)

Tactic:
by

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)ᴴ = single j i (star a)

Tactic:
by

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
v : n → α
⊢ (diagonal v)ᴴ = diagonal (star v)

Tactic:
by

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
v w : m → α
⊢ star v ⬝ᵥ star w = star (w ⬝ᵥ v)

Tactic:
by

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
v w : m → α
⊢ star v ⬝ᵥ w = star (star w ⬝ᵥ v)

Tactic:
by

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
v w : m → α
⊢ v ⬝ᵥ star w = star (w ⬝ᵥ star v)

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : Mul α
inst✝ : StarMul α
w : m → α
v : n → α
⊢ (vecMulVec w v).map star = (vecMulVec (star v) (star w))ᵀ

Tactic:
by

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

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : Matrix n n α
v : n → α
⊢ M = (diagonal v)ᴴ ↔ M = diagonal (star v)

Tactic:
by

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : Matrix n n α
v : n → α
⊢ M = (diagonal v).map star ↔ M = diagonal (star v)

Tactic:
by

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

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

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 : Matrix m n α
⊢ Mᴴ = 0 ↔ M = 0

Tactic:
by

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 : Matrix m n α
⊢ M.map star = 0 ↔ M = 0

Tactic:
by

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
⊢ 1ᴴ = 1

Tactic:
by

Goal state after:
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 = 1ᴴ ↔ M = 1

Tactic:
by

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

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
d : ℕ
⊢ (↑d)ᴴ = ↑d

Tactic:
by

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
d : ℕ
⊢ (↑d).map star = ↑d

Tactic:
by

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

Goal state after:
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 α
d : ℕ
⊢ M = (↑d)ᴴ ↔ M = ↑d

Tactic:
by

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

Tactic:
by

Goal state after:
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 α
d : ℕ
⊢ M = (↑d).map star ↔ M = ↑d

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Ring α
inst✝ : StarRing α
d : ℤ
⊢ (↑d)ᴴ = ↑d

Tactic:
by

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) ∈ skewAdjoint A

Tactic:
by

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Ring α
inst✝ : StarRing α
d : ℤ
⊢ (↑d).map star = ↑d

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Ring α
inst✝ : StarRing α
M : Matrix n n α
d : ℤ
⊢ M = (↑d)ᴴ ↔ M = ↑d

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Ring α
inst✝ : StarRing α
M : Matrix n n α
d : ℤ
⊢ M = (↑d).map star ↔ M = ↑d

Tactic:
by

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
⊢ ↑((selfAdjointPart R) x) + ↑((skewAdjointPart R) x) = x

Tactic:
by

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

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

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
⊢ ↑((selfAdjointPart R) x) = x

Tactic:
by

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✝³ : Star R
inst✝² : Star α
inst✝¹ : SMul R α
inst✝ : SMul Rᵐᵒᵖ α
c : R
M : Matrix m n α
h : ∀ (r : R) (a : α), star (r • a) = MulOpposite.op (star r) • star a
⊢ ∀ (i : n) (j : m), (c • M)ᴴ i j = (MulOpposite.op (star c) • Mᴴ) i j

Tactic:
by

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

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
⊢ 0 = ↑0

Tactic:
ZeroMemClass.coe_zero

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
⊢ 0 = 0
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
⊢ ↑((skewAdjointPart R) x) = ↑0

Tactic:
by

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

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✝ : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
⊢ ↑((selfAdjointPart R ∘ₗ (skewAdjoint.submodule R A).subtype) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)

Tactic:
by

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

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✝ : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
⊢ ↑((skewAdjointPart R ∘ₗ (skewAdjoint.submodule R A).subtype) ⟨x, hx⟩) = ↑(LinearMap.id ⟨x, hx⟩)

Tactic:
by

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

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

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

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

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

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : Fintype n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
M : Matrix m n α
N : Matrix n l α
⊢ ∀ (i : l) (j : m), (M * N)ᴴ i j = (Nᴴ * Mᴴ) i j

Tactic:
by

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

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 α).toFun (r • M) = r • (conjTransposeRingEquiv n α).toFun M

Tactic:
by

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
⊢ A ≃ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)

Tactic:
by

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✝³ : Semiring A
inst✝² : StarMul A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
r : R
⊢ (algebraMap R A) (star r) = star ((algebraMap R A) r)

Tactic:
by

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✝³ : Semiring A
inst✝² : StarMul A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
r : R
hr : IsSelfAdjoint r
⊢ IsSelfAdjoint ((algebraMap R A) r)

Tactic:
by

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

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ N = span R (Set.range (⇑N.subtype ∘ ⇑b))

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
span_b : N = span R (Set.range (⇑N.subtype ∘ ⇑b))
⊢ ∀ (c : R), ∀ y_1 ∈ span R (Set.range (⇑N.subtype ∘ ⇑b)), c • y + y_1 = 0 → c = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x✝¹ y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
span_b : N = span R (Set.range (⇑N.subtype ∘ ⇑b))
x : M
x✝ : x ∈ ⊤
⊢ x ∈ span R (Set.range (Fin.cons y (⇑N.subtype ∘ ⇑b)))

Tactic:
by

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
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ ⇑(mkFinCons y b hli hsp) = Fin.cons y (Subtype.val ∘ ⇑b)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι 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
⊢ N = span R (Set.range (⇑N.subtype ∘ ⇑b))

Tactic:
by

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

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι 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
span_b : N = span R (Set.range (⇑N.subtype ∘ ⇑b))
⊢ ∀ (c : R), ∀ y_1 ∈ span R (Set.range (⇑N.subtype ∘ ⇑b)), c • y + y_1 = 0 → c = 0

Tactic:
by

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
A B : Matrix (n ⊕ o) (l ⊕ m) α
x✝ :
  A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂
h₁₁ : A.toBlocks₁₁ = B.toBlocks₁₁
h₁₂ : A.toBlocks₁₂ = B.toBlocks₁₂
h₂₁ : A.toBlocks₂₁ = B.toBlocks₂₁
h₂₂ : A.toBlocks₂₂ = B.toBlocks₂₂
⊢ A = B

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x✝¹ y✝ : M
b✝ : Basis ι 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
span_b : N = span R (Set.range (⇑N.subtype ∘ ⇑b))
x : M
x✝ : x ∈ ⊤
⊢ x ∈ span R (Set.range (Fin.snoc (⇑N.subtype ∘ ⇑b) y))

Tactic:
by

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

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
⊢ ⇑(b.mkFinSnoc y hli hsp) = Fin.snoc (Subtype.val ∘ ⇑b) y

Tactic:
by

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

Goal state before:
pp: R : Type u_7
inst✝ : Semiring R
⊢ (Basis.finTwoProd R) 0 = (1, 0)

Tactic:
by

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

Goal state before:
pp: R : Type u_7
inst✝ : Semiring R
⊢ (Basis.finTwoProd R) 1 = (0, 1)

Tactic:
by

Goal state after:
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.repr ((b.prod b') (Sum.inl i)).1 = b.repr (b i)

Tactic:
by

Goal state after:
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.repr ((b.prod b') (Sum.inr i)).1 = b.repr 0

Tactic:
by

Goal state after:
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'.repr ((b.prod b') (Sum.inl i)).2 = b'.repr 0

Tactic:
by

Goal state after:
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✝ i : ι'
⊢ (b'.repr ((b.prod b') (Sum.inr i✝)).2) i = (b'.repr (b' i✝)) i

Tactic:
simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b'.repr.apply_symm_apply,
      LinearEquiv.symm_symm, repr_self, Finsupp.snd_sumFinsuppLEquivProdFinsupp]

Goal state after:
ι : 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✝ i : ι'
⊢ (single (Sum.inr i✝) 1) (Sum.inr i) = (single i✝ 1) i