awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : StarAddMonoid R
x : R
⊢ IsSelfAdjoint (x + star x)

Tactic:
simp only [isSelfAdjoint_iff, add_comm, star_add, star_star]

Premises used: star_star, StarAddMonoid.star_add, add_comm, isSelfAdjoint_iff
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : StarAddMonoid R
x : R
⊢ IsSelfAdjoint (star x + x)

Tactic:
simp only [isSelfAdjoint_iff, add_comm, star_add, star_star]

Premises used: star_star, StarAddMonoid.star_add, add_comm, isSelfAdjoint_iff
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Semigroup R
inst_1 : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
⊢ IsSelfAdjoint (z * x * star z)

Tactic:
simp only [isSelfAdjoint_iff, star_mul, star_star, mul_assoc, hx.star_eq]

Premises used: star_star, mul_assoc, StarMul.star_mul, isSelfAdjoint_iff, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Semigroup R
inst_1 : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
⊢ IsSelfAdjoint (star z * x * z)

Tactic:
simp only [isSelfAdjoint_iff, star_mul, star_star, mul_assoc, hx.star_eq]

Premises used: star_star, mul_assoc, StarMul.star_mul, isSelfAdjoint_iff, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Semigroup R
inst_1 : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
hz : IsSelfAdjoint z
nth_rewrite : IsSelfAdjoint (z * x * star z)
⊢ IsSelfAdjoint (z * x * z)

Tactic:
nth_rewrite 2 [← hz]
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Semigroup R
inst_1 : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
hz : IsSelfAdjoint z
⊢ IsSelfAdjoint (z * x * star z)

Tactic:
conjugate hx z

Premises used: IsSelfAdjoint.conjugate
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Semigroup R
inst_1 : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
hz : IsSelfAdjoint z
⊢ IsSelfAdjoint (z * x * star z)

Tactic:
exact conjugate hx z

Premises used: IsSelfAdjoint.conjugate
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : MulOneClass R
inst_1 : StarMul R
⊢ IsSelfAdjoint.{u_1} (R := R) 1

Tactic:
star_one R

Premises used: IsSelfAdjoint, star_one
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x : R
hx : IsSelfAdjoint x
n : ℕ
⊢ IsSelfAdjoint (x ^ n)

Tactic:
simp only [isSelfAdjoint_iff, star_pow, hx.star_eq]

Premises used: isSelfAdjoint_iff, IsSelfAdjoint.star_eq, star_pow
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x : R
inst_2 : Invertible x
rw :
  star (@Invertible.invOf _ MulOne.toMul MulOne.toOne x _) = @Invertible.invOf _ MulOne.toMul MulOne.toOne x _ ↔
    IsSelfAdjoint x
rw₁ :
  star (@Invertible.invOf _ MulOne.toMul MulOne.toOne x _) = @Invertible.invOf _ MulOne.toMul MulOne.toOne x _ ↔
    star x = x
rw₂ :
  @Invertible.invOf _ MulOne.toMul MulOne.toOne (star x) _ = @Invertible.invOf _ MulOne.toMul MulOne.toOne x _ ↔
    star x = x
rw₃ rw₄ : star x = x ↔ star x = x
⊢ IsSelfAdjoint (@Invertible.invOf _ MulOne.toMul MulOne.toOne x _) ↔ IsSelfAdjoint x

Tactic:
rw [isSelfAdjoint_iff, isSelfAdjoint_iff, star_invOf, invOf_inj]

Premises used: isSelfAdjoint_iff, invOf_inj, star_invOf
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
a u : R
hu : IsUnit u
⊢ IsSelfAdjoint (u * a * star u) ↔ IsSelfAdjoint a

Tactic:
simp [IsSelfAdjoint, mul_assoc, hu.mul_right_inj, hu.star.mul_left_inj]

Premises used: IsUnit.star, IsSelfAdjoint, mul_assoc, IsUnit.mul_right_inj, IsUnit.mul_left_inj
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
a u : R
hu : IsUnit u
⊢ IsSelfAdjoint (star u * a * u) ↔ IsSelfAdjoint a

Tactic:
simpa using hu.star.isSelfAdjoint_conjugate_iff

Premises used: IsUnit.star, IsUnit.isSelfAdjoint_conjugate_iff
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : StarRing R
n : ℕ
⊢ IsSelfAdjoint.{u_1} (R := R) (↑n : R)

Tactic:
star_natCast _

Premises used: IsSelfAdjoint, star_natCast
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : StarRing R
n : ℕ
inst_2 : n.AtLeastTwo
⊢ IsSelfAdjoint.{u_1} (R := R) (OfNat.ofNat n)

Tactic:
.natCast n

Premises used: IsSelfAdjoint.natCast
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
A : Type u_2
a : A
inst : Semiring A
inst_1 : StarRing A
ha : IsSelfAdjoint a
rw : star a⁻¹ʳ = a⁻¹ʳ
rw₁ : (star a)⁻¹ʳ = a⁻¹ʳ
rw₂ rw₃ : a⁻¹ʳ = a⁻¹ʳ
⊢ IsSelfAdjoint a⁻¹ʳ

Tactic:
rw [isSelfAdjoint_iff, ← Ring.inverse_star, ha.star_eq]

Premises used: Ring.inverse_star, isSelfAdjoint_iff, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
A : Type u_2
a : A
inst : Semiring A
inst_1 : StarRing A
ha : IsUnit a
h : IsSelfAdjoint a⁻¹ʳ
⊢ IsSelfAdjoint a

Tactic:
grind [h.ringInverse]

Premises used: IsSelfAdjoint.ringInverse
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : CommSemigroup R
inst_1 : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x * y)

Tactic:
simp only [isSelfAdjoint_iff, star_mul', hx.star_eq, hy.star_eq]

Premises used: isSelfAdjoint_iff, star_mul', IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
α : Type u_3
inst : CommSemiring α
inst_1 : StarRing α
a : α
ha : IsSelfAdjoint a
⊢ (starRingEnd α : (a : α) → α) a = a

Tactic:
ha.star_eq

Premises used: IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Ring R
inst_1 : StarRing R
z : ℤ
⊢ IsSelfAdjoint.{u_1} (R := R) (↑z : R)

Tactic:
star_intCast _

Premises used: IsSelfAdjoint, star_intCast
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Group R
inst_1 : StarMul R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint x⁻¹

Tactic:
simp only [isSelfAdjoint_iff, star_inv, hx.star_eq]

Premises used: isSelfAdjoint_iff, IsSelfAdjoint.star_eq, star_inv
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Group R
inst_1 : StarMul R
x : R
⊢ IsSelfAdjoint x⁻¹ ↔ IsSelfAdjoint x

Tactic:
simp [isSelfAdjoint_iff]

Premises used: isSelfAdjoint_iff
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Group R
inst_1 : StarMul R
x : R
hx : IsSelfAdjoint x
n : ℤ
⊢ IsSelfAdjoint (x ^ n)

Tactic:
simp only [isSelfAdjoint_iff, star_zpow, hx.star_eq]

Premises used: isSelfAdjoint_iff, star_zpow, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : GroupWithZero R
inst_1 : StarMul R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint x⁻¹

Tactic:
simp only [isSelfAdjoint_iff, star_inv₀, hx.star_eq]

Premises used: isSelfAdjoint_iff, IsSelfAdjoint.star_eq, star_inv₀
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : GroupWithZero R
inst_1 : StarMul R
x : R
⊢ IsSelfAdjoint x⁻¹ ↔ IsSelfAdjoint x

Tactic:
simp [isSelfAdjoint_iff]

Premises used: isSelfAdjoint_iff
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : GroupWithZero R
inst_1 : StarMul R
x : R
hx : IsSelfAdjoint x
n : ℤ
⊢ IsSelfAdjoint (x ^ n)

Tactic:
simp only [isSelfAdjoint_iff, star_zpow₀, hx.star_eq]

Premises used: isSelfAdjoint_iff, star_zpow₀, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : DivisionSemiring R
inst_1 : StarRing R
q : ℚ≥0
⊢ IsSelfAdjoint.{u_1} (R := R) (↑q : R)

Tactic:
star_nnratCast _

Premises used: IsSelfAdjoint, star_nnratCast
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : StarRing R
x : ℚ
⊢ IsSelfAdjoint.{u_1} (R := R) (↑x : R)

Tactic:
star_ratCast _

Premises used: IsSelfAdjoint, star_ratCast
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Semifield R
inst_1 : StarRing R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x / y)

Tactic:
simp only [isSelfAdjoint_iff, star_div₀, hx.star_eq, hy.star_eq]

Premises used: isSelfAdjoint_iff, star_div₀, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Star R
inst_1 : Star A
inst_2 : SMul R A
inst_3 : StarModule R A
r : R
hr : IsSelfAdjoint r
x : A
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (r • x)

Tactic:
simp only [isSelfAdjoint_iff, star_smul, hr.star_eq, hx.star_eq]

Premises used: StarModule.star_smul, isSelfAdjoint_iff, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : StarMul R
inst_2 : Star A
inst_3 : MulAction R A
inst_4 : StarModule R A
r : R
hr : IsSelfAdjoint r
hu : IsUnit r
x : A
⊢ IsSelfAdjoint (r • x) ↔ IsSelfAdjoint x

Tactic:
⟨fun hrx ↦ ?_, .smul hr⟩

Premises used: Iff.intro, IsSelfAdjoint.smul
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : StarMul R
inst_2 : Star A
inst_3 : MulAction R A
inst_4 : StarModule R A
r : R
hr : IsSelfAdjoint r
hu : IsUnit r
x : A
refine : ∀ (hrx : IsSelfAdjoint (r • x)), IsSelfAdjoint x
⊢ IsSelfAdjoint (r • x) ↔ IsSelfAdjoint x

Tactic:
refine ⟨fun hrx ↦ ?_, .smul hr⟩
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : StarMul R
inst_2 : Star A
inst_3 : MulAction R A
inst_4 : StarModule R A
r : R
hr : IsSelfAdjoint r
hu : IsUnit r
x : A
hrx : IsSelfAdjoint (r • x)
⊢ IsUnit r

Tactic:
hu
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : StarMul R
inst_2 : Star A
inst_3 : MulAction R A
inst_4 : StarModule R A
r : R
hr : IsSelfAdjoint r
hu : IsUnit r
x : A
hrx : IsSelfAdjoint (r • x)
lift : ∀ (r : Rˣ) (hr : IsSelfAdjoint (↑r : R)) (hrx : IsSelfAdjoint ((↑r : R) • x)), IsSelfAdjoint x
⊢ IsSelfAdjoint x

Tactic:
lift r to Rˣ using hu
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : StarMul R
inst_2 : Star A
inst_3 : MulAction R A
inst_4 : StarModule R A
x : A
r : Rˣ
hr : IsSelfAdjoint (↑r : R)
hrx : IsSelfAdjoint ((↑r : R) • x)
rw : IsSelfAdjoint (r⁻¹ • r • x)
⊢ IsSelfAdjoint x

Tactic:
rw [← inv_smul_smul r x]

Premises used: inv_smul_smul
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : StarMul R
inst_2 : Star A
inst_3 : MulAction R A
inst_4 : StarModule R A
x : A
r : Rˣ
hr : IsSelfAdjoint (↑r : R)
hrx : IsSelfAdjoint ((↑r : R) • x)
⊢ IsSelfAdjoint r

Tactic:
replace hr : IsSelfAdjoint r := Units.ext hr.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : StarMul R
inst_2 : Star A
inst_3 : MulAction R A
inst_4 : StarModule R A
x : A
r : Rˣ
hrx : IsSelfAdjoint ((↑r : R) • x)
hr : IsSelfAdjoint r
⊢ IsSelfAdjoint (r⁻¹ • r • x)

Tactic:
hr.inv.smul hrx

Premises used: IsSelfAdjoint.inv, IsSelfAdjoint.smul
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : StarMul R
inst_2 : Star A
inst_3 : MulAction R A
inst_4 : StarModule R A
x : A
r : Rˣ
hrx : IsSelfAdjoint ((↑r : R) • x)
hr : IsSelfAdjoint r
⊢ IsSelfAdjoint (r⁻¹ • r • x)

Tactic:
exact hr.inv.smul hrx

Premises used: IsSelfAdjoint.inv, IsSelfAdjoint.smul
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : AddCommGroup R
inst_1 : StarAddMonoid R
x y : R
hx : star x = -x
hy : star y = -y
rw : star x + star y = -(x + y)
rw₁ : -x + star y = -(x + y)
rw₂ : -x + -y = -(x + y)
rw₃ rw₄ : -x + -y = -x + -y
⊢ star (x + y) = -(x + y)

Tactic:
rw [star_add x y, hx, hy, neg_add]

Premises used: StarAddMonoid.star_add, neg_add
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : AddCommGroup R
inst_1 : StarAddMonoid R
⊢ Eq.{u_1 + 1} (α := R) (star 0) (-0)

Tactic:
simp only [star_zero, neg_zero]

Premises used: star_zero, neg_zero
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : AddCommGroup R
inst_1 : StarAddMonoid R
x : R
hx : star x = -x
⊢ star (-x) = - -x

Tactic:
simp only [hx, star_neg]

Premises used: star_neg
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : StarAddMonoid R
x : R
⊢ x ∈ AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (selfAdjoint R))) ↔ star x = x

Tactic:
Iff.rfl

Premises used: IsSelfAdjoint, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : StarAddMonoid R
x : R
⊢ x ∈ AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (selfAdjoint R))) ↔ star x = x

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : StarAddMonoid R
x : ↥(selfAdjoint R)
⊢ star (↑x : R) = (↑x : R)

Tactic:
x.prop

Premises used: IsSelfAdjoint, Set.Mem, setOf, Subtype.prop
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : StarAddMonoid R
x : ↥(selfAdjoint R)
⊢ IsSelfAdjoint (↑x : R)

Tactic:
simp [isSelfAdjoint_iff]

Premises used: isSelfAdjoint_iff
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : NonUnitalRing R
inst_1 : StarRing R
x : ↥(selfAdjoint R)
⊢ IsStarNormal (↑x : R)

Tactic:
x.prop.isStarNormal

Premises used: IsSelfAdjoint.isStarNormal, Subtype.prop
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Ring R
inst_1 : StarRing R
⊢ Eq.{u_1 + 1} (α := R) (↑1 : R) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Ring R
inst_1 : StarRing R
inst_2 : Nontrivial R
⊢ Nontrivial.{u_1} ↥(selfAdjoint R)

Tactic:
⟨⟨0, 1, ne_of_apply_ne Subtype.val zero_ne_one⟩⟩

Premises used: zero_ne_one, Nontrivial.mk, ne_of_apply_ne, Exists.intro, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Ring R
inst_1 : StarRing R
x : ↥(selfAdjoint R)
n : ℕ
⊢ (↑(x ^ n) : R) = (↑x : R) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : NonUnitalCommRing R
inst_1 : StarRing R
x y : ↥(selfAdjoint R)
⊢ (↑(x * y) : R) = (↑x : R) * (↑y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : StarRing R
n : ℕ
x : ↥(selfAdjoint R)
⊢ (↑(n • x) : R) = n • (↑x : R)

Tactic:
rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : StarRing R
n : ℤ
x : ↥(selfAdjoint R)
⊢ (↑(n • x) : R) = n • (↑x : R)

Tactic:
rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Field R
inst_1 : StarRing R
x : ↥(selfAdjoint R)
⊢ (↑x⁻¹ : R) = (↑x : R)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Field R
inst_1 : StarRing R
x y : ↥(selfAdjoint R)
⊢ (↑(x / y) : R) = (↑x : R) / (↑y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Field R
inst_1 : StarRing R
x : ↥(selfAdjoint R)
z : ℤ
⊢ (↑(x ^ z) : R) = (↑x : R) ^ z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Field R
inst_1 : StarRing R
q : ℚ≥0
⊢ Eq.{u_1 + 1} (α := R) (↑(↑q : ↥(selfAdjoint R)) : R) (↑q : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Field R
inst_1 : StarRing R
q : ℚ
⊢ Eq.{u_1 + 1} (α := R) (↑(↑q : ↥(selfAdjoint R)) : R) (↑q : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Field R
inst_1 : StarRing R
a : ℚ≥0
x : ↥(selfAdjoint R)
rw : Membership.mem (γ := AddSubgroup R) (selfAdjoint R) ((↑a : R) * (↑x : R))
⊢ Membership.mem (γ := AddSubgroup R) (selfAdjoint R) (a • (↑x : R))

Tactic:
rw [NNRat.smul_def]

Premises used: NNRat.smul_def
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Field R
inst_1 : StarRing R
a : ℚ≥0
x : ↥(selfAdjoint R)
⊢ Membership.mem (γ := AddSubgroup R) (selfAdjoint R) ((↑a : R) * (↑x : R))

Tactic:
.mul (.nnratCast a) x.prop

Premises used: IsSelfAdjoint, Set.Mem, setOf, Subtype.prop, IsSelfAdjoint.nnratCast, IsSelfAdjoint.mul
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Field R
inst_1 : StarRing R
a : ℚ≥0
x : ↥(selfAdjoint R)
⊢ Membership.mem (γ := AddSubgroup R) (selfAdjoint R) ((↑a : R) * (↑x : R))

Tactic:
exact .mul (.nnratCast a) x.prop
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Field R
inst_1 : StarRing R
a : ℚ
x : ↥(selfAdjoint R)
rw : Membership.mem (γ := AddSubgroup R) (selfAdjoint R) ((↑a : R) * (↑x : R))
⊢ Membership.mem (γ := AddSubgroup R) (selfAdjoint R) (a • (↑x : R))

Tactic:
rw [Rat.smul_def]

Premises used: Rat.smul_def
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Field R
inst_1 : StarRing R
a : ℚ
x : ↥(selfAdjoint R)
⊢ Membership.mem (γ := AddSubgroup R) (selfAdjoint R) ((↑a : R) * (↑x : R))

Tactic:
.mul (.ratCast a) x.prop

Premises used: IsSelfAdjoint, Set.Mem, setOf, IsSelfAdjoint.ratCast, Subtype.prop, IsSelfAdjoint.mul
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Field R
inst_1 : StarRing R
a : ℚ
x : ↥(selfAdjoint R)
⊢ Membership.mem (γ := AddSubgroup R) (selfAdjoint R) ((↑a : R) * (↑x : R))

Tactic:
exact .mul (.ratCast a) x.prop
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Field R
inst_1 : StarRing R
q : ℚ≥0
x : ↥(selfAdjoint R)
⊢ (↑(q • x) : R) = q • (↑x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Field R
inst_1 : StarRing R
q : ℚ
x : ↥(selfAdjoint R)
⊢ (↑(q • x) : R) = q • (↑x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Field R
inst_1 : StarRing R
n : ℤ
x : ↥(selfAdjoint R)
⊢ (↑(n • x) : R) = n • (↑x : R)

Tactic:
rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Star R
inst_1 : TrivialStar R
inst_2 : AddGroup A
inst_3 : StarAddMonoid A
inst_4 : SMul R A
inst_5 : StarModule R A
r : R
x : ↥(selfAdjoint A)
⊢ (↑(r • x) : A) = r • (↑x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : StarAddMonoid R
x : R
⊢ x ∈ AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (skewAdjoint R))) ↔
    star x = -x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : StarAddMonoid R
x : R
⊢ x ∈ AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (skewAdjoint R))) ↔
    star x = -x

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : StarAddMonoid R
x : ↥(skewAdjoint R)
⊢ star (↑x : R) = -(↑x : R)

Tactic:
x.prop

Premises used: Set.Mem, setOf, Subtype.prop
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Ring R
inst_1 : StarRing R
x : R
hx : Membership.mem (γ := AddSubgroup R) (skewAdjoint R) x
z : R
⊢ Membership.mem (γ := AddSubgroup R) (skewAdjoint R) (z * x * star z)

Tactic:
simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, neg_mul, mul_neg, mul_assoc]

Premises used: star_star, skewAdjoint.mem_iff, mul_assoc, Iff.mp, StarMul.star_mul, neg_mul, mul_neg
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Ring R
inst_1 : StarRing R
x : R
hx : Membership.mem (γ := AddSubgroup R) (skewAdjoint R) x
z : R
⊢ Membership.mem (γ := AddSubgroup R) (skewAdjoint R) (star z * x * z)

Tactic:
simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, neg_mul, mul_neg, mul_assoc]

Premises used: star_star, skewAdjoint.mem_iff, mul_assoc, Iff.mp, StarMul.star_mul, neg_mul, mul_neg
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Ring R
inst_1 : StarRing R
x : R
hx : Membership.mem (γ := AddSubgroup R) (skewAdjoint R) x
⊢ star x = -x

Tactic:
simp only [mem_iff] at hx

Premises used: skewAdjoint.mem_iff
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Ring R
inst_1 : StarRing R
x : R
hx : star x = -x
⊢ Commute (star x) x

Tactic:
simp only [hx, Commute.neg_left, Commute.refl]

Premises used: Commute.neg_left, Commute.refl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Ring R
inst_1 : StarRing R
x : ↥(skewAdjoint R)
⊢ IsStarNormal (↑x : R)

Tactic:
isStarNormal_of_mem (SetLike.coe_mem _)

Premises used: skewAdjoint.isStarNormal_of_mem, SetLike.coe_mem
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Star R
inst_1 : TrivialStar R
inst_2 : AddCommGroup A
inst_3 : StarAddMonoid A
inst_4 : Monoid R
inst_5 : DistribMulAction R A
inst_6 : StarModule R A
r : R
x : A
h : Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x
rw : star (r • x) = -(r • x)
rw₁ : star r • star x = -(r • x)
rw₂ : r • star x = -(r • x)
rw₃ : r • -x = -(r • x)
rw₄ rw₅ : -(r • x) = -(r • x)
⊢ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) (r • x)

Tactic:
rw [mem_iff, star_smul, star_trivial, mem_iff.mp h, smul_neg r]

Premises used: skewAdjoint.mem_iff, StarModule.star_smul, TrivialStar.star_trivial, smul_neg, Iff.mp
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Star R
inst_1 : TrivialStar R
inst_2 : AddCommGroup A
inst_3 : StarAddMonoid A
inst_4 : Monoid R
inst_5 : DistribMulAction R A
inst_6 : StarModule R A
r : R
x : ↥(skewAdjoint A)
⊢ (↑(r • x) : A) = r • (↑x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Ring R
inst_1 : AddCommGroup A
inst_2 : Module R A
inst_3 : StarAddMonoid R
inst_4 : StarAddMonoid A
inst_5 : StarModule R A
r : R
hr : Membership.mem (γ := AddSubgroup R) (skewAdjoint R) r
a : A
ha : IsSelfAdjoint a
⊢ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) (r • a)

Tactic:
(star_smul _ _).trans <| (congr_arg₂ _ hr ha).trans <| neg_smul _ _

Premises used: neg_smul, Set.Mem, StarModule.star_smul, setOf, Eq.trans, congr_arg₂
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Ring R
inst_1 : AddCommGroup A
inst_2 : Module R A
inst_3 : StarAddMonoid R
inst_4 : StarAddMonoid A
inst_5 : StarModule R A
r : R
hr : Membership.mem (γ := AddSubgroup R) (skewAdjoint R) r
a : A
ha : Membership.mem (γ := AddSubgroup A) (skewAdjoint A) a
⊢ IsSelfAdjoint (r • a)

Tactic:
(star_smul _ _).trans <| (congr_arg₂ _ hr ha).trans <| neg_smul_neg _ _

Premises used: IsSelfAdjoint, neg_smul_neg, StarModule.star_smul, Eq.trans, congr_arg₂
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : StarAddMonoid R
⊢ Commute.{u_1} (S := R) (star 0) 0

Tactic:
simp only [Commute.refl, star_zero]

Premises used: Commute.refl, star_zero
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : MulOneClass R
inst_1 : StarMul R
⊢ Commute.{u_1} (S := R) (star 1) 1

Tactic:
simp only [Commute.refl, star_one]

Premises used: Commute.refl, star_one
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Mul R
inst_1 : StarMul R
x : R
inst_2 : IsStarNormal x
rw : x * star x = star x * x
rw₁ rw₂ : x * star x = x * star x
⊢ star (star x) * star x = star x * star (star x)

Tactic:
rw [star_star, star_comm_self']

Premises used: star_comm_self', star_star
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : StarAddMonoid R
x : R
inst_2 : IsStarNormal x
simp_rw : -star x * -x = -x * -star x
simp_rw₁ : star x * x = x * star x
⊢ star (-x) * -x = -x * star (-x)

Tactic:
simp_rw [star_neg, neg_mul_neg, star_comm_self']

Premises used: star_comm_self', star_neg, neg_mul_neg
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : StarMul R
x : Rˣ
inst_2 : IsStarNormal (↑x : R)
⊢ Commute (star (↑x⁻¹ : R)) (↑x⁻¹ : R)

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

Premises used: IsStarNormal.star_comm_self, Commute.units_val_iff, Units.coe_star_inv