-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma iInf_rat_gt_defaultRatCDF (t : ℚ) :
    ⨅ r : Ioi t, defaultRatCDF r = defaultRatCDF t

Proof state:
case neg.refine_2
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
x : ↑(Ioi t)
⊢ 1 ≤ if ↑x < 0 then 0 else 1

Tactic:
rw [if_neg]

Result:
case neg.refine_2.hnc
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
x : ↑(Ioi t)
⊢ ¬↑x < 0

Proof state:
case pos.refine_2
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
x : ↑(Ioi t)
⊢ 0 ≤ if ↑x < 0 then 0 else 1

Tactic:
split_ifs

Result:
case pos
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
x : ↑(Ioi t)
h✝ : ↑x < 0
⊢ 0 ≤ 0

case neg
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
x : ↑(Ioi t)
h✝ : ¬↑x < 0
⊢ 0 ≤ 1

Proof state:
t : ℚ
⊢ (⨅ r, if ↑r < 0 then 0 else 1) = if t < 0 then 0 else 1

Tactic:
have h_bdd : BddBelow (range fun r : ↥(Ioi t) ↦ ite ((r : ℚ) < 0) (0 : ℝ) 1) := by
  refine ⟨0, fun x hx ↦ ?_⟩
  obtain ⟨y, rfl⟩ := mem_range.mpr hx
  dsimp only
  split_ifs
  exacts [le_rfl, zero_le_one]

Result:
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
⊢ (⨅ r, if ↑r < 0 then 0 else 1) = if t < 0 then 0 else 1

Proof state:
case pos.refine_1.intro.intro
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
q : ℚ
htq : t < q
hq_neg : q < 0
⊢ (⨅ r, if ↑r < 0 then 0 else 1) ≤ 0

Tactic:
refine (ciInf_le h_bdd ⟨q, htq⟩).trans ?_

Result:
case pos.refine_1.intro.intro
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
q : ℚ
htq : t < q
hq_neg : q < 0
⊢ (if ↑⟨q, htq⟩ < 0 then 0 else 1) ≤ 0

Proof state:
case pos
t : ℚ
y : ↑(Ioi t)
hx : (fun r => if ↑r < 0 then 0 else 1) y ∈ range fun r => if ↑r < 0 then 0 else 1
h✝ : ↑y < 0
⊢ 0 ≤ 0

case neg
t : ℚ
y : ↑(Ioi t)
hx : (fun r => if ↑r < 0 then 0 else 1) y ∈ range fun r => if ↑r < 0 then 0 else 1
h✝ : ¬↑y < 0
⊢ 0 ≤ 1

Tactic:
exacts [le_rfl, zero_le_one]

Result:
no goals

Proof state:
t : ℚ
x : ℝ
hx : x ∈ range fun r => if ↑r < 0 then 0 else 1
⊢ 0 ≤ x

Tactic:
obtain ⟨y, rfl⟩ := mem_range.mpr hx

Result:
case intro
t : ℚ
y : ↑(Ioi t)
hx : (fun r => if ↑r < 0 then 0 else 1) y ∈ range fun r => if ↑r < 0 then 0 else 1
⊢ 0 ≤ (fun r => if ↑r < 0 then 0 else 1) y

Proof state:
case neg.refine_2.hnc
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
x : ↑(Ioi t)
⊢ ¬↑x < 0

Tactic:
rw [not_lt] at h ⊢

Result:
case neg.refine_2.hnc
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : 0 ≤ t
x : ↑(Ioi t)
⊢ 0 ≤ ↑x

Proof state:
case neg
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
⊢ (⨅ r, if ↑r < 0 then 0 else 1) = 1

Tactic:
refine le_antisymm ?_ ?_

Result:
case neg.refine_1
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
⊢ (⨅ r, if ↑r < 0 then 0 else 1) ≤ 1

case neg.refine_2
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
⊢ 1 ≤ ⨅ r, if ↑r < 0 then 0 else 1

Proof state:
t : ℚ
⊢ ⨅ r, defaultRatCDF ↑r = defaultRatCDF t

Tactic:
simp only [defaultRatCDF]

Result:
t : ℚ
⊢ (⨅ r, if ↑r < 0 then 0 else 1) = if t < 0 then 0 else 1

Proof state:
case intro
t : ℚ
y : ↑(Ioi t)
hx : (fun r => if ↑r < 0 then 0 else 1) y ∈ range fun r => if ↑r < 0 then 0 else 1
⊢ 0 ≤ if ↑y < 0 then 0 else 1

Tactic:
split_ifs

Result:
case pos
t : ℚ
y : ↑(Ioi t)
hx : (fun r => if ↑r < 0 then 0 else 1) y ∈ range fun r => if ↑r < 0 then 0 else 1
h✝ : ↑y < 0
⊢ 0 ≤ 0

case neg
t : ℚ
y : ↑(Ioi t)
hx : (fun r => if ↑r < 0 then 0 else 1) y ∈ range fun r => if ↑r < 0 then 0 else 1
h✝ : ¬↑y < 0
⊢ 0 ≤ 1

Proof state:
case pos.refine_1.intro.intro
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
q : ℚ
htq : t < q
hq_neg : q < 0
⊢ (if ↑⟨q, htq⟩ < 0 then 0 else 1) ≤ 0

Tactic:
rw [if_pos]

Result:
case pos.refine_1.intro.intro.hc
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
q : ℚ
htq : t < q
hq_neg : q < 0
⊢ ↑⟨q, htq⟩ < 0

Proof state:
case pos
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
h✝ : ↑⟨t + 1, ⋯⟩ < 0
⊢ 0 ≤ 1

case neg
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
h✝ : ¬↑⟨t + 1, ⋯⟩ < 0
⊢ 1 ≤ 1

Tactic:
exacts [zero_le_one, le_rfl]

Result:
no goals

Proof state:
case pos
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
x : ↑(Ioi t)
h✝ : ↑x < 0
⊢ 0 ≤ 0

case neg
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
x : ↑(Ioi t)
h✝ : ¬↑x < 0
⊢ 0 ≤ 1

Tactic:
exacts [le_rfl, zero_le_one]

Result:
no goals

Proof state:
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
⊢ (⨅ r, if ↑r < 0 then 0 else 1) = if t < 0 then 0 else 1

Tactic:
split_ifs with h

Result:
case pos
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
⊢ (⨅ r, if ↑r < 0 then 0 else 1) = 0

case neg
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
⊢ (⨅ r, if ↑r < 0 then 0 else 1) = 1

Proof state:
case neg.refine_1
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
⊢ (⨅ r, if ↑r < 0 then 0 else 1) ≤ 1

Tactic:
refine (ciInf_le h_bdd ⟨t + 1, lt_add_one t⟩).trans ?_

Result:
case neg.refine_1
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
⊢ (if ↑⟨t + 1, ⋯⟩ < 0 then 0 else 1) ≤ 1

Proof state:
case pos.refine_1
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
⊢ (⨅ r, if ↑r < 0 then 0 else 1) ≤ 0

Tactic:
obtain ⟨q, htq, hq_neg⟩ : ∃ q, t < q ∧ q < 0 := ⟨t / 2, by linarith, by linarith⟩

Result:
case pos.refine_1.intro.intro
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
q : ℚ
htq : t < q
hq_neg : q < 0
⊢ (⨅ r, if ↑r < 0 then 0 else 1) ≤ 0

Proof state:
case neg.refine_1
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
⊢ (if ↑⟨t + 1, ⋯⟩ < 0 then 0 else 1) ≤ 1

Tactic:
split_ifs

Result:
case pos
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
h✝ : ↑⟨t + 1, ⋯⟩ < 0
⊢ 0 ≤ 1

case neg
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
h✝ : ¬↑⟨t + 1, ⋯⟩ < 0
⊢ 1 ≤ 1

Proof state:
case neg.refine_2.hnc
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : 0 ≤ t
x : ↑(Ioi t)
⊢ 0 ≤ ↑x

Tactic:
exact h.trans (mem_Ioi.mp x.prop).le

Result:
no goals

Proof state:
case neg.refine_2
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
⊢ 1 ≤ ⨅ r, if ↑r < 0 then 0 else 1

Tactic:
refine le_ciInf fun x ↦ ?_

Result:
case neg.refine_2
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : ¬t < 0
x : ↑(Ioi t)
⊢ 1 ≤ if ↑x < 0 then 0 else 1

Proof state:
t : ℚ
⊢ BddBelow (range fun r => if ↑r < 0 then 0 else 1)

Tactic:
refine ⟨0, fun x hx ↦ ?_⟩

Result:
t : ℚ
x : ℝ
hx : x ∈ range fun r => if ↑r < 0 then 0 else 1
⊢ 0 ≤ x

Proof state:
case pos.refine_1.intro.intro.hc
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
q : ℚ
htq : t < q
hq_neg : q < 0
⊢ ↑⟨q, htq⟩ < 0

Tactic:
rwa [Subtype.coe_mk]

Result:
no goals

Proof state:
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
⊢ t / 2 < 0

Tactic:
linarith

Result:
no goals

Proof state:
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
⊢ t < t / 2

Tactic:
linarith

Result:
no goals

Proof state:
case pos
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
⊢ (⨅ r, if ↑r < 0 then 0 else 1) = 0

Tactic:
refine le_antisymm ?_ (le_ciInf fun x ↦ ?_)

Result:
case pos.refine_1
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
⊢ (⨅ r, if ↑r < 0 then 0 else 1) ≤ 0

case pos.refine_2
t : ℚ
h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)
h : t < 0
x : ↑(Ioi t)
⊢ 0 ≤ if ↑x < 0 then 0 else 1