awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
C : Set (Set α)
D : Set (Set β)
hC : generateFrom C = inst
hD : generateFrom D = inst_1
h2C : IsCountablySpanning C
h2D : IsCountablySpanning D
⊢ Eq (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
    Prod.instMeasurableSpace
have rw : Eq (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
  Prod.instMeasurableSpace
Tactic: rw [← hC, ← hD, generateFrom_prod_eq h2C h2D]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
C : Set (Set α)
D : Set (Set β)
hC : generateFrom C = inst
hD : generateFrom D = inst_1
h2C : IsCountablySpanning C
h2D : IsCountablySpanning D
rw :
  Eq (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
    Prod.instMeasurableSpace
⊢ Eq (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
    Prod.instMeasurableSpace
have rw₁ : Eq (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
  Prod.instMeasurableSpace
Tactic: rw [← hC, ← hD, generateFrom_prod_eq h2C h2D]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
C : Set (Set α)
D : Set (Set β)
hC : generateFrom C = inst
hD : generateFrom D = inst_1
h2C : IsCountablySpanning C
h2D : IsCountablySpanning D
rw :
  Eq (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
    Prod.instMeasurableSpace
rw₁ :
  Eq (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
    Prod.instMeasurableSpace
⊢ Eq (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
    Prod.instMeasurableSpace
have rw₂ : Eq (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
  (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
Tactic: rw [← hC, ← hD, generateFrom_prod_eq h2C h2D]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
X : α → β
Y : α → γ
⊢ MeasurableSpace.comap (fun (ω : α) ↦ (X ω, Y ω)) (mβ.prod mγ) =
    MeasurableSpace.comap X mβ ⊔ MeasurableSpace.comap Y mγ
have 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γ
Tactic: simp_rw [MeasurableSpace.prod, comap_sup, comap_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
X : γ → α
Y : δ → β
⊢ MeasurableSpace.comap (Prod.map X Y) (mα.prod mβ) = (MeasurableSpace.comap X mα).prod (MeasurableSpace.comap Y mβ)
have 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β
Tactic: simp_rw [MeasurableSpace.prod, comap_sup, comap_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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
⊢ MeasurableEmbedding (Prod.map g f)
have rw : Function.Injective (Prod.map g f) ∧
  MeasurableSpace.comap (Prod.map g f) Prod.instMeasurableSpace = Prod.instMeasurableSpace ∧
    MeasurableSet (range (Prod.map g f))
Tactic: rw [MeasurableEmbedding.iff_comap_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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))
have refine_1 : MeasurableSpace.comap (Prod.map g f) Prod.instMeasurableSpace = Prod.instMeasurableSpace
Tactic: refine ⟨hg.injective.prodMap hf.injective, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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
⊢ Function.Injective (Prod.map g f) ∧
    MeasurableSpace.comap (Prod.map g f) Prod.instMeasurableSpace = Prod.instMeasurableSpace ∧
      MeasurableSet (range (Prod.map g f))
have refine_2 : MeasurableSet (range (Prod.map g f))
Tactic: refine ⟨hg.injective.prodMap hf.injective, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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
⊢ MeasurableSpace.comap (Prod.map g f) Prod.instMeasurableSpace = Prod.instMeasurableSpace
have refine_1 : MeasurableSpace.comap (Prod.map g f) (mδ.prod mβ) = Prod.instMeasurableSpace
Tactic: rw [Prod.instMeasurableSpace, Prod.instMeasurableSpace, MeasurableSpace.comap_prodMap,
      hg.comap_eq, hf.comap_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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
⊢ MeasurableSpace.comap (Prod.map g f) Prod.instMeasurableSpace = Prod.instMeasurableSpace
have refine_1₁ : MeasurableSpace.comap (Prod.map g f) (mδ.prod mβ) = mγ.prod mα
Tactic: rw [Prod.instMeasurableSpace, Prod.instMeasurableSpace, MeasurableSpace.comap_prodMap,
      hg.comap_eq, hf.comap_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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α
⊢ MeasurableSpace.comap (Prod.map g f) Prod.instMeasurableSpace = Prod.instMeasurableSpace
have refine_1₂ : (MeasurableSpace.comap g mδ).prod (MeasurableSpace.comap f mβ) = mγ.prod mα
Tactic: rw [Prod.instMeasurableSpace, Prod.instMeasurableSpace, MeasurableSpace.comap_prodMap,
      hg.comap_eq, hf.comap_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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α
⊢ MeasurableSpace.comap (Prod.map g f) Prod.instMeasurableSpace = Prod.instMeasurableSpace
have refine_1₃ : mγ.prod (MeasurableSpace.comap f mβ) = mγ.prod mα
Tactic: rw [Prod.instMeasurableSpace, Prod.instMeasurableSpace, MeasurableSpace.comap_prodMap,
      hg.comap_eq, hf.comap_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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α
⊢ MeasurableSpace.comap (Prod.map g f) Prod.instMeasurableSpace = Prod.instMeasurableSpace
have refine_1₄ : mγ.prod mα = mγ.prod mα
Tactic: rw [Prod.instMeasurableSpace, Prod.instMeasurableSpace, MeasurableSpace.comap_prodMap,
      hg.comap_eq, hf.comap_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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 (Prod.map g f))
have refine_2 : MeasurableSet (range g ×ˢ range f)
Tactic: rw [range_prodMap]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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' : γ
⊢ Eq (α := α × β) ((fun (y : γ) ↦ (x, f y)) y) ((fun (y : γ) ↦ (x, f y)) y') → y = y'
have simp : f y = f y' → y = y'
Tactic: simp only [Prod.mk.injEq, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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 (α := α × β) ((fun (y : γ) ↦ (x, f y)) '' s)
have h : (fun (y : γ) ↦ (x, f y)) '' s = SProd.sprod (α := Set α) {x} (f '' s)
Tactic: convert! (MeasurableSet.singleton x).prod (hf.measurableSet_image.mpr hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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
⊢ (fun (y : γ) ↦ (x, f y)) '' s = SProd.sprod (α := Set α) {x} (f '' s)
have h : ∀ (x_1 : α × β),
  Membership.mem (γ := Set (α × β)) ((fun (y : γ) ↦ (x, f y)) '' s) x_1 ↔ x_1 ∈ SProd.sprod (α := Set α) {x} (f '' s)
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEDisjoint (goal)
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)
have 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)
Tactic: refine ⟨fun i => toMeasurable μ (s i ∩ ⋃ j ∈ ({i}ᶜ : Set ι), s j), fun i =>
    measurableSet_toMeasurable _ _, fun i => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEDisjoint (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: refine ⟨fun i => toMeasurable μ (s i ∩ ⋃ j ∈ ({i}ᶜ : Set ι), s j), fun i =>
    measurableSet_toMeasurable _ _, fun i => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEDisjoint (goal)
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)
        ((fun (i : ι) ↦ toMeasurable μ (s i ∩ ⋃ (j : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i}ᶜ j), s j)) i) :
      ENNReal)
    (0 : ENNReal)
have refine_1 : Eq (α := ENNReal)
  ((μ : (a : Set α) → ENNReal) (⋃ (i_1 : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i}ᶜ i_1), s i ∩ s i_1) : ENNReal)
  (0 : ENNReal)
Tactic: simp only [measure_toMeasurable, inter_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEDisjoint (goal)
Goal:
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
⊢ 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)
have 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)
Tactic: simp only [Pairwise, disjoint_left, onFun, mem_diff, not_and, and_imp, Classical.not_not]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEDisjoint (hypothesis)
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 ∈ toMeasurable μ (s j ∩ ⋃ (j_1 : ι), ⋃ (_ : Membership.mem (γ := Set ι) {j}ᶜ j_1), s j_1)
have hU₁ : 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)
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEDisjoint (hypothesis)
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 ∈ toMeasurable μ (s j ∩ ⋃ (j_1 : ι), ⋃ (_ : Membership.mem (γ := Set ι) {j}ᶜ j_1), s j_1)
have hU₁ : 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
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEDisjoint (goal)
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
⊢ AEDisjoint μ t s
have rwa : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal) (0 : ENNReal)
Tactic: rwa [AEDisjoint, inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEDisjoint (goal)
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)
⊢ AEDisjoint μ t s
have rwa₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)
Tactic: rwa [AEDisjoint, inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEDisjoint (goal)
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : Disjoint s t
⊢ AEDisjoint μ s t
have rw : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)
Tactic: rw [AEDisjoint, disjoint_iff_inter_eq_empty.1 h, measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEDisjoint (goal)
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)
⊢ AEDisjoint μ s t
have rw₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) ∅ : ENNReal) (0 : ENNReal)
Tactic: rw [AEDisjoint, disjoint_iff_inter_eq_empty.1 h, measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEDisjoint (goal)
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)
⊢ AEDisjoint μ s t
have rw₂ : Eq (α := ENNReal) 0 0
Tactic: rw [AEDisjoint, disjoint_iff_inter_eq_empty.1 h, measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
⊢ AEMeasurable (_m := m0) f 0
have a : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
h : Nontrivial α
⊢ AEMeasurable (_m := m0) f 0
have inhabit : ∀ (inhabited_h : Inhabited α), AEMeasurable (_m := m0) f 0
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
h : NeZero (R := Measure β) (Measure.map f μ)
⊢ AEMeasurable f μ
have by_contra : ∀ (h' : ¬AEMeasurable f μ), False
Tactic: by_contra h'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
⊢ AEMeasurable f (sum μ)
have a : Nontrivial β
Tactic: nontriviality β
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
⊢ AEMeasurable f (sum μ)
have inhabit : ∀ (inhabited_h : Inhabited β), AEMeasurable f (sum μ)
Tactic: inhabit β
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
i : ι
⊢ Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) {x : α | f x ≠ mk f sorry x} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
⊢ AEMeasurable f (sum μ)
have hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have hsμ : ∀ i, μ i (s i) = 0 := by
    intro i
    rw [measure_toMeasurable]
    exact (h i).ae_eq_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ AEMeasurable f (sum μ)
have hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
Tactic: have hsm : MeasurableSet (⋂ i, s i) :=
    MeasurableSet.iInter fun i => measurableSet_toMeasurable _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
i : ι
x : α
hx : x ∉ s i
⊢ f x = mk f ⋯ x
have contrapose! : ∀ (hx : f x ≠ mk f sorry x), x ∈ s i
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
⊢ AEMeasurable f (sum μ)
have hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f sorry x
Tactic: have hs : ∀ i x, x ∉ s i → f x = (h i).mk f x := by
    intro i x hx
    contrapose! hx
    exact subset_toMeasurable _ _ hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
⊢ AEMeasurable f (sum μ)
have refine_1 : Measurable (α := (↑(⋂ (i : ι), s i) : Type u_2)) (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), s i) g)
Tactic: refine ⟨g, measurable_of_restrict_of_restrict_compl hsm ?_ ?_, ae_sum_iff.mpr fun i => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
refine_1 : Measurable (α := (↑(⋂ (i : ι), s i) : Type u_2)) (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), s i) g)
⊢ AEMeasurable f (sum μ)
have refine_2 : Measurable (α := (↑(⋂ (i : ι), s i)ᶜ : Type u_2)) (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), s i)ᶜ g)
Tactic: refine ⟨g, measurable_of_restrict_of_restrict_compl hsm ?_ ?_, ae_sum_iff.mpr fun i => ?_⟩