Theorem: RectangleIntegral_congr (PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean)

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

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 • ?_
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)

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 ?_
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

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 ?_
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

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⟩
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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⟩
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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⟩
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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⟩
State after:
no goals

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
State after:
no goals

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
State after:
no goals