awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
Goal:
d : ℕ
W : MorphismProperty (Truncated d)
inst : W.IsMultiplicative
δ_mem :
  ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)),
    W (X := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := n } ⋯) (Y :=
      ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := n + 1 } ⋯) (δ d i ⋯ ⋯)
σ_mem :
  ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)),
    W (X := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := n + 1 } ⋯) (Y :=
      ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := n } ⋯) (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f :
      Quiver.Hom (V := Truncated d)
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha)
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := b } hb))
    (h : a + b = c), W f
a : ℕ
ha hb : a ≤ d
f :
  Quiver.Hom (V := Truncated d)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } hb)
h : a + a = c + 1
h₁ : Epi f.hom
h₂ : Mono f.hom
pos :
  ∀
    (h₁ :
      Epi (X :=
        ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha))
        (InducedCategory.Hom.hom
          (𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha))))
    (h₂ :
      Mono (X :=
        ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha))
        (InducedCategory.Hom.hom
          (𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha)))),
    W (X := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha)
      (𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha))
⊢ W f

Tactic:
obtain rfl : f = 𝟙 _ := ObjectProperty.hom_ext _ (SimplexCategory.eq_id_of_epi _)

Premises used: CategoryTheory.CategoryStruct.id, SimplexCategory.eq_id_of_epi, CategoryTheory.ObjectProperty.hom_ext, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
Goal:
d : ℕ
W : MorphismProperty (Truncated d)
inst : W.IsMultiplicative
δ_mem :
  ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)),
    W (X := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := n } ⋯) (Y :=
      ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := n + 1 } ⋯) (δ d i ⋯ ⋯)
σ_mem :
  ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)),
    W (X := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := n + 1 } ⋯) (Y :=
      ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := n } ⋯) (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f :
      Quiver.Hom (V := Truncated d)
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha)
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := b } hb))
    (h : a + b = c), W f
a : ℕ
ha hb : a ≤ d
h : a + a = c + 1
h₁ :
  Epi (X :=
    ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha))
    (InducedCategory.Hom.hom
      (𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha)))
h₂ :
  Mono (X :=
    ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha))
    (InducedCategory.Hom.hom
      (𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha)))
⊢ W (X := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha)
    (𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha))

Tactic:
apply W.id_mem

Premises used: CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
Goal:
W : MorphismProperty SimplexCategory
inst : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
⊢ ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤

Tactic:
have hW (d : ℕ) : W.inverseImage (Truncated.inclusion d) = ⊤ :=
    Truncated.morphismProperty_eq_top _ (fun _ _ i ↦ δ_mem i)
      (fun _ _ i ↦ σ_mem i)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
Goal:
W : MorphismProperty SimplexCategory
inst : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
h : ∀ ⦃a b : SimplexCategory⦄ (f : a ⟶ b), W f ↔ ⊤ f
⊢ W = ⊤

Tactic:
ext a b f
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
Goal:
W : MorphismProperty SimplexCategory
inst : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
h : W f
⊢ W f ↔ ⊤ f

Tactic:
simp only [MorphismProperty.top_apply, iff_true]

Premises used: iff_true, CategoryTheory.MorphismProperty.top_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
Goal:
W : MorphismProperty SimplexCategory
inst : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ a.len ≤ max a.len b.len

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
Goal:
W : MorphismProperty SimplexCategory
inst : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ b.len ≤ max a.len b.len

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
Goal:
W : MorphismProperty SimplexCategory
inst : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
h :
  W.inverseImage (Truncated.inclusion (max a.len b.len)) (X :=
    ObjectProperty.FullSubcategory.mk (P := fun (a_1 : SimplexCategory) ↦ a_1.len ≤ max a.len b.len) a ⋯)
    (Truncated.Hom.tr f ⋯ ⋯)
⊢ W f

Tactic:
change W.inverseImage (Truncated.inclusion (max a.len b.len))
    (Truncated.Hom.tr f (ha := by simp) (hb := by simp))

Premises used: SimplexCategory.Truncated.Hom.tr, CategoryTheory.MorphismProperty.inverseImage, Max.max, SimplexCategory.Truncated.inclusion, SimplexCategory.len
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
Goal:
W : MorphismProperty SimplexCategory
inst : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ W.inverseImage (Truncated.inclusion (max a.len b.len)) (X :=
    ObjectProperty.FullSubcategory.mk (P := fun (a_1 : SimplexCategory) ↦ a_1.len ≤ max a.len b.len) a ⋯)
    (Truncated.Hom.tr f ⋯ ⋯)

Tactic:
simp only [hW, MorphismProperty.top_apply]

Premises used: CategoryTheory.MorphismProperty.top_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev
Goal:
n m : SimplexCategory
f : n ⟶ m
i j : Fin (n.len + 1)
hij : i ≤ j
rw :
  LE.le (α := Fin (m.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m)
        j.rev :
      (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m)
        i.rev :
      (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m)
⊢ LE.le (α := Fin (m.len + 1))
    ((fun (i : Fin (n.len + 1)) ↦
        (Fin.rev
            ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                  fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
                (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m)
              i.rev) :
          Fin (m.len + 1)))
      i)
    ((fun (i : Fin (n.len + 1)) ↦
        (Fin.rev
            ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                  fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
                (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m)
              i.rev) :
          Fin (m.len + 1)))
      j)

Tactic:
rw [Fin.rev_le_rev]

Premises used: Fin.rev_le_rev
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev
Goal:
n m : SimplexCategory
f : n ⟶ m
i j : Fin (n.len + 1)
hij : i ≤ j
rwa rwa₁ rwa₂ rwa₃ : i ≤ j
⊢ j.rev ≤ i.rev

Tactic:
rwa [Fin.rev_le_rev]

Premises used: Fin.rev_le_rev
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev
Goal:
n m : SimplexCategory
f : n ⟶ m
i j : Fin (n.len + 1)
hij : i ≤ j
⊢ LE.le (α := Fin (m.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m)
        j.rev :
      (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m)
        i.rev :
      (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m)

Tactic:
exact f.toOrderHom.monotone (by rwa [Fin.rev_le_rev])

Premises used: OrderHom.monotone, SimplexCategory.Hom.toOrderHom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev
Goal:
n m : SimplexCategory
f : n ⟶ m
i : Fin (n.len + 1)
⊢ Eq (α := Fin (m.len + 1)) ((Hom.toOrderHom (rev.map f) : (a : Fin (n.len + 1)) → Fin (m.len + 1)) i : Fin (m.len + 1))
    (Fin.rev ((Hom.toOrderHom f : (a : Fin (n.len + 1)) → Fin (m.len + 1)) i.rev) : Fin (m.len + 1))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev
Goal:
n : ℕ
i : Fin (n + 2)
a :
  ∀ (j : Fin ((rev.obj { len := n : SimplexCategory }).len + 1)),
    Eq (α := Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1))
      ((Hom.toOrderHom (rev.map (δ i)) :
            (a : Fin ((rev.obj { len := n }).len + 1)) → Fin ((rev.obj { len := n + 1 }).len + 1))
          j :
        Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1))
      ((Hom.toOrderHom (δ i.rev) :
            (a : Fin ((rev.obj { len := n }).len + 1)) → Fin ((rev.obj { len := n + 1 }).len + 1))
          j :
        Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1))
⊢ rev.map (δ i) = δ i.rev

Tactic:
ext j : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin ((rev.obj { len := n : SimplexCategory }).len + 1)
a :
  Eq (α := Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1))
    (Fin.rev
      ((Hom.toOrderHom (δ i) : (a : Fin ((rev.obj { len := n }).len + 1)) → Fin ((rev.obj { len := n + 1 }).len + 1))
        j.rev))
    ((Hom.toOrderHom (δ i.rev) : (a : Fin ((rev.obj { len := n }).len + 1)) → Fin ((rev.obj { len := n + 1 }).len + 1))
      j)
⊢ Eq (α := Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1))
    ((Hom.toOrderHom (rev.map (δ i)) :
          (a : Fin ((rev.obj { len := n }).len + 1)) → Fin ((rev.obj { len := n + 1 }).len + 1))
        j :
      Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1))
    ((Hom.toOrderHom (δ i.rev) : (a : Fin ((rev.obj { len := n }).len + 1)) → Fin ((rev.obj { len := n + 1 }).len + 1))
        j :
      Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1))

Tactic:
rw [rev_map_apply]

Premises used: SimplexCategory.rev_map_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin ((rev.obj { len := n : SimplexCategory }).len + 1)
a : (i.succAbove j.rev).rev = i.rev.succAbove j
⊢ Eq (α := Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1))
    (Fin.rev
      ((Hom.toOrderHom (δ i) : (a : Fin ((rev.obj { len := n }).len + 1)) → Fin ((rev.obj { len := n + 1 }).len + 1))
        j.rev))
    ((Hom.toOrderHom (δ i.rev) : (a : Fin ((rev.obj { len := n }).len + 1)) → Fin ((rev.obj { len := n + 1 }).len + 1))
      j)

Tactic:
dsimp [δ]

Premises used: SimplexCategory.δ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin ((rev.obj { len := n : SimplexCategory }).len + 1)
a : (i.rev.succAbove j).rev.rev = i.rev.succAbove j
a₁ a₂ : i.rev.succAbove j = i.rev.succAbove j
⊢ (i.succAbove j.rev).rev = i.rev.succAbove j

Tactic:
rw [Fin.succAbove_rev_right, Fin.rev_rev]

Premises used: Fin.succAbove_rev_right, Fin.rev_rev
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev
Goal:
n : ℕ
i : Fin (n + 1)
a :
  ∀ (j : Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1)),
    Eq (α := Fin ((rev.obj { len := n : SimplexCategory }).len + 1))
      ((Hom.toOrderHom (rev.map (σ i)) :
            (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1))
          j :
        Fin ((rev.obj { len := n : SimplexCategory }).len + 1))
      ((Hom.toOrderHom (σ i.rev) :
            (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1))
          j :
        Fin ((rev.obj { len := n : SimplexCategory }).len + 1))
⊢ rev.map (σ i) = σ i.rev

Tactic:
ext j : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1)
a :
  Eq (α := Fin ((rev.obj { len := n : SimplexCategory }).len + 1))
    (Fin.rev
      ((Hom.toOrderHom (σ i) : (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1))
        j.rev))
    ((Hom.toOrderHom (σ i.rev) : (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1))
      j)
⊢ Eq (α := Fin ((rev.obj { len := n : SimplexCategory }).len + 1))
    ((Hom.toOrderHom (rev.map (σ i)) :
          (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1))
        j :
      Fin ((rev.obj { len := n : SimplexCategory }).len + 1))
    ((Hom.toOrderHom (σ i.rev) : (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1))
        j :
      Fin ((rev.obj { len := n : SimplexCategory }).len + 1))

Tactic:
rw [rev_map_apply]

Premises used: SimplexCategory.rev_map_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1)
a : (i.predAbove j.rev).rev = i.rev.predAbove j
⊢ Eq (α := Fin ((rev.obj { len := n : SimplexCategory }).len + 1))
    (Fin.rev
      ((Hom.toOrderHom (σ i) : (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1))
        j.rev))
    ((Hom.toOrderHom (σ i.rev) : (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1))
      j)

Tactic:
dsimp [σ]

Premises used: SimplexCategory.σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1)
a : (i.rev.predAbove j).rev.rev = i.rev.predAbove j
a₁ a₂ : i.rev.predAbove j = i.rev.predAbove j
⊢ (i.predAbove j.rev).rev = i.rev.predAbove j

Tactic:
rw [Fin.predAbove_rev_right, Fin.rev_rev]

Premises used: Fin.predAbove_rev_right, Fin.rev_rev
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev
Goal:
n m : SimplexCategory
f : n ⟶ m
⊢ rev.map (rev.map f) = f

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev
Goal:
⊢ rev.IsEquivalence

Tactic:
revEquivalence.isEquivalence_functor

Premises used: SimplexCategory.revEquivalence, CategoryTheory.Equivalence.isEquivalence_functor, SimplexCategory.rev
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
Goal:
a : SemiSimplexCategory
⊢ Eq (α := Fin (a.len + 1) ↪o Fin (a.len + 1))
    ((homEquiv : (a_1 : a ⟶ a) → Fin (a.len + 1) ↪o Fin (a.len + 1)) (𝟙 a) : Fin (a.len + 1) ↪o Fin (a.len + 1))
    (RelEmbedding.refl fun (x1 x2 : Fin (a.len + 1)) ↦ x1 ≤ x2 :
      (fun (x1 x2 : Fin (a.len + 1)) ↦ x1 ≤ x2) ↪r fun (x1 x2 : Fin (a.len + 1)) ↦ x1 ≤ x2)

Tactic:
rfl

Premises used: RelEmbedding.refl, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
Goal:
a b c : SemiSimplexCategory
f : a ⟶ b
g : b ⟶ c
⊢ Eq (α := Fin (a.len + 1) ↪o Fin (c.len + 1))
    ((homEquiv : (a_1 : a ⟶ c) → Fin (a.len + 1) ↪o Fin (c.len + 1)) (f ≫ g) : Fin (a.len + 1) ↪o Fin (c.len + 1))
    (RelEmbedding.trans (r := fun (x1 x2 : Fin (a.len + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (b.len + 1)) ↦ x1 ≤ x2)
        (t := fun (x1 x2 : Fin (c.len + 1)) ↦ x1 ≤ x2)
        ((homEquiv : (a_1 : a ⟶ b) → Fin (a.len + 1) ↪o Fin (b.len + 1)) f)
        ((homEquiv : (a : b ⟶ c) → Fin (b.len + 1) ↪o Fin (c.len + 1)) g) :
      (fun (x1 x2 : Fin (a.len + 1)) ↦ x1 ≤ x2) ↪r fun (x1 x2 : Fin (c.len + 1)) ↦ x1 ≤ x2)

Tactic:
rfl

Premises used: RelEmbedding.trans, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
Goal:
a b : SemiSimplexCategory
f g : a ⟶ b
h :
  Eq (α := Fin (a.len + 1) ↪o Fin (b.len + 1))
    ((homEquiv : (a_1 : a ⟶ b) → Fin (a.len + 1) ↪o Fin (b.len + 1)) f : Fin (a.len + 1) ↪o Fin (b.len + 1))
    ((homEquiv : (a_1 : a ⟶ b) → Fin (a.len + 1) ↪o Fin (b.len + 1)) g : Fin (a.len + 1) ↪o Fin (b.len + 1))
⊢ f = g

Tactic:
homEquiv.injective h

Premises used: SemiSimplexCategory.homEquiv, Equiv.injective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
Goal:
n : ℕ
⊢ toSimplexCategory.obj ⦋n⦌ₛ = ⦋n⦌

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
Goal:
X Y : SemiSimplexCategory
a₁ a₂ : X ⟶ Y
h : toSimplexCategory.map a₁ = toSimplexCategory.map a₂
h₁ :
  ∀ (x : Fin (X.len + 1)),
    Eq (α := Fin (Y.len + 1))
      ((((homEquiv : (a : X ⟶ Y) → Fin (X.len + 1) ↪o Fin (Y.len + 1)) a₁ : Fin (X.len + 1) ↪o Fin (Y.len + 1)) :
            (a : Fin (X.len + 1)) → Fin (Y.len + 1))
          x :
        Fin (Y.len + 1))
      ((((homEquiv : (a : X ⟶ Y) → Fin (X.len + 1) ↪o Fin (Y.len + 1)) a₂ : Fin (X.len + 1) ↪o Fin (Y.len + 1)) :
            (a : Fin (X.len + 1)) → Fin (Y.len + 1))
          x :
        Fin (Y.len + 1))
⊢ a₁ = a₂

Tactic:
ext : 2
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
Goal:
X Y : SemiSimplexCategory
a₁ a₂ : X ⟶ Y
h : toSimplexCategory.map a₁ = toSimplexCategory.map a₂
x : Fin (X.len + 1)
⊢ Eq (α := Fin (Y.len + 1))
    ((((homEquiv : (a : X ⟶ Y) → Fin (X.len + 1) ↪o Fin (Y.len + 1)) a₁ : Fin (X.len + 1) ↪o Fin (Y.len + 1)) :
          (a : Fin (X.len + 1)) → Fin (Y.len + 1))
        x :
      Fin (Y.len + 1))
    ((((homEquiv : (a : X ⟶ Y) → Fin (X.len + 1) ↪o Fin (Y.len + 1)) a₂ : Fin (X.len + 1) ↪o Fin (Y.len + 1)) :
          (a : Fin (X.len + 1)) → Fin (Y.len + 1))
        x :
      Fin (Y.len + 1))

Tactic:
apply ConcreteCategory.congr_hom h

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
Goal:
n m : SemiSimplexCategory
f : n ⟶ m
rw :
  Function.Injective (α := Fin ((toSimplexCategory.obj n).len + 1)) (β := Fin ((toSimplexCategory.obj m).len + 1))
    (⇑(SimplexCategory.Hom.toOrderHom (toSimplexCategory.map f)) :
      (a : Fin ((toSimplexCategory.obj n).len + 1)) → Fin ((toSimplexCategory.obj m).len + 1))
⊢ Mono (toSimplexCategory.map f)

Tactic:
rw [SimplexCategory.mono_iff_injective]

Premises used: SimplexCategory.mono_iff_injective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
Goal:
n m : SemiSimplexCategory
f : n ⟶ m
⊢ Function.Injective (α := Fin ((toSimplexCategory.obj n).len + 1)) (β := Fin ((toSimplexCategory.obj m).len + 1))
    (⇑(SimplexCategory.Hom.toOrderHom (toSimplexCategory.map f)) :
      (a : Fin ((toSimplexCategory.obj n).len + 1)) → Fin ((toSimplexCategory.obj m).len + 1))

Tactic:
(homEquiv f).injective

Premises used: SemiSimplexCategory.homEquiv, RelEmbedding.injective, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
Goal:
n m : SemiSimplexCategory
f : n ⟶ m
⊢ Function.Injective (α := Fin ((toSimplexCategory.obj n).len + 1)) (β := Fin ((toSimplexCategory.obj m).len + 1))
    (⇑(SimplexCategory.Hom.toOrderHom (toSimplexCategory.map f)) :
      (a : Fin ((toSimplexCategory.obj n).len + 1)) → Fin ((toSimplexCategory.obj m).len + 1))

Tactic:
exact (homEquiv f).injective

Premises used: SemiSimplexCategory.homEquiv, RelEmbedding.injective, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
Goal:
n m : SemiSimplexCategory
f : n ⟶ m
Z : SemiSimplexCategory
g₁ g₂ : Z ⟶ n
h : g₁ ≫ f = g₂ ≫ f
a : toSimplexCategory.map g₁ = toSimplexCategory.map g₂
⊢ g₁ = g₂

Tactic:
apply toSimplexCategory.map_injective

Premises used: SemiSimplexCategory.toSimplexCategory, CategoryTheory.Functor.map_injective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
Goal:
n m : SemiSimplexCategory
f : n ⟶ m
Z : SemiSimplexCategory
g₁ g₂ : Z ⟶ n
h : g₁ ≫ f = g₂ ≫ f
⊢ toSimplexCategory.map g₁ = toSimplexCategory.map g₂

Tactic:
simp only [← cancel_mono (toSimplexCategory.map f), ← Functor.map_comp, h]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.map, SemiSimplexCategory.toSimplexCategory, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
Goal:
n m : SemiSimplexCategory
f : toSimplexCategory.obj n ⟶ toSimplexCategory.obj m
inst rwa rwa₁ rwa₂ rwa₃ : Mono f
⊢ Function.Injective (α := Fin ((toSimplexCategory.obj n).len + 1)) (β := Fin ((toSimplexCategory.obj m).len + 1))
    (⇑(SimplexCategory.Hom.toOrderHom f) :
      (a : Fin ((toSimplexCategory.obj n).len + 1)) → Fin ((toSimplexCategory.obj m).len + 1))

Tactic:
rwa [← SimplexCategory.mono_iff_injective]

Premises used: SimplexCategory.mono_iff_injective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
Goal:
n m : SemiSimplexCategory
f : toSimplexCategory.obj n ⟶ toSimplexCategory.obj m
inst : Mono f
⊢ toSimplexCategory.map (homOfMono f) = f

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
dsimp : LE.le (α := Fin 2) (if j₁.castSucc < i then 0 else 1) (if j₂.castSucc < i then 0 else 1)
⊢ LE.le (α := Fin (⦋1⦌.len + 1))
    ((fun (j : Fin (⦋n⦌.len + 1)) ↦ (if j.castSucc < i then 0 else 1 : Fin (⦋1⦌.len + 1))) j₁)
    ((fun (j : Fin (⦋n⦌.len + 1)) ↦ (if j.castSucc < i then 0 else 1 : Fin (⦋1⦌.len + 1))) j₂)

Tactic:
dsimp