-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
@[simp]
lemma diag_subinterval_eq {n} (j l : ℕ) (hjl : j + l ≤ n) :
    diag l ≫ subinterval j l hjl = intervalEdge j l hjl

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

Tactic:
rw [Nat.add_comm]

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

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

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

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

Proof state:
n j l : ℕ
hjl : j + l ≤ n
⊢ diag l ≫ subinterval j l hjl = intervalEdge j l hjl

Tactic:
unfold subinterval intervalEdge diag mkOfLe

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

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

Tactic:
rfl

Result:
no goals

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

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

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

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

Tactic:
ext i

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

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

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

Result:
no goals

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

Tactic:
rw [Nat.add_comm]

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

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

Tactic:
rfl

Result:
no goals