Theorem: FormalSum.act_sum (UnitConjecture/FreeModule.lean)

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
s : FormalSum R X
⊢ scmul a s ++ scmul b s ≈ scmul (a + b) s
Tactic:
induction s with
| nil =>
  simp [scmul]
  apply eqlCoords.refl
| cons h t ih =>
  apply funext; intro x₀
  let il₁ := congrFun ih x₀    
  rw [← append_coords]
  simp [scmul, coords, right_distrib, monom_coords_hom]
  rw [← append_coords] at il₁ 
  rw [← il₁]
  conv =>
    lhs
    rw [add_assoc]
    arg 2
    rw [← add_assoc]
    arg 1
    rw [add_comm]
  conv =>
    lhs
    rw [add_assoc]
    rw [← add_assoc]
State after:
no goals

State before:
case nil
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
⊢ scmul a [] ++ scmul b [] ≈ scmul (a + b) []
Tactic:
simp [scmul]
State after:
case nil
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
⊢ [] ≈ []

State before:
case nil
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
⊢ [] ≈ []
Tactic:
apply eqlCoords.refl
State after:
no goals

State before:
case cons
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
⊢ scmul a (h :: t) ++ scmul b (h :: t) ≈ scmul (a + b) (h :: t)
Tactic:
apply funext
State after:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
⊢ ∀ (x : X), coords (scmul a (h :: t) ++ scmul b (h :: t)) x = coords (scmul (a + b) (h :: t)) x

State before:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
⊢ ∀ (x : X), coords (scmul a (h :: t) ++ scmul b (h :: t)) x = coords (scmul (a + b) (h :: t)) x
Tactic:
intro x₀
State after:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
⊢ coords (scmul a (h :: t) ++ scmul b (h :: t)) x₀ = coords (scmul (a + b) (h :: t)) x₀

State before:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
⊢ coords (scmul a (h :: t) ++ scmul b (h :: t)) x₀ = coords (scmul (a + b) (h :: t)) x₀
Tactic:
let il₁ := congrFun ih x₀
State after:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t ++ scmul b t) x₀ = coords (scmul (a + b) t) x₀ := congrFun ih x₀
⊢ coords (scmul a (h :: t) ++ scmul b (h :: t)) x₀ = coords (scmul (a + b) (h :: t)) x₀

State before:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t ++ scmul b t) x₀ = coords (scmul (a + b) t) x₀ := congrFun ih x₀
⊢ coords (scmul a (h :: t) ++ scmul b (h :: t)) x₀ = coords (scmul (a + b) (h :: t)) x₀
Tactic:
rw [← append_coords]
State after:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t ++ scmul b t) x₀ = coords (scmul (a + b) t) x₀ := congrFun ih x₀
⊢ coords (scmul a (h :: t)) x₀ + coords (scmul b (h :: t)) x₀ = coords (scmul (a + b) (h :: t)) x₀

State before:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t ++ scmul b t) x₀ = coords (scmul (a + b) t) x₀ := congrFun ih x₀
⊢ coords (scmul a (h :: t)) x₀ + coords (scmul b (h :: t)) x₀ = coords (scmul (a + b) (h :: t)) x₀
Tactic:
simp [scmul, coords, right_distrib, monom_coords_hom]
State after:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t ++ scmul b t) x₀ = coords (scmul (a + b) t) x₀ := congrFun ih x₀
⊢ monomCoeff R X x₀ (a * h.1, h.2) + coords (scmul a t) x₀ +
      (monomCoeff R X x₀ (b * h.1, h.2) + coords (scmul b t) x₀) =
    monomCoeff R X x₀ (a * h.1, h.2) + monomCoeff R X x₀ (b * h.1, h.2) + coords (scmul (a + b) t) x₀

State before:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t ++ scmul b t) x₀ = coords (scmul (a + b) t) x₀ := congrFun ih x₀
⊢ monomCoeff R X x₀ (a * h.1, h.2) + coords (scmul a t) x₀ +
      (monomCoeff R X x₀ (b * h.1, h.2) + coords (scmul b t) x₀) =
    monomCoeff R X x₀ (a * h.1, h.2) + monomCoeff R X x₀ (b * h.1, h.2) + coords (scmul (a + b) t) x₀
Tactic:
rw [← append_coords] at il₁
State after:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t) x₀ + coords (scmul b t) x₀ = coords (scmul (a + b) t) x₀
⊢ monomCoeff R X x₀ (a * h.1, h.2) + coords (scmul a t) x₀ +
      (monomCoeff R X x₀ (b * h.1, h.2) + coords (scmul b t) x₀) =
    monomCoeff R X x₀ (a * h.1, h.2) + monomCoeff R X x₀ (b * h.1, h.2) + coords (scmul (a + b) t) x₀

State before:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t) x₀ + coords (scmul b t) x₀ = coords (scmul (a + b) t) x₀
⊢ monomCoeff R X x₀ (a * h.1, h.2) + coords (scmul a t) x₀ +
      (monomCoeff R X x₀ (b * h.1, h.2) + coords (scmul b t) x₀) =
    monomCoeff R X x₀ (a * h.1, h.2) + monomCoeff R X x₀ (b * h.1, h.2) + coords (scmul (a + b) t) x₀
Tactic:
rw [← il₁]
State after:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t) x₀ + coords (scmul b t) x₀ = coords (scmul (a + b) t) x₀
⊢ monomCoeff R X x₀ (a * h.1, h.2) + coords (scmul a t) x₀ +
      (monomCoeff R X x₀ (b * h.1, h.2) + coords (scmul b t) x₀) =
    monomCoeff R X x₀ (a * h.1, h.2) + monomCoeff R X x₀ (b * h.1, h.2) +
      (coords (scmul a t) x₀ + coords (scmul b t) x₀)

State before:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t) x₀ + coords (scmul b t) x₀ = coords (scmul (a + b) t) x₀
⊢ monomCoeff R X x₀ (a * h.1, h.2) + coords (scmul a t) x₀ +
      (monomCoeff R X x₀ (b * h.1, h.2) + coords (scmul b t) x₀) =
    monomCoeff R X x₀ (a * h.1, h.2) + monomCoeff R X x₀ (b * h.1, h.2) +
      (coords (scmul a t) x₀ + coords (scmul b t) x₀)
Tactic:
conv =>
  lhs
  rw [add_assoc]
  arg 2
  rw [← add_assoc]
  arg 1
  rw [add_comm]
State after:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t) x₀ + coords (scmul b t) x₀ = coords (scmul (a + b) t) x₀
⊢ monomCoeff R X x₀ (a * h.1, h.2) +
      (monomCoeff R X x₀ (b * h.1, h.2) + coords (scmul a t) x₀ + coords (scmul b t) x₀) =
    monomCoeff R X x₀ (a * h.1, h.2) + monomCoeff R X x₀ (b * h.1, h.2) +
      (coords (scmul a t) x₀ + coords (scmul b t) x₀)

State before:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t) x₀ + coords (scmul b t) x₀ = coords (scmul (a + b) t) x₀
⊢ monomCoeff R X x₀ (a * h.1, h.2) +
      (monomCoeff R X x₀ (b * h.1, h.2) + coords (scmul a t) x₀ + coords (scmul b t) x₀) =
    monomCoeff R X x₀ (a * h.1, h.2) + monomCoeff R X x₀ (b * h.1, h.2) +
      (coords (scmul a t) x₀ + coords (scmul b t) x₀)
Tactic:
conv =>
  lhs
  rw [add_assoc]
  rw [← add_assoc]
State after:
no goals