no goals
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
⊢ _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
classical
  wlog h' : i₁ < i₂
  exact (this c h.symm (h.lt_or_lt.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
case inr
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
this :
  ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin (length c)},
    i₁ ≠ i₂ → i₁ < i₂ → _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
h' : ¬i₁ < i₂
⊢ _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))

n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
⊢ _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
⊢ _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
wlog h' : i₁ < i₂
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
⊢ _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
case inr
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
this :
  ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin (length c)},
    i₁ ≠ i₂ → i₁ < i₂ → _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
h' : ¬i₁ < i₂
⊢ _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))

n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
⊢ _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
exact (this c h.symm (h.lt_or_lt.resolve_left h')).symm
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
⊢ False
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
⊢ _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
by_contra d
case intro.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
x : Fin n
hx₁ : x ∈ Set.range ↑(embedding c i₁)
hx₂ : x ∈ Set.range ↑(embedding c i₂)
⊢ False
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
⊢ False
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
case intro.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
x : Fin n
hx₁ : x ∈ Set.range ↑(embedding c i₁)
hx₂ : x ∈ Set.range ↑(embedding c i₂)
A : Nat.succ ↑i₁ ≤ ↑i₂
⊢ False
case intro.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
x : Fin n
hx₁ : x ∈ Set.range ↑(embedding c i₁)
hx₂ : x ∈ Set.range ↑(embedding c i₂)
⊢ False
have A : (i₁ : ℕ).succ ≤ i₂ := Nat.succ_le_of_lt h'
case intro.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
x : Fin n
hx₁ : x ∈ Set.range ↑(embedding c i₁)
hx₂ : x ∈ Set.range ↑(embedding c i₂)
A : Nat.succ ↑i₁ ≤ ↑i₂
⊢ ↑x < ↑x
case intro.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
x : Fin n
hx₁ : x ∈ Set.range ↑(embedding c i₁)
hx₂ : x ∈ Set.range ↑(embedding c i₂)
A : Nat.succ ↑i₁ ≤ ↑i₂
⊢ False
apply lt_irrefl (x : ℕ)
no goals
case intro.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
x : Fin n
hx₁ : x ∈ Set.range ↑(embedding c i₁)
hx₂ : x ∈ Set.range ↑(embedding c i₂)
A : Nat.succ ↑i₁ ≤ ↑i₂
⊢ ↑x < ↑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