Weird behavior of rw?

Stream: new members

[Sebastian Zimmer]

I'm trying to shorten the following proof:

lemma sqr_roots_one (x : ℝ) (p : x ^ 2 = 1) : x = 1 ∨ x = -1 := begin
cases le_total x 0,
right,
rw [neg_eq_iff_neg_eq.1],
rw [← sqrt_sqr (neg_le_neg h), pow_two, neg_mul_neg, ← pow_two, p, sqrt_one],
left, rw [← sqrt_sqr h, p, sqrt_one],
end

But when I try to combine the two adjacent rw tactics into one it doesn't work.

[Chris Hughes]

That's because rw [neg_eq_iff_neg_eq.1], solved your goal, but created a new one. rw [eq_neg_iff_eq_neg], should allow you to merge the goals.
Incidentally, here's the shortest proof

lemma sqr_roots_one (x : ℝ) (p : x ^ 2 = 1) : x = 1 ∨ x = -1 :=
by rwa [pow_two, mul_self_eq_one_iff] at p

[Sebastian Zimmer]

Lol I feel like I searched for everything except mul_self :oh_no:

[Johan Commelin]

lemma sqr_roots_one (x : ℝ) (p : x ^ 2 = 1) : x = 1 ∨ x = -1 :=
by rwa [←mul_self_eq_one_iff, ←pow_two]

[Chris Hughes]

I think this is one area the library isn't entirely consistent. There's a mix of pow_two and mul_self.

[Scott Olson]

For the record I found this way that lets you write the original with a merged rw:

lemma sqr_roots_one (x : ℝ) (p : x ^ 2 = 1) : x = 1 ∨ x = -1 := begin
cases le_total x 0,
right,
symmetry,
rw [neg_eq_iff_neg_eq, ← sqrt_sqr (neg_le_neg h), pow_two, neg_mul_neg, ← pow_two, p, sqrt_one],
left, rw [← sqrt_sqr h, p, sqrt_one],
end

[Scott Olson]

(Didn't work without symmetry first because of the way neg_eq_iff_neg_eq is written)

[Sebastian Zimmer]

This is probably a stupid question but how do I prove 2 \neq 0 in \com ?

[Sebastian Zimmer]

I noticed there is a theorem two_ne_zero that sounded promising but doesn't seem to work

[Chris Hughes]

I think it's two_ne_zero'. Not a stupid question.

[Sebastian Zimmer]

Thanks that worked. What is the difference between two_ne_zero and two_ne_zero'?

[Scott Olson]

Different typeclass requirements, I guess:

#check @two_ne_zero
-- two_ne_zero : ∀ {α : Type u_1} [_inst_1 : linear_ordered_field α], 2 ≠ 0

#check @two_ne_zero'
-- two_ne_zero' : ∀ {α : Type u_1} [_inst_1 : add_monoid α] [_inst_2 : has_one α] [_inst_3 : char_zero α], 2 ≠ 0

[Chris Hughes]

It's a core thing. Every linear ordered field has characteristic zero, but two_ne_zero is in core, so it can't be changed, and therefore we need a version for char_zero as well.