-- Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
theorem integral_eq_of_hasDerivWithinAt_off_countable_of_le (f f' : ℝ → E) {a b : ℝ}
    (hle : a ≤ b) {s : Set ℝ} (hs : s.Countable) (Hc : ContinuousOn f (Icc a b))
    (Hd : ∀ x ∈ Ioo a b \ s, HasDerivAt f (f' x) x) (Hi : IntervalIntegrable f' volume a b) :
    ∫ x in a..b, f' x = f b - f a

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
e_symm : ∀ (x : Fin 1 → ℝ), e.symm x = x 0
F' : ℝ → ℝ →L[ℝ] E := fun x => smulRight 1 (f' x)
hF' : ∀ (x y : ℝ), (F' x) y = y • f' x
this : ∀ (c : ℝ), const (Fin 0) c = fun a => isEmptyElim a
⊢ (∫ (x : Fin 0 → ℝ) in
        Set.Icc ((ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm a ∘ Fin.succAbove 0)
          ((ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm b ∘ Fin.succAbove 0),
        f (Fin.insertNth 0 ((ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm b 0) x 0)) -
      ∫ (x : Fin 0 → ℝ) in
        Set.Icc ((ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm a ∘ Fin.succAbove 0)
          ((ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm b ∘ Fin.succAbove 0),
        f (Fin.insertNth 0 ((ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm a 0) x 0) =
    f b - f a

Tactic:
simp [this, volume_pi, Measure.pi_of_empty fun _ : Fin 0 => volume]

Result:
no goals

Proof state:
case refine_4
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hi : IntegrableOn f' (Set.Ioc a b) volume
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
e_symm : ∀ (x : Fin 1 → ℝ), e.symm x = x 0
F' : ℝ → ℝ →L[ℝ] E := fun x => smulRight 1 (f' x)
hF' : ∀ (x y : ℝ), (F' x) y = y • f' x
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ IntegrableOn f' (Set.Icc a b) volume

Tactic:
exact Hi.congr_set_ae Ioc_ae_eq_Icc.symm

Result:
no goals

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
e_symm : ∀ (x : Fin 1 → ℝ), e.symm x = x 0
F' : ℝ → ℝ →L[ℝ] E := fun x => smulRight 1 (f' x)
hF' : ∀ (x y : ℝ), (F' x) y = y • f' x
⊢ ∑ i : Fin 1,
      ((∫ (x : Fin 0 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), f (e.symm (i.insertNth (e b i) x))) -
        ∫ (x : Fin 0 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), f (e.symm (i.insertNth (e a i) x))) =
    f b - f a

Tactic:
simp only [e, Fin.sum_univ_one, e_symm]

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
e_symm : ∀ (x : Fin 1 → ℝ), e.symm x = x 0
F' : ℝ → ℝ →L[ℝ] E := fun x => smulRight 1 (f' x)
hF' : ∀ (x y : ℝ), (F' x) y = y • f' x
⊢ (∫ (x : Fin 0 → ℝ) in
        Set.Icc ((ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm a ∘ Fin.succAbove 0)
          ((ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm b ∘ Fin.succAbove 0),
        f (Fin.insertNth 0 ((ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm b 0) x 0)) -
      ∫ (x : Fin 0 → ℝ) in
        Set.Icc ((ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm a ∘ Fin.succAbove 0)
          ((ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm b ∘ Fin.succAbove 0),
        f (Fin.insertNth 0 ((ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm a 0) x 0) =
    f b - f a

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
e_symm : ∀ (x : Fin 1 → ℝ), e.symm x = x 0
F' : ℝ → ℝ →L[ℝ] E := fun x => smulRight 1 (f' x)
hF' : ∀ (x y : ℝ), (F' x) y = y • f' x
⊢ ∫ (x : ℝ) in a..b, f' x = ∫ (x : ℝ) in Set.Icc a b, f' x

Tactic:
rw [intervalIntegral.integral_of_le hle, setIntegral_congr_set Ioc_ae_eq_Icc]

Result:
no goals

Proof state:
case refine_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
e_symm : ∀ (x : Fin 1 → ℝ), e.symm x = x 0
F' : ℝ → ℝ →L[ℝ] E := fun x => smulRight 1 (f' x)
hF' : ∀ (x y : ℝ), (F' x) y = y • f' x
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ ∀ (x y : ℝ), e x ≤ e y ↔ x ≤ y

Tactic:
exact fun x y => (OrderIso.funUnique (Fin 1) ℝ).symm.le_iff_le

Result:
no goals