awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
X : α → β
Y : α → γ
simp_rw :
  MeasurableSpace.comap (Function.comp (β := β × γ) Prod.fst fun (ω : α) ↦ (X ω, Y ω)) mβ ⊔
      MeasurableSpace.comap (Function.comp (β := β × γ) Prod.snd fun (ω : α) ↦ (X ω, Y ω)) mγ =
    MeasurableSpace.comap X mβ ⊔ MeasurableSpace.comap Y mγ
⊢ MeasurableSpace.comap (fun (ω : α) ↦ (X ω, Y ω)) (mβ.prod mγ) =
    MeasurableSpace.comap X mβ ⊔ MeasurableSpace.comap Y mγ

Tactic:
simp_rw [MeasurableSpace.prod, comap_sup, comap_comp]

Premises used: MeasurableSpace.prod, MeasurableSpace.comap_comp, MeasurableSpace.comap_sup
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
X : α → β
Y : α → γ
⊢ MeasurableSpace.comap (Function.comp (β := β × γ) Prod.fst fun (ω : α) ↦ (X ω, Y ω)) mβ ⊔
      MeasurableSpace.comap (Function.comp (β := β × γ) Prod.snd fun (ω : α) ↦ (X ω, Y ω)) mγ =
    MeasurableSpace.comap X mβ ⊔ MeasurableSpace.comap Y mγ

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
X : γ → α
Y : δ → β
simp_rw :
  MeasurableSpace.comap (Prod.fst ∘ Prod.map X Y) mα ⊔ MeasurableSpace.comap (Prod.snd ∘ Prod.map X Y) mβ =
    MeasurableSpace.comap (X ∘ Prod.fst) mα ⊔ MeasurableSpace.comap (Y ∘ Prod.snd) mβ
⊢ MeasurableSpace.comap (Prod.map X Y) (mα.prod mβ) = (MeasurableSpace.comap X mα).prod (MeasurableSpace.comap Y mβ)

Tactic:
simp_rw [MeasurableSpace.prod, comap_sup, comap_comp]

Premises used: MeasurableSpace.prod, MeasurableSpace.comap_comp, MeasurableSpace.comap_sup
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
X : γ → α
Y : δ → β
⊢ MeasurableSpace.comap (Prod.fst ∘ Prod.map X Y) mα ⊔ MeasurableSpace.comap (Prod.snd ∘ Prod.map X Y) mβ =
    MeasurableSpace.comap (X ∘ Prod.fst) mα ⊔ MeasurableSpace.comap (Y ∘ Prod.snd) mβ

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
rw :
  Function.Injective (Prod.map g f) ∧
    MeasurableSpace.comap (Prod.map g f) Prod.instMeasurableSpace = Prod.instMeasurableSpace ∧
      MeasurableSet (range (Prod.map g f))
⊢ MeasurableEmbedding (Prod.map g f)

Tactic:
rw [MeasurableEmbedding.iff_comap_eq]

Premises used: MeasurableEmbedding.iff_comap_eq
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ Function.Injective (Prod.map g f) ∧
    MeasurableSpace.comap (Prod.map g f) Prod.instMeasurableSpace = Prod.instMeasurableSpace ∧
      MeasurableSet (range (Prod.map g f))

Tactic:
⟨hg.injective.prodMap hf.injective, ?_, ?_⟩

Premises used: Function.Injective.prodMap, MeasurableEmbedding.injective, And.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
refine_1 : MeasurableSpace.comap (Prod.map g f) Prod.instMeasurableSpace = Prod.instMeasurableSpace
refine_2 : MeasurableSet (range (Prod.map g f))
⊢ Function.Injective (Prod.map g f) ∧
    MeasurableSpace.comap (Prod.map g f) Prod.instMeasurableSpace = Prod.instMeasurableSpace ∧
      MeasurableSet (range (Prod.map g f))

Tactic:
refine ⟨hg.injective.prodMap hf.injective, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
refine_1 : MeasurableSpace.comap (Prod.map g f) (mδ.prod mβ) = Prod.instMeasurableSpace
refine_1₁ : MeasurableSpace.comap (Prod.map g f) (mδ.prod mβ) = mγ.prod mα
refine_1₂ : (MeasurableSpace.comap g mδ).prod (MeasurableSpace.comap f mβ) = mγ.prod mα
refine_1₃ : mγ.prod (MeasurableSpace.comap f mβ) = mγ.prod mα
refine_1₄ refine_1₅ : mγ.prod mα = mγ.prod mα
⊢ MeasurableSpace.comap (Prod.map g f) Prod.instMeasurableSpace = Prod.instMeasurableSpace

Tactic:
rw [Prod.instMeasurableSpace, Prod.instMeasurableSpace, MeasurableSpace.comap_prodMap,
      hg.comap_eq, hf.comap_eq]

Premises used: MeasurableSpace.comap_prodMap, MeasurableEmbedding.comap_eq, Prod.instMeasurableSpace
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
refine_2 : MeasurableSet (range g ×ˢ range f)
⊢ MeasurableSet (range (Prod.map g f))

Tactic:
rw [range_prodMap]

Premises used: Set.range_prodMap
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ MeasurableSet (range g ×ˢ range f)

Tactic:
hg.measurableSet_range.prod hf.measurableSet_range

Premises used: MeasurableSet.prod, MeasurableEmbedding.measurableSet_range
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ MeasurableSet (range g ×ˢ range f)

Tactic:
exact hg.measurableSet_range.prod hf.measurableSet_range

Premises used: MeasurableSet.prod, MeasurableEmbedding.measurableSet_range
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst_1 : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α
f : γ → β
hf : MeasurableEmbedding f
y y' : γ
simp : f y = f y' → y = y'
⊢ Eq (α := α × β) ((fun (y : γ) ↦ (x, f y)) y) ((fun (y : γ) ↦ (x, f y)) y') → y = y'

Tactic:
simp only [Prod.mk.injEq, true_and]

Premises used: Prod.mk.injEq, true_and
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst_1 : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α
f : γ → β
hf : MeasurableEmbedding f
y y' : γ
⊢ f y = f y' → y = y'

Tactic:
fun h ↦ hf.injective h

Premises used: MeasurableEmbedding.injective
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst_1 : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α
f : γ → β
hf : MeasurableEmbedding f
y y' : γ
⊢ f y = f y' → y = y'

Tactic:
exact fun h ↦ hf.injective h

Premises used: MeasurableEmbedding.injective
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst_1 : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α
f : γ → β
hf : MeasurableEmbedding f
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet (SProd.sprod (α := Set α) {x} (f '' s))

Tactic:
(MeasurableSet.singleton x).prod (hf.measurableSet_image.mpr hs)

Premises used: Iff.mpr, MeasurableSet.singleton, MeasurableEmbedding.measurableSet_image, MeasurableSet.prod
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst_1 : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α
f : γ → β
hf : MeasurableEmbedding f
s : Set γ
hs : MeasurableSet s
h : (fun (y : γ) ↦ (x, f y)) '' s = SProd.sprod (α := Set α) {x} (f '' s)
⊢ MeasurableSet (α := α × β) ((fun (y : γ) ↦ (x, f y)) '' s)

Tactic:
convert! (MeasurableSet.singleton x).prod (hf.measurableSet_image.mpr hs)

Premises used: Iff.mpr, MeasurableSet.singleton, MeasurableEmbedding.measurableSet_image, MeasurableSet.prod
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst_1 : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α
f : γ → β
hf : MeasurableEmbedding f
s : Set γ
hs : MeasurableSet s
h :
  ∀ (x_1 : α × β),
    Membership.mem (γ := Set (α × β)) ((fun (y : γ) ↦ (x, f y)) '' s) x_1 ↔ x_1 ∈ SProd.sprod (α := Set α) {x} (f '' s)
⊢ (fun (y : γ) ↦ (x, f y)) '' s = SProd.sprod (α := Set α) {x} (f '' s)

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst_1 : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x_1 : α
f : γ → β
hf : MeasurableEmbedding f
s : Set γ
hs : MeasurableSet s
x : α × β
⊢ Membership.mem (γ := Set (α × β)) ((fun (y : γ) ↦ (x_1, f y)) '' s) x ↔ x ∈ SProd.sprod (α := Set α) {x_1} (f '' s)

Tactic:
simp [Prod.ext_iff, eq_comm, ← exists_and_left, and_left_comm]

Premises used: Prod.ext_iff, exists_and_left, and_left_comm, eq_comm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
x : α
⊢ MeasurableEmbedding (α := β) (Prod.mk x)

Tactic:
MeasurableEmbedding.prodMk_left x MeasurableEmbedding.id

Premises used: MeasurableEmbedding.id, MeasurableEmbedding.prodMk_left
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst_1 : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : γ → β
hf : MeasurableEmbedding f
x : α
⊢ MeasurableEmbedding (β := β × α) fun (y : γ) ↦ (f y, x)

Tactic:
MeasurableEquiv.prodComm.measurableEmbedding.comp (hf.prodMk_left _)

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEquiv.prodComm, MeasurableEmbedding.prodMk_left, MeasurableEmbedding.comp, Prod.swap
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
x : α
⊢ MeasurableEmbedding (β := β × α) fun (y : β) ↦ (y, x)

Tactic:
MeasurableEmbedding.prodMk_right MeasurableEmbedding.id x

Premises used: MeasurableEmbedding.id, MeasurableEmbedding.prodMk_right
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
⊢ ∃ (t : ι → Set α),
    (∀ (i : ι), MeasurableSet (t i)) ∧
      (∀ (i : ι), Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t i) : ENNReal) (0 : ENNReal)) ∧
        Pairwise.{u_1} (α := ι) (onFun.{u_1 + 1, u_2 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ s i \ t i)

Tactic:
⟨fun i => toMeasurable μ (s i ∩ ⋃ j ∈ ({i}ᶜ : Set ι), s j), fun i =>
    measurableSet_toMeasurable _ _, fun i => ?_, ?_⟩

Premises used: Inter.inter, MeasureTheory.measurableSet_toMeasurable, And.intro, Exists.intro, MeasureTheory.toMeasurable, Set.iUnion
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
refine_1 :
  ∀ (i : ι),
    Eq (α := ENNReal)
      ((μ : (a : Set α) → ENNReal)
          ((fun (i : ι) ↦ toMeasurable μ (s i ∩ ⋃ (j : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i}ᶜ j), s j)) i) :
        ENNReal)
      (0 : ENNReal)
refine_2 :
  Pairwise.{u_1} (α := ι)
    (onFun.{u_1 + 1, u_2 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦
      s i \ (fun (i : ι) ↦ toMeasurable μ (s i ∩ ⋃ (j : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i}ᶜ j), s j)) i)
⊢ ∃ (t : ι → Set α),
    (∀ (i : ι), MeasurableSet (t i)) ∧
      (∀ (i : ι), Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t i) : ENNReal) (0 : ENNReal)) ∧
        Pairwise.{u_1} (α := ι) (onFun.{u_1 + 1, u_2 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ s i \ t i)

Tactic:
refine ⟨fun i => toMeasurable μ (s i ∩ ⋃ j ∈ ({i}ᶜ : Set ι), s j), fun i =>
    measurableSet_toMeasurable _ _, fun i => ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i : ι
refine_1 :
  Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal) (⋃ (i_1 : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i}ᶜ i_1), s i ∩ s i_1) : ENNReal)
    (0 : ENNReal)
⊢ Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal)
        ((fun (i : ι) ↦ toMeasurable μ (s i ∩ ⋃ (j : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i}ᶜ j), s j)) i) :
      ENNReal)
    (0 : ENNReal)

Tactic:
simp only [measure_toMeasurable, inter_iUnion]

Premises used: MeasureTheory.measure_toMeasurable, Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i : ι
⊢ Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal) (⋃ (i_1 : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i}ᶜ i_1), s i ∩ s i_1) : ENNReal)
    (0 : ENNReal)

Tactic:
(measure_biUnion_null_iff <| to_countable _).2 fun j hj => hd (Ne.symm hj)

Premises used: Iff.mpr, Ne.symm, Set.to_countable, MeasureTheory.measure_biUnion_null_iff
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i : ι
⊢ Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal) (⋃ (i_1 : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i}ᶜ i_1), s i ∩ s i_1) : ENNReal)
    (0 : ENNReal)

Tactic:
exact (measure_biUnion_null_iff <| to_countable _).2 fun j hj => hd (Ne.symm hj)

Premises used: Iff.mpr, Ne.symm, Set.to_countable, MeasureTheory.measure_biUnion_null_iff
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
refine_2 :
  ∀ ⦃i j : ι⦄,
    i ≠ j →
      ∀ ⦃a : α⦄,
        a ∈ s i →
          a ∉ toMeasurable μ (s i ∩ ⋃ (j : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i}ᶜ j), s j) →
            a ∈ s j → a ∈ toMeasurable μ (s j ∩ ⋃ (j_1 : ι), ⋃ (_ : Membership.mem (γ := Set ι) {j}ᶜ j_1), s j_1)
⊢ Pairwise.{u_1} (α := ι)
    (onFun.{u_1 + 1, u_2 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦
      s i \ (fun (i : ι) ↦ toMeasurable μ (s i ∩ ⋃ (j : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i}ᶜ j), s j)) i)

Tactic:
simp only [Pairwise, disjoint_left, onFun, mem_diff, not_and, and_imp, Classical.not_not]

Premises used: Function.onFun, Classical.not_not, and_imp, Set.disjoint_left, Set.mem_diff, Pairwise, not_and
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i j : ι
hne : i ≠ j
x : α
hi : x ∈ s i
hU : x ∉ toMeasurable μ (s i ∩ ⋃ (j : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i}ᶜ j), s j)
hj : x ∈ s j
⊢ x ∉ s i ∩ ⋃ (j : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i}ᶜ j), s j

Tactic:
replace hU : x ∉ s i ∩ iUnion fun j ↦ iUnion fun _ ↦ s j :=
      fun h ↦ hU (subset_toMeasurable _ _ h)
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i j : ι
hne : i ≠ j
x : α
hi : x ∈ s i
hj : x ∈ s j
hU : x ∉ s i ∩ ⋃ (j : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i}ᶜ j), s j
⊢ x ∈ s i → ∀ (x_1 : ι) (x_2 : Membership.mem (γ := Set ι) {i}ᶜ x_1), x ∉ s x_1

Tactic:
simp only [mem_inter_iff, mem_iUnion, not_and, not_exists] at hU

Premises used: Set.mem_inter_iff, Set.mem_iUnion, not_exists, not_and
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i j : ι
hne : i ≠ j
x : α
hi : x ∈ s i
hj : x ∈ s j
hU : x ∈ s i → ∀ (x_1 : ι) (x_2 : Membership.mem (γ := Set ι) {i}ᶜ x_1), x ∉ s x_1
⊢ x ∈ toMeasurable μ (s j ∩ ⋃ (j_1 : ι), ⋃ (_ : Membership.mem (γ := Set ι) {j}ᶜ j_1), s j_1)

Tactic:
(hU hi j hne.symm hj).elim

Premises used: False.elim, Ne.symm
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i j : ι
hne : i ≠ j
x : α
hi : x ∈ s i
hj : x ∈ s j
hU : x ∈ s i → ∀ (x_1 : ι) (x_2 : Membership.mem (γ := Set ι) {i}ᶜ x_1), x ∉ s x_1
⊢ x ∈ toMeasurable μ (s j ∩ ⋃ (j_1 : ι), ⋃ (_ : Membership.mem (γ := Set ι) {j}ᶜ j_1), s j_1)

Tactic:
exact (hU hi j hne.symm hj).elim

Premises used: False.elim, Ne.symm
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)

Tactic:
h

Premises used: MeasureTheory.AEDisjoint
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
rwa : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal) (0 : ENNReal)
rwa₁ rwa₂ rwa₃ rwa₄ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)
⊢ AEDisjoint μ t s

Tactic:
rwa [AEDisjoint, inter_comm]

Premises used: MeasureTheory.AEDisjoint, Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
⊢ Symmetric (AEDisjoint μ)

Tactic:
fun _ _ => AEDisjoint.symm

Premises used: Symmetric, MeasureTheory.AEDisjoint.symm
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ AEDisjoint μ s t ↔ AEDisjoint μ t s

Tactic:
⟨AEDisjoint.symm, AEDisjoint.symm⟩

Premises used: MeasureTheory.AEDisjoint.symm, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : Disjoint s t
rw : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)
rw₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) ∅ : ENNReal) (0 : ENNReal)
rw₂ rw₃ : Eq (α := ENNReal) 0 0
⊢ AEDisjoint μ s t

Tactic:
rw [AEDisjoint, disjoint_iff_inter_eq_empty.1 h, measure_empty]

Premises used: MeasureTheory.measure_empty, MeasureTheory.AEDisjoint, Set.disjoint_iff_inter_eq_empty, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : ι → Set α
hf : Pairwise (Disjoint on f)
⊢ Pairwise (AEDisjoint μ on f)

Tactic:
hf.mono fun _i _j h => h.aedisjoint

Premises used: Disjoint.aedisjoint, Pairwise.mono
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : ι → Set α
s : Set ι
hf : s.PairwiseDisjoint f
⊢ s.Pairwise (AEDisjoint μ on f)

Tactic:
hf.mono' fun _i _j h => h.aedisjoint

Premises used: Set.Pairwise.mono'
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
h : AEDisjoint μ s t
hu : u ≤ᶠ[ae μ] s
hv : v ≤ᶠ[ae μ] t
⊢ AEDisjoint μ u v

Tactic:
measure_mono_null_ae (hu.inter hv) h

Premises used: MeasureTheory.AEDisjoint, Filter.EventuallyLE.inter, MeasureTheory.measure_mono_null_ae
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
h : AEDisjoint μ s t
hu : u ⊆ s
hv : v ⊆ t
⊢ AEDisjoint μ u v

Tactic:
mono_ae h (HasSubset.Subset.eventuallyLE hu) (HasSubset.Subset.eventuallyLE hv)

Premises used: HasSubset.Subset.eventuallyLE, MeasureTheory.AEDisjoint.mono_ae
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
h : AEDisjoint μ s t
hu : u =ᶠ[ae μ] s
hv : v =ᶠ[ae μ] t
⊢ AEDisjoint μ u v

Tactic:
mono_ae h (Filter.EventuallyEq.le hu) (Filter.EventuallyEq.le hv)

Premises used: Filter.EventuallyEq.le, MeasureTheory.AEDisjoint.mono_ae
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
t : Set α
ι : Sort u_3
inst : Countable ι
s : ι → Set α
⊢ AEDisjoint μ (⋃ (i : ι), s i) t ↔ ∀ (i : ι), AEDisjoint μ (s i) t

Tactic:
simp only [AEDisjoint, iUnion_inter, measure_iUnion_null_iff]

Premises used: MeasureTheory.measure_iUnion_null_iff, MeasureTheory.AEDisjoint, Set.iUnion_inter
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set α
ι : Sort u_3
inst : Countable ι
t : ι → Set α
⊢ AEDisjoint μ s (⋃ (i : ι), t i) ↔ ∀ (i : ι), AEDisjoint μ s (t i)

Tactic:
simp only [AEDisjoint, inter_iUnion, measure_iUnion_null_iff]

Premises used: MeasureTheory.measure_iUnion_null_iff, MeasureTheory.AEDisjoint, Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u : Set α
⊢ AEDisjoint μ (s ∪ t) u ↔ AEDisjoint μ s u ∧ AEDisjoint μ t u

Tactic:
simp [union_eq_iUnion, and_comm]

Premises used: and_comm, Set.union_eq_iUnion
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u : Set α
⊢ AEDisjoint μ s (t ∪ u) ↔ AEDisjoint μ s t ∧ AEDisjoint μ s u

Tactic:
simp [union_eq_iUnion, and_comm]

Premises used: and_comm, Set.union_eq_iUnion
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : AEDisjoint μ s u
ht : AEDisjoint μ t u
⊢ AEDisjoint μ (s ∪ t) u

Tactic:
union_left_iff.mpr ⟨hs, ht⟩

Premises used: Iff.mpr, And.intro, MeasureTheory.AEDisjoint.union_left_iff
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : AEDisjoint μ s t
hu : AEDisjoint μ s u
⊢ AEDisjoint μ s (t ∪ u)

Tactic:
union_right_iff.2 ⟨ht, hu⟩

Premises used: Iff.mpr, MeasureTheory.AEDisjoint.union_right_iff, And.intro
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
⊢ s \ t =ᶠ[ae μ] s

Tactic:
@diff_self_inter _ s t ▸ diff_null_ae_eq_self h

Premises used: Set.diff_self_inter, MeasureTheory.diff_null_ae_eq_self, Eq.rec
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
⊢ t \ s =ᶠ[ae μ] t

Tactic:
diff_ae_eq_left <| AEDisjoint.symm h

Premises used: MeasureTheory.AEDisjoint.symm, MeasureTheory.AEDisjoint.diff_ae_eq_left
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s \ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)

Tactic:
measure_congr <| AEDisjoint.diff_ae_eq_left h

Premises used: MeasureTheory.measure_congr, MeasureTheory.AEDisjoint.diff_ae_eq_left
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t \ s) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)

Tactic:
measure_congr <| AEDisjoint.diff_ae_eq_right h

Premises used: MeasureTheory.measure_congr, MeasureTheory.AEDisjoint.diff_ae_eq_right
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
x : α
hx : x ∈ s \ toMeasurable μ (s ∩ t)
⊢ x ∈ s \ t

Tactic:
simpa using ⟨hx.1, fun hxt => hx.2 <| subset_toMeasurable _ _ ⟨hx.1, hxt⟩⟩