Theorem: gradebook_schema_is_quiz_schema (Table/ExamplePrograms.lean)

State before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ IsQuizSchema (schema gradebook)
Tactic:
repeat (first | apply IsQuizSchema.consQuiz (by decide)
              | apply IsQuizSchema.consNonQuiz (by decide)
              | apply IsQuizSchema.nil)
State after:
no goals

State before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ IsQuizSchema []
Tactic:
(first | apply IsQuizSchema.consQuiz (by decide)
       | apply IsQuizSchema.consNonQuiz (by decide)
       | apply IsQuizSchema.nil)
State after:
no goals

State before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ IsQuizSchema []
Tactic:
first | apply IsQuizSchema.consQuiz (by decide)
      | apply IsQuizSchema.consNonQuiz (by decide)
      | apply IsQuizSchema.nil
State after:
no goals

State before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ IsQuizSchema [("final", Nat)]
Tactic:
apply IsQuizSchema.consQuiz (by decide)
State after:
no goals

State before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ String.startsWith "quiz4" "quiz" = true
Tactic:
decide
State after:
no goals

State before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ IsQuizSchema [("final", Nat)]
Tactic:
apply IsQuizSchema.consNonQuiz (by decide)
State after:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ IsQuizSchema []

State before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ String.startsWith "final" "quiz" = false
Tactic:
decide
State after:
no goals

State before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ IsQuizSchema []
Tactic:
apply IsQuizSchema.nil
State after:
no goals