a b c : Int
x✝ : a ≤ b ∧ a ≤ c
h₁ : a ≤ b
h₂ : a ≤ c
⊢ a ≤ if b ≤ c then b else c
a b c : Int
x✝ : a ≤ b ∧ a ≤ c
h₁ : a ≤ b
h₂ : a ≤ c
⊢ a ≤ min b c
rw [Int.min_def]
no goals
a b c : Int
x✝ : a ≤ b ∧ a ≤ c
h₁ : a ≤ b
h₂ : a ≤ c
⊢ a ≤ if b ≤ c then b else c
split <;> assumption