Refined Count Triples Star is Big O B

theorem refinedCountTriplesStar_isBigO_B  {α β γ : ℝ}  /- I'm surprised these assumptions are not necessary.    Shoud think about if I've done something wrong - Arend -/  -- (hα_pos : 0 < α) (hβ_pos : 0 < β) (hγ_pos : 0 < γ)  -- (hα1 : α ≤ 1) (hβ1 : β ≤ 1) (hγ1 : γ ≤ 1)  {x : ℕ} (h2X : 2 ≤ x) {ε : ℝ} (hε_pos : 0 < ε) (hε : ε < 1/2) :  ∃ s : Finset ((Fin (d ε) → ℕ) × (Fin (d ε) → ℕ) × (Fin (d ε) → ℕ) × (Fin 3 → ℕ)),    refinedCountTriplesStar α β γ x ≤      const ε * (x : ℝ) ^ ε * ↑(s.sup (fun ⟨X, Y, Z, c⟩ ↦ B (d ε) c X Y Z): ℕ) ∧    ∀ X Y Z : Fin (d ε) → ℕ,    ∀ c : Fin 3 → ℕ,    ⟨X, Y, Z, c⟩ ∈ s →    (x:ℝ)^(α - ε) ≤ 2 ^ d ε * ∏ j, X j ∧ ∏ j, X j ≤ 2 * (x : ℝ) ^ (α + ε) ∧    (x:ℝ)^(β - ε) ≤ 2 ^ d ε * ∏ j, Y j ∧ ∏ j, Y j ≤ 2 * (x : ℝ) ^ (β + ε) ∧    (x:ℝ)^(γ - ε) ≤ 2 ^ d ε * ∏ j, Z j ∧ ∏ j, Z j ≤ 2 * (x : ℝ) ^ (γ + ε) ∧    ∏ i, X i ^ (i.val + 1) ≤ x ∧    ∏ i, Y i ^ (i.val + 1) ≤ x ∧    ∏ i, Z i ^ (i.val + 1) ≤ x ∧    (x : ℝ) ^ (1 - ε^2) ≤ 2^(Nat.choose (d ε + 1) 2 + 1) * ∏ i, Z i ^ (i.val + 1) ∧    (Nat.Coprime (c 0) (c 1)) ∧ (Nat.Coprime (c 1) (c 2)) ∧ (Nat.Coprime (c 0) (c 2)) ∧    (∀ i, 1 ≤ c i) ∧    (∀ i, (c i : ℝ) ≤ (x : ℝ) ^ ε)    := by  have h₁ := refinedCountTriplesStar_le_card_BUnion α β γ (d := d ε) x ε hε_pos hε rfl  simp_rw [BUnion, Finset.sup_eq_biUnion] at h₁  have h₂ := h₁.trans Finset.card_biUnion_le |>.trans (sum_le_card_mul_sup ..)  use (indexSet' α β γ (d ε) x ε).image fun ⟨u, v, w, c⟩ ↦    ⟨fun i ↦ 2 ^ u i, fun i ↦ 2 ^ v i, fun i ↦ 2 ^ w i, c⟩  simp only [Finset.sup_image, Finset.mem_image, Prod.mk.injEq, Prod.exists, Nat.cast_prod,    Nat.cast_pow, forall_exists_index, and_imp]  refine ⟨?_, ?_⟩  · calc      _ ≤ ((_ : ℕ) : ℝ) := Nat.cast_le.2 h₂      _ ≤ _ := by        push_cast        gcongr        · have := const_nonneg (ε := ε)          positivity        · exact card_indexSet'_le_pow ε α β γ (d ε) x rfl h2X hε_pos hε        rfl  rintro X Y Z _ u v w c huvwc rfl rfl rfl rfl  simp only [Nat.cast_pow, Nat.cast_ofNat]  revert huvwc  simp only [indexSet', Finset.mem_filter, Finset.mem_product, Fintype.mem_piFinset, Finset.mem_Icc,    zero_le, true_and, Finset.mem_Ioc, and_imp]  rintro _ _ _ hc _ _ _ _ _ _ _ _ _ _ _ _ _  refine ⟨by assumption, by assumption, by assumption, by assumption, by assumption, by assumption,    by assumption, by assumption, by assumption, by assumption, by assumption, by assumption,    by assumption, ?_, ?_⟩  · intro i    apply Nat.succ_le_of_lt    apply hc i |>.1  · intro i    calc      (c i : ℝ) ≤ (⌊(x:ℝ) ^ (ε / 4)⌋₊ : ℝ) := by        norm_cast        apply (hc i).2      _ ≤ (x : ℝ)^(ε/4) := by        apply Nat.floor_le        positivity      _ ≤  _ := by        gcongr        · norm_cast; omega        · linarith