wide code blocks

Stream: Zulip meta

[Kevin Buzzard]

Is it me or is it no longer the case that it's easy to read wide code blocks? Did there used to be a little scroll bar and now it's gone?

[Kevin Buzzard]

oh wut? It's there now.

[Kevin Buzzard]

lemma int.exists_nat_eq_of_nonneg {x : ℤ} (h : 0 ≤ x) : ∃ (y : ℕ), (y : ℤ) = x :=
begin
  cases x,
  { simp },
  { refine absurd h _,
    simp },
end

lemma int.pow_right_injective {x : ℤ} (h : 2 ≤ x) : function.injective (λ (n : ℕ), x ^ n) :=
begin
  intros n m hnm,
  obtain ⟨y, rfl⟩ : ∃ (y : ℕ), (y : ℤ) = x := int.exists_nat_eq_of_nonneg ((zero_le_two).trans h),
  have : 2 ≤ y,
  { rw ←int.coe_nat_le,
    simpa using h },
  apply nat.pow_right_injective this,
  simpa [←int.coe_nat_pow, int.coe_nat_inj'] using hnm
end

@[simp]
theorem dyadic_mk' {m n} : dyadic_mk (m, ⟨2 ^ n, n, rfl⟩) = m • powers_half n :=
begin
  dsimp,
  generalize_proofs h,
  congr,
  simp only [powers_two, mem_powers_iff, subtype.coe_mk] at h,
  apply int.pow_right_injective le_rfl,
  simpa using classical.some_spec h
end

was the block where I didn't get one

[Kevin Buzzard]

Ignore me, I'm clearly going mad