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
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
s x : R
⊢ x ≤ x + (fun (s : R) ↦ star s * s) s

Tactic:
(h_le_iff _ _).mpr ⟨s, rfl⟩

Premises used: Iff.mpr, Exists.intro, rfl
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
s x : R
⊢ x ≤ x + (fun (s : R) ↦ star s * s) s

Tactic:
exact (h_le_iff _ _).mpr ⟨s, rfl⟩

Premises used: Iff.mpr, Exists.intro, rfl
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
x_1 y : R
hx : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x_1
hy : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) y
ha : ∀ (x y : R) (hpxy : y = x + x_1), x ≤ y
hb : ∀ (x y_1 : R) (hpxy : y_1 = x + y), x ≤ y_1
x : R
refine_2 : x ≤ x + x_1 + y
⊢ x ≤ x + (x_1 + y)

Tactic:
rw [← add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
x_1 y : R
hx : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x_1
hy : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) y
ha : ∀ (x y : R) (hpxy : y = x + x_1), x ≤ y
hb : ∀ (x y_1 : R) (hpxy : y_1 = x + y), x ≤ y_1
x : R
⊢ x ≤ x + x_1 + y

Tactic:
(ha _ _ rfl).trans (hb _ _ rfl)

Premises used: LE.le.trans, rfl
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
x_1 y : R
hx : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x_1
hy : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) y
ha : ∀ (x y : R) (hpxy : y = x + x_1), x ≤ y
hb : ∀ (x y_1 : R) (hpxy : y_1 = x + y), x ≤ y_1
x : R
⊢ x ≤ x + x_1 + y

Tactic:
exact (ha _ _ rfl).trans (hb _ _ rfl)

Premises used: LE.le.trans, rfl
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x_1 y_1 x y : R
hle : x ≤ y
z : R
rw :
  ∀
    (hle :
      ∃ (p : R),
        Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p)
    (z : R),
    ∃ (p : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y + z = x + z + p
⊢ x + z ≤ y + z

Tactic:
rw [StarOrderedRing.le_iff] at hle ⊢

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

Tactic:
hle.imp fun s hs ↦ ?_

Premises used: Exists.imp
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x_1 y_1 x y : R
hle :
  ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
z : R
refine :
  ∀ (s : R)
    (hs : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) s ∧ y = x + s),
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) s ∧ y + z = x + z + s
⊢ ∃ (p : R),
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y + z = x + z + p

Tactic:
refine hle.imp fun s hs ↦ ?_

Premises used: Exists.imp
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x_1 y_1 x y : R
hle :
  ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
z s : R
hs : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) s ∧ y = x + s
rw :
  Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) s ∧ x + z + s = x + z + s
⊢ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) s ∧ y + z = x + z + s

Tactic:
rw [hs.2, add_right_comm]

Premises used: add_right_comm, And.right
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x_1 y_1 x y : R
hle :
  ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
z s : R
hs : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) s ∧ y = x + s
⊢ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) s ∧ x + z + s = x + z + s

Tactic:
⟨hs.1, rfl⟩

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

Tactic:
exact ⟨hs.1, 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 : R
⊢ 0 ≤ x ↔ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x

Tactic:
simp only [le_iff, zero_add, exists_eq_right']

Premises used: exists_eq_right', zero_add, 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 : R
⊢ 0 < x ↔ x ≠ 0 ∧ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x

Tactic:
simp [lt_iff_le_and_ne, and_comm, eq_comm, le_iff]

Premises used: lt_iff_le_and_ne, and_comm, eq_comm, 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 y : R
inst_4 : IsCancelAdd R
rw :
  (∃ (x_1 : R),
      x ≠ y ∧
        Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x_1 ∧
          y = x + x_1) ↔
    ∃ (p : R),
      p ≠ 0 ∧ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
⊢ x < y ↔
    ∃ (p : R),
      p ≠ 0 ∧ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p

Tactic:
rw [lt_iff_le_and_ne, and_comm, StarOrderedRing.le_iff, ← exists_and_left]

Premises used: lt_iff_le_and_ne, exists_and_left, and_comm, 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 y : R
inst_4 : IsCancelAdd R
a :
  ∀ (p : R),
    x ≠ y ∧ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p ↔
      p ≠ 0 ∧ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
⊢ (∃ (x_1 : R),
      x ≠ y ∧
        Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x_1 ∧
          y = x + x_1) ↔
    ∃ (p : R),
      p ≠ 0 ∧ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p

Tactic:
congr! 2 with p
-- 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
inst_4 : IsCancelAdd R
p : R
⊢ x ≠ y ∧ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p ↔
    p ≠ 0 ∧ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p

Tactic:
simp +contextual [← and_assoc]

Premises used: and_assoc
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff :
  ∀ (x : R), 0 ≤ x ↔ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x
x y : R
⊢ AddLeftMono R

Tactic:
have : AddLeftMono R := ⟨fun _ _ _ h => h_add h _⟩
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff :
  ∀ (x : R), 0 ≤ x ↔ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x
x y : R
this : AddLeftMono R
⊢ x ≤ y ↔
    ∃ (p : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p

Tactic:
simpa only [← sub_eq_iff_eq_add', sub_nonneg, exists_eq_right'] using h_nonneg_iff (y - x)

Premises used: exists_eq_right', HSub.hSub, sub_nonneg, sub_eq_iff_eq_add'
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ ∃ (s : R), x = star s * s
⊢ AddLeftMono R

Tactic:
have : AddLeftMono R := ⟨fun _ _ _ h => h_add h _⟩
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ ∃ (s : R), x = star s * s
this : AddLeftMono R
⊢ ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s

Tactic:
simpa [sub_eq_iff_eq_add', sub_nonneg] using fun x y => h_nonneg_iff (y - x)

Premises used: HSub.hSub, sub_nonneg, sub_eq_iff_eq_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 y : R
h : x ≤ y
hx : IsSelfAdjoint x
⊢ ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p

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 y : R
h : x ≤ y
hx : IsSelfAdjoint x
h₁ :
  ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
⊢ IsSelfAdjoint x

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 y : R
h :
  ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
hx : IsSelfAdjoint x
obtain :
  ∀ (d : R) (hd : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) d),
    IsSelfAdjoint (x + d)
⊢ IsSelfAdjoint y

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 : R
hx : IsSelfAdjoint x
d : R
hd : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) d
rw : x + star d = x + d
⊢ IsSelfAdjoint (x + d)

Tactic:
rw [IsSelfAdjoint, star_add, hx.star_eq]

Premises used: IsSelfAdjoint, StarAddMonoid.star_add, 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
x : R
hx : IsSelfAdjoint x
d : R
hd : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) d
e_a : star d = d
⊢ x + star d = x + d

Tactic:
congr
-- 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
hx : IsSelfAdjoint x
d : R
hd : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) d
⊢ star d = d

Tactic:
AddMonoidHom.eqOn_closureM (f := starAddEquiv (R := R)) (g := .id R) ?_ hd

Premises used: AddMonoidHom.eqOn_closureM
-- 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
hx : IsSelfAdjoint x
d : R
hd : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) d
e_a :
  EqOn (α := R) (β := R) (⇑(↑starAddEquiv : R →+ R) : (a : R) → R) (⇑(AddMonoidHom.id R) : (a : R) → R)
    (range fun (s : R) ↦ star s * s)
⊢ star d = d

Tactic:
refine AddMonoidHom.eqOn_closureM (f := starAddEquiv (R := R)) (g := .id R) ?_ hd

Premises used: AddMonoidHom.eqOn_closureM
-- 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
hx : IsSelfAdjoint x
d : R
hd : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) d
s : R
⊢ Eq (α := R) (((↑starAddEquiv : R →+ R) : (a : R) → R) ((fun (s : R) ↦ star s * s) s) : R)
    ((AddMonoidHom.id R : (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 : R
hx : 0 ≤ x
⊢ IsSelfAdjoint x

Tactic:
.mono hx <| .zero R

Premises used: IsSelfAdjoint.zero, IsSelfAdjoint.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 : R
hx : 0 ≤ x
⊢ star x = x

Tactic:
hx.isSelfAdjoint.star_eq

Premises used: LE.le.isSelfAdjoint, 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
r : R
⊢ 0 ≤ star r * r

Tactic:
StarOrderedRing.nonneg_iff.mpr <| AddSubmonoid.subset_closure ⟨r, rfl⟩

Premises used: Iff.mpr, AddSubmonoid.subset_closure, StarOrderedRing.nonneg_iff, Exists.intro, 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
r : R
⊢ 0 ≤ r * star r

Tactic:
simpa only [star_star] using star_mul_self_nonneg (star r)

Premises used: star_star, star_mul_self_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 : IsSelfAdjoint a
⊢ 0 ≤ a * a

Tactic:
simpa [ha.star_eq] using star_mul_self_nonneg a

Premises used: star_mul_self_nonneg, 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
p : R
hp : IsStarProjection p
⊢ 0 ≤ p

Tactic:
hp.isIdempotentElem ▸ hp.isSelfAdjoint.mul_self_nonneg

Premises used: IsStarProjection.isIdempotentElem, Eq.rec, IsSelfAdjoint.mul_self_nonneg, IsStarProjection.isSelfAdjoint
-- 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
rw :
  ∀ (ha : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) a) (c : R),
    0 ≤ star c * a * c
⊢ 0 ≤ star c * a * c

Tactic:
rw [StarOrderedRing.nonneg_iff] at ha

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 : R
ha : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) a
c : R
rw : 0 ≤ 0 * c
rw₁ rw₂ : LE.le.{u_1} (α := R) 0 0
⊢ 0 ≤ star c * 0 * c

Tactic:
rw [mul_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_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
a : R
ha : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) a
c : R
refine_1 : ∀ (x : R) (hx : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) x), 0 ≤ star c * x * c
refine_2 :
  ∀ (x y : R),
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x →
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) y →
        ∀ (hx : 0 ≤ star c * x * c) (hy : 0 ≤ star c * y * c), 0 ≤ star c * (x + y) * c
⊢ 0 ≤ star c * a * c

Tactic:
refine AddSubmonoid.closure_induction (fun x hx => ?_)
    (by rw [mul_zero, zero_mul]) (fun x y _ _ hx hy => ?_) ha
-- 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 s * s)) a
c x : R
hx : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) x
refine_1 : ∀ (x : R), 0 ≤ star c * (fun (s : R) ↦ star s * s) x * c
⊢ 0 ≤ star c * x * c

Tactic:
obtain ⟨x, rfl⟩ := hx

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 : R
ha : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) a
c x : R
⊢ 0 ≤ star (x * c) * (x * c)

Tactic:
star_mul_self_nonneg (x * c)

Premises used: HMul.hMul, star_mul_self_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 : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) a
c x : R
h : star c * (fun (s : R) ↦ star s * s) x * c = star (x * c) * (x * c)
⊢ 0 ≤ star c * (fun (s : R) ↦ star s * s) x * c

Tactic:
convert! star_mul_self_nonneg (x * c) using 1

Premises used: HMul.hMul, star_mul_self_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 : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) a
c x : R
h : star c * (fun (s : R) ↦ star s * s) x * c = star c * star x * (x * c)
h₁ : star c * star x * x * c = star c * star x * (x * c)
h₂ h₃ : star c * star x * (x * c) = star c * star x * (x * c)
⊢ star c * (fun (s : R) ↦ star s * s) x * c = star (x * c) * (x * c)

Tactic:
rw [star_mul, ← mul_assoc, mul_assoc _ _ c]

Premises used: mul_assoc, StarMul.star_mul
-- 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 s * s)) a
c x y : R
h : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x
h_1 : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) y
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
rw : 0 ≤ star c * x * c
⊢ 0 ≤ star c * x * c + 0

Tactic:
rw [add_zero]

Premises used: add_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
a : R
ha : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) a
c x y : R
h : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x
h_1 : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) y
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * x * c

Tactic:
hx
-- 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 s * s)) a
c x y : R
h : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x
h_1 : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) y
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * x * c

Tactic:
exact hx
-- 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 s * s)) a
c x y : R
h : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x
h_1 : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) y
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ star c * x * c + 0 ≤ star c * x * c + star c * y * c

Tactic:
gcongr
-- 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 s * s)) a
c x y : R
h : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x
h_1 : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) y
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
rw : star c * x * c + star c * y * c ≤ (star c * x + star c * y) * c
rw₁ rw₂ : star c * x * c + star c * y * c ≤ star c * x * c + star c * y * c
⊢ star c * x * c + star c * y * c ≤ star c * (x + y) * c

Tactic:
rw [mul_add, add_mul]

Premises used: add_mul, mul_add