Introduction: Cormac Deignan

Stream: new members

[Cormac Deignan]

Hello everyone, hope all is well. I'm a maths student interested in Lean, but am still only a learner. Not sure if this is the right place for it, but I'm stuck on this problem:

example (x n : ℕ) : 1 + x ^ n = (1 - (x^n)^2) / (1 - x ^ n) :=
begin
  sorry,
end

I tried ring_exp, but no luck. I know this is probably a trivial question, (or already explained somewhere here), so thanks in advance for any help.

[Adam Topaz]

This is false:

import tactic.slim_check

example (x n : ℕ) : 1 + x ^ n = (1 - (x^n)^2) / (1 - x ^ n) :=
by slim_check

[Adam Topaz]

The issue is that subtraction and division for natural numbers don't behave as mathematicians usually expect.

[Johan Commelin]

The solution is to prove

example (x n : ℕ) : (1 + x ^ n : ℚ) = (1 - (x^n)^2) / (1 - x ^ n) :=
begin
  sorry,
end

[Johan Commelin]

Note that this is still false for x ^ n = 1, since you'll be dividing by 0.

[Adam Topaz]

Here's a proof with the additional assumption that $x^n \neq 1$:

import data.rat.basic
import tactic.field_simp
import tactic.ring

example (x n : ℕ) (h : x^n ≠ 1): (1 + x ^ n : ℚ) = (1 - (x^n)^2) / (1 - x ^ n) :=
begin
  have : (1 - x^n : ℚ) ≠ 0,
  { contrapose h,
    simp only [not_not] at h ⊢,
    rw sub_eq_zero at h,
    exact_mod_cast h.symm },
  field_simp,
  ring,
end

[Ruben Van de Velde]

  { contrapose h,
    simp only [not_not] at h ⊢,

can probably be

  { contrapose! h,

[Adam Topaz]

Yeah, I always forget contrapose! exists ;)

[Yaël Dillies]

Why not just intro h?

[Adam Topaz]

sure, you can intro c, apply h, but I think the word "contrapose" hits closer to home for most mathematicians....