awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
⊢ δ
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i)
          (⟨0, ⋯⟩ : Fin ({ len := 1 : SimplexCategory }.len + 1))) ≫
      σ ((fun (i : Fin ({ len := 0 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) =
    𝟙 (mk 0)

Tactic:
exact δ_comp_σ_self

Premises used: SimplexCategoryGenRel.δ_comp_σ_self
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
⊢ δ
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i)
          (⟨1, ⋯⟩ : Fin ({ len := 1 : SimplexCategory }.len + 1))) ≫
      σ ((fun (i : Fin ({ len := 0 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) =
    𝟙 (mk 0)

Tactic:
δ_comp_σ_succ

Premises used: Fin.succ, SimplexCategoryGenRel.δ_comp_σ_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
⊢ δ
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i)
          (⟨1, ⋯⟩ : Fin ({ len := 1 : SimplexCategory }.len + 1))) ≫
      σ ((fun (i : Fin ({ len := 0 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) =
    𝟙 (mk 0)

Tactic:
exact δ_comp_σ_succ

Premises used: SimplexCategoryGenRel.δ_comp_σ_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
i' : Fin (HAdd.hAdd (α := ℕ) 0 2)
⊢ δ i' ≫ σ i = 𝟙 (mk 0) ≫ 𝟙 (mk 0)

Tactic:
simp [switch_δ_σ₀]

Premises used: _private.0.SimplexCategoryGenRel.switch_δ_σ₀
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
i' : Fin (HAdd.hAdd (α := ℕ) 0 2)
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk 0 ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
exact ⟨_, _, _, P_σ.id_mem _, P_δ.id_mem _, by simp [switch_δ_σ₀]⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
succ :
  ∀ (h : δ i' ≫ σ i = 𝟙 (mk (n + 1))),
    ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m
succ₁ :
  ∀ (j : Fin (n + 1)) (j' : Fin (n + 2)) (h : δ i' ≫ σ i = σ j ≫ δ j'),
    ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
obtain h | ⟨j, j', h⟩ := switch_δ_σ i i'

Premises used: _private.0.SimplexCategoryGenRel.switch_δ_σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
h : δ i' ≫ σ i = 𝟙 (mk (n + 1))
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ≫ 𝟙 (mk (n + 1))

Tactic:
simp [h]
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
h : δ i' ≫ σ i = 𝟙 (mk (n + 1))
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
exact ⟨_, _, _, P_σ.id_mem _, P_δ.id_mem _, by simp [h]⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
j : Fin (n + 1)
j' : Fin (n + 2)
h : δ i' ≫ σ i = σ j ≫ δ j'
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
⟨_, _, _, P_σ.σ _, P_δ.δ _, h⟩

Premises used: SimplexCategoryGenRel.P_σ.σ, SimplexCategoryGenRel.P_δ.δ, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
j : Fin (n + 1)
j' : Fin (n + 2)
h : δ i' ≫ σ i = σ j ≫ δ j'
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
exact ⟨_, _, _, P_σ.σ _, P_δ.δ _, h⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 1)
i' : Fin (n + 2)
zero :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (i' : Fin (HAdd.hAdd (α := ℕ) 0 2)),
    ∃ (z : SimplexCategoryGenRel) (e : mk 0 ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m
succ :
  ∀ (n : ℕ) (i : Fin (n + 1 + 1)) (i' : Fin (n + 1 + 2)),
    ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
cases n with
  | zero => exact ⟨_, _, _, P_σ.id_mem _, P_δ.id_mem _, by simp [switch_δ_σ₀]⟩
  | succ n =>
    obtain h | ⟨j, j', h⟩ := switch_δ_σ i i'
    · exact ⟨_, _, _, P_σ.id_mem _, P_δ.id_mem _, by simp [h]⟩
    · exact ⟨_, _, _, P_σ.σ _, P_δ.δ _, h⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
x : SimplexCategoryGenRel
f : x ⟶ mk (HAdd.hAdd (α := ℕ) 0 1)
h : faces f
zero :
  ∀ (i_1 : Fin (HAdd.hAdd (α := ℕ) 0 2)),
    ∃ (z : SimplexCategoryGenRel) (e : mk 0 ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), δ i_1 ≫ σ i = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m

Tactic:
cases h
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
i_1 : Fin (HAdd.hAdd (α := ℕ) 0 2)
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk 0 ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), δ i_1 ≫ σ i = e ≫ m

Tactic:
factor_δ_σ _ _

Premises used: _private.0.SimplexCategoryGenRel.factor_δ_σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
i_1 : Fin (HAdd.hAdd (α := ℕ) 0 2)
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk 0 ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), δ i_1 ≫ σ i = e ≫ m

Tactic:
exact factor_δ_σ _ _

Premises used: _private.0.SimplexCategoryGenRel.factor_δ_σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ 𝟙 (mk (HAdd.hAdd (α := ℕ) 0 1)) ≫ σ i = σ i ≫ 𝟙 (mk 0)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk (HAdd.hAdd (α := ℕ) 0 1) ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m),
    𝟙 (mk (HAdd.hAdd (α := ℕ) 0 1)) ≫ σ i = e ≫ m

Tactic:
exact ⟨_, _, _, P_σ.σ i, P_δ.id_mem _, by simp⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
x y : SimplexCategoryGenRel
j : x ⟶ y
hf : faces.multiplicativeClosure j
f : y ⟶ mk (HAdd.hAdd (α := ℕ) 0 1)
hg : faces f
zero :
  ∀ ⦃X Y : SimplexCategoryGenRel⦄ (k : Fin (HAdd.hAdd (α := ℕ) 0 2)) (j : x ⟶ mk 0)
    (hf : faces.multiplicativeClosure j),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), (j ≫ δ k) ≫ σ i = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), (j ≫ f) ≫ σ i = e ≫ m

Tactic:
obtain ⟨k⟩ := hg
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
x X Y : SimplexCategoryGenRel
k : Fin (HAdd.hAdd (α := ℕ) 0 2)
j : x ⟶ mk 0
hf : faces.multiplicativeClosure j
zero :
  ∀ (hf : faces.multiplicativeClosure (eqToHom ⋯)),
    ∃ (z : SimplexCategoryGenRel) (e : mk 0 ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), (eqToHom ⋯ ≫ δ k) ≫ σ i = e ≫ m
zero₁ :
  ∀ (hf' : x.len < (mk 0).len),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), (j ≫ δ k) ≫ σ i = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), (j ≫ δ k) ≫ σ i = e ≫ m

Tactic:
obtain ⟨rfl, rfl⟩ | hf' := eq_or_len_le_of_P_δ hf

Premises used: SimplexCategoryGenRel.eq_or_len_le_of_P_δ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
X Y : SimplexCategoryGenRel
k : Fin (HAdd.hAdd (α := ℕ) 0 2)
hf : faces.multiplicativeClosure (eqToHom ⋯)
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk 0 ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), (eqToHom ⋯ ≫ δ k) ≫ σ i = e ≫ m

Tactic:
simpa using factor_δ_σ i k

Premises used: _private.0.SimplexCategoryGenRel.factor_δ_σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
x X Y : SimplexCategoryGenRel
k : Fin (HAdd.hAdd (α := ℕ) 0 2)
j : x ⟶ mk 0
hf : faces.multiplicativeClosure j
hf' : x.len < (mk 0).len
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), (j ≫ δ k) ≫ σ i = e ≫ m

Tactic:
simp at hf'
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
x : SimplexCategoryGenRel
f : x ⟶ mk (HAdd.hAdd (α := ℕ) 0 1)
hf : P_δ f
zero :
  ∀ (h : faces f), ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
zero₁ :
  ∃ (z : SimplexCategoryGenRel) (e : mk (HAdd.hAdd (α := ℕ) 0 1) ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m),
    𝟙 (mk (HAdd.hAdd (α := ℕ) 0 1)) ≫ σ i = e ≫ m
zero₂ :
  ∀ {y : SimplexCategoryGenRel} (j : x ⟶ y) (hf : faces.multiplicativeClosure j) (f : y ⟶ mk (HAdd.hAdd (α := ℕ) 0 1))
    (hg : faces f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), (j ≫ f) ≫ σ i = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m

Tactic:
cases hf with
    | of _ h => cases h; exact factor_δ_σ _ _
    | id => exact ⟨_, _, _, P_σ.σ i, P_δ.id_mem _, by simp⟩
    | comp_of j f hf hg =>
      obtain ⟨k⟩ := hg
      obtain ⟨rfl, rfl⟩ | hf' := eq_or_len_le_of_P_δ hf
      · simpa using factor_δ_σ i k
      · simp at hf'

Premises used: _private.0.SimplexCategoryGenRel.factor_δ_σ, id, SimplexCategoryGenRel.eq_or_len_le_of_P_δ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x : SimplexCategoryGenRel
f : x ⟶ mk (n + 1 + 1)
h : faces f
succ :
  ∀ (i_1 : Fin (n + 1 + 2)),
    ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), δ i_1 ≫ σ i = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m

Tactic:
cases h
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
i_1 : Fin (n + 1 + 2)
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), δ i_1 ≫ σ i = e ≫ m

Tactic:
factor_δ_σ _ _

Premises used: _private.0.SimplexCategoryGenRel.factor_δ_σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
i_1 : Fin (n + 1 + 2)
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), δ i_1 ≫ σ i = e ≫ m

Tactic:
exact factor_δ_σ _ _

Premises used: _private.0.SimplexCategoryGenRel.factor_δ_σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
⊢ 𝟙 (mk (n + 1 + 1)) ≫ σ i = σ i ≫ 𝟙 (mk (n + 1))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1 + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m),
    𝟙 (mk (n + 1 + 1)) ≫ σ i = e ≫ m

Tactic:
exact ⟨_, _, _, P_σ.σ i, P_δ.id_mem _, by simp⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x y : SimplexCategoryGenRel
f : x ⟶ y
hf : faces.multiplicativeClosure f
g : y ⟶ mk (n + 1 + 1)
hg : faces g
succ :
  ∀ ⦃X Y : SimplexCategoryGenRel⦄ (k : Fin (n + 1 + 2)) (f : x ⟶ mk (n + 1)) (hf : faces.multiplicativeClosure f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ g) ≫ σ i = e ≫ m

Tactic:
obtain ⟨k⟩ := hg
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
succ :
  ∀ (hf : faces.multiplicativeClosure (eqToHom ⋯)),
    ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m),
      (eqToHom ⋯ ≫ δ k) ≫ σ i = e ≫ m
succ₁ :
  ∀ (h' : x.len < (mk (n + 1)).len),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
obtain ⟨rfl, rfl⟩ | h' := eq_or_len_le_of_P_δ hf

Premises used: SimplexCategoryGenRel.eq_or_len_le_of_P_δ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
hf : faces.multiplicativeClosure (eqToHom ⋯)
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m),
    (eqToHom ⋯ ≫ δ k) ≫ σ i = e ≫ m

Tactic:
simpa using factor_δ_σ i k

Premises used: _private.0.SimplexCategoryGenRel.factor_δ_σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
succ :
  ∀ (h'' : δ k ≫ σ i = 𝟙 (mk (n + 1))),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m
succ₁ :
  ∀ (j : Fin (n + 1)) (j' : Fin (n + 2)) (h'' : δ k ≫ σ i = σ j ≫ δ j'),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
obtain h'' | ⟨j, j', h''⟩ := switch_δ_σ i k

Premises used: _private.0.SimplexCategoryGenRel.switch_δ_σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
h'' : δ k ≫ σ i = 𝟙 (mk (n + 1))
⊢ (f ≫ δ k) ≫ σ i = 𝟙 x ≫ f

Tactic:
simp [h'']
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
h'' : δ k ≫ σ i = 𝟙 (mk (n + 1))
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
exact ⟨_, _, _, P_σ.id_mem _, hf, by simp [h'']⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
j : Fin (n + 1)
j' : Fin (n + 2)
h'' : δ k ≫ σ i = σ j ≫ δ j'
succ :
  ∀ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (he : P_σ e) (hm : P_δ m) (fac : f ≫ σ j = e ≫ m),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
obtain ⟨z, e, m, he, hm, fac⟩ := hn j f hf
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
j : Fin (n + 1)
j' : Fin (n + 2)
h'' : δ k ≫ σ i = σ j ≫ δ j'
z : SimplexCategoryGenRel
e : x ⟶ z
m : z ⟶ mk n
he : P_σ e
hm : P_δ m
fac : f ≫ σ j = e ≫ m
⊢ (f ≫ δ k) ≫ σ i = e ≫ m ≫ δ j'

Tactic:
simp [h'', reassoc_of% fac]
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
j : Fin (n + 1)
j' : Fin (n + 2)
h'' : δ k ≫ σ i = σ j ≫ δ j'
z : SimplexCategoryGenRel
e : x ⟶ z
m : z ⟶ mk n
he : P_σ e
hm : P_δ m
fac : f ≫ σ j = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
exact ⟨z, e, m ≫ δ j', he, P_δ.comp_mem _ _ hm (P_δ.δ j'),
            by simp [h'', reassoc_of% fac]⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x : SimplexCategoryGenRel
f : x ⟶ mk (n + 1 + 1)
hf : P_δ f
succ :
  ∀ (h : faces f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
succ₁ :
  ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1 + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m),
    𝟙 (mk (n + 1 + 1)) ≫ σ i = e ≫ m
succ₂ :
  ∀ {y : SimplexCategoryGenRel} (f : x ⟶ y) (hf : faces.multiplicativeClosure f) (g : y ⟶ mk (n + 1 + 1))
    (hg : faces g),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ g) ≫ σ i = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m

Tactic:
cases hf with
    | of _ h => cases h; exact factor_δ_σ _ _
    | id n => exact ⟨_, _, _, P_σ.σ i, P_δ.id_mem _, by simp⟩
    | comp_of f g hf hg =>
      obtain ⟨k⟩ := hg
      obtain ⟨rfl, rfl⟩ | h' := eq_or_len_le_of_P_δ hf
      · simpa using factor_δ_σ i k
      · obtain h'' | ⟨j, j', h''⟩ := switch_δ_σ i k
        · exact ⟨_, _, _, P_σ.id_mem _, hf, by simp [h'']⟩
        · obtain ⟨z, e, m, he, hm, fac⟩ := hn j f hf
          exact ⟨z, e, m ≫ δ j', he, P_δ.comp_mem _ _ hm (P_δ.δ j'),
            by simp [h'', reassoc_of% fac]⟩

Premises used: _private.0.SimplexCategoryGenRel.factor_δ_σ, id, SimplexCategoryGenRel.eq_or_len_le_of_P_δ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 1)
x : SimplexCategoryGenRel
f : x ⟶ mk (n + 1)
hf : P_δ f
zero :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (HAdd.hAdd (α := ℕ) 0 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
succ :
  ∀ (n : ℕ)
    (hn :
      ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)) (hf : P_δ f),
        ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m)
    (i : Fin (n + 1 + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1 + 1)) (hf : P_δ f),
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m

Tactic:
induction n generalizing x with
  | zero => cases hf with
    | of _ h => cases h; exact factor_δ_σ _ _
    | id => exact ⟨_, _, _, P_σ.σ i, P_δ.id_mem _, by simp⟩
    | comp_of j f hf hg =>
      obtain ⟨k⟩ := hg
      obtain ⟨rfl, rfl⟩ | hf' := eq_or_len_le_of_P_δ hf
      · simpa using factor_δ_σ i k
      · simp at hf'
  | succ n hn =>
    cases hf with
    | of _ h => cases h; exact factor_δ_σ _ _
    | id n => exact ⟨_, _, _, P_σ.σ i, P_δ.id_mem _, by simp⟩
    | comp_of f g hf hg =>
      obtain ⟨k⟩ := hg
      obtain ⟨rfl, rfl⟩ | h' := eq_or_len_le_of_P_δ hf
      · simpa using factor_δ_σ i k
      · obtain h'' | ⟨j, j', h''⟩ := switch_δ_σ i k
        · exact ⟨_, _, _, P_σ.id_mem _, hf, by simp [h'']⟩
        · obtain ⟨z, e, m, he, hm, fac⟩ := hn j f hf
          exact ⟨z, e, m ≫ δ j', he, P_δ.comp_mem _ _ hm (P_δ.δ j'),
            by simp [h'', reassoc_of% fac]⟩

Premises used: _private.0.SimplexCategoryGenRel.factor_δ_σ, id, SimplexCategoryGenRel.eq_or_len_le_of_P_δ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n : ℕ
h : 𝟙 (mk n) = 𝟙 (mk n) ≫ 𝟙 (mk n)
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), 𝟙 (mk n) = e ≫ m

Tactic:
use (mk n), (𝟙 (mk n)), (𝟙 (mk n)), P_σ.id_mem _, P_δ.id_mem _

Premises used: SimplexCategoryGenRel.mk, CategoryTheory.CategoryStruct.id, SimplexCategoryGenRel.P_σ, SimplexCategoryGenRel.P_δ, CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n : ℕ
⊢ 𝟙 (mk n) = 𝟙 (mk n) ≫ 𝟙 (mk n)

Tactic:
simp