Is there a bug in field_simp tactic?

Stream: mathlib4

[Alexan Ayrapetyan]

Hi. This lean4 code actually does compile without any errors

import Mathlib

import Aesop

set_option maxHeartbeats 0

open Topology Filter Real Complex TopologicalSpace Finset Function Metric Nat Rat
open scoped BigOperators Matrix

theorem lean_workbook_plus_11408 : (4 / 3) * (6 / 4) * (8 / 5) * (10 / 6) * (12 / 7) * (14 / 8) = 1   := by/-
  We need to verify that the product of the fractions \\( \\frac{4}{3} \\times \\frac{6}{4} \\times \\frac{8}{5} \\times \\frac{10}{6} \\times \\frac{12}{7} \\times \\frac{14}{8} \\) equals 1. Each fraction in the product can be simplified by canceling out common factors in the numerator and the denominator. After canceling common factors, each term simplifies to 1. Therefore, the product of these terms is 1.
  -/
  -- Simplify the expression by canceling out common factors in the numerator and the denominator.
  field_simp

clearly the math is wrong since the answer of the expression is 16, even though lean does not through any errors here.
Moreover, when I change answer to 16 I do get an error
simp made no progress

[Yaël Dillies]

4 / 3 = 1 because everything is a natural by default. Try (4 / 3 : ℚ) instead

[Notification Bot]

This topic was moved here from #lean4 > Is there a bug in field_simp tactic? by Floris van Doorn.

[Alexan Ayrapetyan]

Thanks a lot!