awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
rw : HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) = μ i
rw₁ : HSMul.hSMul (α := ℝ≥0∞) 1 (μ i) = μ i
⊢ map (eval (β := α) i) (Measure.pi (α := α) μ) = μ i
have rw₂ : ∀ x ∈ Finset.erase Finset.univ i, Eq (α := ℝ≥0∞) ((μ x : (a : Set (α x)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: classical
  rw [Measure.pi_map_eval, Finset.prod_eq_one, one_smul]
  exact fun _ _ ↦ measure_univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
rw : HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) = μ i
rw₁ : HSMul.hSMul (α := ℝ≥0∞) 1 (μ i) = μ i
rw₂ : ∀ x ∈ Finset.erase Finset.univ i, Eq (α := ℝ≥0∞) ((μ x : (a : Set (α x)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ map (eval (β := α) i) (Measure.pi (α := α) μ) = μ i
have rw₃ : μ i = μ i
Tactic: classical
  rw [Measure.pi_map_eval, Finset.prod_eq_one, one_smul]
  exact fun _ _ ↦ measure_univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (Measure.pi (α := α) μ).restrict (Set.pi (α := α) univ fun (i : ι) ↦ s i) =
    Measure.pi (α := α) fun (i : ι) ↦ (μ i).restrict (s i)
have refine : ∀ (x : (i : ι) → Set (α i)) (h : ∀ (i : ι), MeasurableSet (x i)),
  Eq (α := ℝ≥0∞)
    (((Measure.pi (α := α) μ).restrict (Set.pi (α := α) univ fun (i : ι) ↦ s i) : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ x) :
      ℝ≥0∞)
    (∏ i : ι, ((μ i).restrict (s i) : (a : Set (α i)) → ℝ≥0∞) (x i) : ℝ≥0∞)
Tactic: refine (pi_eq fun _ h ↦ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
s x : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (x i)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.pi (α := α) μ).restrict (Set.pi (α := α) univ fun (i : ι) ↦ s i) : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ x) :
      ℝ≥0∞)
    (∏ i : ι, ((μ i).restrict (s i) : (a : Set (α i)) → ℝ≥0∞) (x i) : ℝ≥0∞)
have simp_rw : Eq (α := ℝ≥0∞)
  ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
      (Set.pi (α := α) univ x ∩ Set.pi (α := α) univ fun (i : ι) ↦ s i) :
    ℝ≥0∞)
  (∏ i : ι, ((μ i).restrict (s i) : (a : Set (α i)) → ℝ≥0∞) (x i) : ℝ≥0∞)
Tactic: simp_rw [restrict_apply (MeasurableSet.univ_pi h), restrict_apply (h _),
    ← Set.pi_inter_distrib, pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
s x : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (x i)
simp_rw :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ x ∩ Set.pi (α := α) univ fun (i : ι) ↦ s i) :
      ℝ≥0∞)
    (∏ i : ι, ((μ i).restrict (s i) : (a : Set (α i)) → ℝ≥0∞) (x i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.pi (α := α) μ).restrict (Set.pi (α := α) univ fun (i : ι) ↦ s i) : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ x) :
      ℝ≥0∞)
    (∏ i : ι, ((μ i).restrict (s i) : (a : Set (α i)) → ℝ≥0∞) (x i) : ℝ≥0∞)
have simp_rw₁ : Eq (α := ℝ≥0∞)
  ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
      (Set.pi (α := α) univ x ∩ Set.pi (α := α) univ fun (i : ι) ↦ s i) :
    ℝ≥0∞)
  (∏ x_1 : ι, (μ x_1 : (a : Set (α x_1)) → ℝ≥0∞) (x x_1 ∩ s x_1) : ℝ≥0∞)
Tactic: simp_rw [restrict_apply (MeasurableSet.univ_pi h), restrict_apply (h _),
    ← Set.pi_inter_distrib, pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
s x : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (x i)
simp_rw :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ x ∩ Set.pi (α := α) univ fun (i : ι) ↦ s i) :
      ℝ≥0∞)
    (∏ i : ι, ((μ i).restrict (s i) : (a : Set (α i)) → ℝ≥0∞) (x i) : ℝ≥0∞)
simp_rw₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ x ∩ Set.pi (α := α) univ fun (i : ι) ↦ s i) :
      ℝ≥0∞)
    (∏ x_1 : ι, (μ x_1 : (a : Set (α x_1)) → ℝ≥0∞) (x x_1 ∩ s x_1) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.pi (α := α) μ).restrict (Set.pi (α := α) univ fun (i : ι) ↦ s i) : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ x) :
      ℝ≥0∞)
    (∏ i : ι, ((μ i).restrict (s i) : (a : Set (α i)) → ℝ≥0∞) (x i) : ℝ≥0∞)
have simp_rw₂ : Eq (α := ℝ≥0∞)
  ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ fun (i : ι) ↦ x i ∩ s i) : ℝ≥0∞)
  (∏ x_1 : ι, (μ x_1 : (a : Set (α x_1)) → ℝ≥0∞) (x x_1 ∩ s x_1) : ℝ≥0∞)
Tactic: simp_rw [restrict_apply (MeasurableSet.univ_pi h), restrict_apply (h _),
    ← Set.pi_inter_distrib, pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
β : Option ι → Type u_4
inst_1 : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst_2 : ∀ (i : Option ι), SigmaFinite (μ i)
⊢ map (α := ((i : ι) → β (some i)) × β none)
      (⇑(MeasurableEquiv.symm (MeasurableEquiv.piOptionEquivProd β)) :
        (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i)
      (Measure.prod (Measure.pi (α := fun (i : ι) ↦ β (some i)) fun (i : ι) ↦ μ (some i)) (μ none)) =
    Measure.pi (α := β) μ
have refine : ∀ (s : (i : Option ι) → Set (β i)),
  (∀ (i : Option ι), MeasurableSet (s i)) →
    Eq (α := ℝ≥0∞)
      ((map (α := ((i : ι) → β (some i)) × β none)
              (⇑(MeasurableEquiv.symm (MeasurableEquiv.piOptionEquivProd β)) :
                (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i)
              (Measure.prod (Measure.pi (α := fun (i : ι) ↦ β (some i)) fun (i : ι) ↦ μ (some i)) (μ none)) :
            (a : Set ((i : Option ι) → β i)) → ℝ≥0∞)
          (Set.pi (α := β) univ s) :
        ℝ≥0∞)
      (∏ i : Option ι, (μ i : (a : Set (β i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: refine pi_eq (fun s _ ↦ ?_) |>.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
β : Option ι → Type u_4
inst_1 : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst_2 : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
h : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piOptionEquivProd β)
⊢ Eq (α := ℝ≥0∞)
    ((map (α := ((i : ι) → β (some i)) × β none)
            (⇑(MeasurableEquiv.symm (MeasurableEquiv.piOptionEquivProd β)) :
              (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i)
            (Measure.prod (Measure.pi (α := fun (i : ι) ↦ β (some i)) fun (i : ι) ↦ μ (some i)) (μ none)) :
          (a : Set ((i : Option ι) → β i)) → ℝ≥0∞)
        (Set.pi (α := β) univ s) :
      ℝ≥0∞)
    (∏ i : Option ι, (μ i : (a : Set (β i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have me : MeasurableEmbedding (α := ((i : ι) → β (some i)) × β none) (β := (i : Option ι) → β i)
  (⇑e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i)
Tactic: have me := MeasurableEquiv.measurableEmbedding e_meas
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
β : Option ι → Type u_4
inst_1 : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst_2 : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
h : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piOptionEquivProd β)
me :
  MeasurableEmbedding (α := ((i : ι) → β (some i)) × β none) (β := (i : Option ι) → β i)
    (⇑e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i)
⊢ (⇑e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) ⁻¹' Set.pi (α := β) univ s =
    SProd.sprod (α := Set ((i : ι) → β (some i))) (β := Set (β none))
      (Set.pi (α := fun (i : ι) ↦ β (some i)) univ fun (i : ι) ↦ s (some i)) (s none)
have h : ∀ (x : ((i : ι) → β (some i)) × β none),
  Membership.mem (γ := Set (((i : ι) → β (some i)) × β none))
      ((⇑e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) ⁻¹' Set.pi (α := β) univ s) x ↔
    x ∈
      SProd.sprod (α := Set ((i : ι) → β (some i))) (β := Set (β none))
        (Set.pi (α := fun (i : ι) ↦ β (some i)) univ fun (i : ι) ↦ s (some i)) (s none)
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
β : Option ι → Type u_4
inst_1 : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst_2 : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
h : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piOptionEquivProd β)
me :
  MeasurableEmbedding (α := ((i : ι) → β (some i)) × β none) (β := (i : Option ι) → β i)
    (⇑e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i)
x : ((i : ι) → β (some i)) × β none
⊢ Membership.mem (γ := Set (((i : ι) → β (some i)) × β none))
      ((⇑e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) ⁻¹' Set.pi (α := β) univ s) x ↔
    x ∈
      SProd.sprod (α := Set ((i : ι) → β (some i))) (β := Set (β none))
        (Set.pi (α := fun (i : ι) ↦ β (some i)) univ fun (i : ι) ↦ s (some i)) (s none)
have h : (∀ (i : Option ι),
    Membership.mem (α := β i) (s i)
      ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x i : β i)) ↔
  (∀ (i : ι), Membership.mem (γ := Set (β (some i))) (s (some i)) (x.1 i)) ∧
    Membership.mem (γ := Set (β none)) (s none) x.2
Tactic: simp only [mem_preimage, Set.mem_pi, mem_univ, forall_true_left, mem_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
β : Option ι → Type u_4
inst_1 : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst_2 : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
h : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piOptionEquivProd β)
me :
  MeasurableEmbedding (α := ((i : ι) → β (some i)) × β none) (β := (i : Option ι) → β i)
    (⇑e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i)
x : ((i : ι) → β (some i)) × β none
tauto tauto₁ :
  (∀ (i : Option ι),
      Membership.mem (α := β i) (s i)
        ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x i : β i)) →
    (∀ (i : ι), Membership.mem (γ := Set (β (some i))) (s (some i)) (x.1 i)) ∧
      Membership.mem (γ := Set (β none)) (s none) x.2
⊢ (∀ (i : Option ι),
      Membership.mem (α := β i) (s i)
        ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x i : β i)) →
    (∀ (i : ι), Membership.mem (γ := Set (β (some i))) (s (some i)) (x.1 i)) ∧
      Membership.mem (γ := Set (β none)) (s none) x.2
have left : (∀ (i : Option ι),
    Membership.mem (α := β i) (s i)
      ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x i : β i)) →
  ∀ (i : ι), Membership.mem (γ := Set (β (some i))) (s (some i)) (x.1 i)
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
β : Option ι → Type u_4
inst_1 : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst_2 : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
h : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piOptionEquivProd β)
me :
  MeasurableEmbedding (α := ((i : ι) → β (some i)) × β none) (β := (i : Option ι) → β i)
    (⇑e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i)
x : ((i : ι) → β (some i)) × β none
tauto tauto₁ :
  (∀ (i : Option ι),
      Membership.mem (α := β i) (s i)
        ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x i : β i)) →
    (∀ (i : ι), Membership.mem (γ := Set (β (some i))) (s (some i)) (x.1 i)) ∧
      Membership.mem (γ := Set (β none)) (s none) x.2
left :
  (∀ (i : Option ι),
      Membership.mem (α := β i) (s i)
        ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x i : β i)) →
    ∀ (i : ι), Membership.mem (γ := Set (β (some i))) (s (some i)) (x.1 i)
⊢ (∀ (i : Option ι),
      Membership.mem (α := β i) (s i)
        ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x i : β i)) →
    (∀ (i : ι), Membership.mem (γ := Set (β (some i))) (s (some i)) (x.1 i)) ∧
      Membership.mem (γ := Set (β none)) (s none) x.2
have right : (∀ (i : Option ι),
    Membership.mem (α := β i) (s i)
      ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x i : β i)) →
  Membership.mem (γ := Set (β none)) (s none) x.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
β : Option ι → Type u_4
inst_1 : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst_2 : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
h : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piOptionEquivProd β)
me :
  MeasurableEmbedding (α := ((i : ι) → β (some i)) × β none) (β := (i : Option ι) → β i)
    (⇑e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i)
x : ((i : ι) → β (some i)) × β none
⊢ (∀ (i : Option ι),
      Membership.mem (α := β i) (s i)
        ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x i : β i)) ↔
    (∀ (i : ι), Membership.mem (γ := Set (β (some i))) (s (some i)) (x.1 i)) ∧
      Membership.mem (γ := Set (β none)) (s none) x.2
have h : (∀ (i : ι), Membership.mem (γ := Set (β (some i))) (s (some i)) (x.1 i)) ∧
    Membership.mem (γ := Set (β none)) (s none) x.2 →
  ∀ (i : Option ι),
    Membership.mem (α := β i) (s i) ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x i : β i)
Tactic: refine ⟨by tauto, fun _ i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
β : Option ι → Type u_4
inst_1 : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst_2 : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
h : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piOptionEquivProd β)
me :
  MeasurableEmbedding (α := ((i : ι) → β (some i)) × β none) (β := (i : Option ι) → β i)
    (⇑e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i)
x : ((i : ι) → β (some i)) × β none
h_1 :
  (∀ (i : ι), Membership.mem (γ := Set (β (some i))) (s (some i)) (x.1 i)) ∧
    Membership.mem (γ := Set (β none)) (s none) x.2
i : Option ι
⊢ Membership.mem (α := β i) (s i) ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x i : β i)
have h : Membership.mem (α := β none) (γ := Set (β none)) (s none)
  ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x none : β none)
Tactic: rcases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
β : Option ι → Type u_4
inst_1 : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst_2 : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
h_1 : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piOptionEquivProd β)
me :
  MeasurableEmbedding (α := ((i : ι) → β (some i)) × β none) (β := (i : Option ι) → β i)
    (⇑e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i)
x : ((i : ι) → β (some i)) × β none
h_2 :
  (∀ (i : ι), Membership.mem (γ := Set (β (some i))) (s (some i)) (x.1 i)) ∧
    Membership.mem (γ := Set (β none)) (s none) x.2
i : Option ι
h :
  Membership.mem (α := β none) (γ := Set (β none)) (s none)
    ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x none : β none)
⊢ Membership.mem (α := β i) (s i) ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x i : β i)
have h₁ : ∀ (val : ι),
  Membership.mem (α := β (some val)) (γ := Set (β (some val))) (s (some val))
    ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x (some val) : β (some val))
Tactic: rcases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
β : Option ι → Type u_4
inst_1 : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst_2 : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
h : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piOptionEquivProd β)
me :
  MeasurableEmbedding (α := ((i : ι) → β (some i)) × β none) (β := (i : Option ι) → β i)
    (⇑e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i)
x : ((i : ι) → β (some i)) × β none
h_1 :
  (∀ (i : ι), Membership.mem (γ := Set (β (some i))) (s (some i)) (x.1 i)) ∧
    Membership.mem (γ := Set (β none)) (s none) x.2
⊢ Membership.mem (α := β none) (γ := Set (β none)) (s none)
    ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x none : β none)
have h : (∀ (i : ι), Membership.mem (γ := Set (β (some i))) (s (some i)) (x.1 i)) →
  Membership.mem (γ := Set (β none)) (s none) x.2 →
    Membership.mem (α := β none) (γ := Set (β none)) (s none)
      ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x none : β none)
Tactic: tauto
Cleared hypotheses: h_1
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
β : Option ι → Type u_4
inst_1 : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst_2 : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
h : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piOptionEquivProd β)
me :
  MeasurableEmbedding (α := ((i : ι) → β (some i)) × β none) (β := (i : Option ι) → β i)
    (⇑e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i)
x : ((i : ι) → β (some i)) × β none
h_1 :
  (∀ (i : ι), Membership.mem (γ := Set (β (some i))) (s (some i)) (x.1 i)) ∧
    Membership.mem (γ := Set (β none)) (s none) x.2
val : ι
⊢ Membership.mem (α := β (some val)) (γ := Set (β (some val))) (s (some val))
    ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x (some val) : β (some val))
have h : (∀ (i : ι), Membership.mem (γ := Set (β (some i))) (s (some i)) (x.1 i)) →
  Membership.mem (γ := Set (β none)) (s none) x.2 →
    Membership.mem (α := β (some val)) (γ := Set (β (some val))) (s (some val))
      ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x (some val) : β (some val))
Tactic: tauto
Cleared hypotheses: h_1
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
β : Option ι → Type u_4
inst_1 : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst_2 : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
h : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piOptionEquivProd β)
me :
  MeasurableEmbedding (α := ((i : ι) → β (some i)) × β none) (β := (i : Option ι) → β i)
    (⇑e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i)
⊢ Eq (α := ℝ≥0∞)
    ((map (α := ((i : ι) → β (some i)) × β none)
            (⇑(MeasurableEquiv.symm (MeasurableEquiv.piOptionEquivProd β)) :
              (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i)
            (Measure.prod (Measure.pi (α := fun (i : ι) ↦ β (some i)) fun (i : ι) ↦ μ (some i)) (μ none)) :
          (a : Set ((i : Option ι) → β i)) → ℝ≥0∞)
        (Set.pi (α := β) univ s) :
      ℝ≥0∞)
    (∏ i : Option ι, (μ i : (a : Set (β i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have this : (⇑e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) ⁻¹' Set.pi (α := β) univ s =
  SProd.sprod (α := Set ((i : ι) → β (some i))) (β := Set (β none))
    (Set.pi (α := fun (i : ι) ↦ β (some i)) univ fun (i : ι) ↦ s (some i)) (s none)
Tactic: have : e_meas ⁻¹' pi univ s = (pi univ (fun i ↦ s (some i))) ×ˢ (s none) := by
    ext x
    simp only [mem_preimage, Set.mem_pi, mem_univ, forall_true_left, mem_prod]
    refine ⟨by tauto, fun _ i ↦ ?_⟩
    rcases i <;> tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : ∀ (i : ι), NoAtoms (μ i)
f : (i : ι) → α i
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ Iio (f i)) =ᶠ[ae (Measure.pi (α := α) μ)] Iic f
have rw : (Set.pi (α := α) univ fun (i : ι) ↦ Iio (f i)) =ᶠ[ae (Measure.pi (α := α) μ)]
  Set.pi (α := α) univ fun (i : ι) ↦ Iic (f i)
Tactic: rw [← pi_univ_Iic]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : ∀ (i : ι), NoAtoms (μ i)
f : (i : ι) → α i
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ Ioi (f i)) =ᶠ[ae (Measure.pi (α := α) μ)] Ici f
have rw : (Set.pi (α := α) univ fun (i : ι) ↦ Ioi (f i)) =ᶠ[ae (Measure.pi (α := α) μ)]
  Set.pi (α := α) univ fun (i : ι) ↦ Ici (f i)
Tactic: rw [← pi_univ_Ici]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ Ioo (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)] Icc f g
have rw : (Set.pi (α := α) univ fun (i : ι) ↦ Ioo (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)]
  Set.pi (α := α) univ fun (i : ι) ↦ Icc (f i) (g i)
Tactic: rw [← pi_univ_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ Ioc (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)] Icc f g
have rw : (Set.pi (α := α) univ fun (i : ι) ↦ Ioc (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)]
  Set.pi (α := α) univ fun (i : ι) ↦ Icc (f i) (g i)
Tactic: rw [← pi_univ_Icc]