awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
ι : Type u_1
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
inst_2 : Infinite ι
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
hr₀ : r ≠ 0
hr : ∀ (i : ι), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s i)
t : Set ℕ
ht : t.Infinite
h :
  ∀ ⦃u : Set ℕ⦄,
    u ⊆ t →
      u.Finite →
        LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n)) : ℝ≥0∞)
u : Set ι
hut : u ⊆ (⇑(Infinite.natEmbedding ι) : (a : ℕ) → ι) '' t
hu : u.Finite
n : ℕ
hi : Membership.mem (α := ι) u ((Infinite.natEmbedding ι : (a : ℕ) → ι) n : ι)
⊢ ⋂ (n : ℕ),
      ⋂ (_ : Membership.mem (γ := Set ℕ) ((⇑(Infinite.natEmbedding ι) : (a : ℕ) → ι) ⁻¹' u) n),
        s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n) ⊆
    s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n)

Tactic:
exact iInter₂_subset n hi

Premises used: Set.iInter₂_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 : 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
inl :
  ∀ (hf' : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → HasFDerivWithinAt f (f' x) ∅ x),
    ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
      (∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)) ∧
        Subset.{u_1} (α := Set E) ∅ (⋃ (n : ℕ), t n) ∧
          (∀ (n : ℕ), ApproximatesLinearOn f (A n) (∅ ∩ t n) (r (A n))) ∧
            (Set.Nonempty.{u_1} (α := E) ∅ → ∀ (n : ℕ), ∃ (y : E), Membership.mem (γ := Set E) ∅ y ∧ A n = f' y)
inr :
  ∀ (hs : s.Nonempty),
    ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
      (∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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),
    (∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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 eq_empty_or_nonempty s with (rfl | hs)

Premises used: Set.eq_empty_or_nonempty, rfl
-- 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 : SecondCountableTopology F
f : E → F
f' : E → E →L[ℝ] F
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hf' : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → HasFDerivWithinAt f (f' x) ∅ x
⊢ ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
    (∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)) ∧
      Subset.{u_1} (α := Set E) ∅ (⋃ (n : ℕ), t n) ∧
        (∀ (n : ℕ), ApproximatesLinearOn f (A n) (∅ ∩ t n) (r (A n))) ∧
          (Set.Nonempty.{u_1} (α := E) ∅ → ∀ (n : ℕ), ∃ (y : E), Membership.mem (γ := Set E) ∅ y ∧ A n = f' y)

Tactic:
⟨fun _ => ∅, fun _ => 0, ?_, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro, EmptyCollection.emptyCollection, OfNat.ofNat
-- 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 : SecondCountableTopology F
f : E → F
f' : E → E →L[ℝ] F
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hf' : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → HasFDerivWithinAt f (f' x) ∅ x
inl : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((fun (x : ℕ) ↦ (∅ : Set E)) n)
inl₁ : Subset.{u_1} (α := Set E) ∅ (⋃ (n : ℕ), (fun (x : ℕ) ↦ (∅ : Set E)) n)
inl₂ :
  ∀ (n : ℕ),
    ApproximatesLinearOn (𝕜 := ℝ) f ((fun (x : ℕ) ↦ (0 : E →L[ℝ] F)) n) (∅ ∩ (fun (x : ℕ) ↦ (∅ : Set E)) n)
      (r ((fun (x : ℕ) ↦ (0 : E →L[ℝ] F)) n))
inl₃ :
  Set.Nonempty.{u_1} (α := E) ∅ →
    ∀ (n : ℕ), ∃ (y : E), Membership.mem (γ := Set E) ∅ y ∧ (fun (x : ℕ) ↦ (0 : E →L[ℝ] F)) n = f' y
⊢ ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
    (∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)) ∧
      Subset.{u_1} (α := Set E) ∅ (⋃ (n : ℕ), t n) ∧
        (∀ (n : ℕ), ApproximatesLinearOn f (A n) (∅ ∩ t n) (r (A n))) ∧
          (Set.Nonempty.{u_1} (α := E) ∅ → ∀ (n : ℕ), ∃ (y : E), Membership.mem (γ := Set E) ∅ y ∧ A n = f' y)

Tactic:
refine ⟨fun _ => ∅, fun _ => 0, ?_, ?_, ?_, ?_⟩
-- 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 : SecondCountableTopology F
f : E → F
f' : E → E →L[ℝ] F
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hf' : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → HasFDerivWithinAt f (f' x) ∅ x
⊢ ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((fun (x : ℕ) ↦ (∅ : Set E)) n)

Tactic:
simp
-- 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 : SecondCountableTopology F
f : E → F
f' : E → E →L[ℝ] F
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hf' : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → HasFDerivWithinAt f (f' x) ∅ x
⊢ Subset.{u_1} (α := Set E) ∅ (⋃ (n : ℕ), (fun (x : ℕ) ↦ (∅ : Set E)) n)

Tactic:
simp
-- 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 : SecondCountableTopology F
f : E → F
f' : E → E →L[ℝ] F
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hf' : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → HasFDerivWithinAt f (f' x) ∅ x
⊢ ∀ (n : ℕ),
    ApproximatesLinearOn (𝕜 := ℝ) f ((fun (x : ℕ) ↦ (0 : E →L[ℝ] F)) n) (∅ ∩ (fun (x : ℕ) ↦ (∅ : Set E)) n)
      (r ((fun (x : ℕ) ↦ (0 : E →L[ℝ] F)) n))

Tactic:
simp
-- 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 : SecondCountableTopology F
f : E → F
f' : E → E →L[ℝ] F
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hf' : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → HasFDerivWithinAt f (f' x) ∅ x
⊢ Set.Nonempty.{u_1} (α := E) ∅ →
    ∀ (n : ℕ), ∃ (y : E), Membership.mem (γ := Set E) ∅ y ∧ (fun (x : ℕ) ↦ (0 : E →L[ℝ] F)) n = f' y

Tactic:
simp
-- 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 : 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
hs : s.Nonempty
⊢ ∃ (T : Set (↑s : Type u_1)),
    T.Countable ∧
      Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
        (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))

Tactic:
TopologicalSpace.isOpen_iUnion_countable _ fun x => isOpen_ball

Premises used: TopologicalSpace.isOpen_iUnion_countable, Metric.isOpen_ball
-- 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 : 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
hs : s.Nonempty
inr :
  ∀ (T : Set (↑s : Type u_1)) (T_count : T.Countable)
    (hT :
      Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
        (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))),
    ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
      (∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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),
    (∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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:
obtain ⟨T, T_count, hT⟩ :
    ∃ T : Set s,
      T.Countable ∧ ⋃ x ∈ T, ball (f' (x : E)) (r (f' x)) = ⋃ x : s, ball (f' x) (r (f' x)) :=
    TopologicalSpace.isOpen_iUnion_countable _ fun x => isOpen_ball

Premises used: TopologicalSpace.isOpen_iUnion_countable, Set.Elem, Metric.isOpen_ball, Set
-- 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 : 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
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
⊢ ∃ (u : ℕ → ℝ), StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 0)

Tactic:
exists_seq_strictAnti_tendsto (0 : ℝ)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- 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 : 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
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
inr :
  ∀ (u : ℕ → ℝ),
    StrictAnti u →
      ∀ (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)),
        ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
          (∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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),
    (∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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:
obtain ⟨u, _, u_pos, u_lim⟩ :
    ∃ u : ℕ → ℝ, StrictAnti u ∧ (∀ n : ℕ, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- 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 : 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
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ 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) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
x : E
xs : x ∈ s
rw : Membership.mem (γ := Set (E →L[ℝ] F)) (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ)) (f' x)
⊢ Membership.mem (γ := Set (E →L[ℝ] F)) (⋃ z ∈ T, ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)) (f' x)

Tactic:
rw [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 : 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
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ 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) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
x : E
xs : x ∈ s
⊢ Membership.mem (γ := Set (E →L[ℝ] F)) (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ)) (f' x)

Tactic:
mem_iUnion.2 ⟨⟨x, xs⟩, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion, Subtype.mk, Exists.intro
-- 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 : 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
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ 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) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
x : E
xs : x ∈ s
refine :
  f' x ∈
    ball (f' (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ s) x xs) : E))
      (↑(r (f' (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ s) x xs) : E))) : ℝ)
⊢ Membership.mem (γ := Set (E →L[ℝ] F)) (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ)) (f' x)

Tactic:
refine mem_iUnion.2 ⟨⟨x, xs⟩, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro
-- 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 : 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
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ 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) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
x : E
xs : x ∈ s
⊢ f' x ∈
    ball (f' (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ s) x xs) : E))
      (↑(r (f' (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ s) x xs) : E))) : ℝ)

Tactic:
simpa only [mem_ball, Subtype.coe_mk, dist_self] using (rpos (f' x)).bot_lt

Premises used: Subtype.coe_mk, Metric.mem_ball, dist_self, Ne.bot_lt
-- 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 : 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
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ 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) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
x : E
xs : x ∈ s
⊢ Membership.mem (γ := Set (E →L[ℝ] F)) (⋃ z ∈ T, ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)) (f' x)

Tactic:
have : f' x ∈ ⋃ z ∈ T, ball (f' (z : E)) (r (f' z)) := by
        rw [hT]
        refine mem_iUnion.2 ⟨⟨x, xs⟩, ?_⟩
        simpa only [mem_ball, Subtype.coe_mk, dist_self] using (rpos (f' x)).bot_lt
-- 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 : 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
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ 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) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
x : E
xs : x ∈ s
this : Membership.mem (γ := Set (E →L[ℝ] F)) (⋃ z ∈ T, ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)) (f' x)
rwa :
  ∀ (this : ∃ (i : (↑s : Type u_1)) (_ : i ∈ T), f' x ∈ ball (f' (↑i : E)) (↑(r (f' (↑i : E))) : ℝ)),
    ∃ z ∈ T, f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : ∃ x_1 ∈ T, f' x ∈ ball (f' (↑x_1 : E)) (↑(r (f' (↑x_1 : E))) : ℝ)),
    ∃ z ∈ T, f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
⊢ ∃ z ∈ T, f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)

Tactic:
rwa [mem_iUnion₂, bex_def] at this

Premises used: bex_def, Set.mem_iUnion₂
-- 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 : 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
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ 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) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
x : E
xs : x ∈ s
obtain :
  ∀ (z : (↑s : Type u_1)) (zT : z ∈ T) (hz : f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)),
    ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
⊢ ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z

Tactic:
obtain ⟨z, zT, hz⟩ : ∃ z ∈ T, f' x ∈ ball (f' (z : E)) (r (f' z)) := by
      have : f' x ∈ ⋃ z ∈ T, ball (f' (z : E)) (r (f' z)) := by
        rw [hT]
        refine mem_iUnion.2 ⟨⟨x, xs⟩, ?_⟩
        simpa only [mem_ball, Subtype.coe_mk, dist_self] using (rpos (f' x)).bot_lt
      rwa [mem_iUnion₂, bex_def] at this
-- 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 : 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
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ 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) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
x : E
xs : x ∈ s
z : (↑s : Type u_1)
zT : z ∈ T
hz : f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
⊢ ‖f' x - f' (↑z : E)‖ + ((↑(r (f' (↑z : E))) : ℝ) - ‖f' x - f' (↑z : E)‖) = (↑(r (f' (↑z : E))) : ℝ)

Tactic:
abel
-- 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 : 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
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ 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) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
x : E
xs : x ∈ s
z : (↑s : Type u_1)
zT : z ∈ T
hz : f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
refine : 0 < (↑(r (f' (↑z : E))) : ℝ) - ‖f' x - f' (↑z : E)‖
⊢ ∃ (ε : ℝ), 0 < ε ∧ ‖f' x - f' (↑z : E)‖ + ε ≤ (↑(r (f' (↑z : E))) : ℝ)

Tactic:
refine ⟨r (f' z) - ‖f' x - f' z‖, ?_, le_of_eq (by abel)⟩