A tactic I'd find useful

Stream: general

[Bhavik Mehta]

At the moment, field_simp is great for multiplying out equalities in a field. It would be nice if we have something which could also multiply out denominators in an ordered field, potentially using positivity to know what's positive (or negative). Here's the example that made me think of this:

lemma test_case {E A B : ℕ} {K : ℝ} (hK : 0 < K) (hE : K⁻¹ * (A ^ 2 * B) ≤ E)
    (hA : 0 < A) (hB : 0 < B) :
    A / (Real.sqrt 2 * K) ≤ Real.sqrt 2⁻¹ * (E / (A * B)) := by
  rw [inv_mul_le_iff hK] at hE
  rw [mul_div_assoc', div_le_div_iff, ←mul_assoc, ←sq]
  rotate_left
  · positivity
  · positivity
  refine hE.trans_eq ?_
  field_simp
  ring

The proof is pretty ad-hoc but really this feels like it should be simpler... nlinarith can't do it either, even knowing positivity for A,B as reals.

[Yaël Dillies]

@Heather Macbeth has this for teaching IIRC

[Bolton Bailey]

Here is a proof which is much more complicated, but has the virtue of requiring only a single tactic call.

import Mathlib

lemma div_eq_iff' [Field F] (a b c : F) :
    (a / b) = c ↔ (b = 0 ∧ c = 0) ∨ (¬ b = 0 ∧ a = b * c) := by
  by_cases h : b = 0
  · simp_all
    exact eq_comm
  · simp_all
    constructor
    · intro h'
      rw [← h']
      exact (mul_div_cancel' a h).symm
    · intro h'
      rw [h']
      exact mul_div_cancel_left c h

lemma div_le_iff'' [LinearOrderedField F] (a b c : F) :
    (a / b) ≤ c ↔ (b = 0 ∧ 0 ≤ c) ∨ (0 < b ∧ a ≤ b * c) ∨ (b < 0 ∧ b * c ≤ a) := by
  by_cases h : b = 0
  · simp_all
  · simp_all
    cases' lt_or_gt_of_ne h with h' h'
    · have h'' : ¬ 0 < b := by
        exact lt_asymm h'
      simp [h'', h']
      rw [div_le_iff_of_neg h']
      rw [mul_comm]
    · have h'' : ¬ b < 0 := by
        exact lt_asymm h'
      simp [h'', h']
      rw [div_le_iff h']
      rw [mul_comm]

lemma le_div_iff'' [LinearOrderedField F] (a b c : F) :
    a ≤ b / c ↔ (c = 0 ∧ a ≤ 0) ∨ (0 < c ∧ a * c ≤ b) ∨ (c < 0 ∧ b ≤ a * c) := by
  by_cases h : c = 0
  · simp_all
  · simp_all
    cases' lt_or_gt_of_ne h with h' h'
    · have h'' : ¬ 0 < c := by
        exact lt_asymm h'
      simp [h'', h']
      rw [le_div_iff_of_neg h']
    · have h'' : ¬ c < 0 := by
        exact lt_asymm h'
      simp [h'', h']
      rw [le_div_iff h']

example [LinearOrderedField F] (a b c : F) : (a / b) * c = (a * c) / b := by
  exact div_mul_eq_mul_div a b c

lemma mul_lt_zero_iff''' [LinearOrderedField F] (a b : F) :
    a * b < 0 ↔ (a < 0 ∧ 0 < b) ∨ (0 < a ∧ b < 0)  := by
  sorry


lemma test_case {E A B : ℕ} {K : ℝ} (hK : 0 < K) (hE : K⁻¹ * (A ^ 2 * B) ≤ E)
    (hA : 0 < A) (hB : 0 < B) :
    A / (Real.sqrt 2 * K) ≤ Real.sqrt 2⁻¹ * (E / (A * B)) := by
  simpa [-one_div, ←mul_div_assoc, div_mul_eq_mul_div, div_le_iff'', le_div_iff'', mul_lt_zero_iff''',
    Nat.cast_pos.mpr, Nat.pos_iff_ne_zero.mp, ne_of_gt, lt_asymm, inv_eq_one_div, mul_assoc, pow_two,
    mul_comm _ (Real.sqrt _), mul_left_comm _ (Real.sqrt _),
    hA, hB, hK] using hE

[Heather Macbeth]

Yaël Dillies said:

Heather Macbeth has this for teaching IIRC

No, I don't. I faked this tactic (i.e. gave a hack implementation) once or twice for talks (e.g. here) and Terry also proposed it at some point. I think this would be a great tactic, but as you can see at that thread, it seems to require a more principled implementation than field_simp's current implementation.