-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
inr :
  ∀
    (this :
      ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin c.length} (h : i₁ ≠ i₂) (h' : i₁ < i₂),
        _root_.Disjoint (α := Set (Fin n))
          (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n))
          (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)))
    (h' : ¬i₁ < i₂),
    _root_.Disjoint (α := Set (Fin n))
      (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n))
      (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n))
wlog wlog₁ :
  ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin c.length} (h : i₁ ≠ i₂) (h' : i₁ < i₂),
    _root_.Disjoint (α := Set (Fin n))
      (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n))
      (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n))
wlog₂ :
  ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin c.length} (h : i₁ ≠ i₂) (h' : i₁ < i₂)
    (d :
      ¬_root_.Disjoint (α := Set (Fin n))
          (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n))
          (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n))),
    False
wlog₃ :
  ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin c.length} (h : i₁ ≠ i₂) (h' : i₁ < i₂)
    (d :
      ¬_root_.Disjoint (α := Set (Fin n))
          (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n))
          (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)))
    (x : Fin n)
    (hx₁ :
      Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n)) x)
    (hx₂ :
      Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)) x),
    False
wlog₄ :
  ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin c.length} (h : i₁ ≠ i₂) (h' : i₁ < i₂)
    (d :
      ¬_root_.Disjoint (α := Set (Fin n))
          (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n))
          (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)))
    (x : Fin n)
    (hx₁ :
      Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n)) x)
    (hx₂ :
      Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)) x)
    (A : (↑i₁ : ℕ).succ ≤ (↑i₂ : ℕ)), False
wlog₅ :
  ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin c.length} (h : i₁ ≠ i₂) (h' : i₁ < i₂)
    (d :
      ¬_root_.Disjoint (α := Set (Fin n))
          (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n))
          (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)))
    (x : Fin n)
    (hx₁ :
      Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n)) x)
    (hx₂ :
      Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n)) x)
    (A : (↑i₁ : ℕ).succ ≤ (↑i₂ : ℕ)), (↑x : ℕ) < (↑x : ℕ)
⊢ _root_.Disjoint (α := Set (Fin n))
    (Set.range (ι := Fin (c.blocksFun i₁)) (⇑(c.embedding i₁) : (a : Fin (c.blocksFun i₁)) → Fin n))
    (Set.range (ι := Fin (c.blocksFun i₂)) (⇑(c.embedding i₂) : (a : Fin (c.blocksFun i₂)) → Fin n))

Tactic:
classical
    wlog h' : i₁ < i₂
    · exact (this c h.symm (h.lt_or_gt.resolve_left h')).symm
    by_contra d
    obtain ⟨x, hx₁, hx₂⟩ :
      ∃ x : Fin n, x ∈ Set.range (c.embedding i₁) ∧ x ∈ Set.range (c.embedding i₂) :=
      Set.not_disjoint_iff.1 d
    have A : (i₁ : ℕ).succ ≤ i₂ := Nat.succ_le_of_lt h'
    apply lt_irrefl (x : ℕ)
    calc
      (x : ℕ) < c.sizeUpTo (i₁ : ℕ).succ := (c.mem_range_embedding_iff.1 hx₁).2
      _ ≤ c.sizeUpTo (i₂ : ℕ) := monotone_sum_take _ A
      _ ≤ x := (c.mem_range_embedding_iff.1 hx₂).1

Premises used: Fin.val, Composition.embedding, Set.range, Fin, Nat.succ, DFunLike.coe, Composition.sizeUpTo