[Merged by Bors] - chore(Data/Seq): address porting note in terminates_parallel.aux by golfing

[euprunin]

---

Show trace profiling of terminates_parallel.aux: 103 ms before, 118 ms after

Trace profiling of terminates_parallel.aux before PR 30603

diff --git a/Mathlib/Data/Seq/Parallel.lean b/Mathlib/Data/Seq/Parallel.lean
index 5f785ba022..e969377ae5 100644
--- a/Mathlib/Data/Seq/Parallel.lean
+++ b/Mathlib/Data/Seq/Parallel.lean
@@ -48,6 +48,7 @@ private def parallel.aux1 :
 def parallel (S : WSeq (Computation α)) : Computation α :=
   corec parallel.aux1 ([], S)
 
+set_option trace.profiler true in
 theorem terminates_parallel.aux :
     ∀ {l : List (Computation α)} {S c},
       c ∈ l → Terminates c → Terminates (corec parallel.aux1 (l, S)) := by

ℹ [703/703] Built Mathlib.Data.Seq.Parallel (1.3s)
info: Mathlib/Data/Seq/Parallel.lean:52:0: [Elab.async] [0.105135] elaborating proof of Computation.terminates_parallel.aux
  [Elab.definition.value] [0.102557] Computation.terminates_parallel.aux
    [Elab.step] [0.099849] 
          have lem1 : ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) :=
            by
            intro l S e
            obtain ⟨a, e⟩ := e
            have : corec parallel.aux1 (l, S) = return a :=
              by
              apply destruct_eq_pure
              simp only [parallel.aux1, rmap, corec_eq]
              rw [e]
            rw [this]
            exact ret_terminates a
          intro l S c m T
          revert l S
          apply @terminatesRecOn _ _ c T _ _
          · intro a l S m
            apply lem1
            induction l with
            | nil => simp at m
            | cons c l IH => ?_
            simp only [List.mem_cons] at m
            rcases m with e | m
            · rw [← e]
              simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
              split <;> simp
            · obtain ⟨a', e⟩ := IH m
              simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e
              rw [e]
              exact ⟨a', rfl⟩
          · intro s IH l S m
            have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' :=
              by
              induction l generalizing l' with
              | nil => simp at m
              | cons c l IH' => ?_
              simp only [List.mem_cons] at m
              rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
              · rw [← e] at e'
                revert e'
                split
                · simp
                · simp only [destruct_think, Sum.inr.injEq]
                  rintro rfl
                  simp
              · rcases e :
                    List.foldr
                      (fun c o =>
                        match o with
                        | Sum.inl a => Sum.inl a
                        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                      (Sum.inr List.nil) l with
                    a' | ls <;> erw [e] at e'
                · contradiction
                have := IH' m _ e
                revert e'
                cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                rw [← h']
                simp [this]
            rcases h : parallel.aux2 l with a | l'
            · exact lem1 _ _ ⟨a, h⟩
            · have H2 : corec parallel.aux1 (l, S) = think _ :=
                destruct_eq_think
                  (by
                    simp only [parallel.aux1, rmap, corec_eq]
                    rw [h])
              rw [H2]
              refine @Computation.think_terminates _ _ ?_
              have := H1 _ h
              rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> apply IH <;> simp [this]
      [Elab.step] [0.099836] 
            have lem1 : ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) :=
              by
              intro l S e
              obtain ⟨a, e⟩ := e
              have : corec parallel.aux1 (l, S) = return a :=
                by
                apply destruct_eq_pure
                simp only [parallel.aux1, rmap, corec_eq]
                rw [e]
              rw [this]
              exact ret_terminates a
            intro l S c m T
            revert l S
            apply @terminatesRecOn _ _ c T _ _
            · intro a l S m
              apply lem1
              induction l with
              | nil => simp at m
              | cons c l IH => ?_
              simp only [List.mem_cons] at m
              rcases m with e | m
              · rw [← e]
                simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
                split <;> simp
              · obtain ⟨a', e⟩ := IH m
                simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e
                rw [e]
                exact ⟨a', rfl⟩
            · intro s IH l S m
              have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' :=
                by
                induction l generalizing l' with
                | nil => simp at m
                | cons c l IH' => ?_
                simp only [List.mem_cons] at m
                rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                · rw [← e] at e'
                  revert e'
                  split
                  · simp
                  · simp only [destruct_think, Sum.inr.injEq]
                    rintro rfl
                    simp
                · rcases e :
                      List.foldr
                        (fun c o =>
                          match o with
                          | Sum.inl a => Sum.inl a
                          | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                        (Sum.inr List.nil) l with
                      a' | ls <;> erw [e] at e'
                  · contradiction
                  have := IH' m _ e
                  revert e'
                  cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                  rw [← h']
                  simp [this]
              rcases h : parallel.aux2 l with a | l'
              · exact lem1 _ _ ⟨a, h⟩
              · have H2 : corec parallel.aux1 (l, S) = think _ :=
                  destruct_eq_think
                    (by
                      simp only [parallel.aux1, rmap, corec_eq]
                      rw [h])
                rw [H2]
                refine @Computation.think_terminates _ _ ?_
                have := H1 _ h
                rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> apply IH <;> simp [this]
        [Elab.step] [0.018345] have lem1 :
              ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) :=
              by
              intro l S e
              obtain ⟨a, e⟩ := e
              have : corec parallel.aux1 (l, S) = return a :=
                by
                apply destruct_eq_pure
                simp only [parallel.aux1, rmap, corec_eq]
                rw [e]
              rw [this]
              exact ret_terminates a
          [Elab.step] [0.018330] focus
                refine
                  no_implicit_lambda%
                    (have lem1 :
                      ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) := ?body✝;
                    ?_)
                case body✝ =>
                  with_annotate_state"by"
                    ( intro l S e
                      obtain ⟨a, e⟩ := e
                      have : corec parallel.aux1 (l, S) = return a :=
                        by
                        apply destruct_eq_pure
                        simp only [parallel.aux1, rmap, corec_eq]
                        rw [e]
                      rw [this]
                      exact ret_terminates a)
            [Elab.step] [0.018319] 
                  refine
                    no_implicit_lambda%
                      (have lem1 :
                        ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) :=
                        ?body✝;
                      ?_)
                  case body✝ =>
                    with_annotate_state"by"
                      ( intro l S e
                        obtain ⟨a, e⟩ := e
                        have : corec parallel.aux1 (l, S) = return a :=
                          by
                          apply destruct_eq_pure
                          simp only [parallel.aux1, rmap, corec_eq]
                          rw [e]
                        rw [this]
                        exact ret_terminates a)
              [Elab.step] [0.018316] 
                    refine
                      no_implicit_lambda%
                        (have lem1 :
                          ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) :=
                          ?body✝;
                        ?_)
                    case body✝ =>
                      with_annotate_state"by"
                        ( intro l S e
                          obtain ⟨a, e⟩ := e
                          have : corec parallel.aux1 (l, S) = return a :=
                            by
                            apply destruct_eq_pure
                            simp only [parallel.aux1, rmap, corec_eq]
                            rw [e]
                          rw [this]
                          exact ret_terminates a)
                [Elab.step] [0.017269] case body✝ =>
                      with_annotate_state"by"
                        ( intro l S e
                          obtain ⟨a, e⟩ := e
                          have : corec parallel.aux1 (l, S) = return a :=
                            by
                            apply destruct_eq_pure
                            simp only [parallel.aux1, rmap, corec_eq]
                            rw [e]
                          rw [this]
                          exact ret_terminates a)
                  [Elab.step] [0.017240] with_annotate_state"by"
                          ( intro l S e
                            obtain ⟨a, e⟩ := e
                            have : corec parallel.aux1 (l, S) = return a :=
                              by
                              apply destruct_eq_pure
                              simp only [parallel.aux1, rmap, corec_eq]
                              rw [e]
                            rw [this]
                            exact ret_terminates a)
                    [Elab.step] [0.017237] with_annotate_state"by"
                            ( intro l S e
                              obtain ⟨a, e⟩ := e
                              have : corec parallel.aux1 (l, S) = return a :=
                                by
                                apply destruct_eq_pure
                                simp only [parallel.aux1, rmap, corec_eq]
                                rw [e]
                              rw [this]
                              exact ret_terminates a)
                      [Elab.step] [0.017234] with_annotate_state"by"
                            ( intro l S e
                              obtain ⟨a, e⟩ := e
                              have : corec parallel.aux1 (l, S) = return a :=
                                by
                                apply destruct_eq_pure
                                simp only [parallel.aux1, rmap, corec_eq]
                                rw [e]
                              rw [this]
                              exact ret_terminates a)
                        [Elab.step] [0.017229] (
                              intro l S e
                              obtain ⟨a, e⟩ := e
                              have : corec parallel.aux1 (l, S) = return a :=
                                by
                                apply destruct_eq_pure
                                simp only [parallel.aux1, rmap, corec_eq]
                                rw [e]
                              rw [this]
                              exact ret_terminates a)
                          [Elab.step] [0.017226] 
                                intro l S e
                                obtain ⟨a, e⟩ := e
                                have : corec parallel.aux1 (l, S) = return a :=
                                  by
                                  apply destruct_eq_pure
                                  simp only [parallel.aux1, rmap, corec_eq]
                                  rw [e]
                                rw [this]
                                exact ret_terminates a
                            [Elab.step] [0.017221] 
                                  intro l S e
                                  obtain ⟨a, e⟩ := e
                                  have : corec parallel.aux1 (l, S) = return a :=
                                    by
                                    apply destruct_eq_pure
                                    simp only [parallel.aux1, rmap, corec_eq]
                                    rw [e]
                                  rw [this]
                                  exact ret_terminates a
                              [Elab.step] [0.016304] have : corec parallel.aux1 (l, S) = return a :=
                                    by
                                    apply destruct_eq_pure
                                    simp only [parallel.aux1, rmap, corec_eq]
                                    rw [e]
                                [Elab.step] [0.016294] focus
                                      refine
                                        no_implicit_lambda%
                                          (have : corec parallel.aux1 (l, S) = return a := ?body✝;
                                          ?_)
                                      case body✝ =>
                                        with_annotate_state"by"
                                          ( apply destruct_eq_pure
                                            simp only [parallel.aux1, rmap, corec_eq]
                                            rw [e])
                                  [Elab.step] [0.016289] 
                                        refine
                                          no_implicit_lambda%
                                            (have : corec parallel.aux1 (l, S) = return a := ?body✝;
                                            ?_)
                                        case body✝ =>
                                          with_annotate_state"by"
                                            ( apply destruct_eq_pure
                                              simp only [parallel.aux1, rmap, corec_eq]
                                              rw [e])
                                    [Elab.step] [0.016286] 
                                          refine
                                            no_implicit_lambda%
                                              (have : corec parallel.aux1 (l, S) = return a := ?body✝;
                                              ?_)
                                          case body✝ =>
                                            with_annotate_state"by"
                                              ( apply destruct_eq_pure
                                                simp only [parallel.aux1, rmap, corec_eq]
                                                rw [e])
                                      [Elab.step] [0.015214] case body✝ =>
                                            with_annotate_state"by"
                                              ( apply destruct_eq_pure
                                                simp only [parallel.aux1, rmap, corec_eq]
                                                rw [e])
                                        [Elab.step] [0.015195] with_annotate_state"by"
                                                ( apply destruct_eq_pure
                                                  simp only [parallel.aux1, rmap, corec_eq]
                                                  rw [e])
                                          [Elab.step] [0.015192] with_annotate_state"by"
                                                  ( apply destruct_eq_pure
                                                    simp only [parallel.aux1, rmap, corec_eq]
                                                    rw [e])
                                            [Elab.step] [0.015189] with_annotate_state"by"
                                                  ( apply destruct_eq_pure
                                                    simp only [parallel.aux1, rmap, corec_eq]
                                                    rw [e])
                                              [Elab.step] [0.015186] (
                                                    apply destruct_eq_pure
                                                    simp only [parallel.aux1, rmap, corec_eq]
                                                    rw [e])
                                                [Elab.step] [0.015183] 
                                                      apply destruct_eq_pure
                                                      simp only [parallel.aux1, rmap, corec_eq]
                                                      rw [e]
                                                  [Elab.step] [0.015179] 
                                                        apply destruct_eq_pure
                                                        simp only [parallel.aux1, rmap, corec_eq]
                                                        rw [e]
                                                    [Elab.step] [0.014029] simp only [parallel.aux1, rmap, corec_eq]
        [Elab.step] [0.041221] ·
              intro a l S m
              apply lem1
              induction l with
              | nil => simp at m
              | cons c l IH => ?_
              simp only [List.mem_cons] at m
              rcases m with e | m
              · rw [← e]
                simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
                split <;> simp
              · obtain ⟨a', e⟩ := IH m
                simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e
                rw [e]
                exact ⟨a', rfl⟩
          [Elab.step] [0.041152] 
                intro a l S m
                apply lem1
                induction l with
                | nil => simp at m
                | cons c l IH => ?_
                simp only [List.mem_cons] at m
                rcases m with e | m
                · rw [← e]
                  simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
                  split <;> simp
                · obtain ⟨a', e⟩ := IH m
                  simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e
                  rw [e]
                  exact ⟨a', rfl⟩
            [Elab.step] [0.041145] 
                  intro a l S m
                  apply lem1
                  induction l with
                  | nil => simp at m
                  | cons c l IH => ?_
                  simp only [List.mem_cons] at m
                  rcases m with e | m
                  · rw [← e]
                    simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
                    split <;> simp
                  · obtain ⟨a', e⟩ := IH m
                    simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e
                    rw [e]
                    exact ⟨a', rfl⟩
              [Elab.step] [0.029455] ·
                    rw [← e]
                    simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
                    split <;> simp
                [Elab.step] [0.029435] 
                      rw [← e]
                      simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
                      split <;> simp
                  [Elab.step] [0.029431] 
                        rw [← e]
                        simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
                        split <;> simp
                    [Elab.step] [0.022602] split <;> simp
                      [Elab.step] [0.022592] focus
                            split
                            with_annotate_state"<;>" skip
                            all_goals simp
                        [Elab.step] [0.022587] 
                              split
                              with_annotate_state"<;>" skip
                              all_goals simp
                          [Elab.step] [0.022584] 
                                split
                                with_annotate_state"<;>" skip
                                all_goals simp
                            [Elab.step] [0.021498] all_goals simp
                              [Elab.step] [0.020051] simp
                                [Elab.step] [0.020047] simp
                                  [Elab.step] [0.020041] simp
                                    [Meta.Tactic.simp.discharge] [0.018644] IsEmpty.exists_iff discharge ❌️
                                          IsEmpty α
                                      [Meta.synthInstance] [0.018248] ❌️ Nonempty α
        [Elab.step] [0.039784] ·
              intro s IH l S m
              have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' :=
                by
                induction l generalizing l' with
                | nil => simp at m
                | cons c l IH' => ?_
                simp only [List.mem_cons] at m
                rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                · rw [← e] at e'
                  revert e'
                  split
                  · simp
                  · simp only [destruct_think, Sum.inr.injEq]
                    rintro rfl
                    simp
                · rcases e :
                      List.foldr
                        (fun c o =>
                          match o with
                          | Sum.inl a => Sum.inl a
                          | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                        (Sum.inr List.nil) l with
                      a' | ls <;> erw [e] at e'
                  · contradiction
                  have := IH' m _ e
                  revert e'
                  cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                  rw [← h']
                  simp [this]
              rcases h : parallel.aux2 l with a | l'
              · exact lem1 _ _ ⟨a, h⟩
              · have H2 : corec parallel.aux1 (l, S) = think _ :=
                  destruct_eq_think
                    (by
                      simp only [parallel.aux1, rmap, corec_eq]
                      rw [h])
                rw [H2]
                refine @Computation.think_terminates _ _ ?_
                have := H1 _ h
                rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> apply IH <;> simp [this]
          [Elab.step] [0.039742] 
                intro s IH l S m
                have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' :=
                  by
                  induction l generalizing l' with
                  | nil => simp at m
                  | cons c l IH' => ?_
                  simp only [List.mem_cons] at m
                  rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                  · rw [← e] at e'
                    revert e'
                    split
                    · simp
                    · simp only [destruct_think, Sum.inr.injEq]
                      rintro rfl
                      simp
                  · rcases e :
                        List.foldr
                          (fun c o =>
                            match o with
                            | Sum.inl a => Sum.inl a
                            | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                          (Sum.inr List.nil) l with
                        a' | ls <;> erw [e] at e'
                    · contradiction
                    have := IH' m _ e
                    revert e'
                    cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                    rw [← h']
                    simp [this]
                rcases h : parallel.aux2 l with a | l'
                · exact lem1 _ _ ⟨a, h⟩
                · have H2 : corec parallel.aux1 (l, S) = think _ :=
                    destruct_eq_think
                      (by
                        simp only [parallel.aux1, rmap, corec_eq]
                        rw [h])
                  rw [H2]
                  refine @Computation.think_terminates _ _ ?_
                  have := H1 _ h
                  rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> apply IH <;> simp [this]
            [Elab.step] [0.039737] 
                  intro s IH l S m
                  have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' :=
                    by
                    induction l generalizing l' with
                    | nil => simp at m
                    | cons c l IH' => ?_
                    simp only [List.mem_cons] at m
                    rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                    · rw [← e] at e'
                      revert e'
                      split
                      · simp
                      · simp only [destruct_think, Sum.inr.injEq]
                        rintro rfl
                        simp
                    · rcases e :
                          List.foldr
                            (fun c o =>
                              match o with
                              | Sum.inl a => Sum.inl a
                              | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                            (Sum.inr List.nil) l with
                          a' | ls <;> erw [e] at e'
                      · contradiction
                      have := IH' m _ e
                      revert e'
                      cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                      rw [← h']
                      simp [this]
                  rcases h : parallel.aux2 l with a | l'
                  · exact lem1 _ _ ⟨a, h⟩
                  · have H2 : corec parallel.aux1 (l, S) = think _ :=
                      destruct_eq_think
                        (by
                          simp only [parallel.aux1, rmap, corec_eq]
                          rw [h])
                    rw [H2]
                    refine @Computation.think_terminates _ _ ?_
                    have := H1 _ h
                    rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> apply IH <;> simp [this]
              [Elab.step] [0.029671] have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' :=
                    by
                    induction l generalizing l' with
                    | nil => simp at m
                    | cons c l IH' => ?_
                    simp only [List.mem_cons] at m
                    rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                    · rw [← e] at e'
                      revert e'
                      split
                      · simp
                      · simp only [destruct_think, Sum.inr.injEq]
                        rintro rfl
                        simp
                    · rcases e :
                          List.foldr
                            (fun c o =>
                              match o with
                              | Sum.inl a => Sum.inl a
                              | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                            (Sum.inr List.nil) l with
                          a' | ls <;> erw [e] at e'
                      · contradiction
                      have := IH' m _ e
                      revert e'
                      cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                      rw [← h']
                      simp [this]
                [Elab.step] [0.029664] focus
                      refine
                        no_implicit_lambda%
                          (have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' := ?body✝;
                          ?_)
                      case body✝ =>
                        with_annotate_state"by"
                          ( induction l generalizing l' with
                            | nil => simp at m
                            | cons c l IH' => ?_
                            simp only [List.mem_cons] at m
                            rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                            · rw [← e] at e'
                              revert e'
                              split
                              · simp
                              · simp only [destruct_think, Sum.inr.injEq]
                                rintro rfl
                                simp
                            · rcases e :
                                  List.foldr
                                    (fun c o =>
                                      match o with
                                      | Sum.inl a => Sum.inl a
                                      | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                    (Sum.inr List.nil) l with
                                  a' | ls <;> erw [e] at e'
                              · contradiction
                              have := IH' m _ e
                              revert e'
                              cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                              rw [← h']
                              simp [this])
                  [Elab.step] [0.029660] 
                        refine
                          no_implicit_lambda%
                            (have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' := ?body✝;
                            ?_)
                        case body✝ =>
                          with_annotate_state"by"
                            ( induction l generalizing l' with
                              | nil => simp at m
                              | cons c l IH' => ?_
                              simp only [List.mem_cons] at m
                              rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                              · rw [← e] at e'
                                revert e'
                                split
                                · simp
                                · simp only [destruct_think, Sum.inr.injEq]
                                  rintro rfl
                                  simp
                              · rcases e :
                                    List.foldr
                                      (fun c o =>
                                        match o with
                                        | Sum.inl a => Sum.inl a
                                        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                      (Sum.inr List.nil) l with
                                    a' | ls <;> erw [e] at e'
                                · contradiction
                                have := IH' m _ e
                                revert e'
                                cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                                rw [← h']
                                simp [this])
                    [Elab.step] [0.029658] 
                          refine
                            no_implicit_lambda%
                              (have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' := ?body✝;
                              ?_)
                          case body✝ =>
                            with_annotate_state"by"
                              ( induction l generalizing l' with
                                | nil => simp at m
                                | cons c l IH' => ?_
                                simp only [List.mem_cons] at m
                                rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                · rw [← e] at e'
                                  revert e'
                                  split
                                  · simp
                                  · simp only [destruct_think, Sum.inr.injEq]
                                    rintro rfl
                                    simp
                                · rcases e :
                                      List.foldr
                                        (fun c o =>
                                          match o with
                                          | Sum.inl a => Sum.inl a
                                          | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                        (Sum.inr List.nil) l with
                                      a' | ls <;> erw [e] at e'
                                  · contradiction
                                  have := IH' m _ e
                                  revert e'
                                  cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                                  rw [← h']
                                  simp [this])
                      [Elab.step] [0.028856] case body✝ =>
                            with_annotate_state"by"
                              ( induction l generalizing l' with
                                | nil => simp at m
                                | cons c l IH' => ?_
                                simp only [List.mem_cons] at m
                                rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                · rw [← e] at e'
                                  revert e'
                                  split
                                  · simp
                                  · simp only [destruct_think, Sum.inr.injEq]
                                    rintro rfl
                                    simp
                                · rcases e :
                                      List.foldr
                                        (fun c o =>
                                          match o with
                                          | Sum.inl a => Sum.inl a
                                          | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                        (Sum.inr List.nil) l with
                                      a' | ls <;> erw [e] at e'
                                  · contradiction
                                  have := IH' m _ e
                                  revert e'
                                  cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                                  rw [← h']
                                  simp [this])
                        [Elab.step] [0.028835] with_annotate_state"by"
                                ( induction l generalizing l' with
                                  | nil => simp at m
                                  | cons c l IH' => ?_
                                  simp only [List.mem_cons] at m
                                  rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                  · rw [← e] at e'
                                    revert e'
                                    split
                                    · simp
                                    · simp only [destruct_think, Sum.inr.injEq]
                                      rintro rfl
                                      simp
                                  · rcases e :
                                        List.foldr
                                          (fun c o =>
                                            match o with
                                            | Sum.inl a => Sum.inl a
                                            | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                          (Sum.inr List.nil) l with
                                        a' | ls <;> erw [e] at e'
                                    · contradiction
                                    have := IH' m _ e
                                    revert e'
                                    cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                                    rw [← h']
                                    simp [this])
                          [Elab.step] [0.028832] with_annotate_state"by"
                                  ( induction l generalizing l' with
                                    | nil => simp at m
                                    | cons c l IH' => ?_
                                    simp only [List.mem_cons] at m
                                    rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                    · rw [← e] at e'
                                      revert e'
                                      split
                                      · simp
                                      · simp only [destruct_think, Sum.inr.injEq]
                                        rintro rfl
                                        simp
                                    · rcases e :
                                          List.foldr
                                            (fun c o =>
                                              match o with
                                              | Sum.inl a => Sum.inl a
                                              | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                            (Sum.inr List.nil) l with
                                          a' | ls <;> erw [e] at e'
                                      · contradiction
                                      have := IH' m _ e
                                      revert e'
                                      cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                                      rw [← h']
                                      simp [this])
                            [Elab.step] [0.028829] with_annotate_state"by"
                                  ( induction l generalizing l' with
                                    | nil => simp at m
                                    | cons c l IH' => ?_
                                    simp only [List.mem_cons] at m
                                    rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                    · rw [← e] at e'
                                      revert e'
                                      split
                                      · simp
                                      · simp only [destruct_think, Sum.inr.injEq]
                                        rintro rfl
                                        simp
                                    · rcases e :
                                          List.foldr
                                            (fun c o =>
                                              match o with
                                              | Sum.inl a => Sum.inl a
                                              | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                            (Sum.inr List.nil) l with
                                          a' | ls <;> erw [e] at e'
                                      · contradiction
                                      have := IH' m _ e
                                      revert e'
                                      cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                                      rw [← h']
                                      simp [this])
                              [Elab.step] [0.028826] (
                                    induction l generalizing l' with
                                    | nil => simp at m
                                    | cons c l IH' => ?_
                                    simp only [List.mem_cons] at m
                                    rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                    · rw [← e] at e'
                                      revert e'
                                      split
                                      · simp
                                      · simp only [destruct_think, Sum.inr.injEq]
                                        rintro rfl
                                        simp
                                    · rcases e :
                                          List.foldr
                                            (fun c o =>
                                              match o with
                                              | Sum.inl a => Sum.inl a
                                              | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                            (Sum.inr List.nil) l with
                                          a' | ls <;> erw [e] at e'
                                      · contradiction
                                      have := IH' m _ e
                                      revert e'
                                      cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                                      rw [← h']
                                      simp [this])
                                [Elab.step] [0.028823] 
                                      induction l generalizing l' with
                                      | nil => simp at m
                                      | cons c l IH' => ?_
                                      simp only [List.mem_cons] at m
                                      rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                      · rw [← e] at e'
                                        revert e'
                                        split
                                        · simp
                                        · simp only [destruct_think, Sum.inr.injEq]
                                          rintro rfl
                                          simp
                                      · rcases e :
                                            List.foldr
                                              (fun c o =>
                                                match o with
                                                | Sum.inl a => Sum.inl a
                                                | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                              (Sum.inr List.nil) l with
                                            a' | ls <;> erw [e] at e'
                                        · contradiction
                                        have := IH' m _ e
                                        revert e'
                                        cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                                        rw [← h']
                                        simp [this]
                                  [Elab.step] [0.028820] 
                                        induction l generalizing l' with
                                        | nil => simp at m
                                        | cons c l IH' => ?_
                                        simp only [List.mem_cons] at m
                                        rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                        · rw [← e] at e'
                                          revert e'
                                          split
                                          · simp
                                          · simp only [destruct_think, Sum.inr.injEq]
                                            rintro rfl
                                            simp
                                        · rcases e :
                                              List.foldr
                                                (fun c o =>
                                                  match o with
                                                  | Sum.inl a => Sum.inl a
                                                  | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                                (Sum.inr List.nil) l with
                                              a' | ls <;> erw [e] at e'
                                          · contradiction
                                          have := IH' m _ e
                                          revert e'
                                          cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                                          rw [← h']
                                          simp [this]
                                    [Elab.step] [0.013607] ·
                                          rcases e :
                                              List.foldr
                                                (fun c o =>
                                                  match o with
                                                  | Sum.inl a => Sum.inl a
                                                  | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                                (Sum.inr List.nil) l with
                                              a' | ls <;>
                                            erw [e] at e'
                                          · contradiction
                                          have := IH' m _ e
                                          revert e'
                                          cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                                          rw [← h']
                                          simp [this]
                                      [Elab.step] [0.013583] 
                                            rcases e :
                                                List.foldr
                                                  (fun c o =>
                                                    match o with
                                                    | Sum.inl a => Sum.inl a
                                                    | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                                  (Sum.inr List.nil) l with
                                                a' | ls <;>
                                              erw [e] at e'
                                            · contradiction
                                            have := IH' m _ e
                                            revert e'
                                            cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                                            rw [← h']
                                            simp [this]
                                        [Elab.step] [0.013577] 
                                              rcases e :
                                                  List.foldr
                                                    (fun c o =>
                                                      match o with
                                                      | Sum.inl a => Sum.inl a
                                                      | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                                    (Sum.inr List.nil) l with
                                                  a' | ls <;>
                                                erw [e] at e'
                                              · contradiction
                                              have := IH' m _ e
                                              revert e'
                                              cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
                                              rw [← h']
                                              simp [this]
Build completed successfully (703 jobs).

Trace profiling of terminates_parallel.aux after PR 30603

diff --git a/Mathlib/Data/Seq/Parallel.lean b/Mathlib/Data/Seq/Parallel.lean
index 5f785ba022..95b197c847 100644
--- a/Mathlib/Data/Seq/Parallel.lean
+++ b/Mathlib/Data/Seq/Parallel.lean
@@ -48,6 +48,7 @@ private def parallel.aux1 :
 def parallel (S : WSeq (Computation α)) : Computation α :=
   corec parallel.aux1 ([], S)
 
+set_option trace.profiler true in
 theorem terminates_parallel.aux :
     ∀ {l : List (Computation α)} {S c},
       c ∈ l → Terminates c → Terminates (corec parallel.aux1 (l, S)) := by
@@ -96,11 +97,7 @@ theorem terminates_parallel.aux :
           (Sum.inr List.nil) l with a' | ls <;> erw [e] at e'
         · contradiction
         have := IH' m _ e
-        -- Porting note: `revert e'` & `intro e'` are required.
-        revert e'
-        cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
-        rw [← h']
-        simp [this]
+        grind
     rcases h : parallel.aux2 l with a | l'
     · exact lem1 _ _ ⟨a, h⟩
     · have H2 : corec parallel.aux1 (l, S) = think _ := destruct_eq_think (by

ℹ [703/703] Built Mathlib.Data.Seq.Parallel (994ms)
info: Mathlib/Data/Seq/Parallel.lean:52:0: [Elab.async] [0.120987] elaborating proof of Computation.terminates_parallel.aux
  [Elab.definition.value] [0.118452] Computation.terminates_parallel.aux
    [Elab.step] [0.115837] 
          have lem1 : ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) :=
            by
            intro l S e
            obtain ⟨a, e⟩ := e
            have : corec parallel.aux1 (l, S) = return a :=
              by
              apply destruct_eq_pure
              simp only [parallel.aux1, rmap, corec_eq]
              rw [e]
            rw [this]
            exact ret_terminates a
          intro l S c m T
          revert l S
          apply @terminatesRecOn _ _ c T _ _
          · intro a l S m
            apply lem1
            induction l with
            | nil => simp at m
            | cons c l IH => ?_
            simp only [List.mem_cons] at m
            rcases m with e | m
            · rw [← e]
              simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
              split <;> simp
            · obtain ⟨a', e⟩ := IH m
              simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e
              rw [e]
              exact ⟨a', rfl⟩
          · intro s IH l S m
            have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' :=
              by
              induction l generalizing l' with
              | nil => simp at m
              | cons c l IH' => ?_
              simp only [List.mem_cons] at m
              rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
              · rw [← e] at e'
                revert e'
                split
                · simp
                · simp only [destruct_think, Sum.inr.injEq]
                  rintro rfl
                  simp
              · rcases e :
                    List.foldr
                      (fun c o =>
                        match o with
                        | Sum.inl a => Sum.inl a
                        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                      (Sum.inr List.nil) l with
                    a' | ls <;> erw [e] at e'
                · contradiction
                have := IH' m _ e
                grind
            rcases h : parallel.aux2 l with a | l'
            · exact lem1 _ _ ⟨a, h⟩
            · have H2 : corec parallel.aux1 (l, S) = think _ :=
                destruct_eq_think
                  (by
                    simp only [parallel.aux1, rmap, corec_eq]
                    rw [h])
              rw [H2]
              refine @Computation.think_terminates _ _ ?_
              have := H1 _ h
              rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> apply IH <;> simp [this]
      [Elab.step] [0.115825] 
            have lem1 : ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) :=
              by
              intro l S e
              obtain ⟨a, e⟩ := e
              have : corec parallel.aux1 (l, S) = return a :=
                by
                apply destruct_eq_pure
                simp only [parallel.aux1, rmap, corec_eq]
                rw [e]
              rw [this]
              exact ret_terminates a
            intro l S c m T
            revert l S
            apply @terminatesRecOn _ _ c T _ _
            · intro a l S m
              apply lem1
              induction l with
              | nil => simp at m
              | cons c l IH => ?_
              simp only [List.mem_cons] at m
              rcases m with e | m
              · rw [← e]
                simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
                split <;> simp
              · obtain ⟨a', e⟩ := IH m
                simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e
                rw [e]
                exact ⟨a', rfl⟩
            · intro s IH l S m
              have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' :=
                by
                induction l generalizing l' with
                | nil => simp at m
                | cons c l IH' => ?_
                simp only [List.mem_cons] at m
                rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                · rw [← e] at e'
                  revert e'
                  split
                  · simp
                  · simp only [destruct_think, Sum.inr.injEq]
                    rintro rfl
                    simp
                · rcases e :
                      List.foldr
                        (fun c o =>
                          match o with
                          | Sum.inl a => Sum.inl a
                          | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                        (Sum.inr List.nil) l with
                      a' | ls <;> erw [e] at e'
                  · contradiction
                  have := IH' m _ e
                  grind
              rcases h : parallel.aux2 l with a | l'
              · exact lem1 _ _ ⟨a, h⟩
              · have H2 : corec parallel.aux1 (l, S) = think _ :=
                  destruct_eq_think
                    (by
                      simp only [parallel.aux1, rmap, corec_eq]
                      rw [h])
                rw [H2]
                refine @Computation.think_terminates _ _ ?_
                have := H1 _ h
                rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> apply IH <;> simp [this]
        [Elab.step] [0.019000] have lem1 :
              ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) :=
              by
              intro l S e
              obtain ⟨a, e⟩ := e
              have : corec parallel.aux1 (l, S) = return a :=
                by
                apply destruct_eq_pure
                simp only [parallel.aux1, rmap, corec_eq]
                rw [e]
              rw [this]
              exact ret_terminates a
          [Elab.step] [0.018984] focus
                refine
                  no_implicit_lambda%
                    (have lem1 :
                      ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) := ?body✝;
                    ?_)
                case body✝ =>
                  with_annotate_state"by"
                    ( intro l S e
                      obtain ⟨a, e⟩ := e
                      have : corec parallel.aux1 (l, S) = return a :=
                        by
                        apply destruct_eq_pure
                        simp only [parallel.aux1, rmap, corec_eq]
                        rw [e]
                      rw [this]
                      exact ret_terminates a)
            [Elab.step] [0.018975] 
                  refine
                    no_implicit_lambda%
                      (have lem1 :
                        ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) :=
                        ?body✝;
                      ?_)
                  case body✝ =>
                    with_annotate_state"by"
                      ( intro l S e
                        obtain ⟨a, e⟩ := e
                        have : corec parallel.aux1 (l, S) = return a :=
                          by
                          apply destruct_eq_pure
                          simp only [parallel.aux1, rmap, corec_eq]
                          rw [e]
                        rw [this]
                        exact ret_terminates a)
              [Elab.step] [0.018972] 
                    refine
                      no_implicit_lambda%
                        (have lem1 :
                          ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) :=
                          ?body✝;
                        ?_)
                    case body✝ =>
                      with_annotate_state"by"
                        ( intro l S e
                          obtain ⟨a, e⟩ := e
                          have : corec parallel.aux1 (l, S) = return a :=
                            by
                            apply destruct_eq_pure
                            simp only [parallel.aux1, rmap, corec_eq]
                            rw [e]
                          rw [this]
                          exact ret_terminates a)
                [Elab.step] [0.017941] case body✝ =>
                      with_annotate_state"by"
                        ( intro l S e
                          obtain ⟨a, e⟩ := e
                          have : corec parallel.aux1 (l, S) = return a :=
                            by
                            apply destruct_eq_pure
                            simp only [parallel.aux1, rmap, corec_eq]
                            rw [e]
                          rw [this]
                          exact ret_terminates a)
                  [Elab.step] [0.017914] with_annotate_state"by"
                          ( intro l S e
                            obtain ⟨a, e⟩ := e
                            have : corec parallel.aux1 (l, S) = return a :=
                              by
                              apply destruct_eq_pure
                              simp only [parallel.aux1, rmap, corec_eq]
                              rw [e]
                            rw [this]
                            exact ret_terminates a)
                    [Elab.step] [0.017911] with_annotate_state"by"
                            ( intro l S e
                              obtain ⟨a, e⟩ := e
                              have : corec parallel.aux1 (l, S) = return a :=
                                by
                                apply destruct_eq_pure
                                simp only [parallel.aux1, rmap, corec_eq]
                                rw [e]
                              rw [this]
                              exact ret_terminates a)
                      [Elab.step] [0.017907] with_annotate_state"by"
                            ( intro l S e
                              obtain ⟨a, e⟩ := e
                              have : corec parallel.aux1 (l, S) = return a :=
                                by
                                apply destruct_eq_pure
                                simp only [parallel.aux1, rmap, corec_eq]
                                rw [e]
                              rw [this]
                              exact ret_terminates a)
                        [Elab.step] [0.017903] (
                              intro l S e
                              obtain ⟨a, e⟩ := e
                              have : corec parallel.aux1 (l, S) = return a :=
                                by
                                apply destruct_eq_pure
                                simp only [parallel.aux1, rmap, corec_eq]
                                rw [e]
                              rw [this]
                              exact ret_terminates a)
                          [Elab.step] [0.017899] 
                                intro l S e
                                obtain ⟨a, e⟩ := e
                                have : corec parallel.aux1 (l, S) = return a :=
                                  by
                                  apply destruct_eq_pure
                                  simp only [parallel.aux1, rmap, corec_eq]
                                  rw [e]
                                rw [this]
                                exact ret_terminates a
                            [Elab.step] [0.017894] 
                                  intro l S e
                                  obtain ⟨a, e⟩ := e
                                  have : corec parallel.aux1 (l, S) = return a :=
                                    by
                                    apply destruct_eq_pure
                                    simp only [parallel.aux1, rmap, corec_eq]
                                    rw [e]
                                  rw [this]
                                  exact ret_terminates a
                              [Elab.step] [0.016897] have : corec parallel.aux1 (l, S) = return a :=
                                    by
                                    apply destruct_eq_pure
                                    simp only [parallel.aux1, rmap, corec_eq]
                                    rw [e]
                                [Elab.step] [0.016886] focus
                                      refine
                                        no_implicit_lambda%
                                          (have : corec parallel.aux1 (l, S) = return a := ?body✝;
                                          ?_)
                                      case body✝ =>
                                        with_annotate_state"by"
                                          ( apply destruct_eq_pure
                                            simp only [parallel.aux1, rmap, corec_eq]
                                            rw [e])
                                  [Elab.step] [0.016882] 
                                        refine
                                          no_implicit_lambda%
                                            (have : corec parallel.aux1 (l, S) = return a := ?body✝;
                                            ?_)
                                        case body✝ =>
                                          with_annotate_state"by"
                                            ( apply destruct_eq_pure
                                              simp only [parallel.aux1, rmap, corec_eq]
                                              rw [e])
                                    [Elab.step] [0.016879] 
                                          refine
                                            no_implicit_lambda%
                                              (have : corec parallel.aux1 (l, S) = return a := ?body✝;
                                              ?_)
                                          case body✝ =>
                                            with_annotate_state"by"
                                              ( apply destruct_eq_pure
                                                simp only [parallel.aux1, rmap, corec_eq]
                                                rw [e])
                                      [Elab.step] [0.015801] case body✝ =>
                                            with_annotate_state"by"
                                              ( apply destruct_eq_pure
                                                simp only [parallel.aux1, rmap, corec_eq]
                                                rw [e])
                                        [Elab.step] [0.015782] with_annotate_state"by"
                                                ( apply destruct_eq_pure
                                                  simp only [parallel.aux1, rmap, corec_eq]
                                                  rw [e])
                                          [Elab.step] [0.015779] with_annotate_state"by"
                                                  ( apply destruct_eq_pure
                                                    simp only [parallel.aux1, rmap, corec_eq]
                                                    rw [e])
                                            [Elab.step] [0.015776] with_annotate_state"by"
                                                  ( apply destruct_eq_pure
                                                    simp only [parallel.aux1, rmap, corec_eq]
                                                    rw [e])
                                              [Elab.step] [0.015773] (
                                                    apply destruct_eq_pure
                                                    simp only [parallel.aux1, rmap, corec_eq]
                                                    rw [e])
                                                [Elab.step] [0.015770] 
                                                      apply destruct_eq_pure
                                                      simp only [parallel.aux1, rmap, corec_eq]
                                                      rw [e]
                                                  [Elab.step] [0.015766] 
                                                        apply destruct_eq_pure
                                                        simp only [parallel.aux1, rmap, corec_eq]
                                                        rw [e]
                                                    [Elab.step] [0.014670] simp only [parallel.aux1, rmap, corec_eq]
        [Elab.step] [0.045103] ·
              intro a l S m
              apply lem1
              induction l with
              | nil => simp at m
              | cons c l IH => ?_
              simp only [List.mem_cons] at m
              rcases m with e | m
              · rw [← e]
                simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
                split <;> simp
              · obtain ⟨a', e⟩ := IH m
                simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e
                rw [e]
                exact ⟨a', rfl⟩
          [Elab.step] [0.045023] 
                intro a l S m
                apply lem1
                induction l with
                | nil => simp at m
                | cons c l IH => ?_
                simp only [List.mem_cons] at m
                rcases m with e | m
                · rw [← e]
                  simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
                  split <;> simp
                · obtain ⟨a', e⟩ := IH m
                  simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e
                  rw [e]
                  exact ⟨a', rfl⟩
            [Elab.step] [0.045017] 
                  intro a l S m
                  apply lem1
                  induction l with
                  | nil => simp at m
                  | cons c l IH => ?_
                  simp only [List.mem_cons] at m
                  rcases m with e | m
                  · rw [← e]
                    simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
                    split <;> simp
                  · obtain ⟨a', e⟩ := IH m
                    simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e
                    rw [e]
                    exact ⟨a', rfl⟩
              [Elab.step] [0.032845] ·
                    rw [← e]
                    simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
                    split <;> simp
                [Elab.step] [0.032821] 
                      rw [← e]
                      simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
                      split <;> simp
                  [Elab.step] [0.032817] 
                        rw [← e]
                        simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
                        split <;> simp
                    [Elab.step] [0.024938] split <;> simp
                      [Elab.step] [0.024927] focus
                            split
                            with_annotate_state"<;>" skip
                            all_goals simp
                        [Elab.step] [0.024922] 
                              split
                              with_annotate_state"<;>" skip
                              all_goals simp
                          [Elab.step] [0.024918] 
                                split
                                with_annotate_state"<;>" skip
                                all_goals simp
                            [Elab.step] [0.023845] all_goals simp
                              [Elab.step] [0.022480] simp
                                [Elab.step] [0.022476] simp
                                  [Elab.step] [0.022470] simp
                                    [Meta.Tactic.simp.discharge] [0.020882] IsEmpty.exists_iff discharge ❌️
                                          IsEmpty α
                                      [Meta.synthInstance] [0.020479] ❌️ Nonempty α
        [Elab.step] [0.051034] ·
              intro s IH l S m
              have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' :=
                by
                induction l generalizing l' with
                | nil => simp at m
                | cons c l IH' => ?_
                simp only [List.mem_cons] at m
                rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                · rw [← e] at e'
                  revert e'
                  split
                  · simp
                  · simp only [destruct_think, Sum.inr.injEq]
                    rintro rfl
                    simp
                · rcases e :
                      List.foldr
                        (fun c o =>
                          match o with
                          | Sum.inl a => Sum.inl a
                          | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                        (Sum.inr List.nil) l with
                      a' | ls <;> erw [e] at e'
                  · contradiction
                  have := IH' m _ e
                  grind
              rcases h : parallel.aux2 l with a | l'
              · exact lem1 _ _ ⟨a, h⟩
              · have H2 : corec parallel.aux1 (l, S) = think _ :=
                  destruct_eq_think
                    (by
                      simp only [parallel.aux1, rmap, corec_eq]
                      rw [h])
                rw [H2]
                refine @Computation.think_terminates _ _ ?_
                have := H1 _ h
                rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> apply IH <;> simp [this]
          [Elab.step] [0.050982] 
                intro s IH l S m
                have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' :=
                  by
                  induction l generalizing l' with
                  | nil => simp at m
                  | cons c l IH' => ?_
                  simp only [List.mem_cons] at m
                  rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                  · rw [← e] at e'
                    revert e'
                    split
                    · simp
                    · simp only [destruct_think, Sum.inr.injEq]
                      rintro rfl
                      simp
                  · rcases e :
                        List.foldr
                          (fun c o =>
                            match o with
                            | Sum.inl a => Sum.inl a
                            | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                          (Sum.inr List.nil) l with
                        a' | ls <;> erw [e] at e'
                    · contradiction
                    have := IH' m _ e
                    grind
                rcases h : parallel.aux2 l with a | l'
                · exact lem1 _ _ ⟨a, h⟩
                · have H2 : corec parallel.aux1 (l, S) = think _ :=
                    destruct_eq_think
                      (by
                        simp only [parallel.aux1, rmap, corec_eq]
                        rw [h])
                  rw [H2]
                  refine @Computation.think_terminates _ _ ?_
                  have := H1 _ h
                  rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> apply IH <;> simp [this]
            [Elab.step] [0.050974] 
                  intro s IH l S m
                  have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' :=
                    by
                    induction l generalizing l' with
                    | nil => simp at m
                    | cons c l IH' => ?_
                    simp only [List.mem_cons] at m
                    rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                    · rw [← e] at e'
                      revert e'
                      split
                      · simp
                      · simp only [destruct_think, Sum.inr.injEq]
                        rintro rfl
                        simp
                    · rcases e :
                          List.foldr
                            (fun c o =>
                              match o with
                              | Sum.inl a => Sum.inl a
                              | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                            (Sum.inr List.nil) l with
                          a' | ls <;> erw [e] at e'
                      · contradiction
                      have := IH' m _ e
                      grind
                  rcases h : parallel.aux2 l with a | l'
                  · exact lem1 _ _ ⟨a, h⟩
                  · have H2 : corec parallel.aux1 (l, S) = think _ :=
                      destruct_eq_think
                        (by
                          simp only [parallel.aux1, rmap, corec_eq]
                          rw [h])
                    rw [H2]
                    refine @Computation.think_terminates _ _ ?_
                    have := H1 _ h
                    rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> apply IH <;> simp [this]
              [Elab.step] [0.040942] have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' :=
                    by
                    induction l generalizing l' with
                    | nil => simp at m
                    | cons c l IH' => ?_
                    simp only [List.mem_cons] at m
                    rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                    · rw [← e] at e'
                      revert e'
                      split
                      · simp
                      · simp only [destruct_think, Sum.inr.injEq]
                        rintro rfl
                        simp
                    · rcases e :
                          List.foldr
                            (fun c o =>
                              match o with
                              | Sum.inl a => Sum.inl a
                              | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                            (Sum.inr List.nil) l with
                          a' | ls <;> erw [e] at e'
                      · contradiction
                      have := IH' m _ e
                      grind
                [Elab.step] [0.040933] focus
                      refine
                        no_implicit_lambda%
                          (have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' := ?body✝;
                          ?_)
                      case body✝ =>
                        with_annotate_state"by"
                          ( induction l generalizing l' with
                            | nil => simp at m
                            | cons c l IH' => ?_
                            simp only [List.mem_cons] at m
                            rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                            · rw [← e] at e'
                              revert e'
                              split
                              · simp
                              · simp only [destruct_think, Sum.inr.injEq]
                                rintro rfl
                                simp
                            · rcases e :
                                  List.foldr
                                    (fun c o =>
                                      match o with
                                      | Sum.inl a => Sum.inl a
                                      | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                    (Sum.inr List.nil) l with
                                  a' | ls <;> erw [e] at e'
                              · contradiction
                              have := IH' m _ e
                              grind)
                  [Elab.step] [0.040929] 
                        refine
                          no_implicit_lambda%
                            (have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' := ?body✝;
                            ?_)
                        case body✝ =>
                          with_annotate_state"by"
                            ( induction l generalizing l' with
                              | nil => simp at m
                              | cons c l IH' => ?_
                              simp only [List.mem_cons] at m
                              rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                              · rw [← e] at e'
                                revert e'
                                split
                                · simp
                                · simp only [destruct_think, Sum.inr.injEq]
                                  rintro rfl
                                  simp
                              · rcases e :
                                    List.foldr
                                      (fun c o =>
                                        match o with
                                        | Sum.inl a => Sum.inl a
                                        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                      (Sum.inr List.nil) l with
                                    a' | ls <;> erw [e] at e'
                                · contradiction
                                have := IH' m _ e
                                grind)
                    [Elab.step] [0.040926] 
                          refine
                            no_implicit_lambda%
                              (have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' := ?body✝;
                              ?_)
                          case body✝ =>
                            with_annotate_state"by"
                              ( induction l generalizing l' with
                                | nil => simp at m
                                | cons c l IH' => ?_
                                simp only [List.mem_cons] at m
                                rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                · rw [← e] at e'
                                  revert e'
                                  split
                                  · simp
                                  · simp only [destruct_think, Sum.inr.injEq]
                                    rintro rfl
                                    simp
                                · rcases e :
                                      List.foldr
                                        (fun c o =>
                                          match o with
                                          | Sum.inl a => Sum.inl a
                                          | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                        (Sum.inr List.nil) l with
                                      a' | ls <;> erw [e] at e'
                                  · contradiction
                                  have := IH' m _ e
                                  grind)
                      [Elab.step] [0.040081] case body✝ =>
                            with_annotate_state"by"
                              ( induction l generalizing l' with
                                | nil => simp at m
                                | cons c l IH' => ?_
                                simp only [List.mem_cons] at m
                                rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                · rw [← e] at e'
                                  revert e'
                                  split
                                  · simp
                                  · simp only [destruct_think, Sum.inr.injEq]
                                    rintro rfl
                                    simp
                                · rcases e :
                                      List.foldr
                                        (fun c o =>
                                          match o with
                                          | Sum.inl a => Sum.inl a
                                          | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                        (Sum.inr List.nil) l with
                                      a' | ls <;> erw [e] at e'
                                  · contradiction
                                  have := IH' m _ e
                                  grind)
                        [Elab.step] [0.040054] with_annotate_state"by"
                                ( induction l generalizing l' with
                                  | nil => simp at m
                                  | cons c l IH' => ?_
                                  simp only [List.mem_cons] at m
                                  rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                  · rw [← e] at e'
                                    revert e'
                                    split
                                    · simp
                                    · simp only [destruct_think, Sum.inr.injEq]
                                      rintro rfl
                                      simp
                                  · rcases e :
                                        List.foldr
                                          (fun c o =>
                                            match o with
                                            | Sum.inl a => Sum.inl a
                                            | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                          (Sum.inr List.nil) l with
                                        a' | ls <;> erw [e] at e'
                                    · contradiction
                                    have := IH' m _ e
                                    grind)
                          [Elab.step] [0.040051] with_annotate_state"by"
                                  ( induction l generalizing l' with
                                    | nil => simp at m
                                    | cons c l IH' => ?_
                                    simp only [List.mem_cons] at m
                                    rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                    · rw [← e] at e'
                                      revert e'
                                      split
                                      · simp
                                      · simp only [destruct_think, Sum.inr.injEq]
                                        rintro rfl
                                        simp
                                    · rcases e :
                                          List.foldr
                                            (fun c o =>
                                              match o with
                                              | Sum.inl a => Sum.inl a
                                              | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                            (Sum.inr List.nil) l with
                                          a' | ls <;> erw [e] at e'
                                      · contradiction
                                      have := IH' m _ e
                                      grind)
                            [Elab.step] [0.040047] with_annotate_state"by"
                                  ( induction l generalizing l' with
                                    | nil => simp at m
                                    | cons c l IH' => ?_
                                    simp only [List.mem_cons] at m
                                    rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                    · rw [← e] at e'
                                      revert e'
                                      split
                                      · simp
                                      · simp only [destruct_think, Sum.inr.injEq]
                                        rintro rfl
                                        simp
                                    · rcases e :
                                          List.foldr
                                            (fun c o =>
                                              match o with
                                              | Sum.inl a => Sum.inl a
                                              | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                            (Sum.inr List.nil) l with
                                          a' | ls <;> erw [e] at e'
                                      · contradiction
                                      have := IH' m _ e
                                      grind)
                              [Elab.step] [0.040044] (
                                    induction l generalizing l' with
                                    | nil => simp at m
                                    | cons c l IH' => ?_
                                    simp only [List.mem_cons] at m
                                    rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                    · rw [← e] at e'
                                      revert e'
                                      split
                                      · simp
                                      · simp only [destruct_think, Sum.inr.injEq]
                                        rintro rfl
                                        simp
                                    · rcases e :
                                          List.foldr
                                            (fun c o =>
                                              match o with
                                              | Sum.inl a => Sum.inl a
                                              | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                            (Sum.inr List.nil) l with
                                          a' | ls <;> erw [e] at e'
                                      · contradiction
                                      have := IH' m _ e
                                      grind)
                                [Elab.step] [0.040040] 
                                      induction l generalizing l' with
                                      | nil => simp at m
                                      | cons c l IH' => ?_
                                      simp only [List.mem_cons] at m
                                      rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                      · rw [← e] at e'
                                        revert e'
                                        split
                                        · simp
                                        · simp only [destruct_think, Sum.inr.injEq]
                                          rintro rfl
                                          simp
                                      · rcases e :
                                            List.foldr
                                              (fun c o =>
                                                match o with
                                                | Sum.inl a => Sum.inl a
                                                | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                              (Sum.inr List.nil) l with
                                            a' | ls <;> erw [e] at e'
                                        · contradiction
                                        have := IH' m _ e
                                        grind
                                  [Elab.step] [0.040036] 
                                        induction l generalizing l' with
                                        | nil => simp at m
                                        | cons c l IH' => ?_
                                        simp only [List.mem_cons] at m
                                        rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
                                        · rw [← e] at e'
                                          revert e'
                                          split
                                          · simp
                                          · simp only [destruct_think, Sum.inr.injEq]
                                            rintro rfl
                                            simp
                                        · rcases e :
                                              List.foldr
                                                (fun c o =>
                                                  match o with
                                                  | Sum.inl a => Sum.inl a
                                                  | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                                (Sum.inr List.nil) l with
                                              a' | ls <;> erw [e] at e'
                                          · contradiction
                                          have := IH' m _ e
                                          grind
                                    [Elab.step] [0.024684] ·
                                          rcases e :
                                              List.foldr
                                                (fun c o =>
                                                  match o with
                                                  | Sum.inl a => Sum.inl a
                                                  | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                                (Sum.inr List.nil) l with
                                              a' | ls <;>
                                            erw [e] at e'
                                          · contradiction
                                          have := IH' m _ e
                                          grind
                                      [Elab.step] [0.024656] 
                                            rcases e :
                                                List.foldr
                                                  (fun c o =>
                                                    match o with
                                                    | Sum.inl a => Sum.inl a
                                                    | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                                  (Sum.inr List.nil) l with
                                                a' | ls <;>
                                              erw [e] at e'
                                            · contradiction
                                            have := IH' m _ e
                                            grind
                                        [Elab.step] [0.024652] 
                                              rcases e :
                                                  List.foldr
                                                    (fun c o =>
                                                      match o with
                                                      | Sum.inl a => Sum.inl a
                                                      | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
                                                    (Sum.inr List.nil) l with
                                                  a' | ls <;>
                                                erw [e] at e'
                                              · contradiction
                                              have := IH' m _ e
                                              grind
                                          [Elab.step] [0.013736] grind
Build completed successfully (703 jobs).

---

[github-actions]

PR summary 6b1d0f08cb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
517	-1	porting notes

Current commit 3dad389a7e
Reference commit 6b1d0f08cb

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[grunweg]

Thanks!
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[RemyDegenne]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Post-Build Step
• Lint style
• Build