-- Mathlib/Probability/Kernel/WithDensity.lean
lemma withDensity_sub_add_cancel [IsSFiniteKernel κ] {f g : α → β → ℝ≥0∞}
    (hf : Measurable (Function.uncurry f)) (hg : Measurable (Function.uncurry g))
    (hfg : ∀ a, g a ≤ᵐ[κ a] f a) :
    withDensity κ (fun a x ↦ f a x - g a x) + withDensity κ g = withDensity κ f

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a
⊢ κ.withDensity ((fun a x => f a x - g a x) + g) = κ.withDensity f

Tactic:
refine withDensity_congr_ae κ ((hf.sub hg).add hg) hf (fun a ↦ ?_)

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a
a : α
⊢ ((fun a x => f a x - g a x) + g) a =ᶠ[ae (κ a)] f a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a
a : α
⊢ ((fun a x => f a x - g a x) + g) a =ᶠ[ae (κ a)] f a

Tactic:
filter_upwards [hfg a] with x hx

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a
a : α
x : β
hx : g a x ≤ f a x
⊢ ((fun a x => f a x - g a x) + g) a x = f a x

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a
⊢ (κ.withDensity fun a x => f a x - g a x) + κ.withDensity g = κ.withDensity f

Tactic:
rw [← withDensity_add_right _ hg]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a
⊢ κ.withDensity ((fun a x => f a x - g a x) + g) = κ.withDensity f

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a
⊢ Measurable (Function.uncurry fun a x => f a x - g a x)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a
a : α
x : β
hx : g a x ≤ f a x
⊢ ((fun a x => f a x - g a x) + g) a x = f a x

Tactic:
rwa [Pi.add_apply, Pi.add_apply, tsub_add_cancel_iff_le]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a
⊢ Measurable (Function.uncurry fun a x => f a x - g a x)

Tactic:
exact hf.sub hg

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a
⊢ κ.withDensity ((fun a x => f a x - g a x) + g) = κ.withDensity f

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a
⊢ Measurable (Function.uncurry fun a x => f a x - g a x)

Tactic:
swap

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a
⊢ Measurable (Function.uncurry fun a x => f a x - g a x)

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a
⊢ κ.withDensity ((fun a x => f a x - g a x) + g) = κ.withDensity f