Theorem: monom_coords_mul (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
a b : R
⊢ monomCoeff R X x₀ (a * b, x) = a * monomCoeff R X x₀ (b, x)
Tactic:
repeat
  (
    rw [monomCoeff])
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x x₀ : X
a b : R
⊢ (match (a * b, x).2 == x₀ with
    | true => (a * b, x).1
    | false => 0) =
    a *
      match (b, x).2 == x₀ with
      | true => (b, x).1
      | false => 0

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

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x x₀ : X
a b : R
⊢ (match (a * b, x).2 == x₀ with
    | true => (a * b, x).1
    | false => 0) =
    a * monomCoeff R X x₀ (b, x)
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
a b : R
⊢ (match (a * b, x).2 == x₀ with
    | true => (a * b, x).1
    | false => 0) =
    a *
      match (b, x).2 == x₀ with
      | true => (b, x).1
      | false => 0

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x x₀ : X
a b : R
⊢ (match (a * b, x).2 == x₀ with
    | true => (a * b, x).1
    | false => 0) =
    a * monomCoeff R X x₀ (b, x)
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
a b : R
⊢ (match (a * b, x).2 == x₀ with
    | true => (a * b, x).1
    | false => 0) =
    a *
      match (b, x).2 == x₀ with
      | true => (b, x).1
      | false => 0