mathlib

mathlib copied to clipboard

It is nontrivial (currently for me impossible) to use wlog in the following example.

lemma forty_two (a b c : ℕ) (h : (0:ℚ) < 1 - (1/a + 1/b + 1/c)) :
  (1:ℚ)/(1 - (1/a + 1/b + 1/c)) ≤ 42 :=
begin
  wlog : a ≤ b ∧ b ≤ c, -- or some similar incantation involving "using ..."
end

I am perfectly happy with having to prove some side goals.