awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
⊢ SpectrumRestricts a f ↔
    Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (spectrum S a) ∧
      Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)

Tactic:
⟨fun h ↦ ⟨h.rightInvOn, h.left_inv⟩, fun h ↦ .of_rightInvOn h.2 h.1⟩

Premises used: And.right, And.left, And.intro, Iff.intro, SpectrumRestricts.of_rightInvOn, SpectrumRestricts.rightInvOn, QuasispectrumRestricts.left_inv
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
hf : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h : spectrum S a ⊆ Set.range.{u_4, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)
s : S
hs : s ∈ quasispectrum S a
⊢ s = 0 ∨ s ∈ spectrum S a

Tactic:
rw [mem_quasispectrum_iff] at hs

Premises used: mem_quasispectrum_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
hf : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h : spectrum S a ⊆ Set.range.{u_4, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)
s : S
hs : s = 0 ∨ s ∈ spectrum S a
inl : Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) (f 0) : S) (0 : S)
inr : ∀ (hs : s ∈ spectrum S a), (algebraMap R S : (a : R) → S) (f s) = s
⊢ (algebraMap R S : (a : R) → S) (f s) = s

Tactic:
obtain (rfl | hs) := hs

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
hf : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h : spectrum S a ⊆ Set.range.{u_4, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)
⊢ Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) (f 0) : S) (0 : S)

Tactic:
simpa using hf 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
hf : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h : spectrum S a ⊆ Set.range.{u_4, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)
s : S
hs : s ∈ spectrum S a
inr :
  ∀ (r : R) (hs : Membership.mem (α := S) (spectrum S a) ((algebraMap R S : (a : R) → S) r : S)),
    Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) (f ((algebraMap R S : (a : R) → S) r)) : S)
      ((algebraMap R S : (a : R) → S) r : S)
⊢ (algebraMap R S : (a : R) → S) (f s) = s

Tactic:
obtain ⟨r, rfl⟩ := h hs

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
hf : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h : spectrum S a ⊆ Set.range.{u_4, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)
r : R
hs : Membership.mem (α := S) (spectrum S a) ((algebraMap R S : (a : R) → S) r : S)
inr inr₁ : Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap R S : (a : R) → S) r : S)
⊢ Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) (f ((algebraMap R S : (a : R) → S) r)) : S)
    ((algebraMap R S : (a : R) → S) r : S)

Tactic:
rw [hf r]
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a b : A
f : S → R
ha : SpectrumRestricts a f
h : spectrum S a = spectrum S b
rw : Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a)
⊢ Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S b)

Tactic:
rw [quasispectrum_eq_spectrum_union_zero, ← h, ← quasispectrum_eq_spectrum_union_zero]

Premises used: quasispectrum_eq_spectrum_union_zero
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a b : A
f : S → R
ha : SpectrumRestricts a f
h : spectrum S a = spectrum S b
⊢ Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a)

Tactic:
QuasispectrumRestricts.rightInvOn ha

Premises used: QuasispectrumRestricts.rightInvOn
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a b : A
f : S → R
ha : SpectrumRestricts a f
h : spectrum S a = spectrum S b
⊢ Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a)

Tactic:
exact QuasispectrumRestricts.rightInvOn ha

Premises used: QuasispectrumRestricts.rightInvOn
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_6
S : Type u_7
A : Type u_8
inst : Semifield R
inst_1 : Field S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a b : A
f : S → R
⊢ SpectrumRestricts (a * b) f ↔ SpectrumRestricts (b * a) f

Tactic:
QuasispectrumRestricts.mul_comm_iff

Premises used: QuasispectrumRestricts.mul_comm_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
inst_6 : IsScalarTower R S A
h : SpectrumRestricts a f
⊢ (⇑(algebraMap R S) : (a : R) → S) '' spectrum R a = spectrum S a

Tactic:
Set.eq_of_subset_of_subset ?_ fun s hs => ⟨f s, ?_⟩

Premises used: Exists.intro, Set.eq_of_subset_of_subset
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
inst_6 : IsScalarTower R S A
h : SpectrumRestricts a f
refine_1 : (⇑(algebraMap R S) : (a : R) → S) '' spectrum R a ⊆ spectrum S a
refine_2 : ∀ (s : S) (hs : s ∈ spectrum S a), f s ∈ spectrum R a ∧ (algebraMap R S : (a : R) → S) (f s) = s
⊢ (⇑(algebraMap R S) : (a : R) → S) '' spectrum R a = spectrum S a

Tactic:
refine Set.eq_of_subset_of_subset ?_ fun s hs => ⟨f s, ?_⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
inst_6 : IsScalarTower R S A
h : SpectrumRestricts a f
⊢ (⇑(algebraMap R S) : (a : R) → S) '' spectrum R a ⊆ spectrum S a

Tactic:
simpa only [spectrum.preimage_algebraMap] using
      (spectrum S a).image_preimage_subset (algebraMap R S)

Premises used: Algebra.algebraMap, spectrum, spectrum.preimage_algebraMap, Set.image_preimage_subset, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
inst_6 : IsScalarTower R S A
h : SpectrumRestricts a f
s : S
hs : s ∈ spectrum S a
⊢ f s ∈ spectrum R a ∧ (algebraMap R S : (a : R) → S) (f s) = s

Tactic:
⟨spectrum.of_algebraMap_mem S ((h.rightInvOn hs).symm ▸ hs), h.rightInvOn hs⟩

Premises used: And.intro, SpectrumRestricts.rightInvOn, spectrum.of_algebraMap_mem
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
inst_6 : IsScalarTower R S A
h : SpectrumRestricts a f
s : S
hs : s ∈ spectrum S a
⊢ f s ∈ spectrum R a ∧ (algebraMap R S : (a : R) → S) (f s) = s

Tactic:
exact ⟨spectrum.of_algebraMap_mem S ((h.rightInvOn hs).symm ▸ hs), h.rightInvOn hs⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
inst_6 : IsScalarTower R S A
h : SpectrumRestricts a f
⊢ f '' spectrum S a = spectrum R a

Tactic:
simp only [← h.algebraMap_image, Set.image_image, h.left_inv _, Set.image_id']

Premises used: Set.image_image, Set.image_id', SpectrumRestricts.algebraMap_image, QuasispectrumRestricts.left_inv
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
inst_6 : IsScalarTower R S A
h : SpectrumRestricts a f
s : S
hs : s ∈ spectrum S a
⊢ f s ∈ spectrum R a

Tactic:
h.image ▸ ⟨s, hs, rfl⟩

Premises used: Eq.rec, And.intro, SpectrumRestricts.image, Exists.intro, rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
inst_6 : IsScalarTower R S A
h : SpectrumRestricts a f
⊢ spectrum S a ⊆ f ⁻¹' spectrum R a

Tactic:
h.image ▸ (spectrum S a).subset_preimage_image f

Premises used: spectrum, Eq.rec, SpectrumRestricts.image, Set.subset_preimage_image
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
S : Type u_3
R : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Algebra R S
inst_4 : Module R A
inst_5 : Module S A
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
a : A
f : S → R
rw :
  Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a) ∧
      Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S) ↔
    SpectrumRestricts (A := Unitization S A) (↑a : Unitization S A) f
rw₁ :
  Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a) ∧
      Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S) ↔
    Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (spectrum S (A := Unitization S A) (↑a : Unitization S A)) ∧
      Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
rw₂ rw₃ :
  Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a) ∧
      Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S) ↔
    Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a) ∧
      Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
⊢ QuasispectrumRestricts a f ↔ SpectrumRestricts (A := Unitization S A) (↑a : Unitization S A) f

Tactic:
rw [quasispectrumRestricts_iff, spectrumRestricts_iff,
    ← Unitization.quasispectrum_eq_spectrum_inr']

Premises used: spectrumRestricts_iff, quasispectrumRestricts_iff, Unitization.quasispectrum_eq_spectrum_inr'
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S' : Type u_4
A : Type u_5
S : Type u_6
inst : Semifield R
inst_1 : Semifield S'
inst_2 : Field S
inst_3 : NonUnitalRing A
inst_4 : Module R A
inst_5 : Module S' A
inst_6 : Module S A
inst_7 : IsScalarTower S A A
inst_8 : SMulCommClass S A A
inst_9 : Algebra R S'
inst_10 : Algebra S' S
inst_11 : Algebra R S
inst_12 : IsScalarTower S' S A
inst_13 : IsScalarTower R S A
a : A
f : S' → R
⊢ QuasispectrumRestricts a f ↔ SpectrumRestricts (A := Unitization S A) (↑a : Unitization S A) f

Tactic:
simp only [quasispectrumRestricts_iff, SpectrumRestricts, Unitization.quasispectrum_inr_eq]

Premises used: quasispectrumRestricts_iff, Unitization.quasispectrum_inr_eq, SpectrumRestricts
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
⊢ QuasispectrumRestricts a f ↔ SpectrumRestricts a f

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : LE A
inst_1 : Monoid A
inst_2 : Zero A
a : A
⊢ IsStrictlyPositive a ↔ 0 ≤ a ∧ IsUnit a

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsStrictlyPositive
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : LE A
inst_1 : Monoid A
inst_2 : Zero A
a : A
ha : IsStrictlyPositive a
⊢ 0 ≤ a

Tactic:
ha.1

Premises used: And.left
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : LE A
inst_1 : Monoid A
inst_2 : Zero A
a : A
ha : IsStrictlyPositive a
⊢ IsUnit a

Tactic:
ha.2

Premises used: And.right
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : LE A
inst_1 : Monoid A
inst_2 : Zero A
a : A
ha : IsUnit a
ha₀ : 0 ≤ a
⊢ IsStrictlyPositive a

Tactic:
iff_of_unital.mpr ⟨ha₀, ha⟩

Premises used: Iff.mpr, IsStrictlyPositive.iff_of_unital, And.intro
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : Semiring A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ IsSelfAdjoint a

Tactic:
ha.nonneg.isSelfAdjoint

Premises used: LE.le.isSelfAdjoint, IsStrictlyPositive.nonneg
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : LE A
inst_1 : Monoid A
inst_2 : Zero A
inst_3 : ZeroLEOneClass A
⊢ IsStrictlyPositive.{u_1} (A := A) 1

Tactic:
iff_of_unital.mpr ⟨zero_le_one, isUnit_one⟩

Premises used: Iff.mpr, zero_le_one, IsStrictlyPositive.iff_of_unital, isUnit_one, And.intro
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : LE A
inst_1 : Monoid A
inst_2 : Zero A
a : Aˣ
⊢ IsStrictlyPositive (↑a : A) ↔ 0 ≤ (↑a : A)

Tactic:
⟨fun h => h.nonneg, fun h => iff_of_unital.mp ⟨h, a.isUnit⟩⟩

Premises used: IsStrictlyPositive.iff_of_unital, And.intro, Iff.intro, Iff.mp, Units.isUnit, IsStrictlyPositive.nonneg
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : LE A
inst_1 : Monoid A
inst_2 : Zero A
a : Aˣ
h : 0 ≤ (↑a : A)
⊢ IsStrictlyPositive (↑a : A)

Tactic:
a.isStrictlyPositive_iff.mpr h

Premises used: Iff.mpr, Units.isStrictlyPositive_iff
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Monoid A
inst_2 : Zero A
inst_3 : Subsingleton A
a : A
⊢ 0 ≤ a

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : Semiring A
inst_1 : StarRing A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
u a : A
hu : IsUnit u
simp_rw : 0 ≤ a ∧ IsUnit (u * a * star u) ↔ 0 ≤ a ∧ IsUnit a
⊢ IsStrictlyPositive (u * a * star u) ↔ IsStrictlyPositive a

Tactic:
simp_rw [IsStrictlyPositive.iff_of_unital, hu.star_right_conjugate_nonneg_iff]

Premises used: IsUnit.star_right_conjugate_nonneg_iff, IsStrictlyPositive.iff_of_unital
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : Semiring A
inst_1 : StarRing A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
u a : A
hu : IsUnit u
⊢ IsUnit u

Tactic:
hu
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : Semiring A
inst_1 : StarRing A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
u a : A
hu : IsUnit u
lift : ∀ (u : Aˣ), 0 ≤ a ∧ IsUnit ((↑u : A) * a * star (↑u : A)) ↔ 0 ≤ a ∧ IsUnit a
⊢ 0 ≤ a ∧ IsUnit (u * a * star u) ↔ 0 ≤ a ∧ IsUnit a

Tactic:
lift u to Aˣ using hu
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : Semiring A
inst_1 : StarRing A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
a : A
u : Aˣ
rw : 0 ≤ a ∧ IsUnit ((↑u : A) * a * (↑(star u) : A)) ↔ 0 ≤ a ∧ IsUnit a
rw₁ : 0 ≤ a ∧ IsUnit ((↑u : A) * a) ↔ 0 ≤ a ∧ IsUnit a
rw₂ rw₃ : 0 ≤ a ∧ IsUnit a ↔ 0 ≤ a ∧ IsUnit a
⊢ 0 ≤ a ∧ IsUnit ((↑u : A) * a * star (↑u : A)) ↔ 0 ≤ a ∧ IsUnit a

Tactic:
rw [← Units.coe_star, Units.isUnit_mul_units, Units.isUnit_units_mul]

Premises used: Units.coe_star, Units.isUnit_mul_units, Units.isUnit_units_mul
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : Semiring A
inst_1 : StarRing A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
u a : A
hu : IsUnit u
⊢ IsStrictlyPositive (star u * a * u) ↔ IsStrictlyPositive a

Tactic:
simpa using hu.star.isStrictlyPositive_star_right_conjugate_iff

Premises used: IsUnit.star, IsUnit.isStrictlyPositive_star_right_conjugate_iff
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : Semiring A
inst_1 : StarRing A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
a b : A
hb : IsUnit b
hb₂ : IsSelfAdjoint b
⊢ IsStrictlyPositive (b * a * b) ↔ IsStrictlyPositive a

Tactic:
grind [hb.isStrictlyPositive_star_left_conjugate_iff]

Premises used: IsUnit.isStrictlyPositive_star_left_conjugate_iff
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
inst : Semiring A
inst_1 : StarRing A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
a b : A
hb : IsUnit b
hb₂ : IsSelfAdjoint b
ha : IsStrictlyPositive a
⊢ IsStrictlyPositive (b * a * b)

Tactic:
(hb.isStrictlyPositive_iff_conjugate_of_isSelfAdjoint _ _ hb₂).mpr ha

Premises used: Iff.mpr, IsUnit.isStrictlyPositive_iff_conjugate_of_isSelfAdjoint
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : Semifield 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : Algebra 𝕜 A
inst_5 : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
a : A
ha : IsStrictlyPositive a
⊢ c • a * c⁻¹ • (↑⋯.unit⁻¹ : A) = 1 ∧ c⁻¹ • (↑⋯.unit⁻¹ : A) * c • a = 1

Tactic:
simp [(ne_of_lt hc).symm]

Premises used: Ne.symm, ne_of_lt
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : Semifield 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : Algebra 𝕜 A
inst_5 : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
a : A
ha : IsStrictlyPositive a
⊢ IsUnit (c • a)

Tactic:
have hunit : IsUnit (c • a) :=
    isUnit_iff_exists.mpr ⟨c⁻¹ • ha.isUnit.unit⁻¹, by simp [(ne_of_lt hc).symm]⟩
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : Semifield 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : Algebra 𝕜 A
inst_5 : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
a : A
ha : IsStrictlyPositive a
hunit : IsUnit (c • a)
⊢ IsStrictlyPositive (c • a)

Tactic:
hunit.isStrictlyPositive (smul_nonneg hc.le ha.nonneg)

Premises used: smul_nonneg, LT.lt.le, IsUnit.isStrictlyPositive, IsStrictlyPositive.nonneg
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : Semifield 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : Algebra 𝕜 A
inst_5 : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
a : A
ha : IsStrictlyPositive a
hunit : IsUnit (c • a)
⊢ IsStrictlyPositive (c • a)

Tactic:
exact hunit.isStrictlyPositive (smul_nonneg hc.le ha.nonneg)

Premises used: smul_nonneg, LT.lt.le, IsUnit.isStrictlyPositive, IsStrictlyPositive.nonneg
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : ZeroLEOneClass A
inst_3 : Semifield 𝕜
inst_4 : PartialOrder 𝕜
inst_5 : Algebra 𝕜 A
inst_6 : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
rw : IsStrictlyPositive (HSMul.hSMul (β := A) c 1)
⊢ IsStrictlyPositive.{u_1} (A := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) c : A)

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : ZeroLEOneClass A
inst_3 : Semifield 𝕜
inst_4 : PartialOrder 𝕜
inst_5 : Algebra 𝕜 A
inst_6 : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
⊢ IsStrictlyPositive (HSMul.hSMul (β := A) c 1)

Tactic:
IsStrictlyPositive.smul hc isStrictlyPositive_one

Premises used: isStrictlyPositive_one, IsStrictlyPositive.smul
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : ZeroLEOneClass A
inst_3 : Semifield 𝕜
inst_4 : PartialOrder 𝕜
inst_5 : Algebra 𝕜 A
inst_6 : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
⊢ IsStrictlyPositive (HSMul.hSMul (β := A) c 1)

Tactic:
exact IsStrictlyPositive.smul hc isStrictlyPositive_one

Premises used: isStrictlyPositive_one, IsStrictlyPositive.smul
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : CommSemiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : Algebra 𝕜 A
inst_5 : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
⊢ 0 ≤ x

Tactic:
grind
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : CommSemiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : Algebra 𝕜 A
inst_5 : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
⊢ 0 ≤ x

Tactic:
have h₁ : 0 ≤ x := by grind
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : CommSemiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : Algebra 𝕜 A
inst_5 : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
h₁ : 0 ≤ x
⊢ x ≠ 0

Tactic:
grind [= spectrum.zero_notMem_iff]

Premises used: spectrum.zero_notMem_iff
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : CommSemiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : Algebra 𝕜 A
inst_5 : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
h₁ : 0 ≤ x
⊢ x ≠ 0

Tactic:
have h₂ : x ≠ 0 := by grind [= spectrum.zero_notMem_iff]
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : CommSemiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : Algebra 𝕜 A
inst_5 : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
h₁ : 0 ≤ x
h₂ : x ≠ 0
⊢ 0 < x

Tactic:
lt_of_le_of_ne h₁ h₂.symm

Premises used: Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Algebra.StrictPositivity
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : CommSemiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : Algebra 𝕜 A
inst_5 : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
h₁ : 0 ≤ x
h₂ : x ≠ 0
⊢ 0 < x

Tactic:
exact lt_of_le_of_ne h₁ h₂.symm

Premises used: Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
carrier : Set A
mul_mem' : ∀ {a b : A}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
toSubsemigroup : Subsemigroup A := { carrier := carrier, mul_mem' := @mul_mem' }
one_mem' : 1 ∈ carrier
toSubmonoid : Submonoid A := { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' }
add_mem' : ∀ {a b : A}, a ∈ carrier → b ∈ carrier → a + b ∈ carrier
toAddSubsemigroup : AddSubsemigroup A := { carrier := carrier, add_mem' := @add_mem' }
algebraMap_mem' : ∀ (r : R), Membership.mem (α := A) carrier ((algebraMap R A : (a : R) → A) r : A)
⊢ 0 ∈ carrier

Tactic:
(algebraMap R A).map_zero ▸ algebraMap_mem' 0

Premises used: Algebra.algebraMap, Set.Mem, Eq.rec, RingHom.map_zero, OfNat.ofNat