awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
G : Type u_3
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
hf' : TendstoUniformly f' g' l
hf_1 : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x
hfg_1 : ∀ (x : 𝕜), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x : 𝕜
hf : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x
hfg : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
⊢ TendstoUniformlyOn f' g' l Set.univ

Tactic:
have hf' : TendstoUniformlyOn f' g' l Set.univ := by rwa [tendstoUniformlyOn_univ]
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
G : Type u_3
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
hf'_1 : TendstoUniformly f' g' l
hf_1 : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x
hfg_1 : ∀ (x : 𝕜), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x : 𝕜
hf : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x
hfg : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
hf' : TendstoUniformlyOn f' g' l Set.univ
⊢ HasDerivAt g (g' x) x

Tactic:
hasDerivAt_of_tendstoUniformlyOn isOpen_univ hf' hf hfg (Set.mem_univ x)

Premises used: hasDerivAt_of_tendstoUniformlyOn, isOpen_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
G : Type u_3
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
hf'_1 : TendstoUniformly f' g' l
hf_1 : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x
hfg_1 : ∀ (x : 𝕜), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x : 𝕜
hf : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x
hfg : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
hf' : TendstoUniformlyOn f' g' l Set.univ
⊢ HasDerivAt g (g' x) x

Tactic:
exact hasDerivAt_of_tendstoUniformlyOn isOpen_univ hf' hf hfg (Set.mem_univ x)

Premises used: hasDerivAt_of_tendstoUniformlyOn, isOpen_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
M : ℝ
hM : M ≤ 1
h : ∀ (z : ℂ), z ∈ stolzSet M ↔ Membership.mem (γ := Set ℂ) ∅ z
⊢ stolzSet M = ∅

Tactic:
ext z
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
M : ℝ
hM : M ≤ 1
z : ℂ
h : 0 < 1 - ‖z‖ → M * (1 - ‖z‖) ≤ ‖1 - z‖
⊢ z ∈ stolzSet M ↔ Membership.mem (γ := Set ℂ) ∅ z

Tactic:
rw [stolzSet, Set.mem_setOf, Set.mem_empty_iff_false, iff_false, not_and, not_lt, ← sub_pos]

Premises used: sub_pos, iff_false, Set.mem_setOf, not_lt, Set.mem_empty_iff_false, not_and, Complex.stolzSet
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
M : ℝ
hM : M ≤ 1
z : ℂ
zn : 0 < 1 - ‖z‖
ha : 0 ≤ 1 - ‖z‖
⊢ M * (1 - ‖z‖) ≤ 1 * (1 - ‖z‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
M : ℝ
hM : M ≤ 1
z : ℂ
zn : 0 < 1 - ‖z‖
rw : 1 - ‖z‖ = Norm.norm (E := ℂ) 1 - ‖z‖
rw₁ rw₂ : 1 - ‖z‖ = 1 - ‖z‖
⊢ 1 * (1 - ‖z‖) = Norm.norm (E := ℂ) 1 - ‖z‖

Tactic:
rw [one_mul, norm_one]

Premises used: NormOneClass.norm_one, one_mul
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
M : ℝ
hM : M ≤ 1
z : ℂ
zn : 0 < 1 - ‖z‖
⊢ Norm.norm (E := ℂ) 1 - ‖z‖ ≤ ‖1 - z‖

Tactic:
norm_sub_norm_le _ _

Premises used: norm_sub_norm_le
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
M : ℝ
hM : M ≤ 1
z : ℂ
zn : 0 < 1 - ‖z‖
_ : M * (1 - ‖z‖) ≤ 1 * (1 - ‖z‖)
_₁ : 1 * (1 - ‖z‖) = Norm.norm (E := ℂ) 1 - ‖z‖
⊢ M * (1 - ‖z‖) ≤ ‖1 - z‖

Tactic:
calc
    _ ≤ 1 * (1 - ‖z‖) := by gcongr
    _ = ‖(1 : ℂ)‖ - ‖z‖ := by rw [one_mul, norm_one]
    _ ≤ _ := norm_sub_norm_le _ _

Premises used: Norm.norm, HSub.hSub, norm_sub_norm_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
M : ℝ
hM : 1 < M
⊢ Tendsto id (Filter.map ofReal (𝓝[<] 1)) (𝓝[stolzSet M] 1)

Tactic:
tendsto_map' <| tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within ofReal
    (tendsto_nhdsWithin_of_tendsto_nhds <| ofRealCLM.continuous.tendsto' 1 1 rfl) ?_

Premises used: Filter.tendsto_map', Complex.ofRealCLM, Complex.ofReal, ContinuousLinearMap.continuous, tendsto_nhdsWithin_of_tendsto_nhds, tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, Continuous.tendsto', OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
M : ℝ
hM : 1 < M
refine : ∀ᶠ (x : ℝ) in 𝓝[<] 1, (↑x : ℂ) ∈ stolzSet M
⊢ Tendsto id (Filter.map ofReal (𝓝[<] 1)) (𝓝[stolzSet M] 1)

Tactic:
refine tendsto_map' <| tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within ofReal
    (tendsto_nhdsWithin_of_tendsto_nhds <| ofRealCLM.continuous.tendsto' 1 1 rfl) ?_

Premises used: Filter.tendsto_map', Complex.ofRealCLM, Complex.ofReal, ContinuousLinearMap.continuous, tendsto_nhdsWithin_of_tendsto_nhds, tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, Continuous.tendsto', OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
M : ℝ
hM : 1 < M
simp : ∃ (u : Set ℝ), IsOpen u ∧ 1 ∈ u ∧ u ∩ Set.Iio 1 ⊆ {x : ℝ | (↑x : ℂ) ∈ stolzSet M}
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, (↑x : ℂ) ∈ stolzSet M

Tactic:
simp only [eventually_iff, mem_nhdsWithin]

Premises used: Filter.eventually_iff, mem_nhdsWithin
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
M : ℝ
hM : 1 < M
⊢ Membership.mem (γ := Set ℝ) (Set.Ioo 0 2) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
M : ℝ
hM : 1 < M
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Set.Ioo 0 2 ∩ Set.Iio 1) x),
    Membership.mem (γ := Set ℝ) {x : ℝ | (↑x : ℂ) ∈ stolzSet M} x
⊢ ∃ (u : Set ℝ), IsOpen u ∧ 1 ∈ u ∧ u ∩ Set.Iio 1 ⊆ {x : ℝ | (↑x : ℂ) ∈ stolzSet M}

Tactic:
refine ⟨Set.Ioo 0 2, isOpen_Ioo, by simp, fun x hx ↦ ?_⟩
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
M : ℝ
hM : 1 < M
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioo 0 2 ∩ Set.Iio 1) x
⊢ (0 < x ∧ x < 2) ∧ x < 1

Tactic:
push _ ∈ _ at hx
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
M : ℝ
hM : 1 < M
x : ℝ
hx : (0 < x ∧ x < 2) ∧ x < 1
simp : x < 1 ∧ 1 - x < M * (1 - x)
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | (↑x : ℂ) ∈ stolzSet M} x

Tactic:
simp only [Set.mem_setOf_eq, stolzSet, ← ofReal_one, ← ofReal_sub, norm_real,
    norm_of_nonneg hx.1.1.le, norm_of_nonneg <| (sub_pos.mpr hx.2).le]

Premises used: Iff.mpr, sub_pos, LT.lt.le, Complex.ofReal_one, Set.mem_setOf_eq, Complex.norm_real, And.right, And.left, Complex.ofReal_sub, Real.norm_of_nonneg, Complex.stolzSet
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
M : ℝ
hM : 1 < M
x : ℝ
hx : (0 < x ∧ x < 2) ∧ x < 1
⊢ x < 1 ∧ 1 - x < M * (1 - x)

Tactic:
⟨hx.2, lt_mul_left (sub_pos.mpr hx.2) hM⟩

Premises used: Iff.mpr, sub_pos, And.right, And.intro, lt_mul_left
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
M : ℝ
hM : 1 < M
x : ℝ
hx : (0 < x ∧ x < 2) ∧ x < 1
⊢ x < 1 ∧ 1 - x < M * (1 - x)

Tactic:
exact ⟨hx.2, lt_mul_left (sub_pos.mpr hx.2) hM⟩
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
⊢ 0 < 2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
⊢ 0 < 1 / (1 + HPow.hPow (β := ℕ) s 2)

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
refine :
  ∀ (x y : ℝ) (hx₀ : 0 < x) (hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)) (hy : |y| < s * x),
    √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
      (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
⊢ ∃ (M : ℝ) (ε : ℝ),
    0 < M ∧
      0 < ε ∧
        ∀ (x y : ℝ),
          0 < x →
            x < ε →
              |y| < s * x →
                √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
                  M * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))

Tactic:
refine ⟨2 * √(1 + s ^ 2) + 1, 1 / (1 + s ^ 2), by positivity, by positivity,
    fun x y hx₀ hx₁ hy ↦ ?_⟩
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
rw :
  HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) |y| 2 ≤ HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) (s * x) 2
⊢ HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) (s * x) 2

Tactic:
rw [← sq_abs y]

Premises used: sq_abs
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
bc : 0 ≤ |y|
⊢ HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) |y| 2 ≤ HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) (s * x) 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
e_x : HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) (s * x) 2 = 1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * x * x
⊢ √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) (s * x) 2) = √(1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * x * x)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
⊢ HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) (s * x) 2 = 1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * x * x

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
a : 0 ≤ x
a₁ : 0 ≤ 1 + HPow.hPow (β := ℕ) s 2
⊢ √(1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * x * x) ≤
    √(1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * (1 / (1 + HPow.hPow (β := ℕ) s 2)) * x)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
e_x : 1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * (1 / (1 + HPow.hPow (β := ℕ) s 2)) * x = 1 - x
⊢ √(1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * (1 / (1 + HPow.hPow (β := ℕ) s 2)) * x) = √(1 - x)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
⊢ 1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * (1 / (1 + HPow.hPow (β := ℕ) s 2)) * x = 1 - x

Tactic:
field
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
simp_rw : √(1 + -x) ≤ 1 + -x / 2
⊢ √(1 - x) ≤ 1 - x / 2

Tactic:
simp_rw [sub_eq_add_neg, ← neg_div]

Premises used: neg_div, sub_eq_add_neg
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
⊢ √(1 + -x) ≤ 1 + -x / 2

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

Premises used: Iff.mpr, Real.sqrt_one_add_le, LT.lt.le, LT.lt.trans_le, neg_le_neg_iff
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
refine : 1 / (1 + HPow.hPow (β := ℕ) s 2) ≤ 1
⊢ √(1 + -x) ≤ 1 + -x / 2

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

Premises used: Iff.mpr, Real.sqrt_one_add_le, LT.lt.le, LT.lt.trans_le, neg_le_neg_iff
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
⊢ 0 < 1 + HPow.hPow (β := ℕ) s 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
rw : 1 ≤ 1 + HPow.hPow (β := ℕ) s 2
⊢ 1 / (1 + HPow.hPow (β := ℕ) s 2) ≤ 1

Tactic:
rw [div_le_one (by positivity)]

Premises used: div_le_one
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
⊢ 1 ≤ 1 + HPow.hPow (β := ℕ) s 2

Tactic:
le_add_of_nonneg_right <| sq_nonneg s

Premises used: le_add_of_nonneg_right, sq_nonneg
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
⊢ 1 ≤ 1 + HPow.hPow (β := ℕ) s 2

Tactic:
exact le_add_of_nonneg_right <| sq_nonneg s

Premises used: le_add_of_nonneg_right, sq_nonneg
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
calc :
  √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) (s * x) 2) = √(1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * x * x)
calc₁ :
  √(1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * x * x) ≤
    √(1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * (1 / (1 + HPow.hPow (β := ℕ) s 2)) * x)
calc₂ : √(1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * (1 / (1 + HPow.hPow (β := ℕ) s 2)) * x) = √(1 - x)
calc₃ : √(1 - x) ≤ 1 - x / 2
⊢ √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2

Tactic:
calc √((1 - x) ^ 2 + y ^ 2)
      _ ≤ √((1 - x) ^ 2 + (s * x) ^ 2) := sqrt_le_sqrt <| by rw [← sq_abs y]; gcongr
      _ = √(1 - 2 * x + (1 + s ^ 2) * x * x) := by congr 1; ring
      _ ≤ √(1 - 2 * x + (1 + s ^ 2) * (1 / (1 + s ^ 2)) * x) := by gcongr
      _ = √(1 - x) := by congr 1; field
      _ ≤ 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

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Real.sqrt_le_sqrt, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
⊢ √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2

Tactic:
have H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2 := by
    calc √((1 - x) ^ 2 + y ^ 2)
      _ ≤ √((1 - x) ^ 2 + (s * x) ^ 2) := sqrt_le_sqrt <| by rw [← sq_abs y]; gcongr
      _ = √(1 - 2 * x + (1 + s ^ 2) * x * x) := by congr 1; ring
      _ ≤ √(1 - 2 * x + (1 + s ^ 2) * (1 / (1 + s ^ 2)) * x) := by gcongr
      _ = √(1 - x) := by congr 1; field
      _ ≤ 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
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
rw : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) |y| 2) ≤ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2)
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2)

Tactic:
rw [← sq_abs y]

Premises used: sq_abs
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
a : 0 ≤ |y|
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) |y| 2) ≤ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
e_x : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2 = (1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2) = √((1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2)

Tactic:
congr
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
⊢ HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2 = (1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
rw : √(1 + HPow.hPow (β := ℕ) s 2) * √(HPow.hPow (β := ℕ) x 2) = √(1 + HPow.hPow (β := ℕ) s 2) * x
rw₁ rw₂ : √(1 + HPow.hPow (β := ℕ) s 2) * x = √(1 + HPow.hPow (β := ℕ) s 2) * x
⊢ √((1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2) = √(1 + HPow.hPow (β := ℕ) s 2) * x

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

Premises used: LT.lt.le, sq_nonneg, Real.sqrt_sq, Real.sqrt_mul'
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
⊢ √(1 + HPow.hPow (β := ℕ) s 2) * x = 2 * √(1 + HPow.hPow (β := ℕ) s 2) * (x / 2)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
hbc : 2 * √(1 + HPow.hPow (β := ℕ) s 2) < 2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1
⊢ 2 * √(1 + HPow.hPow (β := ℕ) s 2) * (x / 2) < (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (x / 2)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
⊢ 2 * √(1 + HPow.hPow (β := ℕ) s 2) < 2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1

Tactic:
lt_add_one _

Premises used: lt_add_one
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
⊢ 2 * √(1 + HPow.hPow (β := ℕ) s 2) < 2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1

Tactic:
exact lt_add_one _

Premises used: lt_add_one
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
hbc : x / 2 ≤ 1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2)
⊢ (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (x / 2) ≤
    (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
⊢ x / 2 ≤ 1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2)

Tactic:
le_sub_comm.mpr H

Premises used: Iff.mpr, le_sub_comm
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
⊢ x / 2 ≤ 1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2)

Tactic:
exact le_sub_comm.mpr H

Premises used: Iff.mpr, le_sub_comm
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
calc : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2)
calc₁ :
  √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2) = √((1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2)
calc₂ : √((1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2) = √(1 + HPow.hPow (β := ℕ) s 2) * x
calc₃ : √(1 + HPow.hPow (β := ℕ) s 2) * x = 2 * √(1 + HPow.hPow (β := ℕ) s 2) * (x / 2)
calc₄ : 2 * √(1 + HPow.hPow (β := ℕ) s 2) * (x / 2) < (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (x / 2)
calc₅ :
  (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (x / 2) ≤
    (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
    (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))

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

Premises used: HMul.hMul, HDiv.hDiv, HPow.hPow, HAdd.hAdd, Real.sqrt, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
hs : 0 < s
h :
  ∀ (M ε : ℝ) (hM : 0 < M) (hε : 0 < ε)
    (H :
      ∀ (x y : ℝ),
        0 < x →
          x < ε →
            |y| < s * x →
              √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
                M * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))),
    {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ ∃ (M : ℝ) (ε : ℝ), 0 < M ∧ 0 < ε ∧ {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M

Tactic:
peel stolzCone_subset_stolzSet_aux' s with M ε hM hε H

Premises used: _private.0.Complex.stolzCone_subset_stolzSet_aux'
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H :
  ∀ (x y : ℝ),
    0 < x →
      x < ε →
        |y| < s * x →
          √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
            M * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
z : ℂ
hzl : Membership.mem (γ := Set ℂ) {z : ℂ | 1 - ε < z.re} z
hzr : z ∈ stolzCone s
⊢ (1 - z).re < ε

Tactic:
rw [Set.mem_setOf_eq, sub_lt_comm, ← one_re, ← sub_re] at hzl

Premises used: sub_lt_comm, Complex.sub_re, Set.mem_setOf_eq, Complex.one_re
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H :
  ∀ (x y : ℝ),
    0 < x →
      x < ε →
        |y| < s * x →
          √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
            M * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
z : ℂ
hzl : Membership.mem (γ := Set ℂ) {z : ℂ | 1 - ε < z.re} z
hzr : z ∈ stolzCone s
hzl₁ : (1 - z).re < ε
⊢ z ∈ stolzCone s

Tactic:
rw [Set.mem_setOf_eq, sub_lt_comm, ← one_re, ← sub_re] at hzl

Premises used: sub_lt_comm, Complex.sub_re, Set.mem_setOf_eq, Complex.one_re
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H :
  ∀ (x y : ℝ),
    0 < x →
      x < ε →
        |y| < s * x →
          √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
            M * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
z : ℂ
hzl : (1 - z).re < ε
hzr : z ∈ stolzCone s
⊢ |z.im| < s * (1 - z).re

Tactic:
rw [stolzCone, Set.mem_setOf_eq, ← one_re, ← sub_re] at hzr

Premises used: Complex.sub_re, Set.mem_setOf_eq, Complex.one_re, Complex.stolzCone
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H :
  ∀ (x y : ℝ),
    0 < x →
      x < ε →
        |y| < s * x →
          √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
            M * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
⊢ √(HPow.hPow (β := ℕ) (1 - z).re 2 + HPow.hPow (β := ℕ) z.im 2) <
    M * (1 - √(HPow.hPow (β := ℕ) (1 - (1 - z).re) 2 + HPow.hPow (β := ℕ) z.im 2))

Tactic:
replace H :=
    H (1 - z).re z.im ((mul_pos_iff_of_pos_left hs).mp <| (abs_nonneg z.im).trans_lt hzr) hzl hzr
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H :
  √(HPow.hPow (β := ℕ) (1 - z).re 2 + HPow.hPow (β := ℕ) z.im 2) <
    M * (1 - √(HPow.hPow (β := ℕ) (1 - (1 - z).re) 2 + HPow.hPow (β := ℕ) z.im 2))
⊢ HPow.hPow (β := ℕ) z.im 2 = HPow.hPow (β := ℕ) (1 - z).im 2

Tactic:
simp only [sub_im, one_im, zero_sub, neg_sq]

Premises used: Complex.sub_im, neg_sq, zero_sub, Complex.one_im