mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∈ p2
⊢ univ ∩ f2 n ∈ π n

pp: case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∉ p2
⊢ univ ∩ univ ∈ π n

Tactic:
·

Goal state after:
case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∈ p2
⊢ univ ∩ f2 n ∈ π n
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∉ p2
⊢ univ ∩ univ ∈ π n

Tactic:
·

Goal state after:
case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∉ p2
⊢ univ ∩ univ ∈ π n
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case mp
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (∀ (t : Set α),
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t) →
    ∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t

pp: case mpr
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤
          (inducedOuterMeasure m P0 m0) t) →
    ∀ (t : Set α),
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t

Tactic:
·

Goal state after:
case mp
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (∀ (t : Set α),
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t) →
    ∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
hs : μ sᶜ = 0
⊢ s = univ

pp: case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
⊢ s = univ → μ sᶜ = 0

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
hs : μ sᶜ = 0
⊢ s = univ
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
⊢ s = univ → μ sᶜ = 0

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
⊢ s = univ → μ sᶜ = 0
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
⊢ s = univ → μ sᶜ = 0

Tactic:
· rintro rfl
    simp

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) ≤ ⨆ i ∈ S, m i

pp: case refine_2
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ ⨆ i ∈ S, m i ≤ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S)

Tactic:
·

Goal state after:
case refine_1
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) ≤ ⨆ i ∈ S, m i
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ ⨆ i ∈ S, m i ≤ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S)

Tactic:
·

Goal state after:
case refine_2
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ ⨆ i ∈ S, m i ≤ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case mpr
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤
          (inducedOuterMeasure m P0 m0) t) →
    ∀ (t : Set α),
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t

Tactic:
·

Goal state after:
case mpr
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤
          (inducedOuterMeasure m P0 m0) t) →
    ∀ (t : Set α),
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᵐ[μ] ∅
⊢ s ∪ t =ᵐ[μ] s ↔ s ∪ t =ᵐ[μ] s ∪ ∅

Tactic:
union_empty

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᵐ[μ] ∅
⊢ s ∪ t =ᵐ[μ] s ↔ s ∪ t =ᵐ[μ] s
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
⊢ μ hs.choose = μ s

pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ μ h's.choose = μ s

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ¬∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ μ ⋯.choose = μ s

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
⊢ μ hs.choose = μ s
Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun n ↦ aeSeq hf p n x

Tactic:
simp only [aeSeq, hx, if_true]
  rw [funext fun n => mk_eq_fun_of_mem_aeSeqSet hf hx n]
  have h_ss : aeSeqSet hf p ⊆ { x | p x fun n => f n x } := by
    rw [← compl_compl { x | p x fun n => f n x }, aeSeqSet, Set.compl_subset_compl]
    refine Set.Subset.trans (Set.compl_subset_compl.mpr ?_) (subset_toMeasurable _ _)
    exact fun x hx => hx.2
  have hx' := Set.mem_of_subset_of_mem h_ss hx
  exact hx'

Goal state after:
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ μ h's.choose = μ s

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ¬∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ μ ⋯.choose = μ s

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ μ h's.choose = μ s
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ¬∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ μ ⋯.choose = μ s

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ¬∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ μ ⋯.choose = μ s
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: case mp
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ AEMeasurable g μ → ∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ

pp: case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ (∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ) → AEMeasurable g μ

Tactic:
·

Goal state after:
case mp
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ AEMeasurable g μ → ∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ (∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ) → AEMeasurable g μ

Tactic:
·

Goal state after:
case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ (∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ) → AEMeasurable g μ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case mp
α : Type u_1
s t : Set α
⊢ (∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = t) → t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

pp: case mpr
α : Type u_1
s t : Set α
⊢ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ → ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = t

Tactic:
·

Goal state after:
case mp
α : Type u_1
s t : Set α
⊢ (∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = t) → t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

pp: case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

Tactic:
·

Goal state after:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

pp: case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∉ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

Tactic:
·

Goal state after:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∉ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

Tactic:
·

Goal state after:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∉ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

Tactic:
·

Goal state after:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

pp: case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

Tactic:
·

Goal state after:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

Tactic:
·

Goal state after:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case mpr
α : Type u_1
s t : Set α
⊢ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ → ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = t

Tactic:
·

Goal state after:
case mpr
α : Type u_1
s t : Set α
⊢ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ → ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = t
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ i, U i ∈ ⨅ i, f i

pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ MeasurableSet (⋂ i, U i)

pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ i, U i ⊆ ⋂ i, V i

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ i, U i ∈ ⨅ i, f i
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
⊢ ∑' (i : ℕ), m (disjointed f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯

Tactic:
refine ENNReal.tsum_le_tsum fun i => ?_

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
i : ℕ
⊢ m (disjointed f i) ⋯ ≤ m (f i) ⋯
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ MeasurableSet (⋂ i, U i)

pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ i, U i ⊆ ⋂ i, V i

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ MeasurableSet (⋂ i, U i)
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ i, U i ⊆ ⋂ i, V i

Tactic:
·

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ i, U i ⊆ ⋂ i, V i
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ms = ∞
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ms = ∞
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms