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
i : Fin c.length
hi : i.succ ∈ univ
j : Fin c.length
a✝¹ :
  j.castSucc ∈ univ →
    (i.castSucc ∈ univ →
        i.castSucc ≠ j.castSucc →
          j.castSucc < i.castSucc →
            (Disjoint on fun m ↦
                range
                  (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0)
                    (fun m ↦ succ ∘ c.emb m) m))
              i.castSucc j.castSucc) →
      i.succ ≠ j.castSucc →
        j.castSucc < i.succ →
          (Disjoint on fun m ↦
              range
                (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m)
                  m))
            i.succ j.castSucc
hj : j.succ ∈ univ
a✝ :
  i.castSucc ∈ univ →
    i.castSucc ≠ j.succ →
      j.succ < i.castSucc →
        (Disjoint on fun m ↦
            range
              (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m)
                m))
          i.castSucc j.succ
hij : i.succ ≠ j.succ
h : j.succ < i.succ
⊢ ∀ ⦃a : Fin (n + 1)⦄, a ∈ range (succ ∘ c.emb i) → ∀ ⦃b : Fin (n + 1)⦄, b ∈ range (succ ∘ c.emb j) → a ≠ b

Tactic:
simp only [mem_range, comp_apply, ne_eq, forall_exists_index, forall_apply_eq_imp_iff,
          succ_inj]

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
i : Fin c.length
hi : i.succ ∈ univ
j : Fin c.length
a✝¹ :
  j.castSucc ∈ univ →
    (i.castSucc ∈ univ →
        i.castSucc ≠ j.castSucc →
          j.castSucc < i.castSucc →
            (Disjoint on fun m ↦
                range
                  (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0)
                    (fun m ↦ succ ∘ c.emb m) m))
              i.castSucc j.castSucc) →
      i.succ ≠ j.castSucc →
        j.castSucc < i.succ →
          (Disjoint on fun m ↦
              range
                (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m)
                  m))
            i.succ j.castSucc
hj : j.succ ∈ univ
a✝ :
  i.castSucc ∈ univ →
    i.castSucc ≠ j.succ →
      j.succ < i.castSucc →
        (Disjoint on fun m ↦
            range
              (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m)
                m))
          i.castSucc j.succ
hij : i.succ ≠ j.succ
h : j.succ < i.succ
⊢ ∀ (a : Fin (cons 1 c.partSize i.succ)) (a_1 : Fin (cons 1 c.partSize j.succ)), ¬c.emb i a = c.emb j a_1