-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma meas_countablePartitionSet_le_of_fst_le (hκν : fst κ ≤ ν) (n : ℕ) (a : α) (x : γ)
    (s : Set β) :
    κ a (countablePartitionSet n x ×ˢ s) ≤ ν a (countablePartitionSet n x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ (κ a) (countablePartitionSet n x ×ˢ s) ≤ (κ.fst a) (countablePartitionSet n x)

Tactic:
rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ (κ a) (countablePartitionSet n x ×ˢ s) ≤ (κ a) {p | p.1 ∈ countablePartitionSet n x}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x✝ : γ
s : Set β
x : γ × β
⊢ x.1 ∈ countablePartitionSet n x✝ → x.2 ∈ s → x.1 ∈ countablePartitionSet n x✝

Tactic:
exact fun h _ ↦ h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ (κ a) (countablePartitionSet n x ×ˢ s) ≤ (κ a) {p | p.1 ∈ countablePartitionSet n x}

Tactic:
refine measure_mono (fun x ↦ ?_)

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x✝ : γ
s : Set β
x : γ × β
⊢ x ∈ countablePartitionSet n x✝ ×ˢ s → x ∈ {p | p.1 ∈ countablePartitionSet n x✝}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ (κ a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)

Tactic:
calc κ a (countablePartitionSet n x ×ˢ s)
  ≤ fst κ a (countablePartitionSet n x) := by
      rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)]
      refine measure_mono (fun x ↦ ?_)
      simp only [mem_prod, mem_setOf_eq, and_imp]
      exact fun h _ ↦ h
_ ≤ ν a (countablePartitionSet n x) := hκν a _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x✝ : γ
s : Set β
x : γ × β
⊢ x ∈ countablePartitionSet n x✝ ×ˢ s → x ∈ {p | p.1 ∈ countablePartitionSet n x✝}

Tactic:
simp only [mem_prod, mem_setOf_eq, and_imp]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x✝ : γ
s : Set β
x : γ × β
⊢ x.1 ∈ countablePartitionSet n x✝ → x.2 ∈ s → x.1 ∈ countablePartitionSet n x✝