MathlibDemo.lean:468:75
Tactic state
No goals
Expected type
h_cubic : CubicResidueProperty
h_buell : Buell3Property
x y z : ℤ
h_eq : y ^ 2 + x ^ 3 * y + z ^ 3 + 3 = 0
t : ℤ
ht_eq : t ^ 2 = x ^ 6 - 4 * z ^ 3 - 12
ht3 : ¬3 ∣ t
ht4 : t % 4 ≠ 2
p : ℕ
hp_prime : Nat.Prime p
hp_dvd : p ∣ (t ^ 2 + 12).natAbs
hp_val_not_div3 : ¬3 ∣ (x ^ 6 - 4 * z ^ 3).natAbs.factorization p
hp_odd : Odd p
hp_not_form : ¬∃ u v, ↑p = u ^ 2 + 27 * v ^ 2
this : Fact (Nat.Prime p)
hp_mod3 : p % 3 = 1
h_no_cubic : ¬∃ y, y ^ 3 = 2
h_sub : x ^ 6 - 4 * z ^ 3 = t ^ 2 + 12
h_val_eq : (x ^ 6 - 4 * z ^ 3).natAbs.factorization p = (t ^ 2 + 12).natAbs.factorization p
⊢ ¬3 ∣ (x ^ 6 - 4 * z ^ 3).natAbs.factorization p
All Messages (36)
MathlibDemo.lean:66:81
This simp argument is unused:
  ZMod.natCast_eq_zero_iff

Hint: Omit it from the simp argument list.
  simp_all +decide [ ZMod.natCast_eq_zero_iff ]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
MathlibDemo.lean:113:114
Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
MathlibDemo.lean:123:10
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:140:46
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:143:49
This simp argument is unused:
  Nat.factorization_eq_zero_of_not_dvd

Hint: Omit it from the simp argument list.
  simp_all +decide [ Nat.factorization_eq_zero_of_not_dvd, ←[← even_iff_two_dvd, parity_simps ]parity_simps]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
MathlibDemo.lean:150:2
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:160:2
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:197:19
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:200:35
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:204:56
This simp argument is unused:
  pow_sub

Hint: Omit it from the simp argument list.
  simp_all +decide [ pow_sub, pow_add ][pow_add]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
MathlibDemo.lean:204:65
This simp argument is unused:
  pow_add

Hint: Omit it from the simp argument list.
  simp_all +decide [ pow_sub, pow_add ][pow_sub]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
MathlibDemo.lean:205:78
This simp argument is unused:
  pow_mul

Hint: Omit it from the simp argument list.
  simp_all +decide [ pow_add, pow_mul ][pow_add]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
MathlibDemo.lean:207:78
This simp argument is unused:
  pow_mul

Hint: Omit it from the simp argument list.
  simp_all +decide [ pow_add, pow_mul ][pow_add]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
MathlibDemo.lean:211:35
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:221:15
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:225:112
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:226:80
This simp argument is unused:
  Nat.mod_eq_of_lt

Hint: Omit it from the simp argument list.
  simp_all +decide [ Nat.dvd_iff_mod_eq_zero, Nat.mod_eq_of_lt ][Nat.dvd_iff_mod_eq_zero]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
MathlibDemo.lean:228:41
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:228:41
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:232:55
This simp argument is unused:
  pow_sub

Hint: Omit it from the simp argument list.
  simp_all +decide [ pow_sub ]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
MathlibDemo.lean:233:32
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:233:32
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:234:39
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:237:48
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:244:47
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:247:46
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:248:28
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:258:4
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:294:10
Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
MathlibDemo.lean:296:165
This simp argument is unused:
  Nat.factorization_eq_zero_of_not_dvd

Hint: Omit it from the simp argument list.
  simp_all +decide [ Nat.factorization_eq_zero_of_not_dvd, ← Int.natCast_dvd_natCast ][←
        Int.natCast_dvd_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
MathlibDemo.lean:302:49
This simp argument is unused:
  Nat.factorization_eq_zero_iff

Hint: Omit it from the simp argument list.
  simp_all +decide [ Nat.factorization_eq_zero_iff ]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
MathlibDemo.lean:323:24
Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
MathlibDemo.lean:357:77
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:358:30
aesop: failed to prove the goal after exhaustive search.
MathlibDemo.lean:359:130
This simp argument is unused:
  ← even_iff_two_dvd

Hint: Omit it from the simp argument list.
  simp_all +decide [ ← even_iff_two_dvd, parity_simps ][parity_simps]

Note: Simp arguments with `←` have the additional effect of removing the other direction from the simp set, even if the simp argument itself is unused. If the hint above does not work, try replacing `←` with `-` to only get that effect and silence this warning.

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
MathlibDemo.lean:393:8
Try this:
  [apply] exact main_theorem_mod_nine x z t ht