awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : Preorder F
inst_5 : MeasureSpace F
inst_6 : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord :
  ∀ (x y : F),
    LE.le (α := Fin (n + 1) → ℝ) ((eL : (a : F) → Fin (n + 1) → ℝ) x : Fin (n + 1) → ℝ)
        ((eL : (a : F) → Fin (n + 1) → ℝ) y : Fin (n + 1) → ℝ) ↔
      x ≤ y
he_vol : MeasurePreserving (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF :
  ∀ (x : F),
    DF x =
      ∑ i : Fin (n + 1),
        (f' i x : (a : F) → E)
          ((eL.symm : (a : Fin (n + 1) → ℝ) → F) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : F)
Hi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ)
hIcc :
  Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
      (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ)) =
    Set.Icc a b
hIcc' :
  Eq (α := Set (Fin (n + 1) → ℝ))
    (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))
    ((⇑eL.symm : (a : Fin (n + 1) → ℝ) → F) ⁻¹' Set.Icc a b : Set (Fin (n + 1) → ℝ))
x : (i : Fin (n + 1)) → ℝ
hx :
  Membership.mem (γ := Set ((i : Fin (n + 1)) → ℝ))
    ((Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦
        Set.Ioo ((eL : (a : F) → Fin (n + 1) → ℝ) a i) ((eL : (a : F) → Fin (n + 1) → ℝ) b i)) \
      (⇑eL.symm : (a : Fin (n + 1) → ℝ) → F) ⁻¹' s)
    x
i : Fin (n + 1)
⊢ Membership.mem (α := F) (γ := Set F)
    (interior
      (Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
        (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))))
    ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x : F)

Tactic:
preimage_interior_subset_interior_preimage eL.continuous ?_

Premises used: Set.Mem, preimage_interior_subset_interior_preimage, ContinuousLinearEquiv.continuous
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : Preorder F
inst_5 : MeasureSpace F
inst_6 : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord :
  ∀ (x y : F),
    LE.le (α := Fin (n + 1) → ℝ) ((eL : (a : F) → Fin (n + 1) → ℝ) x : Fin (n + 1) → ℝ)
        ((eL : (a : F) → Fin (n + 1) → ℝ) y : Fin (n + 1) → ℝ) ↔
      x ≤ y
he_vol : MeasurePreserving (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF :
  ∀ (x : F),
    DF x =
      ∑ i : Fin (n + 1),
        (f' i x : (a : F) → E)
          ((eL.symm : (a : Fin (n + 1) → ℝ) → F) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : F)
Hi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ)
hIcc :
  Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
      (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ)) =
    Set.Icc a b
hIcc' :
  Eq (α := Set (Fin (n + 1) → ℝ))
    (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))
    ((⇑eL.symm : (a : Fin (n + 1) → ℝ) → F) ⁻¹' Set.Icc a b : Set (Fin (n + 1) → ℝ))
x : (i : Fin (n + 1)) → ℝ
hx :
  Membership.mem (γ := Set ((i : Fin (n + 1)) → ℝ))
    ((Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦
        Set.Ioo ((eL : (a : F) → Fin (n + 1) → ℝ) a i) ((eL : (a : F) → Fin (n + 1) → ℝ) b i)) \
      (⇑eL.symm : (a : Fin (n + 1) → ℝ) → F) ⁻¹' s)
    x
i : Fin (n + 1)
refine_2 :
  Membership.mem (α := F) (γ := Set F)
    (Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
      (interior (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b)) :
        Set (Fin (n + 1) → ℝ)))
    ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x : F)
⊢ Membership.mem (α := F) (γ := Set F)
    (interior
      (Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
        (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))))
    ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x : F)

Tactic:
refine preimage_interior_subset_interior_preimage eL.continuous ?_

Premises used: preimage_interior_subset_interior_preimage, ContinuousLinearEquiv.continuous
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : Preorder F
inst_5 : MeasureSpace F
inst_6 : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord :
  ∀ (x y : F),
    LE.le (α := Fin (n + 1) → ℝ) ((eL : (a : F) → Fin (n + 1) → ℝ) x : Fin (n + 1) → ℝ)
        ((eL : (a : F) → Fin (n + 1) → ℝ) y : Fin (n + 1) → ℝ) ↔
      x ≤ y
he_vol : MeasurePreserving (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF :
  ∀ (x : F),
    DF x =
      ∑ i : Fin (n + 1),
        (f' i x : (a : F) → E)
          ((eL.symm : (a : Fin (n + 1) → ℝ) → F) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : F)
Hi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ)
hIcc :
  Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
      (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ)) =
    Set.Icc a b
hIcc' :
  Eq (α := Set (Fin (n + 1) → ℝ))
    (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))
    ((⇑eL.symm : (a : Fin (n + 1) → ℝ) → F) ⁻¹' Set.Icc a b : Set (Fin (n + 1) → ℝ))
x : (i : Fin (n + 1)) → ℝ
hx :
  Membership.mem (γ := Set ((i : Fin (n + 1)) → ℝ))
    ((Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦
        Set.Ioo ((eL : (a : F) → Fin (n + 1) → ℝ) a i) ((eL : (a : F) → Fin (n + 1) → ℝ) b i)) \
      (⇑eL.symm : (a : Fin (n + 1) → ℝ) → F) ⁻¹' s)
    x
i : Fin (n + 1)
⊢ Membership.mem (α := F) (γ := Set F)
    (Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
      (interior (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b)) :
        Set (Fin (n + 1) → ℝ)))
    ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x : F)

Tactic:
simpa only [Set.mem_preimage, eL.apply_symm_apply, ← pi_univ_Icc,
          interior_pi_set (@finite_univ (Fin _) _), interior_Icc] using hx.1

Premises used: ContinuousLinearEquiv.apply_symm_apply, interior_Icc, And.left, Set.finite_univ, interior_pi_set, Set.mem_preimage, Set.pi_univ_Icc
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : Preorder F
inst_5 : MeasureSpace F
inst_6 : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord :
  ∀ (x y : F),
    LE.le (α := Fin (n + 1) → ℝ) ((eL : (a : F) → Fin (n + 1) → ℝ) x : Fin (n + 1) → ℝ)
        ((eL : (a : F) → Fin (n + 1) → ℝ) y : Fin (n + 1) → ℝ) ↔
      x ≤ y
he_vol : MeasurePreserving (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF :
  ∀ (x : F),
    DF x =
      ∑ i : Fin (n + 1),
        (f' i x : (a : F) → E)
          ((eL.symm : (a : Fin (n + 1) → ℝ) → F) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : F)
Hi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ)
hIcc :
  Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
      (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ)) =
    Set.Icc a b
hIcc' :
  Eq (α := Set (Fin (n + 1) → ℝ))
    (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))
    ((⇑eL.symm : (a : Fin (n + 1) → ℝ) → F) ⁻¹' Set.Icc a b : Set (Fin (n + 1) → ℝ))
refine_3 :
  IntegrableOn.{u_1, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    ((fun (x : Fin (n + 1) → ℝ) ↦
        ∑ i : Fin (n + 1),
          ((fun (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ) ↦
                  f' i ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x) ∘SL (↑eL.symm : (Fin (n + 1) → ℝ) →L[ℝ] F))
                i x :
              (a : Fin (n + 1) → ℝ) → E)
            (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1)) ∘
      (⇑eL : (a : F) → Fin (n + 1) → ℝ))
    (Set.Icc a b) volume
⊢ IntegrableOn.{0, u} (α := Fin (n + 1) → ℝ) (ε := E) (mα :=
    (MeasureSpace.toMeasurableSpace : MeasurableSpace (Fin (n + 1) → ℝ)))
    (fun (x : Fin (n + 1) → ℝ) ↦
      (∑ i : Fin (n + 1),
          ((fun (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ) ↦
                  f' i ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x) ∘SL (↑eL.symm : (Fin (n + 1) → ℝ) →L[ℝ] F))
                i x :
              (a : Fin (n + 1) → ℝ) → E)
            (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) :
        E))
    (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))
    (volume : Measure (Fin (n + 1) → ℝ))

Tactic:
rw [← he_vol.integrableOn_comp_preimage he_emb, hIcc]

Premises used: MeasureTheory.MeasurePreserving.integrableOn_comp_preimage
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : Preorder F
inst_5 : MeasureSpace F
inst_6 : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord :
  ∀ (x y : F),
    LE.le (α := Fin (n + 1) → ℝ) ((eL : (a : F) → Fin (n + 1) → ℝ) x : Fin (n + 1) → ℝ)
        ((eL : (a : F) → Fin (n + 1) → ℝ) y : Fin (n + 1) → ℝ) ↔
      x ≤ y
he_vol : MeasurePreserving (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF :
  ∀ (x : F),
    DF x =
      ∑ i : Fin (n + 1),
        (f' i x : (a : F) → E)
          ((eL.symm : (a : Fin (n + 1) → ℝ) → F) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : F)
Hi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ)
hIcc :
  Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
      (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ)) =
    Set.Icc a b
hIcc' :
  Eq (α := Set (Fin (n + 1) → ℝ))
    (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))
    ((⇑eL.symm : (a : Fin (n + 1) → ℝ) → F) ⁻¹' Set.Icc a b : Set (Fin (n + 1) → ℝ))
⊢ IntegrableOn.{u_1, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    ((fun (x : Fin (n + 1) → ℝ) ↦
        ∑ i : Fin (n + 1),
          ((fun (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ) ↦
                  f' i ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x) ∘SL (↑eL.symm : (Fin (n + 1) → ℝ) →L[ℝ] F))
                i x :
              (a : Fin (n + 1) → ℝ) → E)
            (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1)) ∘
      (⇑eL : (a : F) → Fin (n + 1) → ℝ))
    (Set.Icc a b) volume

Tactic:
simp [← hDF, Function.comp_def, Hi]

Premises used: Function.comp_def
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : 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.symm (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ)
F' : ℝ → ℝ →L[ℝ] E := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
rw :
  Eq.{u + 1} (α := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Ioc a b)) fun (x : ℝ) ↦ f' x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : ℝ) ↦ f' x)
rw₁ rw₂ :
  Eq.{u + 1} (α := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : ℝ) ↦ f' x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : ℝ) ↦ f' x)
⊢ Eq.{u + 1} (α := E) (∫ (x : ℝ) in a..b, f' x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : ℝ) ↦ f' x)

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

Premises used: MeasureTheory.Ioc_ae_eq_Icc, intervalIntegral.integral_of_le, MeasureTheory.setIntegral_congr_set
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : 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.symm (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ)
F' : ℝ → ℝ →L[ℝ] E := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
⊢ ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x

Tactic:
simp only [← interior_Icc] at Hd

Premises used: interior_Icc
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : 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.symm (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ)
F' : ℝ → ℝ →L[ℝ] E := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : ℝ) ↦ f' x)
    (∑ i : Fin 1,
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ) → Fin 1 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ) → Fin 1 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 0 → ℝ) ↦
          f ((e.symm : (a : Fin 1 → ℝ) → ℝ) (i.insertNth (α := fun (a : Fin 1) ↦ ℝ) ((e : (a : ℝ) → Fin 1 → ℝ) b i) x)))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ) → Fin 1 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ) → Fin 1 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 0 → ℝ) ↦
          f
            ((e.symm : (a : Fin 1 → ℝ) → ℝ)
              (i.insertNth (α := fun (a : Fin 1) ↦ ℝ) ((e : (a : ℝ) → Fin 1 → ℝ) a i) x))))

Tactic:
integral_divergence_of_hasFDerivAt_off_countable_of_equiv e ?_ ?_ (fun _ => f)
          (fun _ => F') s hs a b hle (fun _ => Hc) (fun x hx _ => Hd x hx) _ ?_ ?_

Premises used: MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_of_equiv
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : 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.symm (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ)
F' : ℝ → ℝ →L[ℝ] E := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
refine_1 :
  ∀ (x y : ℝ),
    LE.le (α := Fin (HAdd.hAdd (α := ℕ) 0 1) → ℝ) ((e : (a : ℝ) → Fin (0 + 1) → ℝ) x : Fin (HAdd.hAdd (α := ℕ) 0 1) → ℝ)
        ((e : (a : ℝ) → Fin (0 + 1) → ℝ) y : Fin (HAdd.hAdd (α := ℕ) 0 1) → ℝ) ↔
      x ≤ y
refine_2 :
  MeasurePreserving (α := ℝ) (β := Fin (HAdd.hAdd (α := ℕ) 0 1) → ℝ) (⇑e : (a : ℝ) → Fin (0 + 1) → ℝ) volume volume
refine_3 :
  ∀ (x : ℝ),
    f' x =
      ∑ i : Fin (0 + 1),
        ((fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ F') i x : (a : ℝ) → E)
          ((e.symm : (a : Fin (0 + 1) → ℝ) → ℝ) (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ ℝ) i 1) : ℝ)
refine_4 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Set.Icc a b) volume
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : ℝ) ↦ f' x)
    (∑ i : Fin 1,
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ) → Fin 1 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ) → Fin 1 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 0 → ℝ) ↦
          f ((e.symm : (a : Fin 1 → ℝ) → ℝ) (i.insertNth (α := fun (a : Fin 1) ↦ ℝ) ((e : (a : ℝ) → Fin 1 → ℝ) b i) x)))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ) → Fin 1 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ) → Fin 1 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 0 → ℝ) ↦
          f
            ((e.symm : (a : Fin 1 → ℝ) → ℝ)
              (i.insertNth (α := fun (a : Fin 1) ↦ ℝ) ((e : (a : ℝ) → Fin 1 → ℝ) a i) x))))

Tactic:
refine
        integral_divergence_of_hasFDerivAt_off_countable_of_equiv e ?_ ?_ (fun _ => f)
          (fun _ => F') s hs a b hle (fun _ => Hc) (fun x hx _ => Hd x hx) _ ?_ ?_

Premises used: MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_of_equiv
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : 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.symm (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ)
F' : ℝ → ℝ →L[ℝ] E := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ ∀ (x y : ℝ),
    LE.le (α := Fin (HAdd.hAdd (α := ℕ) 0 1) → ℝ) ((e : (a : ℝ) → Fin (0 + 1) → ℝ) x : Fin (HAdd.hAdd (α := ℕ) 0 1) → ℝ)
        ((e : (a : ℝ) → Fin (0 + 1) → ℝ) y : Fin (HAdd.hAdd (α := ℕ) 0 1) → ℝ) ↔
      x ≤ y

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

Premises used: Real, OrderIso.funUnique, OrderIso.le_iff_le, OrderIso.symm, OfNat.ofNat, Fin
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : 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.symm (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ)
F' : ℝ → ℝ →L[ℝ] E := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ MeasurePreserving (α := ℝ) (β := Fin (HAdd.hAdd (α := ℕ) 0 1) → ℝ) (⇑e : (a : ℝ) → Fin (0 + 1) → ℝ) volume volume

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

Premises used: Eq.mpr, Real, MeasureTheory.MeasurePreserving.symm, List.ofFn, Fin.ofNat, Fin.foldr.loop, Multiset.cons, Multiset.ofList, uniqueElim, OfNat.ofNat, Fin, List.finRange, MeasureTheory.volume_preserving_funUnique
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : 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.symm (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ)
F' : ℝ → ℝ →L[ℝ] E := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ MeasurePreserving (α := ℝ) (β := Fin (HAdd.hAdd (α := ℕ) 0 1) → ℝ) (⇑e : (a : ℝ) → Fin (0 + 1) → ℝ) volume volume

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

Premises used: Real, MeasureTheory.MeasurePreserving.symm, OfNat.ofNat, Fin, MeasureTheory.volume_preserving_funUnique
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : 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.symm (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ)
F' : ℝ → ℝ →L[ℝ] E := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ ∀ (x : ℝ),
    f' x =
      ∑ i : Fin (0 + 1),
        ((fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ F') i x : (a : ℝ) → E)
          ((e.symm : (a : Fin (0 + 1) → ℝ) → ℝ) (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ ℝ) i 1) : ℝ)

Tactic:
simp [F', e]
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : 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.symm (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ)
F' : ℝ → ℝ →L[ℝ] E := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ IntegrableOn (mα := Real.measurableSpace) f' (Set.Ioc a b) volume

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hle] at Hi

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : 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.symm (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ)
F' : ℝ → ℝ →L[ℝ] E := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
Hi₁ : IntegrableOn (mα := Real.measurableSpace) f' (Set.Ioc a b) volume
⊢ ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hle] at Hi

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le