How do I prove statements about calculations in fields?

Stream: mathlib4

[Markus Schmaus]

Consider the following mwe, as demonstrated, I can prove this, but the proof feels cumbersome and if the terms themselves become more complex it becomes worse. Is there a better way to prove statements like these over fields?

import Mathlib

example (a b c : Rat) (i : Int) (h1 : b + 1 = c ^ (i + 1)) (h2 : c ≠ 0) :
    (a + b) / 2 = a + (c * c ^ i - 1 - a) / 2 := by
  simp [zpow_add₀ h2] at h1
  rw [mul_comm] at h1
  rw [← h1]
  field_simp
  ring_nf

[Heather Macbeth]

The expansion of c ^ (i + 1) as c * c ^ i for integer i currently requires special handling. The rest can be automated:

example (a b c : Rat) (i : Int) (h1 : b + 1 = c ^ (i + 1)) (h2 : c ≠ 0) :
    (a + b) / 2 = a + (c * c ^ i - 1 - a) / 2 := by
  simp [zpow_add₀ h2] at h1
  linear_combination h1 / 2 -- or `linarith`

[Heather Macbeth]

If the power i were taken from $\mathbb{N}$ rather than $\mathbb{Z}$ then it would be handled automatically.

example (a b c : Rat) (i : Nat) (h1 : b + 1 = c ^ (i + 1)) :
    (a + b) / 2 = a + (c * c ^ i - 1 - a) / 2 := by
  linear_combination h1 / 2

But an integer power is implicitly a potential fraction, but it isn't currently in the scope of the dedicated fraction-handling tactic (field_simp) -- so integer powers currently basically always require special handling.

[Markus Schmaus]

Thanks, that's very useful. How do I handle equations with different type? If not just i, but also b and c are in ℕ, then this fails

import Mathlib

example (a : Rat) (b c i : Nat) (h1 : b + 1 = c ^ (i + 1)) :
    (a + b) / 2 = a + (c * c ^ i - 1 - a) / 2 := by
  linear_combination h1 / 2 -- fails

[llllvvuu]

This works:

example (a : Rat) (b c i : Nat) (h1 : b + 1 = c ^ (i + 1)) :
    (a + b) / 2 = a + (c * c ^ i - 1 - a) / 2 := by
  qify at h1
  linear_combination h1 / 2

More manual way (checking the definitions for zify/qify/rify and searching for qify_simps/etc reveals that they do essentially this):

example (a : Rat) (b c i : Nat) (h1 : b + 1 = c ^ (i + 1)) :
    (a + b) / 2 = a + (c * c ^ i - 1 - a) / 2 := by
  apply_fun ((↑) : ℕ → ℚ) at h1
  push_cast at h1
  linear_combination h1 / 2