Omega adds unnecessary axioms

Stream: lean4

[Arshak Parsa]

I was trying to define real numbers in lean

protected def Rat.abs (a : Rat) : Rat :=
  {num:=a.num.natAbs,den:=a.den,den_nz:=a.den_nz,reduced:=a.reduced}

local notation a "⁻¹" => Rat.inv a

structure Real where
  seq : Nat → Rat
  reg {n m : Nat} : (seq m - seq n).abs ≤ m⁻¹ + n⁻¹

then I found out my definition depends on Classical.choice.
I traced down the problem and finally found out that some theorems in Lean are proved by omega tactic, which adds unnecessary axioms!
One of those theorems is Nat.add_eq_right

-- 'Nat.add_eq_right' depends on axioms: [propext, Classical.choice, Quot.sound]
#print axioms Nat.add_eq_right

-- 'add_eq_right' depends on axioms: [propext]
theorem add_eq_right {a b : Nat} : a + b = b ↔ a = 0 := by
  constructor
  . intro h
    rewrite (occs := .pos [2]) [← (Nat.zero_add b)] at h
    exact Eq.symm (Nat.add_right_cancel (id (Eq.symm h)))
  . intro h
    rw [h]
    exact Nat.zero_add b

-- 'add_eq_right0' depends on axioms: [propext, Quot.sound]
theorem add_eq_right0 {a b : Nat} : a + b = b ↔ a = 0 := by
  constructor;omega;omega

As you can see , this theorem could be easily proved without Classical.choice(and even Quot.sound). I guess the omega tactic had an option called useClassical but couldn't find this option in lean 4.20. Anyways, IMO, there are two ways to solve this problem:
1- Change the code of the omega tactic
2- Write the proofs in Lean without omega (or at least use a constructor tactic before the omega to avoid Classical.choice)
Should I create an issue for this?

[Henrik Böving]

This is not considered a problem by the core team of Lean, there have been previous attempts at reducing the axioms used by proofs in core and the answer is usually that it's not worth the time to make sure certain parts of the library stay axiom free or to change certain tactics such that they do not use some axiom.

[Eric Wieser]

I'll note that while the number of people who care about avoiding the use of Classical.choice in a proof is rather small, I suspect that a far smaller group care about propext or Quot.sound