awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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‖}
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)))
⊢ ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)

Tactic:
have K_closed : ∀ (n) (z : T) (p), IsClosed (K n z p) := fun n z p =>
    isClosed_closure.inter isClosed_closedBall
-- 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‖}
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)
haveI : ∀ (this : Encodable (↑T : Type u_1)), ∃ (F : ℕ → ℕ × (↑T : Type u_1) × ℕ), Function.Surjective F
⊢ ∃ (F : ℕ → ℕ × (↑T : Type u_1) × ℕ), Function.Surjective F

Tactic:
haveI : Encodable T := T_count.toEncodable
-- 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‖}
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)
this : Encodable (↑T : Type u_1)
rcases : ∀ (x : E) (xs : x ∈ s), Nonempty.{u_1 + 1} (↑T : Type u_1)
⊢ Nonempty.{u_1 + 1} (↑T : Type u_1)

Tactic:
rcases hs with ⟨x, xs⟩
-- 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
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‖}
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)
this : Encodable (↑T : Type u_1)
x : E
xs : x ∈ s
rcases : ∀ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z → Nonempty.{u_1 + 1} (↑T : Type u_1)
⊢ Nonempty.{u_1 + 1} (↑T : Type u_1)

Tactic:
rcases s_subset x xs with ⟨n, z, _⟩
-- 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
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‖}
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)
this : Encodable (↑T : Type u_1)
x : E
xs : x ∈ s
n : ℕ
z : (↑T : Type u_1)
h : x ∈ M n z
⊢ Nonempty.{u_1 + 1} (↑T : Type u_1)

Tactic:
⟨z⟩

Premises used: Nonempty.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
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‖}
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)
this : Encodable (↑T : Type u_1)
x : E
xs : x ∈ s
n : ℕ
z : (↑T : Type u_1)
h : x ∈ M n z
⊢ Nonempty.{u_1 + 1} (↑T : Type u_1)

Tactic:
exact ⟨z⟩
-- 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‖}
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)
this : Encodable (↑T : Type u_1)
⊢ Nonempty.{u_1 + 1} (↑T : Type u_1)

Tactic:
have : Nonempty T := by
      rcases hs with ⟨x, xs⟩
      rcases s_subset x xs with ⟨n, z, _⟩
      exact ⟨z⟩
-- 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‖}
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)
this_1 : Encodable (↑T : Type u_1)
this : Nonempty.{u_1 + 1} (↑T : Type u_1)
inhabit : ∀ (inhabited_h : Inhabited (↑T : Type u_1)), ∃ (F : ℕ → ℕ × (↑T : Type u_1) × ℕ), Function.Surjective F
⊢ ∃ (F : ℕ → ℕ × (↑T : Type u_1) × ℕ), Function.Surjective F

Tactic:
inhabit ↥T
-- 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‖}
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)
this_1 : Encodable (↑T : Type u_1)
this : Nonempty.{u_1 + 1} (↑T : Type u_1)
inhabited_h : Inhabited (↑T : Type u_1)
⊢ ∃ (F : ℕ → ℕ × (↑T : Type u_1) × ℕ), Function.Surjective F

Tactic:
⟨_, Encodable.surjective_decode_getD (ℕ × T × ℕ) default⟩

Premises used: Inhabited.default, Set.Elem, Nat, Exists.intro, Prod, Encodable.surjective_decode_getD
-- 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‖}
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)
this_1 : Encodable (↑T : Type u_1)
this : Nonempty.{u_1 + 1} (↑T : Type u_1)
inhabited_h : Inhabited (↑T : Type u_1)
⊢ ∃ (F : ℕ → ℕ × (↑T : Type u_1) × ℕ), Function.Surjective F

Tactic:
exact ⟨_, Encodable.surjective_decode_getD (ℕ × T × ℕ) default⟩
-- 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‖}
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)
inr :
  ∀ (F_1 : ℕ → ℕ × (↑T : Type u_1) × ℕ) (hF : Function.Surjective F_1),
    ∃ (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 ⟨F, hF⟩ : ∃ F : ℕ → ℕ × T × ℕ, Function.Surjective F := by
    haveI : Encodable T := T_count.toEncodable
    have : Nonempty T := by
      rcases hs with ⟨x, xs⟩
      rcases s_subset x xs with ⟨n, z, _⟩
      exact ⟨z⟩
    inhabit ↥T
    exact ⟨_, Encodable.surjective_decode_getD (ℕ × T × ℕ) default⟩

Premises used: Function.Surjective
-- 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
⊢ ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F_1),
    (∀ (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:
⟨fun q => K (F q).1 (F q).2.1 (F q).2.2, fun q => f' (F q).2.1, fun n => K_closed _ _ _,
      fun x xs => ?_, fun q => K_approx _ _ _, fun _ q => ⟨(F q).2.1, (F q).2.1.1.2, rfl⟩⟩

Premises used: Prod.fst, And.intro, Exists.intro, Subtype.val, Prod.snd, rfl, Subtype.property