case mp.intro.left
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ 0 ≤ t

case mp.intro.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ t ≤ 1 / a

case mpr.intro.left
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ 0 ≤ a * t

case mpr.intro.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ a * t ≤ 1
a t : ℝ
ha : 0 < a
⊢ a * t ∈ I ↔ t ∈ Icc 0 (1 / a)
constructor <;> rintro ⟨h₁, h₂⟩ <;> constructor
no goals
case mp.intro.left
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ 0 ≤ t
exact nonneg_of_mul_nonneg_right h₁ ha
no goals
case mp.intro.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ t ≤ 1 / a
rwa [le_div_iff ha, mul_comm]
no goals
case mpr.intro.left
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ 0 ≤ a * t
exact mul_nonneg ha.le h₁
no goals
case mpr.intro.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ a * t ≤ 1
rwa [le_div_iff ha, mul_comm] at h₂