[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ a * a = 0 ↔
    ∀ (x y : R),
      ↑(↑(LinearEquiv.toEquiv (LinearEquiv.symm (LinearMap.ringLmapEquivSelf R ℕ A))) a) x *
          ↑(↑(LinearEquiv.toEquiv (LinearEquiv.symm (LinearMap.ringLmapEquivSelf R ℕ A))) a) y =
        0
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ a * a = 0 ↔ ∀ (x y : R), x • a * y • a = 0
[PROOFSTEP]
simp_rw [smul_mul_smul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ a * a = 0 ↔ ∀ (x y : R), (x * y) • (a * a) = 0
[PROOFSTEP]
refine' ⟨fun h x y => h.symm ▸ smul_zero _, fun h => by simpa using h 1 1⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : ∀ (x y : R), (x * y) • (a * a) = 0
⊢ a * a = 0
[PROOFSTEP]
simpa using h 1 1
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
e : { e // e * e = 0 }
⊢ ↑(↑lift e) ε = ↑e
[PROOFSTEP]
simp only [lift_apply_apply, fst_eps, map_zero, snd_eps, one_smul, zero_add]


[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
x✝ : ℕ
n : ℕ := x✝
h : ¬n < E.order
k : Fin E.order
⊢ n - E.order + ↑k < n
[PROOFSTEP]
rw [add_comm, ← add_tsub_assoc_of_le (not_lt.mp h), tsub_lt_iff_left]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
x✝ : ℕ
n : ℕ := x✝
h : ¬n < E.order
k : Fin E.order
⊢ ↑k + n < E.order + n
[PROOFSTEP]
exact add_lt_add_right k.is_lt n
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
x✝ : ℕ
n : ℕ := x✝
h : ¬n < E.order
k : Fin E.order
⊢ E.order ≤ ↑k + n
[PROOFSTEP]
convert add_le_add (zero_le (k : ℕ)) (not_lt.mp h)
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
x✝ : ℕ
n : ℕ := x✝
h : ¬n < E.order
k : Fin E.order
⊢ E.order = 0 + E.order
[PROOFSTEP]
simp only [zero_add]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
⊢ IsSolution E (mkSol E init)
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : ℕ
⊢ mkSol E init (n + E.order) = ∑ i : Fin E.order, coeffs E i * mkSol E init (n + ↑i)
[PROOFSTEP]
rw [mkSol]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : ℕ
⊢ (if h : n + E.order < E.order then init { val := n + E.order, isLt := h }
    else
      ∑ k : Fin E.order,
        let_fun x := (_ : n + E.order - E.order + ↑k < n + E.order);
        coeffs E k * mkSol E init (n + E.order - E.order + ↑k)) =
    ∑ i : Fin E.order, coeffs E i * mkSol E init (n + ↑i)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
⊢ ∀ (n : Fin E.order), mkSol E init ↑n = init n
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : Fin E.order
⊢ mkSol E init ↑n = init n
[PROOFSTEP]
rw [mkSol]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : Fin E.order
⊢ (if h : ↑n < E.order then init { val := ↑n, isLt := h }
    else
      ∑ k : Fin E.order,
        let_fun x := (_ : ↑n - E.order + ↑k < ↑n);
        coeffs E k * mkSol E init (↑n - E.order + ↑k)) =
    init n
[PROOFSTEP]
simp only [n.is_lt, dif_pos, Fin.mk_val, Fin.eta]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
⊢ ∀ (n : ℕ), u n = mkSol E init n
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
⊢ u n = mkSol E init n
[PROOFSTEP]
rw [mkSol]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
⊢ u n =
    if h : n < E.order then init { val := n, isLt := h }
    else
      ∑ k : Fin E.order,
        let_fun x := (_ : n - E.order + ↑k < n);
        coeffs E k * mkSol E init (n - E.order + ↑k)
[PROOFSTEP]
split_ifs with h'
[GOAL]
case pos
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : n < E.order
⊢ u n = init { val := n, isLt := h' }
[PROOFSTEP]
exact_mod_cast heq ⟨n, h'⟩
[GOAL]
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ u n =
    ∑ k : Fin E.order,
      let_fun x := (_ : n - E.order + ↑k < n);
      coeffs E k * mkSol E init (n - E.order + ↑k)
[PROOFSTEP]
simp only
[GOAL]
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ u n = ∑ x : Fin E.order, coeffs E x * mkSol E init (n - E.order + ↑x)
[PROOFSTEP]
rw [← tsub_add_cancel_of_le (le_of_not_lt h'), h (n - E.order)]
[GOAL]
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ ∑ i : Fin E.order, coeffs E i * u (n - E.order + ↑i) =
    ∑ x : Fin E.order, coeffs E x * mkSol E init (n - E.order + E.order - E.order + ↑x)
[PROOFSTEP]
congr with k
[GOAL]
case neg.e_f.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ coeffs E k * u (n - E.order + ↑k) = coeffs E k * mkSol E init (n - E.order + E.order - E.order + ↑k)
[PROOFSTEP]
have : n - E.order + k < n :=
  by
  rw [add_comm, ← add_tsub_assoc_of_le (not_lt.mp h'), tsub_lt_iff_left]
  · exact add_lt_add_right k.is_lt n
  · convert add_le_add (zero_le (k : ℕ)) (not_lt.mp h')
    simp only [zero_add]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ n - E.order + ↑k < n
[PROOFSTEP]
rw [add_comm, ← add_tsub_assoc_of_le (not_lt.mp h'), tsub_lt_iff_left]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ ↑k + n < E.order + n
[PROOFSTEP]
exact add_lt_add_right k.is_lt n
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ E.order ≤ ↑k + n
[PROOFSTEP]
convert add_le_add (zero_le (k : ℕ)) (not_lt.mp h')
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ E.order = 0 + E.order
[PROOFSTEP]
simp only [zero_add]
[GOAL]
case neg.e_f.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
this : n - E.order + ↑k < n
⊢ coeffs E k * u (n - E.order + ↑k) = coeffs E k * mkSol E init (n - E.order + E.order - E.order + ↑k)
[PROOFSTEP]
rw [eq_mk_of_is_sol_of_eq_init h heq (n - E.order + k)]
[GOAL]
case neg.e_f.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
this : n - E.order + ↑k < n
⊢ coeffs E k * mkSol E (fun n => init n) (n - E.order + ↑k) =
    coeffs E k * mkSol E init (n - E.order + E.order - E.order + ↑k)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : u ∈ {u | IsSolution E u}
hv : v ∈ {u | IsSolution E u}
n : ℕ
⊢ (u + v) (n + E.order) = ∑ i : Fin E.order, coeffs E i * (u + v) (n + ↑i)
[PROOFSTEP]
simp [mul_add, sum_add_distrib, hu n, hv n]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
n : ℕ
⊢ OfNat.ofNat 0 (n + E.order) = ∑ i : Fin E.order, coeffs E i * OfNat.ofNat 0 (n + ↑i)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
a : α
u : ℕ → α
hu :
  u ∈
    {
          toAddSubsemigroup :=
            { carrier := {u | IsSolution E u},
              add_mem' :=
                (_ :
                  ∀ {u v : ℕ → α},
                    u ∈ {u | IsSolution E u} →
                      v ∈ {u | IsSolution E u} →
                        ∀ (n : ℕ),
                          u (n + E.order) + v (n + E.order) = ∑ i : Fin E.order, coeffs E i * (u + v) (n + ↑i)) },
          zero_mem' :=
            (_ : ∀ (n : ℕ), 0 = ∑ i : Fin E.order, coeffs E i * OfNat.ofNat 0 (n + ↑i)) }.toAddSubsemigroup.carrier
n : ℕ
⊢ (a • u) (n + E.order) = ∑ i : Fin E.order, coeffs E i * (a • u) (n + ↑i)
[PROOFSTEP]
simp [hu n, mul_sum]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
a : α
u : ℕ → α
hu :
  u ∈
    {
          toAddSubsemigroup :=
            { carrier := {u | IsSolution E u},
              add_mem' :=
                (_ :
                  ∀ {u v : ℕ → α},
                    u ∈ {u | IsSolution E u} →
                      v ∈ {u | IsSolution E u} →
                        ∀ (n : ℕ),
                          u (n + E.order) + v (n + E.order) = ∑ i : Fin E.order, coeffs E i * (u + v) (n + ↑i)) },
          zero_mem' :=
            (_ : ∀ (n : ℕ), 0 = ∑ i : Fin E.order, coeffs E i * OfNat.ofNat 0 (n + ↑i)) }.toAddSubsemigroup.carrier
n : ℕ
⊢ ∑ x : Fin E.order, a * (coeffs E x * u (n + ↑x)) = ∑ x : Fin E.order, coeffs E x * (a * u (n + ↑x))
[PROOFSTEP]
congr
[GOAL]
case e_f
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
a : α
u : ℕ → α
hu :
  u ∈
    {
          toAddSubsemigroup :=
            { carrier := {u | IsSolution E u},
              add_mem' :=
                (_ :
                  ∀ {u v : ℕ → α},
                    u ∈ {u | IsSolution E u} →
                      v ∈ {u | IsSolution E u} →
                        ∀ (n : ℕ),
                          u (n + E.order) + v (n + E.order) = ∑ i : Fin E.order, coeffs E i * (u + v) (n + ↑i)) },
          zero_mem' :=
            (_ : ∀ (n : ℕ), 0 = ∑ i : Fin E.order, coeffs E i * OfNat.ofNat 0 (n + ↑i)) }.toAddSubsemigroup.carrier
n : ℕ
⊢ (fun x => a * (coeffs E x * u (n + ↑x))) = fun x => coeffs E x * (a * u (n + ↑x))
[PROOFSTEP]
ext
[GOAL]
case e_f.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
a : α
u : ℕ → α
hu :
  u ∈
    {
          toAddSubsemigroup :=
            { carrier := {u | IsSolution E u},
              add_mem' :=
                (_ :
                  ∀ {u v : ℕ → α},
                    u ∈ {u | IsSolution E u} →
                      v ∈ {u | IsSolution E u} →
                        ∀ (n : ℕ),
                          u (n + E.order) + v (n + E.order) = ∑ i : Fin E.order, coeffs E i * (u + v) (n + ↑i)) },
          zero_mem' :=
            (_ : ∀ (n : ℕ), 0 = ∑ i : Fin E.order, coeffs E i * OfNat.ofNat 0 (n + ↑i)) }.toAddSubsemigroup.carrier
n : ℕ
x✝ : Fin E.order
⊢ a * (coeffs E x✝ * u (n + ↑x✝)) = coeffs E x✝ * (a * u (n + ↑x✝))
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : { x // x ∈ solSpace E }
⊢ (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : { x // x ∈ solSpace E }
x✝ : Fin E.order
⊢ (fun u x => ↑u ↑x) (u + v) x✝ = ((fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
a : α
u : { x // x ∈ solSpace E }
⊢ AddHom.toFun
      { toFun := fun u x => ↑u ↑x,
        map_add' :=
          (_ :
            ∀ (u v : { x // x ∈ solSpace E }),
              (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
      (a • u) =
    ↑(RingHom.id α) a •
      AddHom.toFun
        { toFun := fun u x => ↑u ↑x,
          map_add' :=
            (_ :
              ∀ (u v : { x // x ∈ solSpace E }),
                (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
        u
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
a : α
u : { x // x ∈ solSpace E }
x✝ : Fin E.order
⊢ AddHom.toFun
      { toFun := fun u x => ↑u ↑x,
        map_add' :=
          (_ :
            ∀ (u v : { x // x ∈ solSpace E }),
              (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
      (a • u) x✝ =
    (↑(RingHom.id α) a •
        AddHom.toFun
          { toFun := fun u x => ↑u ↑x,
            map_add' :=
              (_ :
                ∀ (u v : { x // x ∈ solSpace E }),
                  (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
          u)
      x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : { x // x ∈ solSpace E }
⊢ (fun u => { val := mkSol E u, property := (_ : IsSolution E (mkSol E u)) })
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun u x => ↑u ↑x,
                map_add' :=
                  (_ :
                    ∀ (u v : { x // x ∈ solSpace E }),
                      (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) },
            map_smul' :=
              (_ :
                ∀ (a : α) (u : { x // x ∈ solSpace E }),
                  AddHom.toFun
                      { toFun := fun u x => ↑u ↑x,
                        map_add' :=
                          (_ :
                            ∀ (u v : { x // x ∈ solSpace E }),
                              (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                      (a • u) =
                    ↑(RingHom.id α) a •
                      AddHom.toFun
                        { toFun := fun u x => ↑u ↑x,
                          map_add' :=
                            (_ :
                              ∀ (u v : { x // x ∈ solSpace E }),
                                (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                        u) }.toAddHom
        u) =
    u
[PROOFSTEP]
ext n
[GOAL]
case a.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : { x // x ∈ solSpace E }
n : ℕ
⊢ ↑((fun u => { val := mkSol E u, property := (_ : IsSolution E (mkSol E u)) })
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun u x => ↑u ↑x,
                    map_add' :=
                      (_ :
                        ∀ (u v : { x // x ∈ solSpace E }),
                          (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) },
                map_smul' :=
                  (_ :
                    ∀ (a : α) (u : { x // x ∈ solSpace E }),
                      AddHom.toFun
                          { toFun := fun u x => ↑u ↑x,
                            map_add' :=
                              (_ :
                                ∀ (u v : { x // x ∈ solSpace E }),
                                  (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                          (a • u) =
                        ↑(RingHom.id α) a •
                          AddHom.toFun
                            { toFun := fun u x => ↑u ↑x,
                              map_add' :=
                                (_ :
                                  ∀ (u v : { x // x ∈ solSpace E }),
                                    (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                            u) }.toAddHom
            u))
      n =
    ↑u n
[PROOFSTEP]
symm
[GOAL]
case a.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : { x // x ∈ solSpace E }
n : ℕ
⊢ ↑u n =
    ↑((fun u => { val := mkSol E u, property := (_ : IsSolution E (mkSol E u)) })
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun u x => ↑u ↑x,
                    map_add' :=
                      (_ :
                        ∀ (u v : { x // x ∈ solSpace E }),
                          (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) },
                map_smul' :=
                  (_ :
                    ∀ (a : α) (u : { x // x ∈ solSpace E }),
                      AddHom.toFun
                          { toFun := fun u x => ↑u ↑x,
                            map_add' :=
                              (_ :
                                ∀ (u v : { x // x ∈ solSpace E }),
                                  (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                          (a • u) =
                        ↑(RingHom.id α) a •
                          AddHom.toFun
                            { toFun := fun u x => ↑u ↑x,
                              map_add' :=
                                (_ :
                                  ∀ (u v : { x // x ∈ solSpace E }),
                                    (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                            u) }.toAddHom
            u))
      n
[PROOFSTEP]
apply E.eq_mk_of_is_sol_of_eq_init u.2
[GOAL]
case a.h.heq
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : { x // x ∈ solSpace E }
n : ℕ
⊢ ∀ (n : Fin E.order),
    ↑u ↑n =
      AddHom.toFun
        {
            toAddHom :=
              { toFun := fun u x => ↑u ↑x,
                map_add' :=
                  (_ :
                    ∀ (u v : { x // x ∈ solSpace E }),
                      (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) },
            map_smul' :=
              (_ :
                ∀ (a : α) (u : { x // x ∈ solSpace E }),
                  AddHom.toFun
                      { toFun := fun u x => ↑u ↑x,
                        map_add' :=
                          (_ :
                            ∀ (u v : { x // x ∈ solSpace E }),
                              (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                      (a • u) =
                    ↑(RingHom.id α) a •
                      AddHom.toFun
                        { toFun := fun u x => ↑u ↑x,
                          map_add' :=
                            (_ :
                              ∀ (u v : { x // x ∈ solSpace E }),
                                (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                        u) }.toAddHom
        u n
[PROOFSTEP]
intro k
[GOAL]
case a.h.heq
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : { x // x ∈ solSpace E }
n : ℕ
k : Fin E.order
⊢ ↑u ↑k =
    AddHom.toFun
      {
          toAddHom :=
            { toFun := fun u x => ↑u ↑x,
              map_add' :=
                (_ :
                  ∀ (u v : { x // x ∈ solSpace E }),
                    (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) },
          map_smul' :=
            (_ :
              ∀ (a : α) (u : { x // x ∈ solSpace E }),
                AddHom.toFun
                    { toFun := fun u x => ↑u ↑x,
                      map_add' :=
                        (_ :
                          ∀ (u v : { x // x ∈ solSpace E }),
                            (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                    (a • u) =
                  ↑(RingHom.id α) a •
                    AddHom.toFun
                      { toFun := fun u x => ↑u ↑x,
                        map_add' :=
                          (_ :
                            ∀ (u v : { x // x ∈ solSpace E }),
                              (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                      u) }.toAddHom
      u k
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
⊢ u = v ↔ Set.EqOn u v ↑(range E.order)
[PROOFSTEP]
refine' Iff.intro (fun h x _ ↦ h ▸ rfl) _
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
⊢ Set.EqOn u v ↑(range E.order) → u = v
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
⊢ u = v
[PROOFSTEP]
set u' : ↥E.solSpace := ⟨u, hu⟩
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
⊢ u = v
[PROOFSTEP]
set v' : ↥E.solSpace := ⟨v, hv⟩
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
v' : { x // x ∈ solSpace E } := { val := v, property := hv }
⊢ u = v
[PROOFSTEP]
change u'.val = v'.val
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
v' : { x // x ∈ solSpace E } := { val := v, property := hv }
⊢ ↑u' = ↑v'
[PROOFSTEP]
suffices h' : u' = v'
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
v' : { x // x ∈ solSpace E } := { val := v, property := hv }
h' : u' = v'
⊢ ↑u' = ↑v'
case h'
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
v' : { x // x ∈ solSpace E } := { val := v, property := hv }
⊢ u' = v'
[PROOFSTEP]
exact h' ▸ rfl
[GOAL]
case h'
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
v' : { x // x ∈ solSpace E } := { val := v, property := hv }
⊢ u' = v'
[PROOFSTEP]
rw [← E.toInit.toEquiv.apply_eq_iff_eq, LinearEquiv.coe_toEquiv]
[GOAL]
case h'
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
v' : { x // x ∈ solSpace E } := { val := v, property := hv }
⊢ ↑(toInit E) u' = ↑(toInit E) v'
[PROOFSTEP]
ext x
[GOAL]
case h'.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
v' : { x // x ∈ solSpace E } := { val := v, property := hv }
x : Fin E.order
⊢ ↑(toInit E) u' x = ↑(toInit E) v' x
[PROOFSTEP]
exact_mod_cast h (mem_range.mpr x.2)
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x y : Fin E.order → α
⊢ (fun X i => if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i)
      (x + y) =
    (fun X i => if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i)
        x +
      (fun X i => if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i)
        y
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x y : Fin E.order → α
i : Fin E.order
⊢ (fun X i => if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i)
      (x + y) i =
    ((fun X i => if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i)
          x +
        (fun X i =>
            if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i)
          y)
      i
[PROOFSTEP]
simp only
[GOAL]
case h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x y : Fin E.order → α
i : Fin E.order
⊢ (if h : ↑i + 1 < E.order then (x + y) { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * (x + y) i) =
    ((fun i => if h : ↑i + 1 < E.order then x { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * x i) +
        fun i => if h : ↑i + 1 < E.order then y { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * y i)
      i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x y : Fin E.order → α
i : Fin E.order
h : ↑i + 1 < E.order
⊢ (x + y) { val := ↑i + 1, isLt := h } =
    ((fun i => if h : ↑i + 1 < E.order then x { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * x i) +
        fun i => if h : ↑i + 1 < E.order then y { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * y i)
      i
[PROOFSTEP]
simp [h, mul_add, sum_add_distrib]
[GOAL]
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x y : Fin E.order → α
i : Fin E.order
h : ¬↑i + 1 < E.order
⊢ ∑ i : Fin E.order, coeffs E i * (x + y) i =
    ((fun i => if h : ↑i + 1 < E.order then x { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * x i) +
        fun i => if h : ↑i + 1 < E.order then y { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * y i)
      i
[PROOFSTEP]
simp [h, mul_add, sum_add_distrib]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x : α
y : Fin E.order → α
⊢ AddHom.toFun
      {
        toFun := fun X i =>
          if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i,
        map_add' :=
          (_ :
            ∀ (x y : Fin E.order → α),
              (fun X i =>
                    if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                    else ∑ i : Fin E.order, coeffs E i * X i)
                  (x + y) =
                (fun X i =>
                      if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                      else ∑ i : Fin E.order, coeffs E i * X i)
                    x +
                  (fun X i =>
                      if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                      else ∑ i : Fin E.order, coeffs E i * X i)
                    y) }
      (x • y) =
    ↑(RingHom.id α) x •
      AddHom.toFun
        {
          toFun := fun X i =>
            if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i,
          map_add' :=
            (_ :
              ∀ (x y : Fin E.order → α),
                (fun X i =>
                      if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                      else ∑ i : Fin E.order, coeffs E i * X i)
                    (x + y) =
                  (fun X i =>
                        if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                        else ∑ i : Fin E.order, coeffs E i * X i)
                      x +
                    (fun X i =>
                        if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                        else ∑ i : Fin E.order, coeffs E i * X i)
                      y) }
        y
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x : α
y : Fin E.order → α
i : Fin E.order
⊢ AddHom.toFun
      {
        toFun := fun X i =>
          if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i,
        map_add' :=
          (_ :
            ∀ (x y : Fin E.order → α),
              (fun X i =>
                    if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                    else ∑ i : Fin E.order, coeffs E i * X i)
                  (x + y) =
                (fun X i =>
                      if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                      else ∑ i : Fin E.order, coeffs E i * X i)
                    x +
                  (fun X i =>
                      if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                      else ∑ i : Fin E.order, coeffs E i * X i)
                    y) }
      (x • y) i =
    (↑(RingHom.id α) x •
        AddHom.toFun
          {
            toFun := fun X i =>
              if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i,
            map_add' :=
              (_ :
                ∀ (x y : Fin E.order → α),
                  (fun X i =>
                        if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                        else ∑ i : Fin E.order, coeffs E i * X i)
                      (x + y) =
                    (fun X i =>
                          if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                          else ∑ i : Fin E.order, coeffs E i * X i)
                        x +
                      (fun X i =>
                          if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                          else ∑ i : Fin E.order, coeffs E i * X i)
                        y) }
          y)
      i
[PROOFSTEP]
simp only
[GOAL]
case h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x : α
y : Fin E.order → α
i : Fin E.order
⊢ (if h : ↑i + 1 < E.order then (x • y) { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * (x • y) i) =
    (↑(RingHom.id α) x • fun i =>
        if h : ↑i + 1 < E.order then y { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * y i)
      i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x : α
y : Fin E.order → α
i : Fin E.order
h : ↑i + 1 < E.order
⊢ (x • y) { val := ↑i + 1, isLt := h } =
    (↑(RingHom.id α) x • fun i =>
        if h : ↑i + 1 < E.order then y { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * y i)
      i
[PROOFSTEP]
simp [h, mul_sum]
[GOAL]
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x : α
y : Fin E.order → α
i : Fin E.order
h : ¬↑i + 1 < E.order
⊢ ∑ i : Fin E.order, coeffs E i * (x • y) i =
    (↑(RingHom.id α) x • fun i =>
        if h : ↑i + 1 < E.order then y { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * y i)
      i
[PROOFSTEP]
simp [h, mul_sum]
[GOAL]
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x : α
y : Fin E.order → α
i : Fin E.order
h : ¬↑i + 1 < E.order
⊢ ∑ x_1 : Fin E.order, coeffs E x_1 * (x * y x_1) = ∑ x_1 : Fin E.order, x * (coeffs E x_1 * y x_1)
[PROOFSTEP]
exact sum_congr rfl fun x _ ↦ by ac_rfl
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x✝¹ : α
y : Fin E.order → α
i : Fin E.order
h : ¬↑i + 1 < E.order
x : Fin E.order
x✝ : x ∈ univ
⊢ coeffs E x * (x✝¹ * y x) = x✝¹ * (coeffs E x * y x)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (IsSolution E fun n => q ^ n) ↔ IsRoot (charPoly E) q
[PROOFSTEP]
rw [charPoly, Polynomial.IsRoot.def, Polynomial.eval]
[GOAL]
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (IsSolution E fun n => q ^ n) ↔
    eval₂ (RingHom.id α) q (↑(monomial E.order) 1 - ∑ i : Fin E.order, ↑(monomial ↑i) (coeffs E i)) = 0
[PROOFSTEP]
simp only [Polynomial.eval₂_finset_sum, one_mul, RingHom.id_apply, Polynomial.eval₂_monomial, Polynomial.eval₂_sub]
[GOAL]
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (IsSolution E fun n => q ^ n) ↔ q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (IsSolution E fun n => q ^ n) → q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : IsSolution E fun n => q ^ n
⊢ q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
[PROOFSTEP]
simpa [sub_eq_zero] using h 0
[GOAL]
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0 → IsSolution E fun n => q ^ n
[PROOFSTEP]
intro h n
[GOAL]
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
n : ℕ
⊢ (fun n => q ^ n) (n + E.order) = ∑ i : Fin E.order, coeffs E i * (fun n => q ^ n) (n + ↑i)
[PROOFSTEP]
simp only [pow_add, sub_eq_zero.mp h, mul_sum]
[GOAL]
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
n : ℕ
⊢ ∑ x : Fin E.order, q ^ n * (coeffs E x * q ^ ↑x) = ∑ x : Fin E.order, coeffs E x * (q ^ n * q ^ ↑x)
[PROOFSTEP]
exact sum_congr rfl fun _ _ ↦ by ring
[GOAL]
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
n : ℕ
x✝¹ : Fin E.order
x✝ : x✝¹ ∈ univ
⊢ q ^ n * (coeffs E x✝¹ * q ^ ↑x✝¹) = coeffs E x✝¹ * (q ^ n * q ^ ↑x✝¹)
[PROOFSTEP]
ring


[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : SMulWithZero R M
a✝ : R
b : M
inst✝² : Zero R'
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : ZeroHom M' M
hf : Injective ↑f
smul : ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b
a : R
⊢ ↑f (a • 0) = ↑f 0
[PROOFSTEP]
simp [smul]
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : SMulWithZero R M
a✝ : R
b : M
inst✝² : Zero R'
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : ZeroHom M' M
hf : Injective ↑f
smul : ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b
a : M'
⊢ ↑f (0 • a) = ↑f 0
[PROOFSTEP]
simp [smul]
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : SMulWithZero R M
a : R
b : M
inst✝² : Zero R'
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : ZeroHom M M'
hf : Surjective ↑f
smul : ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b
c : R
⊢ c • 0 = 0
[PROOFSTEP]
rw [← f.map_zero, ← smul, smul_zero]
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : SMulWithZero R M
a : R
b : M
inst✝² : Zero R'
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : ZeroHom M M'
hf : Surjective ↑f
smul : ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b
m : M'
⊢ 0 • m = 0
[PROOFSTEP]
rcases hf m with ⟨x, rfl⟩
[GOAL]
case intro
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : SMulWithZero R M
a : R
b : M
inst✝² : Zero R'
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : ZeroHom M M'
hf : Surjective ↑f
smul : ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b
x : M
⊢ 0 • ↑f x = 0
[PROOFSTEP]
simp [← smul]
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : SMulWithZero R M
a : R
b : M
inst✝² : Zero R'
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : ZeroHom R' R
m : M
⊢ 0 • m = 0
[PROOFSTEP]
show (f 0) • m = 0
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : SMulWithZero R M
a : R
b : M
inst✝² : Zero R'
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : ZeroHom R' R
m : M
⊢ ↑f 0 • m = 0
[PROOFSTEP]
rw [map_zero, zero_smul]
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero R'
inst✝² : Zero M
inst✝¹ : MulActionWithZero R M
inst✝ : Subsingleton R
x y : M
⊢ x = y
[PROOFSTEP]
rw [← one_smul R x, ← one_smul R y, Subsingleton.elim (1 : R) 0, zero_smul, zero_smul]
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : MonoidWithZero R
inst✝⁴ : MonoidWithZero R'
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : R' →*₀ R
src✝ : SMulWithZero R' M := SMulWithZero.compHom M ↑f
m : M
⊢ 1 • m = m
[PROOFSTEP]
show (f 1) • m = m
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : MonoidWithZero R
inst✝⁴ : MonoidWithZero R'
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : R' →*₀ R
src✝ : SMulWithZero R' M := SMulWithZero.compHom M ↑f
m : M
⊢ ↑f 1 • m = m
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : MonoidWithZero R
inst✝⁴ : MonoidWithZero R'
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : R' →*₀ R
src✝ : SMulWithZero R' M := SMulWithZero.compHom M ↑f
r s : R'
m : M
⊢ (r * s) • m = r • s • m
[PROOFSTEP]
show f (r * s) • m = (f r) • (f s) • m
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : MonoidWithZero R
inst✝⁴ : MonoidWithZero R'
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : R' →*₀ R
src✝ : SMulWithZero R' M := SMulWithZero.compHom M ↑f
r s : R'
m : M
⊢ ↑f (r * s) • m = ↑f r • ↑f s • m
[PROOFSTEP]
simp [mul_smul]
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
[PROOFSTEP]
obtain rfl | hc := eq_or_ne c 0
[GOAL]
case inl
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
x : β
⊢ (0 • x)⁻¹ = 0⁻¹ • x⁻¹
[PROOFSTEP]
simp only [inv_zero, zero_smul]
[GOAL]
case inr
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
[PROOFSTEP]
obtain rfl | hx := eq_or_ne x 0
[GOAL]
case inr.inl
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
hc : c ≠ 0
⊢ (c • 0)⁻¹ = c⁻¹ • 0⁻¹
[PROOFSTEP]
simp only [inv_zero, smul_zero]
[GOAL]
case inr.inr
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
hx : x ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
[PROOFSTEP]
refine' inv_eq_of_mul_eq_one_left _
[GOAL]
case inr.inr
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
hx : x ≠ 0
⊢ c⁻¹ • x⁻¹ * c • x = 1
[PROOFSTEP]
rw [smul_mul_smul, inv_mul_cancel hc, inv_mul_cancel hx, one_smul]


[GOAL]
⊢ ∀ (a b c : PUnit), a * b * c = a * (b * c)
[PROOFSTEP]
intros
[GOAL]
a✝ b✝ c✝ : PUnit
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a : PUnit), 1 * a = a
[PROOFSTEP]
intros
[GOAL]
a✝ : PUnit
⊢ 1 * a✝ = a✝
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a : PUnit), a * 1 = a
[PROOFSTEP]
intros
[GOAL]
a✝ : PUnit
⊢ a✝ * 1 = a✝
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a : PUnit), a⁻¹ * a = 1
[PROOFSTEP]
intros
[GOAL]
a✝ : PUnit
⊢ a✝⁻¹ * a✝ = 1
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a b : PUnit), a * b = b * a
[PROOFSTEP]
intros
[GOAL]
a✝ b✝ : PUnit
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
rfl
  -- shortcut instances
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
⊢ ∀ (a b c : PUnit), a * (b + c) = a * b + a * c
[PROOFSTEP]
intros
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
a✝ b✝ c✝ : PUnit
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
[PROOFSTEP]
rfl
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
⊢ ∀ (a b c : PUnit), (a + b) * c = a * c + b * c
[PROOFSTEP]
intros
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
a✝ b✝ c✝ : PUnit
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
[PROOFSTEP]
rfl
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
⊢ ∀ (a : PUnit), 0 * a = 0
[PROOFSTEP]
intros
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
a✝ : PUnit
⊢ 0 * a✝ = 0
[PROOFSTEP]
rfl
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
⊢ ∀ (a : PUnit), a * 0 = 0
[PROOFSTEP]
intros
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
a✝ : PUnit
⊢ a✝ * 0 = 0
[PROOFSTEP]
rfl
[GOAL]
⊢ CancelCommMonoidWithZero PUnit
[PROOFSTEP]
refine' { PUnit.commRing with .. }
[GOAL]
src✝ : CommRing PUnit := commRing
⊢ ∀ {a b c : PUnit}, a ≠ 0 → a * b = a * c → b = c
[PROOFSTEP]
intros
[GOAL]
src✝ : CommRing PUnit := commRing
a✝² b✝ c✝ : PUnit
a✝¹ : a✝² ≠ 0
a✝ : a✝² * b✝ = a✝² * c✝
⊢ b✝ = c✝
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
⊢ ∀ {a b : PUnit}, a ≠ 0 → b ≠ 0 → (fun x => 1) (a * b) = (fun x => 1) a * (fun x => 1) b
[PROOFSTEP]
intros
[GOAL]
a✝² b✝ : PUnit
a✝¹ : a✝² ≠ 0
a✝ : b✝ ≠ 0
⊢ (fun x => 1) (a✝² * b✝) = (fun x => 1) a✝² * (fun x => 1) b✝
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (u : PUnitˣ), (fun x => 1) ↑u = u⁻¹
[PROOFSTEP]
intros
[GOAL]
u✝ : PUnitˣ
⊢ (fun x => 1) ↑u✝ = u✝⁻¹
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a : PUnit), (fun x x => unit) 0 a = 0
[PROOFSTEP]
intros
[GOAL]
a✝ : PUnit
⊢ (fun x x => unit) 0 a✝ = 0
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a : PUnit), (fun x x => unit) a 0 = 0
[PROOFSTEP]
intros
[GOAL]
a✝ : PUnit
⊢ (fun x x => unit) a✝ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a b : PUnit), ↑normalize (gcd a b) = gcd a b
[PROOFSTEP]
intros
[GOAL]
a✝ b✝ : PUnit
⊢ ↑normalize (gcd a✝ b✝) = gcd a✝ b✝
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a b : PUnit), ↑normalize (lcm a b) = lcm a b
[PROOFSTEP]
intros
[GOAL]
a✝ b✝ : PUnit
⊢ ↑normalize (lcm a✝ b✝) = lcm a✝ b✝
[PROOFSTEP]
rfl
  --porting notes: simpNF lint: simp can prove this @[simp]
[GOAL]
⊢ CanonicallyOrderedAddMonoid PUnit
[PROOFSTEP]
refine'
  { PUnit.commRing, PUnit.completeBooleanAlgebra with
    exists_add_of_le := fun {_ _} _ => ⟨unit, Subsingleton.elim _ _⟩ .. }
[GOAL]
case refine'_1
src✝¹ : CommRing PUnit := commRing
src✝ : CompleteBooleanAlgebra PUnit := completeBooleanAlgebra
⊢ ∀ (a b : PUnit), a ≤ b → ∀ (c : PUnit), c + a ≤ c + b
[PROOFSTEP]
intros
[GOAL]
case refine'_2
src✝¹ : CommRing PUnit := commRing
src✝ : CompleteBooleanAlgebra PUnit := completeBooleanAlgebra
⊢ ∀ (a b : PUnit), a ≤ a + b
[PROOFSTEP]
intros
[GOAL]
case refine'_1
src✝¹ : CommRing PUnit := commRing
src✝ : CompleteBooleanAlgebra PUnit := completeBooleanAlgebra
a✝¹ b✝ : PUnit
a✝ : a✝¹ ≤ b✝
c✝ : PUnit
⊢ c✝ + a✝¹ ≤ c✝ + b✝
[PROOFSTEP]
trivial
[GOAL]
case refine'_2
src✝¹ : CommRing PUnit := commRing
src✝ : CompleteBooleanAlgebra PUnit := completeBooleanAlgebra
a✝ b✝ : PUnit
⊢ a✝ ≤ a✝ + b✝
[PROOFSTEP]
trivial
[GOAL]
src✝¹ : CanonicallyOrderedAddMonoid PUnit := canonicallyOrderedAddMonoid
src✝ : LinearOrder PUnit := linearOrder
⊢ ∀ (a b : PUnit), a ≤ b → ∀ (c : PUnit), c + a ≤ c + b
[PROOFSTEP]
intros
[GOAL]
src✝¹ : CanonicallyOrderedAddMonoid PUnit := canonicallyOrderedAddMonoid
src✝ : LinearOrder PUnit := linearOrder
a✝¹ b✝ : PUnit
a✝ : a✝¹ ≤ b✝
c✝ : PUnit
⊢ c✝ + a✝¹ ≤ c✝ + b✝
[PROOFSTEP]
rfl
[GOAL]
R : Type ?u.10038
inst✝ : Zero R
⊢ SMulWithZero R PUnit
[PROOFSTEP]
refine' { PUnit.smul with .. }
[GOAL]
case refine'_1
R : Type ?u.10038
inst✝ : Zero R
src✝ : SMul R PUnit := smul
⊢ ∀ (a : R), a • 0 = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type ?u.10038
inst✝ : Zero R
src✝ : SMul R PUnit := smul
⊢ ∀ (m : PUnit), 0 • m = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type ?u.10038
inst✝ : Zero R
src✝ : SMul R PUnit := smul
a✝ : R
⊢ a✝ • 0 = 0
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case refine'_2
R : Type ?u.10038
inst✝ : Zero R
src✝ : SMul R PUnit := smul
m✝ : PUnit
⊢ 0 • m✝ = 0
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
R : Type ?u.10319
inst✝ : Monoid R
⊢ MulAction R PUnit
[PROOFSTEP]
refine' { PUnit.smul with .. }
[GOAL]
case refine'_1
R : Type ?u.10319
inst✝ : Monoid R
src✝ : SMul R PUnit := smul
⊢ ∀ (b : PUnit), 1 • b = b
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type ?u.10319
inst✝ : Monoid R
src✝ : SMul R PUnit := smul
⊢ ∀ (x y : R) (b : PUnit), (x * y) • b = x • y • b
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type ?u.10319
inst✝ : Monoid R
src✝ : SMul R PUnit := smul
b✝ : PUnit
⊢ 1 • b✝ = b✝
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case refine'_2
R : Type ?u.10319
inst✝ : Monoid R
src✝ : SMul R PUnit := smul
x✝ y✝ : R
b✝ : PUnit
⊢ (x✝ * y✝) • b✝ = x✝ • y✝ • b✝
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
R : Type ?u.10545
inst✝ : Monoid R
⊢ DistribMulAction R PUnit
[PROOFSTEP]
refine' { PUnit.mulAction with .. }
[GOAL]
case refine'_1
R : Type ?u.10545
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
⊢ ∀ (a : R), a • 0 = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type ?u.10545
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
⊢ ∀ (a : R) (x y : PUnit), a • (x + y) = a • x + a • y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type ?u.10545
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
a✝ : R
⊢ a✝ • 0 = 0
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case refine'_2
R : Type ?u.10545
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
a✝ : R
x✝ y✝ : PUnit
⊢ a✝ • (x✝ + y✝) = a✝ • x✝ + a✝ • y✝
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
R : Type ?u.11055
inst✝ : Monoid R
⊢ MulDistribMulAction R PUnit
[PROOFSTEP]
refine' { PUnit.mulAction with .. }
[GOAL]
case refine'_1
R : Type ?u.11055
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
⊢ ∀ (r : R) (x y : PUnit), r • (x * y) = r • x * r • y
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type ?u.11055
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
⊢ ∀ (r : R), r • 1 = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type ?u.11055
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
r✝ : R
x✝ y✝ : PUnit
⊢ r✝ • (x✝ * y✝) = r✝ • x✝ * r✝ • y✝
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case refine'_2
R : Type ?u.11055
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
r✝ : R
⊢ r✝ • 1 = 1
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
R : Type ?u.13538
inst✝ : Semiring R
⊢ Module R PUnit
[PROOFSTEP]
refine' { PUnit.distribMulAction with .. }
[GOAL]
case refine'_1
R : Type ?u.13538
inst✝ : Semiring R
src✝ : DistribMulAction R PUnit := distribMulAction
⊢ ∀ (r s : R) (x : PUnit), (r + s) • x = r • x + s • x
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type ?u.13538
inst✝ : Semiring R
src✝ : DistribMulAction R PUnit := distribMulAction
⊢ ∀ (x : PUnit), 0 • x = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type ?u.13538
inst✝ : Semiring R
src✝ : DistribMulAction R PUnit := distribMulAction
r✝ s✝ : R
x✝ : PUnit
⊢ (r✝ + s✝) • x✝ = r✝ • x✝ + s✝ • x✝
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case refine'_2
R : Type ?u.13538
inst✝ : Semiring R
src✝ : DistribMulAction R PUnit := distribMulAction
x✝ : PUnit
⊢ 0 • x✝ = 0
[PROOFSTEP]
exact Subsingleton.elim _ _