awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x : ℝ
x_1 : 𝕜
⊢ (RCLike.complexRingEquiv h).toFun (x • x_1) =
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) x : ℝ) ((RCLike.complexRingEquiv h).toFun x_1)
have simp : (↑x : ℂ) * (↑((RCLike.im : (a : 𝕜) → ℝ) x_1) : ℂ) * I = (↑x : ℂ) * ((↑((RCLike.im : (a : 𝕜) → ℝ) x_1) : ℂ) * I)
Tactic: simp [RCLike.smul_re, RCLike.smul_im, ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
x : 𝕜
⊢ norm (E := ℂ)
      (({ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯,
              invFun := (RCLike.complexRingEquiv h).invFun, left_inv := ⋯, right_inv := ⋯ : 𝕜 ≃ₗ[ℝ] ℂ } :
            (a : 𝕜) → ℂ)
          x :
        ℂ) =
    ‖x‖
have rw : (normSq : (a : ℂ) → ℝ)
    (({ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := sorry, map_smul' := sorry,
            invFun := (RCLike.complexRingEquiv h).invFun, left_inv := sorry, right_inv := sorry } :
          (a : 𝕜) → ℂ)
        x :
      ℂ) =
  HMul.hMul (α := ℝ) (β := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) x : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) x : ℝ) +
    HMul.hMul (α := ℝ) (β := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) x : ℝ) ((RCLike.im : (a : 𝕜) → ℝ) x : ℝ)
Tactic: rw [← sq_eq_sq₀ (by positivity) (by positivity), ← normSq_eq_norm_sq, ← RCLike.normSq_eq_def',
      RCLike.normSq_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
a : 𝕜
⊢ ‖(↑((RCLike.re : (a : 𝕜) → ℝ) a) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) a) : ℂ) * I‖ = ‖a‖
have inl : ∀ (h : Eq.{u_2 + 1} (α := 𝕜) RCLike.I 0),
  ‖(↑((RCLike.re : (a : 𝕜) → ℝ) a) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) a) : ℂ) * I‖ = ‖a‖
Tactic: obtain (h | h) := RCLike.I_eq_zero_or_im_I_eq_one (K := 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
a : 𝕜
inl :
  ∀ (h : Eq.{u_2 + 1} (α := 𝕜) RCLike.I 0),
    ‖(↑((RCLike.re : (a : 𝕜) → ℝ) a) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) a) : ℂ) * I‖ = ‖a‖
⊢ ‖(↑((RCLike.re : (a : 𝕜) → ℝ) a) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) a) : ℂ) * I‖ = ‖a‖
have inr : ∀ (h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)),
  ‖(↑((RCLike.re : (a : 𝕜) → ℝ) a) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) a) : ℂ) * I‖ = ‖a‖
Tactic: obtain (h | h) := RCLike.I_eq_zero_or_im_I_eq_one (K := 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
a : 𝕜
h : Eq.{u_2 + 1} (α := 𝕜) RCLike.I 0
⊢ ‖(↑((RCLike.re : (a : 𝕜) → ℝ) a) : ℂ) + (↑((RCLike.im : (a : 𝕜) → ℝ) a) : ℂ) * I‖ = ‖a‖
have inl : ‖(↑((RCLike.re : (a : 𝕜) → ℝ) ((↑((RCLike.re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑0 : 𝕜) RCLike.I)) : ℂ) +
      (↑((RCLike.im : (a : 𝕜) → ℝ) ((↑((RCLike.re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑0 : 𝕜) RCLike.I)) : ℂ) *
        I‖ =
  ‖(↑((RCLike.re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑0 : 𝕜) RCLike.I‖
Tactic: rw [← RCLike.re_add_im a, RCLike.im_eq_zero h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
⊢ ∀ (x y : ℤ), dist (α := ℂ) (↑x : ℂ) (↑y : ℂ) = dist x y
have simp_rw : ∀ (x y : ℤ), dist (↑(↑x : ℝ) : ℂ) (↑(↑y : ℝ) : ℂ) = dist x y
Tactic: simp_rw [← Complex.ofReal_intCast,
    Complex.isometry_ofReal.dist_eq, Int.dist_cast_real, implies_true]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
simp_rw : ∀ (x y : ℤ), dist (↑(↑x : ℝ) : ℂ) (↑(↑y : ℝ) : ℂ) = dist x y
⊢ ∀ (x y : ℤ), dist (α := ℂ) (↑x : ℂ) (↑y : ℂ) = dist x y
have simp_rw₁ : ∀ (x y : ℤ), dist (α := ℝ) (↑x : ℝ) (↑y : ℝ) = dist x y
Tactic: simp_rw [← Complex.ofReal_intCast,
    Complex.isometry_ofReal.dist_eq, Int.dist_cast_real, implies_true]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
simp_rw : ∀ (x y : ℤ), dist (↑(↑x : ℝ) : ℂ) (↑(↑y : ℝ) : ℂ) = dist x y
simp_rw₁ : ∀ (x y : ℤ), dist (α := ℝ) (↑x : ℝ) (↑y : ℝ) = dist x y
⊢ ∀ (x y : ℤ), dist (α := ℂ) (↑x : ℂ) (↑y : ℂ) = dist x y
have simp_rw₂ : ∀ (x y : ℤ), True
Tactic: simp_rw [← Complex.ofReal_intCast,
    Complex.isometry_ofReal.dist_eq, Int.dist_cast_real, implies_true]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
hz : 0 ≤ z
⊢ z = (↑‖z‖ : ℂ)
have lift : ∀ (z : ℝ) (hz : 0 ≤ (↑z : ℂ)), (↑z : ℂ) = (↑‖(↑z : ℂ)‖ : ℂ)
Tactic: lift z to ℝ using hz.2.symm
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℝ
hz : 0 ≤ (↑z : ℂ)
⊢ (↑z : ℂ) = (↑‖(↑z : ℂ)‖ : ℂ)
have rw : (↑z : ℂ) = (↑‖z‖ : ℂ)
Tactic: rw [norm_real, Real.norm_of_nonneg (id hz.1 : 0 ≤ z)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℝ
hz : 0 ≤ (↑z : ℂ)
rw : (↑z : ℂ) = (↑‖z‖ : ℂ)
⊢ (↑z : ℂ) = (↑‖(↑z : ℂ)‖ : ℂ)
have rw₁ : (↑z : ℂ) = (↑z : ℂ)
Tactic: rw [norm_real, Real.norm_of_nonneg (id hz.1 : 0 ≤ z)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
x : ℂ
hx : IsSelfAdjoint x
⊢ 0 ≤ x.re ↔ 0 ≤ x
have rw : LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : ℂ) → ℝ) x : ℝ) ↔ 0 ≤ x
Tactic: rw [← RCLike.re_eq_complex_re]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (hypothesis)
Goal:
x y : ℂ
h : x ≤ y
⊢ x.re ≤ y.re
have h₁ : LE.le (α := ℝ) ((RCLike.re : (a : ℂ) → ℝ) x : ℝ) ((RCLike.re : (a : ℂ) → ℝ) y : ℝ) ∧
  Eq (α := ℝ) ((RCLike.im : (a : ℂ) → ℝ) x : ℝ) ((RCLike.im : (a : ℂ) → ℝ) y : ℝ)
Tactic: rw [RCLike.le_iff_re_im] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
L : SummationFilter α
f : α → 𝕜
c : 𝕜
⊢ HasSum f c L ↔
    HasSum (α := ℝ) (fun (x : α) ↦ ((re : (a : 𝕜) → ℝ) (f x) : ℝ)) ((re : (a : 𝕜) → ℝ) c : ℝ) L ∧
      HasSum (α := ℝ) (fun (x : α) ↦ ((im : (a : 𝕜) → ℝ) (f x) : ℝ)) ((im : (a : 𝕜) → ℝ) c : ℝ) L
have refine : HasSum (α := ℝ) (fun (x : α) ↦ ((re : (a : 𝕜) → ℝ) (f x) : ℝ)) ((re : (a : 𝕜) → ℝ) c : ℝ) L ∧
    HasSum (α := ℝ) (fun (x : α) ↦ ((im : (a : 𝕜) → ℝ) (f x) : ℝ)) ((im : (a : 𝕜) → ℝ) c : ℝ) L →
  HasSum f c L
Tactic: refine ⟨fun h => ⟨hasSum_re _ h, hasSum_im _ h⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
⊢ (0 < z.re ∨ z.im ≠ 0) ∨ 0 < (-z).re ∨ (-z).im ≠ 0
have hz₁ : ¬(z.re = re 0 ∧ z.im = im 0)
Tactic: rw [ne_eq, Complex.ext_iff] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (hypothesis)
Goal:
z : ℂ
hz : ¬(z.re = re 0 ∧ z.im = im 0)
⊢ (0 < z.re ∨ z.im ≠ 0) ∨ 0 < (-z).re ∨ (-z).im ≠ 0
have hz₁ : ∀ (_ : z.re = re 0), z.im ≠ im 0
Tactic: push Not at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
hz : ∀ (_ : z.re = re 0), z.im ≠ im 0
⊢ (0 < z.re ∨ z.im ≠ 0) ∨ 0 < (-z).re ∨ (-z).im ≠ 0
have simp_all : ∀ (hz : ∀ (_ : z.re = 0), ¬z.im = 0), (0 < z.re ∨ ¬z.im = 0) ∨ z.re < 0 ∨ ¬z.im = 0
Tactic: simp_all only [ne_eq, zero_re, zero_im, neg_re, Left.neg_pos_iff, neg_im, neg_eq_zero]
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
hz : ∀ (_ : z.re = 0), ¬z.im = 0
⊢ (0 < z.re ∨ ¬z.im = 0) ∨ z.re < 0 ∨ ¬z.im = 0
have by_contra! : ∀ (contra : (z.re ≤ 0 ∧ z.im = 0) ∧ 0 ≤ z.re ∧ z.im = 0), False
Tactic: by_contra! contra
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
z : ℂ
hz : Membership.mem (γ := Set ℂ) (Metric.ball 1 1) z
⊢ z ∈ slitPlane
have h : 0 < z.re
Tactic: apply Or.inl
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
⊢ s ⊆ slitPlane ↔ -(↑r : ℂ) ∉ s
have simp_rw : (∀ x ∈ s, ¬x ≤ 0) ↔ -(↑r : ℂ) ∉ s
Tactic: simp_rw [Set.subset_def, mem_slitPlane_iff_not_le_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
⊢ (∀ x ∈ s, ¬x ≤ 0) ↔ -(↑r : ℂ) ∉ s
have contrapose! : (∃ x ∈ s, x ≤ 0) ↔ -(↑r : ℂ) ∈ s
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
⊢ (∃ x ∈ s, x ≤ 0) ↔ -(↑r : ℂ) ∈ s
have refine : (∃ x ∈ s, x ≤ 0) → -(↑r : ℂ) ∈ s
Tactic: refine ⟨?_, fun hr ↦ ⟨_, hr, by simpa using hs hr⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (hypothesis)
Goal:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
z : ℂ
hzs : z ∈ s
hz : z ≤ 0
⊢ -(↑r : ℂ) ∈ s
have this : ‖z‖ = r
Tactic: have : ‖z‖ = r := by simpa using hs hzs
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
A : Type u_1
inst : SeminormedAddCommGroup A
inst_1 : StarAddMonoid A
inst_2 : NormedSpace ℂ A
inst_3 : StarModule ℂ A
inst_4 : NormedStarGroup A
x : A
⊢ norm (E := ↥(selfAdjoint A))
      (((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x : ↥(selfAdjoint A)) ≤
    ‖x‖
have rw : 2⁻¹ * ‖x + star x‖ ≤ 2⁻¹ * (2 * ‖x‖)
Tactic: rw [← inv_mul_cancel_left₀ two_ne_zero ‖x‖, ← AddSubgroup.norm_coe, realPart_apply_coe,
    norm_smul, norm_inv, Real.norm_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
A : Type u_1
inst : SeminormedAddCommGroup A
inst_1 : StarAddMonoid A
inst_2 : NormedSpace ℂ A
inst_3 : StarModule ℂ A
inst_4 : NormedStarGroup A
x : A
⊢ 2⁻¹ * ‖x + star x‖ ≤ 2⁻¹ * (2 * ‖x‖)
have hbc : ‖x + star x‖ ≤ 2 * ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
A : Type u_1
inst : SeminormedAddCommGroup A
inst_1 : StarAddMonoid A
inst_2 : NormedSpace ℂ A
inst_3 : StarModule ℂ A
inst_4 : NormedStarGroup A
x : A
⊢ norm (E := ↥(selfAdjoint A))
      (((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x : ↥(selfAdjoint A)) ≤
    ‖x‖
have calc : norm (E := ↥(selfAdjoint A))
    (((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x : ↥(selfAdjoint A)) =
  norm (E := ↥(selfAdjoint A))
    (((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (Complex.I • -x) : ↥(selfAdjoint A))
Tactic: calc ‖imaginaryPart x‖ = ‖realPart (Complex.I • (-x))‖ := by simp
    _ ≤ ‖x‖ := by simpa only [smul_neg, map_neg, realPart_I_smul, neg_neg,
        AddSubgroupClass.coe_norm, norm_neg, norm_smul, Complex.norm_I, one_mul] using
        realPart.norm_le (Complex.I • (-x))
-- Lean 4 proof step from Mathlib.Analysis.Complex.Basic (goal)
Goal:
A : Type u_1
inst : SeminormedAddCommGroup A
inst_1 : StarAddMonoid A
inst_2 : NormedSpace ℂ A
inst_3 : StarModule ℂ A
inst_4 : NormedStarGroup A
x : A
calc :
  norm (E := ↥(selfAdjoint A))
      (((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x : ↥(selfAdjoint A)) =
    norm (E := ↥(selfAdjoint A))
      (((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (Complex.I • -x) : ↥(selfAdjoint A))
⊢ norm (E := ↥(selfAdjoint A))
      (((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x : ↥(selfAdjoint A)) ≤
    ‖x‖
have calc₁ : norm (E := ↥(selfAdjoint A))
    (((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (Complex.I • -x) : ↥(selfAdjoint A)) ≤
  ‖x‖
Tactic: calc ‖imaginaryPart x‖ = ‖realPart (Complex.I • (-x))‖ := by simp
    _ ≤ ‖x‖ := by simpa only [smul_neg, map_neg, realPart_I_smul, neg_neg,
        AddSubgroupClass.coe_norm, norm_neg, norm_smul, Complex.norm_I, one_mul] using
        realPart.norm_le (Complex.I • (-x))
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
M : ℝ
z w : ℂ
h_1 : M ≠ 0
h_2 : 2 * (↑M : ℂ) - z ≠ 0
h : w = z / (2 * (↑M : ℂ) - z)
⊢ z = 2 * (↑M : ℂ) * w / (1 + w)
have rw : z = 2 * (↑M : ℂ) * (z / (2 * (↑M : ℂ) - z)) / (1 + z / (2 * (↑M : ℂ) - z))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
M : ℝ
z w : ℂ
h_1 : M ≠ 0
h_2 : 2 * (↑M : ℂ) - z ≠ 0
h : w = z / (2 * (↑M : ℂ) - z)
⊢ z = 2 * (↑M : ℂ) * (z / (2 * (↑M : ℂ) - z)) / (1 + z / (2 * (↑M : ℂ) - z))
have field_simp : z = z * 2 * (↑M : ℂ) / (2 * (↑M : ℂ) - z + z)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
M : ℝ
z w : ℂ
h_1 : M ≠ 0
h_2 : 2 * (↑M : ℂ) - z ≠ 0
h : w = z / (2 * (↑M : ℂ) - z)
⊢ z = z * 2 * (↑M : ℂ) / (2 * (↑M : ℂ) - z + z)
have ring_nf : z = z * (↑M : ℂ) * (↑M : ℂ)⁻¹
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
M : ℝ
z w : ℂ
h_1 : M ≠ 0
h_2 : 2 * (↑M : ℂ) - z ≠ 0
h : w = z / (2 * (↑M : ℂ) - z)
⊢ z = z * (↑M : ℂ) * (↑M : ℂ)⁻¹
have h₁ : (↑M : ℂ) ≠ 0
Tactic: rw [mul_inv_cancel_right₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
M : ℝ
z w : ℂ
h_1 : M ≠ 0
h_2 : 2 * (↑M : ℂ) - z ≠ 0
h : w = z / (2 * (↑M : ℂ) - z)
⊢ (↑M : ℂ) ≠ 0
have h₁ : ¬M = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
⊢ ‖2 * (↑M : ℂ) * w / (1 + w)‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
have simp : 2 * M * ‖w‖ / ‖1 + w‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
Tactic: simp only [norm_div, norm_mul, norm_ofNat, norm_real, Real.norm_eq_abs, abs_of_pos hM]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
⊢ 2 * M * ‖w‖ / ‖1 + w‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
have hdb : 1 - ‖w‖ ≤ ‖1 + w‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
⊢ 1 - ‖w‖ ≤ ‖1 + w‖
have hdb : norm (E := ℂ) 1 - ‖w‖ ≤ ‖1 + w‖
Tactic: rw [← norm_one (α := ℂ)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
M : ℝ
z : ℂ
h : 0 < M
h_1 : z.re ≤ M
⊢ ‖z‖ ≤ ‖2 * (↑M : ℂ) - z‖
have rw : HPow.hPow (β := ℕ) ‖z‖ 2 ≤ HPow.hPow (β := ℕ) ‖2 * (↑M : ℂ) - z‖ 2
Tactic: rw [← sq_le_sq₀ (by positivity) (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
M : ℝ
z : ℂ
h : 0 < M
h_1 : z.re ≤ M
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 ≤ HPow.hPow (β := ℕ) ‖2 * (↑M : ℂ) - z‖ 2
have suffices : z.re * z.re ≤ (2 * M - z.re) * (2 * M - z.re)
Tactic: suffices z.re * z.re ≤ (2 * M - z.re) * (2 * M - z.re) by simpa [Complex.sq_norm, normSq_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
M : ℝ
z : ℂ
h : 0 < M
h_1 : z.re ≤ M
⊢ z.re * z.re ≤ (2 * M - z.re) * (2 * M - z.re)
have nlinarith : (2 * M - z.re) * (2 * M - z.re) < z.re * z.re →
  (2 * M - z.re) * (2 * M - z.re) - z.re * z.re + 4 * (0 - (0 - M) * (z.re - M)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
M : ℝ
z : ℂ
h : 0 < M
h_1 : z.re ≤ M
nlinarith :
  (2 * M - z.re) * (2 * M - z.re) < z.re * z.re →
    (2 * M - z.re) * (2 * M - z.re) - z.re * z.re + 4 * (0 - (0 - M) * (z.re - M)) = 0
⊢ z.re * z.re ≤ (2 * M - z.re) * (2 * M - z.re)
have nlinarith₁ : (2 * M - z.re) * (2 * M - z.re) < z.re * z.re → GT.gt (α := ℝ) 4 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
⊢ ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ 1 / R * ‖z‖
have rw : dist (f z / (2 * (↑M : ℂ) - f z)) 0 ≤ 1 / R * dist z 0
Tactic: rw [← dist_zero_right, ← dist_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
⊢ dist (f z / (2 * (↑M : ℂ) - f z)) 0 ≤ 1 / R * dist z 0
have nth_rw : dist (f z / (2 * (↑M : ℂ) - f z)) (f 0 / (2 * (↑M : ℂ) - f 0)) ≤ 1 / R * dist z 0
Tactic: nth_rw 1 [← zero_div (2 * M - f 0), ← hf₂]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
⊢ dist (f z / (2 * (↑M : ℂ) - f z)) (f 0 / (2 * (↑M : ℂ) - f 0)) ≤ 1 / R * dist z 0
have apply : DifferentiableOn ℂ (F := ℂ) (fun {z : ℂ} ↦ f z / (2 * (↑M : ℂ) - f z)) (ball 0 R)
Tactic: apply dist_le_div_mul_dist_of_mapsTo_ball (R₂ := 1) ?_ (fun x hx ↦ ?_) hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
apply : DifferentiableOn ℂ (F := ℂ) (fun {z : ℂ} ↦ f z / (2 * (↑M : ℂ) - f z)) (ball 0 R)
⊢ dist (f z / (2 * (↑M : ℂ) - f z)) (f 0 / (2 * (↑M : ℂ) - f 0)) ≤ 1 / R * dist z 0
have apply₁ : ∀ (x : ℂ) (hx : Membership.mem (γ := Set ℂ) (ball 0 R) x),
  f x / (2 * (↑M : ℂ) - f x) ∈ closedBall (f 0 / (2 * (↑M : ℂ) - f 0)) 1
Tactic: apply dist_le_div_mul_dist_of_mapsTo_ball (R₂ := 1) ?_ (fun x hx ↦ ?_) hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
⊢ DifferentiableOn ℂ (F := ℂ) (fun {z : ℂ} ↦ f z / (2 * (↑M : ℂ) - f z)) (ball 0 R)
have apply : ∀ (x : ℂ) (hx : Membership.mem (γ := Set ℂ) (ball 0 R) x) (h : 2 * (↑M : ℂ) - f x = 0), False
Tactic: apply hf.div (hf.const_sub _) fun x hx h ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (hypothesis)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
x : ℂ
hx : Membership.mem (γ := Set ℂ) (ball 0 R) x
h : 2 * (↑M : ℂ) - f x = 0
⊢ False
have this : Membership.mem (γ := Set ℂ) {z : ℂ | z.re ≤ M} (2 * (↑M : ℂ))
Tactic: have := sub_eq_zero.mp h ▸ hf₁ hx
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (hypothesis)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
w : ℂ := f z / (2 * (↑M : ℂ) - f z)
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)
have hzR : ‖z‖ < R
Tactic: have hzR : ‖z‖ < R := mem_ball_zero_iff.mp hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (hypothesis)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
w : ℂ := f z / (2 * (↑M : ℂ) - f z)
hzR : ‖z‖ < R
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)
have hwR : ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ ‖z‖ / R
Tactic: have hwR := by simpa only [dist_zero_right, div_one, mul_comm (1 / R), mul_one_div]
    using schwarz_applied hM hf hf₁ hz hf₂
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (hypothesis)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
w : ℂ := f z / (2 * (↑M : ℂ) - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ ‖z‖ / R
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)
have h_denom : 2 * (↑M : ℂ) - f z ≠ 0
Tactic: have h_denom : 2 * M - f z ≠ 0 := sub_ne_zero_of_ne (fun h => by simpa [← h, hM] using hf₁ hz)
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
w : ℂ := f z / (2 * (↑M : ℂ) - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * (↑M : ℂ) - f z ≠ 0
⊢ ‖f z‖ = ‖2 * (↑M : ℂ) * w / (1 + w)‖
have rw : ‖2 * (↑M : ℂ) * (f z / (2 * (↑M : ℂ) - f z)) / (1 + f z / (2 * (↑M : ℂ) - f z))‖ = ‖2 * (↑M : ℂ) * w / (1 + w)‖
Tactic: rw [eq_mul_div_one_add_of_eq_div_sub hM.ne' h_denom rfl]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
w : ℂ := f z / (2 * (↑M : ℂ) - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * (↑M : ℂ) - f z ≠ 0
⊢ ‖2 * (↑M : ℂ) * w / (1 + w)‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
have simp : 2 * M * ‖w‖ / ‖1 + w‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
Tactic: simp only [norm_div, norm_mul, norm_ofNat, norm_real, Real.norm_eq_abs, abs_of_pos hM]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
w : ℂ := f z / (2 * (↑M : ℂ) - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * (↑M : ℂ) - f z ≠ 0
⊢ 2 * M * ‖w‖ / ‖1 + w‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
have hd : 0 < 1 - ‖w‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
w : ℂ := f z / (2 * (↑M : ℂ) - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * (↑M : ℂ) - f z ≠ 0
hd : 0 < 1 - ‖w‖
⊢ 2 * M * ‖w‖ / ‖1 + w‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
have hdb : 1 - ‖w‖ ≤ ‖1 + w‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
w : ℂ := f z / (2 * (↑M : ℂ) - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * (↑M : ℂ) - f z ≠ 0
⊢ 0 < 1 - ‖w‖
have linarith : 1 - ‖w‖ ≤ 0 → 1 - ‖w‖ - 0 + (1 * ‖f z / (2 * (↑M : ℂ) - f z)‖ - HMul.hMul (α := ℝ) 1 1) = 0
Tactic: linarith [hwR.trans_lt ((div_lt_one₀ hR).mpr hzR)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
w : ℂ := f z / (2 * (↑M : ℂ) - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * (↑M : ℂ) - f z ≠ 0
⊢ 2 * M * (‖w‖ / (1 - ‖w‖)) ≤ 2 * M * (‖z‖ / R / (1 - ‖z‖ / R))
have hbc : 0 < 1 - ‖z‖ / R
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
w : ℂ := f z / (2 * (↑M : ℂ) - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * (↑M : ℂ) - f z ≠ 0
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)
have calc : ‖f z‖ = ‖2 * (↑M : ℂ) * w / (1 + w)‖
Tactic: calc ‖f z‖
    _ = ‖2 * M * w / (1 + w)‖ := by rw [eq_mul_div_one_add_of_eq_div_sub hM.ne' h_denom rfl]
    _ ≤ 2 * M * ‖w‖ / (1 - ‖w‖) := by
      simp only [norm_div, norm_mul, norm_ofNat, norm_real, Real.norm_eq_abs, abs_of_pos hM]
      gcongr
      · linarith [hwR.trans_lt ((div_lt_one₀ hR).mpr hzR)]
      · simpa using norm_sub_le_norm_add 1 w
    _ = 2 * M * (‖w‖ / (1 - ‖w‖)) := by ring
    _ ≤ 2 * M * (‖z‖ / R / (1 - ‖z‖ / R)) := by gcongr; simpa [div_lt_one hR]
    _ = 2 * M * ‖z‖ / (R - ‖z‖) := by field_simp