awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
rw : circleAverage (poissonKernel c w • f) c R = circleAverage (re ∘ herglotzRieszKernel c w • f) c R
⊢ circleAverage (poissonKernel c w • f) c R = f w

Tactic:
rw [← hf.circleAverage_re_herglotzRieszKernel_smul hw]

Premises used: InnerProductSpace.HarmonicContOnCl.circleAverage_re_herglotzRieszKernel_smul
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
x : ℂ
h : x ∈ sphere c |R|
⊢ (poissonKernel c w • f) x = (re ∘ herglotzRieszKernel c w • f) x

Tactic:
simp_rw [← poissonKernel_eq_re_herglotzRieszKernel]

Premises used: poissonKernel_eq_re_herglotzRieszKernel
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ circleAverage (poissonKernel c w • f) c R = circleAverage (re ∘ herglotzRieszKernel c w • f) c R

Tactic:
apply circleAverage_congr_sphere
    (fun _ _ ↦ by simp_rw [← poissonKernel_eq_re_herglotzRieszKernel])

Premises used: Real.circleAverage_congr_sphere
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r : ℝ
hz : z ∈ ball c r
suffices : dist ((↑z.re : ℂ) + (↑c.im : ℂ) * I) c ≤ dist z c
⊢ (↑z.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r

Tactic:
suffices dist (z.re + c.im * I) c ≤ dist z c from lt_of_le_of_lt this hz
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r : ℝ
hz : z ∈ ball c r
⊢ 0 ≤
    √(HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑c.im : ℂ) * I).re - c.re) 2 +
        HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑c.im : ℂ) * I).im - c.im) 2)

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r : ℝ
hz : z ∈ ball c r
⊢ 0 ≤ HPow.hPow (β := ℕ) (z.re - c.re) 2 + HPow.hPow (β := ℕ) (z.im - c.im) 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r : ℝ
hz : z ∈ ball c r
⊢ 0 ≤
    HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑c.im : ℂ) * I).re - c.re) 2 +
      HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑c.im : ℂ) * I).im - c.im) 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r : ℝ
hz : z ∈ ball c r
rw :
  HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑c.im : ℂ) * I).re - c.re) 2 +
      HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑c.im : ℂ) * I).im - c.im) 2 ≤
    HPow.hPow (β := ℕ) (z.re - c.re) 2 + HPow.hPow (β := ℕ) (z.im - c.im) 2
⊢ dist ((↑z.re : ℂ) + (↑c.im : ℂ) * I) c ≤ dist z c

Tactic:
rw [dist_eq_re_im, dist_eq_re_im, Real.le_sqrt (by positivity) (by positivity),
    Real.sq_sqrt (by positivity)]

Premises used: Real.sq_sqrt, Real.le_sqrt, Complex.dist_eq_re_im
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r : ℝ
hz : z ∈ ball c r
⊢ HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑c.im : ℂ) * I).re - c.re) 2 +
      HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑c.im : ℂ) * I).im - c.im) 2 ≤
    HPow.hPow (β := ℕ) (z.re - c.re) 2 + HPow.hPow (β := ℕ) (z.im - c.im) 2

Tactic:
simp [sq_nonneg _]

Premises used: sq_nonneg
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r x : ℝ
hx : x ∈ Ioo (z.re - (r - dist z c)) (z.re + (r - dist z c))
⊢ let r₁ := r - dist z c;
  x ∈ Ioo (z.re - r₁) (z.re + r₁)

Tactic:
set r₁ := r - dist z c

Premises used: Dist.dist
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
hx : x ∈ Ioo (z.re - r₁) (z.re + r₁)
⊢ let s := Ioo (z.re - r₁) (z.re + r₁);
  x ∈ s

Tactic:
set s := Ioo (z.re - r₁) (z.re + r₁)

Premises used: HSub.hSub, Complex.re, HAdd.hAdd, Set.Ioo
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
y : ℂ
yRe : y.re ∈ s
yIm : y.im = z.im
rw : |y.re - z.re| < r₁
⊢ y ∈ ball z r₁

Tactic:
rw [mem_ball, dist_eq_re_im, yIm, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs]

Premises used: sub_self, Real.sqrt_sq_eq_abs, Metric.mem_ball, two_ne_zero, add_zero, zero_pow, Complex.dist_eq_re_im
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
y : ℂ
yRe : y.re ∈ s
yIm : y.im = z.im
⊢ |y.re - z.re| < r₁

Tactic:
grind [abs_lt]

Premises used: abs_lt
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
⊢ s ×ℂ {z.im} ⊆ ball z r₁

Tactic:
have s_ball₁ : s ×ℂ {z.im} ⊆ ball z r₁ := by
    rintro y ⟨yRe : y.re ∈ s, yIm : y.im = z.im⟩
    rw [mem_ball, dist_eq_re_im, yIm, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs]
    grind [abs_lt]
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
s_ball₁ : s ×ℂ {z.im} ⊆ ball z r₁
this : s ×ℂ {z.im} ⊆ ball c r
⊢ (↑x : ℂ) + (↑z.im : ℂ) * I ∈ s ×ℂ {z.im}

Tactic:
simp [mem_reProdIm, hx]

Premises used: Complex.mem_reProdIm
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
s_ball₁ : s ×ℂ {z.im} ⊆ ball z r₁
suffices : s ×ℂ {z.im} ⊆ ball c r
⊢ (↑x : ℂ) + (↑z.im : ℂ) * I ∈ ball c r

Tactic:
suffices s ×ℂ {z.im} ⊆ ball c r from this <| by simp [mem_reProdIm, hx]
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
s_ball₁ : s ×ℂ {z.im} ⊆ ball z r₁
⊢ r₁ + dist z c ≤ r

Tactic:
simp [r₁]
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
s_ball₁ : s ×ℂ {z.im} ⊆ ball z r₁
⊢ s ×ℂ {z.im} ⊆ ball c r

Tactic:
exact s_ball₁.trans <| ball_subset_ball' <| by simp [r₁]

Premises used: HasSubset.Subset.trans, Metric.ball_subset_ball'
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ (↑z.re : ℂ) + (↑y : ℂ) * I ∈ closedBall c r

Tactic:
le_trans ?_ (mem_closedBall.mp z_in_ball)

Premises used: Set.Mem, setOf, Iff.mp, Metric.mem_closedBall, Metric.closedBall, le_trans
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
refine : dist ((↑z.re : ℂ) + (↑y : ℂ) * I) c ≤ dist z c
⊢ (↑z.re : ℂ) + (↑y : ℂ) * I ∈ closedBall c r

Tactic:
refine le_trans ?_ (mem_closedBall.mp z_in_ball)

Premises used: Iff.mp, Metric.mem_closedBall, le_trans
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ 0 ≤
    √(HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑y : ℂ) * I).re - c.re) 2 +
        HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑y : ℂ) * I).im - c.im) 2)

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ 0 ≤ HPow.hPow (β := ℕ) (z.re - c.re) 2 + HPow.hPow (β := ℕ) (z.im - c.im) 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ 0 ≤
    HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑y : ℂ) * I).re - c.re) 2 +
      HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑y : ℂ) * I).im - c.im) 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
rw :
  HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑y : ℂ) * I).re - c.re) 2 +
      HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑y : ℂ) * I).im - c.im) 2 ≤
    HPow.hPow (β := ℕ) (z.re - c.re) 2 + HPow.hPow (β := ℕ) (z.im - c.im) 2
⊢ dist ((↑z.re : ℂ) + (↑y : ℂ) * I) c ≤ dist z c

Tactic:
rw [dist_eq_re_im, dist_eq_re_im, Real.le_sqrt (by positivity) (by positivity),
    Real.sq_sqrt (by positivity)]

Premises used: Real.sq_sqrt, Real.le_sqrt, Complex.dist_eq_re_im
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
this : HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2
⊢ HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑y : ℂ) * I).re - c.re) 2 +
      HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑y : ℂ) * I).im - c.im) 2 ≤
    HPow.hPow (β := ℕ) (z.re - c.re) 2 + HPow.hPow (β := ℕ) (z.im - c.im) 2

Tactic:
simpa
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
suffices : HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2
⊢ HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑y : ℂ) * I).re - c.re) 2 +
      HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑y : ℂ) * I).im - c.im) 2 ≤
    HPow.hPow (β := ℕ) (z.re - c.re) 2 + HPow.hPow (β := ℕ) (z.im - c.im) 2

Tactic:
suffices (y - c.im) ^ 2 ≤ (z.im - c.im) ^ 2 by simpa
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
inl : c.im < y ∧ y ≤ z.im → HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2
inr : z.im < y ∧ y ≤ c.im → HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2
⊢ HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2

Tactic:
cases mem_uIoc.mp y_in_I

Premises used: Set.mem_uIoc, Iff.mp
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
h : c.im < y ∧ y ≤ z.im
nlinarith :
  HPow.hPow (β := ℕ) (z.im - c.im) 2 < HPow.hPow (β := ℕ) (y - c.im) 2 →
    HPow.hPow (β := ℕ) (z.im - c.im) 2 - HPow.hPow (β := ℕ) (y - c.im) 2 + 2 * (0 - (c.im - y) * (y - z.im)) +
        (0 - (y - z.im) * (y - z.im)) =
      0
nlinarith₁ : HPow.hPow (β := ℕ) (z.im - c.im) 2 < HPow.hPow (β := ℕ) (y - c.im) 2 → GT.gt (α := ℝ) 2 0
⊢ HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
h : z.im < y ∧ y ≤ c.im
nlinarith :
  HPow.hPow (β := ℕ) (z.im - c.im) 2 < HPow.hPow (β := ℕ) (y - c.im) 2 →
    HPow.hPow (β := ℕ) (z.im - c.im) 2 - HPow.hPow (β := ℕ) (y - c.im) 2 + (0 - (z.im - y) * (z.im - y)) +
        2 * (0 - (z.im - y) * (y - c.im)) =
      0
nlinarith₁ : HPow.hPow (β := ℕ) (z.im - c.im) 2 < HPow.hPow (β := ℕ) (y - c.im) 2 → GT.gt (α := ℝ) 2 0
⊢ HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c : ℂ
r a₁ a₂ b : ℝ
ha₁ : (↑a₁ : ℂ) + (↑b : ℂ) * I ∈ ball c r
ha₂ : (↑a₂ : ℂ) + (↑b : ℂ) * I ∈ ball c r
⊢ ((↑a₁ : ℂ) + (↑b : ℂ) * I).Rectangle ((↑a₂ : ℂ) + (↑b : ℂ) * I) ⊆ ball c r

Tactic:
Convex.rectangle_subset (convex_ball c r) ha₁ ha₂ ?_ ?_

Premises used: Complex.Convex.rectangle_subset, convex_ball
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c : ℂ
r a₁ a₂ b : ℝ
ha₁ : (↑a₁ : ℂ) + (↑b : ℂ) * I ∈ ball c r
ha₂ : (↑a₂ : ℂ) + (↑b : ℂ) * I ∈ ball c r
h :
  (fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]] =
    ((↑a₁ : ℂ) + (↑b : ℂ) * I).Rectangle ((↑a₂ : ℂ) + (↑b : ℂ) * I)
convert_1 : (↑((↑a₁ : ℂ) + (↑b : ℂ) * I).re : ℂ) + (↑((↑a₂ : ℂ) + (↑b : ℂ) * I).im : ℂ) * I ∈ ball c r
convert_2 : (↑((↑a₂ : ℂ) + (↑b : ℂ) * I).re : ℂ) + (↑((↑a₁ : ℂ) + (↑b : ℂ) * I).im : ℂ) * I ∈ ball c r
⊢ (fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]] ⊆ ball c r

Tactic:
convert! Convex.rectangle_subset (convex_ball c r) ha₁ ha₂ ?_ ?_ using 1

Premises used: Complex.Convex.rectangle_subset, convex_ball
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c : ℂ
r a₁ a₂ b : ℝ
ha₁ : (↑a₁ : ℂ) + (↑b : ℂ) * I ∈ ball c r
ha₂ : (↑a₂ : ℂ) + (↑b : ℂ) * I ∈ ball c r
⊢ (fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]] =
    ((↑a₁ : ℂ) + (↑b : ℂ) * I).Rectangle ((↑a₂ : ℂ) + (↑b : ℂ) * I)

Tactic:
simp [horizontalSegment_eq a₁ a₂ b, ha₁, ha₂, Rectangle]

Premises used: Complex.Rectangle, Complex.horizontalSegment_eq
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c : ℂ
r a₁ a₂ b : ℝ
ha₁ : (↑a₁ : ℂ) + (↑b : ℂ) * I ∈ ball c r
ha₂ : (↑a₂ : ℂ) + (↑b : ℂ) * I ∈ ball c r
⊢ (↑((↑a₁ : ℂ) + (↑b : ℂ) * I).re : ℂ) + (↑((↑a₂ : ℂ) + (↑b : ℂ) * I).im : ℂ) * I ∈ ball c r

Tactic:
simp [horizontalSegment_eq a₁ a₂ b, ha₁, ha₂, Rectangle]

Premises used: Complex.Rectangle, Complex.horizontalSegment_eq
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c : ℂ
r a₁ a₂ b : ℝ
ha₁ : (↑a₁ : ℂ) + (↑b : ℂ) * I ∈ ball c r
ha₂ : (↑a₂ : ℂ) + (↑b : ℂ) * I ∈ ball c r
⊢ (↑((↑a₂ : ℂ) + (↑b : ℂ) * I).re : ℂ) + (↑((↑a₁ : ℂ) + (↑b : ℂ) * I).im : ℂ) * I ∈ ball c r

Tactic:
simp [horizontalSegment_eq a₁ a₂ b, ha₁, ha₂, Rectangle]

Premises used: Complex.Rectangle, Complex.horizontalSegment_eq
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c : ℂ
r a b₁ b₂ : ℝ
hb₁ : (↑a : ℂ) + (↑b₁ : ℂ) * I ∈ ball c r
hb₂ : (↑a : ℂ) + (↑b₂ : ℂ) * I ∈ ball c r
⊢ ((↑a : ℂ) + (↑b₁ : ℂ) * I).Rectangle ((↑a : ℂ) + (↑b₂ : ℂ) * I) ⊆ ball c r

Tactic:
Convex.rectangle_subset (convex_ball c r) hb₁ hb₂ ?_ ?_

Premises used: Complex.Convex.rectangle_subset, convex_ball
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c : ℂ
r a b₁ b₂ : ℝ
hb₁ : (↑a : ℂ) + (↑b₁ : ℂ) * I ∈ ball c r
hb₂ : (↑a : ℂ) + (↑b₂ : ℂ) * I ∈ ball c r
h :
  (fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]] =
    ((↑a : ℂ) + (↑b₁ : ℂ) * I).Rectangle ((↑a : ℂ) + (↑b₂ : ℂ) * I)
convert_1 : (↑((↑a : ℂ) + (↑b₁ : ℂ) * I).re : ℂ) + (↑((↑a : ℂ) + (↑b₂ : ℂ) * I).im : ℂ) * I ∈ ball c r
convert_2 : (↑((↑a : ℂ) + (↑b₂ : ℂ) * I).re : ℂ) + (↑((↑a : ℂ) + (↑b₁ : ℂ) * I).im : ℂ) * I ∈ ball c r
⊢ (fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]] ⊆ ball c r

Tactic:
convert! Convex.rectangle_subset (convex_ball c r) hb₁ hb₂ ?_ ?_ using 1

Premises used: Complex.Convex.rectangle_subset, convex_ball
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c : ℂ
r a b₁ b₂ : ℝ
hb₁ : (↑a : ℂ) + (↑b₁ : ℂ) * I ∈ ball c r
hb₂ : (↑a : ℂ) + (↑b₂ : ℂ) * I ∈ ball c r
⊢ (fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]] =
    ((↑a : ℂ) + (↑b₁ : ℂ) * I).Rectangle ((↑a : ℂ) + (↑b₂ : ℂ) * I)

Tactic:
simp [verticalSegment_eq a b₁ b₂, hb₁, hb₂, Rectangle]

Premises used: Complex.verticalSegment_eq, Complex.Rectangle
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c : ℂ
r a b₁ b₂ : ℝ
hb₁ : (↑a : ℂ) + (↑b₁ : ℂ) * I ∈ ball c r
hb₂ : (↑a : ℂ) + (↑b₂ : ℂ) * I ∈ ball c r
⊢ (↑((↑a : ℂ) + (↑b₁ : ℂ) * I).re : ℂ) + (↑((↑a : ℂ) + (↑b₂ : ℂ) * I).im : ℂ) * I ∈ ball c r

Tactic:
simp [verticalSegment_eq a b₁ b₂, hb₁, hb₂, Rectangle]

Premises used: Complex.verticalSegment_eq, Complex.Rectangle
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c : ℂ
r a b₁ b₂ : ℝ
hb₁ : (↑a : ℂ) + (↑b₁ : ℂ) * I ∈ ball c r
hb₂ : (↑a : ℂ) + (↑b₂ : ℂ) * I ∈ ball c r
⊢ (↑((↑a : ℂ) + (↑b₂ : ℂ) * I).re : ℂ) + (↑((↑a : ℂ) + (↑b₁ : ℂ) * I).im : ℂ) * I ∈ ball c r

Tactic:
simp [verticalSegment_eq a b₁ b₂, hb₁, hb₂, Rectangle]

Premises used: Complex.verticalSegment_eq, Complex.Rectangle
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
hb₁ : (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball c r
hb₂ : (↑w.re : ℂ) + (↑w.im : ℂ) * I ∈ ball c r
⊢ (fun (y : ℝ) ↦ (↑w.re : ℂ) + (↑y : ℂ) * I) '' [[z.im, w.im]] ⊆ ball c r

Tactic:
apply mem_ball_of_map_im_aux₁

Premises used: _private.0.Complex.mem_ball_of_map_im_aux₁
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ r - dist z c + dist z c ≤ r

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
hb₁ : (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball z (r - dist z c)
⊢ (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball c r

Tactic:
apply mem_of_subset_of_mem (ball_subset_ball' (by simp) : ball z (r - dist z c) ⊆ ball c r)

Premises used: Set.mem_of_subset_of_mem, Metric.ball_subset_ball'
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
hb₂ : (↑w.re : ℂ) + (↑w.im : ℂ) * I ∈ ball z (r - dist z c)
⊢ (↑w.re : ℂ) + (↑w.im : ℂ) * I ∈ ball c r

Tactic:
apply mem_of_subset_of_mem (ball_subset_ball' (by simp) : ball z (r - dist z c) ⊆ ball c r)

Premises used: Set.mem_of_subset_of_mem, Metric.ball_subset_ball'
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball z (r - dist z c)

Tactic:
re_add_im_mul_mem_ball hw

Premises used: _private.0.Complex.re_add_im_mul_mem_ball
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball z (r - dist z c)

Tactic:
exact re_add_im_mul_mem_ball hw

Premises used: _private.0.Complex.re_add_im_mul_mem_ball
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ (↑w.re : ℂ) + (↑w.im : ℂ) * I ∈ ball z (r - dist z c)

Tactic:
simpa using hw
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z w : ℂ
f : ℂ → E
simp :
  (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) +
      ((-∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        -HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I))) =
    HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I))
⊢ z.wedgeIntegral w f + w.wedgeIntegral z f =
    HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I))

Tactic:
simp only [wedgeIntegral, intervalIntegral.integral_symm z.re w.re,
    intervalIntegral.integral_symm z.im w.im, smul_neg]

Premises used: Complex.wedgeIntegral, Complex.im, smul_neg, intervalIntegral.integral_symm, Complex.re
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z w : ℂ
f : ℂ → E
⊢ (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) +
      ((-∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        -HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I))) =
    HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I))

Tactic:
abel
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
h : IsExactOn f s
x₀ : ℂ
y : E
obtain : ∀ (η : ℂ → E) (hη : ∀ z ∈ s, HasDerivAt η (f z) z), ∃ (g : ℂ → E), g x₀ = y ∧ ∀ x ∈ s, HasDerivAt g (f x) x
⊢ ∃ (g : ℂ → E), g x₀ = y ∧ ∀ x ∈ s, HasDerivAt g (f x) x

Tactic:
obtain ⟨η, hη⟩ := h
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
x₀ : ℂ
y : E
η : ℂ → E
hη : ∀ z ∈ s, HasDerivAt η (f z) z
⊢ η x₀ - η x₀ + y = y

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
x₀ : ℂ
y : E
η : ℂ → E
hη : ∀ z ∈ s, HasDerivAt η (f z) z
⊢ ∀ x ∈ s, HasDerivAt (fun (z : ℂ) ↦ η z - η x₀ + y) (f x) x

Tactic:
simpa using hη
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
x₀ : ℂ
y : E
η : ℂ → E
hη : ∀ z ∈ s, HasDerivAt η (f z) z
w : ℂ → E
left : η x₀ - η x₀ + y = y
right : ∀ x ∈ s, HasDerivAt (fun (z : ℂ) ↦ η z - η x₀ + y) (f x) x
⊢ ∃ (g : ℂ → E), g x₀ = y ∧ ∀ x ∈ s, HasDerivAt g (f x) x

Tactic:
use fun z ↦ η z - η x₀ + y, by simp, by simpa using hη

Premises used: HSub.hSub, HAdd.hAdd
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
U V : Set ℂ
h : U ⊆ V
hf : IsConservativeOn f V
⊢ IsConservativeOn f U

Tactic:
fun z w hzw ↦ hf z w (hzw.trans h)

Premises used: HasSubset.Subset.trans, Complex.IsConservativeOn
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
U : Set ℂ
hf : DifferentiableOn ℂ f U
z w : ℂ
hzw : z.Rectangle w ⊆ U
rw :
  HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I)) =
    0
⊢ z.wedgeIntegral w f = -w.wedgeIntegral z f

Tactic:
rw [← add_eq_zero_iff_eq_neg, wedgeIntegral_add_wedgeIntegral_eq]

Premises used: add_eq_zero_iff_eq_neg, Complex.wedgeIntegral_add_wedgeIntegral_eq
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
U : Set ℂ
hf : DifferentiableOn ℂ f U
z w : ℂ
hzw : z.Rectangle w ⊆ U
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I)) =
    0

Tactic:
integral_boundary_rect_eq_zero_of_differentiableOn f z w <| hf.mono hzw

Premises used: Complex.integral_boundary_rect_eq_zero_of_differentiableOn, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
U : Set ℂ
hf : DifferentiableOn ℂ f U
z w : ℂ
hzw : z.Rectangle w ⊆ U
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I)) =
    0

Tactic:
exact integral_boundary_rect_eq_zero_of_differentiableOn f z w <| hf.mono hzw

Premises used: Complex.integral_boundary_rect_eq_zero_of_differentiableOn, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
hf : IsExactOn f U
obtain : ∀ (g : ℂ → E) (hg : ∀ z ∈ U, HasDerivAt g (f z) z), DifferentiableOn ℂ f U
⊢ DifferentiableOn ℂ f U

Tactic:
obtain ⟨g, hg⟩ := hf
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
g : ℂ → E
hg : ∀ z ∈ U, HasDerivAt g (f z) z
⊢ DifferentiableOn ℂ g U

Tactic:
have hg' : DifferentiableOn ℂ g U := fun z hz ↦ (hg z hz).differentiableAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
g : ℂ → E
hg : ∀ z ∈ U, HasDerivAt g (f z) z
hg' : DifferentiableOn ℂ g U
⊢ DifferentiableOn ℂ f U

Tactic:
(differentiableOn_congr <| fun z hz ↦ (hg z hz).deriv).mp <| hg'.deriv hU

Premises used: DifferentiableOn.deriv, HasDerivAt.deriv, Iff.mp, differentiableOn_congr