[Lean ]Fix & Proof numbertheory_notequiv2i2jasqbsqdiv8

[DyeKuu]

Note:

The negation should negate also the forall. To verify if my formalization is correct, I provide proof of it.

[albertqjiang]

I'm sure the new formalisation is correct. However I wonder whether the formalisation is incorrect if the negation sign is inside?

[DyeKuu]

I'm sure the new formalisation is correct. However I wonder whether the formalisation is incorrect if the negation sign is inside?

You mean whether the original one is provable? It's equiv to

∀ a b : ℤ, ¬ (∃ i j, a = 2*i ∧ b=2*j) ↔ (∃ k, a^2 + b^2 = 8*k))

so that's probably what you mean by negation sign is inside? I ponder around it and found that:

• Either we pop the negation back to the front to make it be

  ¬ ∃ a b : ℤ, (∃ i j, a = 2*i ∧ b=2*j) ↔ (∃ k, a^2 + b^2 = 8*k))

  this can be falsified by a = b = 0, but I haven't found the tactic.

• Either using not_iff, leads to a goal

  given a b even, prove that for all k, a^2 + b^2 \neq 8*k.

[albertqjiang]

I'm sure the new formalisation is correct. However I wonder whether the formalisation is incorrect if the negation sign is inside?

You mean whether the original one is provable? It's equiv to

∀ a b : ℤ, ¬ (∃ i j, a = 2*i ∧ b=2*j) ↔ (∃ k, a^2 + b^2 = 8*k))

so that's probably what you mean by negation sign is inside? I ponder around it and found that:

• Either we pop the negation back to the front to make it be

¬ ∃ a b : ℤ, (∃ i j, a = 2*i ∧ b=2*j) ↔ (∃ k, a^2 + b^2 = 8*k))

• Either using not_iff, leads to a goal

given a b even, prove that for all k, a^2 + b^2 \neq 8*k.

Ah this makes sense. Thanks for clarifying for me.