-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma IsRatStieltjesPoint.ite {f g : α → ℚ → ℝ} {a : α} (p : α → Prop) [DecidablePred p]
    (hf : p a → IsRatStieltjesPoint f a) (hg : ¬ p a → IsRatStieltjesPoint g a) :
    IsRatStieltjesPoint (fun a ↦ if p a then f a else g a) a where
  mono

Proof state:
case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Monotone (f a)

case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Monotone (g a)

Tactic:
exacts [(hf h).mono, (hg h).mono]

Result:
no goals

Proof state:
case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Tendsto (f a) atTop (𝓝 1)

case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Tendsto (g a) atTop (𝓝 1)

Tactic:
exacts [(hf h).tendsto_atTop_one, (hg h).tendsto_atTop_one]

Result:
no goals

Proof state:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
⊢ ∀ (t : ℚ), ⨅ r, (if p a then f a else g a) ↑r = (if p a then f a else g a) t

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ ∀ (t : ℚ), ⨅ r, f a ↑r = f a t

case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ ∀ (t : ℚ), ⨅ r, g a ↑r = g a t

Proof state:
case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ ∀ (t : ℚ), ⨅ r, f a ↑r = f a t

case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ ∀ (t : ℚ), ⨅ r, g a ↑r = g a t

Tactic:
exacts [(hf h).iInf_rat_gt_eq, (hg h).iInf_rat_gt_eq]

Result:
no goals

Proof state:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
⊢ Tendsto (if p a then f a else g a) atTop (𝓝 1)

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Tendsto (f a) atTop (𝓝 1)

case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Tendsto (g a) atTop (𝓝 1)

Proof state:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
⊢ Tendsto (if p a then f a else g a) atBot (𝓝 0)

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Tendsto (f a) atBot (𝓝 0)

case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Tendsto (g a) atBot (𝓝 0)

Proof state:
case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Tendsto (f a) atBot (𝓝 0)

case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Tendsto (g a) atBot (𝓝 0)

Tactic:
exacts [(hf h).tendsto_atBot_zero, (hg h).tendsto_atBot_zero]

Result:
no goals

Proof state:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
⊢ Monotone (if p a then f a else g a)

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Monotone (f a)

case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Monotone (g a)