n : ℕ
c : Composition n
j : Fin n
H : ¬sizeUpTo c ↑(index c j) ≤ ↑j
⊢ False
n : ℕ
c : Composition n
j : Fin n
⊢ sizeUpTo c ↑(index c j) ≤ ↑j
by_contra H
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ¬sizeUpTo c ↑i ≤ ↑j
⊢ False
n : ℕ
c : Composition n
j : Fin n
H : ¬sizeUpTo c ↑(index c j) ≤ ↑j
⊢ False
set i := c.index j
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
⊢ False
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ¬sizeUpTo c ↑i ≤ ↑j
⊢ False
push_neg  at H
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
⊢ False
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
⊢ False
have i_pos : (0 : ℕ) < i := by
  by_contra' i_pos
  revert H
  simp [nonpos_iff_eq_zero.1 i_pos, c.sizeUpTo_zero]
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
i₁ : ℕ := Nat.pred ↑i
⊢ False
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
⊢ False
let i₁ := (i : ℕ).pred
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
i₁ : ℕ := Nat.pred ↑i
i₁_lt_i : i₁ < ↑i
⊢ False
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
i₁ : ℕ := Nat.pred ↑i
⊢ False
have i₁_lt_i : i₁ < i := Nat.pred_lt (ne_of_gt i_pos)
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
i₁ : ℕ := Nat.pred ↑i
i₁_lt_i : i₁ < ↑i
i₁_succ : Nat.succ i₁ = ↑i
⊢ False
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
i₁ : ℕ := Nat.pred ↑i
i₁_lt_i : i₁ < ↑i
⊢ False
have i₁_succ : i₁.succ = i := Nat.succ_pred_eq_of_pos i_pos
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
i₁ : ℕ := Nat.pred ↑i
i₁_lt_i : i₁ < ↑i
i₁_succ : Nat.succ i₁ = ↑i
this : ¬(↑j < sizeUpTo c (Nat.succ i₁) ∧ i₁ < length c)
⊢ False
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
i₁ : ℕ := Nat.pred ↑i
i₁_lt_i : i₁ < ↑i
i₁_succ : Nat.succ i₁ = ↑i
⊢ False
have := Nat.find_min (c.index_exists j.2) i₁_lt_i
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
i₁ : ℕ := Nat.pred ↑i
i₁_lt_i : i₁ < ↑i
i₁_succ : Nat.succ i₁ = ↑i
this : sizeUpTo c ↑(index c j) ≤ ↑j
⊢ False
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
i₁ : ℕ := Nat.pred ↑i
i₁_lt_i : i₁ < ↑i
i₁_succ : Nat.succ i₁ = ↑i
this : ¬(↑j < sizeUpTo c (Nat.succ i₁) ∧ i₁ < length c)
⊢ False
simp [lt_trans i₁_lt_i (c.index j).2, i₁_succ] at this
no goals
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
i₁ : ℕ := Nat.pred ↑i
i₁_lt_i : i₁ < ↑i
i₁_succ : Nat.succ i₁ = ↑i
this : sizeUpTo c ↑(index c j) ≤ ↑j
⊢ False
exact Nat.lt_le_antisymm H this
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : ↑(index c j) ≤ 0
⊢ False
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
⊢ 0 < ↑i
by_contra' i_pos
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
i_pos : ↑(index c j) ≤ 0
⊢ ↑j < sizeUpTo c ↑(index c j) → False
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : ↑(index c j) ≤ 0
⊢ False
revert H
no goals
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
i_pos : ↑(index c j) ≤ 0
⊢ ↑j < sizeUpTo c ↑(index c j) → False
simp [nonpos_iff_eq_zero.1 i_pos, c.sizeUpTo_zero]