awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
hτ : IsStoppingTime ℱ τ
i : ι
inst_4 : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
⊢ μ[f | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ (↑i : WithTop ι)})] μ[f | hτ.measurableSpace]
have refine : ∀ (t : Set Ω),
  MeasurableSet ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ t)
Tactic: refine (condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le
    (hτ.min_const i).measurableSpace_le (hτ.measurableSet_le' i) fun t => ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
hτ : IsStoppingTime ℱ τ
i : ι
inst_4 : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
t : Set Ω
⊢ MeasurableSet ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ t)
have rw : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
Tactic: rw [Set.inter_comm _ t, hτ.measurableSet_inter_le_const_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
hτ : IsStoppingTime ℱ τ
i : ι
inst_4 : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
t : Set Ω
rw : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
⊢ MeasurableSet ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ t)
have rw₁ : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
Tactic: rw [Set.inter_comm _ t, hτ.measurableSet_inter_le_const_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
inst_7 : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
⊢ μ[f | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] μ[f | (↑ℱ : ι → MeasurableSpace Ω) i]
have refine : ∀ (t : Set Ω),
  MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
Tactic: refine condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le (ℱ.le i)
    (hτ.measurableSet_eq' i) fun t => ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
inst_7 : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
t : Set Ω
⊢ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
have rw : MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
Tactic: rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
inst_7 : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
t : Set Ω
rw : MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
⊢ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
have rw₁ : MeasurableSet (t ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
Tactic: rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : SecondCountableTopology ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_7 : SigmaFinite (μ.trim ⋯)
⊢ μ[f | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})] μ[f | hτ.measurableSpace]
have this : SigmaFinite (μ.trim sorry)
Tactic: have : SigmaFinite (μ.trim hτ.measurableSpace_le) :=
    sigmaFiniteTrim_mono _ (hτ.measurableSpace_min hσ ▸ inf_le_left)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : SecondCountableTopology ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_7 : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
⊢ μ[f | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})] μ[f | hτ.measurableSpace]
have refine : ∀ (t : Set Ω), MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t) ↔ MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t)
Tactic: refine (condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le
    (hτ.min hσ).measurableSpace_le (hτ.measurableSet_le_stopping_time hσ) fun t => ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : SecondCountableTopology ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_7 : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
t : Set Ω
⊢ MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t) ↔ MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t)
have rw : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω}) ↔ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})
Tactic: rw [Set.inter_comm _ t, hτ.measurableSet_inter_le_iff hσ]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : SecondCountableTopology ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_7 : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
t : Set Ω
rw : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω}) ↔ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})
⊢ MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t) ↔ MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t)
have rw₁ : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω}) ↔ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})
Tactic: rw [Set.inter_comm _ t, hτ.measurableSet_inter_le_iff hσ]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ IsProjectiveMeasureFamily (α := X) fun (I : Finset ι) ↦
    Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι)
have refine : ∀ (I J : Finset ι) (hJI : J ⊆ I) (s : (i : ↥J) → Set (X (↑i : ι))) (ms : ∀ (i : ↥J), MeasurableSet (s i)),
  Eq (α := ℝ≥0∞)
    ((Measure.map (restrict₂ (π := X) hJI)
            ((fun (I : Finset ι) ↦
                (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) :
                  Measure ((i : ↥I) → X (↑i : ι))))
              I) :
          (a : Set ((i : ↥J) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: refine fun I J hJI ↦ Measure.pi_eq (fun s ms ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (restrict₂ (π := X) hJI)
            ((fun (I : Finset ι) ↦
                (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) :
                  Measure ((i : ↥I) → X (↑i : ι))))
              I) :
          (a : Set ((i : ↥J) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
have simp_rw : Eq (α := ℝ≥0∞)
  (∏ x ∈ I,
    Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
      (fun (i : ↥I) ↦
        ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
          (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
      1 x)
  (∏ x ∈ J,
    Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ J))
      (fun (i : ↥J) ↦ ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i)) 1 x)
Tactic: simp_rw [Measure.map_apply (measurable_restrict₂ hJI) (.univ_pi ms), restrict₂_preimage hJI,
    Measure.pi_pi, prod_eq_prod_extend]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞)
    (∏ x ∈ I,
      Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
        (fun (i : ↥I) ↦
          ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
            (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
        1 x)
    (∏ x ∈ J,
      Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ J))
        (fun (i : ↥J) ↦ ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i)) 1 x)
have refine_1 : ∀ (x : ι) (hx : x ∈ I \ J),
  Eq (α := ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
      (fun (i : ↥I) ↦
        ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
          (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
      1 x)
    1
Tactic: refine (prod_subset_one_on_sdiff hJI (fun x hx ↦ ?_) (fun x hx ↦ ?_)).symm
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
refine_1 :
  ∀ (x : ι) (hx : x ∈ I \ J),
    Eq (α := ℝ≥0∞)
      (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
        (fun (i : ↥I) ↦
          ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
            (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
        1 x)
      1
⊢ Eq (α := ℝ≥0∞)
    (∏ x ∈ I,
      Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
        (fun (i : ↥I) ↦
          ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
            (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
        1 x)
    (∏ x ∈ J,
      Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ J))
        (fun (i : ↥J) ↦ ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i)) 1 x)
have refine_2 : ∀ (x : ι) (hx : x ∈ J),
  Eq (α := ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ J))
      (fun (i : ↥J) ↦ ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i)) 1 x)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
      (fun (i : ↥I) ↦
        ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
          (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
      1 x)
Tactic: refine (prod_subset_one_on_sdiff hJI (fun x hx ↦ ?_) (fun x hx ↦ ?_)).symm
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ I \ J
⊢ Eq (α := ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
      (fun (i : ↥I) ↦
        ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
          (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
      1 x)
    1
have refine_1 : Eq (α := ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x sorry) : ι) :
        Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x sorry) : ι))) :
      (a : Set (X (↑⟨x, sorry⟩ : ι))) → ℝ≥0∞)
    (if h : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x sorry) : ι) ∈ J then
      s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x sorry) : ι) h)
    else Set.univ))
  1
Tactic: rw [Function.extend_val_apply (mem_sdiff.1 hx).1, dif_neg (mem_sdiff.1 hx).2, measure_univ]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ I \ J
refine_1 :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) :
          Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι))) :
        (a : Set (X (↑⟨x, ⋯⟩ : ι))) → ℝ≥0∞)
      (if h : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) ∈ J then
        s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) h)
      else Set.univ))
    1
⊢ Eq (α := ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
      (fun (i : ↥I) ↦
        ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
          (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
      1 x)
    1
have refine_1₁ : Eq (α := ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x sorry) : ι) :
          Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x sorry) : ι))) :
        (a : Set (X (↑⟨x, sorry⟩ : ι))) → ℝ≥0∞)
      Set.univ :
    ℝ≥0∞)
  (1 : ℝ≥0∞)
Tactic: rw [Function.extend_val_apply (mem_sdiff.1 hx).1, dif_neg (mem_sdiff.1 hx).2, measure_univ]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ I \ J
refine_1 :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) :
          Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι))) :
        (a : Set (X (↑⟨x, ⋯⟩ : ι))) → ℝ≥0∞)
      (if h : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) ∈ J then
        s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) h)
      else Set.univ))
    1
refine_1₁ :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) :
            Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι))) :
          (a : Set (X (↑⟨x, ⋯⟩ : ι))) → ℝ≥0∞)
        Set.univ :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
      (fun (i : ↥I) ↦
        ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
          (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
      1 x)
    1
have refine_1₂ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [Function.extend_val_apply (mem_sdiff.1 hx).1, dif_neg (mem_sdiff.1 hx).2, measure_univ]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ J
⊢ Eq (α := ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ J))
      (fun (i : ↥J) ↦ ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i)) 1 x)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
      (fun (i : ↥I) ↦
        ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
          (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
      1 x)
have refine_2 : Eq (α := ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι) :
          Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι))) :
        (a : Set (X (↑⟨x, hx⟩ : ι))) → ℝ≥0∞)
      (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx)) :
    ℝ≥0∞)
  (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
      (fun (i : ↥I) ↦
        ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
          (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
      1 x :
    ℝ≥0∞)
Tactic: rw [Function.extend_val_apply hx, Function.extend_val_apply (hJI hx), dif_pos hx]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ J
refine_2 :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι) :
            Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι))) :
          (a : Set (X (↑⟨x, hx⟩ : ι))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx)) :
      ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
        (fun (i : ↥I) ↦
          ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
            (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
        1 x :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ J))
      (fun (i : ↥J) ↦ ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i)) 1 x)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
      (fun (i : ↥I) ↦
        ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
          (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
      1 x)
have refine_2₁ : Eq (α := ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι) :
          Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι))) :
        (a : Set (X (↑⟨x, hx⟩ : ι))) → ℝ≥0∞)
      (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx)) :
    ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x sorry) : ι) :
          Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x sorry) : ι))) :
        (a : Set (X (↑⟨x, sorry⟩ : ι))) → ℝ≥0∞)
      (if h : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x sorry) : ι) ∈ J then
        s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x sorry) : ι) h)
      else Set.univ) :
    ℝ≥0∞)
Tactic: rw [Function.extend_val_apply hx, Function.extend_val_apply (hJI hx), dif_pos hx]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ J
refine_2 :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι) :
            Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι))) :
          (a : Set (X (↑⟨x, hx⟩ : ι))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx)) :
      ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
        (fun (i : ↥I) ↦
          ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
            (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
        1 x :
      ℝ≥0∞)
refine_2₁ :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι) :
            Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι))) :
          (a : Set (X (↑⟨x, hx⟩ : ι))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx)) :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) :
            Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι))) :
          (a : Set (X (↑⟨x, ⋯⟩ : ι))) → ℝ≥0∞)
        (if h : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) ∈ J then
          s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) h)
        else Set.univ) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ J))
      (fun (i : ↥J) ↦ ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i)) 1 x)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
      (fun (i : ↥I) ↦
        ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
          (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
      1 x)
have refine_2₂ : Eq (α := ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι) :
          Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι))) :
        (a : Set (X (↑⟨x, hx⟩ : ι))) → ℝ≥0∞)
      (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx)) :
    ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x sorry) : ι) :
          Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x sorry) : ι))) :
        (a : Set (X (↑⟨x, sorry⟩ : ι))) → ℝ≥0∞)
      (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x sorry) : ι) hx)) :
    ℝ≥0∞)
Tactic: rw [Function.extend_val_apply hx, Function.extend_val_apply (hJI hx), dif_pos hx]