Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
s✝ : Set (↑I × ↑I)
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s✝.Countable
hφt : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a_1, b_1) ∈ t
hω : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, (a_1, b_1) ∉ s✝ → HasFDerivWithinAt ω (dω (φ (a_1, b_1))) t (φ (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a_1 ∈ Ioo 0 1,
    ∀ b_1 ∈ Ioo 0 1,
      (a_1, b_1) ∉ s✝ →
        ∀ u ∈ tangentConeAt ℝ t (φ (a_1, b_1)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a_1, b_1)), ((dω (φ (a_1, b_1))) u) v = ((dω (φ (a_1, b_1))) v) u
U : Set (ℝ × ℝ) := Ioo 0 1 ×ˢ Ioo 0 1
hU : U = Ioo 0 1 ×ˢ Ioo 0 1
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E := fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ : ψ = fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hψφ : ∀ (a_1 b_1 : ↑I), ψ (↑a_1, ↑b_1) = φ (a_1, b_1)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
hψUt : MapsTo ψ U t
dψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fderivWithin ℝ ψ (Icc 0 1)
s' : Set (ℝ × ℝ) := Prod.map Subtype.val Subtype.val '' s✝
hs' : s' = Prod.map Subtype.val Subtype.val '' s✝
hmem_s' : ∀ (x y : ↑I), (↑x, ↑y) ∈ s' ↔ (x, y) ∈ s✝
hs'c : s'.Countable
hdψ : ∀ a ∈ U, HasFDerivAt ψ (dψ a) a
d2ψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] E := fderivWithin ℝ dψ (Icc 0 1)
hd2ψ : ∀ a ∈ U, HasFDerivAt dψ (d2ψ a) a
hd2ψ_symm : ∀ a ∈ Icc 0 1, ∀ (x y : ℝ × ℝ), ((d2ψ a) x) y = ((d2ψ a) y) x
η : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ ω (ψ a) ∘SL dψ a
f : ℝ × ℝ → F := fun a ↦ (η a) (0, 1)
hf : ∀ a ∈ Icc 0 1, f a = (ω (ψ a)) (derivWithin (ψ ∘ fun x ↦ (a.1, x)) I a.2)
g : ℝ × ℝ → F := fun a ↦ -(η a) (1, 0)
hg : ∀ a ∈ Icc 0 1, g a = (ω (ψ a)) (-derivWithin (ψ ∘ fun x ↦ (x, a.2)) I a.1)
this :
  (((∫ (x : ℝ) in 0..1, g (x, 1)) - ∫ (x : ℝ) in 0..1, g (x, 0)) + ∫ (y : ℝ) in 0..1, f (1, y)) -
      ∫ (y : ℝ) in 0..1, f (0, y) =
    0
s : ↑I
⊢ ∫ (t : ℝ) in 0..1, f (↑s, t) =
    ∫ (t : ℝ) in 0..1,
      (ω ({ toContinuousMap := φ.curry s, source' := ⋯, target' := ⋯ }.extend t))
        (derivWithin ⇑{ toContinuousMap := φ.curry s, source' := ⋯, target' := ⋯ }.extend I t)

Tactic:
apply intervalIntegral.integral_congr

Goal state after:
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
s✝ : Set (↑I × ↑I)
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s✝.Countable
hφt : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a_1, b_1) ∈ t
hω : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, (a_1, b_1) ∉ s✝ → HasFDerivWithinAt ω (dω (φ (a_1, b_1))) t (φ (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a_1 ∈ Ioo 0 1,
    ∀ b_1 ∈ Ioo 0 1,
      (a_1, b_1) ∉ s✝ →
        ∀ u ∈ tangentConeAt ℝ t (φ (a_1, b_1)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a_1, b_1)), ((dω (φ (a_1, b_1))) u) v = ((dω (φ (a_1, b_1))) v) u
U : Set (ℝ × ℝ) := ⋯
hU : U = Ioo 0 1 ×ˢ Ioo 0 1
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E := ⋯
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ : ψ = fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hψφ : ∀ (a_1 b_1 : ↑I), ψ (↑a_1, ↑b_1) = φ (a_1, b_1)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
hψUt : MapsTo ψ U t
dψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := ⋯
s' : Set (ℝ × ℝ) := ⋯
hs' : s' = Prod.map Subtype.val Subtype.val '' s✝
hmem_s' : ∀ (x y : ↑I), (↑x, ↑y) ∈ s' ↔ (x, y) ∈ s✝
hs'c : s'.Countable
hdψ : ∀ a ∈ U, HasFDerivAt ψ (dψ a) a
d2ψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] E := ⋯
hd2ψ : ∀ a ∈ U, HasFDerivAt dψ (d2ψ a) a
hd2ψ_symm : ∀ a ∈ Icc 0 1, ∀ (x y : ℝ × ℝ), ((d2ψ a) x) y = ((d2ψ a) y) x
η : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := ⋯
f : ℝ × ℝ → F := ⋯
hf : ∀ a ∈ Icc 0 1, f a = (ω (ψ a)) (derivWithin (ψ ∘ fun x ↦ (a.1, x)) I a.2)
g : ℝ × ℝ → F := ⋯
hg : ∀ a ∈ Icc 0 1, g a = (ω (ψ a)) (-derivWithin (ψ ∘ fun x ↦ (x, a.2)) I a.1)
this :
  (((∫ (x : ℝ) in 0..1, g (x, 1)) - ∫ (x : ℝ) in 0..1, g (x, 0)) + ∫ (y : ℝ) in 0..1, f (1, y)) -
      ∫ (y : ℝ) in 0..1, f (0, y) =
    0
s : ↑I
⊢ EqOn (fun x ↦ f (↑s, x))
    (fun x ↦
      (ω ({ toContinuousMap := φ.curry s, source' := ⋯, target' := ⋯ }.extend x))
        (derivWithin ⇑{ toContinuousMap := φ.curry s, source' := ⋯, target' := ⋯ }.extend I x))
    [[0, 1]]