awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ x + z ≤ y + z
have 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
Tactic: rw [StarOrderedRing.le_iff] at hle ⊢
Cleared hypotheses: hle, z
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
have 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
Tactic: refine hle.imp fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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 ∧ y + z = x + z + s
have rw : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) s ∧ x + z + s = x + z + s
Tactic: rw [hs.2, add_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ x < y ↔
    ∃ (p : R),
      p ≠ 0 ∧ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
have 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
Tactic: rw [lt_iff_le_and_ne, and_comm, StarOrderedRing.le_iff, ← exists_and_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ (∃ (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
have 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
Tactic: congr! 2 with p
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (hypothesis)
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
⊢ x ≤ y ↔
    ∃ (p : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
have this : AddLeftMono R
Tactic: have : AddLeftMono R := ⟨fun _ _ _ h => h_add h _⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (hypothesis)
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
⊢ ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
have this : AddLeftMono R
Tactic: have : AddLeftMono R := ⟨fun _ _ _ h => h_add h _⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (hypothesis)
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
⊢ IsSelfAdjoint y
have h₁ : ∃ (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
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ IsSelfAdjoint y
have obtain : ∀ (d : R) (hd : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) d),
  IsSelfAdjoint (x + d)
Tactic: obtain ⟨d, hd, rfl⟩ := h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ IsSelfAdjoint (x + d)
have rw : x + star d = x + d
Tactic: rw [IsSelfAdjoint, star_add, hx.star_eq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ x + star d = x + d
have e_a : star d = d
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
have e_a : EqOn (α := R) (β := R) (⇑(↑starAddEquiv : R →+ R) : (a : R) → R) (⇑(AddMonoidHom.id R) : (a : R) → R)
  (range fun (s : R) ↦ star s * s)
Tactic: refine AddMonoidHom.eqOn_closureM (f := starAddEquiv (R := R)) (g := .id R) ?_ hd
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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 ≤ star c * a * c
have rw : ∀ (ha : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) a) (c : R),
  0 ≤ star c * a * c
Tactic: rw [StarOrderedRing.nonneg_iff] at ha
Cleared hypotheses: ha, c
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ 0 ≤ star c * 0 * c
have rw : 0 ≤ 0 * c
Tactic: rw [mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ 0 ≤ star c * 0 * c
have rw₁ : LE.le.{u_1} (α := R) 0 0
Tactic: rw [mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ 0 ≤ star c * a * c
have refine_1 : ∀ (x : R) (hx : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) x), 0 ≤ star c * x * c
Tactic: refine AddSubmonoid.closure_induction (fun x hx => ?_)
    (by rw [mul_zero, zero_mul]) (fun x y _ _ hx hy => ?_) ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ 0 ≤ star c * a * c
have 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
Tactic: refine AddSubmonoid.closure_induction (fun x hx => ?_)
    (by rw [mul_zero, zero_mul]) (fun x y _ _ hx hy => ?_) ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ 0 ≤ star c * x * c
have refine_1 : ∀ (x : R), 0 ≤ star c * (fun (s : R) ↦ star s * s) x * c
Tactic: obtain ⟨x, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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 c * (fun (s : R) ↦ star s * s) x * c
have h : star c * (fun (s : R) ↦ star s * s) x * c = star (x * c) * (x * c)
Tactic: convert! star_mul_self_nonneg (x * c) using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ star c * (fun (s : R) ↦ star s * s) x * c = star (x * c) * (x * c)
have h : star c * (fun (s : R) ↦ star s * s) x * c = star c * star x * (x * c)
Tactic: rw [star_mul, ← mul_assoc, mul_assoc _ _ c]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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)
⊢ star c * (fun (s : R) ↦ star s * s) x * c = star (x * c) * (x * c)
have h₁ : star c * star x * x * c = star c * star x * (x * c)
Tactic: rw [star_mul, ← mul_assoc, mul_assoc _ _ c]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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)
⊢ star c * (fun (s : R) ↦ star s * s) x * c = star (x * c) * (x * c)
have h₂ : star c * star x * (x * c) = star c * star x * (x * c)
Tactic: rw [star_mul, ← mul_assoc, mul_assoc _ _ c]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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 + star c * y * c ≤ star c * (x + y) * c
have rw : star c * x * c + star c * y * c ≤ (star c * x + star c * y) * c
Tactic: rw [mul_add, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ star c * x * c + star c * y * c ≤ star c * (x + y) * c
have rw₁ : star c * x * c + star c * y * c ≤ star c * x * c + star c * y * c
Tactic: rw [mul_add, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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 + y) * c
have star : 0 ≤ star c * x * c + 0
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ 0 ≤ Star.star c * (x + y) * c
have star₁ : Star.star c * x * c + 0 ≤ Star.star c * x * c + Star.star c * 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ 0 ≤ Star.star c * (x + y) * c
have star₂ : Star.star c * x * c + Star.star c * y * c ≤ 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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 * c
have nth_rewrite : 0 ≤ c * a * star c
Tactic: nth_rewrite 2 [← hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ star c * a * c ≤ star c * b * c
have 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
Tactic: rw [StarOrderedRing.le_iff] at hab ⊢
Cleared hypotheses: hab, c
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨p, hp, rfl⟩ := hab
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ ∃ (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
have simp_rw : ∀ (hp : 0 ≤ p), ∃ (p_1 : R), 0 ≤ p_1 ∧ star c * (a + p) * c = star c * a * c + p_1
Tactic: simp_rw [← StarOrderedRing.nonneg_iff] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x y : R
⊢ star x ≤ star y ↔ x ≤ y
have suffices : ∀ (x y : R), x ≤ y → star x ≤ star 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⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ star x ≤ star y
have 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
Tactic: rw [StarOrderedRing.le_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ ∃ (p : R),
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ star y = star x + p
have 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
Tactic: obtain ⟨d, hd, rfl⟩ := h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
have refine : Membership.mem (α := R) (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s))
  ((starAddEquiv : (a : R) → R) d : R)
Tactic: refine ⟨starAddEquiv d, ?_, star_add _ _⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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)
have 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))
Tactic: refine AddMonoidHom.mclosure_preimage_le _ _ <| AddSubmonoid.closure_mono ?_ hd
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x y : R
⊢ star x < star y ↔ x < y
have pos : ∀ (h : x = y), star x < star y ↔ x < y
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ star x < star y ↔ x < y
have neg : ∀ (h : ¬x = y), star x < star y ↔ x < y
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x y : R
⊢ star x ≤ y ↔ x ≤ star y
have rw : star (star x) ≤ star y ↔ x ≤ star y
Tactic: rw [← star_le_star_iff, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ star x ≤ y ↔ x ≤ star y
have rw₁ : x ≤ star y ↔ x ≤ star y
Tactic: rw [← star_le_star_iff, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
x y : R
⊢ star x < y ↔ x < star y
have rw : star (star x) < star y ↔ x < star y
Tactic: rw [← star_lt_star_iff, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ star x < y ↔ x < star y
have rw₁ : x < star y ↔ x < star y
Tactic: rw [← star_lt_star_iff, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
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
⊢ star c * a * c < star c * b * c
have rw : a ≠ b
Tactic: rw [(star_left_conjugate_le_conjugate hab.le _).lt_iff_ne, hc.right.ne_iff, hc.star.left.ne_iff]