Flipping an equality

Stream: new members

[Omnikar]

Hi, I just found out about Lean recently and have been reading through and following along with "Theorem Proving with Lean 4." I've come here to ask: given hab : a = b, how would I obtain hba : b = a?

[Omnikar]

Oh, I found the answer, it's Eq.symm

[Kevin Buzzard]

You can probably even use hab.symm because of dot notation

[Rick de Wolf]

Hi, I have a hypothesis h : a = b which I would like to reverse to get h : b = a. What I'm currently using is this:

import Mathlib
example MWE {a b : Real} (h : a = b) : a^2=b^2 := by
  apply Eq.symm at h

This turns h into a hypothesis containing a forall statement, which seems more convoluted than necessary. Is there a better way to reverse equalities?

[Bryan Gin-ge Chen]

You could write h.symm wherever you need a proof of b = a, but that might be a pain if there are many occurrences.

[Ruben Van de Velde]

Huh, that's not what I expected apply to do, but you can use one of these:

import Mathlib
example MWE {a b : Real} (h : a = b) : a^2=b^2 := by
  replace h := h.symm
  rw [eq_comm] at h
  sorry

[Rick de Wolf]

Ah that's a nice approach! It doesn't work in this case unfortunately, since I need to rw [...] at h after flipping h. Here is the proof I'm working with:

import Mathlib
lemma indep_self (h : IndepSet A A) : ℙ A = 0 ∨ ℙ A = 1 := by
  unfold IndepSet at h
  rw [inter_self] at h
  -- apply Eq.symm at h -- TODO Ask why this doesn't work?
  have h' : ℙ A * ℙ A = ℙ A := Eq.symm h
  rw [ENNReal.mul_self_eq_self_iff] at h'
  rcases h' with h'|h'|h'
  · left; exact h'
  · right; exact h'
  · measurability
  done

[Rick de Wolf]

Nvm! Replace is a nice tactic in this case. Dankjewel :)

[Ruben Van de Velde]

In this case I would add the eq_comm in the rw you're doing anyway, but yeah, either works

[Rick de Wolf]

Good idea :thumbs_up: