Challenge: solve two simultaneous equations (by automation?)

Stream: FLT

[Kevin Buzzard]

import Mathlib.RingTheory.OreLocalization.Ring

/-!

# Algebra instances of Ore Localizations

If `R` is a commutative ring with submonoid `S`, and if `A` is a commutative `R`-algebra,
then my guess is that `A[S⁻¹]` is an `R[S⁻¹]`-algebra. Let's see if I'm right and if so,
in what generality.

-/

namespace OreLocalization

variable {R A : Type*} [CommMonoid R] [CommMagma A] [MulAction R A] [IsScalarTower R A A]
  {S : Submonoid R}

@[to_additive]
private def mul' (a₁ : A) (s₁ : S) (a₂ : A) (s₂ : S) : A[S⁻¹] :=
  a₁ * a₂ /ₒ (s₂ * s₁)

@[to_additive]
private def mul''
  (a : A) (s : S) : A[S⁻¹] → A[S⁻¹] :=
  liftExpand (mul' a s) fun a₁ r₁ ⟨s₁, hs₁⟩ hr₁s₁ => by
  unfold OreLocalization.mul'
  simp only at hr₁s₁ ⊢
  rw [oreDiv_eq_iff]
  use ⟨s₁, hs₁⟩, r₁ * s₁
  simp only [Submonoid.mk_smul, Submonoid.coe_mul]
  constructor
  · rw [← smul_mul_assoc]
    rw [← smul_mul_assoc]
    rw [mul_comm]
    rw [smul_mul_assoc, smul_mul_assoc]
    rw [mul_comm]
    -- it's like a bloody Rubik's cube
    rw [smul_mul_assoc]
    rw [← mul_smul]
  · obtain ⟨s₂, hs₂⟩ := s
    simpa only [Submonoid.mk_smul, Submonoid.coe_mul] using mul_left_comm s₁ (r₁ * s₁) s₂

@[to_additive]
protected def mul : A[S⁻¹] → A[S⁻¹] → A[S⁻¹] :=
  liftExpand mul'' fun a₁ r₁ s hs => by
  obtain ⟨s₁, hs₁⟩ := s
  simp only at hs
  unfold OreLocalization.mul''
  simp
  unfold OreLocalization.mul'
  dsimp
  ext sa
  induction sa
  rename_i a s_temp
  obtain ⟨s, hs⟩ := s_temp
  rw [liftExpand_of]
  rw [liftExpand_of]
  rw [oreDiv_eq_iff]
  simp only [Submonoid.mk_smul, Submonoid.coe_mul]
  /- The challenge: The data is `Mul R` and `Mul A` and `SMul R A`, i.e. we have
  `* : R × R → R` and `* : A × A → A` and `• : R → A → A`. The problem is to simultaneously
  solve the two equations
  `u • (r₁ • a₁ * a) = v • (a₁ * a)`
  `u * (s * (r₁ * s₁)) = v * (s * s₁)`
  for `u` and `v` in `R`. The solutions can depend on the variables `r₁` etc.
  Naming convention: r's and s's are in R, a's are in A.
  Here are the axioms:

  * `mul_comm` works for both `R` and `A` (because of `CommMonoid R` and `CommMagma A`)
  * `mul_smul : (r₁ * r₂) • a = r₁ • (r₂ • a)` works because of `MulAction R A`. Note that
      this is about multiplication in `R`.
  * `smul_mul_assoc : (r • a₁) * a₂ = r • (a₁ * a₂)` works because of `IsScalarTower R A A`.
      This is about multiplication in `A`.

  For an added twist, you are given that some combinations of variables are in a submonoid `S` of `R`
  (see the precise hypotheses in the infoview for details) and you have to also ensure
  that `u ∈ S`.

  -/
  sorry

#exit

instance : Mul (A[S⁻¹]) where
  mul := OreLocalization.mul

example (as bt : R[S⁻¹]) : as * bt = as • bt := rfl -- fails on mathlib master;
-- works if irreducibiliy of OreLocalization.smul is removed

There's a fun sorry. We need it for Fermat! Maybe don't post spoilers here? Is this the sort of thing an SMT solver can do? I haven't done it myself yet BTW

[Ruben Van de Velde]

'OreLocalization.mul' depends on axioms: [propext, Quot.sound]

(by hand)

[Kevin Buzzard]

Nice to know it's true :-) Thanks!

[Kevin Buzzard]

Oh I think the one I did explicitly was harder. Try deleting mul'' and replacing it with

@[to_additive]
private def mul''
  (a : A) (s : S) : A[S⁻¹] → A[S⁻¹] :=
  liftExpand (mul' a s) fun a₁ r₁ ⟨s₁, hs₁⟩ hr₁s₁ => by
  unfold OreLocalization.mul'
  simp only at hr₁s₁ ⊢
  rw [oreDiv_eq_iff]
  sorry

Same rules.

[Ruben Van de Velde]

Same witnesses, slightly harder for the first goal and easier for the second

[Kevin Buzzard]

The next one is here on main.

[Ruben Van de Velde]

I'd better take a look, then

[Kevin Buzzard]

Looks like the trickiest one yet.

[Ruben Van de Velde]

Sorry-free in FLT#130; quite a messy proof, though

[Martin Dvořák]

I love your style that combines calc with ?_ for non-one-liners!