Commutative semiring without Orzech property

CommSemiring_Not_OrzechProperty.lean

import Mathlib.Algebra.Tropical.Basic
import Mathlib.RingTheory.OrzechProperty

-- https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMB0BBdAcwFMsokcAVKCMYAYyXRwCEkBnBgKFElkRQZsOAErAAdoUqpi0AJ44A8lABexeqgAKNMMVhyuXJFjLEAbnBFwAXAF441WgyZwAFAHVgaSrTiASQgBKQ2NTCwQbOABlAFcsEAgAE2j0Yks3KwB1ywC4AHcZKGIuODhGKChgPRt7AG8wOAAfODAcAEY4QBMiZpwAJgBfYrgkBISAfRBiEAByaqGR0ZTR4YS3QEbgWZEgkrUaccmZuzhFwoAzdDcABgjNwfYQZL3puCg4UbhUWfv0BeJxh4rCKh4B8oIYJOwYEhxPRUtZEIlksQcAAxCReVJWcL5PRFEonQijGC%2BQ5YAwlEopeBgdpw8KHQAX5K5WgAaC4BZlHX5E%2BquJCzJnXAIBQCX5IMKcQqT0InT7IyWa12ZzRqdzgK4ZtReTnsQThJUvS6izmv0OdzRtFxMAAI7RVInC1wen0gAeHLkwo5qGFrzggDLCOAAflGmvJUFycAA2qjxOwJTh6BBfmAkMAoABdMWc%2BAIA72GJxBEpHDsZPiNKGjlgfqZhPiMx6bNTHDLR5uHPFr6t51ufPxJJF9ixWMwUYlqFwAA8TRwEnOUDOQszJVc7buDwmIDgch7sT7iOLQ4lo9Lk%2BnEhe8%2FQQsnAG4AHxLuCccCR6mVnocxx0RjMFvEK0%2FCc8CuMAKwfHC3ZdHIAQZlwCQ6nAJzSnAgBJhIA6QQRiIaaIHkBS4nARLIg6m4Mq4OAwDocDtAAVHAIBtG0cAANR0QxH6sa0vTspmIASD8yrAICwHrIcnjeL4gQ%2BsGgwgEgYBLCMMxvG8JLbsQzrwBO95PrwkadssHItkZ8wJiAIAZiUsnyWu6AzC8JH2KScDqZp2nPvUEb6SMHKdikQGjKZ5mGGgsiFJug5QAAVuoMDAPWoxIXCRHQrFEDiDgMRRTFcV2rM9plpu%2FqDE6ZEUb4rgALQKnAtH0Zx7QsXVvQ%2BWxiq8eI%2FEAkCayzGJqA%2BPUknKR6cCkpmLk3k%2BuRyZNl6ZoOJy6jC7AcYxLGlZRNGrVKjWtXA9hNe0Y1aiU7l8hGJw%2BQ8BlwIACYR0dd7DsBA9AcvdX7OMwZXyTdRlPS9FmhuGEauG8tWtc28z%2FgJQmfjon2Q2M0N%2BfA9E9IDJTqUg9DwIsLYQCcoziGl4jEASKM9aJXj9RJOSuFgszVfT27wfQoHECKwUyNAkxwMTI4SNFOM5QlEQADVwMlwtpTgACS4hC7F9aIXlDqC36o1kqUHDECt6u8oAgQSzIy5GUZVCocqbvhshyTnuUxrPs5GCBpsKWzkrygBBBMbG3W5b31wDbSoqm4KnZG7zxnGCMaQtCsJwAAwhAZmRJMqYSIQaSHBIJx6PLEJQjCXOhbz%2FOjNAagaNotANnIoxWHCEvKJXWg6LXWf2PlPr%2BmXgvZfFSFToMzfqK3Nf6DOCv978BOjtEWXC%2FFs994vqRkaBbazAg15vJmUupelWDAIrIugYxEUnwPXBAA

abbrev R := Tropical (WithTop ℤ)

abbrev M : Submodule R (R × R) where
  carrier := {p | p.1 ≤ p.2}
  add_mem' := add_le_add (α := R)
  zero_mem' := le_refl (0 : R)
  smul_mem' r _ h := mul_le_mul_right h r

instance : Module.Finite R M where
  fg_top := by
    let p1 : M := ⟨(1,0), le_top (a := (1 : R))⟩
    let p2 : M := ⟨(1,1), le_refl (1 : R)⟩
    refine ⟨{p1, p2}, top_unique fun ⟨⟨x, y⟩, h⟩ _ ↦ ?_⟩
    rw [Finset.coe_pair]
    let M' := Submodule.span R {p1, p2}
    convert M'.add_mem (M'.smul_mem x (Submodule.subset_span <| .inl rfl))
      (M'.smul_mem y (Submodule.subset_span <| .inr rfl)) <;>
      simp [p1, p2, Tropical.add_eq_left (id h : x ≤ y)]

def f : M →ₗ[R] M where
  toFun m := ⟨(.trop 1 * m.1.1 + m.1.2, m.1.2),
    min_le_right (α := WithTop ℤ) _ _⟩
  map_add' _ _ := by ext <;> simp [mul_add, add_add_add_comm]
  map_smul' r m := by ext <;> simp [mul_add, mul_left_comm]

theorem surjective_f : Function.Surjective f := fun m ↦ 
  ⟨⟨(.trop (-1) * m.1.1 + m.1.2, m.1.2), min_le_right (α := WithTop ℤ) _ _⟩, by
    ext; swap; rfl
    suffices m.1.1 + (.trop 1 * m.1.2 + m.1.2) = m.1.1 by
      simpa [f, mul_add, ← mul_assoc, ← Tropical.trop_add, add_assoc]
    rw [(_ * m.1.2).add_eq_right, Tropical.add_eq_left m.2]
    exact le_add_of_nonneg_left (α := WithTop ℤ) (b := 1) (by decide)⟩

theorem not_injective_f : ¬ Function.Injective f := fun inj ↦ by
  cases inj (a₁ := ⟨(.trop (-1), .trop 0), by simp+decide [M]⟩)
    (a₂ := ⟨(.trop 0, .trop 0), le_refl (_ : R)⟩) rfl

instance : CommSemiring R := inferInstance

theorem not_orzechProperty_R : ¬ OrzechProperty R := fun _ ↦ not_injective_f <|
  OrzechProperty.injective_of_surjective_of_injective (.id (M := M)) _ 
    Function.bijective_id.1 surjective_f