awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set (β × α)
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    (∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)) : (a : Set (β × α)) → ℝ≥0∞) s)
    (∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) : (a : Set (β × α)) → ℝ≥0∞) s)
⊢ Eq (α := ℝ≥0∞)
    ((sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)) : (a : Set (β × α)) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) : (a : Set (β × α)) → ℝ≥0∞) s :
      ℝ≥0∞)

Tactic:
rw [sum_apply _ hs, sum_apply _ hs]

Premises used: MeasureTheory.Measure.sum_apply
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set (β × α)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)) : (a : Set (β × α)) → ℝ≥0∞) s)
    (∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) : (a : Set (β × α)) → ℝ≥0∞) s)

Tactic:
((Equiv.prodComm ℕ ℕ).tsum_eq _).symm

Premises used: Equiv.prodComm, Equiv.tsum_eq, Nat, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set (β × α)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)) : (a : Set (β × α)) → ℝ≥0∞) s)
    (∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) : (a : Set (β × α)) → ℝ≥0∞) s)

Tactic:
exact ((Equiv.prodComm ℕ ℕ).tsum_eq _).symm

Premises used: Equiv.prodComm, Equiv.tsum_eq, Nat, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
⊢ Eq (α := Measure (β × α)) (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)))
    (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))

Tactic:
have : sum (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)))
       = sum (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) := by
    ext s hs
    rw [sum_apply _ hs, sum_apply _ hs]
    exact ((Equiv.prodComm ℕ ℕ).tsum_eq _).symm
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
this :
  Eq (α := Measure (β × α)) (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)))
    (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
rw :
  Eq (α := Measure (β × α)) (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
    (sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq ν p.1).prod (sfiniteSeq μ p.2))
⊢ map Prod.swap (μ.prod ν) = ν.prod μ

Tactic:
rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, prod_sum, prod_sum,
    map_sum measurable_swap.aemeasurable, this]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.map_sum, MeasureTheory.sum_sfiniteSeq, measurable_swap, MeasureTheory.Measure.prod_sum
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
this :
  Eq (α := Measure (β × α)) (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)))
    (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
e_f :
  Eq (α := ℕ × ℕ → Measure (β × α)) (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
    fun (p : ℕ × ℕ) ↦ (sfiniteSeq ν p.1).prod (sfiniteSeq μ p.2)
⊢ Eq (α := Measure (β × α)) (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
    (sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq ν p.1).prod (sfiniteSeq μ p.2))

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
this :
  Eq (α := Measure (β × α)) (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)))
    (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
e_f :
  ∀ (i : ℕ × ℕ), map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) = (sfiniteSeq ν i.1).prod (sfiniteSeq μ i.2)
⊢ Eq (α := ℕ × ℕ → Measure (β × α)) (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
    fun (p : ℕ × ℕ) ↦ (sfiniteSeq ν p.1).prod (sfiniteSeq μ p.2)

Tactic:
ext1 i
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
this :
  Eq (α := Measure (β × α)) (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)))
    (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
i : ℕ × ℕ
⊢ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) = (sfiniteSeq ν i.1).prod (sfiniteSeq μ i.2)

Tactic:
(prod_eq ?_).symm

Premises used: MeasureTheory.Measure.prod_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
this :
  Eq (α := Measure (β × α)) (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)))
    (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
i : ℕ × ℕ
e_f :
  ∀ (s : Set β) (t : Set α),
    MeasurableSet s →
      MeasurableSet t →
        (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) : (a : Set (β × α)) → ℝ≥0∞) (s ×ˢ t) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
            ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) = (sfiniteSeq ν i.1).prod (sfiniteSeq μ i.2)

Tactic:
refine (prod_eq ?_).symm

Premises used: MeasureTheory.Measure.prod_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
this :
  Eq (α := Measure (β × α)) (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)))
    (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
i : ℕ × ℕ
s : Set β
t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
e_f :
  ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1) : (a : Set (α × β)) → ℝ≥0∞) (Prod.swap ⁻¹' s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
e_f₁ :
  ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1) : (a : Set (α × β)) → ℝ≥0∞) (t ×ˢ s) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
e_f₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) : (a : Set (β × α)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp_rw [map_apply measurable_swap (hs.prod ht), preimage_swap_prod, prod_prod, mul_comm]

Premises used: MeasureTheory.Measure.map_apply, MeasurableSet.prod, MeasureTheory.Measure.prod_prod, measurable_swap, mul_comm, Set.preimage_swap_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
⊢ MeasurePreserving Prod.swap (μ.prod ν) (ν.prod μ)

Tactic:
⟨measurable_swap, prod_swap⟩

Premises used: MeasureTheory.MeasurePreserving.mk, MeasureTheory.Measure.prod_swap, measurable_swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
rw :
  ∫⁻ (x : β), (μ : (a : Set α) → ℝ≥0∞) (Prod.mk x ⁻¹' Prod.swap ⁻¹' s) ∂ν =
    ∫⁻ (y : β), (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, y)) ⁻¹' s) ∂ν
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s = ∫⁻ (y : β), (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, y)) ⁻¹' s) ∂ν

Tactic:
rw [← prod_swap, map_apply measurable_swap hs, prod_apply (measurable_swap hs)]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.prod_apply, MeasureTheory.Measure.prod_swap, measurable_swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), (μ : (a : Set α) → ℝ≥0∞) (Prod.mk x ⁻¹' Prod.swap ⁻¹' s) ∂ν =
    ∫⁻ (y : β), (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, y)) ⁻¹' s) ∂ν

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
p : α → β → Prop
h : MeasurableSet (α := α × β) {x : α × β | p x.1 x.2}
⊢ AEMeasurable Prod.swap (ν.prod μ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
p : α → β → Prop
h : MeasurableSet (α := α × β) {x : α × β | p x.1 x.2}
rw : (∀ᵐ (x : β × α) ∂ν.prod μ, p x.swap.1 x.swap.2) ↔ ∀ᵐ (x : β × α) ∂ν.prod μ, p x.2 x.1
⊢ (∀ᵐ (x : α × β) ∂μ.prod ν, p x.1 x.2) ↔ ∀ᵐ (x : β × α) ∂ν.prod μ, p x.2 x.1

Tactic:
rw [← prod_swap, ae_map_iff (by fun_prop) h]

Premises used: MeasureTheory.ae_map_iff, MeasureTheory.Measure.prod_swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
p : α → β → Prop
h : MeasurableSet (α := α × β) {x : α × β | p x.1 x.2}
⊢ (∀ᵐ (x : β × α) ∂ν.prod μ, p x.swap.1 x.swap.2) ↔ ∀ᵐ (x : β × α) ∂ν.prod μ, p x.2 x.1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : Ne (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet s μ

Tactic:
.right_of_prod ?_ ht

Premises used: MeasureTheory.NullMeasurableSet.right_of_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : Ne (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
refine : NullMeasurableSet (t ×ˢ s) (ν.prod μ)
⊢ NullMeasurableSet s μ

Tactic:
refine .right_of_prod ?_ ht
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : Ne (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
rw : NullMeasurableSet (Prod.swap ⁻¹' s ×ˢ t) (ν.prod μ)
⊢ NullMeasurableSet (t ×ˢ s) (ν.prod μ)

Tactic:
rw [← preimage_swap_prod]

Premises used: Set.preimage_swap_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : Ne (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet (Prod.swap ⁻¹' s ×ˢ t) (ν.prod μ)

Tactic:
h.preimage measurePreserving_swap.quasiMeasurePreserving

Premises used: MeasureTheory.NullMeasurableSet.preimage, MeasureTheory.MeasurePreserving.quasiMeasurePreserving, MeasureTheory.Measure.measurePreserving_swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : Ne (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet (Prod.swap ⁻¹' s ×ˢ t) (ν.prod μ)

Tactic:
exact h.preimage measurePreserving_swap.quasiMeasurePreserving

Premises used: MeasureTheory.NullMeasurableSet.preimage, MeasureTheory.MeasurePreserving.quasiMeasurePreserving, MeasureTheory.Measure.measurePreserving_swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
inst_4 : NeZero ν
s : Set α
h : NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν)
rwa rwa₁ rwa₂ rwa₃ : NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν)
⊢ NullMeasurableSet (SProd.sprod (β := Set β) s univ) (μ.prod ν)

Tactic:
rwa [prod_univ]

Premises used: Set.prod_univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
inst_4 : NeZero ν
s : Set α
⊢ NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν) ↔ NullMeasurableSet s μ

Tactic:
⟨.of_preimage_fst, (.preimage · quasiMeasurePreserving_fst)⟩

Premises used: MeasureTheory.NullMeasurableSet.of_preimage_fst, MeasureTheory.Measure.quasiMeasurePreserving_fst, MeasureTheory.NullMeasurableSet.preimage, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : NeZero ν
f : α → γ
⊢ NullMeasurable (f ∘ Prod.fst) (μ.prod ν) ↔ NullMeasurable f μ

Tactic:
forall₂_congr fun s _ ↦ nullMeasurableSet_preimage_fst (s := f ⁻¹' s)

Premises used: MeasureTheory.Measure.nullMeasurableSet_preimage_fst, forall₂_congr, MeasureTheory.NullMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ht : Ne (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔ NullMeasurableSet s μ ∧ NullMeasurableSet t ν

Tactic:
⟨fun h ↦ ⟨h.left_of_prod ht, h.right_of_prod hs⟩, fun ⟨hs, ht⟩ ↦ hs.prod ht⟩

Premises used: SProd.sprod, MeasureTheory.NullMeasurableSet, MeasureTheory.NullMeasurableSet.left_of_prod, MeasureTheory.Measure.prod, And.intro, Iff.intro, MeasureTheory.NullMeasurableSet.right_of_prod, MeasureTheory.NullMeasurableSet.prod, _private.0.MeasureTheory.Measure.nullMeasurableSet_prod_of_ne_zero.match_1
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
inl :
  ∀ (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
      NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
          Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
inr :
  ∀ (hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
      NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
          Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
    NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rcases eq_or_ne (μ s) 0 with hs | hs

Premises used: eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
    NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [NullMeasurableSet.of_null, *]

Premises used: MeasureTheory.NullMeasurableSet.of_null
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
inr :
  ∀ (ht : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
    NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
      NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
          Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
inr₁ :
  ∀ (ht : Ne (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
    NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
      NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
          Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
    NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rcases eq_or_ne (ν t) 0 with ht | ht

Premises used: eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ht : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
    NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [NullMeasurableSet.of_null, *]

Premises used: MeasureTheory.NullMeasurableSet.of_null
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ht : Ne (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
    NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [*, nullMeasurableSet_prod_of_ne_zero]

Premises used: MeasureTheory.Measure.nullMeasurableSet_prod_of_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : SFinite τ
h :
  ∀ (s : Set (α × β × γ)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((sum fun (p : ℕ × ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)) :
            (a : Set (α × β × γ)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((sum fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2)) :
            (a : Set (α × β × γ)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ Eq (α := Measure (α × β × γ))
    (sum fun (p : ℕ × ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)))
    (sum fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2)))

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : SFinite τ
s : Set (α × β × γ)
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    (∑' (c : (ℕ × ℕ) × ℕ),
      ((sfiniteSeq μ ((Equiv.prodAssoc ℕ ℕ ℕ : (a : (ℕ × ℕ) × ℕ) → ℕ × ℕ × ℕ) c).1).prod
            ((sfiniteSeq ν ((Equiv.prodAssoc ℕ ℕ ℕ : (a : (ℕ × ℕ) × ℕ) → ℕ × ℕ × ℕ) c).2.1).prod
              (sfiniteSeq τ ((Equiv.prodAssoc ℕ ℕ ℕ : (a : (ℕ × ℕ) × ℕ) → ℕ × ℕ × ℕ) c).2.2)) :
          (a : Set (α × β × γ)) → ℝ≥0∞)
        s)
    (∑' (i : (ℕ × ℕ) × ℕ),
      ((sfiniteSeq μ i.1.1).prod ((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2)) : (a : Set (α × β × γ)) → ℝ≥0∞) s)
⊢ Eq (α := ℝ≥0∞)
    ((sum fun (p : ℕ × ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)) :
          (a : Set (α × β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((sum fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2)) :
          (a : Set (α × β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [sum_apply _ hs, sum_apply _ hs, ← (Equiv.prodAssoc _ _ _).tsum_eq]

Premises used: Equiv.tsum_eq, MeasureTheory.Measure.sum_apply, Equiv.prodAssoc
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : SFinite τ
s : Set (α × β × γ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (∑' (c : (ℕ × ℕ) × ℕ),
      ((sfiniteSeq μ ((Equiv.prodAssoc ℕ ℕ ℕ : (a : (ℕ × ℕ) × ℕ) → ℕ × ℕ × ℕ) c).1).prod
            ((sfiniteSeq ν ((Equiv.prodAssoc ℕ ℕ ℕ : (a : (ℕ × ℕ) × ℕ) → ℕ × ℕ × ℕ) c).2.1).prod
              (sfiniteSeq τ ((Equiv.prodAssoc ℕ ℕ ℕ : (a : (ℕ × ℕ) × ℕ) → ℕ × ℕ × ℕ) c).2.2)) :
          (a : Set (α × β × γ)) → ℝ≥0∞)
        s)
    (∑' (i : (ℕ × ℕ) × ℕ),
      ((sfiniteSeq μ i.1.1).prod ((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2)) : (a : Set (α × β × γ)) → ℝ≥0∞) s)

Tactic:
simp only [Equiv.prodAssoc_apply]

Premises used: Equiv.prodAssoc_apply