English
For an integer a and integer b with b ≠ 0 in α, the image of a/b in α equals a/b computed in α: (a /. b : α) = a / b.
Русский
Для целого a и целого b, где b ≠ 0 в α, изображение дроби a/b в α равно делению a на b в α: (a /. b : α) = a / b.
LaTeX
$$$\forall a \in \mathbb{Z}, \forall b \in \mathbb{Z},\ (b : \alpha) \neq 0 \Rightarrow (a /. b : \alpha) = a / b.$$$
Lean4
@[norm_cast]
theorem cast_divInt_of_ne_zero (a : ℤ) {b : ℤ} (b0 : (b : α) ≠ 0) : (a /. b : α) = a / b :=
by
have b0' : b ≠ 0 := by
refine mt ?_ b0
simp +contextual
rcases e : a /. b with ⟨n, d, h, c⟩
have d0 : (d : α) ≠ 0 := by
intro d0
have dd := den_dvd a b
rcases show (d : ℤ) ∣ b by rwa [e] at dd with ⟨k, ke⟩
have : (b : α) = (d : α) * (k : α) := by rw [ke, Int.cast_mul, Int.cast_natCast]
rw [d0, zero_mul] at this
contradiction
rw [mk'_eq_divInt] at e
have := congr_arg ((↑) : ℤ → α) ((divInt_eq_divInt_iff b0' <| ne_of_gt <| Int.natCast_pos.2 h.bot_lt).1 e)
rw [Int.cast_mul, Int.cast_mul, Int.cast_natCast] at this
rw [eq_comm, cast_def, div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq, ← mul_assoc, this,
mul_assoc, mul_inv_cancel₀ b0, mul_one]
