-- Mathlib/Analysis/Complex/AbelLimit.lean
private lemma stolzCone_subset_stolzSet_aux' (s : ℝ) :
    ∃ M ε, 0 < M ∧ 0 < ε ∧ ∀ x y, 0 < x → x < ε → |y| < s * x →
      sqrt (x ^ 2 + y ^ 2) < M * (1 - sqrt ((1 - x) ^ 2 + y ^ 2))

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ x ^ 2 + y ^ 2 ≤ x ^ 2 + (s * x) ^ 2

Tactic:
rw [← sq_abs y]

Result:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ x ^ 2 + |y| ^ 2 ≤ x ^ 2 + (s * x) ^ 2

Proof state:
case h
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ x / 2 ≤ 1 - √((1 - x) ^ 2 + y ^ 2)

Tactic:
exact le_sub_comm.mpr H

Result:
no goals

Proof state:
case e_x
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ 1 - 2 * x + x = 1 - x

Tactic:
ring

Result:
no goals

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ √(x ^ 2 + y ^ 2) < (2 * √(1 + s ^ 2) + 1) * (1 - √((1 - x) ^ 2 + y ^ 2))

Tactic:
have H : sqrt ((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2 := by
  calc sqrt ((1 - x) ^ 2 + y ^ 2)
    _ ≤ sqrt ((1 - x) ^ 2 + (s * x) ^ 2) := sqrt_le_sqrt <| by rw [← sq_abs y]; gcongr
    _ = sqrt (1 - 2 * x + (1 + s ^ 2) * x * x) := by congr 1; ring
    _ ≤ sqrt (1 - 2 * x + (1 + s ^ 2) * (1 / (1 + s ^ 2)) * x) := sqrt_le_sqrt <| by gcongr
    _ = sqrt (1 - x) := by congr 1; field_simp; ring
    _ ≤ 1 - x / 2 := by
      simp_rw [sub_eq_add_neg, ← neg_div]
      refine sqrt_one_add_le <| neg_le_neg_iff.mpr (hx₁.trans_le ?_).le
      rw [div_le_one (by positivity)]
      exact le_add_of_nonneg_right <| sq_nonneg s

Result:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ √(x ^ 2 + y ^ 2) < (2 * √(1 + s ^ 2) + 1) * (1 - √((1 - x) ^ 2 + y ^ 2))

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ x ^ 2 + |y| ^ 2 ≤ x ^ 2 + (s * x) ^ 2

Tactic:
gcongr

Result:
no goals

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ √((1 + s ^ 2) * x ^ 2) = √(1 + s ^ 2) * x

Tactic:
rw [sqrt_mul' _ (sq_nonneg x), sqrt_sq hx₀.le]

Result:
no goals

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ √(1 + s ^ 2) * x = 2 * √(1 + s ^ 2) * (x / 2)

Tactic:
ring

Result:
no goals

Proof state:
case e_x
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ x ^ 2 + (s * x) ^ 2 = (1 + s ^ 2) * x ^ 2

Tactic:
ring

Result:
no goals

Proof state:
s : ℝ
⊢ ∃ M ε, 0 < M ∧ 0 < ε ∧ ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))

Tactic:
refine ⟨2 * sqrt (1 + s ^ 2) + 1, 1 / (1 + s ^ 2), by positivity, by positivity,
  fun x y hx₀ hx₁ hy ↦ ?_⟩

Result:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ √(x ^ 2 + y ^ 2) < (2 * √(1 + s ^ 2) + 1) * (1 - √((1 - x) ^ 2 + y ^ 2))

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ 2 * √(1 + s ^ 2) * (x / 2) < (2 * √(1 + s ^ 2) + 1) * (x / 2)

Tactic:
gcongr

Result:
case bc
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ 2 * √(1 + s ^ 2) < 2 * √(1 + s ^ 2) + 1

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ 1 / (1 + s ^ 2) ≤ 1

Tactic:
rw [div_le_one (by positivity)]

Result:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ 1 ≤ 1 + s ^ 2

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ 1 - 2 * x + (1 + s ^ 2) * x * x ≤ 1 - 2 * x + (1 + s ^ 2) * (1 / (1 + s ^ 2)) * x

Tactic:
gcongr

Result:
no goals

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ √(1 - x) ≤ 1 - x / 2

Tactic:
simp_rw [sub_eq_add_neg, ← neg_div]

Result:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ √(1 + -x) ≤ 1 + -x / 2

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ 1 ≤ 1 + s ^ 2

Tactic:
exact le_add_of_nonneg_right <| sq_nonneg s

Result:
no goals

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ √(x ^ 2 + y ^ 2) < (2 * √(1 + s ^ 2) + 1) * (1 - √((1 - x) ^ 2 + y ^ 2))

Tactic:
calc sqrt (x ^ 2 + y ^ 2)
  _ ≤ sqrt (x ^ 2 + (s * x) ^ 2) := sqrt_le_sqrt <| by rw [← sq_abs y]; gcongr
  _ = sqrt ((1 + s ^ 2) * x ^ 2) := by congr; ring
  _ = sqrt (1 + s ^ 2) * x := by rw [sqrt_mul' _ (sq_nonneg x), sqrt_sq hx₀.le]
  _ = 2 * sqrt (1 + s ^ 2) * (x / 2) := by ring
  _ < (2 * sqrt (1 + s ^ 2) + 1) * (x / 2) := by gcongr; exact lt_add_one _
  _ ≤ _ := by gcongr; exact le_sub_comm.mpr H

Result:
no goals

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ √(1 + -x) ≤ 1 + -x / 2

Tactic:
refine sqrt_one_add_le <| neg_le_neg_iff.mpr (hx₁.trans_le ?_).le

Result:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ 1 / (1 + s ^ 2) ≤ 1

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ √(1 - 2 * x + (1 + s ^ 2) * (1 / (1 + s ^ 2)) * x) = √(1 - x)

Tactic:
congr 1

Result:
case e_x
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ 1 - 2 * x + (1 + s ^ 2) * (1 / (1 + s ^ 2)) * x = 1 - x

Proof state:
case e_x
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ (1 - x) ^ 2 + (s * x) ^ 2 = 1 - 2 * x + (1 + s ^ 2) * x * x

Tactic:
ring

Result:
no goals

Proof state:
s : ℝ
⊢ 0 < 1 / (1 + s ^ 2)

Tactic:
positivity

Result:
no goals

Proof state:
s : ℝ
⊢ 0 < 2 * √(1 + s ^ 2) + 1

Tactic:
positivity

Result:
no goals

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ (2 * √(1 + s ^ 2) + 1) * (x / 2) ≤ (2 * √(1 + s ^ 2) + 1) * (1 - √((1 - x) ^ 2 + y ^ 2))

Tactic:
gcongr

Result:
case h
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ x / 2 ≤ 1 - √((1 - x) ^ 2 + y ^ 2)

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ 0 < 1 + s ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
case e_x
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ 1 - 2 * x + (1 + s ^ 2) * (1 / (1 + s ^ 2)) * x = 1 - x

Tactic:
field_simp

Result:
case e_x
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ 1 - 2 * x + x = 1 - x

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ √((1 - x) ^ 2 + (s * x) ^ 2) = √(1 - 2 * x + (1 + s ^ 2) * x * x)

Tactic:
congr 1

Result:
case e_x
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ (1 - x) ^ 2 + (s * x) ^ 2 = 1 - 2 * x + (1 + s ^ 2) * x * x

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2

Tactic:
calc sqrt ((1 - x) ^ 2 + y ^ 2)
  _ ≤ sqrt ((1 - x) ^ 2 + (s * x) ^ 2) := sqrt_le_sqrt <| by rw [← sq_abs y]; gcongr
  _ = sqrt (1 - 2 * x + (1 + s ^ 2) * x * x) := by congr 1; ring
  _ ≤ sqrt (1 - 2 * x + (1 + s ^ 2) * (1 / (1 + s ^ 2)) * x) := sqrt_le_sqrt <| by gcongr
  _ = sqrt (1 - x) := by congr 1; field_simp; ring
  _ ≤ 1 - x / 2 := by
    simp_rw [sub_eq_add_neg, ← neg_div]
    refine sqrt_one_add_le <| neg_le_neg_iff.mpr (hx₁.trans_le ?_).le
    rw [div_le_one (by positivity)]
    exact le_add_of_nonneg_right <| sq_nonneg s

Result:
no goals

Proof state:
case bc
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ 2 * √(1 + s ^ 2) < 2 * √(1 + s ^ 2) + 1

Tactic:
exact lt_add_one _

Result:
no goals