-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem disjoint_range {i₁ i₂ : Fin c.length} (h : i₁ ≠ i₂) :
    Disjoint (Set.range (c.embedding i₁)) (Set.range (c.embedding i₂))

Proof state:
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
⊢ False

Tactic:
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

Result:
case intro.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
x : Fin n
hx₁ : x ∈ Set.range ⇑(c.embedding i₁)
hx₂ : x ∈ Set.range ⇑(c.embedding i₂)
⊢ False

Proof state:
case intro.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
x : Fin n
hx₁ : x ∈ Set.range ⇑(c.embedding i₁)
hx₂ : x ∈ Set.range ⇑(c.embedding i₂)
A : (↑i₁).succ ≤ ↑i₂
⊢ False

Tactic:
apply lt_irrefl (x : ℕ)

Result:
case intro.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
x : Fin n
hx₁ : x ∈ Set.range ⇑(c.embedding i₁)
hx₂ : x ∈ Set.range ⇑(c.embedding i₂)
A : (↑i₁).succ ≤ ↑i₂
⊢ ↑x < ↑x

Proof state:
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
⊢ _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))

Tactic:
wlog h' : i₁ < i₂

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

n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
⊢ _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))

Proof state:
case intro.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
x : Fin n
hx₁ : x ∈ Set.range ⇑(c.embedding i₁)
hx₂ : x ∈ Set.range ⇑(c.embedding i₂)
⊢ False

Tactic:
have A : (i₁ : ℕ).succ ≤ i₂ := Nat.succ_le_of_lt h'

Result:
case intro.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
x : Fin n
hx₁ : x ∈ Set.range ⇑(c.embedding i₁)
hx₂ : x ∈ Set.range ⇑(c.embedding i₂)
A : (↑i₁).succ ≤ ↑i₂
⊢ False

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

Tactic:
exact (this c h.symm (h.lt_or_lt.resolve_left h')).symm

Result:
no goals

Proof state:
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
⊢ _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))

Tactic:
by_contra d

Result:
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
⊢ False

Proof state:
case intro.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
x : Fin n
hx₁ : x ∈ Set.range ⇑(c.embedding i₁)
hx₂ : x ∈ Set.range ⇑(c.embedding i₂)
A : (↑i₁).succ ≤ ↑i₂
⊢ ↑x < ↑x

Tactic:
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

Result:
no goals