-- Mathlib/Probability/Independence/Kernel.lean
@[nontriviality]
lemma iIndepFun.of_subsingleton [IsMarkovKernel κ] [Subsingleton ι] : iIndepFun m f κ μ

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝¹ : IsMarkovKernel κ
inst✝ : Subsingleton ι
s : Finset ι
f' : (i : ι) → Set (β i)
hf' : ∀ i ∈ s, MeasurableSet (f' i)
x : ι
hx : x ∈ s
⊢ s = {x}

Tactic:
ext y

Result:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝¹ : IsMarkovKernel κ
inst✝ : Subsingleton ι
s : Finset ι
f' : (i : ι) → Set (β i)
hf' : ∀ i ∈ s, MeasurableSet (f' i)
x : ι
hx : x ∈ s
y : ι
⊢ y ∈ s ↔ y ∈ {x}

Proof state:
case inr.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝¹ : IsMarkovKernel κ
inst✝ : Subsingleton ι
s : Finset ι
f' : (i : ι) → Set (β i)
hf' : ∀ i ∈ s, MeasurableSet (f' i)
x : ι
hx : x ∈ s
this : s = {x}
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i ⁻¹' f' i) = ∏ i ∈ s, (κ a) (f i ⁻¹' f' i)

Tactic:
simp [this]

Result:
no goals

Proof state:
case inr.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝¹ : IsMarkovKernel κ
inst✝ : Subsingleton ι
s : Finset ι
f' : (i : ι) → Set (β i)
hf' : ∀ i ∈ s, MeasurableSet (f' i)
x : ι
hx : x ∈ s
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i ⁻¹' f' i) = ∏ i ∈ s, (κ a) (f i ⁻¹' f' i)

Tactic:
have : s = {x} := by ext y; simp [Subsingleton.elim y x, hx]

Result:
case inr.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝¹ : IsMarkovKernel κ
inst✝ : Subsingleton ι
s : Finset ι
f' : (i : ι) → Set (β i)
hf' : ∀ i ∈ s, MeasurableSet (f' i)
x : ι
hx : x ∈ s
this : s = {x}
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i ⁻¹' f' i) = ∏ i ∈ s, (κ a) (f i ⁻¹' f' i)

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝¹ : IsMarkovKernel κ
inst✝ : Subsingleton ι
s : Finset ι
f' : (i : ι) → Set (β i)
hf' : ∀ i ∈ s, MeasurableSet (f' i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i ⁻¹' f' i) = ∏ i ∈ s, (κ a) (f i ⁻¹' f' i)

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Result:
case inl
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝¹ : IsMarkovKernel κ
inst✝ : Subsingleton ι
f' : (i : ι) → Set (β i)
hf' : ∀ i ∈ ∅, MeasurableSet (f' i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ ∅, f i ⁻¹' f' i) = ∏ i ∈ ∅, (κ a) (f i ⁻¹' f' i)

case inr.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝¹ : IsMarkovKernel κ
inst✝ : Subsingleton ι
s : Finset ι
f' : (i : ι) → Set (β i)
hf' : ∀ i ∈ s, MeasurableSet (f' i)
x : ι
hx : x ∈ s
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i ⁻¹' f' i) = ∏ i ∈ s, (κ a) (f i ⁻¹' f' i)

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝¹ : IsMarkovKernel κ
inst✝ : Subsingleton ι
⊢ iIndepFun m f κ μ

Tactic:
refine (iIndepFun_iff_measure_inter_preimage_eq_mul ..).2 fun s f' hf' ↦ ?_

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝¹ : IsMarkovKernel κ
inst✝ : Subsingleton ι
s : Finset ι
f' : (i : ι) → Set (β i)
hf' : ∀ i ∈ s, MeasurableSet (f' i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i ⁻¹' f' i) = ∏ i ∈ s, (κ a) (f i ⁻¹' f' i)

Proof state:
case inl
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝¹ : IsMarkovKernel κ
inst✝ : Subsingleton ι
f' : (i : ι) → Set (β i)
hf' : ∀ i ∈ ∅, MeasurableSet (f' i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ ∅, f i ⁻¹' f' i) = ∏ i ∈ ∅, (κ a) (f i ⁻¹' f' i)

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝¹ : IsMarkovKernel κ
inst✝ : Subsingleton ι
s : Finset ι
f' : (i : ι) → Set (β i)
hf' : ∀ i ∈ s, MeasurableSet (f' i)
x : ι
hx : x ∈ s
y : ι
⊢ y ∈ s ↔ y ∈ {x}

Tactic:
simp [Subsingleton.elim y x, hx]

Result:
no goals