How to do something to both sides of an equation?

Stream: new members

[Alex Altair]

I've been going through a few different tutorials, and I've noticed that often my intuition for the next step of a proof is "do something to both sides of the equation". But it seems like the tutorial never does this; either they substitute a hypothesis somewhere, or they use a calc block via a clever rearrangement, or they apply a specific lemma by name. But is there some general purpose way to do this? I feel like there should be, since it's generally true that if two things are equal, then if there's any function that they can be fed into, the output will be the same.

[Kyle Miller]

This is an interesting question, but if you can give some, to ground the discussion it's helpful to have a #mwe ("minimal" isn't usually necessary, but "self-contained" is sufficient)

[Patrick Massot]

Maybe you simply want

import Mathlib.Tactic
import Mathlib.Data.Nat.Basic

example (a b : ℕ) (h : a + b = b) (f : ℕ → ℕ ) : True := by
  apply_fun f at h
  trivial

[Patrick Massot]

On a recent Mathlib you can do fancier things such as

import Mathlib.Tactic
import Mathlib.Data.Nat.Basic

example (a b : ℕ) (h : a + b = b) (f g : ℕ → ℕ ) (h' : f = g) : True := by
  have := congr($h' $h) -- will create this : f (a + b) = g b
  trivial

[Patrick Massot]

But that won't work in most tutorials that have not been updated very recently.

[Kyle Miller]

There are a number of "congruence" tactics, where "congruence" is roughly about proving the goal by proving something involving a part of the LHS and of the RHS of the goal. For example, congr!, convert, convert_to, congrm, and gcongr. The last one can handle inequalities, and congrm lets you zoom in on a related subexpression using a pattern.

Sometimes "doing something to both sides of an equation" like you'd normally want to do is a little inconvenient when formalizing because what you're actually doing is applying some injective function to both sides, and so you would need to show it's in fact injective. Clever rearrangements might be to eliminate needing to do this. apply_fun can also be used on the goal and can set up an auxiliary injectivity goal.

[Alex Altair]

Probably 90% of the time it's addition, subtraction, multiplication and division, but there's going to be a long tail of things like unioning with a given set, or taking the limit, or multiplying by a matrix on the left, et

[Alex Altair]

So there's certainly going to be a thing where you can't apply the inverse of any given function to both sides and have it be equal, but it should be true for true for taking any function? Not sure what you mean about injectivity

[Alex Altair]

I guess there's the case where I want to do this to a hypothesis, and a different case where I want to do it to a goal

[Alex Altair]

And I can imagine that for a goal I'd want to prove something like, a = b, and therefore f(a) = f(b), and it just so happens that f(a) equals the thing on the left side of the goal, and f(b) equals the thing on the right side of the goal

[Kyle Miller]

If you want to prove x = y, it suffices to prove f x = f y if f is injective.

[Kyle Miller]

if you have h : x = y as a hypothesis, then you can use Patrick's suggestions for applying f to both sides to get a new hypothesis

[Alex Altair]

Okay so this seems to be a #mwe;

import Mathlib.Tactic.ApplyFun

example {a b : ℝ} (h : a = b) : a + 1 = b + 1 := by
  apply_fun (· + 1) at h
  exact h

[Alex Altair]

But I take it this isn't idiomatic, and I'm interested to get a feel for why not

[Alex J. Best]

Well this example is a bit too minimal as in this situation I'd just do rw [h]. But I think using apply_fun is idiomatic enough in situations where you want to apply some intermediate function that doesn't just appear in the goal.

[Alex Altair]

... huh ... how does rw know what to rewrite it to?

[Mario Carneiro]

it rewrites every occurrence of a to b

[Alex Altair]

:man_facepalming: