awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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' : 𝕜 → G
x : 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : TendstoLocallyUniformlyOn (deriv ∘ f) g' l s
hf : ∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s
hfg : ∀ x ∈ s, Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
hx : x ∈ s
⊢ ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) ((deriv ∘ f) n x) x
have h : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x : ι |
      Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ DifferentiableOn 𝕜 (f n) s) x} x →
        Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ ∀ x ∈ s, HasDerivAt (f n) ((deriv ∘ f) n x) x) x} x}
    a
Tactic: filter_upwards [hf] with n h z hz using ((h z hz).differentiableAt (hs.mem_nhds hz)).hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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' : 𝕜 → G
x : 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : TendstoLocallyUniformlyOn (deriv ∘ f) g' l s
hf : ∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s
hfg : ∀ x ∈ s, Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
hx : x ∈ s
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ DifferentiableOn 𝕜 (f n) s) x} x →
          Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ ∀ x ∈ s, HasDerivAt (f n) ((deriv ∘ f) n x) x) x} x}
      a
⊢ ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) ((deriv ∘ f) n x) x
have h₁ : ∀ (a : ι), DifferentiableOn 𝕜 (f a) s → ∀ x ∈ s, HasDerivAt (f a) ((deriv ∘ f) a x) x
Tactic: filter_upwards [hf] with n h z hz using ((h z hz).differentiableAt (hs.mem_nhds hz)).hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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 : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x
hfg : ∀ (x : 𝕜), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x : 𝕜
⊢ ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x
have h : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x : ι |
      Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x) x} x →
        Membership.mem (γ := Set ι)
          {x : ι | (fun (n : ι) ↦ ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x) x} x}
    a
Tactic: filter_upwards [hf] with n h x _ using h x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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 : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x
hfg : ∀ (x : 𝕜), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x : 𝕜
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x) x} x →
          Membership.mem (γ := Set ι)
            {x : ι | (fun (n : ι) ↦ ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x) x}
            x}
      a
⊢ ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x
have h₁ : ∀ (a : ι),
  (∀ (x : 𝕜), HasDerivAt (f a) (f' a x) x) →
    ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f a) (f' a x) x
Tactic: filter_upwards [hf] with n h x _ using h x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
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 : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x
hfg : ∀ (x : 𝕜), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x : 𝕜
⊢ HasDerivAt g (g' x) x
have hf₁ : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x
Tactic: have hf : ∀ᶠ n in l, ∀ x : 𝕜, x ∈ Set.univ → HasDerivAt (f n) (f' n x) x := by
    filter_upwards [hf] with n h x _ using h x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
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 : ∀ (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
⊢ HasDerivAt g (g' x) x
have hfg₁ : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
Tactic: have hfg : ∀ x : 𝕜, x ∈ Set.univ → Tendsto (fun n => f n x) l (𝓝 (g x)) := by simp [hfg]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
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))
⊢ HasDerivAt g (g' x) x
have hf'₁ : TendstoUniformlyOn f' g' l Set.univ
Tactic: have hf' : TendstoUniformlyOn f' g' l Set.univ := by rwa [tendstoUniformlyOn_univ]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
M : ℝ
hM : M ≤ 1
⊢ stolzSet M = ∅
have h : ∀ (z : ℂ), z ∈ stolzSet M ↔ Membership.mem (γ := Set ℂ) ∅ z
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
M : ℝ
hM : M ≤ 1
z : ℂ
⊢ z ∈ stolzSet M ↔ Membership.mem (γ := Set ℂ) ∅ z
have h : 0 < 1 - ‖z‖ → M * (1 - ‖z‖) ≤ ‖1 - z‖
Tactic: rw [stolzSet, Set.mem_setOf, Set.mem_empty_iff_false, iff_false, not_and, not_lt, ← sub_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
M : ℝ
hM : M ≤ 1
z : ℂ
zn : 0 < 1 - ‖z‖
⊢ M * (1 - ‖z‖) ≤ 1 * (1 - ‖z‖)
have ha : 0 ≤ 1 - ‖z‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
M : ℝ
hM : M ≤ 1
z : ℂ
zn : 0 < 1 - ‖z‖
⊢ 1 * (1 - ‖z‖) = Norm.norm (E := ℂ) 1 - ‖z‖
have rw : 1 - ‖z‖ = Norm.norm (E := ℂ) 1 - ‖z‖
Tactic: rw [one_mul, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
M : ℝ
hM : M ≤ 1
z : ℂ
zn : 0 < 1 - ‖z‖
rw : 1 - ‖z‖ = Norm.norm (E := ℂ) 1 - ‖z‖
⊢ 1 * (1 - ‖z‖) = Norm.norm (E := ℂ) 1 - ‖z‖
have rw₁ : 1 - ‖z‖ = 1 - ‖z‖
Tactic: rw [one_mul, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
M : ℝ
hM : M ≤ 1
z : ℂ
zn : 0 < 1 - ‖z‖
⊢ M * (1 - ‖z‖) ≤ ‖1 - z‖
have _ : M * (1 - ‖z‖) ≤ 1 * (1 - ‖z‖)
Tactic: calc
    _ ≤ 1 * (1 - ‖z‖) := by gcongr
    _ = ‖(1 : ℂ)‖ - ‖z‖ := by rw [one_mul, norm_one]
    _ ≤ _ := norm_sub_norm_le _ _
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
M : ℝ
hM : M ≤ 1
z : ℂ
zn : 0 < 1 - ‖z‖
_ : M * (1 - ‖z‖) ≤ 1 * (1 - ‖z‖)
⊢ M * (1 - ‖z‖) ≤ ‖1 - z‖
have _₁ : 1 * (1 - ‖z‖) = Norm.norm (E := ℂ) 1 - ‖z‖
Tactic: calc
    _ ≤ 1 * (1 - ‖z‖) := by gcongr
    _ = ‖(1 : ℂ)‖ - ‖z‖ := by rw [one_mul, norm_one]
    _ ≤ _ := norm_sub_norm_le _ _
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
M : ℝ
hM : 1 < M
⊢ Tendsto id (Filter.map ofReal (𝓝[<] 1)) (𝓝[stolzSet M] 1)
have refine : ∀ᶠ (x : ℝ) in 𝓝[<] 1, (↑x : ℂ) ∈ stolzSet M
Tactic: refine tendsto_map' <| tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within ofReal
    (tendsto_nhdsWithin_of_tendsto_nhds <| ofRealCLM.continuous.tendsto' 1 1 rfl) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
M : ℝ
hM : 1 < M
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, (↑x : ℂ) ∈ stolzSet M
have simp : ∃ (u : Set ℝ), IsOpen u ∧ 1 ∈ u ∧ u ∩ Set.Iio 1 ⊆ {x : ℝ | (↑x : ℂ) ∈ stolzSet M}
Tactic: simp only [eventually_iff, mem_nhdsWithin]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
M : ℝ
hM : 1 < M
⊢ ∃ (u : Set ℝ), IsOpen u ∧ 1 ∈ u ∧ u ∩ Set.Iio 1 ⊆ {x : ℝ | (↑x : ℂ) ∈ stolzSet M}
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Set.Ioo 0 2 ∩ Set.Iio 1) x),
  Membership.mem (γ := Set ℝ) {x : ℝ | (↑x : ℂ) ∈ stolzSet M} x
Tactic: refine ⟨Set.Ioo 0 2, isOpen_Ioo, by simp, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
Goal:
M : ℝ
hM : 1 < M
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioo 0 2 ∩ Set.Iio 1) x
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | (↑x : ℂ) ∈ stolzSet M} x
have hx₁ : (0 < x ∧ x < 2) ∧ x < 1
Tactic: push _ ∈ _ at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
M : ℝ
hM : 1 < M
x : ℝ
hx : (0 < x ∧ x < 2) ∧ x < 1
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | (↑x : ℂ) ∈ stolzSet M} x
have simp : x < 1 ∧ 1 - x < M * (1 - 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
s : ℝ
⊢ ∃ (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))
have 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))
Tactic: refine ⟨2 * √(1 + s ^ 2) + 1, 1 / (1 + s ^ 2), by positivity, by positivity,
    fun x y hx₀ hx₁ hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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 ≤ HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) (s * x) 2
have rw : HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) |y| 2 ≤ HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) (s * x) 2
Tactic: rw [← sq_abs y]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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 ≤ HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) (s * x) 2
have bc : 0 ≤ |y|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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)
have e_x : HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) (s * x) 2 = 1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * x * x
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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) * x * x) ≤
    √(1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * (1 / (1 + HPow.hPow (β := ℕ) s 2)) * x)
have a : 0 ≤ x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
a : 0 ≤ x
⊢ √(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)
have a₁ : 0 ≤ 1 + HPow.hPow (β := ℕ) s 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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)
have e_x : 1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * (1 / (1 + HPow.hPow (β := ℕ) s 2)) * x = 1 - x
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
⊢ √(1 - x) ≤ 1 - x / 2
have simp_rw : √(1 + -x) ≤ 1 + -x / 2
Tactic: simp_rw [sub_eq_add_neg, ← neg_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
⊢ √(1 + -x) ≤ 1 + -x / 2
have refine : 1 / (1 + HPow.hPow (β := ℕ) s 2) ≤ 1
Tactic: refine sqrt_one_add_le <| neg_le_neg_iff.mpr (hx₁.trans_le ?_).le
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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) ≤ 1
have rw : 1 ≤ 1 + HPow.hPow (β := ℕ) s 2
Tactic: rw [div_le_one (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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
have calc : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) (s * x) 2) = √(1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * x * x)
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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)
⊢ √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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)
⊢ √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
have calc₂ : √(1 - 2 * x + (1 + HPow.hPow (β := ℕ) s 2) * (1 / (1 + HPow.hPow (β := ℕ) s 2)) * x) = √(1 - x)
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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)
⊢ √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
have calc₃ : √(1 - x) ≤ 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
Goal:
s 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))
have H : √(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
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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 (β := ℕ) y 2) ≤ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2)
have rw : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) |y| 2) ≤ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2)
Tactic: rw [← sq_abs y]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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 (β := ℕ) |y| 2) ≤ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2)
have a : 0 ≤ |y|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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)
have e_x : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2 = (1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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) * HPow.hPow (β := ℕ) x 2) = √(1 + HPow.hPow (β := ℕ) s 2) * x
have rw : √(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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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
⊢ √((1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2) = √(1 + HPow.hPow (β := ℕ) s 2) * x
have rw₁ : √(1 + HPow.hPow (β := ℕ) s 2) * x = √(1 + HPow.hPow (β := ℕ) s 2) * x
Tactic: rw [sqrt_mul' _ (sq_nonneg x), sqrt_sq hx₀.le]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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) * (x / 2) < (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (x / 2)
have hbc : 2 * √(1 + HPow.hPow (β := ℕ) s 2) < 2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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) + 1) * (x / 2) ≤
    (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
have hbc : x / 2 ≤ 1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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 (β := ℕ) y 2) <
    (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
have calc : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 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