awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
h_δ : P_δ f
⊢ (∃ (h : x = y), f = eqToHom h) ∨ x.len < y.len
have of : ∀ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (hx : faces f), (∃ (h : x = y), f = eqToHom h) ∨ x.len < y.len
Tactic: induction h_δ with
  | of _ hx => cases hx; right; simp
  | id => left; use rfl; simp
  | comp_of i u _ hg h' =>
    rcases h' with ⟨e, _⟩ | h' <;>
    apply Or.inr <;>
    cases hg
    · rw [e]
      exact Nat.lt_add_one _
    · exact Nat.lt_succ_of_lt h'
Cleared hypotheses: h_δ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
h_δ : P_δ f
of : ∀ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (hx : faces f), (∃ (h : x = y), f = eqToHom h) ∨ x.len < y.len
⊢ (∃ (h : x = y), f = eqToHom h) ∨ x.len < y.len
have id : ∀ (x : SimplexCategoryGenRel), (∃ (h : x = x), 𝟙 x = eqToHom h) ∨ x.len < x.len
Tactic: induction h_δ with
  | of _ hx => cases hx; right; simp
  | id => left; use rfl; simp
  | comp_of i u _ hg h' =>
    rcases h' with ⟨e, _⟩ | h' <;>
    apply Or.inr <;>
    cases hg
    · rw [e]
      exact Nat.lt_add_one _
    · exact Nat.lt_succ_of_lt h'
Cleared hypotheses: h_δ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
h_δ : P_δ f
of : ∀ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (hx : faces f), (∃ (h : x = y), f = eqToHom h) ∨ x.len < y.len
id : ∀ (x : SimplexCategoryGenRel), (∃ (h : x = x), 𝟙 x = eqToHom h) ∨ x.len < x.len
⊢ (∃ (h : x = y), f = eqToHom h) ∨ x.len < y.len
have comp_of : ∀ {x y z : SimplexCategoryGenRel} (i : x ⟶ y) (u : y ⟶ z),
  faces.multiplicativeClosure i →
    ∀ (hg : faces u) (h' : (∃ (h : x = y), i = eqToHom h) ∨ x.len < y.len),
      (∃ (h : x = z), i ≫ u = eqToHom h) ∨ x.len < z.len
Tactic: induction h_δ with
  | of _ hx => cases hx; right; simp
  | id => left; use rfl; simp
  | comp_of i u _ hg h' =>
    rcases h' with ⟨e, _⟩ | h' <;>
    apply Or.inr <;>
    cases hg
    · rw [e]
      exact Nat.lt_add_one _
    · exact Nat.lt_succ_of_lt h'
Cleared hypotheses: h_δ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
have inl : ∀ (h : i.castSucc < i'), δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
Tactic: obtain h | rfl | h := lt_trichotomy i.castSucc i'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
inl :
  ∀ (h : i.castSucc < i'), δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
have inr : δ i.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i.castSucc ≫ σ i = σ j ≫ δ j'
Tactic: obtain h | rfl | h := lt_trichotomy i.castSucc i'
Cleared hypotheses: i'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
inl :
  ∀ (h : i.castSucc < i'), δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
inr : δ i.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i.castSucc ≫ σ i = σ j ≫ δ j'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
have inr₁ : ∀ (h : i' < i.castSucc), δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
Tactic: obtain h | rfl | h := lt_trichotomy i.castSucc i'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (hypothesis)
Goal:
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i.castSucc < i'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
have h₁ : i.succ ≤ i'
Tactic: rw [Fin.castSucc_lt_iff_succ_le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i.succ ≤ i'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
have inl : ∀ (h : i.succ < i'), δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
Tactic: obtain h | rfl := h.lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i.succ ≤ i'
inl : ∀ (h : i.succ < i'), δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
have inl₁ : ∀ (h : i.succ ≤ i.succ),
  δ i.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i.succ ≫ σ i = σ j ≫ δ j'
Tactic: obtain h | rfl := h.lt_or_eq
Cleared hypotheses: i', h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h_1 : i.succ ≤ i'
h : i.succ < i'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
have inl : ∀ (i' : Fin (n + 2)) (h : i.succ ≤ i'.succ) (h : i.succ < i'.succ),
  δ i'.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.succ ≫ σ i = σ j ≫ δ j'
Tactic: obtain ⟨i', rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)
Cleared hypotheses: i', h_1, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (hypothesis)
Goal:
n : ℕ
i i' : Fin (n + 2)
h_1 : i.succ ≤ i'.succ
h : i.succ < i'.succ
⊢ δ i'.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.succ ≫ σ i = σ j ≫ δ j'
have h₁ : i < i'
Tactic: rw [Fin.succ_lt_succ_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
i i' : Fin (n + 2)
h_1 : i.succ ≤ i'.succ
h : i < i'
⊢ δ i'.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.succ ≫ σ i = σ j ≫ δ j'
have inl : ∀ (i : Fin (n + 1)) (h : i.castSucc.succ ≤ i'.succ) (h : i.castSucc < i'),
  δ i'.succ ≫ σ i.castSucc = 𝟙 (mk (n + 1)) ∨
    ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.succ ≫ σ i.castSucc = σ j ≫ δ j'
Tactic: obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)
Cleared hypotheses: i, h_1, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h_1 : i.castSucc.succ ≤ i'.succ
h : i.castSucc < i'
⊢ δ i'.succ ≫ σ i.castSucc = σ i ≫ δ i'
have rw : σ i ≫ δ i' = σ i ≫ δ i'
Tactic: rw [δ_comp_σ_of_gt h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i' < i.castSucc
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
have inr : ∀ (i' : Fin (n + 2)) (h : i'.castSucc < i.castSucc),
  δ i'.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.castSucc ≫ σ i = σ j ≫ δ j'
Tactic: obtain ⟨i', rfl⟩ := Fin.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)
Cleared hypotheses: i', h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (hypothesis)
Goal:
n : ℕ
i i' : Fin (n + 2)
h : i'.castSucc < i.castSucc
⊢ δ i'.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.castSucc ≫ σ i = σ j ≫ δ j'
have h₁ : i' < i
Tactic: rw [Fin.castSucc_lt_castSucc_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
i i' : Fin (n + 2)
h : i' < i
⊢ δ i'.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.castSucc ≫ σ i = σ j ≫ δ j'
have inr : ∀ (i : Fin (n + 1)) (h : i' < i.succ),
  δ i'.castSucc ≫ σ i.succ = 𝟙 (mk (n + 1)) ∨
    ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.castSucc ≫ σ i.succ = σ j ≫ δ j'
Tactic: obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (hypothesis)
Goal:
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' < i.succ
⊢ δ i'.castSucc ≫ σ i.succ = 𝟙 (mk (n + 1)) ∨
    ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.castSucc ≫ σ i.succ = σ j ≫ δ j'
have h₁ : i' ≤ i.castSucc
Tactic: rw [← Fin.le_castSucc_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' ≤ i.castSucc
⊢ δ i'.castSucc ≫ σ i.succ = σ i ≫ δ i'
have rw : σ i ≫ δ i' = σ i ≫ δ i'
Tactic: rw [δ_comp_σ_of_le h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
i : Fin 1
i' : Fin 2
⊢ δ i' ≫ σ i = 𝟙 (mk 0)
have 0 : δ i' ≫
    σ
      ((fun (i : Fin ({ len := 0 : SimplexCategory }.len + 1)) ↦ i)
        (⟨0, sorry⟩ : Fin ({ len := 0 : SimplexCategory }.len + 1))) =
  𝟙 (mk 0)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
i' : Fin 2
⊢ δ i' ≫
      σ
        ((fun (i : Fin ({ len := 0 : SimplexCategory }.len + 1)) ↦ i)
          (⟨0, ⋯⟩ : Fin ({ len := 0 : SimplexCategory }.len + 1))) =
    𝟙 (mk 0)
have 0 : δ
      ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i)
        (⟨0, sorry⟩ : Fin ({ len := 1 : SimplexCategory }.len + 1))) ≫
    σ ((fun (i : Fin ({ len := 0 : SimplexCategory }.len + 1)) ↦ i) ⟨0, sorry⟩) =
  𝟙 (mk 0)
Tactic: fin_cases i'
Cleared hypotheses: i'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
i' : Fin 2
0 :
  δ
        ((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)
⊢ δ i' ≫
      σ
        ((fun (i : Fin ({ len := 0 : SimplexCategory }.len + 1)) ↦ i)
          (⟨0, ⋯⟩ : Fin ({ len := 0 : SimplexCategory }.len + 1))) =
    𝟙 (mk 0)
have 0₁ : δ
      ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i)
        (⟨1, sorry⟩ : Fin ({ len := 1 : SimplexCategory }.len + 1))) ≫
    σ ((fun (i : Fin ({ len := 0 : SimplexCategory }.len + 1)) ↦ i) ⟨0, sorry⟩) =
  𝟙 (mk 0)
Tactic: fin_cases i'
Cleared hypotheses: i'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
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
have 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
Tactic: obtain h | ⟨j, j', h⟩ := switch_δ_σ i i'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
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
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m
have 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
Tactic: obtain h | ⟨j, j', h⟩ := switch_δ_σ i i'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
i : Fin (n + 1)
i' : Fin (n + 2)
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m
have 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
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⟩
Cleared hypotheses: n, i, i'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
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
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m
have 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
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⟩
Cleared hypotheses: n, i, i'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
x : SimplexCategoryGenRel
f : x ⟶ mk (HAdd.hAdd (α := ℕ) 0 1)
h : faces f
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
have 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
Tactic: cases h
Cleared hypotheses: x, f, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
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
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), (j ≫ f) ≫ σ i = e ≫ m
have 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
Tactic: obtain ⟨k⟩ := hg
Cleared hypotheses: y, j, hf, f, hg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
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
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), (j ≫ δ k) ≫ σ i = e ≫ m
have zero : ∀ (hf : faces.multiplicativeClosure (eqToHom sorry)),
  ∃ (z : SimplexCategoryGenRel) (e : mk 0 ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), (eqToHom sorry ≫ δ k) ≫ σ i = e ≫ m
Tactic: obtain ⟨rfl, rfl⟩ | hf' := eq_or_len_le_of_P_δ hf
Cleared hypotheses: x, j, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
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
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), (j ≫ δ k) ≫ σ i = e ≫ m
have 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
Tactic: obtain ⟨rfl, rfl⟩ | hf' := eq_or_len_le_of_P_δ hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
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
have zero : ∀ (h : faces f), ∃ (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'
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
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
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
have 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
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'
Cleared hypotheses: x, f, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
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
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk 0) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
have 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
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'
Cleared hypotheses: 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)
h : faces f
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
have 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
Tactic: cases h
Cleared hypotheses: x, f, h
-- 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 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
have 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
Tactic: obtain ⟨k⟩ := hg
Cleared hypotheses: y, f, hf, g, hg
-- 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
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m
have succ : ∀ (hf : faces.multiplicativeClosure (eqToHom sorry)),
  ∃ (z : SimplexCategoryGenRel) (e : mk (n + 1) ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m),
    (eqToHom sorry ≫ δ k) ≫ σ i = e ≫ m
Tactic: obtain ⟨rfl, rfl⟩ | h' := eq_or_len_le_of_P_δ hf
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 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
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m
have 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
Tactic: obtain ⟨rfl, rfl⟩ | h' := eq_or_len_le_of_P_δ 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 X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
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
have 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
Tactic: obtain h'' | ⟨j, j', h''⟩ := switch_δ_σ i k
-- 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
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
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk (n + 1)) (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m
have 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
Tactic: obtain h'' | ⟨j, j', h''⟩ := switch_δ_σ i k