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

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝² : InvolutiveStar R
inst✝¹ : SetLike S R
inst✝ : StarMemClass S R
s : S
r : R
hr : star r ∈ s
⊢ star (star r) ∈ s

Tactic:
]

Goal state after:
S : Type u_1
R : Type u_2
inst✝² : InvolutiveStar R
inst✝¹ : SetLike S R
inst✝ : StarMemClass S R
s : S
r : R
hr : star r ∈ s
⊢ star (star r) ∈ s
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ star y * x = star y * x

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ y * star x = y * star x

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ Commute x (star y) ↔ Commute x (star y)

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommGroupWithZero R
inst✝ : StarMul R
x y : R
⊢ (op (star y))⁻¹ * op (star x) = (op (star y))⁻¹ * op (star x)

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
u : Rˣ
⊢ ↑(star u)⁻¹ = ↑(star u)⁻¹

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : ¬IsUnit a
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R✝ : Type u
R : Type u_1
inst✝² : MulOneClass R
inst✝¹ : StarMul R
r : R
inst✝ : Invertible r
⊢ 1 = 1

Tactic:
]

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

Goal state after:
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)
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsLeftRegular x ∧ IsRightRegular x ↔ IsLeftRegular x ∧ IsRightRegular x

Tactic:
]

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

Goal state before:
pp: R : Type u
S : Type v
f : R → S
inst✝¹ : Star R
inst✝ : InvolutiveStar S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
r : R
⊢ f r = f r

Tactic:
]

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

Goal state before:
pp: R : Type u
S : Type v
f : R → S
inst✝³ : Star R
inst✝² : Mul R
inst✝¹ : Mul S
inst✝ : StarMul S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
mul : ∀ (x y : R), f (x * y) = f x * f y
x y : R
⊢ Star.star (f y) * Star.star (f x) = Star.star (f y) * Star.star (f x)

Tactic:
]

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

Goal state before:
pp: R : Type u
S : Type v
f : R → S
inst✝³ : Star R
inst✝² : AddMonoid R
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
add : ∀ (x y : R), f (x + y) = f x + f y
x y : R
⊢ Star.star (f x) + Star.star (f y) = Star.star (f x) + Star.star (f y)

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: M : Type u_1
M₂ : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_3
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ≥0
x : M
⊢ ↑c.num • (↑c.den)⁻¹ • f x = ↑c.num • (↑c.den)⁻¹ • f x

Tactic:
]

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

Goal state before:
pp: M : Type u_1
M₂ : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_3
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ
x : M
⊢ ↑c.num • (↑c.den)⁻¹ • f x = ↑c.num • (↑c.den)⁻¹ • f x

Tactic:
]

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

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

Goal state after:
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
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: case refine_1
R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : Commute x y
⊢ y * x = y * x

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
inst✝¹ : StarMul R
x : R
inst✝ : Invertible x
⊢ star x = x ↔ star x = x

Tactic:
]

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

Goal state before:
pp: A : Type u_2
a : A
inst✝¹ : Semiring A
inst✝ : StarRing A
ha : IsSelfAdjoint a
⊢ a⁻¹ʳ = a⁻¹ʳ

Tactic:
]

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
inst✝² : Star A
inst✝¹ : MulAction R A
inst✝ : StarModule R A
x : A
r : Rˣ
hr : IsSelfAdjoint ↑r
hrx : IsSelfAdjoint (↑r • x)
⊢ IsSelfAdjoint (r⁻¹ • r • x)

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : Monoid R
inst✝³ : StarMul R
inst✝² : Star A
inst✝¹ : MulAction R A
inst✝ : StarModule R A
x : A
r : Rˣ
hr : IsSelfAdjoint ↑r
hrx : IsSelfAdjoint (↑r • x)
⊢ IsSelfAdjoint (r⁻¹ • r • x)
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x y : R
hx : star x = -x
hy : star y = -y
⊢ -x + -y = -x + -y

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (selfAdjoint R).carrier ↔ star x = x

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (selfAdjoint R).carrier ↔ star x = x
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ≥0
x : ↥(selfAdjoint R)
⊢ ↑a * ↑x ∈ selfAdjoint R

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ≥0
x : ↥(selfAdjoint R)
⊢ ↑a * ↑x ∈ selfAdjoint R
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ
x : ↥(selfAdjoint R)
⊢ ↑a * ↑x ∈ selfAdjoint R

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ
x : ↥(selfAdjoint R)
⊢ ↑a * ↑x ∈ selfAdjoint R
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (skewAdjoint R).carrier ↔ star x = -x

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (skewAdjoint R).carrier ↔ star x = -x
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : Star R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : Monoid R
inst✝¹ : DistribMulAction R A
inst✝ : StarModule R A
r : R
x : A
h : x ∈ skewAdjoint A
⊢ -(r • x) = -(r • x)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Mul R
inst✝¹ : StarMul R
x : R
inst✝ : IsStarNormal x
⊢ x * star x = x * star x

Tactic:
]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Mul R
inst✝¹ : StarMul R
inst✝ : TrivialStar R
x : R
⊢ Commute x x

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
⊢ Commute (star (a + b)) (a + b)

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
⊢ Commute (star (a + b)) (a + b)
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
⊢ a * star a + b * star a + (star b * a + b * star b) = a * star a + b * star a + (star b * a + b * star b)

Tactic:
]

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
e₂ : B ≃⋆+* C
a : A
⊢ star (e₂.toFun (e₁.toFun a)) = star (e₂.toFun (e₁.toFun a))

Tactic:
]

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 fun m ↦ star (v m)) = diagonal (star v)

Tactic:
]

Goal state after:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
v : n → α
⊢ (diagonal fun m ↦ star (v m)) = diagonal (star v)
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 w v)ᴴᵀ

Tactic:
]

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : Mul α
inst✝ : StarMul α
w : m → α
v : n → α
⊢ (vecMulVec w v).map star = (vecMulVec w v)ᴴᵀ
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 (star v) ↔ M = diagonal (star v)

Tactic:
]

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

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

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:
simp [conjTranspose, Matrix.map_natCast, diagonal_natCast]

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) = ⅟2 • (x + star x)

Tactic:
]

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

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

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
⊢ x = x

Tactic:
]

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

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

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

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

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

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

Tactic:
]

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
x : M
hx : x ∈ N
hc : c • y + x = 0
⊢ c = 0

Tactic:
]

Goal state after:
ι : 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
x : M
hx : x ∈ N
hc : c • y + x = 0
⊢ c = 0
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 = N

Tactic:
]

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
x : M
hx : x ∈ N
hc : c • y + x = 0
⊢ c = 0

Tactic:
]

Goal state after:
ι : 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
x : M
hx : x ∈ N
hc : c • y + x = 0
⊢ c = 0
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₂₂
⊢ fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂

Tactic:
]

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
  ext i j; rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [fromBlocks]

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
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ x • fromBlocks A B C D = fromBlocks (x • A) (x • B) (x • C) (x • D)

Tactic:
by
  ext i j; rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [fromBlocks]

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

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
⊢ ⊤ ≤ span R (range (w • v))
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
j : M
hj : j ∈ span R (range v)
⊢ j ∈ span R (range (w • v))

Tactic:
]

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
hj : j ∈ span R (range v)
⊢ j ∈ span R (range (w • v))
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
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
⊢ ∀ (p : Submodule R M), range (w • v) ⊆ ↑p → j ∈ p

Tactic:
]

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
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
⊢ ∀ (p : Submodule R M), range (w • v) ⊆ ↑p → j ∈ p
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
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
p : Submodule R M
hp : range (w • v) ⊆ ↑p
i : ι
this : v i ∈ p
⊢ v i ∈ ↑p

Tactic:
]

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
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
p : Submodule R M
hp : range (w • v) ⊆ ↑p
i : ι
this : v i ∈ p
⊢ v i ∈ ↑p
Module: Mathlib.Data.Matrix.Block

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

Tactic:
ext i j
  rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [diagonal]

Goal state after:
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 0) = if i✝.2 = j✝.2 then f (M i✝.2 i✝.1 j✝.1) else 0

Tactic:
]

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
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
h : i✝.2 = j✝.2
⊢ M j✝.2 j✝.1 i✝.1 = M j✝.2 j✝.1 i✝.1

Tactic:
]

Goal state after: