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

Goal state before:
pp: 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
i : ι₂
⊢ ((directSumRight R S M₁' M₂) (m ⊗ₜ[R] n)) i = m ⊗ₜ[R] n i

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Field.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
q : ℚ≥0
⊢ unop ↑q = unop (↑q.num / ↑q.den)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Field.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
q : ℚ
⊢ unop ↑q = unop (↑q.num / ↑q.den)

Tactic:
by

Goal state after:
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
⊢ r ∈ s

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : InvolutiveStar R
r s : R
h : r = star s
⊢ s = star r

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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 (star x) y ↔ Commute x (star y)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : AddMonoid R
inst✝ : StarAddMonoid R
x : R
⊢ star x ≠ 0 ↔ x ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
inst✝¹ : StarRing R
S : Type u_1
inst✝ : NonAssocSemiring S
⊢ Function.Involutive fun f ↦ (starRingEnd R).comp f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ

Tactic:
by

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
⊢ star ⅟r * star r = 1

Tactic:
by

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
⊢ star r * star ⅟r = 1

Tactic:
by

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 = ⅟(star r)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
hx : IsLeftRegular x
a b : R
h : (fun x_1 ↦ x_1 * star x) a = (fun x_1 ↦ x_1 * star x) b
⊢ (fun x_1 ↦ x * x_1) (star a) = (fun x_1 ↦ x * x_1) (star b)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
hx : IsRightRegular x
a b : R
h : (fun x_1 ↦ star x * x_1) a = (fun x_1 ↦ star x * x_1) b
⊢ (fun x_1 ↦ x_1 * x) (star a) = (fun x_1 ↦ x_1 * x) (star b)

Tactic:
by

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

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

Tactic:
by

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 (Star.star (Star.star r)) = f r

Tactic:
by

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
⊢ f (Star.star (x * y)) = f (Star.star y * Star.star x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹ : AddCommMonoid R
inst✝ : StarAddMonoid R
s : Finset ι
x : ι → R
h : ∀ i ∈ s, IsSelfAdjoint (x i)
⊢ IsSelfAdjoint (∑ i ∈ s, x i)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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
⊢ f (Star.star (x + y)) = f (Star.star x + Star.star y)

Tactic:
by

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
⊢ f (Star.star (r • x)) = f (Star.star r • Star.star x)

Tactic:
by

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 • f ((↑c.den)⁻¹ • x) = ↑c.num • (↑c.den)⁻¹ • f x

Tactic:
map_inv_natCast_smul f R S

Goal state after:
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
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
⊢ f (↑c • x) = ↑c • f x

Tactic:
by

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 • f ((↑c.den)⁻¹ • x) = ↑c.num • (↑c.den)⁻¹ • f x

Tactic:
map_inv_natCast_smul f R S

Goal state after:
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
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
⊢ f (↑c • x) = ↑c • f x

Tactic:
by

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 • x = q • x

Tactic:
by

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 • x = q • x

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ n • a) x = (fun a ↦ n • a) y
⊢ x = y

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module ℚ M
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ n • a) x = (fun a ↦ n • a) y
⊢ x = y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : InvolutiveStar R
x : R
⊢ IsSelfAdjoint (star x) ↔ IsSelfAdjoint x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsSelfAdjoint (star x * x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsSelfAdjoint (x * star x)

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ Commute x y ↔ IsSelfAdjoint (x * y)

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y z : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
hz : IsSelfAdjoint z
hxyz : x * y = z
⊢ Commute x y

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Mul R
inst✝ : Star R
x : R
hx : IsSelfAdjoint x
⊢ Commute (star x) x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : StarAddMonoid R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x + y)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (-x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x - y)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : StarAddMonoid R
x : R
⊢ IsSelfAdjoint (x + star x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : StarAddMonoid R
x : R
⊢ IsSelfAdjoint (star x + x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
⊢ IsSelfAdjoint (z * x * star z)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
⊢ IsSelfAdjoint (star z * x * z)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
hz : IsSelfAdjoint z
⊢ IsSelfAdjoint (z * x * z)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
n : ℕ
⊢ IsSelfAdjoint (x ^ n)

Tactic:
by

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
⊢ IsSelfAdjoint ⅟x ↔ IsSelfAdjoint x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
a u : R
hu : IsUnit u
⊢ IsSelfAdjoint (u * a * star u) ↔ IsSelfAdjoint a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
a u : R
hu : IsUnit u
⊢ IsSelfAdjoint (star u * a * u) ↔ IsSelfAdjoint a

Tactic:
by

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
⊢ IsSelfAdjoint a⁻¹ʳ

Tactic:
by

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 : IsUnit a
h : IsSelfAdjoint a⁻¹ʳ
⊢ IsSelfAdjoint a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemigroup R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x * y)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Group R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint x⁻¹

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Group R
inst✝ : StarMul R
x : R
⊢ IsSelfAdjoint x⁻¹ ↔ IsSelfAdjoint x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Group R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
n : ℤ
⊢ IsSelfAdjoint (x ^ n)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint x⁻¹

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
x : R
⊢ IsSelfAdjoint x⁻¹ ↔ IsSelfAdjoint x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
n : ℤ
⊢ IsSelfAdjoint (x ^ n)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semifield R
inst✝ : StarRing R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x / y)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Star R
inst✝² : Star A
inst✝¹ : SMul R A
inst✝ : StarModule R A
r : R
hr : IsSelfAdjoint r
x : A
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (r • x)

Tactic:
by

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
r : R
hr : IsSelfAdjoint r
hu : IsUnit r
x : A
⊢ IsSelfAdjoint (r • x) ↔ IsSelfAdjoint x

Tactic:
by

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 ↔ star x = x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : ↥(selfAdjoint R)
⊢ IsSelfAdjoint ↑x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
⊢ ∀ (n : ℕ) (x : ↥(selfAdjoint R)), ↑(n • x) = n • ↑x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
⊢ ∀ (n : ℤ) (x : ↥(selfAdjoint R)), ↑(n • x) = n • ↑x

Tactic:
by

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

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

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
⊢ ∀ (n : ℤ) (x : ↥(selfAdjoint R)), ↑(n • x) = n • ↑x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : x ∈ skewAdjoint R
z : R
⊢ z * x * star z ∈ skewAdjoint R

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : x ∈ skewAdjoint R
z : R
⊢ star z * x * z ∈ skewAdjoint R

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : x ∈ skewAdjoint R
⊢ Commute (star x) x

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarAddMonoid R
⊢ Commute (star 0) 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : MulOneClass R
inst✝ : StarMul R
⊢ Commute (star 1) 1

Tactic:
by

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

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

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
F : Type u_3
R : Type u_4
S : Type u_5
inst✝⁶ : Mul R
inst✝⁵ : Star R
inst✝⁴ : Mul S
inst✝³ : Star S
inst✝² : FunLike F R S
inst✝¹ : MulHomClass F R S
inst✝ : StarHomClass F R S
f : F
r : R
hr : IsStarNormal r
⊢ Commute (star (f r)) (f r)

Tactic:
by

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 (star x) x

Tactic:
by

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 : IsStarNormal a
hb : IsStarNormal b
⊢ IsStarNormal (a + b)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : StarRing R
a b : R
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ b * a = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : StarRing R
a b : R
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ Commute a b

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

Tactic:
by

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

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

Tactic:
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
D : Type u_4
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Star B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Star C
inst✝¹ : NonUnitalNonAssocSemiring D
inst✝ : Star D
f : B →⋆ₙ+* C
g : A →⋆ₙ+* B
a : A
⊢ (f.comp g.toNonUnitalRingHom).toFun (star a) = star ((f.comp g.toNonUnitalRingHom).toFun a)

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

Goal state after: