Theorem: isSolution_solveOne (One.lean)

State before:
⊢ isSolution solveOne
Tactic:
unfold isSolution solveOne
State after:
⊢ isSolutionModel ((fun input => solveOneModel (stringToElves input)) ∘ elvesToString)

State before:
⊢ isSolutionModel ((fun input => solveOneModel (stringToElves input)) ∘ elvesToString)
Tactic:
simp [Function.comp, isSolutionModel_solveOneModel, elves_roundtrip]
State after:
no goals