Theorem: LSeries.abscissaOfAbsConv_binop_le (EulerProducts/LSeriesUnique.lean)

State before:
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
⊢ abscissaOfAbsConv (F f g) ≤ max (abscissaOfAbsConv f) (abscissaOfAbsConv g)
Tactic:
refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' fun x hx ↦  hF ?_ ?_
State after:
case refine_1
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < ↑x
⊢ LSeriesSummable f ↑x

case refine_2
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < ↑x
⊢ LSeriesSummable g ↑x

State before:
case refine_1
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < ↑x
⊢ LSeriesSummable f ↑x
Tactic:
exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
  (ofReal_re x).symm ▸ (le_max_left ..).trans_lt hx
State after:
no goals

State before:
case refine_2
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < ↑x
⊢ LSeriesSummable g ↑x
Tactic:
exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
    (ofReal_re x).symm ▸ (le_max_right ..).trans_lt hx
State after:
no goals