awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∉ closure s
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)
⊢ 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:
simp only [mem_compl_iff, mem_setOf, h, not_false_eq_true, indicator_of_notMem,
      indicator_of_mem, Pi.one_apply]

Premises used: Pi.one_apply, Set.mem_setOf, Set.indicator_of_mem, Set.indicator_of_notMem, not_false_eq_true, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Order.UpperLower
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)

Tactic:
aux₁ fun _ ↦ hs.compl.exists_subset_ball <| frontier_subset_closure ?_

Premises used: IsUpperSet.compl, IsLowerSet.exists_subset_ball, _private.0.aux₁, frontier_subset_closure
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
pos : ∀ (x_1 : ℝ), x ∈ frontier 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)

Tactic:
refine aux₁ fun _ ↦ hs.compl.exists_subset_ball <| frontier_subset_closure ?_

Premises used: IsUpperSet.compl, IsLowerSet.exists_subset_ball, _private.0.aux₁, frontier_subset_closure
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
x_1 : ℝ
pos pos₁ pos₂ pos₃ : x ∈ frontier s
⊢ x ∈ frontier sᶜ

Tactic:
rwa [frontier_compl]

Premises used: frontier_compl
-- Module: Mathlib.MeasureTheory.Order.UpperLower
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) (𝓝 0)

Tactic:
aux₀ fun _ ↦ hs.exists_subset_ball <| frontier_subset_closure hx

Premises used: IsUpperSet.exists_subset_ball, frontier_subset_closure, _private.0.aux₀
-- Module: Mathlib.MeasureTheory.Order.UpperLower
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) (𝓝 0)

Tactic:
exact aux₀ fun _ ↦ hs.exists_subset_ball <| frontier_subset_closure hx

Premises used: IsUpperSet.exists_subset_ball, frontier_subset_closure, _private.0.aux₀
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
⊢ Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)

Tactic:
measure_mono_null (fun x hx ↦ ?_)
    (Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet _
      (isClosed_closure (s := s)).measurableSet)

Premises used: Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet, IsClosed.measurableSet, MeasureTheory.measure_mono_null, isClosed_closure
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
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
⊢ Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)

Tactic:
refine measure_mono_null (fun x hx ↦ ?_)
    (Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet _
      (isClosed_closure (s := s)).measurableSet)

Premises used: Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet, IsClosed.measurableSet, MeasureTheory.measure_mono_null, isClosed_closure
-- Module: Mathlib.MeasureTheory.Order.UpperLower
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
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
⊢ 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

Premises used: closure
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
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)
⊢ 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:
simp only [mem_compl_iff, mem_setOf, h, not_false_eq_true, indicator_of_notMem,
      indicator_of_mem, Pi.one_apply]

Premises used: Pi.one_apply, Set.mem_setOf, Set.indicator_of_mem, Set.indicator_of_notMem, not_false_eq_true, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∉ closure s
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)
⊢ 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:
simp only [mem_compl_iff, mem_setOf, h, not_false_eq_true, indicator_of_notMem,
      indicator_of_mem, Pi.one_apply]

Premises used: Pi.one_apply, Set.mem_setOf, Set.indicator_of_mem, Set.indicator_of_notMem, not_false_eq_true, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Order.UpperLower
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)

Tactic:
aux₁ fun _ ↦ hs.compl.exists_subset_ball <| frontier_subset_closure ?_

Premises used: IsLowerSet.compl, _private.0.aux₁, IsUpperSet.exists_subset_ball, frontier_subset_closure
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
pos : ∀ (x_1 : ℝ), x ∈ frontier 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)

Tactic:
refine aux₁ fun _ ↦ hs.compl.exists_subset_ball <| frontier_subset_closure ?_

Premises used: IsLowerSet.compl, _private.0.aux₁, IsUpperSet.exists_subset_ball, frontier_subset_closure
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
x_1 : ℝ
pos pos₁ pos₂ pos₃ : x ∈ frontier s
⊢ x ∈ frontier sᶜ

Tactic:
rwa [frontier_compl]

Premises used: frontier_compl
-- Module: Mathlib.MeasureTheory.Order.UpperLower
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) (𝓝 0)

Tactic:
aux₀ fun _ ↦ hs.exists_subset_ball <| frontier_subset_closure hx

Premises used: IsLowerSet.exists_subset_ball, frontier_subset_closure, _private.0.aux₀
-- Module: Mathlib.MeasureTheory.Order.UpperLower
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) (𝓝 0)

Tactic:
exact aux₀ fun _ ↦ hs.exists_subset_ball <| frontier_subset_closure hx

Premises used: IsLowerSet.exists_subset_ball, frontier_subset_closure, _private.0.aux₀
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : s.OrdConnected
rw :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((↑(upperClosure s) : Set (ι → ℝ)) ∩ (↑(lowerClosure s) : Set (ι → ℝ)))) :
      ENNReal)
    (0 : ENNReal)
⊢ Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)

Tactic:
rw [← hs.upperClosure_inter_lowerClosure]

Premises used: Set.OrdConnected.upperClosure_inter_lowerClosure
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : s.OrdConnected
⊢ Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((↑(upperClosure s) : Set (ι → ℝ)) ∩ (↑(lowerClosure s) : Set (ι → ℝ)))) :
      ENNReal)
    (0 : ENNReal)

Tactic:
measure_mono_null (frontier_inter_subset _ _) <| measure_union_null
    (measure_inter_null_of_null_left _ (UpperSet.upper _).null_frontier)
    (measure_inter_null_of_null_right _ (LowerSet.lower _).null_frontier)

Premises used: MeasureTheory.measure_union_null, MeasureTheory.measure_mono_null, MeasureTheory.measure_inter_null_of_null_right, IsUpperSet.null_frontier, MeasureTheory.measure_inter_null_of_null_left, UpperSet.upper, LowerSet.lower, IsLowerSet.null_frontier, frontier_inter_subset
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : s.OrdConnected
⊢ Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((↑(upperClosure s) : Set (ι → ℝ)) ∩ (↑(lowerClosure s) : Set (ι → ℝ)))) :
      ENNReal)
    (0 : ENNReal)

Tactic:
exact measure_mono_null (frontier_inter_subset _ _) <| measure_union_null
    (measure_inter_null_of_null_left _ (UpperSet.upper _).null_frontier)
    (measure_inter_null_of_null_right _ (LowerSet.lower _).null_frontier)

Premises used: MeasureTheory.measure_union_null, MeasureTheory.measure_mono_null, MeasureTheory.measure_inter_null_of_null_right, IsUpperSet.null_frontier, MeasureTheory.measure_inter_null_of_null_left, UpperSet.upper, LowerSet.lower, IsLowerSet.null_frontier, frontier_inter_subset
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : s.OrdConnected
⊢ NullMeasurableSet s (volume : Measure (ι → ℝ))

Tactic:
nullMeasurableSet_of_null_frontier hs.null_frontier

Premises used: Set.OrdConnected.null_frontier, nullMeasurableSet_of_null_frontier
-- Module: Mathlib.MeasureTheory.Order.UpperLower
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)

Tactic:
measure_mono_null ?_ hs.ordConnected.null_frontier

Premises used: IsAntichain.ordConnected, MeasureTheory.measure_mono_null, Set.OrdConnected.null_frontier
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
inst_1 : Nonempty ι
hs : IsAntichain (fun (x1 x2 : ι → ℝ) ↦ x1 ≤ x2) s
refine : s ⊆ frontier s
⊢ Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
refine measure_mono_null ?_ hs.ordConnected.null_frontier

Premises used: IsAntichain.ordConnected, MeasureTheory.measure_mono_null, Set.OrdConnected.null_frontier
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
inst_1 : Nonempty ι
hs : IsAntichain (fun (x1 x2 : ι → ℝ) ↦ x1 ≤ x2) s
rw : s ⊆ closure s
⊢ s ⊆ frontier s

Tactic:
rw [← closure_diff_interior, hs.interior_eq_empty, diff_empty]

Premises used: IsAntichain.interior_eq_empty, Set.diff_empty, closure_diff_interior
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
inst_1 : Nonempty ι
hs : IsAntichain (fun (x1 x2 : ι → ℝ) ↦ x1 ≤ x2) s
⊢ s ⊆ closure s

Tactic:
subset_closure

Premises used: subset_closure
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
inst_1 : Nonempty ι
hs : IsAntichain (fun (x1 x2 : ι → ℝ) ↦ x1 ≤ x2) s
⊢ s ⊆ closure s

Tactic:
exact subset_closure

Premises used: subset_closure
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
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 α
⊢ s ∈ ae μ ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
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
p : α → Prop
⊢ (∀ᵐ (a : α) ∂μ, p a) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬p a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
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 α
⊢ sᶜ ∈ ae μ ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [mem_ae_iff, compl_compl]

Premises used: compl_compl, MeasureTheory.mem_ae_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
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
p : α → Prop
⊢ (∃ᵐ (a : α) ∂μ, p a) ↔ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | p a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
not_congr compl_mem_ae_iff

Premises used: Filter.Frequently, not_congr, MeasureTheory.compl_mem_ae_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
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 α
⊢ (∃ᵐ (a : α) ∂μ, a ∈ s) ↔ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
not_congr compl_mem_ae_iff

Premises used: Filter.Frequently, not_congr, MeasureTheory.compl_mem_ae_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
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∞) ↔ ∀ᵐ (a : α) ∂μ, a ∉ s

Tactic:
compl_mem_ae_iff.symm

Premises used: Set.Mem, Filter.Eventually, setOf, Iff.symm, MeasureTheory.compl_mem_ae_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
p : α → Prop
μ : F
⊢ (∀ (a : α), p a) → ∀ᵐ (a : α) ∂μ, p a

Tactic:
Eventually.of_forall

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
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
inst_2 : Countable ι
p : α → ι → Prop
⊢ (∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i) ↔ ∀ (i : ι), ∀ᵐ (a : α) ∂μ, p a i

Tactic:
eventually_countable_forall

Premises used: eventually_countable_forall
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
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 : α
ha : ∀ (i : ι), p a i
⊢ p a i

Tactic:
ha i
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
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
h₁ h₂ : ∀ (a : α) (ha : ∀ (i : ι), p a i), p a i
⊢ ∀ᵐ (a : α) ∂μ, p a i

Tactic:
filter_upwards [hp] with a ha using ha i
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
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
rw₁ : Set.Countable.{u_1} (α := α) {a : α | ¬p a}
⊢ (∀ᵐ (x : α) ∂μ, p x) ↔ ∀ (x : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞) → p x

Tactic:
rw [ae_iff, measure_null_iff_singleton]

Premises used: MeasureTheory.ae_iff, MeasureTheory.measure_null_iff_singleton
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
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 : α),
      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:
forall_congr' fun _ ↦ not_imp_comm

Premises used: not_imp_comm, forall_congr'
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
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
⊢ Set.Countable.{u_1} (α := α) {a : α | ¬p a}

Tactic:
Set.to_countable _

Premises used: Set.to_countable
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
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 : α),
      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:
exacts [forall_congr' fun _ ↦ not_imp_comm, Set.to_countable _]

Premises used: not_imp_comm, Set.to_countable, forall_congr'
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
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
ι : Type u_4
S : Set ι
hS : S.Countable
p : α → (i : ι) → i ∈ S → Prop
⊢ (∀ᵐ (x : α) ∂μ, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᵐ (x : α) ∂μ, p x i hi

Tactic:
eventually_countable_ball hS

Premises used: eventually_countable_ball
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
f : α → β
⊢ f =ᶠ[ae μ] f

Tactic:
EventuallyEq.rfl

Premises used: Filter.EventuallyEq.rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
f g : α → β
⊢ f =ᶠ[ae μ] g ↔ g =ᶠ[ae μ] f

Tactic:
eventuallyEq_comm

Premises used: Filter.eventuallyEq_comm