case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i : Fin (n + 1), ↑(f' x) (e i) i) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (a i) x) i)

case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
hne : ¬∃ i, a i = b i
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i : Fin (n + 1), ↑(f' x) (e i) i) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (a i) x) i)
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i : Fin (n + 1), ↑(f' x) (e i) i) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (a i) x) i)
rcases em (∃ i, a i = b i) with (⟨i, hi⟩ | hne)
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.pi Set.univ fun i => Set.Ioc (a i) (b i),
      ∑ i : Fin (n + 1), ↑(f' x) (e i) i ∂Measure.pi fun x => volume) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (a i) x) i)
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i : Fin (n + 1), ↑(f' x) (e i) i) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (a i) x) i)
rw [volume_pi, ← set_integral_congr_set_ae Measure.univ_pi_Ioc_ae_eq_Icc]
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.pi Set.univ fun i => Set.Ioc (a i) (b i),
      ∑ i : Fin (n + 1), ↑(f' x) (e i) i ∂Measure.pi fun x => volume) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (a i) x) i)
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.pi Set.univ fun i => Set.Ioc (a i) (b i),
      ∑ i : Fin (n + 1), ↑(f' x) (e i) i ∂Measure.pi fun x => volume) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (a i) x) i)
have hi' : Ioc (a i) (b i) = ∅ := Ioc_eq_empty hi.not_lt
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.pi Set.univ fun i => Set.Ioc (a i) (b i),
      ∑ i : Fin (n + 1), ↑(f' x) (e i) i ∂Measure.pi fun x => volume) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (a i) x) i)
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.pi Set.univ fun i => Set.Ioc (a i) (b i),
      ∑ i : Fin (n + 1), ↑(f' x) (e i) i ∂Measure.pi fun x => volume) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (a i) x) i)
have : (pi Set.univ fun j => Ioc (a j) (b j)) = ∅ := univ_pi_eq_empty hi'
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
⊢ ∀ (x : Fin (n + 1)),
    x ∈ Finset.univ →
      ((∫ (x_1 : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove x)) (b ∘ ↑(Fin.succAbove x)),
            f (Fin.insertNth x (b x) x_1) x) -
          ∫ (x_1 : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove x)) (b ∘ ↑(Fin.succAbove x)),
            f (Fin.insertNth x (a x) x_1) x) =
        0
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.pi Set.univ fun i => Set.Ioc (a i) (b i),
      ∑ i : Fin (n + 1), ↑(f' x) (e i) i ∂Measure.pi fun x => volume) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (a i) x) i)
rw [this, integral_empty, sum_eq_zero]
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
⊢ ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (a j) x) j) =
    0
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
⊢ ∀ (x : Fin (n + 1)),
    x ∈ Finset.univ →
      ((∫ (x_1 : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove x)) (b ∘ ↑(Fin.succAbove x)),
            f (Fin.insertNth x (b x) x_1) x) -
          ∫ (x_1 : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove x)) (b ∘ ↑(Fin.succAbove x)),
            f (Fin.insertNth x (a x) x_1) x) =
        0
rintro j -
case inl.intro.inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
⊢ ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (b i) x) i) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (a i) x) i) =
    0

case inl.intro.inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
hne : i ≠ j
⊢ ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (a j) x) j) =
    0
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
⊢ ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (a j) x) j) =
    0
rcases eq_or_ne i j with (rfl | hne)
no goals
case inl.intro.inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
⊢ ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (b i) x) i) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (a i) x) i) =
    0
simp [hi]
case inl.intro.inr.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
i : Fin n
hi : a (↑(Fin.succAbove j) i) = b (↑(Fin.succAbove j) i)
hi' : Set.Ioc (a (↑(Fin.succAbove j) i)) (b (↑(Fin.succAbove j) i)) = ∅
hne : ↑(Fin.succAbove j) i ≠ j
⊢ ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (a j) x) j) =
    0
case inl.intro.inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
hne : i ≠ j
⊢ ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (a j) x) j) =
    0
rcases Fin.exists_succAbove_eq hne with ⟨i, rfl⟩
case this
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
i : Fin n
hi : a (↑(Fin.succAbove j) i) = b (↑(Fin.succAbove j) i)
hi' : Set.Ioc (a (↑(Fin.succAbove j) i)) (b (↑(Fin.succAbove j) i)) = ∅
hne : ↑(Fin.succAbove j) i ≠ j
⊢ Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)) =ᵐ[volume] ∅

case inl.intro.inr.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
this✝ : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
i : Fin n
hi : a (↑(Fin.succAbove j) i) = b (↑(Fin.succAbove j) i)
hi' : Set.Ioc (a (↑(Fin.succAbove j) i)) (b (↑(Fin.succAbove j) i)) = ∅
hne : ↑(Fin.succAbove j) i ≠ j
this : Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)) =ᵐ[volume] ∅
⊢ ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (a j) x) j) =
    0
case inl.intro.inr.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
i : Fin n
hi : a (↑(Fin.succAbove j) i) = b (↑(Fin.succAbove j) i)
hi' : Set.Ioc (a (↑(Fin.succAbove j) i)) (b (↑(Fin.succAbove j) i)) = ∅
hne : ↑(Fin.succAbove j) i ≠ j
⊢ ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (a j) x) j) =
    0
have : Icc (a ∘ j.succAbove) (b ∘ j.succAbove) =ᵐ[volume] (∅ : Set ℝⁿ)
no goals
case inl.intro.inr.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
this✝ : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
i : Fin n
hi : a (↑(Fin.succAbove j) i) = b (↑(Fin.succAbove j) i)
hi' : Set.Ioc (a (↑(Fin.succAbove j) i)) (b (↑(Fin.succAbove j) i)) = ∅
hne : ↑(Fin.succAbove j) i ≠ j
this : Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)) =ᵐ[volume] ∅
⊢ ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)), f (Fin.insertNth j (a j) x) j) =
    0
rw [set_integral_congr_set_ae this, set_integral_congr_set_ae this, integral_empty,
  integral_empty, sub_self]
case this
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
i : Fin n
hi : a (↑(Fin.succAbove j) i) = b (↑(Fin.succAbove j) i)
hi' : Set.Ioc (a (↑(Fin.succAbove j) i)) (b (↑(Fin.succAbove j) i)) = ∅
hne : ↑(Fin.succAbove j) i ≠ j
⊢ ENNReal.ofReal ((b ∘ ↑(Fin.succAbove j)) i - (a ∘ ↑(Fin.succAbove j)) i) = 0
case this
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
i : Fin n
hi : a (↑(Fin.succAbove j) i) = b (↑(Fin.succAbove j) i)
hi' : Set.Ioc (a (↑(Fin.succAbove j) i)) (b (↑(Fin.succAbove j) i)) = ∅
hne : ↑(Fin.succAbove j) i ≠ j
⊢ Set.Icc (a ∘ ↑(Fin.succAbove j)) (b ∘ ↑(Fin.succAbove j)) =ᵐ[volume] ∅
rw [ae_eq_empty, Real.volume_Icc_pi, prod_eq_zero (Finset.mem_univ i)]
no goals
case this
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
this : (Set.pi Set.univ fun j => Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
i : Fin n
hi : a (↑(Fin.succAbove j) i) = b (↑(Fin.succAbove j) i)
hi' : Set.Ioc (a (↑(Fin.succAbove j) i)) (b (↑(Fin.succAbove j) i)) = ∅
hne : ↑(Fin.succAbove j) i ≠ j
⊢ ENNReal.ofReal ((b ∘ ↑(Fin.succAbove j)) i - (a ∘ ↑(Fin.succAbove j)) i) = 0
simp [hi]
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
hne : ¬∃ i, a i = b i
hlt : ∀ (i : Fin (n + 1)), a i < b i
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i : Fin (n + 1), ↑(f' x) (e i) i) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (a i) x) i)
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
hne : ¬∃ i, a i = b i
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i : Fin (n + 1), ↑(f' x) (e i) i) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (a i) x) i)
have hlt : ∀ i, a i < b i := fun i => (hle i).lt_of_ne fun hi => hne ⟨i, hi⟩
no goals
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ (Set.pi Set.univ fun i => Set.Ioo (a i) (b i)) \ s → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (Set.Icc a b)
hne : ¬∃ i, a i = b i
hlt : ∀ (i : Fin (n + 1)), a i < b i
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i : Fin (n + 1), ↑(f' x) (e i) i) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ ↑(Fin.succAbove i)) (b ∘ ↑(Fin.succAbove i)), f (Fin.insertNth i (a i) x) i)
exact integral_divergence_of_hasFDerivWithinAt_off_countable_aux₂ ⟨a, b, hlt⟩ f f' s hs Hc
  Hd Hi