awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Basic
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

Tactic:
⟨fun h => ⟨hasSum_re _ h, hasSum_im _ h⟩, ?_⟩

Premises used: RCLike.hasSum_re, And.intro, Iff.intro, RCLike.hasSum_im
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
L : SummationFilter α
f : α → 𝕜
c : 𝕜
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
⊢ 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

Tactic:
refine ⟨fun h => ⟨hasSum_re _ h, hasSum_im _ h⟩, ?_⟩
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
L : SummationFilter α
f : α → 𝕜
c : 𝕜
h₁ : HasSum (α := ℝ) (fun (x : α) ↦ ((re : (a : 𝕜) → ℝ) (f x) : ℝ)) ((re : (a : 𝕜) → ℝ) c : ℝ) L
h₂ : HasSum (α := ℝ) (fun (x : α) ↦ ((im : (a : 𝕜) → ℝ) (f x) : ℝ)) ((im : (a : 𝕜) → ℝ) c : ℝ) L
⊢ HasSum f c L

Tactic:
simpa only [re_add_im] using
    ((hasSum_ofReal 𝕜).mpr h₁).add (((hasSum_ofReal 𝕜).mpr h₂).mul_right I)

Premises used: Iff.mpr, RCLike.re_add_im, HasSum.add, RCLike.hasSum_ofReal, RCLike.I, HasSum.mul_right
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
L : SummationFilter α
f : α → ℂ
x : ℂ
⊢ HasSum (fun (x : α) ↦ (starRingEnd ℂ : (a : ℂ) → ℂ) (f x)) x L ↔ HasSum f ((starRingEnd ℂ : (a : ℂ) → ℂ) x) L

Tactic:
RCLike.hasSum_conj _

Premises used: RCLike.hasSum_conj
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
L : SummationFilter α
f : α → ℂ
x : ℂ
⊢ HasSum (α := ℂ) (fun (x : α) ↦ ((starRingEnd ℂ : (a : ℂ) → ℂ) (f x) : ℂ)) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) L ↔
    HasSum f x L

Tactic:
RCLike.hasSum_conj' _

Premises used: RCLike.hasSum_conj'
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
f : α → ℂ
⊢ (Summable (α := ℂ) fun (x : α) ↦ (starRingEnd ℂ : (a : ℂ) → ℂ) (f x)) ↔ Summable f

Tactic:
RCLike.summable_conj _

Premises used: RCLike.summable_conj
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
L : SummationFilter α
f : α → ℂ
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (∑'[L] (a : α), f a) : ℂ)
    (∑'[L] (a : α), (starRingEnd ℂ : (a : ℂ) → ℂ) (f a) : ℂ)

Tactic:
RCLike.conj_tsum _

Premises used: RCLike.conj_tsum
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
L : SummationFilter α
f : α → ℝ
x : ℝ
⊢ HasSum (fun (x : α) ↦ (↑(f x) : ℂ)) (↑x : ℂ) L ↔ HasSum f x L

Tactic:
RCLike.hasSum_ofReal _

Premises used: RCLike.hasSum_ofReal
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
L : SummationFilter α
f : α → ℝ
⊢ Summable (α := ℂ) (fun (x : α) ↦ (↑(f x) : ℂ)) L ↔ Summable f L

Tactic:
RCLike.summable_ofReal _

Premises used: RCLike.summable_ofReal
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
L : SummationFilter α
f : α → ℝ
⊢ (↑(∑'[L] (a : α), f a) : ℂ) = ∑'[L] (a : α), (↑(f a) : ℂ)

Tactic:
RCLike.ofReal_tsum _ _

Premises used: tsum, RCLike.ofReal_tsum
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
L : SummationFilter α
f : α → ℂ
x : ℂ
h : HasSum f x L
⊢ HasSum (fun (x : α) ↦ (f x).re) x.re L

Tactic:
RCLike.hasSum_re ℂ h

Premises used: RCLike.hasSum_re, Complex
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
L : SummationFilter α
f : α → ℂ
x : ℂ
h : HasSum f x L
⊢ HasSum (fun (x : α) ↦ (f x).im) x.im L

Tactic:
RCLike.hasSum_im ℂ h

Premises used: Complex, RCLike.hasSum_im
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
L : SummationFilter α
inst : L.NeBot
f : α → ℂ
h : Summable f L
⊢ re (∑'[L] (a : α), f a) = ∑'[L] (a : α), (f a).re

Tactic:
RCLike.re_tsum _ h

Premises used: RCLike.re_tsum
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
L : SummationFilter α
inst : L.NeBot
f : α → ℂ
h : Summable f L
⊢ im (∑'[L] (a : α), f a) = ∑'[L] (a : α), (f a).im

Tactic:
RCLike.im_tsum _ h

Premises used: RCLike.im_tsum
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
α : Type u_1
L : SummationFilter α
f : α → ℂ
c : ℂ
⊢ HasSum f c L ↔ HasSum (fun (x : α) ↦ (f x).re) c.re L ∧ HasSum (fun (x : α) ↦ (f x).im) c.im L

Tactic:
RCLike.hasSum_iff _ _

Premises used: RCLike.hasSum_iff
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
⊢ z ∈ slitPlane ↔ 0 < z.re ∨ z.im ≠ 0

Tactic:
Set.mem_setOf

Premises used: Set.Mem, Set.mem_setOf, Complex.slitPlane
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
hz : z ≠ 0
⊢ ¬(z.re = re 0 ∧ z.im = im 0)

Tactic:
rw [ne_eq, Complex.ext_iff] at hz

Premises used: Complex.ext_iff, ne_eq
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
hz : ¬(z.re = re 0 ∧ z.im = im 0)
⊢ ∀ (_ : z.re = re 0), z.im ≠ im 0

Tactic:
push Not at hz

Premises used: Not
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
hz : ∀ (_ : z.re = re 0), z.im ≠ im 0
simp_all : ∀ (hz : ∀ (_ : z.re = 0), ¬z.im = 0), (0 < z.re ∨ ¬z.im = 0) ∨ z.re < 0 ∨ ¬z.im = 0
⊢ (0 < z.re ∨ z.im ≠ 0) ∨ 0 < (-z).re ∨ (-z).im ≠ 0

Tactic:
simp_all only [ne_eq, zero_re, zero_im, neg_re, Left.neg_pos_iff, neg_im, neg_eq_zero]

Premises used: neg_eq_zero, Complex.zero_im, ne_eq, Left.neg_pos_iff, Complex.neg_re, Complex.zero_re, Complex.neg_im
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
hz : ∀ (_ : z.re = 0), ¬z.im = 0
by_contra! : ∀ (contra : (z.re ≤ 0 ∧ z.im = 0) ∧ 0 ≤ z.re ∧ z.im = 0), False
⊢ (0 < z.re ∨ ¬z.im = 0) ∨ z.re < 0 ∨ ¬z.im = 0

Tactic:
by_contra! contra
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
hz : ∀ (_ : z.re = 0), ¬z.im = 0
contra : (z.re ≤ 0 ∧ z.im = 0) ∧ 0 ≤ z.re ∧ z.im = 0
⊢ False

Tactic:
hz (le_antisymm contra.1.1 contra.2.1) contra.1.2

Premises used: le_antisymm, And.right, And.left
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
hz : ∀ (_ : z.re = 0), ¬z.im = 0
contra : (z.re ≤ 0 ∧ z.im = 0) ∧ 0 ≤ z.re ∧ z.im = 0
⊢ False

Tactic:
exact hz (le_antisymm contra.1.1 contra.2.1) contra.1.2

Premises used: le_antisymm, And.right, And.left
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ slitPlane = {z : ℂ | 0 < z.re} ∪ {z : ℂ | z.im ≠ 0}

Tactic:
Set.setOf_or.symm

Premises used: Set.union, Set.Mem, setOf, Eq.symm, Set.setOf_or, Not, Complex.slitPlane
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ IsOpen slitPlane

Tactic:
(isOpen_lt continuous_const continuous_re).union (isOpen_ne_fun continuous_im continuous_const)

Premises used: Set.union, isOpen_lt, Set.Mem, Complex.continuous_re, continuous_const, setOf, isOpen_ne_fun, IsOpen.union, Not, Complex.slitPlane, Complex.continuous_im
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℝ
⊢ (↑x : ℂ) ∈ slitPlane ↔ 0 < x

Tactic:
simp [mem_slitPlane_iff]

Premises used: Complex.mem_slitPlane_iff
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
x : ℝ
⊢ -(↑x : ℂ) ∈ slitPlane ↔ x < 0

Tactic:
simpa using ofReal_mem_slitPlane (x := -x)

Premises used: Complex.ofReal_mem_slitPlane
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ 1 ∈ slitPlane

Tactic:
ofReal_mem_slitPlane.2 one_pos

Premises used: Iff.mpr, Set.Mem, Complex.ofReal_mem_slitPlane, one_pos
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ 0 ∉ slitPlane

Tactic:
mt ofReal_mem_slitPlane.1 (lt_irrefl _)

Premises used: lt_irrefl, mt, Complex.ofReal_mem_slitPlane, Iff.mp
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
n : ℕ
⊢ (↑n : ℂ) ∈ slitPlane ↔ n ≠ 0

Tactic:
simpa [pos_iff_ne_zero] using @ofReal_mem_slitPlane n

Premises used: Complex.ofReal_mem_slitPlane, pos_iff_ne_zero
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ OfNat.ofNat n ∈ slitPlane

Tactic:
natCast_mem_slitPlane.2 (NeZero.ne n)

Premises used: Iff.mpr, Set.Mem, Complex.natCast_mem_slitPlane, NeZero.ne
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
⊢ z ∈ slitPlane ↔ ¬z ≤ 0

Tactic:
mem_slitPlane_iff.trans not_le_zero_iff.symm

Premises used: Complex.not_le_zero_iff, Complex.mem_slitPlane_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
⊢ (Set.Iic 0)ᶜ = slitPlane

Tactic:
Set.ext fun _ ↦
  mem_slitPlane_iff_not_le_zero.symm

Premises used: Set.ext, Iff.symm, Complex.mem_slitPlane_iff_not_le_zero
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
hz : z ∈ slitPlane
⊢ z ≠ 0

Tactic:
ne_of_mem_of_not_mem hz zero_notMem_slitPlane

Premises used: ne_of_mem_of_not_mem, Complex.zero_notMem_slitPlane
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
hz : Membership.mem (γ := Set ℂ) (Metric.ball 1 1) z
h : 0 < z.re
⊢ z ∈ slitPlane

Tactic:
apply Or.inl

Premises used: Or.inl
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
hz : Membership.mem (γ := Set ℂ) (Metric.ball 1 1) z
⊢ 0 < z.re

Tactic:
simpa using (re_le_norm _).trans_lt (mem_ball_iff_norm'.1 hz)

Premises used: Complex.re_le_norm, mem_ball_iff_norm', Iff.mp, LE.le.trans_lt
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ Membership.mem (γ := Set ℂ) (Metric.ball 1 1) (1 + z)

Tactic:
simpa
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
simp_rw : (∀ x ∈ s, ¬x ≤ 0) ↔ -(↑r : ℂ) ∉ s
⊢ s ⊆ slitPlane ↔ -(↑r : ℂ) ∉ s

Tactic:
simp_rw [Set.subset_def, mem_slitPlane_iff_not_le_zero]

Premises used: Set.subset_def, Complex.mem_slitPlane_iff_not_le_zero
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
contrapose! : (∃ x ∈ s, x ≤ 0) ↔ -(↑r : ℂ) ∈ s
⊢ (∀ x ∈ s, ¬x ≤ 0) ↔ -(↑r : ℂ) ∉ s

Tactic:
contrapose!
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
hr : -(↑r : ℂ) ∈ s
⊢ -(↑r : ℂ) ≤ 0

Tactic:
simpa using hs hr
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
refine : (∃ x ∈ s, x ≤ 0) → -(↑r : ℂ) ∈ s
⊢ (∃ x ∈ s, x ≤ 0) ↔ -(↑r : ℂ) ∈ s

Tactic:
refine ⟨?_, fun hr ↦ ⟨_, hr, by simpa using hs hr⟩⟩
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
z : ℂ
hzs : z ∈ s
hz : z ≤ 0
⊢ ‖z‖ = r

Tactic:
simpa using hs hzs
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
z : ℂ
hzs : z ∈ s
hz : z ≤ 0
⊢ ‖z‖ = r

Tactic:
have : ‖z‖ = r := by simpa using hs hzs
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
z : ℂ
hzs : z ∈ s
hz : z ≤ 0
this : ‖z‖ = r
⊢ -(↑r : ℂ) ∈ s

Tactic:
simpa [← this, ← norm_neg z ▸ eq_coe_norm_of_nonneg (neg_nonneg.mpr hz)]
-- Module: Mathlib.Analysis.Complex.Basic
Goal:
s t : Set ℝ
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s ×ℂ t)

Tactic:
equivRealProdCLM.toHomeomorph.isCompact_preimage.2 (hs.prod ht)

Premises used: Iff.mpr, Set.Mem, IsCompact.prod, setOf, Set.prod, Homeomorph.isCompact_preimage, Set.inter, Complex.equivRealProdCLM, Complex.reProdIm, Set.preimage, ContinuousLinearEquiv.toHomeomorph
-- Module: Mathlib.Analysis.Complex.Basic
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
rw : 2⁻¹ * ‖x + star x‖ ≤ 2⁻¹ * (2 * ‖x‖)
⊢ norm (E := ↥(selfAdjoint A))
      (((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x : ↥(selfAdjoint A)) ≤
    ‖x‖

Tactic:
rw [← inv_mul_cancel_left₀ two_ne_zero ‖x‖, ← AddSubgroup.norm_coe, realPart_apply_coe,
    norm_smul, norm_inv, Real.norm_ofNat]

Premises used: Norm.norm, norm_smul, inv_mul_cancel_left₀, AddSubgroup.norm_coe, norm_inv, two_ne_zero, realPart_apply_coe, Real.norm_ofNat
-- Module: Mathlib.Analysis.Complex.Basic
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
hbc : ‖x + star x‖ ≤ 2 * ‖x‖
⊢ 2⁻¹ * ‖x + star x‖ ≤ 2⁻¹ * (2 * ‖x‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Basic
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
⊢ ‖x‖ + ‖star x‖ ≤ 2 * ‖x‖

Tactic:
simp [two_mul]

Premises used: two_mul
-- Module: Mathlib.Analysis.Complex.Basic
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
⊢ ‖x + star x‖ ≤ 2 * ‖x‖

Tactic:
exact norm_add_le _ _ |>.trans <| by simp [two_mul]

Premises used: norm_add_le, LE.le.trans
-- Module: Mathlib.Analysis.Complex.Basic
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)) =
    norm (E := ↥(selfAdjoint A))
      (((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (Complex.I • -x) : ↥(selfAdjoint A))

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Basic
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)) (Complex.I • -x) : ↥(selfAdjoint A)) ≤
    ‖x‖

Tactic:
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))

Premises used: norm_smul, realPart.norm_le, neg_neg, smul_neg, map_neg, realPart_I_smul, norm_neg, Complex.norm_I, AddSubgroupClass.coe_norm, HSMul.hSMul, Neg.neg, one_mul, Complex.I
-- Module: Mathlib.Analysis.Complex.Basic
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))
calc₁ :
  norm (E := ↥(selfAdjoint A))
      (((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (Complex.I • -x) : ↥(selfAdjoint A)) ≤
    ‖x‖
⊢ norm (E := ↥(selfAdjoint A))
      (((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) 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))

Premises used: imaginaryPart, HSMul.hSMul, realPart, DFunLike.coe, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
Goal:
M : ℝ
z w : ℂ
h_1 : M ≠ 0
h_2 : 2 * (↑M : ℂ) - z ≠ 0
h : w = z / (2 * (↑M : ℂ) - z)
rw : z = 2 * (↑M : ℂ) * (z / (2 * (↑M : ℂ) - z)) / (1 + z / (2 * (↑M : ℂ) - z))
⊢ z = 2 * (↑M : ℂ) * w / (1 + w)

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
Goal:
M : ℝ
z w : ℂ
h_1 : M ≠ 0
h_2 : 2 * (↑M : ℂ) - z ≠ 0
h : w = z / (2 * (↑M : ℂ) - z)
field_simp : z = z * 2 * (↑M : ℂ) / (2 * (↑M : ℂ) - z + z)
⊢ z = 2 * (↑M : ℂ) * (z / (2 * (↑M : ℂ) - z)) / (1 + z / (2 * (↑M : ℂ) - z))

Tactic:
field_simp
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
Goal:
M : ℝ
z w : ℂ
h_1 : M ≠ 0
h_2 : 2 * (↑M : ℂ) - z ≠ 0
h : w = z / (2 * (↑M : ℂ) - z)
ring_nf : z = z * (↑M : ℂ) * (↑M : ℂ)⁻¹
⊢ z = z * 2 * (↑M : ℂ) / (2 * (↑M : ℂ) - z + z)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
Goal:
M : ℝ
z w : ℂ
h_1 : M ≠ 0
h_2 : 2 * (↑M : ℂ) - z ≠ 0
h : w = z / (2 * (↑M : ℂ) - z)
h₁ : (↑M : ℂ) ≠ 0
⊢ z = z * (↑M : ℂ) * (↑M : ℂ)⁻¹

Tactic:
rw [mul_inv_cancel_right₀]

Premises used: mul_inv_cancel_right₀
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
Goal:
M : ℝ
z w : ℂ
h_1 : M ≠ 0
h_2 : 2 * (↑M : ℂ) - z ≠ 0
h : w = z / (2 * (↑M : ℂ) - z)
h₁ h₂ h₃ h₄ : ¬M = 0
⊢ (↑M : ℂ) ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
Goal:
M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
simp : 2 * M * ‖w‖ / ‖1 + w‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
⊢ ‖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]

Premises used: norm_mul, Complex.norm_real, Complex.norm_ofNat, norm_div, abs_of_pos, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
Goal:
M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
hdb : 1 - ‖w‖ ≤ ‖1 + w‖
⊢ 2 * M * ‖w‖ / ‖1 + w‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
Goal:
M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
hdb : norm (E := ℂ) 1 - ‖w‖ ≤ ‖1 + w‖
⊢ 1 - ‖w‖ ≤ ‖1 + w‖

Tactic:
rw [← norm_one (α := ℂ)]

Premises used: NormOneClass.norm_one
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
Goal:
M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
⊢ norm (E := ℂ) 1 - ‖w‖ ≤ ‖1 + w‖

Tactic:
norm_sub_le_norm_add 1 w

Premises used: norm_sub_le_norm_add, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
Goal:
M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
⊢ norm (E := ℂ) 1 - ‖w‖ ≤ ‖1 + w‖

Tactic:
exact norm_sub_le_norm_add 1 w

Premises used: norm_sub_le_norm_add, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
Goal:
M : ℝ
z : ℂ
h : 0 < M
h_1 : z.re ≤ M
⊢ 0 ≤ ‖z‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
Goal:
M : ℝ
z : ℂ
h : 0 < M
h_1 : z.re ≤ M
⊢ 0 ≤ ‖2 * (↑M : ℂ) - z‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
Goal:
M : ℝ
z : ℂ
h : 0 < M
h_1 : z.re ≤ M
rw : HPow.hPow (β := ℕ) ‖z‖ 2 ≤ HPow.hPow (β := ℕ) ‖2 * (↑M : ℂ) - z‖ 2
⊢ ‖z‖ ≤ ‖2 * (↑M : ℂ) - z‖

Tactic:
rw [← sq_le_sq₀ (by positivity) (by positivity)]

Premises used: sq_le_sq₀
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
Goal:
M : ℝ
z : ℂ
h : 0 < M
h_1 : z.re ≤ M
this : z.re * z.re ≤ (2 * M - z.re) * (2 * M - z.re)
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 ≤ HPow.hPow (β := ℕ) ‖2 * (↑M : ℂ) - z‖ 2

Tactic:
simpa [Complex.sq_norm, normSq_apply]

Premises used: Complex.sq_norm, Complex.normSq_apply
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
Goal:
M : ℝ
z : ℂ
h : 0 < M
h_1 : z.re ≤ M
suffices : z.re * z.re ≤ (2 * M - z.re) * (2 * M - z.re)
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 ≤ HPow.hPow (β := ℕ) ‖2 * (↑M : ℂ) - z‖ 2

Tactic:
suffices z.re * z.re ≤ (2 * M - z.re) * (2 * M - z.re) by simpa [Complex.sq_norm, normSq_apply]
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
nlinarith₁ : (2 * M - z.re) * (2 * M - z.re) < z.re * z.re → GT.gt (α := ℝ) 4 0
⊢ z.re * z.re ≤ (2 * M - z.re) * (2 * M - z.re)

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
rw : dist (f z / (2 * (↑M : ℂ) - f z)) 0 ≤ 1 / R * dist z 0
⊢ ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ 1 / R * ‖z‖

Tactic:
rw [← dist_zero_right, ← dist_zero_right]

Premises used: dist_zero_right
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
nth_rw : dist (f z / (2 * (↑M : ℂ) - f z)) (f 0 / (2 * (↑M : ℂ) - f 0)) ≤ 1 / R * dist z 0
⊢ dist (f z / (2 * (↑M : ℂ) - f z)) 0 ≤ 1 / R * dist z 0

Tactic:
nth_rw 1 [← zero_div (2 * M - f 0), ← hf₂]

Premises used: HMul.hMul, HSub.hSub, zero_div, Complex.ofReal, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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)
apply₁ :
  ∀ (x : ℂ) (hx : Membership.mem (γ := Set ℂ) (ball 0 R) x),
    f x / (2 * (↑M : ℂ) - f x) ∈ closedBall (f 0 / (2 * (↑M : ℂ) - f 0)) 1
⊢ dist (f z / (2 * (↑M : ℂ) - f z)) (f 0 / (2 * (↑M : ℂ) - f 0)) ≤ 1 / R * dist z 0

Tactic:
apply dist_le_div_mul_dist_of_mapsTo_ball (R₂ := 1) ?_ (fun x hx ↦ ?_) hz

Premises used: Complex.dist_le_div_mul_dist_of_mapsTo_ball
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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 : ∀ (x : ℂ) (hx : Membership.mem (γ := Set ℂ) (ball 0 R) x) (h : 2 * (↑M : ℂ) - f x = 0), False
⊢ DifferentiableOn ℂ (F := ℂ) (fun {z : ℂ} ↦ f z / (2 * (↑M : ℂ) - f z)) (ball 0 R)

Tactic:
apply hf.div (hf.const_sub _) fun x hx h ↦ ?_

Premises used: DifferentiableOn.const_sub, DifferentiableOn.div
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | z.re ≤ M} (2 * (↑M : ℂ))

Tactic:
have := sub_eq_zero.mp h ▸ hf₁ hx
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
this : Membership.mem (γ := Set ℂ) {z : ℂ | z.re ≤ M} (2 * (↑M : ℂ))
⊢ False

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
⊢ 0 ≤ ‖2 * (↑M : ℂ) - f x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
⊢ f x / (2 * (↑M : ℂ) - f x) ∈ closedBall (f 0 / (2 * (↑M : ℂ) - f 0)) 1

Tactic:
simpa [hf₂] using
      div_le_one_of_le₀ (norm_le_norm_two_mul_sub hM (hf₁ hx)) (by positivity)

Premises used: div_le_one_of_le₀, _private.0.Complex.norm_le_norm_two_mul_sub
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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)
⊢ ‖z‖ < R

Tactic:
have hzR : ‖z‖ < R := mem_ball_zero_iff.mp hz
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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 : ℂ) - f z)‖ ≤ ‖z‖ / R

Tactic:
simpa only [dist_zero_right, div_one, mul_comm (1 / R), mul_one_div]
    using schwarz_applied hM hf hf₁ hz hf₂

Premises used: HDiv.hDiv, _private.0.Complex.schwarz_applied, mul_one_div, mul_comm, OfNat.ofNat, dist_zero_right, div_one