internlm/Lean-Github huggingface dataset:
Theorem: DiffVertRect_eq_UpperLowerUs
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      (HIntegral f (σ - (0 * T - 1 * 0)) (σ' + (0 * T - 1 * 0)) (0 - (0 * 0 + 1 * T)) -
            HIntegral f (σ - (0 * T - 1 * 0)) (σ' + (0 * T - 1 * 0)) (0 + (0 * 0 + 1 * T)) +
          VIntegral f (σ' + (0 * T - 1 * 0)) (0 - (0 * 0 + 1 * T)) (0 + (0 * 0 + 1 * T)) -
        VIntegral f (σ - (0 * T - 1 * 0)) (0 - (0 * 0 + 1 * T)) (0 + (0 * 0 + 1 * T))) =
    ((HIntegral f σ σ' T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) - I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      ((HIntegral f σ σ' (-T) - I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) +
        I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I))
Tactic:
ring_nf
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      (HIntegral f σ σ' (-T) - HIntegral f σ σ' T + VIntegral f σ' (-T) T - VIntegral f σ (-T) T) =
    ((HIntegral f σ σ' T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) - I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      ((HIntegral f σ σ' (-T) - I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) +
        I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I))
Theorem: DiffVertRect_eq_UpperLowerUs
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      (HIntegral f σ σ' (-T) - HIntegral f σ σ' T + VIntegral f σ' (-T) T - VIntegral f σ (-T) T) =
    ((HIntegral f σ σ' T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) - I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      ((HIntegral f σ σ' (-T) - I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) +
        I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I))
Tactic:
abel
Proof state after:
no goals
Theorem: existsDifferentiableOn_of_bddAbove
Proof state before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f g : ℂ → E
z✝ w p c✝ A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
inst✝ : CompleteSpace E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : HolomorphicOn f (s \ {c})
hb : BddAbove (Norm.norm ∘ f '' (s \ {c}))
z : ℂ
hz : z ∈ s \ {c}
h : ¬z = c
⊢ f z = Function.update f c (limUnder (𝓝[≠] c) f) z
Tactic:
simp [h]
Proof state after:
no goals
Theorem: RectangleIntegral_congr
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ RectangleIntegral f z w = RectangleIntegral g z w
Tactic:
unfold RectangleIntegral VIntegral
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ (HIntegral f z.re w.re z.im - HIntegral f z.re w.re w.im + I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) =
    (HIntegral g z.re w.re z.im - HIntegral g z.re w.re w.im + I • ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I)
Theorem: RectangleIntegral_congr
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ (HIntegral f z.re w.re z.im - HIntegral f z.re w.re w.im + I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) =
    (HIntegral g z.re w.re z.im - HIntegral g z.re w.re w.im + I • ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I)
Tactic:
congrm ?_ - ?_ + I • ?_ - I • ?_
Proof state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ HIntegral f z.re w.re z.im = HIntegral g z.re w.re z.im

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ HIntegral f z.re w.re w.im = HIntegral g z.re w.re w.im

case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) = ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)

case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) = ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I)
Theorem: RectangleIntegral_congr
Proof state before:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ HIntegral f z.re w.re z.im = HIntegral g z.re w.re z.im

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ HIntegral f z.re w.re w.im = HIntegral g z.re w.re w.im

case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) = ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)

case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) = ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I)
Tactic:
all_goals refine intervalIntegral.integral_congr fun _ _ ↦ h ?_
Proof state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.re, w.re]]
⊢ ↑x✝¹ + ↑z.im * I ∈ RectangleBorder z w

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.re, w.re]]
⊢ ↑x✝¹ + ↑w.im * I ∈ RectangleBorder z w

case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.im, w.im]]
⊢ ↑w.re + ↑x✝¹ * I ∈ RectangleBorder z w

case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.im, w.im]]
⊢ ↑z.re + ↑x✝¹ * I ∈ RectangleBorder z w
Theorem: RectangleIntegral_congr
Proof state before:
case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) = ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I)
Tactic:
refine intervalIntegral.integral_congr fun _ _ ↦ h ?_
Proof state after:
case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.im, w.im]]
⊢ ↑z.re + ↑x✝¹ * I ∈ RectangleBorder z w
Theorem: RectangleIntegral_congr
Proof state before:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.re, w.re]]
⊢ ↑x✝¹ + ↑z.im * I ∈ RectangleBorder z w
Tactic:
exact Or.inl <| Or.inl <| Or.inl ⟨by simpa, by simp⟩
Proof state after:
no goals
Theorem: RectangleIntegral_congr
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.re, w.re]]
⊢ ↑x✝¹ + ↑z.im * I ∈ re ⁻¹' [[z.re, w.re]]
Tactic:
simpa
Proof state after:
no goals
Theorem: RectangleIntegral_congr
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.re, w.re]]
⊢ ↑x✝¹ + ↑z.im * I ∈ im ⁻¹' {z.im}
Tactic:
simp
Proof state after:
no goals
Theorem: RectangleIntegral_congr
Proof state before:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.re, w.re]]
⊢ ↑x✝¹ + ↑w.im * I ∈ RectangleBorder z w
Tactic:
exact Or.inl <| Or.inr ⟨by simpa, by simp⟩
Proof state after:
no goals
Theorem: RectangleIntegral_congr
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.re, w.re]]
⊢ ↑x✝¹ + ↑w.im * I ∈ re ⁻¹' [[z.re, w.re]]
Tactic:
simpa
Proof state after:
no goals
Theorem: RectangleIntegral_congr
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.re, w.re]]
⊢ ↑x✝¹ + ↑w.im * I ∈ im ⁻¹' {w.im}
Tactic:
simp
Proof state after:
no goals
Theorem: RectangleIntegral_congr
Proof state before:
case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.im, w.im]]
⊢ ↑w.re + ↑x✝¹ * I ∈ RectangleBorder z w
Tactic:
exact Or.inr ⟨by simp, by simpa⟩
Proof state after:
no goals
Theorem: RectangleIntegral_congr
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.im, w.im]]
⊢ ↑w.re + ↑x✝¹ * I ∈ re ⁻¹' {w.re}
Tactic:
simp
Proof state after:
no goals
Theorem: RectangleIntegral_congr
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.im, w.im]]
⊢ ↑w.re + ↑x✝¹ * I ∈ im ⁻¹' [[z.im, w.im]]
Tactic:
simpa
Proof state after:
no goals
Theorem: RectangleIntegral_congr
Proof state before:
case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.im, w.im]]
⊢ ↑z.re + ↑x✝¹ * I ∈ RectangleBorder z w
Tactic:
exact Or.inl <| Or.inl <| Or.inr ⟨by simp, by simpa⟩
Proof state after:
no goals
Theorem: RectangleIntegral_congr
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.im, w.im]]
⊢ ↑z.re + ↑x✝¹ * I ∈ re ⁻¹' {z.re}
Tactic:
simp
Proof state after:
no goals
Theorem: RectangleIntegral_congr
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.im, w.im]]
⊢ ↑z.re + ↑x✝¹ * I ∈ im ⁻¹' [[z.im, w.im]]
Tactic:
simpa
Proof state after:
no goals
Theorem: RectangleIntegral'_congr
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ RectangleIntegral' f z w = RectangleIntegral' g z w
Tactic:
rw [RectangleIntegral', RectangleIntegral_congr h]
Proof state after:
no goals
Theorem: rectangleIntegral_symm
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g : ℂ → E
z✝ w✝ p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f : ℂ → E
z w : ℂ
⊢ RectangleIntegral f z w = RectangleIntegral f w z
Tactic:
simp_rw [RectangleIntegral, HIntegral, VIntegral, intervalIntegral.integral_symm w.re,
  intervalIntegral.integral_symm w.im, sub_neg_eq_add, smul_neg, sub_neg_eq_add, ← sub_eq_add_neg,
  neg_add_eq_sub, sub_add_eq_add_sub]
Proof state after:
no goals
Theorem: rectangleIntegral_symm_re
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g : ℂ → E
z✝ w✝ p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f : ℂ → E
z w : ℂ
⊢ RectangleIntegral f (↑w.re + ↑z.im * I) (↑z.re + ↑w.im * I) = -RectangleIntegral f z w
Tactic:
simp [RectangleIntegral, ← sub_eq_zero]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g : ℂ → E
z✝ w✝ p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f : ℂ → E
z w : ℂ
⊢ HIntegral f w.re z.re z.im - HIntegral f w.re z.re w.im + VIntegral f z.re z.im w.im - VIntegral f w.re z.im w.im -
        (VIntegral f z.re z.im w.im -
          (HIntegral f z.re w.re z.im - HIntegral f z.re w.re w.im + VIntegral f w.re z.im w.im)) -
      0 =
    0
Theorem: rectangleIntegral_symm_re
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g : ℂ → E
z✝ w✝ p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f : ℂ → E
z w : ℂ
⊢ HIntegral f w.re z.re z.im - HIntegral f w.re z.re w.im + VIntegral f z.re z.im w.im - VIntegral f w.re z.im w.im -
        (VIntegral f z.re z.im w.im -
          (HIntegral f z.re w.re z.im - HIntegral f z.re w.re w.im + VIntegral f w.re z.im w.im)) -
      0 =
    0
Tactic:
rw [HIntegral_symm (y := z.im), HIntegral_symm (y := w.im)]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g : ℂ → E
z✝ w✝ p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f : ℂ → E
z w : ℂ
⊢ -HIntegral f z.re w.re z.im - -HIntegral f z.re w.re w.im + VIntegral f z.re z.im w.im - VIntegral f w.re z.im w.im -
        (VIntegral f z.re z.im w.im -
          (HIntegral f z.re w.re z.im - HIntegral f z.re w.re w.im + VIntegral f w.re z.im w.im)) -
      0 =
    0
Theorem: rectangleIntegral_symm_re
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g : ℂ → E
z✝ w✝ p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f : ℂ → E
z w : ℂ
⊢ -HIntegral f z.re w.re z.im - -HIntegral f z.re w.re w.im + VIntegral f z.re z.im w.im - VIntegral f w.re z.im w.im -
        (VIntegral f z.re z.im w.im -
          (HIntegral f z.re w.re z.im - HIntegral f z.re w.re w.im + VIntegral f w.re z.im w.im)) -
      0 =
    0
Tactic:
abel
Proof state after:
no goals
Theorem: RectangleBorderIntegrable.add
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → E
hf : RectangleBorderIntegrable f z w
hg : RectangleBorderIntegrable g z w
⊢ RectangleIntegral (f + g) z w = RectangleIntegral f z w + RectangleIntegral g z w
Tactic:
dsimp [RectangleIntegral, HIntegral, VIntegral]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → E
hf : RectangleBorderIntegrable f z w
hg : RectangleBorderIntegrable g z w
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I)) -
          ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) + g (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) + g (↑z.re + ↑y * I) =
    ((((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)) +
      ((((∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I))
Theorem: RectangleBorderIntegrable.add
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → E
hf : RectangleBorderIntegrable f z w
hg : RectangleBorderIntegrable g z w
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I)) -
          ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) + g (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) + g (↑z.re + ↑y * I) =
    ((((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)) +
      ((((∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I))
Tactic:
have h₁ := intervalIntegral.integral_add hf.1 hg.1
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → E
hf : RectangleBorderIntegrable f z w
hg : RectangleBorderIntegrable g z w
h₁ :
  ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I) =
    (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) + ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I)) -
          ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) + g (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) + g (↑z.re + ↑y * I) =
    ((((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)) +
      ((((∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I))
Theorem: RectangleBorderIntegrable.add
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → E
hf : RectangleBorderIntegrable f z w
hg : RectangleBorderIntegrable g z w
h₁ :
  ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I) =
    (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) + ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I)) -
          ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) + g (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) + g (↑z.re + ↑y * I) =
    ((((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)) +
      ((((∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I))
Tactic:
have h₂ := intervalIntegral.integral_add hf.2.1 hg.2.1
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → E
hf : RectangleBorderIntegrable f z w
hg : RectangleBorderIntegrable g z w
h₁ :
  ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I) =
    (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) + ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)
h₂ :
  ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I) =
    (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) + ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I)) -
          ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) + g (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) + g (↑z.re + ↑y * I) =
    ((((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)) +
      ((((∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I))