awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
⊢ ∀ᶠ (a : ℕ) in atTop, (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) (⨍⁻ (x : α), f a x ∂μ) 1
have refine_1 : ∀ (n : ℕ), (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) (⨍⁻ (x : α), f n x ∂μ) 1
Tactic: refine Eventually.of_forall fun n ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
n : ℕ
⊢ (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) (⨍⁻ (x : α), f n x ∂μ) 1
have refine_1 : ∀ [IsFiniteMeasure.{u_2} (α := α) (m0 := inst) 0] (hr : ∀ (n : ℕ), r ≤ ((0 : Measure α) : (a : Set α) → ℝ≥0∞) (s n)),
  let M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup (m0 := inst) f 0 < (↑‖f x‖₊ : ℝ≥0∞)};
  let N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1);
  ∀ (hN₀ : Eq (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞))
    (hN₁ :
      ∀ (u : Finset ℕ),
        ((⋂ n ∈ u, s n) \ N).Nonempty →
          LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞))
    (hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂0) (hμ : Ne.{u_2 + 1} (α := Measure α) 0 0)
    (this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂0 ≤ ((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ)
    (hxN : x ∉ N) (hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂0 ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop),
    ⨍⁻ (x : α), f n x ∂0 ≤ 1
Tactic: obtain rfl | _ := eq_zero_or_neZero μ
Cleared hypotheses: μ, inst_1, hr, M, N, hN₀, hN₁, hrf, hμ, this, hxN, hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
n : ℕ
refine_1 :
  ∀ [IsFiniteMeasure.{u_2} (α := α) (m0 := inst) 0] (hr : ∀ (n : ℕ), r ≤ ((0 : Measure α) : (a : Set α) → ℝ≥0∞) (s n)),
    let M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup (m0 := inst) f 0 < (↑‖f x‖₊ : ℝ≥0∞)};
    let N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1);
    ∀ (hN₀ : Eq (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞))
      (hN₁ :
        ∀ (u : Finset ℕ),
          ((⋂ n ∈ u, s n) \ N).Nonempty →
            LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞))
      (hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂0) (hμ : Ne.{u_2 + 1} (α := Measure α) 0 0)
      (this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂0 ≤ ((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ)
      (hxN : x ∉ N) (hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂0 ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop),
      ⨍⁻ (x : α), f n x ∂0 ≤ 1
⊢ (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) (⨍⁻ (x : α), f n x ∂μ) 1
have refine_1₁ : NeZero μ → ⨍⁻ (x : α), f n x ∂μ ≤ 1
Tactic: obtain rfl | _ := eq_zero_or_neZero μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
n : ℕ
h : NeZero μ
⊢ ⨍⁻ (x : α), f n x ∂μ ≤ 1
have refine_1 : ⨍⁻ (x : α), f n x ∂μ ≤ ⨍⁻ (_x : α), 1 ∂μ
Tactic: rw [← laverage_const μ 1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
b : ℝ≥0∞
hb : ∀ᶠ (n : ℕ) in atTop, ⨍⁻ (x : α), f n x ∂μ ≤ b
⊢ HDiv.hDiv (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ b
have refine_2 : ∀ (n : ℕ) (hn : ⨍⁻ (x : α), f n x ∂μ ≤ b), HDiv.hDiv (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ b
Tactic: obtain ⟨n, hn⟩ := hb.exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (hypothesis)
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun (x : ℕ) ↦ f x a) atTop ∂μ ≤ limsup (fun (x_1 : ℕ) ↦ f x_1 x) atTop
b : ℝ≥0∞
hb : ∀ᶠ (n : ℕ) in atTop, ⨍⁻ (x : α), f n x ∂μ ≤ b
n : ℕ
hn : ⨍⁻ (x : α), f n x ∂μ ≤ b
⊢ HDiv.hDiv (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ b
have hn₁ : HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f n x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ b
Tactic: rw [laverage_eq] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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 ι),
    t.Infinite ∧
      ∀ ⦃u : Set ι⦄, u ⊆ t → u.Finite → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ i ∈ u, s i) : ℝ≥0∞)
have obtain : ∀ (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∞)),
  ∃ (t : Set ι),
    t.Infinite ∧
      ∀ ⦃u : Set ι⦄, u ⊆ t → u.Finite → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ i ∈ u, s i) : ℝ≥0∞)
Tactic: obtain ⟨t, ht, h⟩ := bergelson' (fun n ↦ hs <| Infinite.natEmbedding _ n) hr₀ (fun n ↦ hr _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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∞)
⊢ ∃ (t : Set ι),
    t.Infinite ∧
      ∀ ⦃u : Set ι⦄, u ⊆ t → u.Finite → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ i ∈ u, s i) : ℝ≥0∞)
have refine : ∀ (u : Set ι) (hut : u ⊆ (⇑(Infinite.natEmbedding ι) : (a : ℕ) → ι) '' t) (hu : u.Finite) (i : ι) (hi : i ∈ u),
  ⋂ (n : ℕ),
      ⋂ (_ : Membership.mem (γ := Set ℕ) ((⇑(Infinite.natEmbedding ι) : (a : ℕ) → ι) ⁻¹' u) n),
        s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n) ⊆
    s i
Tactic: refine ⟨_, ht.image <| (Infinite.natEmbedding _).injective.injOn, fun u hut hu ↦
    (h (preimage_subset_of_surjOn (Infinite.natEmbedding _).injective hut) <| hu.preimage
    (Embedding.injective _).injOn).trans_le <| measure_mono <| subset_iInter₂ fun i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Intersectivity (goal)
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
i : ι
hi : i ∈ u
⊢ ⋂ (n : ℕ),
      ⋂ (_ : Membership.mem (γ := Set ℕ) ((⇑(Infinite.natEmbedding ι) : (a : ℕ) → ι) ⁻¹' u) n),
        s ((Infinite.natEmbedding ι : (a : ℕ) → ι) n) ⊆
    s i
have obtain : ∀ (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: obtain ⟨n, -, rfl⟩ := hut hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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 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)
have 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)
Tactic: rcases eq_empty_or_nonempty s with (rfl | hs)
Cleared hypotheses: s, hf'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases eq_empty_or_nonempty s with (rfl | hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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)
have inl : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((fun (x : ℕ) ↦ (∅ : Set E)) n)
Tactic: refine ⟨fun _ => ∅, fun _ => 0, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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)
⊢ ∃ (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)
have inl₁ : Subset.{u_1} (α := Set E) ∅ (⋃ (n : ℕ), (fun (x : ℕ) ↦ (∅ : Set E)) n)
Tactic: refine ⟨fun _ => ∅, fun _ => 0, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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)
⊢ ∃ (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)
have inl₂ : ∀ (n : ℕ),
  ApproximatesLinearOn (𝕜 := ℝ) f ((fun (x : ℕ) ↦ (0 : E →L[ℝ] F)) n) (∅ ∩ (fun (x : ℕ) ↦ (∅ : Set E)) n)
    (r ((fun (x : ℕ) ↦ (0 : E →L[ℝ] F)) n))
Tactic: refine ⟨fun _ => ∅, fun _ => 0, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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))
⊢ ∃ (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)
have inl₃ : Set.Nonempty.{u_1} (α := E) ∅ →
  ∀ (n : ℕ), ∃ (y : E), Membership.mem (γ := Set E) ∅ y ∧ (fun (x : ℕ) ↦ (0 : E →L[ℝ] F)) n = f' y
Tactic: refine ⟨fun _ => ∅, fun _ => 0, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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 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)
have 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)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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))) : ℝ))
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨u, _, u_pos, u_lim⟩ :
    ∃ u : ℕ → ℝ, StrictAnti u ∧ (∀ n : ℕ, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)