awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a : R
ha : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ Star.star s * s)) a
c x y : R
h : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ Star.star s * s)) x
h_1 : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ Star.star s * s)) y
hx : 0 ≤ Star.star c * x * c
hy : 0 ≤ Star.star c * y * c
star : 0 ≤ Star.star c * x * c + 0
star₁ : Star.star c * x * c + 0 ≤ Star.star c * x * c + Star.star c * y * c
star₂ : Star.star c * x * c + Star.star c * y * c ≤ Star.star c * (x + y) * c
⊢ 0 ≤ Star.star c * (x + y) * c

Tactic:
calc
      0 ≤ star c * x * c + 0 := by rw [add_zero]; exact hx
      _ ≤ star c * x * c + star c * y * c := by gcongr
      _ ≤ _ := by rw [mul_add, add_mul]

Premises used: Star.star
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
⊢ 0 ≤ c * a * star c

Tactic:
simpa only [star_star] using star_left_conjugate_nonneg ha (star c)

Premises used: star_star, star_left_conjugate_nonneg, Star.star
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
hc : IsSelfAdjoint c
nth_rewrite : 0 ≤ c * a * star c
⊢ 0 ≤ c * a * c

Tactic:
nth_rewrite 2 [← hc]
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
hc : IsSelfAdjoint c
⊢ 0 ≤ c * a * star c

Tactic:
star_right_conjugate_nonneg ha c

Premises used: star_right_conjugate_nonneg
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
hc : IsSelfAdjoint c
⊢ 0 ≤ c * a * star c

Tactic:
exact star_right_conjugate_nonneg ha c

Premises used: star_right_conjugate_nonneg
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
hc : 0 ≤ c
⊢ 0 ≤ c * a * c

Tactic:
IsSelfAdjoint.of_nonneg hc |>.conjugate_nonneg ha

Premises used: IsSelfAdjoint.conjugate_nonneg, IsSelfAdjoint.of_nonneg
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
rw :
  ∀
    (hab :
      ∃ (p : R),
        Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ b = a + p)
    (c : R),
    ∃ (p : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧
        star c * b * c = star c * a * c + p
⊢ star c * a * c ≤ star c * b * c

Tactic:
rw [StarOrderedRing.le_iff] at hab ⊢

Premises used: StarOrderedRing.le_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a b : R
hab :
  ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ b = a + p
c : R
obtain :
  ∀ (p : R) (hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p),
    ∃ (p_1 : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p_1 ∧
        star c * (a + p) * c = star c * a * c + p_1
⊢ ∃ (p : R),
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧
      star c * b * c = star c * a * c + p

Tactic:
obtain ⟨p, hp, rfl⟩ := hab

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a c p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
simp_rw : ∀ (hp : 0 ≤ p), ∃ (p_1 : R), 0 ≤ p_1 ∧ star c * (a + p) * c = star c * a * c + p_1
⊢ ∃ (p_1 : R),
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p_1 ∧
      star c * (a + p) * c = star c * a * c + p_1

Tactic:
simp_rw [← StarOrderedRing.nonneg_iff] at hp ⊢

Premises used: StarOrderedRing.nonneg_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a c p : R
hp : 0 ≤ p
⊢ star c * (a + p) * c = star c * a * c + star c * p * c

Tactic:
simp only [add_mul, mul_add]

Premises used: add_mul, mul_add
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a c p : R
hp : 0 ≤ p
⊢ ∃ (p_1 : R), 0 ≤ p_1 ∧ star c * (a + p) * c = star c * a * c + p_1

Tactic:
exact ⟨star c * p * c, star_left_conjugate_nonneg hp c, by simp only [add_mul, mul_add]⟩
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
⊢ c * a * star c ≤ c * b * star c

Tactic:
simpa only [star_star] using star_left_conjugate_le_conjugate hab (star c)

Premises used: star_star, star_left_conjugate_le_conjugate, Star.star
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
hc : IsSelfAdjoint c
⊢ c * a * c ≤ c * b * c

Tactic:
simpa only [hc.star_eq] using star_left_conjugate_le_conjugate hab c

Premises used: star_left_conjugate_le_conjugate, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
hc : 0 ≤ c
⊢ c * a * c ≤ c * b * c

Tactic:
IsSelfAdjoint.of_nonneg hc |>.conjugate_le_conjugate hab

Premises used: IsSelfAdjoint.conjugate_le_conjugate, IsSelfAdjoint.of_nonneg
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x y : R
this : ∀ (x y : R), x ≤ y → star x ≤ star y
⊢ star x ≤ star y → x ≤ y

Tactic:
simpa only [star_star] using this (star x) (star y)

Premises used: star_star, Star.star
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x y : R
suffices : ∀ (x y : R), x ≤ y → star x ≤ star y
⊢ star x ≤ star y ↔ x ≤ y

Tactic:
suffices ∀ x y, x ≤ y → star x ≤ star y from
    ⟨by simpa only [star_star] using this (star x) (star y), this x y⟩
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x_1 y_1 x y : R
h : x ≤ y
rw :
  ∀
    (h :
      ∃ (p : R),
        Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p),
    ∃ (p : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧
        star y = star x + p
⊢ star x ≤ star y

Tactic:
rw [StarOrderedRing.le_iff] at h ⊢

Premises used: StarOrderedRing.le_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x_1 y_1 x y : R
h :
  ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
obtain :
  ∀ (d : R) (hd : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) d),
    ∃ (p : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧
        star (x + d) = star x + p
⊢ ∃ (p : R),
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ star y = star x + p

Tactic:
obtain ⟨d, hd, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x_1 y x d : R
hd : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) d
⊢ ∃ (p : R),
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧
      star (x + d) = star x + p

Tactic:
⟨starAddEquiv d, ?_, star_add _ _⟩

Premises used: StarAddMonoid.star_add, And.intro, Exists.intro, starAddEquiv, DFunLike.coe
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x_1 y x d : R
hd : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) d
refine :
  Membership.mem (α := R) (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s))
    ((starAddEquiv : (a : R) → R) d : R)
⊢ ∃ (p : R),
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧
      star (x + d) = star x + p

Tactic:
refine ⟨starAddEquiv d, ?_, star_add _ _⟩
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x_1 y x d : R
hd : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) d
⊢ Membership.mem (α := R) (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s))
    ((starAddEquiv : (a : R) → R) d : R)

Tactic:
AddMonoidHom.mclosure_preimage_le _ _ <| AddSubmonoid.closure_mono ?_ hd

Premises used: iInf, Set.Mem, Set.iInter, setOf, AddMonoidHom.mclosure_preimage_le, Set.preimage, AddSubmonoid.closure_mono
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x_1 y x d : R
hd : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) d
refine :
  Subset.{u_1} (α := Set R) (range fun (s : R) ↦ star s * s)
    (preimage (β := R) (⇑starAddEquiv : (a : R) → R) (range fun (s : R) ↦ star s * s))
⊢ Membership.mem (α := R) (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s))
    ((starAddEquiv : (a : R) → R) d : R)

Tactic:
refine AddMonoidHom.mclosure_preimage_le _ _ <| AddSubmonoid.closure_mono ?_ hd

Premises used: AddMonoidHom.mclosure_preimage_le, AddSubmonoid.closure_mono
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x_1 y x d : R
hd : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) d
s : R
⊢ Eq.{u_1 + 1} (α := R) ((fun (s : R) ↦ star s * s) s : R)
    ((starAddEquiv : (a : R) → R) ((fun (s : R) ↦ star s * s) s) : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x_1 y x d : R
hd : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) d
s : R
⊢ Membership.mem (γ := Set R) (preimage (β := R) (⇑starAddEquiv : (a : R) → R) (range fun (s : R) ↦ star s * s))
    ((fun (s : R) ↦ star s * s) s)

Tactic:
exact ⟨s, by simp⟩
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x y : R
pos : ∀ (h : x = y), star x < star y ↔ x < y
neg : ∀ (h : ¬x = y), star x < star y ↔ x < y
⊢ star x < star y ↔ x < y

Tactic:
by_cases h : x = y
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x y : R
h : x = y
⊢ star x < star y ↔ x < y

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x y : R
h : ¬x = y
⊢ star x < star y ↔ x < y

Tactic:
simpa [le_iff_lt_or_eq, h] using star_le_star_iff (x := x) (y := y)

Premises used: le_iff_lt_or_eq, star_le_star_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x y : R
rw : star (star x) ≤ star y ↔ x ≤ star y
rw₁ rw₂ : x ≤ star y ↔ x ≤ star y
⊢ star x ≤ y ↔ x ≤ star y

Tactic:
rw [← star_le_star_iff, star_star]

Premises used: star_star, star_le_star_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x y : R
rw : star (star x) < star y ↔ x < star y
rw₁ rw₂ : x < star y ↔ x < star y
⊢ star x < y ↔ x < star y

Tactic:
rw [← star_lt_star_iff, star_star]

Premises used: star_star, star_lt_star_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x : R
⊢ 0 ≤ star x ↔ 0 ≤ x

Tactic:
simpa using star_le_star_iff (x := 0) (y := x)

Premises used: star_le_star_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x : R
⊢ star x ≤ 0 ↔ x ≤ 0

Tactic:
simpa using star_le_star_iff (x := x) (y := 0)

Premises used: star_le_star_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x : R
⊢ 0 < star x ↔ 0 < x

Tactic:
simpa using star_lt_star_iff (x := 0) (y := x)

Premises used: star_lt_star_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x : R
⊢ star x < 0 ↔ x < 0

Tactic:
simpa using star_lt_star_iff (x := x) (y := 0)

Premises used: star_lt_star_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a b : R
hab : a < b
c : R
hc : IsRegular c
rw : a ≠ b
⊢ star c * a * c < star c * b * c

Tactic:
rw [(star_left_conjugate_le_conjugate hab.le _).lt_iff_ne, hc.right.ne_iff, hc.star.left.ne_iff]

Premises used: IsRegular.right, Function.Injective.ne_iff, LT.lt.le, star_left_conjugate_le_conjugate, LE.le.lt_iff_ne, IsRegular.left, IsRegular.star
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a b : R
hab : a < b
c : R
hc : IsRegular c
⊢ a ≠ b

Tactic:
hab.ne

Premises used: LT.lt.ne
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a b : R
hab : a < b
c : R
hc : IsRegular c
⊢ a ≠ b

Tactic:
exact hab.ne

Premises used: LT.lt.ne
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a b : R
hab : a < b
c : R
hc : IsRegular c
⊢ c * a * star c < c * b * star c

Tactic:
simpa only [star_star] using star_left_conjugate_lt_conjugate hab hc.star

Premises used: star_star, star_left_conjugate_lt_conjugate, IsRegular.star
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a : R
ha : 0 < a
c : R
hc : IsRegular c
⊢ 0 < star c * a * c

Tactic:
simpa only [mul_zero, zero_mul] using star_left_conjugate_lt_conjugate ha hc

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, star_left_conjugate_lt_conjugate
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a : R
ha : 0 < a
c : R
hc : IsRegular c
⊢ 0 < c * a * star c

Tactic:
simpa only [star_star] using star_left_conjugate_pos ha hc.star

Premises used: star_star, star_left_conjugate_pos, IsRegular.star
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Nontrivial R
x : R
hx : IsRegular x
rw : 0 ≠ x
⊢ 0 < star x * x

Tactic:
rw [(star_mul_self_nonneg _).lt_iff_ne, ← mul_zero (star x), hx.star.left.ne_iff]

Premises used: Function.Injective.ne_iff, star_mul_self_nonneg, MulZeroClass.mul_zero, LE.le.lt_iff_ne, IsRegular.left, IsRegular.star, Star.star
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Nontrivial R
x : R
hx : IsRegular x
⊢ 0 ≠ x

Tactic:
hx.ne_zero.symm

Premises used: Ne.symm, IsRegular.ne_zero
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Nontrivial R
x : R
hx : IsRegular x
⊢ 0 ≠ x

Tactic:
exact hx.ne_zero.symm

Premises used: Ne.symm, IsRegular.ne_zero
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Nontrivial R
x : R
hx : IsRegular x
⊢ 0 < x * star x

Tactic:
simpa using star_mul_self_pos hx.star

Premises used: IsRegular.star, star_mul_self_pos
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
⊢ LE.le.{u_1} (α := R) 0 1

Tactic:
simpa using star_mul_self_nonneg (1 : R)

Premises used: star_mul_self_nonneg, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x : R
⊢ 1 ≤ star x ↔ 1 ≤ x

Tactic:
simpa using star_le_star_iff (x := 1) (y := x)

Premises used: star_le_star_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x : R
⊢ star x ≤ 1 ↔ x ≤ 1

Tactic:
simpa using star_le_star_iff (x := x) (y := 1)

Premises used: star_le_star_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x : R
⊢ 1 < star x ↔ 1 < x

Tactic:
simpa using star_lt_star_iff (x := 1) (y := x)

Premises used: star_lt_star_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x : R
⊢ star x < 1 ↔ x < 1

Tactic:
simpa using star_lt_star_iff (x := x) (y := 1)

Premises used: star_lt_star_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
a : R
ha : IsSelfAdjoint a
⊢ 0 ≤ HPow.hPow (β := ℕ) a 2

Tactic:
simp [sq, ha.mul_self_nonneg]

Premises used: sq, IsSelfAdjoint.mul_self_nonneg
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
⊢ 0 ≤ u * x * star u ↔ 0 ≤ x

Tactic:
⟨fun h ↦ ?_, fun h ↦ star_right_conjugate_nonneg h _⟩

Premises used: Iff.intro, star_right_conjugate_nonneg
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
refine : ∀ (h : 0 ≤ u * x * star u), 0 ≤ x
⊢ 0 ≤ u * x * star u ↔ 0 ≤ x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ star_right_conjugate_nonneg h _⟩
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
obtain : ∀ (v : R) (hv : v * u = 1), 0 ≤ x
⊢ 0 ≤ x

Tactic:
obtain ⟨v, hv⟩ := hu.exists_left_inv

Premises used: IsUnit.exists_left_inv
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
⊢ 0 ≤ v * u * x * star u * star v

Tactic:
simpa [← mul_assoc] using star_right_conjugate_nonneg h v

Premises used: mul_assoc, star_right_conjugate_nonneg
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
⊢ 0 ≤ v * u * x * star u * star v

Tactic:
have := by simpa [← mul_assoc] using star_right_conjugate_nonneg h v
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ v * u * x * star u * star v
rwa : ∀ (this : 0 ≤ 1 * x * star u * star v), 0 ≤ x
rwa₁ : ∀ (this : 0 ≤ x * star u * star v), 0 ≤ x
rwa₂ : ∀ (this : 0 ≤ x * (star u * star v)), 0 ≤ x
rwa₃ : ∀ (this : 0 ≤ x * star (v * u)), 0 ≤ x
rwa₄ : ∀ (this : 0 ≤ x * star 1), 0 ≤ x
rwa₅ : ∀ (this : 0 ≤ x * 1), 0 ≤ x
rwa₆ rwa₇ rwa₈ rwa₉ : ∀ (this : 0 ≤ x), 0 ≤ x
⊢ 0 ≤ x

Tactic:
rwa [hv, one_mul, mul_assoc, ← star_mul, hv, star_one, mul_one] at this

Premises used: mul_assoc, StarMul.star_mul, mul_one, one_mul, star_one
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
⊢ 0 ≤ star u * x * u ↔ 0 ≤ x

Tactic:
simpa using hu.star.star_right_conjugate_nonneg_iff

Premises used: IsUnit.star, IsUnit.star_right_conjugate_nonneg_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : NonUnitalSemiring R
inst_1 : StarRing R
inst_2 : PartialOrder R
inst_3 : StarOrderedRing R
x y : Rᵐᵒᵖ
rw :
  (∃ (p : R),
      Membership.mem (γ := AddSubmonoid R)
          (AddSubmonoid.comap (F := R ≃+ Rᵐᵒᵖ) opAddEquiv
            (AddSubmonoid.map (F := R ≃+ Rᵐᵒᵖ) opAddEquiv (AddSubmonoid.closure (range fun (s : R) ↦ star s * s))))
          p ∧
        unop y = unop x + p) ↔
    ∃ (x_1 : R),
      Membership.mem (γ := AddSubmonoid Rᵐᵒᵖ) (AddSubmonoid.closure (range fun (s : Rᵐᵒᵖ) ↦ star s * s)) (op x_1) ∧
        y = x + op x_1
⊢ x ≤ y ↔
    ∃ (p : Rᵐᵒᵖ),
      Membership.mem (γ := AddSubmonoid Rᵐᵒᵖ) (AddSubmonoid.closure (range fun (s : Rᵐᵒᵖ) ↦ star s * s)) p ∧ y = x + p

Tactic:
rw [← unop_le_unop, StarOrderedRing.le_iff, op_surjective.exists,
      ← (AddSubmonoid.closure _).comap_map_eq_of_injective opAddEquiv.injective]

Premises used: Function.Surjective.exists, MulOpposite.opAddEquiv, MulOpposite.unop_le_unop, StarOrderedRing.le_iff, AddSubmonoid.closure, AddEquiv.injective, MulOpposite.op_surjective, AddSubmonoid.comap_map_eq_of_injective