awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m : OuterMeasure α
ι : Type u_3
f : ι → OuterMeasure α
s : ℕ → Set α
h : Pairwise (Disjoint on s)
rw :
  LE.le (α := ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i))
    (∑' (b : ι) (a : ℕ), (f b : (a : Set α) → ℝ≥0∞) (s a))
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i))
    (∑' (i : ℕ) (i_1 : ι), (f i_1 : (a : Set α) → ℝ≥0∞) (s i))

Tactic:
rw [ENNReal.tsum_comm]

Premises used: ENNReal.tsum_comm
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m : OuterMeasure α
ι : Type u_3
f : ι → OuterMeasure α
s : ℕ → Set α
h : Pairwise (Disjoint on s)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i))
    (∑' (b : ι) (a : ℕ), (f b : (a : Set α) → ℝ≥0∞) (s a))

Tactic:
ENNReal.tsum_le_tsum fun i => measure_iUnion_le _

Premises used: ENNReal.tsum_le_tsum, MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m : OuterMeasure α
ι : Type u_3
f : ι → OuterMeasure α
s : ℕ → Set α
h : Pairwise (Disjoint on s)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i))
    (∑' (b : ι) (a : ℕ), (f b : (a : Set α) → ℝ≥0∞) (s a))

Tactic:
exact ENNReal.tsum_le_tsum fun i => measure_iUnion_le _

Premises used: ENNReal.tsum_le_tsum, MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
ι : Type u_3
f : ι → OuterMeasure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl

Premises used: tsum, rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
a : ℝ≥0∞
b : α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((a • dirac b : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator (fun (x : α) ↦ a) b : ℝ≥0∞)

Tactic:
simp only [smul_apply, smul_eq_mul, dirac_apply, ← indicator_mul_right _ fun _ => a, mul_one]

Premises used: MeasureTheory.OuterMeasure.dirac_apply, smul_eq_mul, mul_one, Set.indicator_mul_right, MeasureTheory.OuterMeasure.smul_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β_1 : Type u_2
m_1 : OuterMeasure α
β : Type u_3
f : α → β
m : OuterMeasure β
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) (f '' ∅) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β_1 : Type u_2
m_1 : OuterMeasure α
β : Type u_3
f : α → β
m : OuterMeasure β
x x_1 : Set α
h : x ⊆ x_1
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) (f '' x) : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) (f '' x_1) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β_1 : Type u_2
m_1 : OuterMeasure α
β : Type u_3
f : α → β
m : OuterMeasure β
s : ℕ → Set α
h : Pairwise (Disjoint on s)
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) (f '' ⋃ (i : ℕ), s i) : ℝ≥0∞)
    (∑' (i : ℕ), (m : (a : Set β) → ℝ≥0∞) (f '' s i) : ℝ≥0∞)

Tactic:
simpa only [image_iUnion] using measure_iUnion_le _

Premises used: Set.image_iUnion, MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_3
f : α → β
m : OuterMeasure β
s : Set α
⊢ Eq (α := ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) m : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((m : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_3
f : α → β
⊢ Monotone.{u_3, u_1} (α := OuterMeasure β) (β := OuterMeasure α) (⇑(comap f) : (a : OuterMeasure β) → OuterMeasure α)

Tactic:
fun _ _ h _ => h _

Premises used: Monotone, Set.image
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_3
ι : Sort u_4
f : α → β
m : ι → OuterMeasure β
s : Set α
⊢ Eq (α := ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) (⨆ (i : ι), m i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)
    (((⨆ (i : ι), (comap f : (a : OuterMeasure β) → OuterMeasure α) (m i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)

Tactic:
simp only [comap_apply, iSup_apply]

Premises used: MeasureTheory.OuterMeasure.comap_apply, MeasureTheory.OuterMeasure.iSup_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
s t : Set α
m : OuterMeasure α
⊢ Eq (α := ℝ≥0∞)
    ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) m : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
simp [restrict, inter_comm t]

Premises used: MeasureTheory.OuterMeasure.restrict, Set.inter_comm
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
m m' : OuterMeasure α
hm : m ≤ m'
u : Set α
simp : LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞) ((m' : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) m : OuterMeasure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
    ((((restrict t : (a : OuterMeasure α) → OuterMeasure α) m' : OuterMeasure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
simp only [restrict_apply]

Premises used: MeasureTheory.OuterMeasure.restrict_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
m m' : OuterMeasure α
hm : m ≤ m'
u : Set α
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞) ((m' : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)

Tactic:
(hm _).trans (m'.mono <| inter_subset_inter_right _ h)

Premises used: Set.inter_subset_inter_right, MeasureTheory.OuterMeasure.mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
m m' : OuterMeasure α
hm : m ≤ m'
u : Set α
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞) ((m' : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)

Tactic:
exact (hm _).trans (m'.mono <| inter_subset_inter_right _ h)

Premises used: Set.inter_subset_inter_right, MeasureTheory.OuterMeasure.mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
m : OuterMeasure α
s : Set α
⊢ Eq (α := ℝ≥0∞)
    ((((restrict univ : (a : OuterMeasure α) → OuterMeasure α) m : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
m : OuterMeasure α
s : Set α
⊢ Eq (α := ℝ≥0∞)
    ((((restrict ∅ : (a : OuterMeasure α) → OuterMeasure α) m : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
ι : Sort u_3
s : Set α
m : ι → OuterMeasure α
⊢ Eq (α := OuterMeasure α) ((restrict s : (a : OuterMeasure α) → OuterMeasure α) (⨆ (i : ι), m i) : OuterMeasure α)
    (⨆ (i : ι), (restrict s : (a : OuterMeasure α) → OuterMeasure α) (m i) : OuterMeasure α)

Tactic:
simp [restrict]

Premises used: MeasureTheory.OuterMeasure.restrict
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_3
f : α → β
m : OuterMeasure β
s : Set β
⊢ f '' f ⁻¹' s =
    image (α := { x : β // x ∈ range f }) (Subtype.val (p := fun (x : β) ↦ x ∈ range f))
      (Subtype.val (p := fun (x : β) ↦ x ∈ range f) ⁻¹' s)

Tactic:
simp only [image_preimage_eq_inter_range, Subtype.range_coe]

Premises used: Subtype.range_coe, Set.image_preimage_eq_inter_range
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_3
f : α → β
m : OuterMeasure β
⊢ (map f : (a : OuterMeasure α) → OuterMeasure β) ((comap f : (a : OuterMeasure β) → OuterMeasure α) m) ≤ m

Tactic:
fun _ =>
  m.mono <| image_preimage_subset _ _

Premises used: MeasureTheory.OuterMeasure.mono, Set.image_preimage_subset
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
m : OuterMeasure α
s : Set α
⊢ (restrict s : (a : OuterMeasure α) → OuterMeasure α) m ≤ m

Tactic:
map_comap_le _ _

Premises used: MeasureTheory.OuterMeasure.map_comap_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_3
ma : OuterMeasure α
mb : OuterMeasure β
f : α → β
h : (map f : (a : OuterMeasure α) → OuterMeasure β) ma ≤ mb
s : Set β
⊢ LE.le (α := ℝ≥0∞)
    ((((map f : (a : OuterMeasure α) → OuterMeasure β) ma : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) mb : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa using h (s ∩ range f)

Premises used: Inter.inter, Set.range
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_3
f : α → β
hf : Surjective f
m : OuterMeasure β
s : Set β
rw :
  Eq (α := ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) m : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((m : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((map f : (a : OuterMeasure α) → OuterMeasure β) ((comap f : (a : OuterMeasure β) → OuterMeasure α) m) :
            OuterMeasure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((m : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_apply, comap_apply, hf.image_preimage]

Premises used: MeasureTheory.OuterMeasure.map_apply, MeasureTheory.OuterMeasure.comap_apply, Function.Surjective.image_preimage
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_3
f : α → β
m : OuterMeasure α
⊢ m ≤ (comap f : (a : OuterMeasure β) → OuterMeasure α) ((map f : (a : OuterMeasure α) → OuterMeasure β) m)

Tactic:
fun _ =>
  m.mono <| subset_preimage_image _ _

Premises used: MeasureTheory.OuterMeasure.mono, Set.subset_preimage_image
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_3
f : α → β
hf : Injective f
m : OuterMeasure α
s : Set α
rw :
  Eq (α := ℝ≥0∞)
    ((((map f : (a : OuterMeasure α) → OuterMeasure β) m : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s) : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) ((map f : (a : OuterMeasure α) → OuterMeasure β) m) :
            OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [comap_apply, map_apply, hf.preimage_image]

Premises used: MeasureTheory.OuterMeasure.map_apply, MeasureTheory.OuterMeasure.comap_apply, Function.Injective.preimage_image
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
s : Set α
h : s.Nonempty
a : α
as : a ∈ s
⊢ LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) ∞ (dirac a) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [smul_dirac_apply, as]

Premises used: MeasureTheory.OuterMeasure.smul_dirac_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
s : Set α
h : s = ∅
⊢ Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨅ (_ : s = ∅), 0 : ℝ≥0∞)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
s : Set α
h : s.Nonempty
⊢ Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨅ (_ : s = ∅), 0 : ℝ≥0∞)

Tactic:
simp [h, h.ne_empty]

Premises used: Set.Nonempty.ne_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
hs : s.Nonempty
rw :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ∞ ∞
⊢ Eq (α := ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) ⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [comap_apply, top_apply hs, top_apply (hs.image _)]

Premises used: MeasureTheory.OuterMeasure.comap_apply, Set.Nonempty.image, MeasureTheory.OuterMeasure.top_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞)
rw₃ : Eq (α := ℝ≥0∞) (⨅ (_ : f ⁻¹' s = ∅), 0 : ℝ≥0∞) (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞)
rw₄ : Eq (α := ℝ≥0∞) (⨅ (_ : f ⁻¹' s = ∅), 0) (⨅ (_ : f '' f ⁻¹' s = ∅), 0)
rw₅ rw₆ : Eq (α := ℝ≥0∞) (⨅ (_ : f ⁻¹' s = ∅), 0) (⨅ (_ : f ⁻¹' s = ∅), 0)
⊢ Eq (α := ℝ≥0∞) ((((map f : (a : OuterMeasure α) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_apply, restrict_apply, ← image_preimage_eq_inter_range, top_apply', top_apply',
      Set.image_eq_empty]

Premises used: MeasureTheory.OuterMeasure.map_apply, Set.image_preimage_eq_inter_range, Set.image_eq_empty, MeasureTheory.OuterMeasure.top_apply', MeasureTheory.OuterMeasure.restrict_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
rw :
  Eq (α := OuterMeasure β) ((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β)
    (⊤ : OuterMeasure β)
rw₁ :
  Eq.{u_2 + 1} (α := OuterMeasure β) ((restrict univ : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β)
    (⊤ : OuterMeasure β)
rw₂ rw₃ : Eq.{u_2 + 1} (α := OuterMeasure β) ⊤ ⊤
⊢ Eq.{u_2 + 1} (α := OuterMeasure β) ((map f : (a : OuterMeasure α) → OuterMeasure β) ⊤) ⊤

Tactic:
rw [map_top, hf.range_eq, restrict_univ]

Premises used: MeasureTheory.OuterMeasure.restrict_univ, Function.Surjective.range_eq, MeasureTheory.OuterMeasure.map_top
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
inst : MeasurableSpace α
⊢ IsPiSystem.{u_3} (α := α) {s : Set α | MeasurableSet s}

Tactic:
fun _ hs _ ht _ => hs.inter ht

Premises used: MeasurableSet, Set.Mem, setOf, IsPiSystem, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S s : Set α
h_s : Membership.mem (γ := Set (Set α)) {S} s
t : Set α
h_t : Membership.mem (γ := Set (Set α)) {S} t
_ : (s ∩ t).Nonempty → Membership.mem (γ := Set (Set α)) {S} (s ∩ t)
⊢ (s ∩ t).Nonempty → Membership.mem (γ := Set (Set α)) {S} (s ∩ t)

Tactic:
_
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S s : Set α
h_s : Membership.mem (γ := Set (Set α)) {S} s
t : Set α
h_t : Membership.mem (γ := Set (Set α)) {S} t
h : (s ∩ t).Nonempty
rw : Membership.mem (γ := Set (Set α)) {S} (S ∩ t)
rw₁ : Membership.mem (γ := Set (Set α)) {S} (S ∩ S)
rw₂ : Membership.mem (γ := Set (Set α)) {S} S
rw₃ rw₄ : S = S
⊢ Membership.mem (γ := Set (Set α)) {S} (s ∩ t)

Tactic:
rw [Set.mem_singleton_iff.1 h_s, Set.mem_singleton_iff.1 h_t, Set.inter_self,
    Set.mem_singleton_iff]

Premises used: Set.inter_self, Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert ∅ S
t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
inl : ∀ (hs : s = ∅), s ∩ t ∈ insert ∅ S
inr : ∀ (hs : s ∈ S), s ∩ t ∈ insert ∅ S
⊢ s ∩ t ∈ insert ∅ S

Tactic:
rcases hs with hs | hs
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s = ∅
⊢ s ∩ t ∈ insert ∅ S

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
inr : ∀ (ht : t = ∅), s ∩ t ∈ insert ∅ S
inr₁ : ∀ (ht : t ∈ S), s ∩ t ∈ insert ∅ S
⊢ s ∩ t ∈ insert ∅ S

Tactic:
rcases ht with ht | ht
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t = ∅
⊢ s ∩ t ∈ insert ∅ S

Tactic:
simp [ht]
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert ∅ S

Tactic:
Set.mem_insert_of_mem _ (h_pi s hs t ht hst)

Premises used: Set.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert ∅ S

Tactic:
exact Set.mem_insert_of_mem _ (h_pi s hs t ht hst)

Premises used: Set.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert univ S
t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
inl : ∀ (hs : s = univ), s ∩ t ∈ insert univ S
inr : ∀ (hs : s ∈ S), s ∩ t ∈ insert univ S
⊢ s ∩ t ∈ insert univ S

Tactic:
rcases hs with hs | hs
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s = univ
inl : ∀ (ht : t = univ), s ∩ t ∈ insert univ S
inl₁ : ∀ (ht : t ∈ S), s ∩ t ∈ insert univ S
⊢ s ∩ t ∈ insert univ S

Tactic:
rcases ht with ht | ht
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s = univ
ht : t = univ
⊢ s ∩ t ∈ insert univ S

Tactic:
simp [hs, ht]
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s = univ
ht : t ∈ S
⊢ s ∩ t ∈ insert univ S

Tactic:
simp [hs, ht]
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
inr : ∀ (ht : t = univ), s ∩ t ∈ insert univ S
inr₁ : ∀ (ht : t ∈ S), s ∩ t ∈ insert univ S
⊢ s ∩ t ∈ insert univ S

Tactic:
rcases ht with ht | ht
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t = univ
⊢ s ∩ t ∈ insert univ S

Tactic:
simp [hs, ht]
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert univ S

Tactic:
Set.mem_insert_of_mem _ (h_pi s hs t ht hst)

Premises used: Set.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert univ S

Tactic:
exact Set.mem_insert_of_mem _ (h_pi s hs t ht hst)

Premises used: Set.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : (f ⁻¹' s ∩ f ⁻¹' t).Nonempty
rw :
  ∀ (hst : (f ⁻¹' (s ∩ t)).Nonempty),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ t ∈ S, f ⁻¹' t = s} (f ⁻¹' (s ∩ t))
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ t ∈ S, f ⁻¹' t = s} (f ⁻¹' s ∩ f ⁻¹' t)

Tactic:
rw [← Set.preimage_inter] at hst ⊢

Premises used: Set.preimage_inter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : (f ⁻¹' (s ∩ t)).Nonempty
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ t ∈ S, f ⁻¹' t = s} (f ⁻¹' (s ∩ t))

Tactic:
⟨s ∩ t, h_pi s hs_mem t ht_mem (nonempty_of_nonempty_preimage hst), rfl⟩

Premises used: Set.Mem, setOf, Set.nonempty_of_nonempty_preimage, Inter.inter, And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : (f ⁻¹' (s ∩ t)).Nonempty
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ t ∈ S, f ⁻¹' t = s} (f ⁻¹' (s ∩ t))

Tactic:
exact ⟨s ∩ t, h_pi s hs_mem t ht_mem (nonempty_of_nonempty_preimage hst), rfl⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
s : ℕ → Set α
C : Set (Set α)
hC : IsPiSystem C
h : ∀ (n : ℕ), s n ∈ C
h' : (dissipate s 0).Nonempty
⊢ dissipate s 0 ∈ C

Tactic:
simpa using h 0

Premises used: OfNat.ofNat
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
s : ℕ → Set α
C : Set (Set α)
hC : IsPiSystem C
h : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ∀ (h' : (dissipate s n).Nonempty), dissipate s n ∈ C
h' : (dissipate s (n + 1)).Nonempty
succ : ∀ (h' : (dissipate s n ∩ s (n + 1)).Nonempty), dissipate s n ∩ s (n + 1) ∈ C
⊢ dissipate s (n + 1) ∈ C

Tactic:
rw [dissipate_succ] at h' ⊢

Premises used: Set.dissipate_succ
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
s : ℕ → Set α
C : Set (Set α)
hC : IsPiSystem C
h : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ∀ (h' : (dissipate s n).Nonempty), dissipate s n ∈ C
h' : (dissipate s n ∩ s (n + 1)).Nonempty
⊢ dissipate s n ∩ s (n + 1) ∈ C

Tactic:
hC (dissipate s n) (hn h'.left) (s (n + 1)) (h (n + 1)) h'

Premises used: Set.dissipate, HAdd.hAdd, Set.Nonempty.left, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
s : ℕ → Set α
C : Set (Set α)
hC : IsPiSystem C
h : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ∀ (h' : (dissipate s n).Nonempty), dissipate s n ∈ C
h' : (dissipate s n ∩ s (n + 1)).Nonempty
⊢ dissipate s n ∩ s (n + 1) ∈ C

Tactic:
exact hC (dissipate s n) (hn h'.left) (s (n + 1)) (h (n + 1)) h'

Premises used: Set.dissipate, HAdd.hAdd, Set.Nonempty.left, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
s : ℕ → Set α
C : Set (Set α)
hC : IsPiSystem C
h : ∀ (n : ℕ), s n ∈ C
n : ℕ
h' : (dissipate s n).Nonempty
zero : ∀ (h' : (dissipate s 0).Nonempty), dissipate s 0 ∈ C
succ :
  ∀ (n : ℕ) (hn : ∀ (h' : (dissipate s n).Nonempty), dissipate s n ∈ C) (h' : (dissipate s (n + 1)).Nonempty),
    dissipate s (n + 1) ∈ C
⊢ dissipate s n ∈ C

Tactic:
induction n with
  | zero => simpa using h 0
  | succ n hn =>
    rw [dissipate_succ] at h' ⊢
    exact hC (dissipate s n) (hn h'.left) (s (n + 1)) (h (n + 1)) h'

Premises used: Set.dissipate_succ, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun (x1 x2 : Set (Set α)) ↦ x1 ≤ x2) p
t1 : Set α
ht1 : Membership.mem (γ := Set (Set α)) (⋃ (n : ι), p n) t1
t2 : Set α
ht2 : Membership.mem (γ := Set (Set α)) (⋃ (n : ι), p n) t2
h : (t1 ∩ t2).Nonempty
rw :
  ∀ (ht1 : ∃ (i : ι), t1 ∈ p i) (t2 : Set α) (ht2 : ∃ (i : ι), t2 ∈ p i) (h : (t1 ∩ t2).Nonempty),
    ∃ (i : ι), t1 ∩ t2 ∈ p i
⊢ Membership.mem (γ := Set (Set α)) (⋃ (n : ι), p n) (t1 ∩ t2)

Tactic:
rw [Set.mem_iUnion] at ht1 ht2 ⊢

Premises used: Set.mem_iUnion
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun (x1 x2 : Set (Set α)) ↦ x1 ≤ x2) p
t1 : Set α
ht1 : ∃ (i : ι), t1 ∈ p i
t2 : Set α
ht2 : ∃ (i : ι), t2 ∈ p i
h : (t1 ∩ t2).Nonempty
obtain : ∀ (n : ι) (ht1 : t1 ∈ p n), ∃ (i : ι), t1 ∩ t2 ∈ p i
⊢ ∃ (i : ι), t1 ∩ t2 ∈ p i

Tactic:
obtain ⟨n, ht1⟩ := ht1
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun (x1 x2 : Set (Set α)) ↦ x1 ≤ x2) p
t1 t2 : Set α
ht2 : ∃ (i : ι), t2 ∈ p i
h : (t1 ∩ t2).Nonempty
n : ι
ht1 : t1 ∈ p n
obtain : ∀ (m : ι) (ht2 : t2 ∈ p m), ∃ (i : ι), t1 ∩ t2 ∈ p i
⊢ ∃ (i : ι), t1 ∩ t2 ∈ p i

Tactic:
obtain ⟨m, ht2⟩ := ht2