aroots

Stream: mathlib4

[Patrick Massot]

New challenge coming from the silly idea of having some concrete examples in #mil:

import Mathlib
open Polynomial Complex

example : aroots (X^2 + 1 : ℝ[X]) ℂ = {I, -I} := sorry

[Patrick Massot]

I'll sleep while our European number theorists work on this.

[Patrick Massot]

I guess they will pretend this is analysis, not number theory, so let me also ask about

import Mathlib
open Polynomial

example : aroots (2*X - 1 : ℤ[X]) ℚ = {1/2} := sorry

[Patrick Massot]

While we are with number theory challenges, what about

import Mathlib.RingTheory.DedekindDomain.Ideal

example {ι : Type*} [Fintype ι] (a : ι → ℕ) (e : ι → ℕ)
  (coprime : ∀ i j, i ≠ j → IsCoprime (a i) (a j)) : ZMod (∏ i, a i) ≃+* ∀ i, ZMod (a i) := by
  sorry

It may or may not help to start with

example {ι : Type*} [Fintype ι] (P : ι → ℤ) (e : ι → ℕ) (prime : ∀ i, Prime (P i))
  (coprime : ∀ i j, i ≠ j → P i ≠ P j) :
    ℤ ⧸ ∏ i, (Ideal.span ({P i} : Set ℤ)) ^ e i ≃+* ∀ i, ℤ ⧸ (Ideal.span {P i}) ^ e i := by
  apply IsDedekindDomain.quotientEquivPiOfProdEq
  all_goals { sorry }

[Patrick Massot]

and it may or may not help to use docs#ZMod.chineseRemainder.

[Patrick Massot]

This question is in the context of writing in #mil: "we have a fancy Chinese remainder theorem docs#Ideal.quotientInfRingEquivPiQuotient but of course it easily implies the stupidly elementary one, as long we notice intersection and product are the same there since integers form a Dedekind domain".

[Patrick Massot]

Now I remember why we never do examples or elementary versions in Mathlib.

[Yongyi Chen]

I actually did something similar for fun last week: proving that the roots of $x^2 + 2x + 1$ are $\{-1,-1\}$ as a muiltiset.

import Mathlib
open Polynomial

noncomputable abbrev my_poly : ℝ[X] := X^2 + 2 * X + 1

example : my_poly.roots = {-1, -1} := by
  have factored : my_poly = (X + 1) * (X + 1) := by ring
  rw [factored]
  have p_ne_zero : my_poly ≠ 0 := mt (congr_arg fun p => coeff p 0) (by simp only [coeff_add, coeff_X_pow, ite_false,
    mul_coeff_zero, coeff_X_zero, mul_zero, coeff_one_zero, zero_add, coeff_zero, one_ne_zero])
  rw [roots_mul (factored ▸ p_ne_zero)]
  have := roots_X_sub_C (-1 : ℝ)
  simp only [map_neg, map_one, sub_neg_eq_add] at this
  rw [this]
  trivial

I used roots instead of aroots though. So maybe a strategy is to base change to $\mathbb C$ then do something like what I did.

[Yongyi Chen]

Patrick Massot said:

I guess they will pretend this is analysis, not number theory, so let me also ask about

import Mathlib
open Polynomial

example : aroots (2*X - 1 : ℤ[X]) ℚ = {1/2} := sorry

My solution:

import Mathlib
import Polynomial

example : aroots (2*X - 1 : ℤ[X]) ℚ = {1/2} := by
  simp only [aroots_def, algebraMap_int_eq, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X,
    Polynomial.map_one]
  have := roots_X_sub_C (1 / 2 : ℚ)
  rw [← roots_C_mul, mul_sub, ← C_mul, mul_one_div, div_self_of_invertible] at this
  all_goals trivial

Found that a forward proof is easiest because simp likes to turn C a into a : ℚ[x] which is actually harder to work with.

[Yongyi Chen]

Patrick Massot said:

New challenge coming from the silly idea of having some concrete examples in #mil:

import Mathlib
open Polynomial Complex

example : aroots (X^2 + 1 : ℝ[X]) ℂ = {I, -I} := sorry

example : aroots (X^2 + 1 : ℝ[X]) ℂ = {I, -I} := by
  simp only [aroots_def, Polynomial.map_add, Polynomial.map_pow, map_X, Polynomial.map_one]
  have factored : (X ^ 2 + 1 : ℂ[X]) = (X - C I) * (X - C (-I)) := by
    ring_nf
    simp only [map_neg, mul_neg, sub_self, zero_add, ← C_mul, I_mul_I, neg_neg, map_one, add_comm]
  have p_ne_zero : (X ^ 2 + 1 : ℂ[X]) ≠ 0 := mt (congr_arg fun p => coeff p 0) (by simp only [coeff_add,
    coeff_X_pow, ite_false, coeff_one_zero, zero_add, coeff_zero, one_ne_zero, not_false_eq_true])
  rw [factored, roots_mul (factored ▸ p_ne_zero), roots_X_sub_C, roots_X_sub_C]
  rfl

[Ruben Van de Velde]

So much for leaving it to the Europeans (good morning) :)

[Yongyi Chen]

Good night!

[Damiano Testa]

Yongyi Chen said:

Patrick Massot said:

New challenge coming from the silly idea of having some concrete examples in #mil:

import Mathlib
open Polynomial Complex

example : aroots (X^2 + 1 : ℝ[X]) ℂ = {I, -I} := sorry

example : aroots (X^2 + 1 : ℝ[X]) ℂ = {I, -I} := by
  simp only [aroots_def, Polynomial.map_add, Polynomial.map_pow, map_X, Polynomial.map_one]
  have factored : (X ^ 2 + 1 : ℂ[X]) = (X - C I) * (X - C (-I)) := by
    ring_nf
    simp only [map_neg, mul_neg, sub_self, zero_add, ← C_mul, I_mul_I, neg_neg, map_one, add_comm]
  have p_ne_zero : (X ^ 2 + 1 : ℂ[X]) ≠ 0 := mt (congr_arg fun p => coeff p 0) (by simp only [coeff_add,
    coeff_X_pow, ite_false, coeff_one_zero, zero_add, coeff_zero, one_ne_zero, not_false_eq_true])
  rw [factored, roots_mul (factored ▸ p_ne_zero), roots_X_sub_C, roots_X_sub_C]
  rfl

Just for didactic purposes, p_ne_zero in Yongyi Chen's proof can be split into

  have natDegree_p : natDegree (X ^ 2 + 1 : ℂ[X]) = 2 := by compute_degree!
  have p_ne_zero : (X ^ 2 + 1 : ℂ[X]) ≠ 0 := by
    apply ne_zero_of_natDegree_gt (n := 1)
    linarith

[Patrick Massot]

Thank you very much @Yongyi Chen! We clearly need to work to make this a lot easier, but at least it's doable.

[Patrick Massot]

@Mario Carneiro I've heard rumors saying you're interested in merging CAS and ITP and that you need at least one new project a day. Could we have a polynomial tactic that normalizes (X - C Complex.I) * (X - C (-Complex.I)) to X^2 - C (Complex.I ^2) so that the above example becomes nice?

[Mario Carneiro]

I think you could probably do that using polyrith

[Mario Carneiro]

it's a ring equation modulo I^2 = -1

[Mario Carneiro]

which one is the #mwe example to simplify?

[Patrick Massot]

Not only modulo I^2 = -1, you also need to know that C is a ring morphism.

[Patrick Massot]

import Mathlib
open Polynomial Complex

example : aroots (X^2 + 1 : ℝ[X]) ℂ = {I, -I} := by
  simp only [aroots_def, Polynomial.map_add, Polynomial.map_pow, map_X, Polynomial.map_one]
  have factored : (X ^ 2 + 1 : ℂ[X]) = (X - C I) * (X - C (-I)) := by
    ring_nf
    simp only [map_neg, mul_neg, sub_self, zero_add, ← C_mul, I_mul_I, neg_neg, map_one, add_comm]
  have p_ne_zero : (X ^ 2 + 1 : ℂ[X]) ≠ 0 := mt (congr_arg fun p => coeff p 0) (by simp only [coeff_add,
    coeff_X_pow, ite_false, coeff_one_zero, zero_add, coeff_zero, one_ne_zero, not_false_eq_true])
  rw [factored, roots_mul (factored ▸ p_ne_zero), roots_X_sub_C, roots_X_sub_C]
  rfl

[Patrick Massot]

Both haves would be nice to optimize, but here I'm talking about the first one.

[Mario Carneiro]

I believe something like this was going to come up in our factorization project anyway, cc: @Alex J. Best

[Mario Carneiro]

this was supposed to be the "easy" direction

[Mario Carneiro]

I guess as long as you keep the C I isolated it is possible to do it without any ring morphism reasoning

[Patrick Massot]

Sure. Exactly your favorite kind of project: doable in one sitting.

[Patrick Massot]

Mario Carneiro said:

I guess as long as you keep the C I isolated it is possible to do it without any ring morphism reasoning

I don't understand what this means.

[Mario Carneiro]

I mean that you can prove (X ^ 2 + 1 : ℂ[X]) = (X - C I) * (X - -(C I)) as a ring equation modulo C I * C I = -1

[Patrick Massot]

Sure, but then you need ring morphism reasoning to go from I*I = -1 to what you need.

[Mario Carneiro]

I'm saying if that theorem is just available then you can use it for a polyrith proof

[Mario Carneiro]

that's not an unreasonable theorem to have in the library

[Mario Carneiro]

  have factored : (X ^ 2 + 1 : ℂ[X]) = (X - C I) * (X - C (-I)) := by
    rw [C_neg]
    linear_combination show (C I * C I : ℂ[X]) = -1 by simp [← C_mul]

[Patrick Massot]

That's a nice trick but using linear_combination like this is really strange.

[Patrick Massot]

My current compilation of tricks to make it readable is

example : aroots (X^2 + 1 : ℝ[X]) ℂ = {I, -I} := by
  suffices roots (X ^ 2 + 1 : ℂ[X]) = {I, -I} by simpa [aroots_def]
  have factored : (X ^ 2 + 1 : ℂ[X]) = (X - C I) * (X - C (-I)) := by
    rw [C_neg]
    linear_combination show (C I * C I : ℂ[X]) = -1 by simp [← C_mul]
  have p_ne_zero : (X - C I) * (X - C (-I)) ≠ 0 := by
    intro H
    apply_fun eval 0 at H
    simp [eval] at H
  simp only [factored, roots_mul p_ne_zero, roots_X_sub_C]
  rfl

[Mario Carneiro]

well, it's a bit golfed, the more reasonable way to write it is:

theorem C_I_mul_C_I : (C I * C I : ℂ[X]) = -1 := by simp [← C_mul]

example : aroots (X^2 + 1 : ℝ[X]) ℂ = {I, -I} := by
  simp only [aroots_def, Polynomial.map_add, Polynomial.map_pow, map_X, Polynomial.map_one]
  have factored : (X ^ 2 + 1 : ℂ[X]) = (X - C I) * (X - C (-I)) := by
    rw [C_neg]
    linear_combination C_I_mul_C_I
  sorry

[Mario Carneiro]

or polyrith [C_I_mul_C_I] which generates that line

[Patrick Massot]

I still think the new lemma shouldn't be needed when using your new tactic. Only I_mul_I should be invoked.

[Mario Carneiro]

this isn't so much a new tactic as an extension to ring

[Mario Carneiro]

working with multivariate polynomial equations is literally what ring is designed to do

[Patrick Massot]

Ok, granted: Your new extension of ring.

[Alex J. Best]

Kazuhiko Sakaguchi was telling me this week that the coq ring tactic pushes all ring homomorphisms inwards as a preprocessing step (and even does this recursively or some such)

[Patrick Massot]

Patrick Massot said:

While we are with number theory challenges, what about

import Mathlib.RingTheory.DedekindDomain.Ideal

example {ι : Type*} [Fintype ι] (a : ι → ℕ) (e : ι → ℕ)
  (coprime : ∀ i j, i ≠ j → IsCoprime (a i) (a j)) : ZMod (∏ i, a i) ≃+* ∀ i, ZMod (a i) := by
  sorry

I had enough sleep so I stopped waiting on European people:

open BigOperators Ideal

lemma IsCoprime.natCast {R : Type*} [CommSemiring R] {a b : ℕ} (h : IsCoprime a b) :
    IsCoprime (a : R) (b : R) := by
  rcases h with ⟨u, v, H⟩
  use u, v
  rw_mod_cast [H]
  exact Nat.cast_one

theorem Ideal.iInf_span_singleton_natCast {R : Type*} [CommSemiring R] {ι : Type*} [Fintype ι]
    {I : ι → ℕ} (hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)) :
    ⨅ (i : ι), Ideal.span {(I i : R)} = Ideal.span {((∏ i : ι, I i : ℕ) : R)} := by
  rw [Ideal.iInf_span_singleton, Nat.cast_prod]
  exact fun i j h ↦ (hI i j h).natCast

example {ι : Type*} [Fintype ι] (a : ι → ℕ) (coprime : ∀ i j, i ≠ j → IsCoprime (a i) (a j)) :
    ZMod (∏ i, a i) ≃+* ∀ i, ZMod (a i) :=
  have : ∀ (i j : ι), i ≠ j → IsCoprime (span {(a i : ℤ)}) (span {(a j : ℤ)}) :=
    fun i j h ↦ (isCoprime_span_singleton_iff _ _).mpr ((coprime i j h).natCast (R := ℤ))
  Int.quotientSpanNatEquivZMod _ |>.symm.trans <|
  quotEquivOfEq (iInf_span_singleton_natCast (R := ℤ) coprime) |>.symm.trans <|
  quotientInfRingEquivPiQuotient _ this |>.trans <|
  RingEquiv.piCongrRight fun i ↦ Int.quotientSpanNatEquivZMod (a i)

[Patrick Massot]

It would be easier to read without lean4#2217 of course.

[Eric Wieser]

#6509 contains a workaround for lean4#2217

[Patrick Massot]

Nice! Is there any obstacle to moving forward?

[Patrick Massot]

In the meantime I opened #7599 with the ZMod Chinese remainder.

[Eric Wieser]

Just someone's time to implement it, and the fact that you have to write both sides of the morphism every time

[Eric Wieser]

By both sides, I'm referring to the LHS in

  calc
    A ≃ₗ[R] B := f
    B ≃ₗ[R] C := g
    C ≃ₗ[R] D := h

[Patrick Massot]

Oh, that's indeed disappointing.

[Eric Wieser]

Maybe if you locally turn off the "refuse to find instances by unification" behavior it works

[Eric Wieser]

I don't remember how to do that, or whether it's actually possible in this situation

[Timo Carlin-Burns]

Patrick Massot said:

While we are with number theory challenges, what about

import Mathlib.RingTheory.DedekindDomain.Ideal

example {ι : Type*} [Fintype ι] (a : ι → ℕ) (e : ι → ℕ)
  (coprime : ∀ i j, i ≠ j → IsCoprime (a i) (a j)) : ZMod (∏ i, a i) ≃+* ∀ i, ZMod (a i) := by
  sorry

Don't you want docs#Nat.Coprime not docs#IsCoprime ? IsCoprime n m for natural numbers is only true if n or m is 1.

[Patrick Massot]

Oh thanks! The theorem was still true (and indeed Lean agrees, but a bit disappointing).

[Timo Carlin-Burns]

Here is a version for CommRings.. I don't know if the theorem is true in a CommSemiring since we can't deduce IsCoprime from Nat.Coprime

open BigOperators Ideal

lemma IsCoprime.intCast {R : Type*} [CommRing R] {a b : ℤ} (h : IsCoprime a b) :
    IsCoprime (a : R) (b : R) := by
  rcases h with ⟨u, v, H⟩
  use u, v
  rw_mod_cast [H]
  exact Int.cast_one

lemma Nat.Coprime.cast {R : Type*} [CommRing R] {a b : ℕ} (h : Nat.Coprime a b) :
    IsCoprime (a : R) (b : R) := by
  rw [← isCoprime_iff_coprime] at h
  rw [← Int.cast_ofNat a, ← Int.cast_ofNat b]
  exact IsCoprime.intCast h

theorem Ideal.iInf_span_singleton_natCast {R : Type*} [CommRing R] {ι : Type*} [Fintype ι]
    {I : ι → ℕ} (hI : ∀ (i j : ι), i ≠ j → Nat.Coprime (I i) (I j)) :
    ⨅ (i : ι), Ideal.span {(I i : R)} = Ideal.span {((∏ i : ι, I i : ℕ) : R)} := by
  rw [Ideal.iInf_span_singleton, Nat.cast_prod]
  exact fun i j h ↦ (hI i j h).cast

noncomputable example {ι : Type*} [Fintype ι] (a : ι → ℕ) (coprime : ∀ i j, i ≠ j → Nat.Coprime (a i) (a j)) :
    ZMod (∏ i, a i) ≃+* ∀ i, ZMod (a i) :=
  have : ∀ (i j : ι), i ≠ j → IsCoprime (span {(a i : ℤ)}) (span {(a j : ℤ)}) :=
    fun i j h ↦ (isCoprime_span_singleton_iff _ _).mpr ((coprime i j h).cast (R := ℤ))
  Int.quotientSpanNatEquivZMod _ |>.symm.trans <|
  quotEquivOfEq (iInf_span_singleton_natCast (R := ℤ) coprime) |>.symm.trans <|
  quotientInfRingEquivPiQuotient _ this |>.trans <|
  RingEquiv.piCongrRight fun i ↦ Int.quotientSpanNatEquivZMod (a i)

[Patrick Massot]

Thanks!

[Timo Carlin-Burns]

Indeed, the statement is false in general for a CommSemiring. I thought it would be a fun exercise to try and prove a counterexample:

semiring counterexample

import Mathlib
open BigOperators Ideal

/-- The semiring ℕ ⊕ {2, 3, 4, ...} such that
operations between the two sets land in the latter..
We are setting up a counterexample because
(inr 6) ∈ span {inl 2} ⊓ span {inl 3} but (inr 6) ∉ span {inl 6} -/
@[ext]
structure S where
  val : ℕ
  b : Bool
  h : b → 1 < val

namespace S

instance : Zero S where
  zero := ⟨0, false, by simp⟩

instance : One S where
  one := ⟨1, false, by simp⟩

@[simp] theorem val_zero : (0 : S).val = 0 := by rfl
@[simp] theorem b_zero : (0 : S).b = false := by rfl
@[simp] theorem val_one : (1 : S).val = 1 := by rfl
@[simp] theorem b_one : (1 : S).b = false := by rfl

instance : Add S where
  add := by
    refine fun ⟨n, b, h⟩ ⟨n', b', h'⟩ => ⟨n + n', b || b', fun hbb => ?_⟩
    rw [Bool.or_coe_iff] at hbb
    rcases hbb with hb | hb'
    . exact Nat.lt_add_right 1 n n' (h hb)
    . exact Nat.lt_add_left 1 n' n (h' hb')

instance : Mul S where
  mul := by
    refine fun ⟨n, b, _⟩ ⟨n', b', _⟩ => ⟨n * n', 1 < n * n' && (b || b'), fun hbb => ?_⟩
    simp only [Bool.and_eq_true, decide_eq_true_eq, Bool.or_eq_true] at hbb
    exact hbb.left

@[simp] theorem val_add (s t : S) : (s + t).val = s.val + t.val := by
  rfl

@[simp] theorem b_add (s t : S) : (s + t).b = (s.b || t.b) := by
  rfl

@[simp] theorem val_mul (s t : S) : (s * t).val = s.val * t.val := by
  rfl

@[simp] theorem b_mul (s t : S) : (s * t).b = (1 < s.val * t.val && (s.b || t.b)) := by
  rfl

protected theorem left_distrib : (a b c : S) → a * (b + c) = a * b + a * c
  | ⟨1, true, h⟩, _, _
  | _, ⟨1, true, h⟩, _
  | _, _, ⟨1, true, h⟩
  | _, ⟨0, true, h⟩, _
  | _, _, ⟨0, true, h⟩ => by simp at h
  | ⟨0, b, h⟩, s, t
  | _, ⟨0, false, _⟩, _
  | _, _, ⟨0, false, _⟩ => by ext <;> simp
  | ⟨_, false, _⟩, ⟨_, false, _⟩, ⟨_, false, _⟩ => by
    ext <;> simp [Nat.left_distrib]
  | ⟨n + 2, true, _⟩, ⟨m + 1, _, _⟩, ⟨k + 1, _, _⟩
  | ⟨n + 1, _, _⟩, ⟨m + 2, true, _⟩, ⟨k + 1, _, _⟩ => by
    ext
    . simp [Nat.left_distrib]
    . rw [Bool.eq_iff_iff]
      simp
      ring_nf
      refine ⟨fun _ => Or.inl ?_, fun h => ?_⟩
      <;> repeat apply Nat.lt_add_right
      <;> norm_num
  | ⟨n + 1, _, _⟩, ⟨m + 1, _, _⟩, ⟨k + 2, true, _⟩ => by
    ext
    . simp [Nat.left_distrib]
    . rw [Bool.eq_iff_iff]
      simp
      ring_nf
      refine ⟨fun _ => Or.inr ?_, fun h => ?_⟩
      <;> repeat apply Nat.lt_add_right
      <;> norm_num

protected theorem mul_comm (a b : S) : a * b = b * a := by
  intros; ext <;> simp [Nat.mul_comm, Bool.or_comm]

protected theorem mul_assoc : (a b c : S) → a * b * c = a * (b * c)
  | ⟨1, true, h⟩, _, _
  | _, ⟨1, true, h⟩, _
  | _, _, ⟨1, true, h⟩
  | _, ⟨0, true, h⟩, _
  | _, _, ⟨0, true, h⟩ => by simp at h
  | ⟨0, b, h⟩, s, t
  | _, ⟨0, false, _⟩, _
  | _, _, ⟨0, false, _⟩ => by ext <;> simp
  | ⟨_, false, _⟩, ⟨_, false, _⟩, ⟨_, false, _⟩ => by
    ext <;> simp [Nat.mul_assoc]
  | ⟨n + 2, true, _⟩, ⟨m + 1, _, _⟩, ⟨k + 1, _, _⟩ => by
    ext
    . simp [Nat.mul_assoc]
    . rw [Bool.eq_iff_iff]
      simp
      ring_nf
      refine ⟨fun _ => ?_, fun _ => ⟨?_, Or.inl ?_⟩⟩
      <;> repeat apply Nat.lt_add_right
      <;> norm_num
  | ⟨n + 1, _, _⟩, ⟨m + 2, true, _⟩, ⟨k + 1, _, _⟩ => by
    ext
    . simp [Nat.mul_assoc]
    . rw [Bool.eq_iff_iff]
      simp
      ring_nf
      refine ⟨fun _ => ⟨?_, Or.inr ?_⟩, fun _ => ⟨?_, Or.inl ?_⟩⟩
      <;> repeat apply Nat.lt_add_right
      <;> norm_num
  | ⟨n + 1, _, _⟩, ⟨m + 1, _, _⟩, ⟨k + 2, true, _⟩ => by
    ext
    . simp [Nat.mul_assoc]
    . rw [Bool.eq_iff_iff]
      simp
      ring_nf
      refine ⟨fun _ => ⟨?_, Or.inr ?_⟩, fun _ => ?_⟩
      <;> repeat apply Nat.lt_add_right
      <;> norm_num

protected theorem S.one_mul : (a : S) → 1 * a = a
  | ⟨_, false, h⟩ => by ext <;> simp
  | ⟨_, true, h⟩ => by
    ext
    . simp
    . simp at h ⊢
      assumption

instance : CommSemiring S where
  add_assoc := by intros; ext <;> simp [Nat.add_assoc, Bool.or_assoc]
  zero_add := by intros; ext <;> simp
  add_zero := by intros; ext <;> simp
  add_comm := by intros; ext <;> simp [Nat.add_comm, Bool.or_comm]
  left_distrib := S.left_distrib
  right_distrib := by
    intros a b c
    rw [S.mul_comm, S.left_distrib, S.mul_comm a c, S.mul_comm b c]
  zero_mul := by intros; ext <;> simp
  mul_zero := by intros; ext <;> simp
  mul_assoc := S.mul_assoc
  one_mul := S.one_mul
  mul_one := by intros; rw [S.mul_comm, S.one_mul]
  natCast := fun n => ⟨n, false, by simp⟩
  natCast_zero := by rfl
  natCast_succ := by intros; ext <;> simp
  mul_comm := S.mul_comm

@[simp] theorem val_natCast (n : ℕ) [n.AtLeastTwo] : (no_index (OfNat.ofNat n : S)).val = n := by rfl

theorem counterexample :
    Ideal.span {(2 : S)} ⊓ Ideal.span {(3 : S)} ≠ Ideal.span {(6 : S)} := by
  have h6 : true → 1 < 6 := by simp
  suffices ⟨6, true, h6⟩ ∈ Ideal.span {(2 : S)} ⊓ Ideal.span {(3 : S)} ∧ ⟨6, true, h6⟩ ∉ Ideal.span {(6 : S)} by
    intro h
    rw [h] at this
    simp_all only [and_not_self]
  rw [mem_inf (R := S), mem_span_singleton', mem_span_singleton', mem_span_singleton']
  refine ⟨⟨?_, ?_⟩, ?_⟩
  . use ⟨3, true, by simp⟩
    rfl
  . use ⟨2, true, by simp⟩
    rfl
  . rintro ⟨a, h⟩
    rw [S.ext_iff] at h
    simp at h
    rcases h with ⟨hval, _, hb⟩
    have := a.h hb
    linarith

end S

axiom Ideal.iInf_span_singleton_natCast {R : Type*} [CommSemiring R] {ι : Type*} [Fintype ι]
    {I : ι → ℕ} (hI : ∀ (i j : ι), i ≠ j → Nat.Coprime (I i) (I j)) :
    ⨅ (i : ι), Ideal.span {(I i : R)} = Ideal.span {((∏ i : ι, I i : ℕ) : R)}

example : False := by
  apply S.counterexample
  have : ∀ (i j : ({2, 3} : Finset ℕ)), i ≠ j → Nat.Coprime i j := by
    rintro ⟨i, hi⟩ ⟨j, hj⟩
    fin_cases hi
    <;> fin_cases hj
    <;> simp
  convert Ideal.iInf_span_singleton_natCast (R := S) this
  ext
  simp

[Mario Carneiro]

@Patrick Massot said:

Mario Carneiro I've heard rumors saying you're interested in merging CAS and ITP and that you need at least one new project a day. Could we have a polynomial tactic that normalizes (X - C Complex.I) * (X - C (-Complex.I)) to X^2 - C (Complex.I ^2) so that the above example becomes nice?

Here it is: #7601. The linear_combination proof is still a little scuffed because it doesn't know how to make use of equalities in the wrong type (it doesn't know what ring hom to use to lift the equation), but after lifting I_mul_I ring is able to get it:

example (X : ℂ[X]) : X ^ 2 + 1 = (X - C I) * (X - C (-I)) := by
  have := congr_arg (C : ℂ → ℂ[X]) I_mul_I
  linear_combination this

[Patrick Massot]

It looks great but the PR doesn't build.

[Patrick Massot]

And the failure seem to be indeed about ring and not an unrelated timeout.

[Patrick Massot]

In defense of ring, this docs#odd_sq_dvd_geom_sum₂_sub is a really nasty proof. And I guess ring doesn't like docs#Finset.sum.

[Patrick Massot]

Even the linkifier doesn't like that lemma.

[Patrick Massot]

I meant this proof

[Patrick Massot]

It would be nice to drastically simplify this proof, but it would also be nice to make sure ring does not time out in such hostile territory.