awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
apply : IsSeparable.{u_1} (α := F) (range fun (x : ℝ) ↦ derivWithin f (Ici x) x)
⊢ StronglyMeasurable.{0, u_1} (β := F) fun (x : ℝ) ↦ derivWithin f (Ici x) x

Tactic:
apply stronglyMeasurable_iff_measurable_separable.2 ⟨measurable_derivWithin_Ici f, ?_⟩

Premises used: Iff.mpr, stronglyMeasurable_iff_measurable_separable, And.intro, measurable_derivWithin_Ici
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
⊢ ∃ (t : Set ℝ), t.Countable ∧ Dense t

Tactic:
exists_countable_dense ℝ

Premises used: Real, TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
obtain :
  ∀ (t : Set ℝ) (t_count : t.Countable) (ht : Dense t),
    IsSeparable.{u_1} (α := F) (range fun (x : ℝ) ↦ derivWithin f (Ici x) x)
⊢ IsSeparable.{u_1} (α := F) (range fun (x : ℝ) ↦ derivWithin f (Ici x) x)

Tactic:
obtain ⟨t, t_count, ht⟩ : ∃ t : Set ℝ, t.Countable ∧ Dense t := exists_countable_dense ℝ

Premises used: Real, TopologicalSpace.exists_countable_dense, Set
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
suffices :
  (range fun (x : ℝ) ↦ derivWithin f (Ici x) x) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span ℝ (f '' t)) : Set F)
⊢ IsSeparable.{u_1} (α := F) (range fun (x : ℝ) ↦ derivWithin f (Ici x) x)

Tactic:
suffices H : range (fun x ↦ derivWithin f (Ici x) x) ⊆ closure (Submodule.span ℝ (f '' t)) from
    IsSeparable.mono (t_count.image f).isSeparable.span.closure H
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
suffices :
  (range fun (y : ℝ) ↦ derivWithin f (Ici x) y) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span ℝ (f '' t)) : Set F)
⊢ (fun (x : ℝ) ↦ derivWithin f (Ici x) x) x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span ℝ (f '' t)) : Set F)

Tactic:
suffices H' : range (fun y ↦ derivWithin f (Ici x) y) ⊆ closure (Submodule.span ℝ (f '' t)) from
    H' (mem_range_self _)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
h : Ici x ⊆ closure (Ici x ∩ t)
⊢ (range fun (y : ℝ) ↦ derivWithin f (Ici x) y) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span ℝ (f '' t)) : Set F)

Tactic:
apply range_derivWithin_subset_closure_span_image

Premises used: range_derivWithin_subset_closure_span_image
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
⊢ Ici x = closure (Ioi x ∩ closure t)

Tactic:
simp [dense_iff_closure_eq.1 ht]

Premises used: dense_iff_closure_eq, Iff.mp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
h : Ioi x ∩ closure t ⊆ closure (Ioi x ∩ t)
⊢ closure (Ioi x ∩ closure t) ⊆ closure (closure (Ioi x ∩ t))

Tactic:
apply closure_mono

Premises used: closure_mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
⊢ Ioi x ∩ closure t ⊆ closure (Ioi x ∩ t)

Tactic:
simpa [inter_comm] using (isOpen_Ioi (a := x)).closure_inter (s := t)

Premises used: IsOpen.closure_inter, Set.inter_comm, isOpen_Ioi
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
rw : closure (Ioi x ∩ t) ⊆ closure (Ici x ∩ t)
⊢ closure (closure (Ioi x ∩ t)) ⊆ closure (Ici x ∩ t)

Tactic:
rw [closure_closure]

Premises used: closure_closure
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
⊢ closure (Ioi x ∩ t) ⊆ closure (Ici x ∩ t)

Tactic:
closure_mono (inter_subset_inter_left _ Ioi_subset_Ici_self)

Premises used: Set.Ioi_subset_Ici_self, closure_mono, Set.inter_subset_inter_left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
⊢ closure (Ioi x ∩ t) ⊆ closure (Ici x ∩ t)

Tactic:
exact closure_mono (inter_subset_inter_left _ Ioi_subset_Ici_self)

Premises used: Set.Ioi_subset_Ici_self, closure_mono, Set.inter_subset_inter_left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
calc : Ici x = closure (Ioi x ∩ closure t)
calc₁ : closure (Ioi x ∩ closure t) ⊆ closure (closure (Ioi x ∩ t))
calc₂ : closure (closure (Ioi x ∩ t)) ⊆ closure (Ici x ∩ t)
⊢ Ici x ⊆ closure (Ici x ∩ t)

Tactic:
calc Ici x
    = closure (Ioi x ∩ closure t) := by simp [dense_iff_closure_eq.1 ht]
  _ ⊆ closure (closure (Ioi x ∩ t)) := by
      apply closure_mono
      simpa [inter_comm] using (isOpen_Ioi (a := x)).closure_inter (s := t)
  _ ⊆ closure (Ici x ∩ t) := by
      rw [closure_closure]
      exact closure_mono (inter_subset_inter_left _ Ioi_subset_Ici_self)

Premises used: Set.Ioi, Set.Ici, Inter.inter, closure
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
inst_3 : MeasurableSpace F
inst_4 : BorelSpace F
μ : Measure ℝ
⊢ AEMeasurable.{0, u_1} (β := F) (fun (x : ℝ) ↦ derivWithin f (Ici x) x) μ

Tactic:
(measurable_derivWithin_Ici f).aemeasurable

Premises used: Measurable.aemeasurable, measurable_derivWithin_Ici
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
μ : Measure ℝ
⊢ AEStronglyMeasurable.{0, u_1} (β := F) (fun (x : ℝ) ↦ derivWithin f (Ici x) x) μ

Tactic:
(stronglyMeasurable_derivWithin_Ici f).aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, stronglyMeasurable_derivWithin_Ici
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
⊢ MeasurableSet (α := ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ioi x) x}

Tactic:
simpa [differentiableWithinAt_Ioi_iff_Ici] using measurableSet_of_differentiableWithinAt_Ici f

Premises used: measurableSet_of_differentiableWithinAt_Ici, differentiableWithinAt_Ioi_iff_Ici
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
inst_3 : MeasurableSpace F
inst_4 : BorelSpace F
⊢ Measurable.{0, u_1} (β := F) fun (x : ℝ) ↦ derivWithin f (Ioi x) x

Tactic:
simpa [derivWithin_Ioi_eq_Ici] using measurable_derivWithin_Ici f

Premises used: derivWithin_Ioi_eq_Ici, measurable_derivWithin_Ici
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
⊢ StronglyMeasurable.{0, u_1} (β := F) fun (x : ℝ) ↦ derivWithin f (Ioi x) x

Tactic:
simpa [derivWithin_Ioi_eq_Ici] using stronglyMeasurable_derivWithin_Ici f

Premises used: stronglyMeasurable_derivWithin_Ici, derivWithin_Ioi_eq_Ici
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
inst_3 : MeasurableSpace F
inst_4 : BorelSpace F
μ : Measure ℝ
⊢ AEMeasurable.{0, u_1} (β := F) (fun (x : ℝ) ↦ derivWithin f (Ioi x) x) μ

Tactic:
(measurable_derivWithin_Ioi f).aemeasurable

Premises used: Measurable.aemeasurable, measurable_derivWithin_Ioi
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
μ : Measure ℝ
⊢ AEStronglyMeasurable.{0, u_1} (β := F) (fun (x : ℝ) ↦ derivWithin f (Ioi x) x) μ

Tactic:
(stronglyMeasurable_derivWithin_Ioi f).aestronglyMeasurable

Premises used: stronglyMeasurable_derivWithin_Ioi, MeasureTheory.StronglyMeasurable.aestronglyMeasurable
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
⊢ ProperSpace E

Tactic:
have : ProperSpace E := .of_locallyCompactSpace 𝕜
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
simp :
  IsOpen[instTopologicalSpaceProd]
    {p : α × E |
      ∃ (r' : ℝ),
        (r / 2 < r' ∧ r' ≤ r) ∧
          ∀ (y : E),
            dist y p.2 < r' →
              ∀ (z : E),
                dist z p.2 < r' →
                  ‖f p.1 z - f p.1 y -
                        HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                    s * r}
⊢ IsOpen[instTopologicalSpaceProd] {p : α × E | p.2 ∈ A (f p.1) L r s}

Tactic:
simp only [A, mem_Ioc, mem_ball, map_sub, mem_setOf_eq]

Premises used: map_sub, FDerivMeasurableAux.A, Set.mem_setOf_eq, Metric.mem_ball, Set.mem_Ioc
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
apply :
  ∀ (x : α × E),
    Membership.mem (γ := Set (α × E))
        {p : α × E |
          ∃ (r' : ℝ),
            (r / 2 < r' ∧ r' ≤ r) ∧
              ∀ (y : E),
                dist y p.2 < r' →
                  ∀ (z : E),
                    dist z p.2 < r' →
                      ‖f p.1 z - f p.1 y -
                            HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                        s * r}
        x →
      {p : α × E |
          ∃ (r' : ℝ),
            (r / 2 < r' ∧ r' ≤ r) ∧
              ∀ (y : E),
                dist y p.2 < r' →
                  ∀ (z : E),
                    dist z p.2 < r' →
                      ‖f p.1 z - f p.1 y -
                            HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                        s * r} ∈
        𝓝 x
⊢ IsOpen[instTopologicalSpaceProd]
    {p : α × E |
      ∃ (r' : ℝ),
        (r / 2 < r' ∧ r' ≤ r) ∧
          ∀ (y : E),
            dist y p.2 < r' →
              ∀ (z : E),
                dist z p.2 < r' →
                  ‖f p.1 z - f p.1 y -
                        HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                    s * r}

Tactic:
apply isOpen_iff_mem_nhds.2

Premises used: Iff.mpr, isOpen_iff_mem_nhds
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
rcases :
  ∀ (t : ℝ) (hrt : r / 2 < t) (htr' : t < r'),
    {p : α × E |
        ∃ (r' : ℝ),
          (r / 2 < r' ∧ r' ≤ r) ∧
            ∀ (y : E),
              dist y p.2 < r' →
                ∀ (z : E),
                  dist z p.2 < r' →
                    ‖f p.1 z - f p.1 y -
                          HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                      s * r} ∈
      𝓝 (a, x)
⊢ {p : α × E |
      ∃ (r' : ℝ),
        (r / 2 < r' ∧ r' ≤ r) ∧
          ∀ (y : E),
            dist y p.2 < r' →
              ∀ (z : E),
                dist z p.2 < r' →
                  ‖f p.1 z - f p.1 y -
                        HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                    s * r} ∈
    𝓝 (a, x)

Tactic:
rcases exists_between Irr' with ⟨t, hrt, htr'⟩

Premises used: exists_between
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
rcases :
  ∀ (t' : ℝ) (hrt' : r / 2 < t') (ht't : t' < t),
    {p : α × E |
        ∃ (r' : ℝ),
          (r / 2 < r' ∧ r' ≤ r) ∧
            ∀ (y : E),
              dist y p.2 < r' →
                ∀ (z : E),
                  dist z p.2 < r' →
                    ‖f p.1 z - f p.1 y -
                          HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                      s * r} ∈
      𝓝 (a, x)
⊢ {p : α × E |
      ∃ (r' : ℝ),
        (r / 2 < r' ∧ r' ≤ r) ∧
          ∀ (y : E),
            dist y p.2 < r' →
              ∀ (z : E),
                dist z p.2 < r' →
                  ‖f p.1 z - f p.1 y -
                        HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                    s * r} ∈
    𝓝 (a, x)

Tactic:
rcases exists_between hrt with ⟨t', hrt', ht't⟩

Premises used: exists_between
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : E × E) ↦
    ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : E × E) ↦
    ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖

Tactic:
have B : Continuous (fun (p : E × E) ↦ ‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖) := by fun_prop
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
B :
  Continuous[instTopologicalSpaceProd, _] fun (p : E × E) ↦
    ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖
simp : 0 ≤ t
⊢ (closedBall x t ×ˢ closedBall x t).Nonempty

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
B :
  Continuous[instTopologicalSpaceProd, _] fun (p : E × E) ↦
    ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖
linarith : t < 0 → 2 / 2 = 1
linarith₁ : t < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : t < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : t < 0 → 2 / 2 = 1
linarith₄ : t < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : t < 0 → GT.gt (α := ℝ) 2 0
linarith₆ : t < 0 → 2 / 2 = 1
linarith₇ : t < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : t < 0 → GT.gt (α := ℝ) 2 0
linarith₉ : t < 0 → r' - r + (t - r') + (1 * r - 2 * t') + 2 * (t' - t) + (t - 0) = 0
linarith₁₀ : t < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ t

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
B :
  Continuous[instTopologicalSpaceProd, _] fun (p : E × E) ↦
    ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖
⊢ (closedBall x t ×ˢ closedBall x t).Nonempty

Tactic:
have C : (closedBall x t ×ˢ closedBall x t).Nonempty := by simp; linarith