Theorem: ThunkOrdering.lex_assoc (Katydid/Std/ThunkOrdering.lean)

State before:
⊢ ∀ (a b c : Thunk Ordering), lex (lex a b) c = lex a (lex b c)
Tactic:
intros a b c
State after:
a b c : Thunk Ordering
⊢ lex (lex a b) c = lex a (lex b c)

State before:
a b c : Thunk Ordering
⊢ lex (lex a b) c = lex a (lex b c)
Tactic:
unfold lex
State after:
a b c : Thunk Ordering
⊢ (match
      Thunk.get
        (match Thunk.get a with
        | Ordering.eq => b
        | x => { fn := fun x => Thunk.get a }) with
    | Ordering.eq => c
    | x =>
      {
        fn := fun x =>
          Thunk.get
            (match Thunk.get a with
            | Ordering.eq => b
            | x => { fn := fun x => Thunk.get a }) }) =
    match Thunk.get a with
    | Ordering.eq =>
      match Thunk.get b with
      | Ordering.eq => c
      | x => { fn := fun x => Thunk.get b }
    | x => { fn := fun x => Thunk.get a }

State before:
a b c : Thunk Ordering
⊢ (match
      Thunk.get
        (match Thunk.get a with
        | Ordering.eq => b
        | x => { fn := fun x => Thunk.get a }) with
    | Ordering.eq => c
    | x =>
      {
        fn := fun x =>
          Thunk.get
            (match Thunk.get a with
            | Ordering.eq => b
            | x => { fn := fun x => Thunk.get a }) }) =
    match Thunk.get a with
    | Ordering.eq =>
      match Thunk.get b with
      | Ordering.eq => c
      | x => { fn := fun x => Thunk.get b }
    | x => { fn := fun x => Thunk.get a }
Tactic:
cases a.get with
| lt => simp only
        simp [Thunk.get]
| gt => dsimp
        rfl
| eq => dsimp only
State after:
no goals

State before:
case lt
a b c : Thunk Ordering
⊢ (match
      Thunk.get
        (match Ordering.lt with
        | Ordering.eq => b
        | x => { fn := fun x => Ordering.lt }) with
    | Ordering.eq => c
    | x =>
      {
        fn := fun x =>
          Thunk.get
            (match Ordering.lt with
            | Ordering.eq => b
            | x => { fn := fun x => Ordering.lt }) }) =
    match Ordering.lt with
    | Ordering.eq =>
      match Thunk.get b with
      | Ordering.eq => c
      | x => { fn := fun x => Thunk.get b }
    | x => { fn := fun x => Ordering.lt }
Tactic:
simp only
State after:
case lt
a b c : Thunk Ordering
⊢ (match Thunk.get { fn := fun x => Ordering.lt } with
    | Ordering.eq => c
    | x => { fn := fun x => Thunk.get { fn := fun x => Ordering.lt } }) =
    { fn := fun x => Ordering.lt }

State before:
case lt
a b c : Thunk Ordering
⊢ (match Thunk.get { fn := fun x => Ordering.lt } with
    | Ordering.eq => c
    | x => { fn := fun x => Thunk.get { fn := fun x => Ordering.lt } }) =
    { fn := fun x => Ordering.lt }
Tactic:
simp [Thunk.get]
State after:
no goals

State before:
case gt
a b c : Thunk Ordering
⊢ (match
      Thunk.get
        (match Ordering.gt with
        | Ordering.eq => b
        | x => { fn := fun x => Ordering.gt }) with
    | Ordering.eq => c
    | x =>
      {
        fn := fun x =>
          Thunk.get
            (match Ordering.gt with
            | Ordering.eq => b
            | x => { fn := fun x => Ordering.gt }) }) =
    match Ordering.gt with
    | Ordering.eq =>
      match Thunk.get b with
      | Ordering.eq => c
      | x => { fn := fun x => Thunk.get b }
    | x => { fn := fun x => Ordering.gt }
Tactic:
dsimp
State after:
case gt
a b c : Thunk Ordering
⊢ (match Thunk.get { fn := fun x => Ordering.gt } with
    | Ordering.eq => c
    | x => { fn := fun x => Thunk.get { fn := fun x => Ordering.gt } }) =
    { fn := fun x => Ordering.gt }

State before:
case gt
a b c : Thunk Ordering
⊢ (match Thunk.get { fn := fun x => Ordering.gt } with
    | Ordering.eq => c
    | x => { fn := fun x => Thunk.get { fn := fun x => Ordering.gt } }) =
    { fn := fun x => Ordering.gt }
Tactic:
rfl
State after:
no goals

State before:
case eq
a b c : Thunk Ordering
⊢ (match
      Thunk.get
        (match Ordering.eq with
        | Ordering.eq => b
        | x => { fn := fun x => Ordering.eq }) with
    | Ordering.eq => c
    | x =>
      {
        fn := fun x =>
          Thunk.get
            (match Ordering.eq with
            | Ordering.eq => b
            | x => { fn := fun x => Ordering.eq }) }) =
    match Ordering.eq with
    | Ordering.eq =>
      match Thunk.get b with
      | Ordering.eq => c
      | x => { fn := fun x => Thunk.get b }
    | x => { fn := fun x => Ordering.eq }
Tactic:
dsimp only
State after:
no goals