-- Mathlib/Algebra/Order/Star/Basic.lean
/-- To construct a `StarOrderedRing` instance it suffices to show that `x ≤ y` if and only if
`y = x + star s * s` for some `s : R`.

This is provided for convenience because it holds in some common scenarios (e.g.,`ℝ≥0`, `C(X, ℝ≥0)`)
and obviates the hassle of `AddSubmonoid.closure_induction` when creating those instances.

If you are working with a `NonUnitalRing` and not a `NonUnitalSemiring`, see
`StarOrderedRing.of_nonneg_iff` for a more convenient version.
-/
lemma of_le_iff [NonUnitalSemiring R] [PartialOrder R] [StarRing R]
    (h_le_iff : ∀ x y : R, x ≤ y ↔ ∃ s, y = x + star s * s) : StarOrderedRing R where
  le_iff x y

Proof state:
case refine_2.intro.intro.refine_1
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ ∀ x ∈ range fun s => star s * s, ∀ (x_1 y : R), y = x_1 + x → x_1 ≤ y

Tactic:
rintro _ ⟨s, rfl⟩ x y rfl

Result:
case refine_2.intro.intro.refine_1.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
s x : R
⊢ x ≤ x + (fun s => star s * s) s

Proof state:
case refine_1.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
h : x ≤ y
p : R
hp : y = x + star p * p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p

Tactic:
exact ⟨star p * p, AddSubmonoid.subset_closure ⟨p, rfl⟩, hp⟩

Result:
no goals

Proof state:
case refine_2.intro.intro.refine_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
x✝ y✝ : R
hx✝ : x✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
hy✝ : y✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
ha : ∀ (x y : R), y = x + x✝ → x ≤ y
hb : ∀ (x y : R), y = x + y✝ → x ≤ y
x : R
⊢ x ≤ x + (x✝ + y✝)

Tactic:
rw [← add_assoc]

Result:
case refine_2.intro.intro.refine_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
x✝ y✝ : R
hx✝ : x✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
hy✝ : y✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
ha : ∀ (x y : R), y = x + x✝ → x ≤ y
hb : ∀ (x y : R), y = x + y✝ → x ≤ y
x : R
⊢ x ≤ x + x✝ + y✝

Proof state:
case refine_2.intro.intro.refine_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ ∀ (x y : R),
    x ∈ AddSubmonoid.closure (range fun s => star s * s) →
      y ∈ AddSubmonoid.closure (range fun s => star s * s) →
        (∀ (x_1 y : R), y = x_1 + x → x_1 ≤ y) →
          (∀ (x y_1 : R), y_1 = x + y → x ≤ y_1) → ∀ (x_1 y_1 : R), y_1 = x_1 + (x + y) → x_1 ≤ y_1

Tactic:
rintro _ _ _ _ ha hb x y rfl

Result:
case refine_2.intro.intro.refine_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
x✝ y✝ : R
hx✝ : x✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
hy✝ : y✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
ha : ∀ (x y : R), y = x + x✝ → x ≤ y
hb : ∀ (x y : R), y = x + y✝ → x ≤ y
x : R
⊢ x ≤ x + (x✝ + y✝)

Proof state:
case refine_2.intro.intro.refine_1.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
s x : R
⊢ x ≤ x + (fun s => star s * s) s

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

Result:
no goals

Proof state:
case refine_1
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
h : x ≤ y
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p

Tactic:
obtain ⟨p, hp⟩ := (h_le_iff x y).mp h

Result:
case refine_1.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
h : x ≤ y
p : R
hp : y = x + star p * p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p

Proof state:
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
⊢ x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p

Tactic:
refine ⟨fun h => ?_, ?_⟩

Result:
case refine_1
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
h : x ≤ y
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p

case refine_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
⊢ (∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p) → x ≤ y

Proof state:
case refine_2.intro.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
hpxy : y = x + p
⊢ x ≤ y

Tactic:
revert x y hpxy

Result:
case refine_2.intro.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ ∀ (x y : R), y = x + p → x ≤ y

Proof state:
case refine_2.intro.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ ∀ (x y : R), y = x + p → x ≤ y

Tactic:
refine AddSubmonoid.closure_induction ?_ (fun x y h => add_zero x ▸ h.ge) ?_ hp

Result:
case refine_2.intro.intro.refine_1
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ ∀ x ∈ range fun s => star s * s, ∀ (x_1 y : R), y = x_1 + x → x_1 ≤ y

case refine_2.intro.intro.refine_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ ∀ (x y : R),
    x ∈ AddSubmonoid.closure (range fun s => star s * s) →
      y ∈ AddSubmonoid.closure (range fun s => star s * s) →
        (∀ (x_1 y : R), y = x_1 + x → x_1 ≤ y) →
          (∀ (x y_1 : R), y_1 = x + y → x ≤ y_1) → ∀ (x_1 y_1 : R), y_1 = x_1 + (x + y) → x_1 ≤ y_1

Proof state:
case refine_2.intro.intro.refine_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
x✝ y✝ : R
hx✝ : x✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
hy✝ : y✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
ha : ∀ (x y : R), y = x + x✝ → x ≤ y
hb : ∀ (x y : R), y = x + y✝ → x ≤ y
x : R
⊢ x ≤ x + x✝ + y✝

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

Result:
no goals