-- Mathlib/Algebra/LinearRecurrence.lean
theorem sol_eq_of_eq_init (u v : ℕ → α) (hu : E.IsSolution u) (hv : E.IsSolution v) :
    u = v ↔ Set.EqOn u v ↑(range E.order)

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
⊢ u = v ↔ Set.EqOn u v ↑(range E.order)

Tactic:
refine Iff.intro (fun h x _ ↦ h ▸ rfl) ?_

Result:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
⊢ Set.EqOn u v ↑(range E.order) → u = v

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
h : Set.EqOn u v ↑(range E.order)
u' : ↥E.solSpace := ⟨u, hu⟩
v' : ↥E.solSpace := ⟨v, hv⟩
⊢ E.toInit u' = E.toInit v'

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
h : Set.EqOn u v ↑(range E.order)
u' : ↥E.solSpace := ⟨u, hu⟩
v' : ↥E.solSpace := ⟨v, hv⟩
x : Fin E.order
⊢ E.toInit u' x = E.toInit v' x

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
h : Set.EqOn u v ↑(range E.order)
⊢ u = v

Tactic:
set u' : ↥E.solSpace := ⟨u, hu⟩

Result:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
h : Set.EqOn u v ↑(range E.order)
u' : ↥E.solSpace := ⟨u, hu⟩
⊢ u = v

Proof state:
case h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
h : Set.EqOn u v ↑(range E.order)
u' : ↥E.solSpace := ⟨u, hu⟩
v' : ↥E.solSpace := ⟨v, hv⟩
x : Fin E.order
⊢ E.toInit u' x = E.toInit v' x

Tactic:
exact mod_cast h (mem_range.mpr x.2)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
⊢ Set.EqOn u v ↑(range E.order) → u = v

Tactic:
intro h

Result:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
h : Set.EqOn u v ↑(range E.order)
⊢ u = v

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
h : Set.EqOn u v ↑(range E.order)
u' : ↥E.solSpace := ⟨u, hu⟩
v' : ↥E.solSpace := ⟨v, hv⟩
⊢ u' = v'

Tactic:
rw [← E.toInit.toEquiv.apply_eq_iff_eq, LinearEquiv.coe_toEquiv]

Result:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
h : Set.EqOn u v ↑(range E.order)
u' : ↥E.solSpace := ⟨u, hu⟩
v' : ↥E.solSpace := ⟨v, hv⟩
⊢ E.toInit u' = E.toInit v'

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
h : Set.EqOn u v ↑(range E.order)
u' : ↥E.solSpace := ⟨u, hu⟩
⊢ u = v

Tactic:
set v' : ↥E.solSpace := ⟨v, hv⟩

Result:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
h : Set.EqOn u v ↑(range E.order)
u' : ↥E.solSpace := ⟨u, hu⟩
v' : ↥E.solSpace := ⟨v, hv⟩
⊢ u = v

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
h : Set.EqOn u v ↑(range E.order)
u' : ↥E.solSpace := ⟨u, hu⟩
v' : ↥E.solSpace := ⟨v, hv⟩
⊢ ↑u' = ↑v'

Tactic:
suffices h' : u' = v' from h' ▸ rfl

Result:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
h : Set.EqOn u v ↑(range E.order)
u' : ↥E.solSpace := ⟨u, hu⟩
v' : ↥E.solSpace := ⟨v, hv⟩
⊢ u' = v'

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
h : Set.EqOn u v ↑(range E.order)
u' : ↥E.solSpace := ⟨u, hu⟩
v' : ↥E.solSpace := ⟨v, hv⟩
⊢ u = v

Tactic:
change u'.val = v'.val

Result:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : E.IsSolution u
hv : E.IsSolution v
h : Set.EqOn u v ↑(range E.order)
u' : ↥E.solSpace := ⟨u, hu⟩
v' : ↥E.solSpace := ⟨v, hv⟩
⊢ ↑u' = ↑v'