awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
hs :
  Membership.mem (γ := Set ((i : ι) → Set (X i)))
    (Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s}) s
t : (i : κ) → Set (Y i)
ht :
  Membership.mem (γ := Set ((i : κ) → Set (Y i)))
    (Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t}) t
hs₁ : ∀ (i : ι), IsClosed[inst i] (s i)
⊢ ∀ (i : κ), IsClosed[inst_3 i] (t i)

Tactic:
simp only [Set.mem_pi, mem_univ, mem_setOf_eq, forall_const] at hs ht

Premises used: Set.mem_pi, Set.mem_setOf_eq, Set.mem_univ, forall_const
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst i] (s i)
ht : ∀ (i : κ), IsClosed[inst_3 i] (t i)
⊢ ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (α := ℕ)
      (ofNNReal ∘ fun (x : ℕ) ↦
        HMul.hMul (α := ℝ≥0) (∏ c : ι, (⋯.apprSeq (F := s c) x : (a : X c) → ℝ≥0) (p.1 c))
          (∏ c : κ, (⋯.apprSeq (F := t c) x : (a : Y c) → ℝ≥0) (p.2 c)))
      atTop
      (𝓝
        (↑(HMul.hMul (α := ℝ≥0) (∏ c : ι, (s c).indicator (fun (x : X c) ↦ 1) (p.1 c))
              (∏ c : κ, (t c).indicator (fun (x : Y c) ↦ 1) (p.2 c))) :
          ℝ≥0∞))

Tactic:
have (p : (Π i, X i) × (Π j, Y j)) := ENNReal.continuous_coe.tendsto _ |>.comp <|
    (tendsto_finsetProd Finset.univ (fun i _ ↦ tendsto_pi_nhds.1
      (HasOuterApproxClosed.tendsto_apprSeq (hs i)) (p.1 i))).mul
    (tendsto_finsetProd Finset.univ (fun j _ ↦ tendsto_pi_nhds.1
      (HasOuterApproxClosed.tendsto_apprSeq (ht j)) (p.2 j)))
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
this_1 : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst i] (s i)
ht : ∀ (i : κ), IsClosed[inst_3 i] (t i)
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (α := ℕ)
      (ofNNReal ∘ fun (x : ℕ) ↦
        HMul.hMul (α := ℝ≥0) (∏ c : ι, (⋯.apprSeq (F := s c) x : (a : X c) → ℝ≥0) (p.1 c))
          (∏ c : κ, (⋯.apprSeq (F := t c) x : (a : Y c) → ℝ≥0) (p.2 c)))
      atTop
      (𝓝
        (↑(HMul.hMul (α := ℝ≥0) (∏ c : ι, (s c).indicator (fun (x : X c) ↦ 1) (p.1 c))
              (∏ c : κ, (t c).indicator (fun (x : Y c) ↦ 1) (p.2 c))) :
          ℝ≥0∞))
x : (i : ι) → X i
pos : ∀ (hy : x ∈ Set.pi (α := X) univ s), Eq (α := ℝ≥0) (∏ x_1 : ι, if x x_1 ∈ s x_1 then 1 else 0) 1
neg : ∀ (hy : x ∉ Set.pi (α := X) univ s), Eq (α := ℝ≥0) (∏ x_1 : ι, if x x_1 ∈ s x_1 then 1 else 0) 0
⊢ Eq (α := ℝ≥0) (∏ x_1 : ι, if x x_1 ∈ s x_1 then 1 else 0) (if x ∈ Set.pi (α := X) univ s then 1 else 0)

Tactic:
split_ifs with hy
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
this_1 : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst i] (s i)
ht : ∀ (i : κ), IsClosed[inst_3 i] (t i)
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (α := ℕ)
      (ofNNReal ∘ fun (x : ℕ) ↦
        HMul.hMul (α := ℝ≥0) (∏ c : ι, (⋯.apprSeq (F := s c) x : (a : X c) → ℝ≥0) (p.1 c))
          (∏ c : κ, (⋯.apprSeq (F := t c) x : (a : Y c) → ℝ≥0) (p.2 c)))
      atTop
      (𝓝
        (↑(HMul.hMul (α := ℝ≥0) (∏ c : ι, (s c).indicator (fun (x : X c) ↦ 1) (p.1 c))
              (∏ c : κ, (t c).indicator (fun (x : Y c) ↦ 1) (p.2 c))) :
          ℝ≥0∞))
x : (i : ι) → X i
hy : x ∈ Set.pi (α := X) univ s
⊢ ∀ (i : ι), x i ∈ s i

Tactic:
simp only [Set.mem_pi, mem_univ, forall_const] at hy

Premises used: Set.mem_pi, Set.mem_univ, forall_const
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
this_1 : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst i] (s i)
ht : ∀ (i : κ), IsClosed[inst_3 i] (t i)
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (α := ℕ)
      (ofNNReal ∘ fun (x : ℕ) ↦
        HMul.hMul (α := ℝ≥0) (∏ c : ι, (⋯.apprSeq (F := s c) x : (a : X c) → ℝ≥0) (p.1 c))
          (∏ c : κ, (⋯.apprSeq (F := t c) x : (a : Y c) → ℝ≥0) (p.2 c)))
      atTop
      (𝓝
        (↑(HMul.hMul (α := ℝ≥0) (∏ c : ι, (s c).indicator (fun (x : X c) ↦ 1) (p.1 c))
              (∏ c : κ, (t c).indicator (fun (x : Y c) ↦ 1) (p.2 c))) :
          ℝ≥0∞))
x : (i : ι) → X i
hy : ∀ (i : ι), x i ∈ s i
⊢ ∀ (x_1 : ι), Membership.mem (γ := Finset ι) Finset.univ x_1 → Eq (α := ℝ≥0) (if x x_1 ∈ s x_1 then 1 else 0) 1

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
this_1 : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst i] (s i)
ht : ∀ (i : κ), IsClosed[inst_3 i] (t i)
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (α := ℕ)
      (ofNNReal ∘ fun (x : ℕ) ↦
        HMul.hMul (α := ℝ≥0) (∏ c : ι, (⋯.apprSeq (F := s c) x : (a : X c) → ℝ≥0) (p.1 c))
          (∏ c : κ, (⋯.apprSeq (F := t c) x : (a : Y c) → ℝ≥0) (p.2 c)))
      atTop
      (𝓝
        (↑(HMul.hMul (α := ℝ≥0) (∏ c : ι, (s c).indicator (fun (x : X c) ↦ 1) (p.1 c))
              (∏ c : κ, (t c).indicator (fun (x : Y c) ↦ 1) (p.2 c))) :
          ℝ≥0∞))
x : (i : ι) → X i
hy : ∀ (i : ι), x i ∈ s i
⊢ Eq (α := ℝ≥0) (∏ x_1 : ι, if x x_1 ∈ s x_1 then 1 else 0) 1

Tactic:
exact Finset.prod_eq_one (by simpa)

Premises used: Finset.prod_eq_one
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
this_1 : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst i] (s i)
ht : ∀ (i : κ), IsClosed[inst_3 i] (t i)
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (α := ℕ)
      (ofNNReal ∘ fun (x : ℕ) ↦
        HMul.hMul (α := ℝ≥0) (∏ c : ι, (⋯.apprSeq (F := s c) x : (a : X c) → ℝ≥0) (p.1 c))
          (∏ c : κ, (⋯.apprSeq (F := t c) x : (a : Y c) → ℝ≥0) (p.2 c)))
      atTop
      (𝓝
        (↑(HMul.hMul (α := ℝ≥0) (∏ c : ι, (s c).indicator (fun (x : X c) ↦ 1) (p.1 c))
              (∏ c : κ, (t c).indicator (fun (x : Y c) ↦ 1) (p.2 c))) :
          ℝ≥0∞))
x : (i : ι) → X i
hy : x ∉ Set.pi (α := X) univ s
⊢ Eq (α := ℝ≥0) (∏ x_1 : ι, if x x_1 ∈ s x_1 then 1 else 0) 0

Tactic:
simpa [Finset.prod_eq_zero_iff] using hy

Premises used: Finset.prod_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
this_1 : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst i] (s i)
ht : ∀ (i : κ), IsClosed[inst_3 i] (t i)
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (α := ℕ)
      (ofNNReal ∘ fun (x : ℕ) ↦
        HMul.hMul (α := ℝ≥0) (∏ c : ι, (⋯.apprSeq (F := s c) x : (a : X c) → ℝ≥0) (p.1 c))
          (∏ c : κ, (⋯.apprSeq (F := t c) x : (a : Y c) → ℝ≥0) (p.2 c)))
      atTop
      (𝓝
        (↑(HMul.hMul (α := ℝ≥0) (∏ c : ι, (s c).indicator (fun (x : X c) ↦ 1) (p.1 c))
              (∏ c : κ, (t c).indicator (fun (x : Y c) ↦ 1) (p.2 c))) :
          ℝ≥0∞))
⊢ ∀ (x : (i : ι) → X i),
    Eq (α := ℝ≥0) (∏ i : ι, (s i).indicator (fun (x : X i) ↦ 1) (x i)) ((Set.pi (α := X) univ s).indicator 1 x)

Tactic:
have hp1 (x : Π i, X i) : ∏ i, (s i).indicator (fun _ ↦ (1 : ℝ≥0)) (x i) =
      (Set.univ.pi s).indicator 1 x := by
    simp only [Set.indicator, Set.mem_pi, mem_univ, forall_const, Pi.ofNat_apply]
    split_ifs with hy
    · simp only [Set.mem_pi, mem_univ, forall_const] at hy
      exact Finset.prod_eq_one (by simpa)
    · simpa [Finset.prod_eq_zero_iff] using hy
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
this_1 : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst i] (s i)
ht : ∀ (i : κ), IsClosed[inst_3 i] (t i)
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (α := ℕ)
      (ofNNReal ∘ fun (x : ℕ) ↦
        HMul.hMul (α := ℝ≥0) (∏ c : ι, (⋯.apprSeq (F := s c) x : (a : X c) → ℝ≥0) (p.1 c))
          (∏ c : κ, (⋯.apprSeq (F := t c) x : (a : Y c) → ℝ≥0) (p.2 c)))
      atTop
      (𝓝
        (↑(HMul.hMul (α := ℝ≥0) (∏ c : ι, (s c).indicator (fun (x : X c) ↦ 1) (p.1 c))
              (∏ c : κ, (t c).indicator (fun (x : Y c) ↦ 1) (p.2 c))) :
          ℝ≥0∞))
hp1 :
  ∀ (x : (i : ι) → X i),
    Eq (α := ℝ≥0) (∏ i : ι, (s i).indicator (fun (x : X i) ↦ 1) (x i)) ((Set.pi (α := X) univ s).indicator 1 x)
y : (j : κ) → Y j
pos : ∀ (hy : y ∈ Set.pi (α := Y) univ t), Eq (α := ℝ≥0) (∏ x : κ, if y x ∈ t x then 1 else 0) 1
neg : ∀ (hy : y ∉ Set.pi (α := Y) univ t), Eq (α := ℝ≥0) (∏ x : κ, if y x ∈ t x then 1 else 0) 0
⊢ Eq (α := ℝ≥0) (∏ x : κ, if y x ∈ t x then 1 else 0) (if y ∈ Set.pi (α := Y) univ t then 1 else 0)

Tactic:
split_ifs with hy