awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < (↑i : ℕ)
hₙ : (↑i : ℕ) < n
rw : 2 ≤ n
⊢ n = 2 ∨ 2 < n

Tactic:
rw [eq_comm, or_comm, ← le_iff_lt_or_eq]

Premises used: eq_comm, le_iff_lt_or_eq, or_comm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < (↑i : ℕ)
hₙ : (↑i : ℕ) < n
⊢ 2 ≤ n

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < (↑i : ℕ)
hₙ : (↑i : ℕ) < n
refine_2 :
  ∀ {i : Fin (HAdd.hAdd (α := ℕ) 2 1)} (j : Fin 2) (h₀ : 0 < (↑i : ℕ)) (hₙ : (↑i : ℕ) < 2),
    card (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) {i, j.castSucc, j.succ} ≤ 2
refine_2₁ : ∀ (hn : 2 < n), card (α := Fin (n + 1)) {i, j.castSucc, j.succ} ≤ n
⊢ card (α := Fin (n + 1)) {i, j.castSucc, j.succ} ≤ n

Tactic:
obtain rfl | hn : n = 2 ∨ 2 < n := by
    rw [eq_comm, or_comm, ← le_iff_lt_or_eq]; lia

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
j : Fin 2
h₀ : 0 < (↑i : ℕ)
hₙ : (↑i : ℕ) < 2
refine_2 :
  ∀ {i : Fin (HAdd.hAdd (α := ℕ) 2 1)} (j : Fin 2) (h₀ : 0 < (↑i : ℕ)) (hₙ : (↑i : ℕ) < 2),
    card (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) {i, j.castSucc, j.succ} ≤ 2
⊢ card (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) {i, j.castSucc, j.succ} ≤ 2

Tactic:
revert i j
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
⊢ ∀ {i : Fin (HAdd.hAdd (α := ℕ) 2 1)} (j : Fin 2) (h₀ : 0 < (↑i : ℕ)) (hₙ : (↑i : ℕ) < 2),
    card (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) {i, j.castSucc, j.succ} ≤ 2

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < (↑i : ℕ)
hₙ : (↑i : ℕ) < n
hn : 2 < n
⊢ card (α := Fin (n + 1)) {i, j.castSucc, j.succ} ≤ n

Tactic:
Finset.card_le_three.trans hn

Premises used: Finset.card_le_three, LE.le.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < (↑i : ℕ)
hₙ : (↑i : ℕ) < n
hn : 2 < n
⊢ card (α := Fin (n + 1)) {i, j.castSucc, j.succ} ≤ n

Tactic:
exact Finset.card_le_three.trans hn

Premises used: Finset.card_le_three, LE.le.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ k < n + 3 + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ k + 1 < n + 3 + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ k + 2 < n + 3 + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
refine_1 : (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ≤ ⟨k + 1, ⋯⟩
refine_2 : (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) ≤ ⟨k + 2, ⋯⟩
refine_3 :
  Membership.mem (γ := Set (Δ[n + 3] _⦋2⦌)) (Λ[n + 3, i].obj (op ⦋2⦌))
    (stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯)
⊢ Λ[n + 3, i].toSSet _⦋2⦌

Tactic:
refine ⟨stdSimplex.triangle
    (n := n+3) ⟨k, by lia⟩ ⟨k+1, by lia⟩ ⟨k+2, by lia⟩ ?_ ?_, ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ≤ ⟨k + 1, ⋯⟩

Tactic:
simp only [Fin.mk_le_mk, le_add_iff_nonneg_right, zero_le]

Premises used: zero_le, Fin.mk_le_mk, le_add_iff_nonneg_right
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) ≤ ⟨k + 2, ⋯⟩

Tactic:
simp only [Fin.mk_le_mk, add_le_add_iff_left, one_le_two]

Premises used: Fin.mk_le_mk, add_le_add_iff_left, one_le_two
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
refine_3 :
  ∃ (i_1 : Fin (n + 3 + 1)),
    ¬i_1 = i ∧
      ∀ (i : Fin 3),
        ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯
                  ⋯ :
                (a : Fin 3) → Fin (n + 3 + 1))
              i =
            i_1
⊢ Membership.mem (γ := Set (Δ[n + 3] _⦋2⦌)) (Λ[n + 3, i].obj (op ⦋2⦌))
    (stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯)

Tactic:
simp only [horn_eq_iSup, Subfunctor.iSup_obj, Set.iUnion_coe_set,
    Set.mem_compl_iff, Set.mem_singleton_iff, Set.mem_iUnion, stdSimplex.mem_face_iff,
    Nat.reduceAdd, mem_compl, mem_singleton, exists_prop]

Premises used: Finset.mem_singleton, Set.mem_iUnion, Set.iUnion_coe_set, Nat.reduceAdd, SSet.stdSimplex.mem_face_iff, Finset.mem_compl, exists_prop, Set.mem_singleton_iff, SSet.horn_eq_iSup, CategoryTheory.Subfunctor.iSup_obj, Set.mem_compl_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ k < n + 4

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ k + 1 < n + 4

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ k + 2 < n + 4

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
hS :
  Eq (α := Finset (Fin (n + 4))) {i, (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))}
    univ
obtain :
  ∀ (i : ℕ) (hi : i < n + 4) (h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))) (hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3))
    (hS :
      Eq (α := Finset (Fin (n + 4)))
        {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ),
    False
⊢ False

Tactic:
obtain ⟨i, hi⟩ := i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
pos : ∀ (hk : k = 0), False
neg : ∀ (hk : ¬k = 0), False
⊢ False

Tactic:
by_cases hk : k = 0
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
hk : k = 0
⊢ 0 < n + 2

Tactic:
subst hk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
hk : k = 0
h₁ : 0 < n + 2
⊢ Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, ⋯⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 4)),
      (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (n + 4))}
    univ

Tactic:
subst hk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
h : 0 < n + 2
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, ⋯⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 4)),
      (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (n + 4))}
    univ
⊢ Membership.mem (γ := Finset (Fin (n + 3 + 1))) univ (Fin.last (n + 3))

Tactic:
have := Finset.mem_univ (Fin.last _ : Fin (n + 4))
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
h : 0 < n + 2
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, ⋯⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 4)),
      (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (n + 4))}
    univ
this : Membership.mem (γ := Finset (Fin (n + 3 + 1))) univ (Fin.last (n + 3))
⊢ Membership.mem (γ := Finset (Fin (n + 3 + 1)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, ⋯⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 4)),
      (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (n + 4))}
    (Fin.last (n + 3))

Tactic:
rw [← hS] at this
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
h : 0 < n + 2
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, ⋯⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 4)),
      (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (n + 4))}
    univ
this :
  Membership.mem (γ := Finset (Fin (n + 3 + 1)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, ⋯⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 4)),
      (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (n + 4))}
    (Fin.last (n + 3))
⊢ n + 3 = i

Tactic:
simp only [Fin.zero_eta, zero_add, Fin.mk_one, mem_insert, Fin.ext_iff, Fin.val_last,
        Fin.val_zero, AddLeftCancelMonoid.add_eq_zero, OfNat.ofNat_ne_zero, and_false,
        Fin.val_one, Nat.reduceEqDiff, mem_singleton, or_self, or_false] at this

Premises used: Fin.mk_one, Finset.mem_singleton, Fin.ext_iff, OfNat.ofNat_ne_zero, AddLeftCancelMonoid.add_eq_zero, Fin.val_one, Finset.mem_insert, zero_add, Fin.zero_eta, Nat.reduceEqDiff, or_self, or_false, and_false, Fin.val_zero, Fin.val_last
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
h : 0 < n + 2
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, ⋯⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 4)),
      (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (n + 4))}
    univ
this : n + 3 = i
⊢ i < n + 3

Tactic:
simp only [Fin.lt_def, Fin.val_last] at hₙ

Premises used: Fin.lt_def, Fin.val_last
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
h : 0 < n + 2
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, ⋯⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 4)),
      (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (n + 4))}
    univ
this : n + 3 = i
hₙ : i < n + 3
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
hk : ¬k = 0
⊢ Membership.mem (γ := Finset (Fin (n + 4))) univ 0

Tactic:
have := Finset.mem_univ (0 : Fin (n + 4))
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
hk : ¬k = 0
this : Membership.mem (γ := Finset (Fin (n + 4))) univ 0
⊢ Membership.mem (γ := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} 0

Tactic:
rw [← hS] at this
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
hk : ¬k = 0
this :
  Membership.mem (γ := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} 0
⊢ 0 = i ∨ 0 = k

Tactic:
simp only [mem_insert, Fin.ext_iff, Fin.val_zero, right_eq_add,
        AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, mem_singleton,
        OfNat.ofNat_ne_zero, or_self, or_false] at this

Premises used: Finset.mem_singleton, Fin.ext_iff, OfNat.ofNat_ne_zero, AddLeftCancelMonoid.add_eq_zero, Finset.mem_insert, or_self, or_false, and_false, right_eq_add, one_ne_zero, Fin.val_zero
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
hk : ¬k = 0
this : 0 = i ∨ 0 = k
neg :
  ∀ (hi : 0 < n + 4) (h₀ : 0 < (⟨0, hi⟩ : Fin (n + 4))) (hₙ : (⟨0, hi⟩ : Fin (n + 4)) < Fin.last (n + 3))
    (hS :
      Eq (α := Finset (Fin (n + 4)))
        {(⟨0, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ),
    False
neg₁ :
  ∀ (h : 0 < n + 2)
    (hS :
      Eq (α := Finset (Fin (n + 4)))
        {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, ⋯⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 4)),
          (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (n + 4))}
        univ)
    (hk : ¬Eq (α := ℕ) 0 0), False
⊢ False

Tactic:
obtain rfl | rfl := this

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n k : ℕ
h : k < n + 2
hk : ¬k = 0
hi : 0 < n + 4
h₀ : 0 < (⟨0, hi⟩ : Fin (n + 4))
hₙ : (⟨0, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨0, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
⊢ False

Tactic:
tauto
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
h : 0 < n + 2
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, ⋯⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 4)),
      (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (n + 4))}
    univ
hk : ¬Eq (α := ℕ) 0 0
⊢ False

Tactic:
tauto
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ ¬Eq (α := Finset (Fin (n + 4))) {i, (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))}
      univ

Tactic:
have hS : ¬ ({i, (⟨k, by lia⟩ : Fin (n + 4)), (⟨k + 1, by lia⟩ : Fin (n + 4)),
      (⟨k + 2, by lia⟩ : Fin (n + 4))} = Finset.univ) := fun hS ↦ by
    obtain ⟨i, hi⟩ := i
    by_cases hk : k = 0
    · subst hk
      have := Finset.mem_univ (Fin.last _ : Fin (n + 4))
      rw [← hS] at this
      -- this was produced using `simp? [Fin.ext_iff] at this`
      simp only [Fin.zero_eta, zero_add, Fin.mk_one, mem_insert, Fin.ext_iff, Fin.val_last,
        Fin.val_zero, AddLeftCancelMonoid.add_eq_zero, OfNat.ofNat_ne_zero, and_false,
        Fin.val_one, Nat.reduceEqDiff, mem_singleton, or_self, or_false] at this
      simp only [Fin.lt_def, Fin.val_last] at hₙ
      lia
    · have := Finset.mem_univ (0 : Fin (n + 4))
      rw [← hS] at this
      -- this was produced using `simp? [Fin.ext_iff] at this`
      simp only [mem_insert, Fin.ext_iff, Fin.val_zero, right_eq_add,
        AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, mem_singleton,
        OfNat.ofNat_ne_zero, or_self, or_false] at this
      obtain rfl | rfl := this <;> tauto
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
hS :
  ¬Eq (α := Finset (Fin (n + 4))) {i, (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))}
      univ
⊢ ∃ (x : Fin (n + 4)), x ∉ {i, (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))}

Tactic:
rw [Finset.eq_univ_iff_forall, not_forall] at hS

Premises used: Finset.eq_univ_iff_forall, Classical.not_forall
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
hS : ∃ (x : Fin (n + 4)), x ∉ {i, (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))}
refine_3 :
  ∀ (l : Fin (n + 4)) (hl : l ∉ {i, (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))}),
    ∃ (i_1 : Fin (n + 3 + 1)),
      ¬i_1 = i ∧
        ∀ (i : Fin 3),
          ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1))
                    ⋯ ⋯ :
                  (a : Fin 3) → Fin (n + 3 + 1))
                i =
              i_1
⊢ ∃ (i_1 : Fin (n + 3 + 1)),
    ¬i_1 = i ∧
      ∀ (i : Fin 3),
        ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯
                  ⋯ :
                (a : Fin 3) → Fin (n + 3 + 1))
              i =
            i_1

Tactic:
obtain ⟨l, hl⟩ := hS
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
l : Fin (n + 4)
hl : l ∉ {i, (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))}
⊢ ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩

Tactic:
simp only [mem_insert, mem_singleton, not_or] at hl

Premises used: Finset.mem_singleton, Finset.mem_insert, not_or
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
l : Fin (n + 4)
hl : ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩
⊢ ∃ (i_1 : Fin (n + 3 + 1)),
    ¬i_1 = i ∧
      ∀ (i : Fin 3),
        ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯
                  ⋯ :
                (a : Fin 3) → Fin (n + 3 + 1))
              i =
            i_1

Tactic:
⟨l, hl.1, fun a ↦ ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
l : Fin (n + 4)
hl : ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩
refine_3 :
  ∀ (a : Fin 3),
    ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
            (a : Fin 3) → Fin (n + 3 + 1))
          a =
        l
⊢ ∃ (i_1 : Fin (n + 3 + 1)),
    ¬i_1 = i ∧
      ∀ (i : Fin 3),
        ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯
                  ⋯ :
                (a : Fin 3) → Fin (n + 3 + 1))
              i =
            i_1

Tactic:
refine ⟨l, hl.1, fun a ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
l : Fin (n + 4)
hl : ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩
a : Fin 3
refine_3 :
  ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) =
      l
refine_3₁ :
  ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨1, ⋯⟩) =
      l
refine_3₂ :
  ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨2, ⋯⟩) =
      l
⊢ ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        a =
      l

Tactic:
fin_cases a
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
l : Fin (n + 4)
hl : ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩
⊢ ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) =
      l

Tactic:
Ne.symm hl.2.1

Premises used: Ne.symm, And.right, And.left
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
l : Fin (n + 4)
hl : ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩
⊢ ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) =
      l

Tactic:
exact Ne.symm hl.2.1

Premises used: Ne.symm, And.right, And.left
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
l : Fin (n + 4)
hl : ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩
⊢ ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨1, ⋯⟩) =
      l

Tactic:
Ne.symm hl.2.2.1

Premises used: Ne.symm, And.right, And.left
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
l : Fin (n + 4)
hl : ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩
⊢ ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨1, ⋯⟩) =
      l

Tactic:
exact Ne.symm hl.2.2.1

Premises used: Ne.symm, And.right, And.left
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
l : Fin (n + 4)
hl : ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩
⊢ ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨2, ⋯⟩) =
      l

Tactic:
Ne.symm hl.2.2.2

Premises used: Ne.symm, And.right
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
l : Fin (n + 4)
hl : ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩
⊢ ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨2, ⋯⟩) =
      l

Tactic:
exact Ne.symm hl.2.2.2

Premises used: Ne.symm, And.right
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i j : Fin (n + 2)
h : j ≠ i
⊢ Subfunctor.range (stdSimplex.δ j) ≤ Λ[n + 1, i]

Tactic:
simpa using face_le_horn _ _ h

Premises used: SSet.face_le_horn
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    Eq (α := (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₁.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₂.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
rw : Subfunctor.equalizer σ₁ σ₂ = Λ[n + 1, i]
⊢ σ₁ = σ₂

Tactic:
rw [← Subfunctor.equalizer_eq_iff]

Premises used: CategoryTheory.Subfunctor.equalizer_eq_iff