awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F_1 : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : SecondCountableTopology F_1
f : E → F_1
s : Set E
f' : E → E →L[ℝ] F_1
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F_1) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F_1), r A ≠ 0
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F_1)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F_1) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F_1) (y - x) : F_1)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
closure_M_subset :
  ∀ (n : ℕ) (z : (↑T : Type u_1)), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → (↑T : Type u_1) → ℕ → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ) ↦
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ),
    ApproximatesLinearOn f (f' (↑(↑z : (↑s : Type u_1)) : E)) (s ∩ K n z p) (r (f' (↑(↑z : (↑s : Type u_1)) : E)))
K_closed :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
F : ℕ → ℕ × (↑T : Type u_1) × ℕ
hF : Function.Surjective F
x : E
xs : x ∈ s
n : ℕ
z : (↑T : Type u_1)
hnz : x ∈ M n z
p : ℕ
hp : x ∈ closedBall (d p) (u n / 3)
⊢ ∃ (q : ℕ), F q = (n, z, p)

Tactic:
hF _
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F_1 : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : SecondCountableTopology F_1
f : E → F_1
s : Set E
f' : E → E →L[ℝ] F_1
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F_1) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F_1), r A ≠ 0
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F_1)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F_1) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F_1) (y - x) : F_1)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
closure_M_subset :
  ∀ (n : ℕ) (z : (↑T : Type u_1)), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → (↑T : Type u_1) → ℕ → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ) ↦
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ),
    ApproximatesLinearOn f (f' (↑(↑z : (↑s : Type u_1)) : E)) (s ∩ K n z p) (r (f' (↑(↑z : (↑s : Type u_1)) : E)))
K_closed :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
F : ℕ → ℕ × (↑T : Type u_1) × ℕ
hF : Function.Surjective F
x : E
xs : x ∈ s
n : ℕ
z : (↑T : Type u_1)
hnz : x ∈ M n z
p : ℕ
hp : x ∈ closedBall (d p) (u n / 3)
inr :
  ∀ (q : ℕ) (hq : F q = (n, z, p)),
    Membership.mem (γ := Set E) (⋃ (n : ℕ), (fun (q : ℕ) ↦ K (F q).1 (F q).2.1 (F q).2.2) n) x
⊢ Membership.mem (γ := Set E) (⋃ (n : ℕ), (fun (q : ℕ) ↦ K (F q).1 (F q).2.1 (F q).2.2) n) x

Tactic:
obtain ⟨q, hq⟩ : ∃ q, F q = (n, z, p) := hF _

Premises used: Prod.mk
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F_1 : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : SecondCountableTopology F_1
f : E → F_1
s : Set E
f' : E → E →L[ℝ] F_1
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F_1) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F_1), r A ≠ 0
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F_1)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F_1) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F_1) (y - x) : F_1)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
closure_M_subset :
  ∀ (n : ℕ) (z : (↑T : Type u_1)), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → (↑T : Type u_1) → ℕ → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ) ↦
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ),
    ApproximatesLinearOn f (f' (↑(↑z : (↑s : Type u_1)) : E)) (s ∩ K n z p) (r (f' (↑(↑z : (↑s : Type u_1)) : E)))
K_closed :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
F : ℕ → ℕ × (↑T : Type u_1) × ℕ
hF : Function.Surjective F
x : E
xs : x ∈ s
n : ℕ
z : (↑T : Type u_1)
hnz : x ∈ M n z
p : ℕ
hp : x ∈ closedBall (d p) (u n / 3)
q : ℕ
hq : F q = (n, z, p)
apply : x ∈ K (F q).1 (F q).2.1 (F q).2.2
⊢ Membership.mem (γ := Set E) (⋃ (n : ℕ), (fun (q : ℕ) ↦ K (F q).1 (F q).2.1 (F q).2.2) n) x

Tactic:
apply mem_iUnion.2 ⟨q, _⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F_1 : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : SecondCountableTopology F_1
f : E → F_1
s : Set E
f' : E → E →L[ℝ] F_1
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F_1) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F_1), r A ≠ 0
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F_1)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F_1) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F_1) (y - x) : F_1)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
closure_M_subset :
  ∀ (n : ℕ) (z : (↑T : Type u_1)), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → (↑T : Type u_1) → ℕ → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ) ↦
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ),
    ApproximatesLinearOn f (f' (↑(↑z : (↑s : Type u_1)) : E)) (s ∩ K n z p) (r (f' (↑(↑z : (↑s : Type u_1)) : E)))
K_closed :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
F : ℕ → ℕ × (↑T : Type u_1) × ℕ
hF : Function.Surjective F
x : E
xs : x ∈ s
n : ℕ
z : (↑T : Type u_1)
hnz : x ∈ M n z
p : ℕ
hp : x ∈ closedBall (d p) (u n / 3)
q : ℕ
hq : F q = (n, z, p)
simp : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z)
⊢ x ∈ K (F q).1 (F q).2.1 (F q).2.2

Tactic:
simp -zeta only [K, hq, mem_inter_iff, hp, and_true]

Premises used: and_true, Set.mem_inter_iff
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F_1 : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : SecondCountableTopology F_1
f : E → F_1
s : Set E
f' : E → E →L[ℝ] F_1
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F_1) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F_1), r A ≠ 0
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F_1)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F_1) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F_1) (y - x) : F_1)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
closure_M_subset :
  ∀ (n : ℕ) (z : (↑T : Type u_1)), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → (↑T : Type u_1) → ℕ → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ) ↦
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ),
    ApproximatesLinearOn f (f' (↑(↑z : (↑s : Type u_1)) : E)) (s ∩ K n z p) (r (f' (↑(↑z : (↑s : Type u_1)) : E)))
K_closed :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
F : ℕ → ℕ × (↑T : Type u_1) × ℕ
hF : Function.Surjective F
x : E
xs : x ∈ s
n : ℕ
z : (↑T : Type u_1)
hnz : x ∈ M n z
p : ℕ
hp : x ∈ closedBall (d p) (u n / 3)
q : ℕ
hq : F q = (n, z, p)
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z)

Tactic:
subset_closure hnz

Premises used: subset_closure
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F_1 : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : SecondCountableTopology F_1
f : E → F_1
s : Set E
f' : E → E →L[ℝ] F_1
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F_1) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F_1), r A ≠ 0
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F_1)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F_1) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F_1) (y - x) : F_1)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
closure_M_subset :
  ∀ (n : ℕ) (z : (↑T : Type u_1)), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → (↑T : Type u_1) → ℕ → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ) ↦
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ),
    ApproximatesLinearOn f (f' (↑(↑z : (↑s : Type u_1)) : E)) (s ∩ K n z p) (r (f' (↑(↑z : (↑s : Type u_1)) : E)))
K_closed :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
F : ℕ → ℕ × (↑T : Type u_1) × ℕ
hF : Function.Surjective F
x : E
xs : x ∈ s
n : ℕ
z : (↑T : Type u_1)
hnz : x ∈ M n z
p : ℕ
hp : x ∈ closedBall (d p) (u n / 3)
q : ℕ
hq : F q = (n, z, p)
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z)

Tactic:
exact subset_closure hnz

Premises used: subset_closure
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
rcases :
  ∀ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F)
    (t_closed : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n))
    (st : s ⊆ ⋃ (n : ℕ), t n) (t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n)))
    (ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y),
    ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
      Pairwise (Disjoint on t) ∧
        (∀ (n : ℕ), MeasurableSet (t n)) ∧
          s ⊆ ⋃ (n : ℕ), t n ∧
            (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧
              (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)
⊢ ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
    Pairwise (Disjoint on t) ∧
      (∀ (n : ℕ), MeasurableSet (t n)) ∧
        s ⊆ ⋃ (n : ℕ), t n ∧
          (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)

Tactic:
rcases exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' r rpos with
    ⟨t, A, t_closed, st, t_approx, ht⟩

Premises used: exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)
st : s ⊆ ⋃ (n : ℕ), t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
    Pairwise (Disjoint on t) ∧
      (∀ (n : ℕ), MeasurableSet (t n)) ∧
        s ⊆ ⋃ (n : ℕ), t n ∧
          (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)

Tactic:
⟨disjointed t, A, disjoint_disjointed _,
      MeasurableSet.disjointed fun n => (t_closed n).measurableSet, ?_, ?_, ht⟩

Premises used: disjointed, IsClosed.measurableSet, And.intro, Exists.intro, MeasurableSet.disjointed, disjoint_disjointed
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)
st : s ⊆ ⋃ (n : ℕ), t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
refine_1 : s ⊆ ⋃ (n : ℕ), disjointed t n
refine_2 : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ disjointed t n) (r (A n))
⊢ ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
    Pairwise (Disjoint on t) ∧
      (∀ (n : ℕ), MeasurableSet (t n)) ∧
        s ⊆ ⋃ (n : ℕ), t n ∧
          (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)

Tactic:
refine
    ⟨disjointed t, A, disjoint_disjointed _,
      MeasurableSet.disjointed fun n => (t_closed n).measurableSet, ?_, ?_, ht⟩
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)
st : s ⊆ ⋃ (n : ℕ), t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
refine_1 : s ⊆ ⋃ (i : ℕ), t i
⊢ s ⊆ ⋃ (n : ℕ), disjointed t n

Tactic:
rw [iUnion_disjointed]

Premises used: iUnion_disjointed
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)
st : s ⊆ ⋃ (n : ℕ), t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ s ⊆ ⋃ (i : ℕ), t i

Tactic:
st
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)
st : s ⊆ ⋃ (n : ℕ), t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ s ⊆ ⋃ (i : ℕ), t i

Tactic:
exact st
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)
st : s ⊆ ⋃ (n : ℕ), t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
n : ℕ
⊢ ApproximatesLinearOn f (A n) (s ∩ disjointed t n) (r (A n))

Tactic:
(t_approx n).mono_set (inter_subset_inter_right _ (disjointed_subset _ _))

Premises used: Set.inter_subset_inter_right, ApproximatesLinearOn.mono_set, disjointed_subset
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)
st : s ⊆ ⋃ (n : ℕ), t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
n : ℕ
⊢ ApproximatesLinearOn f (A n) (s ∩ disjointed t n) (r (A n))

Tactic:
exact (t_approx n).mono_set (inter_subset_inter_right _ (disjointed_subset _ _))

Premises used: Set.inter_subset_inter_right, ApproximatesLinearOn.mono_set, disjointed_subset
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
a :
  Membership.mem (γ := Filter ℝ≥0) (𝓝 0)
    {x : ℝ≥0 |
      (fun (δ : ℝ≥0) ↦
          ∀ (s : Set E) (f : E → E),
            ApproximatesLinearOn f A s δ →
              (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
        x}
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝[>] 0,
    ∀ (s : Set E) (f : E → E),
      ApproximatesLinearOn f A s δ →
        (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
⊢ IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))

Tactic:
have HC : IsCompact (A '' closedBall 0 1) :=
      (ProperSpace.isCompact_closedBall _ _).image A.continuous
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
HC : IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
apply :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
    (𝓝 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)

Tactic:
apply Tendsto.mono_left _ nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
HC : IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
    (𝓝 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)

Tactic:
tendsto_measure_cthickening_of_isCompact HC

Premises used: tendsto_measure_cthickening_of_isCompact