Theorem: monom_coords_hom (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) = monomCoeff R X x₀ (a, x) + 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) =
    (match (a, x).2 == x₀ with
      | true => (a, x).1
      | false => 0) +
      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) =
    (match (a, x).2 == x₀ with
      | true => (a, x).1
      | false => 0) +
      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) =
    (match (a, x).2 == x₀ with
      | true => (a, x).1
      | false => 0) +
      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) =
    (match (a, x).2 == x₀ with
      | true => (a, x).1
      | false => 0) +
      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) =
    (match (a, x).2 == x₀ with
      | true => (a, x).1
      | false => 0) +
      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) =
    (match (a, x).2 == x₀ with
      | true => (a, x).1
      | false => 0) +
      match (b, x).2 == x₀ with
      | true => (b, x).1
      | false => 0