R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Field R
p q : R[X]
u : R[X]ˣ
n : ℕ
⊢ (1 / if n = 0 then coeff (↑u) 0 else 0) = if n = 0 then coeff (↑u⁻¹) 0 else 0
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Field R
p q : R[X]
u : R[X]ˣ
n : ℕ
⊢ (coeff (↑u) n)⁻¹ = coeff (↑u⁻¹) n
rw [eq_C_of_degree_eq_zero (degree_coe_units u), eq_C_of_degree_eq_zero (degree_coe_units u⁻¹),
  coeff_C, coeff_C, inv_eq_one_div]
case inl
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Field R
p q : R[X]
u : R[X]ˣ
n : ℕ
h✝ : n = 0
⊢ 1 / coeff (↑u) 0 = coeff (↑u⁻¹) 0

case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Field R
p q : R[X]
u : R[X]ˣ
n : ℕ
h✝ : ¬n = 0
⊢ 1 / 0 = 0
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Field R
p q : R[X]
u : R[X]ˣ
n : ℕ
⊢ (1 / if n = 0 then coeff (↑u) 0 else 0) = if n = 0 then coeff (↑u⁻¹) 0 else 0
split_ifs
case inl
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Field R
p q : R[X]
u : R[X]ˣ
n : ℕ
h✝ : n = 0
⊢ eval 0 ↑1 = 1
case inl
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Field R
p q : R[X]
u : R[X]ˣ
n : ℕ
h✝ : n = 0
⊢ 1 / coeff (↑u) 0 = coeff (↑u⁻¹) 0
rw [div_eq_iff_mul_eq (coeff_coe_units_zero_ne_zero u), coeff_zero_eq_eval_zero,
    coeff_zero_eq_eval_zero, ← eval_mul, ← Units.val_mul, inv_mul_self]
no goals
case inl
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Field R
p q : R[X]
u : R[X]ˣ
n : ℕ
h✝ : n = 0
⊢ eval 0 ↑1 = 1
simp
no goals
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Field R
p q : R[X]
u : R[X]ˣ
n : ℕ
h✝ : ¬n = 0
⊢ 1 / 0 = 0
simp