Zulip Chat Archive

Stream: new members

Topic: Flipping an equality


Omnikar (Sep 24 2022 at 20:40):

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 (Sep 24 2022 at 20:44):

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

Kevin Buzzard (Sep 24 2022 at 22:10):

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

Rick de Wolf (Oct 17 2024 at 19:14):

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 (Oct 17 2024 at 19:17):

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 (Oct 17 2024 at 19:25):

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 (Oct 17 2024 at 19:25):

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 (Oct 17 2024 at 19:26):

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

Ruben Van de Velde (Oct 17 2024 at 19:27):

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

Rick de Wolf (Oct 17 2024 at 19:28):

Good idea :thumbs_up:


Last updated: May 02 2025 at 03:31 UTC