Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case succ.succ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ c : OrderedFinpartition n
j i : Fin c.length
a✝¹ :
  (i.castSucc < j.castSucc →
      (fun m ↦
            cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
              ⟨cons 1 c.partSize m - 1, ⋯⟩)
          i.castSucc <
        (fun m ↦
            cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
              ⟨cons 1 c.partSize m - 1, ⋯⟩)
          j.castSucc) →
    i.castSucc < j.succ →
      (fun m ↦
            cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
              ⟨cons 1 c.partSize m - 1, ⋯⟩)
          i.castSucc <
        (fun m ↦
            cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
              ⟨cons 1 c.partSize m - 1, ⋯⟩)
          j.succ
a✝ :
  i.succ < j.castSucc →
    (fun m ↦
          cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
            ⟨cons 1 c.partSize m - 1, ⋯⟩)
        i.succ <
      (fun m ↦
          cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
            ⟨cons 1 c.partSize m - 1, ⋯⟩)
        j.castSucc
hij : i.succ < j.succ
⊢ (fun m ↦
        cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
          ⟨cons 1 c.partSize m - 1, ⋯⟩)
      i.succ <
    (fun m ↦
        cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
          ⟨cons 1 c.partSize m - 1, ⋯⟩)
      j.succ

Tactic:
simp only [cons_succ, cases_succ, comp_apply, succ_lt_succ_iff]

Goal state after:
case succ.succ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ c : OrderedFinpartition n
j i : Fin c.length
a✝¹ :
  (i.castSucc < j.castSucc →
      (fun m ↦
            cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
              ⟨cons 1 c.partSize m - 1, ⋯⟩)
          i.castSucc <
        (fun m ↦
            cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
              ⟨cons 1 c.partSize m - 1, ⋯⟩)
          j.castSucc) →
    i.castSucc < j.succ →
      (fun m ↦
            cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
              ⟨cons 1 c.partSize m - 1, ⋯⟩)
          i.castSucc <
        (fun m ↦
            cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
              ⟨cons 1 c.partSize m - 1, ⋯⟩)
          j.succ
a✝ :
  i.succ < j.castSucc →
    (fun m ↦
          cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
            ⟨cons 1 c.partSize m - 1, ⋯⟩)
        i.succ <
      (fun m ↦
          cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
            ⟨cons 1 c.partSize m - 1, ⋯⟩)
        j.castSucc
hij : i.succ < j.succ
⊢ c.emb i ⟨c.partSize i - 1, ⋯⟩ < c.emb j ⟨c.partSize j - 1, ⋯⟩