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