-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem sizeUpTo_index_le (j : Fin n) : c.sizeUpTo (c.index j) ≤ j

Proof state:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
i₁ : ℕ := (↑i).pred
i₁_lt_i : i₁ < ↑i
i₁_succ : i₁ + 1 = ↑i
this : c.sizeUpTo ↑i ≤ ↑j
⊢ False

Tactic:
exact Nat.lt_le_asymm H this

Result:
no goals

Proof state:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
⊢ 0 < ↑i

Tactic:
by_contra! i_pos

Result:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : ↑i ≤ 0
⊢ False

Proof state:
n : ℕ
c : Composition n
j : Fin n
H : ¬c.sizeUpTo ↑(c.index j) ≤ ↑j
⊢ False

Tactic:
set i := c.index j

Result:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ¬c.sizeUpTo ↑i ≤ ↑j
⊢ False

Proof state:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ¬c.sizeUpTo ↑i ≤ ↑j
⊢ False

Tactic:
push_neg at H

Result:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
⊢ False

Proof state:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
i₁ : ℕ := (↑i).pred
i₁_lt_i : i₁ < ↑i
i₁_succ : i₁ + 1 = ↑i
this : ¬(↑j < c.sizeUpTo (i₁ + 1) ∧ i₁ < c.length)
⊢ False

Tactic:
simp [lt_trans i₁_lt_i (c.index j).2, i₁_succ] at this

Result:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
i₁ : ℕ := (↑i).pred
i₁_lt_i : i₁ < ↑i
i₁_succ : i₁ + 1 = ↑i
this : c.sizeUpTo ↑i ≤ ↑j
⊢ False

Proof state:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
⊢ False

Tactic:
let i₁ := (i : ℕ).pred

Result:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
i₁ : ℕ := (↑i).pred
⊢ False

Proof state:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
⊢ False

Tactic:
have i_pos : (0 : ℕ) < i := by
  by_contra! i_pos
  revert H
  simp [nonpos_iff_eq_zero.1 i_pos, c.sizeUpTo_zero]

Result:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
⊢ False

Proof state:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : ↑i ≤ 0
⊢ False

Tactic:
revert H

Result:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
i_pos : ↑i ≤ 0
⊢ ↑j < c.sizeUpTo ↑i → False

Proof state:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
i_pos : ↑i ≤ 0
⊢ ↑j < c.sizeUpTo ↑i → False

Tactic:
simp [nonpos_iff_eq_zero.1 i_pos, c.sizeUpTo_zero]

Result:
no goals

Proof state:
n : ℕ
c : Composition n
j : Fin n
⊢ c.sizeUpTo ↑(c.index j) ≤ ↑j

Tactic:
by_contra H

Result:
n : ℕ
c : Composition n
j : Fin n
H : ¬c.sizeUpTo ↑(c.index j) ≤ ↑j
⊢ False

Proof state:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
i₁ : ℕ := (↑i).pred
⊢ False

Tactic:
have i₁_lt_i : i₁ < i := Nat.pred_lt (ne_of_gt i_pos)

Result:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
i₁ : ℕ := (↑i).pred
i₁_lt_i : i₁ < ↑i
⊢ False

Proof state:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
i₁ : ℕ := (↑i).pred
i₁_lt_i : i₁ < ↑i
⊢ False

Tactic:
have i₁_succ : i₁ + 1 = i := Nat.succ_pred_eq_of_pos i_pos

Result:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
i₁ : ℕ := (↑i).pred
i₁_lt_i : i₁ < ↑i
i₁_succ : i₁ + 1 = ↑i
⊢ False

Proof state:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
i₁ : ℕ := (↑i).pred
i₁_lt_i : i₁ < ↑i
i₁_succ : i₁ + 1 = ↑i
⊢ False

Tactic:
have := Nat.find_min (c.index_exists j.2) i₁_lt_i

Result:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
i₁ : ℕ := (↑i).pred
i₁_lt_i : i₁ < ↑i
i₁_succ : i₁ + 1 = ↑i
this : ¬(↑j < c.sizeUpTo (i₁ + 1) ∧ i₁ < c.length)
⊢ False