> Math notation is a peculiar, loosely defined, context-dependent, ambiguous syntax That's the point. This is what going all-in on formality looks like: /

> Math notation is a peculiar, loosely defined, context-dependent, ambiguous syntax That's the point. This is what going all-in on formality looks like: /-- If n is divisible by m then the set of divisors of m is a subset of the set of divisors of n lemma divisors_subset_of_dvd {m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) : divisors m ⊆ divisors n := finset.subset_iff.2 $ λ x hx, nat.mem_divisors.mpr (⟨(nat.mem_divisors.mp hx).1.trans h, hzero⟩) where each of those names is a reference to another proof - the full call tree would be far, far worse. Compare that to a handwritten proof: Let x be a divisor of m. Then there exists some y such that m = x * y. n is divisible by m, so there exists some k such that n = m * k. Thus n = (x * y) * k = x * (y * k) and x is a divisor of n.