awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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)) → ℝ),
    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)),
        HasFDerivAt.{0, 0, u} (𝕜 := ℝ) (F := E)
          ((fun (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ) ↦ f i ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x)) i)
          ((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)
          x
have refine_2 : ∀ (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) (interior (Set.Icc a b)) ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x : F)
Tactic: refine fun x hx i => (Hd (eL.symm x) ⟨?_, hx.2⟩ i).comp x eL.symm.hasFDerivAt
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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) (interior (Set.Icc a b)) ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x : F)
have refine_2 : 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: rw [← hIcc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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)
have 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)
Tactic: refine preimage_interior_subset_interior_preimage eL.continuous ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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.{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) → ℝ))
have 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
Tactic: rw [← he_vol.integrableOn_comp_preimage he_emb, hIcc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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)
⊢ Eq.{u + 1} (α := E) (∫ (x : ℝ) in a..b, f' x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : ℝ) ↦ f' x)
have 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)
Tactic: rw [intervalIntegral.integral_of_le hle, setIntegral_congr_set Ioc_ae_eq_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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)
⊢ Eq.{u + 1} (α := E) (∫ (x : ℝ) in a..b, f' x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : ℝ) ↦ f' x)
have 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)
Tactic: rw [intervalIntegral.integral_of_le hle, setIntegral_congr_set Ioc_ae_eq_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (hypothesis)
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)
⊢ 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))))
have Hd₁ : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
Tactic: simp only [← interior_Icc] at Hd
Cleared hypotheses: Hd
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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))))
have 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
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) _ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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
⊢ 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))))
have refine_2 : MeasurePreserving (α := ℝ) (β := Fin (HAdd.hAdd (α := ℕ) 0 1) → ℝ) (⇑e : (a : ℝ) → Fin (0 + 1) → ℝ) volume volume
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) _ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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
⊢ 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))))
have 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) : ℝ)
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) _ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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) : ℝ)
⊢ 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))))
have refine_4 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Set.Icc a b) volume
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) _ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (hypothesis)
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α := MeasureSpace.toMeasurableSpace) f' (Set.Icc a b) volume
have Hi₁ : IntegrableOn (mα := Real.measurableSpace) f' (Set.Ioc a b) volume
Tactic: rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hle] at Hi
Cleared hypotheses: Hi, e, F', Hd