α : 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
α : 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)
refine' Iff.intro (fun h x _ ↦ h ▸ rfl) _
α : 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
α : 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
intro 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 }
⊢ u = v
α : 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
set u' : ↥E.solSpace := ⟨u, hu⟩
α : 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
α : 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
set v' : ↥E.solSpace := ⟨v, hv⟩
α : 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'
α : 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
change u'.val = v'.val
α : 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'
α : 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'
suffices h' : 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'
α : 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'
exact h' ▸ rfl
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'
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'
rw [← E.toInit.toEquiv.apply_eq_iff_eq, LinearEquiv.coe_toEquiv]
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
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'
ext x
no goals
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
exact_mod_cast h (mem_range.mpr x.2)