awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
I : Set ι
s t : (i : ι) → Set (α i)
h : ∀ i ∈ I, s i =ᶠ[ae (μ i)] t i
⊢ I.pi (α := α) s =ᶠ[ae (Measure.pi (α := α) μ)] I.pi (α := α) t

Tactic:
(ae_le_set_pi fun i hi => (h i hi).le).antisymm (ae_le_set_pi fun i hi => (h i hi).symm.le)

Premises used: MeasureTheory.Measure.ae_le_set_pi, Filter.EventuallyEq.le, Filter.EventuallyLE.antisymm, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 (α := β) μ

Tactic:
pi_eq (fun s _ ↦ ?_) |>.symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
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∞)
⊢ 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 (α := β) μ

Tactic:
refine pi_eq (fun s _ ↦ ?_) |>.symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 β)
⊢ 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
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
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)
⊢ (⇑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:
ext x
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 :
  (∀ (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
⊢ 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:
simp only [mem_preimage, Set.mem_pi, mem_univ, forall_true_left, mem_prod]

Premises used: forall_true_left, Set.mem_pi, Set.mem_prod, Set.mem_univ, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
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
left₁ left₂ 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)
right₁ right₂ 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
left₄ left₅ 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)
right₄ right₅ 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
left₇ 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)
right₇ 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
⊢ (∀ (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:
tauto
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 :
  (∀ (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 : 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:
refine ⟨by tauto, fun _ i ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
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))
⊢ Membership.mem (α := β i) (s i) ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x i : β i)

Tactic:
rcases i
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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
h h₁ 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)
⊢ Membership.mem (α := β none) (γ := Set (β none)) (s none)
    ((e_meas : (a : ((i : ι) → β (some i)) × β none) → (i : Option ι) → β i) x none : β none)

Tactic:
tauto
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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
val : ι
h h₁ h₂ h₃ h₄ h₅ h₆ 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))
⊢ 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
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)

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
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
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)
⊢ 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:
simp only [e_meas, me.map_apply, univ_option, Finset.prod_insertNone, this,
    prod_prod, pi_pi, mul_comm]

Premises used: MeasureTheory.Measure.prod_prod, MeasurableEmbedding.map_apply, Finset.prod_insertNone, mul_comm, univ_option, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
s : Set ι
f : (i : ι) → α i
⊢ (s.pi (α := α) fun (i : ι) ↦ Iio (f i)) =ᶠ[ae (Measure.pi (α := α) μ)] s.pi (α := α) fun (i : ι) ↦ Iic (f i)

Tactic:
ae_eq_set_pi fun _ _ => Iio_ae_eq_Iic

Premises used: MeasureTheory.Measure.ae_eq_set_pi, MeasureTheory.Iio_ae_eq_Iic
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
s : Set ι
f : (i : ι) → α i
⊢ (s.pi (α := α) fun (i : ι) ↦ Ioi (f i)) =ᶠ[ae (Measure.pi (α := α) μ)] s.pi (α := α) fun (i : ι) ↦ Ici (f i)

Tactic:
ae_eq_set_pi fun _ _ => Ioi_ae_eq_Ici

Premises used: MeasureTheory.Ioi_ae_eq_Ici, MeasureTheory.Measure.ae_eq_set_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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
rw :
  (Set.pi (α := α) univ fun (i : ι) ↦ Iio (f i)) =ᶠ[ae (Measure.pi (α := α) μ)]
    Set.pi (α := α) univ fun (i : ι) ↦ Iic (f i)
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ Iio (f i)) =ᶠ[ae (Measure.pi (α := α) μ)] Iic f

Tactic:
rw [← pi_univ_Iic]

Premises used: Set.pi_univ_Iic
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 (α := α) μ)]
    Set.pi (α := α) univ fun (i : ι) ↦ Iic (f i)

Tactic:
pi_Iio_ae_eq_pi_Iic

Premises used: MeasureTheory.Measure.pi_Iio_ae_eq_pi_Iic
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 (α := α) μ)]
    Set.pi (α := α) univ fun (i : ι) ↦ Iic (f i)

Tactic:
exact pi_Iio_ae_eq_pi_Iic

Premises used: MeasureTheory.Measure.pi_Iio_ae_eq_pi_Iic
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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
rw :
  (Set.pi (α := α) univ fun (i : ι) ↦ Ioi (f i)) =ᶠ[ae (Measure.pi (α := α) μ)]
    Set.pi (α := α) univ fun (i : ι) ↦ Ici (f i)
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ Ioi (f i)) =ᶠ[ae (Measure.pi (α := α) μ)] Ici f

Tactic:
rw [← pi_univ_Ici]

Premises used: Set.pi_univ_Ici
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 (α := α) μ)]
    Set.pi (α := α) univ fun (i : ι) ↦ Ici (f i)

Tactic:
pi_Ioi_ae_eq_pi_Ici

Premises used: MeasureTheory.Measure.pi_Ioi_ae_eq_pi_Ici
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 (α := α) μ)]
    Set.pi (α := α) univ fun (i : ι) ↦ Ici (f i)

Tactic:
exact pi_Ioi_ae_eq_pi_Ici

Premises used: MeasureTheory.Measure.pi_Ioi_ae_eq_pi_Ici
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
s : Set ι
f g : (i : ι) → α i
⊢ (s.pi (α := α) fun (i : ι) ↦ Ioo (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)]
    s.pi (α := α) fun (i : ι) ↦ Icc (f i) (g i)

Tactic:
ae_eq_set_pi fun _ _ => Ioo_ae_eq_Icc

Premises used: MeasureTheory.Ioo_ae_eq_Icc, MeasureTheory.Measure.ae_eq_set_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
s : Set ι
f g : (i : ι) → α i
⊢ (s.pi (α := α) fun (i : ι) ↦ Ioo (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)]
    s.pi (α := α) fun (i : ι) ↦ Ioc (f i) (g i)

Tactic:
ae_eq_set_pi fun _ _ => Ioo_ae_eq_Ioc

Premises used: MeasureTheory.Ioo_ae_eq_Ioc, MeasureTheory.Measure.ae_eq_set_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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
rw :
  (Set.pi (α := α) univ fun (i : ι) ↦ Ioo (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)]
    Set.pi (α := α) univ fun (i : ι) ↦ Icc (f i) (g i)
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ Ioo (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)] Icc f g

Tactic:
rw [← pi_univ_Icc]

Premises used: Set.pi_univ_Icc
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 (α := α) μ)]
    Set.pi (α := α) univ fun (i : ι) ↦ Icc (f i) (g i)

Tactic:
pi_Ioo_ae_eq_pi_Icc

Premises used: MeasureTheory.Measure.pi_Ioo_ae_eq_pi_Icc
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 (α := α) μ)]
    Set.pi (α := α) univ fun (i : ι) ↦ Icc (f i) (g i)

Tactic:
exact pi_Ioo_ae_eq_pi_Icc

Premises used: MeasureTheory.Measure.pi_Ioo_ae_eq_pi_Icc