awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
u : Set Ω
ht_1 : MeasurableSet u
hu : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} u
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} uᶜ

Tactic:
exact hu.compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
f : ℕ → Set Ω
hs_1 : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (f n)
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (⋃ (i : ℕ), f i)

Tactic:
.iUnion hf

Premises used: MeasurableSet, Set.Mem, setOf, MeasurableSet.iUnion
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
f : ℕ → Set Ω
hs_1 : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (f n)
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (⋃ (i : ℕ), f i)

Tactic:
exact .iUnion hf
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s'
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
refine_1 :
  ∀ (t : Set Ω) (ht : Membership.mem (γ := Set (Set Ω)) {s} t),
    MeasurableSet t → Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t
refine_1₁ : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} ∅
refine_1₂ :
  ∀ (u : Set Ω),
    MeasurableSet u →
      ∀ (hu : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} u),
        Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} uᶜ
refine_1₃ :
  ∀ (f : ℕ → Set Ω),
    (∀ (n : ℕ), MeasurableSet (f n)) →
      ∀ (hf : ∀ (n : ℕ), Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (f n)),
        Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (⋃ (i : ℕ), f i)
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s'

Tactic:
induction s', hs' using generateFrom_induction with
    | hC t ht => exact ht ▸ hs
    | empty => exact @MeasurableSet.empty _ m₁
    | compl u _ hu => exact hu.compl
    | iUnion f _ hf => exact .iUnion hf

Premises used: MeasurableSet.empty, Compl.compl, Set.iUnion
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s_1 t : Set Ω
hs_1 : MeasurableSet s_1
ht : MeasurableSet t
s' t' : Set Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s'
s : Set Ω
hs : Membership.mem (γ := Set (Set Ω)) {t} s
ht_1 : MeasurableSet s
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s

Tactic:
hs ▸ ht

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s_1 t : Set Ω
hs_1 : MeasurableSet s_1
ht : MeasurableSet t
s' t' : Set Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s'
s : Set Ω
hs : Membership.mem (γ := Set (Set Ω)) {t} s
ht_1 : MeasurableSet s
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s

Tactic:
exact hs ▸ ht
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s'
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} ∅

Tactic:
@MeasurableSet.empty _ m₂

Premises used: MeasurableSet, MeasurableSet.empty, Set.Mem, setOf
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s'
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} ∅

Tactic:
exact @MeasurableSet.empty _ m₂

Premises used: MeasurableSet.empty
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s'
u : Set Ω
ht_1 : MeasurableSet u
hu : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} u
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} uᶜ

Tactic:
hu.compl

Premises used: MeasurableSet, Set.Mem, setOf, MeasurableSet.compl
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s'
u : Set Ω
ht_1 : MeasurableSet u
hu : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} u
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} uᶜ

Tactic:
exact hu.compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s'
f : ℕ → Set Ω
hs_1 : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (f n)
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (⋃ (i : ℕ), f i)

Tactic:
.iUnion hf

Premises used: MeasurableSet, Set.Mem, setOf, MeasurableSet.iUnion
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s'
f : ℕ → Set Ω
hs_1 : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (f n)
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (⋃ (i : ℕ), f i)

Tactic:
exact .iUnion hf
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s'
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
refine_2 :
  ∀ (s : Set Ω) (hs : Membership.mem (γ := Set (Set Ω)) {t} s),
    MeasurableSet s → Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s
refine_2₁ : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} ∅
refine_2₂ :
  ∀ (u : Set Ω),
    MeasurableSet u →
      ∀ (hu : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} u),
        Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} uᶜ
refine_2₃ :
  ∀ (f : ℕ → Set Ω),
    (∀ (n : ℕ), MeasurableSet (f n)) →
      ∀ (hf : ∀ (n : ℕ), Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (f n)),
        Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (⋃ (i : ℕ), f i)
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'

Tactic:
induction t', ht' using generateFrom_induction with
    | hC s hs => exact hs ▸ ht
    | empty => exact @MeasurableSet.empty _ m₂
    | compl u _ hu => exact hu.compl
    | iUnion f _ hf => exact .iUnion hf

Premises used: MeasurableSet.empty, Compl.compl, Set.iUnion
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ _m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
⊢ Indep m₁ m₂ κ μ ↔ ∀ (s t : Set Ω), MeasurableSet s → MeasurableSet t → IndepSet s t κ μ

Tactic:
⟨fun h => fun _s _t hs ht => h.indepSet_of_measurableSet hs ht, fun h s t hs ht =>
    h s t hs ht s t (measurableSet_generateFrom (Set.mem_singleton s))
      (measurableSet_generateFrom (Set.mem_singleton t))⟩

Premises used: Set.mem_singleton, MeasurableSpace.measurableSet_generateFrom, Iff.intro, ProbabilityTheory.Kernel.Indep.indepSet_of_measurableSet
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
β : ι → Type u_10
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
⊢ iIndepFun (β := β) f κ 0

Tactic:
simp [iIndepFun]

Premises used: ProbabilityTheory.Kernel.iIndepFun
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
γ : Type u_6
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
β : Type u_10
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : Ω → β
g : Ω → γ
⊢ IndepFun f g κ 0

Tactic:
simp [IndepFun]

Premises used: ProbabilityTheory.Kernel.IndepFun
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
γ : Type u_6
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
β : Type u_10
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : Ω → β
g : Ω → γ
⊢ IndepFun (mΩ := _mΩ) f g 0 μ

Tactic:
simp [IndepFun]

Premises used: ProbabilityTheory.Kernel.IndepFun
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
β : ι → Type u_10
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
⊢ iIndepFun (β := β) f κ μ ↔ iIndepFun (β := β) f η μ

Tactic:
iIndep_congr h

Premises used: ProbabilityTheory.Kernel.iIndep_congr, ProbabilityTheory.Kernel.iIndepFun
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
γ : Type u_6
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
β : Type u_10
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : Ω → β
g : Ω → γ
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
⊢ IndepFun f g κ μ ↔ IndepFun f g η μ

Tactic:
indep_congr h

Premises used: ProbabilityTheory.Kernel.IndepFun, ProbabilityTheory.Kernel.indep_congr
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Subsingleton ι
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsMarkovKernel κ
⊢ iIndepFun (β := β) f κ μ

Tactic:
simp [iIndepFun]

Premises used: ProbabilityTheory.Kernel.iIndepFun
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : (x : ι) → Ω → β x
hf : iIndepFun (β := β) f κ μ
⊢ iIndep (fun (x : ι) ↦ MeasurableSpace.comap (f x) (mβ x)) κ μ

Tactic:
hf

Premises used: ProbabilityTheory.Kernel.iIndepFun
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : (x : ι) → Ω → β x
h : iIndepFun (β := β) f κ μ
⊢ ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := Ω) (m0 := _mΩ) ((κ : (a : α) → Measure Ω) a)

Tactic:
h.iIndep.ae_isProbabilityMeasure

Premises used: ProbabilityTheory.Kernel.iIndepFun.iIndep, ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
S : Finset ι
f : (x : ι) → Ω → β x
hf : iIndepFun (β := β) f κ μ
hs : ∀ i ∈ S, MeasurableSet (s i)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, s i) : ENNReal)
      (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (s i) : ENNReal)

Tactic:
hf.iIndep.meas_biInter hs

Premises used: ProbabilityTheory.Kernel.iIndep.meas_biInter, ProbabilityTheory.Kernel.iIndepFun.iIndep
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
f : (x : ι) → Ω → β x
inst : Fintype ι
hf : iIndepFun (β := β) f κ μ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), s i) : ENNReal)
      (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (s i) : ENNReal)

Tactic:
hf.iIndep.meas_iInter hs

Premises used: ProbabilityTheory.Kernel.iIndepFun.iIndep, ProbabilityTheory.Kernel.iIndep.meas_iInter
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
γ : Type u_6
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_10
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
hfg : IndepFun f g κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)

Tactic:
hfg _ _ hs ht
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : (x : ι) → Ω → β x
ι' : Type u_9
g : ι' → ι
hg : Function.Injective g
h : iIndepFun (β := β) f κ μ
⊢ iIndepFun (β := fun (i : ι') ↦ β (g i)) (fun (i : ι') ↦ f (g i)) κ μ

Tactic:
iIndep.precomp hg h

Premises used: ProbabilityTheory.Kernel.iIndepFun, ProbabilityTheory.Kernel.iIndep.precomp
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : (x : ι) → Ω → β x
ι' : Type u_9
g : ι' → ι
hg : Function.Surjective g
h : iIndepFun (β := fun (i : ι') ↦ β (g i)) (fun (i : ι') ↦ f (g i)) κ μ
⊢ iIndepFun (β := β) f κ μ

Tactic:
iIndep.of_precomp hg h

Premises used: ProbabilityTheory.Kernel.iIndep.of_precomp, ProbabilityTheory.Kernel.iIndepFun
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : (x : ι) → Ω → β x
ι' : Type u_9
g : ι' → ι
hg : Function.Bijective g
⊢ iIndepFun (β := fun (i : ι') ↦ β (g i)) (fun (i : ι') ↦ f (g i)) κ μ ↔ iIndepFun (β := β) f κ μ

Tactic:
⟨.of_precomp hg.surjective, .precomp hg.injective⟩

Premises used: Function.Bijective.injective, ProbabilityTheory.Kernel.iIndepFun.of_precomp, ProbabilityTheory.Kernel.iIndepFun.precomp, Function.Bijective.surjective, Iff.intro
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf_Indep : iIndepFun (β := β) f κ μ
i j : ι
hij : i ≠ j
⊢ IndepFun (f i) (f j) κ μ

Tactic:
hf_Indep.indep hij

Premises used: ProbabilityTheory.Kernel.IndepFun, ProbabilityTheory.Kernel.iIndep.indep
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mp :
  IndepFun f g κ μ →
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          ∀ᵐ (a : α) ∂μ,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
              HMul.hMul (α := ENNReal) (β := ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)
mpr :
  (∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          ∀ᵐ (a : α) ∂μ,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
              HMul.hMul (α := ENNReal) (β := ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)) →
    IndepFun f g κ μ
⊢ IndepFun f g κ μ ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          ∀ᵐ (a : α) ∂μ,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
              HMul.hMul (α := ENNReal) (β := ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)

Tactic:
constructor
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
h : IndepFun f g κ μ
⊢ ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        ∀ᵐ (a : α) ∂μ,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ENNReal) (β := ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)

Tactic:
fun s t hs ht => h (f ⁻¹' s) (g ⁻¹' t) ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩

Premises used: Set.preimage, And.intro, Exists.intro, rfl
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
h : IndepFun f g κ μ
⊢ ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        ∀ᵐ (a : α) ∂μ,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ENNReal) (β := ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)

Tactic:
refine fun s t hs ht => h (f ⁻¹' s) (g ⁻¹' t) ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩

Premises used: Set.preimage, And.intro, Exists.intro, rfl
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        ∀ᵐ (a : α) ∂μ,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ENNReal) (β := ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)

Tactic:
h s t hs ht
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        ∀ᵐ (a : α) ∂μ,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ENNReal) (β := ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)

Tactic:
exact h s t hs ht
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
⊢ iIndepFun (β := β) f κ μ ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
      ∀ᵐ (a : α) ∂μ,
        Eq (α := ENNReal)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
          (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)

Tactic:
⟨fun h S sets h_meas => h _ fun i hi_mem => ⟨sets i, h_meas i hi_mem, rfl⟩, ?_⟩

Premises used: And.intro, Iff.intro, Exists.intro, rfl