-- Mathlib/Probability/Independence/Kernel.lean
theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
    {f' : Ω → β} {g' : Ω → β'} (hfg : IndepFun f g κ μ)
    (hf : ∀ᵐ a ∂μ, f =ᵐ[κ a] f') (hg : ∀ᵐ a ∂μ, g =ᵐ[κ a] g') :
    IndepFun f' g' κ μ

Proof state:
case h
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g κ μ
hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[ae (κ a)] f'
hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[ae (κ a)] g'
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
a : α
hf' : f =ᶠ[ae (κ a)] f'
hg' : g =ᶠ[ae (κ a)] g'
hfg' : (κ a) (f ⁻¹' A ∩ g ⁻¹' B) = (κ a) (f ⁻¹' A) * (κ a) (g ⁻¹' B)
⊢ (κ a) (f' ⁻¹' A ∩ g' ⁻¹' B) = (κ a) (f' ⁻¹' A) * (κ a) (g' ⁻¹' B)

Tactic:
have h1 : f ⁻¹' A =ᵐ[κ a] f' ⁻¹' A := hf'.fun_comp A

Result:
case h
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g κ μ
hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[ae (κ a)] f'
hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[ae (κ a)] g'
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
a : α
hf' : f =ᶠ[ae (κ a)] f'
hg' : g =ᶠ[ae (κ a)] g'
hfg' : (κ a) (f ⁻¹' A ∩ g ⁻¹' B) = (κ a) (f ⁻¹' A) * (κ a) (g ⁻¹' B)
h1 : f ⁻¹' A =ᶠ[ae (κ a)] f' ⁻¹' A
⊢ (κ a) (f' ⁻¹' A ∩ g' ⁻¹' B) = (κ a) (f' ⁻¹' A) * (κ a) (g' ⁻¹' B)

Proof state:
case h
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g κ μ
hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[ae (κ a)] f'
hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[ae (κ a)] g'
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
a : α
hf' : f =ᶠ[ae (κ a)] f'
hg' : g =ᶠ[ae (κ a)] g'
hfg' : (κ a) (f ⁻¹' A ∩ g ⁻¹' B) = (κ a) (f ⁻¹' A) * (κ a) (g ⁻¹' B)
h1 : f ⁻¹' A =ᶠ[ae (κ a)] f' ⁻¹' A
⊢ (κ a) (f' ⁻¹' A ∩ g' ⁻¹' B) = (κ a) (f' ⁻¹' A) * (κ a) (g' ⁻¹' B)

Tactic:
have h2 : g ⁻¹' B =ᵐ[κ a] g' ⁻¹' B := hg'.fun_comp B

Result:
case h
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g κ μ
hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[ae (κ a)] f'
hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[ae (κ a)] g'
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
a : α
hf' : f =ᶠ[ae (κ a)] f'
hg' : g =ᶠ[ae (κ a)] g'
hfg' : (κ a) (f ⁻¹' A ∩ g ⁻¹' B) = (κ a) (f ⁻¹' A) * (κ a) (g ⁻¹' B)
h1 : f ⁻¹' A =ᶠ[ae (κ a)] f' ⁻¹' A
h2 : g ⁻¹' B =ᶠ[ae (κ a)] g' ⁻¹' B
⊢ (κ a) (f' ⁻¹' A ∩ g' ⁻¹' B) = (κ a) (f' ⁻¹' A) * (κ a) (g' ⁻¹' B)

Proof state:
case intro.intro.intro.intro
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g κ μ
hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[ae (κ a)] f'
hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[ae (κ a)] g'
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (f' ⁻¹' A ∩ g' ⁻¹' B) = (κ a) (f' ⁻¹' A) * (κ a) (g' ⁻¹' B)

Tactic:
filter_upwards [hf, hg, hfg _ _ ⟨_, hA, rfl⟩ ⟨_, hB, rfl⟩] with a hf' hg' hfg'

Result:
case h
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g κ μ
hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[ae (κ a)] f'
hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[ae (κ a)] g'
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
a : α
hf' : f =ᶠ[ae (κ a)] f'
hg' : g =ᶠ[ae (κ a)] g'
hfg' : (κ a) (f ⁻¹' A ∩ g ⁻¹' B) = (κ a) (f ⁻¹' A) * (κ a) (g ⁻¹' B)
⊢ (κ a) (f' ⁻¹' A ∩ g' ⁻¹' B) = (κ a) (f' ⁻¹' A) * (κ a) (g' ⁻¹' B)

Proof state:
case h
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g κ μ
hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[ae (κ a)] f'
hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[ae (κ a)] g'
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
a : α
hf' : f =ᶠ[ae (κ a)] f'
hg' : g =ᶠ[ae (κ a)] g'
hfg' : (κ a) (f ⁻¹' A ∩ g ⁻¹' B) = (κ a) (f ⁻¹' A) * (κ a) (g ⁻¹' B)
h1 : f ⁻¹' A =ᶠ[ae (κ a)] f' ⁻¹' A
h2 : g ⁻¹' B =ᶠ[ae (κ a)] g' ⁻¹' B
⊢ (κ a) (f' ⁻¹' A ∩ g' ⁻¹' B) = (κ a) (f' ⁻¹' A) * (κ a) (g' ⁻¹' B)

Tactic:
rwa [← measure_congr h1, ← measure_congr h2, ← measure_congr (h1.inter h2)]

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g κ μ
hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[ae (κ a)] f'
hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[ae (κ a)] g'
⊢ IndepFun f' g' κ μ

Tactic:
rintro _ _ ⟨A, hA, rfl⟩ ⟨B, hB, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g κ μ
hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[ae (κ a)] f'
hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[ae (κ a)] g'
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (f' ⁻¹' A ∩ g' ⁻¹' B) = (κ a) (f' ⁻¹' A) * (κ a) (g' ⁻¹' B)