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) → ℝ)
h :
  ∀ (x : F),
    Membership.mem (γ := Set F)
        (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) → ℝ)))
        x ↔
      x ∈ Set.Icc a b
⊢ 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

Tactic:
ext1 x
-- 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) → ℝ)
x : F
⊢ Membership.mem (γ := Set F)
      (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) → ℝ)))
      x ↔
    x ∈ Set.Icc a b

Tactic:
simp only [Set.mem_preimage, Set.mem_Icc, he_ord]

Premises used: Set.mem_Icc, Set.mem_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
rw :
  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) → ℝ))
    (Set.preimage (β := F) (⇑eL.symm : (a : Fin (n + 1) → ℝ) → F)
        (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 (Fin (n + 1) → ℝ))
rw₁ rw₂ :
  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) → ℝ))
    (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))
⊢ 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) → ℝ))

Tactic:
rw [← hIcc, eL.symm_preimage_preimage]

Premises used: ContinuousLinearEquiv.symm_preimage_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) → ℝ))
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : F) ↦ DF x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : F) ↦
      ∑ 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))

Tactic:
simp only [hDF]
-- 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) → ℝ))
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : F) ↦
      ∑ 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))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume
        (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) → ℝ))))
      fun (x : F) ↦
      ∑ i : Fin (n + 1),
        (f' i ((eL.symm : (a : Fin (n + 1) → ℝ) → F) ((eL : (a : F) → Fin (n + 1) → ℝ) x : Fin (n + 1) → ℝ)) :
            (a : F) → E)
          ((eL.symm : (a : Fin (n + 1) → ℝ) → F) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : F))

Tactic:
simp only [hIcc, eL.symm_apply_apply]

Premises used: ContinuousLinearEquiv.symm_apply_apply
-- 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) → ℝ))
⊢ ∀ (i : Fin (n + 1)),
    ContinuousOn.{0, u} (X := Fin (n + 1) → ℝ) (Y := E)
      ((fun (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ) ↦ f i ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x)) i :
        (x : Fin (n + 1) → ℝ) → E)
      (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))

Tactic:
fun i => (Hc i).comp eL.symm.continuousOn hIcc'.subset

Premises used: ContinuousLinearEquiv.symm, ContinuousOn.comp, Eq.subset, ContinuousLinearEquiv.continuousOn
-- 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) → ℝ))
⊢ ∀ (i : Fin (n + 1)),
    ContinuousOn.{0, u} (X := Fin (n + 1) → ℝ) (Y := E)
      ((fun (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ) ↦ f i ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x)) i :
        (x : Fin (n + 1) → ℝ) → E)
      (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))

Tactic:
exact fun i => (Hc i).comp eL.symm.continuousOn hIcc'.subset

Premises used: ContinuousLinearEquiv.symm, ContinuousOn.comp, Eq.subset, ContinuousLinearEquiv.continuousOn
-- 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)) → ℝ),
    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

Tactic:
fun x hx i => (Hd (eL.symm x) ⟨?_, hx.2⟩ i).comp x eL.symm.hasFDerivAt

Premises used: ContinuousLinearEquiv.symm, And.right, And.intro, ContinuousLinearEquiv.hasFDerivAt, DFunLike.coe, HasFDerivAt.comp
-- 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_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)
⊢ ∀ (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

Tactic:
refine fun x hx i => (Hd (eL.symm x) ⟨?_, hx.2⟩ i).comp x eL.symm.hasFDerivAt

Premises used: ContinuousLinearEquiv.symm, And.intro, ContinuousLinearEquiv.hasFDerivAt, DFunLike.coe, HasFDerivAt.comp
-- 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)
    (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)
⊢ Membership.mem (α := F) (interior (Set.Icc a b)) ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x : F)

Tactic:
rw [← hIcc]