-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
@[simp]
lemma mkOfSucc_subinterval_eq {n} (j l : ℕ) (hjl : j + l ≤ n) (i : Fin l) :
    mkOfSucc i ≫ subinterval j l hjl =
    mkOfSucc ⟨j + i.1, Nat.lt_of_lt_of_le (Nat.add_lt_add_left i.2 j) hjl⟩

Proof state:
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin (⦋1⦌.len + 1)
⊢ ↑(match 0 with
        | 0 => i✝.castSucc
        | 1 => i✝.succ) +
      j =
    ↑(match 0 with
      | 0 => ⟨j + ↑i✝, ⋯⟩
      | 1 => ⟨j + ↑i✝ + 1, ⋯⟩)

Tactic:
rw [add_comm]

Result:
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin (⦋1⦌.len + 1)
⊢ j +
      ↑(match 0 with
        | 0 => i✝.castSucc
        | 1 => i✝.succ) =
    ↑(match 0 with
      | 0 => ⟨j + ↑i✝, ⋯⟩
      | 1 => ⟨j + ↑i✝ + 1, ⋯⟩)

Proof state:
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin (⦋1⦌.len + 1)
⊢ ↑(match 1 with
        | 0 => i✝.castSucc
        | 1 => i✝.succ) +
      j =
    ↑(match 1 with
      | 0 => ⟨j + ↑i✝, ⋯⟩
      | 1 => ⟨j + ↑i✝ + 1, ⋯⟩)

Tactic:
rw [← Nat.add_comm j _]

Result:
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin (⦋1⦌.len + 1)
⊢ j +
      ↑(match 1 with
        | 0 => i✝.castSucc
        | 1 => i✝.succ) =
    ↑(match 1 with
      | 0 => ⟨j + ↑i✝, ⋯⟩
      | 1 => ⟨j + ↑i✝ + 1, ⋯⟩)

Proof state:
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin (⦋1⦌.len + 1)
⊢ ↑((Hom.toOrderHom
          (mkHom
              {
                toFun := fun x =>
                  match x with
                  | 0 => i✝.castSucc
                  | 1 => i✝.succ,
                monotone' := ⋯ } ≫
            mkHom { toFun := fun i => ⟨↑i + j, ⋯⟩, monotone' := ⋯ }))
        0) =
    ↑((Hom.toOrderHom
          (mkHom
            {
              toFun := fun x =>
                match x with
                | 0 => ⟨j + ↑i✝, ⋯⟩.castSucc
                | 1 => ⟨j + ↑i✝, ⋯⟩.succ,
              monotone' := ⋯ }))
        0)

Tactic:
simp only [len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk,
  OrderHom.mk_comp_mk, Fin.isValue, OrderHom.coe_mk, Function.comp_apply, Fin.castSucc_mk,
  Fin.succ_mk]

Result:
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin (⦋1⦌.len + 1)
⊢ ↑(match 0 with
        | 0 => i✝.castSucc
        | 1 => i✝.succ) +
      j =
    ↑(match 0 with
      | 0 => ⟨j + ↑i✝, ⋯⟩
      | 1 => ⟨j + ↑i✝ + 1, ⋯⟩)

Proof state:
n j l : ℕ
hjl : j + l ≤ n
i : Fin l
⊢ mkOfSucc i ≫ subinterval j l hjl = mkOfSucc ⟨j + ↑i, ⋯⟩

Tactic:
unfold subinterval mkOfSucc

Result:
n j l : ℕ
hjl : j + l ≤ n
i : Fin l
⊢ mkHom
        {
          toFun := fun x =>
            match x with
            | 0 => i.castSucc
            | 1 => i.succ,
          monotone' := ⋯ } ≫
      mkHom { toFun := fun i => ⟨↑i + j, ⋯⟩, monotone' := ⋯ } =
    mkHom
      {
        toFun := fun x =>
          match x with
          | 0 => ⟨j + ↑i, ⋯⟩.castSucc
          | 1 => ⟨j + ↑i, ⋯⟩.succ,
        monotone' := ⋯ }

Proof state:
n j l : ℕ
hjl : j + l ≤ n
i : Fin l
⊢ mkHom
        {
          toFun := fun x =>
            match x with
            | 0 => i.castSucc
            | 1 => i.succ,
          monotone' := ⋯ } ≫
      mkHom { toFun := fun i => ⟨↑i + j, ⋯⟩, monotone' := ⋯ } =
    mkHom
      {
        toFun := fun x =>
          match x with
          | 0 => ⟨j + ↑i, ⋯⟩.castSucc
          | 1 => ⟨j + ↑i, ⋯⟩.succ,
        monotone' := ⋯ }

Tactic:
ext i

Result:
case a.h.h.h
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin (⦋1⦌.len + 1)
⊢ ↑((Hom.toOrderHom
          (mkHom
              {
                toFun := fun x =>
                  match x with
                  | 0 => i✝.castSucc
                  | 1 => i✝.succ,
                monotone' := ⋯ } ≫
            mkHom { toFun := fun i => ⟨↑i + j, ⋯⟩, monotone' := ⋯ }))
        i) =
    ↑((Hom.toOrderHom
          (mkHom
            {
              toFun := fun x =>
                match x with
                | 0 => ⟨j + ↑i✝, ⋯⟩.castSucc
                | 1 => ⟨j + ↑i✝, ⋯⟩.succ,
              monotone' := ⋯ }))
        i)

Proof state:
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin (⦋1⦌.len + 1)
⊢ j +
      ↑(match 0 with
        | 0 => i✝.castSucc
        | 1 => i✝.succ) =
    ↑(match 0 with
      | 0 => ⟨j + ↑i✝, ⋯⟩
      | 1 => ⟨j + ↑i✝ + 1, ⋯⟩)

Tactic:
rfl

Result:
no goals

Proof state:
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin (⦋1⦌.len + 1)
⊢ j +
      ↑(match 1 with
        | 0 => i✝.castSucc
        | 1 => i✝.succ) =
    ↑(match 1 with
      | 0 => ⟨j + ↑i✝, ⋯⟩
      | 1 => ⟨j + ↑i✝ + 1, ⋯⟩)

Tactic:
rfl

Result:
no goals

Proof state:
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin (⦋1⦌.len + 1)
⊢ ↑((Hom.toOrderHom
          (mkHom
              {
                toFun := fun x =>
                  match x with
                  | 0 => i✝.castSucc
                  | 1 => i✝.succ,
                monotone' := ⋯ } ≫
            mkHom { toFun := fun i => ⟨↑i + j, ⋯⟩, monotone' := ⋯ }))
        1) =
    ↑((Hom.toOrderHom
          (mkHom
            {
              toFun := fun x =>
                match x with
                | 0 => ⟨j + ↑i✝, ⋯⟩.castSucc
                | 1 => ⟨j + ↑i✝, ⋯⟩.succ,
              monotone' := ⋯ }))
        1)

Tactic:
simp only [len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk,
  OrderHom.mk_comp_mk, Fin.isValue, OrderHom.coe_mk, Function.comp_apply, Fin.castSucc_mk,
  Fin.succ_mk]

Result:
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin (⦋1⦌.len + 1)
⊢ ↑(match 1 with
        | 0 => i✝.castSucc
        | 1 => i✝.succ) +
      j =
    ↑(match 1 with
      | 0 => ⟨j + ↑i✝, ⋯⟩
      | 1 => ⟨j + ↑i✝ + 1, ⋯⟩)

Proof state:
case a.h.h.h
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin (⦋1⦌.len + 1)
⊢ ↑((Hom.toOrderHom
          (mkHom
              {
                toFun := fun x =>
                  match x with
                  | 0 => i✝.castSucc
                  | 1 => i✝.succ,
                monotone' := ⋯ } ≫
            mkHom { toFun := fun i => ⟨↑i + j, ⋯⟩, monotone' := ⋯ }))
        i) =
    ↑((Hom.toOrderHom
          (mkHom
            {
              toFun := fun x =>
                match x with
                | 0 => ⟨j + ↑i✝, ⋯⟩.castSucc
                | 1 => ⟨j + ↑i✝, ⋯⟩.succ,
              monotone' := ⋯ }))
        i)

Tactic:
match i with
| 0 =>
  simp only [len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk,
    OrderHom.mk_comp_mk, Fin.isValue, OrderHom.coe_mk, Function.comp_apply, Fin.castSucc_mk,
    Fin.succ_mk]
  rw [add_comm]
  rfl
| 1 =>
  simp only [len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk,
    OrderHom.mk_comp_mk, Fin.isValue, OrderHom.coe_mk, Function.comp_apply, Fin.castSucc_mk,
    Fin.succ_mk]
  rw [← Nat.add_comm j _]
  rfl

Result:
no goals