awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty (goal)
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 : a ≤ d
b : ℕ
hb : b + 1 ≤ 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 + 1 } hb)
h : a + (b + 1) = c + 1
h₁ :
  ¬Function.Surjective (α :=
      Fin
        ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
                { len := a : SimplexCategory } ha)).len +
          1))
      (β :=
      Fin
        ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
                { len := b + 1 : SimplexCategory } hb)).len +
          1))
      (⇑(Hom.toOrderHom f.hom) :
        (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
          Fin ({ obj := { len := b + 1 }, property := hb }.obj.len + 1))
i : Fin (b + 2)
g' :
  ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a : SimplexCategory }
        ha) ⟶
    { len := b }
hf' : f = Hom.tr g' ha ⋯ ≫ Hom.tr (SimplexCategory.δ i) ⋯ hb
⊢ W f
have neg : W (Hom.tr g' ha sorry ≫ Hom.tr (SimplexCategory.δ i) sorry hb)
Tactic: rw [hf']
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty (goal)
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 : 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 + 1
h₁ :
  Function.Surjective (α :=
    Fin
      ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
              { len := a : SimplexCategory } ha)).len +
        1))
    (β :=
    Fin
      ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
              { len := b : SimplexCategory } hb)).len +
        1))
    (⇑(Hom.toOrderHom f.hom) :
      (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
        Fin ({ obj := { len := b }, property := hb }.obj.len + 1))
⊢ W f
have pos : ∀
  (h₂ :
    Function.Injective (α :=
      Fin
        ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
                { len := a : SimplexCategory } ha)).len +
          1))
      (β :=
      Fin
        ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
                { len := b : SimplexCategory } hb)).len +
          1))
      (⇑(Hom.toOrderHom f.hom) :
        (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
          Fin ({ obj := { len := b }, property := hb }.obj.len + 1))),
  W f
Tactic: by_cases h₂ : Function.Injective f.hom.toOrderHom
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty (hypothesis)
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 : 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 + 1
h₁ :
  Function.Surjective (α :=
    Fin
      ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
              { len := a : SimplexCategory } ha)).len +
        1))
    (β :=
    Fin
      ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
              { len := b : SimplexCategory } hb)).len +
        1))
    (⇑(Hom.toOrderHom f.hom) :
      (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
        Fin ({ obj := { len := b }, property := hb }.obj.len + 1))
h₂ :
  Function.Injective (α :=
    Fin
      ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
              { len := a : SimplexCategory } ha)).len +
        1))
    (β :=
    Fin
      ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
              { len := b : SimplexCategory } hb)).len +
        1))
    (⇑(Hom.toOrderHom f.hom) :
      (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
        Fin ({ obj := { len := b }, property := hb }.obj.len + 1))
⊢ W f
have h₃ : Epi f.hom
Tactic: rw [← epi_iff_surjective] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty (hypothesis)
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 : 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 + 1
h₁ : Epi f.hom
h₂ :
  Function.Injective (α :=
    Fin
      ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
              { len := a : SimplexCategory } ha)).len +
        1))
    (β :=
    Fin
      ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
              { len := b : SimplexCategory } hb)).len +
        1))
    (⇑(Hom.toOrderHom f.hom) :
      (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
        Fin ({ obj := { len := b }, property := hb }.obj.len + 1))
⊢ W f
have h₃ : Mono f.hom
Tactic: rw [← mono_iff_injective] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty (goal)
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 : 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 + 1
h₁ : Epi f.hom
h₂ : Mono f.hom
⊢ W f
have pos : ∀ (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), W f
Tactic: obtain rfl : a = b := le_antisymm (len_le_of_mono f.hom) (len_le_of_epi f.hom)
Cleared hypotheses: b, hb, f, h, h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty (goal)
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
⊢ W f
have 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))
Tactic: obtain rfl : f = 𝟙 _ := ObjectProperty.hom_ext _ (SimplexCategory.eq_id_of_epi _)
Cleared hypotheses: f, h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty (goal)
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 ⋯ ⋯)
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)
c : ℕ
h : a + b = c
⊢ W f
have h₁ : ∀ (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 = 0), W f
Tactic: induction c generalizing a b with
  | zero =>
    obtain rfl : a = 0 := by lia
    obtain rfl : b = 0 := by lia
    obtain rfl : f = 𝟙 _ := by
      ext i : 3
      apply Subsingleton.elim (α := Fin 1)
    apply MorphismProperty.id_mem
  | succ c hc =>
    by_cases h₁ : Function.Surjective f.hom.toOrderHom; swap
    · obtain _ | b := b
      · exact (h₁ (fun _ ↦ ⟨0, Subsingleton.elim (α := Fin 1) _ _⟩)).elim
      · obtain ⟨i, g', hf'⟩ := eq_comp_δ_of_not_surjective _ h₁
        replace hf' : f = Hom.tr g' ≫ Hom.tr (SimplexCategory.δ i) :=
          InducedCategory.hom_ext hf'
        rw [hf']
        exact W.comp_mem _ _ (hc _ _ _ _ _ (by lia))
          (δ_mem _ (by lia) _)
    by_cases h₂ : Function.Injective f.hom.toOrderHom; swap
    · obtain _ | a := a
      · exact (h₂ (Function.injective_of_subsingleton (α := Fin 1) _)).elim
      · obtain ⟨i, g', hf'⟩ := eq_σ_comp_of_not_injective _ h₂
        replace hf' : f = Hom.tr (SimplexCategory.σ i) ≫ Hom.tr g' :=
          InducedCategory.hom_ext hf'
        rw [hf']
        exact W.comp_mem _ _ (σ_mem _ (by lia) _) (hc _ _ _ _ _ (by lia))
    rw [← epi_iff_surjective] at h₁
    rw [← mono_iff_injective] at h₂
    obtain rfl : a = b := le_antisymm (len_le_of_mono f.hom) (len_le_of_epi f.hom)
    obtain rfl : f = 𝟙 _ := ObjectProperty.hom_ext _ (SimplexCategory.eq_id_of_epi _)
    apply W.id_mem
Cleared hypotheses: a, ha, b, hb, f, c, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty (hypothesis)
Goal:
W : MorphismProperty SimplexCategory
inst : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
⊢ W = ⊤
have hW : ∀ (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)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty (goal)
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) = ⊤
⊢ W = ⊤
have h : ∀ ⦃a b : SimplexCategory⦄ (f : a ⟶ b), W f ↔ ⊤ f
Tactic: ext a b f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty (goal)
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 f ↔ ⊤ f
have h : W f
Tactic: simp only [MorphismProperty.top_apply, iff_true]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty (goal)
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 f
have 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 sorry)
  (Truncated.Hom.tr f sorry sorry)
Tactic: change W.inverseImage (Truncated.inclusion (max a.len b.len))
    (Truncated.Hom.tr f (ha := by simp) (hb := by simp))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Rev (goal)
Goal:
n m : SimplexCategory
f : n ⟶ m
i j : Fin (n.len + 1)
hij : i ≤ j
⊢ 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)
have 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)
Tactic: rw [Fin.rev_le_rev]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Rev (goal)
Goal:
n : ℕ
i : Fin (n + 2)
⊢ rev.map (δ i) = δ i.rev
have 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))
Tactic: ext j : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Rev (goal)
Goal:
n : ℕ
i : Fin (n + 2)
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))
have 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)
Tactic: rw [rev_map_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Rev (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin ((rev.obj { len := n : SimplexCategory }).len + 1)
⊢ 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)
have a : (i.succAbove j.rev).rev = i.rev.succAbove j
Tactic: dsimp [δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Rev (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin ((rev.obj { len := n : SimplexCategory }).len + 1)
⊢ (i.succAbove j.rev).rev = i.rev.succAbove j
have a : (i.rev.succAbove j).rev.rev = i.rev.succAbove j
Tactic: rw [Fin.succAbove_rev_right, Fin.rev_rev]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Rev (goal)
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
⊢ (i.succAbove j.rev).rev = i.rev.succAbove j
have a₁ : i.rev.succAbove j = i.rev.succAbove j
Tactic: rw [Fin.succAbove_rev_right, Fin.rev_rev]