awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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)
have inr : ∀ (x : E) (xs : x ∈ s), Membership.mem (γ := Set E) (⋃ (n : ℕ), (fun (q : ℕ) ↦ K (F q).1 (F q).2.1 (F q).2.2) n) x
Tactic: refine
    ⟨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⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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
⊢ Membership.mem (γ := Set E) (⋃ (n : ℕ), (fun (q : ℕ) ↦ K (F q).1 (F q).2.1 (F q).2.2) n) x
have inr : ∀ (n : ℕ) (z : (↑T : Type u_1)) (hnz : x ∈ M n z),
  Membership.mem (γ := Set E) (⋃ (n : ℕ), (fun (q : ℕ) ↦ K (F q).1 (F q).2.1 (F q).2.2) n) x
Tactic: obtain ⟨n, z, hnz⟩ : ∃ (n : ℕ) (z : T), x ∈ M n z := s_subset x xs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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
⊢ (ball x (u n / 3)).Nonempty
have simp : 0 < u n / 3
Tactic: simp only [nonempty_ball]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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
⊢ 0 < u n / 3
have linarith : u n / 3 ≤ 0 → 3 / 3 = 1
Tactic: linarith [u_pos n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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
linarith : u n / 3 ≤ 0 → 3 / 3 = 1
⊢ 0 < u n / 3
have linarith₁ : u n / 3 ≤ 0 → HMul.hMul (α := ℝ) 1 3 = 3
Tactic: linarith [u_pos n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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
linarith : u n / 3 ≤ 0 → 3 / 3 = 1
linarith₁ : u n / 3 ≤ 0 → HMul.hMul (α := ℝ) 1 3 = 3
⊢ 0 < u n / 3
have linarith₂ : u n / 3 ≤ 0 → GT.gt (α := ℝ) 3 0
Tactic: linarith [u_pos n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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
linarith : u n / 3 ≤ 0 → 3 / 3 = 1
linarith₁ : u n / 3 ≤ 0 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : u n / 3 ≤ 0 → GT.gt (α := ℝ) 3 0
⊢ 0 < u n / 3
have linarith₃ : u n / 3 ≤ 0 → 1 * u n - HMul.hMul (α := ℝ) 3 0 + (0 - u n) = 0
Tactic: linarith [u_pos n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
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 : ℕ), x ∈ closedBall (d p) (u n / 3)
have this : (ball x (u n / 3)).Nonempty
Tactic: have : Set.Nonempty (ball x (u n / 3)) := by simp only [nonempty_ball]; linarith [u_pos n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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
this : (ball x (u n / 3)).Nonempty
⊢ ∃ (p : ℕ), x ∈ closedBall (d p) (u n / 3)
have obtain : ∀ (p : ℕ) (hp : d p ∈ ball x (u n / 3)), ∃ (p : ℕ), x ∈ closedBall (d p) (u n / 3)
Tactic: obtain ⟨p, hp⟩ : ∃ p : ℕ, d p ∈ ball x (u n / 3) := hd.exists_mem_open isOpen_ball this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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
⊢ Membership.mem (γ := Set E) (⋃ (n : ℕ), (fun (q : ℕ) ↦ K (F q).1 (F q).2.1 (F q).2.2) n) x
have inr : ∀ (p : ℕ) (hp : x ∈ closedBall (d p) (u n / 3)),
  Membership.mem (γ := Set E) (⋃ (n : ℕ), (fun (q : ℕ) ↦ K (F q).1 (F q).2.1 (F q).2.2) n) x
Tactic: obtain ⟨p, hp⟩ : ∃ p : ℕ, x ∈ closedBall (d p) (u n / 3) := by
    have : Set.Nonempty (ball x (u n / 3)) := by simp only [nonempty_ball]; linarith [u_pos n]
    obtain ⟨p, hp⟩ : ∃ p : ℕ, d p ∈ ball x (u n / 3) := hd.exists_mem_open isOpen_ball this
    exact ⟨p, (mem_ball'.1 hp).le⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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)
⊢ Membership.mem (γ := Set E) (⋃ (n : ℕ), (fun (q : ℕ) ↦ K (F q).1 (F q).2.1 (F q).2.2) n) x
have 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
Tactic: obtain ⟨q, hq⟩ : ∃ q, F q = (n, z, p) := hF _