[GOAL]
x : ℚ
⊢ 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
[PROOFSTEP]
refine'
  ⟨fun hx => _, fun hx =>
    AddSubmonoid.closure_induction hx (by rintro - ⟨s, rfl⟩; exact mul_self_nonneg s) le_rfl fun _ _ => add_nonneg⟩
    /- If `x = p / q`, then, since `0 ≤ x`, we have `p q : ℕ`, and `p / q` is the sum of `p * q`
          copies of `(1 / q) ^ 2`, and so `x` lies in the `AddSubmonoid` generated by square elements.
    
          Note: it's possible to rephrase this argument as `x = (p * q) • (1 / q) ^ 2`, but this would
          be somewhat challenging without increasing import requirements. -/
        -- Porting note: rewrote proof to avoid removed constructor rat.mk_pnat
[GOAL]
x : ℚ
hx : x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
⊢ ∀ (x : ℚ), (x ∈ Set.range fun s => star s * s) → 0 ≤ x
[PROOFSTEP]
rintro - ⟨s, rfl⟩
[GOAL]
case intro
x : ℚ
hx : x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
s : ℚ
⊢ 0 ≤ (fun s => star s * s) s
[PROOFSTEP]
exact mul_self_nonneg s
[GOAL]
x : ℚ
hx : 0 ≤ x
⊢ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
[PROOFSTEP]
suffices (Finset.range (x.num.natAbs * x.den)).sum (Function.const ℕ ((1 : ℚ) / x.den * ((1 : ℚ) / x.den))) = x by
  exact this ▸ sum_mem fun n _ => AddSubmonoid.subset_closure ⟨_, rfl⟩
[GOAL]
x : ℚ
hx : 0 ≤ x
this : Finset.sum (Finset.range (Int.natAbs x.num * x.den)) (Function.const ℕ (1 / ↑x.den * (1 / ↑x.den))) = x
⊢ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
[PROOFSTEP]
exact this ▸ sum_mem fun n _ => AddSubmonoid.subset_closure ⟨_, rfl⟩
[GOAL]
x : ℚ
hx : 0 ≤ x
⊢ Finset.sum (Finset.range (Int.natAbs x.num * x.den)) (Function.const ℕ (1 / ↑x.den * (1 / ↑x.den))) = x
[PROOFSTEP]
simp only [Function.const_apply, Finset.sum_const, Finset.card_range, nsmul_eq_mul]
[GOAL]
x : ℚ
hx : 0 ≤ x
⊢ ↑(Int.natAbs x.num * x.den) * (1 / ↑x.den * (1 / ↑x.den)) = x
[PROOFSTEP]
rw [← Int.cast_ofNat, Int.ofNat_mul, Int.coe_natAbs, abs_of_nonneg (num_nonneg_iff_zero_le.mpr hx), Int.cast_mul,
  Int.cast_ofNat]
[GOAL]
x : ℚ
hx : 0 ≤ x
⊢ ↑x.num * ↑x.den * (1 / ↑x.den * (1 / ↑x.den)) = x
[PROOFSTEP]
rw [← mul_assoc, mul_assoc (x.num : ℚ), mul_one_div_cancel (Nat.cast_ne_zero.mpr x.pos.ne'), mul_one, mul_one_div,
  Rat.num_div_den]
