-- 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
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a

Tactic:
have e_symm : ∀ x, e.symm x = x 0 := fun x => rfl

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
⊢ ∫ (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
⊢ (∫ (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:
have : ∀ c : ℝ, const (Fin 0) c = isEmptyElim := fun c => Subsingleton.elim _ _

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

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
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a

Tactic:
set e : ℝ ≃L[ℝ] ℝ¹ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).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
⊢ ∫ (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
⊢ ∫ (x : ℝ) in Set.Icc a b, 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)))

Tactic:
simp only [← interior_Icc] at Hd

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)
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 : ℝ) in Set.Icc a b, 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)))

Proof state:
case refine_2
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
⊢ MeasurePreserving (⇑e) volume volume

Tactic:
exact (volume_preserving_funUnique (Fin 1) ℝ).symm _

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 : 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
⊢ IntegrableOn f' (Set.Icc a b) volume

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hle] at Hi

Result:
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