awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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β : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (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)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
a : α
ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h'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)
⊢ ∀ (i : ι) (hi : i ∈ S),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)

Tactic:
have A i (hi : i ∈ S) : (κ a) (g i ⁻¹' sets i) = (κ a) (f i ⁻¹' sets i) := by
    apply measure_congr
    filter_upwards [ha i hi] with ω hω
    change (g i ω ∈ sets i) = (f i ω ∈ sets i)
    simp [hω]
-- 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β : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (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)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
a : α
ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h'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)
A :
  ∀ (i : ι) (hi : i ∈ S),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
H : ⋂ i ∈ S, g i ⁻¹' sets i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] ⋂ i ∈ S, f i ⁻¹' sets i
⊢ Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ⁻¹' sets i) : ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)

Tactic:
apply measure_congr

Premises used: MeasureTheory.measure_congr
-- 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β : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (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)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
a : α
ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h'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)
A :
  ∀ (i : ι) (hi : i ∈ S),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
h₁ :
  ∀ (ω : Ω) (hω : ∀ (i : ι) (hi : i ∈ (↑S : Set ι)), f i ω = g i ω),
    (⋂ (i : ι) (_ : i ∈ S), g i ⁻¹' sets i) ω = (⋂ (i : ι) (_ : i ∈ S), f i ⁻¹' sets i) ω
⊢ ⋂ i ∈ S, g i ⁻¹' sets i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] ⋂ i ∈ S, f i ⁻¹' sets i

Tactic:
filter_upwards [(ae_ball_iff (Finset.countable_toSet S)).2 ha] with ω hω

Premises used: Iff.mpr, MeasureTheory.ae_ball_iff, Finset.countable_toSet
-- 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β : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (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)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
a : α
ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h'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)
A :
  ∀ (i : ι) (hi : i ∈ S),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
ω : Ω
hω : ∀ (i : ι) (hi : i ∈ (↑S : Set ι)), f i ω = g i ω
⊢ Membership.mem (γ := Set Ω) (⋂ i ∈ S, g i ⁻¹' sets i) ω = Membership.mem (γ := Set Ω) (⋂ i ∈ S, f i ⁻¹' sets i) ω

Tactic:
simp +contextual [hω]
-- 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β : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (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)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
a : α
ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h'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)
A :
  ∀ (i : ι) (hi : i ∈ S),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
⊢ Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ⁻¹' sets i) : ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)

Tactic:
have B : (κ a) (⋂ i ∈ S, g i ⁻¹' sets i) = (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) := by
    apply measure_congr
    filter_upwards [(ae_ball_iff (Finset.countable_toSet S)).2 ha] with ω hω
    change (ω ∈ ⋂ i ∈ S, g i ⁻¹' sets i) = (ω ∈ ⋂ i ∈ S, f i ⁻¹' sets i)
    simp +contextual [hω]
-- 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β : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (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)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
a : α
ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h'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)
A :
  ∀ (i : ι) (hi : i ∈ S),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
B :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ⁻¹' sets i) : ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
⊢ 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:
h'a
-- 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β : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (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)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
a : α
ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h'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)
A :
  ∀ (i : ι) (hi : i ∈ S),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
B :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ⁻¹' sets i) : ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
h₁ :
  ∀ (i : ι) (hi : i ∈ S),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
⊢ Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ⁻¹' sets i) : ENNReal)
    (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)

Tactic:
convert! h'a using 2 with i hi
-- 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β : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (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)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
a : α
ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h'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)
A :
  ∀ (i : ι) (hi : i ∈ S),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
B :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ⁻¹' sets i) : ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
i : ι
hi : i ∈ S
⊢ Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)

Tactic:
A i hi
-- 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β : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (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)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
a : α
ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h'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)
A :
  ∀ (i : ι) (hi : i ∈ S),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
B :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ⁻¹' sets i) : ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
i : ι
hi : i ∈ S
⊢ Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)

Tactic:
exact A i hi
-- 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β : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h' : iIndepFun (β := β) g κ μ
⊢ iIndepFun (β := β) f κ μ

Tactic:
h'.congr' fun i ↦ ?_

Premises used: ProbabilityTheory.Kernel.iIndepFun.congr'
-- 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β : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h' : iIndepFun (β := β) g κ μ
refine : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, g i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i
⊢ iIndepFun (β := β) f κ μ

Tactic:
refine h'.congr' fun i ↦ ?_

Premises used: ProbabilityTheory.Kernel.iIndepFun.congr'
-- 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β : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h' : iIndepFun (β := β) g κ μ
i : ι
a : α
ha : f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
⊢ g i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i

Tactic:
ha.symm

Premises used: Filter.EventuallyEq.symm
-- 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β : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h' : iIndepFun (β := β) g κ μ
i : ι
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ g i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i) x} x}
      a
h₂ h₃ :
  ∀ (a : α) (ha : f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i),
    g i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i
⊢ ∀ᵐ (a : α) ∂μ, g i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i

Tactic:
filter_upwards [h i] with a ha using ha.symm
-- 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
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h : iIndepFun (β := β) f κ μ
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
rw :
  ∀
    (h :
      ∀ (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))
    (g : (i : ι) → β i → γ i) (hg : ∀ (i : ι), Measurable (g i)) (S : Finset ι) {sets : (i : ι) → Set (γ i)}
    (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ∘ f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ∘ f i ⁻¹' sets i) : ENNReal)
⊢ iIndepFun (β := γ) (fun (i : ι) ↦ g i ∘ f i) κ μ

Tactic:
rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h ⊢

Premises used: ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul
-- 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
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (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)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
⊢ ∀ (S : Finset ι) {sets : (i : ι) → Set (γ i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ∘ f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ∘ f i ⁻¹' sets i) : ENNReal)

Tactic:
fun t s hs ↦ ?_