case pos
n : ℤ
hn : n = 0
⊢ ↑(n / n) = ↑n / ↑n

case neg
n : ℤ
hn : ¬n = 0
⊢ ↑(n / n) = ↑n / ↑n
n : ℤ
⊢ ↑(n / n) = ↑n / ↑n
by_cases hn : n = 0
case pos

⊢ ↑(0 / 0) = ↑0 / ↑0
case pos
n : ℤ
hn : n = 0
⊢ ↑(n / n) = ↑n / ↑n
subst hn
no goals
case pos

⊢ ↑(0 / 0) = ↑0 / ↑0
simp only [Int.cast_zero, Int.zero_div, zero_div]
case neg
n : ℤ
hn : ¬n = 0
this : ↑n ≠ 0
⊢ ↑(n / n) = ↑n / ↑n
case neg
n : ℤ
hn : ¬n = 0
⊢ ↑(n / n) = ↑n / ↑n
have : (n : ℚ) ≠ 0 := by rwa [← coe_int_inj] at hn
no goals
case neg
n : ℤ
hn : ¬n = 0
this : ↑n ≠ 0
⊢ ↑(n / n) = ↑n / ↑n
simp only [Int.ediv_self hn, Int.cast_one, Ne.def, not_false_iff, div_self this]
no goals
n : ℤ
hn : ¬n = 0
⊢ ↑n ≠ 0
rwa [← coe_int_inj] at hn