Theorem: monom_coords_at_zero (UnitConjecture/FreeModule.lean)

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x₀ x : X
⊢ monomCoeff R X x₀ (0, x) = 0
Tactic:
rw [monomCoeff]
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x₀ x : X
⊢ (match (0, x).2 == x₀ with
    | true => (0, x).1
    | false => 0) =
    0

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x₀ x : X
⊢ (match (0, x).2 == x₀ with
    | true => (0, x).1
    | false => 0) =
    0
Tactic:
cases x == x₀ <;> rfl
State after:
no goals