awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ π i
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
      (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
h s hf
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
⊢ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (fun (x : ι) ↦ (univ : Set Ω)) i ∈ π i

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
h₁ :
  ∀ (a : α)
    (ha :
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
            (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), univ) :
          ℝ≥0∞)
        (∏ i ∈ ∅, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)),
    IsProbabilityMeasure.{u_2} (α := Ω) (m0 := _mΩ) ((κ : (a : α) → Measure Ω) a)
⊢ ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := Ω) (m0 := _mΩ) ((κ : (a : α) → Measure Ω) a)

Tactic:
filter_upwards [h.meas_biInter ∅ (f := fun _ ↦ Set.univ) (by simp)] with a ha

Premises used: ProbabilityTheory.Kernel.iIndepSets.meas_biInter, EmptyCollection.emptyCollection
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
a : α
ha :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), univ) :
      ℝ≥0∞)
    (∏ i ∈ ∅, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simpa using ha
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
a : α
ha :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), univ) :
      ℝ≥0∞)
    (∏ i ∈ ∅, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ IsProbabilityMeasure.{u_2} (α := Ω) (m0 := _mΩ) ((κ : (a : α) → Measure Ω) a)

Tactic:
exact ⟨by simpa using ha⟩
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
s : ι → Set Ω
inst : Fintype ι
h : iIndepSets π κ μ
hs : ∀ (i : ι), s i ∈ π i
a : α
ha :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) Finset.univ i), s i) :
      ℝ≥0∞)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
simp [← ha]
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
s : ι → Set Ω
inst : Fintype ι
h : iIndepSets π κ μ
hs : ∀ (i : ι), s i ∈ π i
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α |
              (fun (a : α) ↦
                  Eq (α := ℝ≥0∞)
                    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
                        (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) Finset.univ i), s i) :
                      ℝ≥0∞)
                    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞))
                x}
            x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (a : α) ↦
                  Eq (α := ℝ≥0∞)
                    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
                    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞))
                x}
            x}
      a
h₂ h₃ :
  ∀ (a : α)
    (ha :
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
            (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) Finset.univ i), s i) :
          ℝ≥0∞)
        (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
      (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
      (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
filter_upwards [h.meas_biInter Finset.univ (fun _i _ ↦ hs _)] with a ha using by simp [← ha]

Premises used: Finset.univ, ProbabilityTheory.Kernel.iIndepSets.meas_biInter
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hμ : iIndep m κ μ
⊢ iIndepSets (fun (x : ι) ↦ {s : Set Ω | MeasurableSet s}) κ μ

Tactic:
hμ

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

Tactic:
h.iIndepSets'.ae_isProbabilityMeasure

Premises used: ProbabilityTheory.Kernel.iIndep.iIndepSets', ProbabilityTheory.Kernel.iIndepSets.ae_isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
S : Finset ι
hμ : iIndep m κ μ
hs : ∀ i ∈ S, MeasurableSet (s i)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
      (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
hμ _ hs
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
inst : Fintype ι
h : iIndep m κ μ
hs : ∀ (i : ι), MeasurableSet (s i)
h₁ :
  ∀ (a : α)
    (ha :
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
            (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) Finset.univ i), s i) :
          ℝ≥0∞)
        (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
      (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
      (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
filter_upwards [h.meas_biInter (fun i (_ : i ∈ Finset.univ) ↦ hs _)] with a ha

Premises used: ProbabilityTheory.Kernel.iIndep.meas_biInter
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
inst : Fintype ι
h : iIndep m κ μ
hs : ∀ (i : ι), MeasurableSet (s i)
a : α
ha :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) Finset.univ i), s i) :
      ℝ≥0∞)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
simp [← ha]
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
inst : Subsingleton ι
m : ι → Set (Set Ω)
κ : Kernel α Ω
inst_1 : IsMarkovKernel κ
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ m i
⊢ s = ∅ ∨ ∃ (i : ι), s = {i}

Tactic:
simpa using (subsingleton_of_subsingleton (s := (s : Set ι))).eq_empty_or_singleton

Premises used: Set.subsingleton_of_subsingleton, Set.Subsingleton.eq_empty_or_singleton
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
inst : Subsingleton ι
m : ι → Set (Set Ω)
κ : Kernel α Ω
inst_1 : IsMarkovKernel κ
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ m i
inl :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ∈ m i),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
            (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), f i) :
          ℝ≥0∞)
        (∏ i ∈ ∅, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
inr :
  ∀ (i : ι) (hf : ∀ (i_1 : ι), Membership.mem (γ := Finset ι) {i} i_1 → f i_1 ∈ m i_1),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
            (⋂ (i_1 : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {i} i_1), f i_1) :
          ℝ≥0∞)
        (∏ i ∈ {i}, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
      (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
obtain rfl | ⟨i, rfl⟩ : s = ∅ ∨ ∃ i, s = {i} := by
    simpa using (subsingleton_of_subsingleton (s := (s : Set ι))).eq_empty_or_singleton

Premises used: rfl
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
inst : Subsingleton ι
m : ι → Set (Set Ω)
κ : Kernel α Ω
inst_1 : IsMarkovKernel κ
f : ι → Set Ω
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ∈ m i
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), f i) :
        ℝ≥0∞)
      (∏ i ∈ ∅, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
inst : Subsingleton ι
m : ι → Set (Set Ω)
κ : Kernel α Ω
inst_1 : IsMarkovKernel κ
f : ι → Set Ω
i : ι
hf : ∀ (i_1 : ι), Membership.mem (γ := Finset ι) {i} i_1 → f i_1 ∈ m i_1
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (⋂ (i_1 : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {i} i_1), f i_1) :
        ℝ≥0∞)
      (∏ i ∈ {i}, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
inst : Subsingleton ι
m : ι → MeasurableSpace Ω
κ : Kernel α Ω
inst_1 : IsMarkovKernel κ
⊢ iIndep m κ μ

Tactic:
simp [iIndep]

Premises used: ProbabilityTheory.Kernel.iIndep
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun (x : ι) ↦ ∅
⊢ ∀ (x : ι'), f' (g x) = f x

Tactic:
have f'_apply x : f' (g x) = f x := hg.extend_apply ..
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun (x : ι) ↦ ∅
f'_apply : ∀ (x : ι'), f' (g x) = f x
simp_rw : ∀ ⦃x : ι'⦄, x ∈ s → f x ∈ π (g x)
⊢ ∀ i ∈ Finset.image g s, f' i ∈ π i

Tactic:
simp_rw [Finset.forall_mem_image, f'_apply]

Premises used: Finset.forall_mem_image
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun (x : ι) ↦ ∅
f'_apply : ∀ (x : ι'), f' (g x) = f x
⊢ ∀ ⦃x : ι'⦄, x ∈ s → f x ∈ π (g x)

Tactic:
hf

Premises used: Set.Mem
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun (x : ι) ↦ ∅
f'_apply : ∀ (x : ι'), f' (g x) = f x
⊢ ∀ ⦃x : ι'⦄, x ∈ s → f x ∈ π (g x)

Tactic:
exact hf
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun (x : ι) ↦ ∅
f'_apply : ∀ (x : ι'), f' (g x) = f x
⊢ ∀ i ∈ Finset.image g s, f' i ∈ π i

Tactic:
have hf' : ∀ i ∈ s.image g, f' i ∈ π i := by
    simp_rw [Finset.forall_mem_image, f'_apply]
    exact hf
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun (x : ι) ↦ ∅
f'_apply : ∀ (x : ι'), f' (g x) = f x
hf' : ∀ i ∈ Finset.image g s, f' i ∈ π i
h₁ :
  ∀ (a : α)
    (ha :
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ Finset.image g s, f' i) : ℝ≥0∞)
        (∏ i ∈ Finset.image g s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f' i) : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
      (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
      (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
filter_upwards [@h (s.image g) f' hf'] with a ha

Premises used: Finset.image
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun (x : ι) ↦ ∅
f'_apply : ∀ (x : ι'), f' (g x) = f x
hf' : ∀ i ∈ Finset.image g s, f' i ∈ π i
a : α
ha :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ Finset.image g s, f' i) : ℝ≥0∞)
    (∏ i ∈ Finset.image g s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f' i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
    (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
simpa [Finset.set_biInter_finset_image, Finset.prod_image hg.injOn, f'_apply] using ha

Premises used: Finset.set_biInter_finset_image, Function.Injective.injOn, Finset.prod_image
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun (x : ι) ↦ ∅
f'_apply : ∀ (x : ι'), f' (g x) = f x
have : ∀ i ∈ Finset.image g s, f' i ∈ π i
have₁ :
  ∀ (hf' : ∀ i ∈ Finset.image g s, f' i ∈ π i),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
        (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have₂ : ∀ i ∈ Finset.image g s, f' i ∈ π i
have₃ have₄ :
  ∀ (hf' : ∀ i ∈ Finset.image g s, f' i ∈ π i),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
        (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
h₁ :
  ∀ (hf' : ∀ i ∈ Finset.image g s, f' i ∈ π i) (a : α)
    (ha :
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ Finset.image g s, f' i) : ℝ≥0∞)
        (∏ i ∈ Finset.image g s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f' i) : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
      (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
      (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
classical
  have hf' : ∀ i ∈ s.image g, f' i ∈ π i := by
    simp_rw [Finset.forall_mem_image, f'_apply]
    exact hf
  filter_upwards [@h (s.image g) f' hf'] with a ha
  simpa [Finset.set_biInter_finset_image, Finset.prod_image hg.injOn, f'_apply] using ha

Premises used: Finset.set_biInter_finset_image
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Surjective g
h : iIndepSets (π ∘ g) κ μ
obtain : ∀ (g' : ι → ι') (hg' : Function.RightInverse g' g), iIndepSets π κ μ
⊢ iIndepSets π κ μ

Tactic:
obtain ⟨g', hg'⟩ := hg.hasRightInverse

Premises used: Function.Surjective.hasRightInverse
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Surjective g
h : iIndepSets (π ∘ g) κ μ
g' : ι → ι'
hg' : Function.RightInverse g' g
⊢ iIndepSets ((π ∘ g) ∘ g') κ μ

Tactic:
h.precomp hg'.injective

Premises used: ProbabilityTheory.Kernel.iIndepSets.precomp, Function.RightInverse.injective
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Surjective g
h : iIndepSets (π ∘ g) κ μ
g' : ι → ι'
hg' : Function.RightInverse g' g
h₁ : π = (π ∘ g) ∘ g'
⊢ iIndepSets π κ μ

Tactic:
convert! h.precomp hg'.injective

Premises used: ProbabilityTheory.Kernel.iIndepSets.precomp, Function.RightInverse.injective
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Surjective g
h : iIndepSets (π ∘ g) κ μ
g' : ι → ι'
hg' : Function.RightInverse g' g
h₁ : π = π ∘ g ∘ g'
h₂ : π = π ∘ id
h₃ h₄ : π = π
⊢ π = (π ∘ g) ∘ g'

Tactic:
rw [Function.comp_assoc, hg'.comp_eq_id, Function.comp_id]

Premises used: Function.comp_id, Function.RightInverse.comp_eq_id, Function.comp_assoc
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Bijective g
⊢ iIndepSets (π ∘ g) κ μ ↔ iIndepSets π κ μ

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

Premises used: Function.Bijective.injective, ProbabilityTheory.Kernel.iIndepSets.precomp, Function.Bijective.surjective, Iff.intro, ProbabilityTheory.Kernel.iIndepSets.of_precomp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndep m κ μ
⊢ iIndep (m ∘ g) κ μ

Tactic:
(iIndepSets.precomp hg h :)

Premises used: MeasurableSet, ProbabilityTheory.Kernel.iIndep, setOf, ProbabilityTheory.Kernel.iIndepSets.precomp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι' : Type u_5
g : ι' → ι
hg : Function.Surjective g
h : iIndep (m ∘ g) κ μ
⊢ iIndep m κ μ

Tactic:
iIndepSets.of_precomp hg h

Premises used: ProbabilityTheory.Kernel.iIndep, ProbabilityTheory.Kernel.iIndepSets.of_precomp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι' : Type u_5
g : ι' → ι
hg : Function.Bijective g
⊢ iIndep (m ∘ g) κ μ ↔ iIndep m κ μ

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

Premises used: Function.Bijective.injective, ProbabilityTheory.Kernel.iIndep.of_precomp, Function.Bijective.surjective, Iff.intro, ProbabilityTheory.Kernel.iIndep.precomp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSet s κ μ
⊢ iIndepSet (s ∘ g) κ μ

Tactic:
iIndep.precomp hg h

Premises used: ProbabilityTheory.Kernel.iIndepSet, ProbabilityTheory.Kernel.iIndep.precomp