awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Order.UpperLower (goal)
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
⊢ Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
        (fun (x : ι → ℝ) ↦
            Tendsto (β := ENNReal)
              (fun (r : ℝ) ↦
                HDiv.hDiv (α := ENNReal) (β := ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
              (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
    x
have pos : ∀ (h : x ∈ closure s),
  Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
        (fun (x : ι → ℝ) ↦
            Tendsto (β := ENNReal)
              (fun (r : ℝ) ↦
                HDiv.hDiv (α := ENNReal) (β := ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
              (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
    x
Tactic: by_cases h : x ∈ closure s
-- Lean 4 proof step from Mathlib.MeasureTheory.Order.UpperLower (goal)
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
pos :
  ∀ (h : x ∈ closure s),
    Membership.mem (γ := Set (ι → ℝ))
      {x : ι → ℝ |
          (fun (x : ι → ℝ) ↦
              Tendsto (β := ENNReal)
                (fun (r : ℝ) ↦
                  HDiv.hDiv (α := ENNReal) (β := ENNReal)
                    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
                (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
            x}ᶜ
      x
⊢ Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
        (fun (x : ι → ℝ) ↦
            Tendsto (β := ENNReal)
              (fun (r : ℝ) ↦
                HDiv.hDiv (α := ENNReal) (β := ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
              (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
    x
have neg : ∀ (h : x ∉ closure s),
  Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
        (fun (x : ι → ℝ) ↦
            Tendsto (β := ENNReal)
              (fun (r : ℝ) ↦
                HDiv.hDiv (α := ENNReal) (β := ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
              (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
    x
Tactic: by_cases h : x ∈ closure s
-- Lean 4 proof step from Mathlib.MeasureTheory.Order.UpperLower (goal)
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
⊢ Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
        (fun (x : ι → ℝ) ↦
            Tendsto (β := ENNReal)
              (fun (r : ℝ) ↦
                HDiv.hDiv (α := ENNReal) (β := ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
              (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
    x
have pos : ¬Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
Tactic: simp only [mem_compl_iff, mem_setOf, h, not_false_eq_true, indicator_of_notMem,
      indicator_of_mem, Pi.one_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Order.UpperLower (goal)
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∉ closure s
⊢ Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
        (fun (x : ι → ℝ) ↦
            Tendsto (β := ENNReal)
              (fun (r : ℝ) ↦
                HDiv.hDiv (α := ENNReal) (β := ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
              (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
    x
have neg : ¬Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 0)
Tactic: simp only [mem_compl_iff, mem_setOf, h, not_false_eq_true, indicator_of_notMem,
      indicator_of_mem, Pi.one_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Order.UpperLower (goal)
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
⊢ ¬Tendsto (β := ENNReal)
      (fun (r : ℝ) ↦
        HDiv.hDiv (α := ENNReal) (β := ENNReal)
          (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
          (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
      (𝓝[>] 0) (𝓝 1)
have pos : ∀ (x_1 : ℝ), x ∈ frontier sᶜ
Tactic: refine aux₁ fun _ ↦ hs.compl.exists_subset_ball <| frontier_subset_closure ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Order.UpperLower (goal)
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
⊢ Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
have refine : ∀ (x : ι → ℝ) (hx : x ∈ frontier s),
  Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
        (fun (x : ι → ℝ) ↦
            Tendsto (β := ENNReal)
              (fun (r : ℝ) ↦
                HDiv.hDiv (α := ENNReal) (β := ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
              (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
    x
Tactic: refine measure_mono_null (fun x hx ↦ ?_)
    (Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet _
      (isClosed_closure (s := s)).measurableSet)
-- Lean 4 proof step from Mathlib.MeasureTheory.Order.UpperLower (goal)
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
⊢ Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
        (fun (x : ι → ℝ) ↦
            Tendsto (β := ENNReal)
              (fun (r : ℝ) ↦
                HDiv.hDiv (α := ENNReal) (β := ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
              (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
    x
have pos : ∀ (h : x ∈ closure s),
  Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
        (fun (x : ι → ℝ) ↦
            Tendsto (β := ENNReal)
              (fun (r : ℝ) ↦
                HDiv.hDiv (α := ENNReal) (β := ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
              (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
    x
Tactic: by_cases h : x ∈ closure s
-- Lean 4 proof step from Mathlib.MeasureTheory.Order.UpperLower (goal)
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
pos :
  ∀ (h : x ∈ closure s),
    Membership.mem (γ := Set (ι → ℝ))
      {x : ι → ℝ |
          (fun (x : ι → ℝ) ↦
              Tendsto (β := ENNReal)
                (fun (r : ℝ) ↦
                  HDiv.hDiv (α := ENNReal) (β := ENNReal)
                    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
                (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
            x}ᶜ
      x
⊢ Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
        (fun (x : ι → ℝ) ↦
            Tendsto (β := ENNReal)
              (fun (r : ℝ) ↦
                HDiv.hDiv (α := ENNReal) (β := ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
              (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
    x
have neg : ∀ (h : x ∉ closure s),
  Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
        (fun (x : ι → ℝ) ↦
            Tendsto (β := ENNReal)
              (fun (r : ℝ) ↦
                HDiv.hDiv (α := ENNReal) (β := ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
              (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
    x
Tactic: by_cases h : x ∈ closure s
-- Lean 4 proof step from Mathlib.MeasureTheory.Order.UpperLower (goal)
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
⊢ Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
        (fun (x : ι → ℝ) ↦
            Tendsto (β := ENNReal)
              (fun (r : ℝ) ↦
                HDiv.hDiv (α := ENNReal) (β := ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
              (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
    x
have pos : ¬Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
Tactic: simp only [mem_compl_iff, mem_setOf, h, not_false_eq_true, indicator_of_notMem,
      indicator_of_mem, Pi.one_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Order.UpperLower (goal)
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∉ closure s
⊢ Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
        (fun (x : ι → ℝ) ↦
            Tendsto (β := ENNReal)
              (fun (r : ℝ) ↦
                HDiv.hDiv (α := ENNReal) (β := ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
              (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
    x
have neg : ¬Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 0)
Tactic: simp only [mem_compl_iff, mem_setOf, h, not_false_eq_true, indicator_of_notMem,
      indicator_of_mem, Pi.one_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Order.UpperLower (goal)
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
⊢ ¬Tendsto (β := ENNReal)
      (fun (r : ℝ) ↦
        HDiv.hDiv (α := ENNReal) (β := ENNReal)
          (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
          (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
      (𝓝[>] 0) (𝓝 1)
have pos : ∀ (x_1 : ℝ), x ∈ frontier sᶜ
Tactic: refine aux₁ fun _ ↦ hs.compl.exists_subset_ball <| frontier_subset_closure ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Order.UpperLower (goal)
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : s.OrdConnected
⊢ Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
have rw : Eq (α := ENNReal)
  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (frontier ((↑(upperClosure s) : Set (ι → ℝ)) ∩ (↑(lowerClosure s) : Set (ι → ℝ)))) :
    ENNReal)
  (0 : ENNReal)
Tactic: rw [← hs.upperClosure_inter_lowerClosure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Order.UpperLower (goal)
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
inst_1 : Nonempty ι
hs : IsAntichain (fun (x1 x2 : ι → ℝ) ↦ x1 ≤ x2) s
⊢ Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) (0 : ENNReal)
have refine : s ⊆ frontier s
Tactic: refine measure_mono_null ?_ hs.ordConnected.null_frontier
-- Lean 4 proof step from Mathlib.MeasureTheory.Order.UpperLower (goal)
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
inst_1 : Nonempty ι
hs : IsAntichain (fun (x1 x2 : ι → ℝ) ↦ x1 ≤ x2) s
⊢ s ⊆ frontier s
have rw : s ⊆ closure s
Tactic: rw [← closure_diff_interior, hs.interior_eq_empty, diff_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
ι : Sort u_4
p : α → ι → Prop
hp : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i
i : ι
⊢ ∀ᵐ (a : α) ∂μ, p a i
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ι), p a i) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ p a i) x} x}
    a
Tactic: filter_upwards [hp] with a ha using ha i
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
ι : Sort u_4
p : α → ι → Prop
hp : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i
i : ι
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ι), p a i) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ p a i) x} x}
      a
⊢ ∀ᵐ (a : α) ∂μ, p a i
have h₁ : ∀ (a : α), (∀ (i : ι), p a i) → p a i
Tactic: filter_upwards [hp] with a ha using ha i
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
inst_2 : Countable α
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ, p x) ↔ ∀ (x : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞) → p x
have rw : (∀ (x : α),
    Membership.mem (γ := Set α) {a : α | ¬p a} x → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
  ∀ (x : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞) → p x
Tactic: rw [ae_iff, measure_null_iff_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
inst_2 : Countable α
p : α → Prop
rw :
  (∀ (x : α),
      Membership.mem (γ := Set α) {a : α | ¬p a} x → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ∀ (x : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞) → p x
⊢ (∀ᵐ (x : α) ∂μ, p x) ↔ ∀ (x : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞) → p x
have rw₁ : Set.Countable.{u_1} (α := α) {a : α | ¬p a}
Tactic: rw [ae_iff, measure_null_iff_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
⊢ ae μ = ⊤ ↔ ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
have simp : (∀ (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ s = univ) ↔
  ∀ (a : α), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [Filter.ext_iff, mem_ae_iff, mem_top, ne_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
⊢ (∀ (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ s = univ) ↔
    ∀ (a : α), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_1 : ∀ (h : ∀ (a : α), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)) (s : Set α)
  (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)), s = univ
Tactic: refine ⟨fun h a ha ↦ by simpa [ha] using (h {a}ᶜ).1, fun h s ↦ ⟨fun hs ↦ ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
refine_1 :
  ∀ (h : ∀ (a : α), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)) (s : Set α)
    (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)), s = univ
⊢ (∀ (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ s = univ) ↔
    ∀ (a : α), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_2 : ∀ (h : ∀ (a : α), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)) (s : Set α),
  s = univ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨fun h a ha ↦ by simpa [ha] using (h {a}ᶜ).1, fun h s ↦ ⟨fun hs ↦ ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s = univ
have refine_1 : ¬sᶜ.Nonempty
Tactic: rw [← compl_empty_iff, ← not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → x ∈ t) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (0 : ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | a ∈ s ∧ a ∉ t} : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp [ae_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
⊢ sᶜ =ᶠ[ae μ] t ↔ s =ᶠ[ae μ] tᶜ
have rw : sᶜᶜ =ᶠ[ae μ] tᶜ ↔ s =ᶠ[ae μ] tᶜ
Tactic: rw [← ae_eq_set_compl_compl, compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
rw : sᶜᶜ =ᶠ[ae μ] tᶜ ↔ s =ᶠ[ae μ] tᶜ
⊢ sᶜ =ᶠ[ae μ] t ↔ s =ᶠ[ae μ] tᶜ
have rw₁ : s =ᶠ[ae μ] tᶜ ↔ s =ᶠ[ae μ] tᶜ
Tactic: rw [← ae_eq_set_compl_compl, compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] univ
⊢ univ ∪ t =ᶠ[ae μ] univ
have rw : univ =ᶠ[ae μ] univ
Tactic: rw [univ_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
⊢ s ∪ t =ᶠ[ae μ] univ
have h₁ : univ = s ∪ univ
Tactic: convert! ae_eq_set_union (ae_eq_refl s) h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
⊢ univ = s ∪ univ
have h₁ : Eq.{u_1 + 1} (α := α → Prop) univ univ
Tactic: rw [union_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
⊢ s ∪ t =ᶠ[ae μ] t
have h₁ : t = ∅ ∪ t
Tactic: convert! ae_eq_set_union h (ae_eq_refl t)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
⊢ t = ∅ ∪ t
have h₁ : t = t
Tactic: rw [empty_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] ∅
⊢ s ∪ t =ᶠ[ae μ] s
have h₁ : s = s ∪ ∅
Tactic: convert! ae_eq_set_union (ae_eq_refl s) h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] ∅
⊢ s = s ∪ ∅
have h₁ : s = s
Tactic: rw [union_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] univ
⊢ s ∩ t =ᶠ[ae μ] t
have h₁ : t = univ ∩ t
Tactic: convert! ae_eq_set_inter h (ae_eq_refl t)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] univ
⊢ t = univ ∩ t
have h₁ : t = t
Tactic: rw [univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
⊢ s ∩ t =ᶠ[ae μ] s
have h₁ : s = s ∩ univ
Tactic: convert! ae_eq_set_inter (ae_eq_refl s) h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
⊢ s = s ∩ univ
have h₁ : s = s
Tactic: rw [inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
⊢ s ∩ t =ᶠ[ae μ] ∅
have h₁ : ∅ = ∅ ∩ t
Tactic: convert! ae_eq_set_inter h (ae_eq_refl t)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
⊢ ∅ = ∅ ∩ t
have h₁ : Eq.{u_1 + 1} (α := α → Prop) ∅ ∅
Tactic: rw [empty_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (goal)
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] ∅
⊢ s ∩ t =ᶠ[ae μ] ∅
have h₁ : ∅ = s ∩ ∅
Tactic: convert! ae_eq_set_inter (ae_eq_refl s) h