case refine'_3
d : Nat
n : Int
d0 : d ≠ 0
this : normalize ?refine'_1 d = normalize ?refine'_2 1 ↔ ?refine'_1 * ↑1 = ?refine'_2 * ↑d
⊢ normalize n d = 0 ↔ n = 0

case refine'_1
d : Nat
n : Int
d0 : d ≠ 0
⊢ Int

case refine'_2
d : Nat
n : Int
d0 : d ≠ 0
⊢ Int
d : Nat
n : Int
d0 : d ≠ 0
⊢ normalize n d = 0 ↔ n = 0
have' := normalize_eq_iff d0 Nat.one_ne_zero
case refine'_3
d : Nat
n : Int
d0 : d ≠ 0
this : normalize ?refine'_1 d = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d
⊢ normalize n d = 0 ↔ n = 0

case refine'_1
d : Nat
n : Int
d0 : d ≠ 0
⊢ Int

case refine'_1
d : Nat
n : Int
d0 : d ≠ 0
⊢ Int
case refine'_3
d : Nat
n : Int
d0 : d ≠ 0
this : normalize ?refine'_1 d = normalize ?refine'_2 1 ↔ ?refine'_1 * ↑1 = ?refine'_2 * ↑d
⊢ normalize n d = 0 ↔ n = 0

case refine'_1
d : Nat
n : Int
d0 : d ≠ 0
⊢ Int

case refine'_2
d : Nat
n : Int
d0 : d ≠ 0
⊢ Int
rw [normalize_zero (d := 1)] at this
case refine'_3
d : Nat
n : Int
d0 : d ≠ 0
this : normalize n d = 0 ↔ n * ↑1 = 0 * ↑d
⊢ n * ↑1 = 0 * ↑d ↔ n = 0
case refine'_3
d : Nat
n : Int
d0 : d ≠ 0
this : normalize ?refine'_1 d = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d
⊢ normalize n d = 0 ↔ n = 0

case refine'_1
d : Nat
n : Int
d0 : d ≠ 0
⊢ Int

case refine'_1
d : Nat
n : Int
d0 : d ≠ 0
⊢ Int
rw [this]
no goals
case refine'_3
d : Nat
n : Int
d0 : d ≠ 0
this : normalize n d = 0 ↔ n * ↑1 = 0 * ↑d
⊢ n * ↑1 = 0 * ↑d ↔ n = 0
simp