awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
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 + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m
have 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
Tactic: obtain ⟨z, e, m, he, hm, fac⟩ := hn j f hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
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
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
have succ : ∀ (h : faces f), ∃ (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]⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
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
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
have 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
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]⟩
Cleared hypotheses: x, f, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
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
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
have 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
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]⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
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
have 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
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]⟩
Cleared hypotheses: n, i, x, f, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
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
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
have 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
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]⟩
Cleared hypotheses: n, i, x, f, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
n : ℕ
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), 𝟙 (mk n) = e ≫ m
have h : 𝟙 (mk n) = 𝟙 (mk n) ≫ 𝟙 (mk n)
Tactic: use (mk n), (𝟙 (mk n)), (𝟙 (mk n)), P_σ.id_mem _, P_δ.id_mem _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
f : mk n ⟶ mk n'
j : Fin (n' + 2)
h : ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e) (_ : P_δ m), f = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk (n' + 1)) (_ : P_σ e) (_ : P_δ m), f ≫ δ j = e ≫ m
have comp_δ : ∀ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n') (he : P_σ e) (hm : P_δ m),
  ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m_1 : z_1 ⟶ mk (n' + 1)) (_ : P_σ e_1) (_ : P_δ m_1),
    (e ≫ m) ≫ δ j = e_1 ≫ m_1
Tactic: obtain ⟨z, e, m, ⟨he, hm, rfl⟩⟩ := h
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
f : mk n ⟶ mk (n' + 1)
j : Fin (n' + 1)
h : ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk (n' + 1)) (_ : P_σ e) (_ : P_δ m), f = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e) (_ : P_δ m), f ≫ σ j = e ≫ m
have comp_σ : ∀ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk (n' + 1)) (he : P_σ e) (hm : P_δ m),
  ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m_1 : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m_1),
    (e ≫ m) ≫ σ j = e_1 ≫ m_1
Tactic: obtain ⟨z, e, m, ⟨he, hm, rfl⟩⟩ := h
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
z : SimplexCategoryGenRel
e : mk n ⟶ z
m : z ⟶ mk (n' + 1)
he : P_σ e
hg : faces m
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m_1 : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m_1),
    (e ≫ m) ≫ σ j = e_1 ≫ m_1
have comp_σ : ∀ ⦃X Y : SimplexCategoryGenRel⦄ (i : Fin (n' + 2)) (e : mk n ⟶ mk n') (he : P_σ e),
  ∃ (z : SimplexCategoryGenRel) (e_1 : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m), (e ≫ δ i) ≫ σ j = e_1 ≫ m
Tactic: rcases hg with ⟨i⟩
Cleared hypotheses: z, e, m, he, hg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
X Y : SimplexCategoryGenRel
i : Fin (n' + 2)
e : mk n ⟶ mk n'
he : P_σ e
⊢ ∃ (z : SimplexCategoryGenRel) (e_1 : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m), (e ≫ δ i) ≫ σ j = e_1 ≫ m
have comp_σ : ∀ (w : SimplexCategoryGenRel) (w_1 : mk n' ⟶ w) (w_2 : w ⟶ mk n') (he₁ : P_σ w_1) (hm₁ : P_δ w_2)
  (h₁ : δ i ≫ σ j = w_1 ≫ w_2),
  ∃ (z : SimplexCategoryGenRel) (e_1 : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m), (e ≫ δ i) ≫ σ j = e_1 ≫ m
Tactic: obtain ⟨_, _, _, ⟨he₁, hm₁, h₁⟩⟩ := factor_δ_σ j i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
n : ℕ
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
y_1 : SimplexCategoryGenRel
f : z ⟶ y_1
hf : faces.multiplicativeClosure f
j : Fin (HAdd.hAdd (α := ℕ) 0 1)
g : y_1 ⟶ mk (HAdd.hAdd (α := ℕ) 0 1)
hg : faces g
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m : z_1 ⟶ mk 0) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m
have comp_σ : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 2)) (f : z ⟶ mk 0) (hf : faces.multiplicativeClosure f),
  ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m : z_1 ⟶ mk 0) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
Tactic: cases hg
Cleared hypotheses: y_1, f, hf, g, hg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
n_1 : ℕ
z : SimplexCategoryGenRel
e : mk n_1 ⟶ z
he : P_σ e
y_1 : SimplexCategoryGenRel
f : z ⟶ y_1
hf : faces.multiplicativeClosure f
n : ℕ
j : Fin (n + 1 + 1)
g : y_1 ⟶ mk (n + 1 + 1)
hg : faces g
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m
have comp_σ : ∀ ⦃X Y : SimplexCategoryGenRel⦄ (i : Fin (n + 1 + 2)) (f : z ⟶ mk (n + 1)) (hf : faces.multiplicativeClosure f),
  ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
Tactic: rcases hg with ⟨i⟩
Cleared hypotheses: y_1, f, hf, g, hg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
n_1 : ℕ
z : SimplexCategoryGenRel
e : mk n_1 ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
have comp_σ : ∀ (h' : δ i ≫ σ j = 𝟙 (mk (n + 1))),
  ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
Tactic: obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
n_1 : ℕ
z : SimplexCategoryGenRel
e : mk n_1 ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
comp_σ :
  ∀ (h' : δ i ≫ σ j = 𝟙 (mk (n + 1))),
    ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
      (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
have comp_σ₁ : ∀ (j' : Fin (n + 1)) (j'' : Fin (n + 2)) (h' : δ i ≫ σ j = σ j' ≫ δ j''),
  ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
Tactic: obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
n_1 : ℕ
z : SimplexCategoryGenRel
e : mk n_1 ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
j' : Fin (n + 1)
j'' : Fin (n + 2)
h' : δ i ≫ σ j = σ j' ≫ δ j''
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
have comp_σ : ∀ (w : SimplexCategoryGenRel) (w_1 : z ⟶ w) (m₁ : w ⟶ mk n) (he₁ : P_σ w_1) (hm₁ : P_δ m₁) (h₁ : f ≫ σ j' = w_1 ≫ m₁),
  ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
Tactic: obtain ⟨_, _, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' f hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
y_1 : SimplexCategoryGenRel
f : z ⟶ y_1
hf : faces.multiplicativeClosure f
g : y_1 ⟶ mk (n' + 1)
hg : faces g
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m
have comp_σ : ∀ (j : Fin (HAdd.hAdd (α := ℕ) 0 1)) (g : y_1 ⟶ mk (HAdd.hAdd (α := ℕ) 0 1)) (hg : faces g),
  ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m : z_1 ⟶ mk 0) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m
Tactic: cases n' with
      | zero =>
        cases hg
        exact ⟨_, _, _, he, hf, by simp [switch_δ_σ₀]⟩
      | succ n =>
        rcases hg with ⟨i⟩
        obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i
        · exact ⟨_, _, _, he, hf, by simp [h']⟩
        · obtain ⟨_, _, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' f hf
          exact ⟨_, _, m₁ ≫ δ j'', P_σ.comp_mem _ _ he he₁, P_δ.comp_mem _ _ hm₁ (P_δ.δ _),
            by simp [← reassoc_of% h₁, h']⟩
Cleared hypotheses: n', j, g, hg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
y_1 : SimplexCategoryGenRel
f : z ⟶ y_1
hf : faces.multiplicativeClosure f
g : y_1 ⟶ mk (n' + 1)
hg : faces g
comp_σ :
  ∀ (j : Fin (HAdd.hAdd (α := ℕ) 0 1)) (g : y_1 ⟶ mk (HAdd.hAdd (α := ℕ) 0 1)) (hg : faces g),
    ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m : z_1 ⟶ mk 0) (_ : P_σ e_1) (_ : P_δ m),
      (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m
have comp_σ₁ : ∀ (n_1 : ℕ) (j : Fin (n_1 + 1 + 1)) (g : y_1 ⟶ mk (n_1 + 1 + 1)) (hg : faces g),
  ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m : z_1 ⟶ mk (n_1 + 1)) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m
Tactic: cases n' with
      | zero =>
        cases hg
        exact ⟨_, _, _, he, hf, by simp [switch_δ_σ₀]⟩
      | succ n =>
        rcases hg with ⟨i⟩
        obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i
        · exact ⟨_, _, _, he, hf, by simp [h']⟩
        · obtain ⟨_, _, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' f hf
          exact ⟨_, _, m₁ ≫ δ j'', P_σ.comp_mem _ _ he he₁, P_δ.comp_mem _ _ hm₁ (P_δ.δ _),
            by simp [← reassoc_of% h₁, h']⟩
Cleared hypotheses: n', j, g, hg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
z : SimplexCategoryGenRel
e : mk n ⟶ z
m : z ⟶ mk (n' + 1)
he : P_σ e
hm : P_δ m
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m_1 : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m_1),
    (e ≫ m) ≫ σ j = e_1 ≫ m_1
have comp_σ : ∀ (hg : faces m),
  ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m_1 : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m_1),
    (e ≫ m) ≫ σ j = e_1 ≫ m_1
Tactic: cases hm with
    | of g hg =>
      rcases hg with ⟨i⟩
      obtain ⟨_, _, _, ⟨he₁, hm₁, h₁⟩⟩ := factor_δ_σ j i
      exact ⟨_, _, _, P_σ.comp_mem _ _ he he₁, hm₁,
        by simp [← h₁]⟩
    | @id n =>
      exact ⟨mk n', e ≫ σ j, 𝟙 _, P_σ.comp_mem _ _ he (P_σ.σ _), P_δ.id_mem _, by simp⟩
    | comp_of f g hf hg =>
      cases n' with
      | zero =>
        cases hg
        exact ⟨_, _, _, he, hf, by simp [switch_δ_σ₀]⟩
      | succ n =>
        rcases hg with ⟨i⟩
        obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i
        · exact ⟨_, _, _, he, hf, by simp [h']⟩
        · obtain ⟨_, _, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' f hf
          exact ⟨_, _, m₁ ≫ δ j'', P_σ.comp_mem _ _ he he₁, P_δ.comp_mem _ _ hm₁ (P_δ.δ _),
            by simp [← reassoc_of% h₁, h']⟩
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
z : SimplexCategoryGenRel
e : mk n ⟶ z
m : z ⟶ mk (n' + 1)
he : P_σ e
hm : P_δ m
comp_σ :
  ∀ (hg : faces m),
    ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m_1 : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m_1),
      (e ≫ m) ≫ σ j = e_1 ≫ m_1
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m_1 : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m_1),
    (e ≫ m) ≫ σ j = e_1 ≫ m_1
have comp_σ₁ : ∀ (e : mk n ⟶ mk (n' + 1)) (he : P_σ e),
  ∃ (z : SimplexCategoryGenRel) (e_1 : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ 𝟙 (mk (n' + 1))) ≫ σ j = e_1 ≫ m
Tactic: cases hm with
    | of g hg =>
      rcases hg with ⟨i⟩
      obtain ⟨_, _, _, ⟨he₁, hm₁, h₁⟩⟩ := factor_δ_σ j i
      exact ⟨_, _, _, P_σ.comp_mem _ _ he he₁, hm₁,
        by simp [← h₁]⟩
    | @id n =>
      exact ⟨mk n', e ≫ σ j, 𝟙 _, P_σ.comp_mem _ _ he (P_σ.σ _), P_δ.id_mem _, by simp⟩
    | comp_of f g hf hg =>
      cases n' with
      | zero =>
        cases hg
        exact ⟨_, _, _, he, hf, by simp [switch_δ_σ₀]⟩
      | succ n =>
        rcases hg with ⟨i⟩
        obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i
        · exact ⟨_, _, _, he, hf, by simp [h']⟩
        · obtain ⟨_, _, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' f hf
          exact ⟨_, _, m₁ ≫ δ j'', P_σ.comp_mem _ _ he he₁, P_δ.comp_mem _ _ hm₁ (P_δ.δ _),
            by simp [← reassoc_of% h₁, h']⟩
Cleared hypotheses: z, e, m, he, hm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
z : SimplexCategoryGenRel
e : mk n ⟶ z
m : z ⟶ mk (n' + 1)
he : P_σ e
hm : P_δ m
comp_σ :
  ∀ (hg : faces m),
    ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m_1 : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m_1),
      (e ≫ m) ≫ σ j = e_1 ≫ m_1
comp_σ₁ :
  ∀ (e : mk n ⟶ mk (n' + 1)) (he : P_σ e),
    ∃ (z : SimplexCategoryGenRel) (e_1 : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m),
      (e ≫ 𝟙 (mk (n' + 1))) ≫ σ j = e_1 ≫ m
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m_1 : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m_1),
    (e ≫ m) ≫ σ j = e_1 ≫ m_1
have comp_σ₂ : ∀ {y : SimplexCategoryGenRel} (f : z ⟶ y) (hf : faces.multiplicativeClosure f) (g : y ⟶ mk (n' + 1)) (hg : faces g),
  ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m
Tactic: cases hm with
    | of g hg =>
      rcases hg with ⟨i⟩
      obtain ⟨_, _, _, ⟨he₁, hm₁, h₁⟩⟩ := factor_δ_σ j i
      exact ⟨_, _, _, P_σ.comp_mem _ _ he he₁, hm₁,
        by simp [← h₁]⟩
    | @id n =>
      exact ⟨mk n', e ≫ σ j, 𝟙 _, P_σ.comp_mem _ _ he (P_σ.σ _), P_δ.id_mem _, by simp⟩
    | comp_of f g hf hg =>
      cases n' with
      | zero =>
        cases hg
        exact ⟨_, _, _, he, hf, by simp [switch_δ_σ₀]⟩
      | succ n =>
        rcases hg with ⟨i⟩
        obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i
        · exact ⟨_, _, _, he, hf, by simp [h']⟩
        · obtain ⟨_, _, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' f hf
          exact ⟨_, _, m₁ ≫ δ j'', P_σ.comp_mem _ _ he he₁, P_δ.comp_mem _ _ hm₁ (P_δ.δ _),
            by simp [← reassoc_of% h₁, h']⟩
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ y) (_ : P_σ e) (_ : P_δ m), f = e ≫ m
have id : ∀ {n : ℕ}, ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), 𝟙 (mk n) = e ≫ m
Tactic: induction f with
  | @id n => use (mk n), (𝟙 (mk n)), (𝟙 (mk n)), P_σ.id_mem _, P_δ.id_mem _; simp
  | @comp_δ n n' f j h =>
    obtain ⟨z, e, m, ⟨he, hm, rfl⟩⟩ := h
    exact ⟨z, e, m ≫ δ j, he, P_δ.comp_mem _ _ hm (P_δ.δ _), by simp⟩
  | @comp_σ n n' f j h =>
    obtain ⟨z, e, m, ⟨he, hm, rfl⟩⟩ := h
    cases hm with
    | of g hg =>
      rcases hg with ⟨i⟩
      obtain ⟨_, _, _, ⟨he₁, hm₁, h₁⟩⟩ := factor_δ_σ j i
      exact ⟨_, _, _, P_σ.comp_mem _ _ he he₁, hm₁,
        by simp [← h₁]⟩
    | @id n =>
      exact ⟨mk n', e ≫ σ j, 𝟙 _, P_σ.comp_mem _ _ he (P_σ.σ _), P_δ.id_mem _, by simp⟩
    | comp_of f g hf hg =>
      cases n' with
      | zero =>
        cases hg
        exact ⟨_, _, _, he, hf, by simp [switch_δ_σ₀]⟩
      | succ n =>
        rcases hg with ⟨i⟩
        obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i
        · exact ⟨_, _, _, he, hf, by simp [h']⟩
        · obtain ⟨_, _, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' f hf
          exact ⟨_, _, m₁ ≫ δ j'', P_σ.comp_mem _ _ he he₁, P_δ.comp_mem _ _ hm₁ (P_δ.δ _),
            by simp [← reassoc_of% h₁, h']⟩
Cleared hypotheses: f