awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd : n ≤ d
S : Finset (Fin (n + 1 + 1))
hS : S.card = d + 1
hx : stdSimplex.face S ≤ A
neg : ∀ (hd : n < d), stdSimplex.face S ≤ Λ[n + 1, i]
neg₁ : ∀ (hd : n ≤ n) (hS : S.card = n + 1), stdSimplex.face S ≤ Λ[n + 1, i]
⊢ stdSimplex.face S ≤ Λ[n + 1, i]

Tactic:
obtain hd | rfl := hd.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd_1 : n ≤ d
S : Finset (Fin (n + 1 + 1))
hS : S.card = d + 1
hx : stdSimplex.face S ≤ A
hd : n < d
rw : S.card = n + 1 + 1
⊢ S = Finset.univ

Tactic:
rw [← Finset.card_eq_iff_eq_univ, Fintype.card_fin]

Premises used: Fintype.card_fin, Finset.card_eq_iff_eq_univ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd_1 : n ≤ d
S : Finset (Fin (n + 1 + 1))
hS : S.card = d + 1
hx : stdSimplex.face S ≤ A
hd : n < d
⊢ n + 1 + 1 ≤ S.card

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd_1 : n ≤ d
S : Finset (Fin (n + 1 + 1))
hS : S.card = d + 1
hx : stdSimplex.face S ≤ A
hd : n < d
⊢ S.card = n + 1 + 1

Tactic:
exact le_antisymm (card_finset_fin_le S) (by lia)

Premises used: card_finset_fin_le, le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd_1 : n ≤ d
S : Finset (Fin (n + 1 + 1))
hS : S.card = d + 1
hx : stdSimplex.face S ≤ A
hd : n < d
neg :
  ∀ (hS : Finset.card (α := Fin (n + 1 + 1)) Finset.univ = d + 1) (hx : stdSimplex.face Finset.univ ≤ A),
    stdSimplex.face Finset.univ ≤ Λ[n + 1, i]
⊢ stdSimplex.face S ≤ Λ[n + 1, i]

Tactic:
obtain rfl : S = .univ := by
          rw [← Finset.card_eq_iff_eq_univ, Fintype.card_fin]
          exact le_antisymm (card_finset_fin_le S) (by lia)

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd_1 : n ≤ d
hd : n < d
hS : Finset.card (α := Fin (n + 1 + 1)) Finset.univ = d + 1
hx : stdSimplex.face Finset.univ ≤ A
⊢ LE.le.{u} (α := Δ[n + 1].Subcomplex) (stdSimplex.face {i}ᶜ) (stdSimplex.face Finset.univ)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd_1 : n ≤ d
hd : n < d
hS : Finset.card (α := Fin (n + 1 + 1)) Finset.univ = d + 1
hx : stdSimplex.face Finset.univ ≤ A
⊢ stdSimplex.face Finset.univ ≤ Λ[n + 1, i]

Tactic:
exact (h (le_trans (by simp) hx)).elim

Premises used: False.elim, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : S.card = n + 1
⊢ Sᶜ.card + S.card = Fintype.card (Fin (n + 1 + 1))

Tactic:
have := S.card_compl_add_card
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : S.card = n + 1
this : Sᶜ.card + S.card = Fintype.card (Fin (n + 1 + 1))
⊢ Sᶜ.card + S.card = n + 1 + 1

Tactic:
rw [Fintype.card_fin] at this

Premises used: Fintype.card_fin
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : S.card = n + 1
this : Sᶜ.card + S.card = n + 1 + 1
⊢ Sᶜ.card = 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : S.card = n + 1
⊢ Sᶜ.card = 1

Tactic:
replace hS : Sᶜ.card = 1 := by
          have := S.card_compl_add_card
          rw [Fintype.card_fin] at this
          lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : Sᶜ.card = 1
⊢ ∃ (a : Fin (n + 1 + 1)), Sᶜ = {a}

Tactic:
rw [Finset.card_eq_one] at hS

Premises used: Finset.card_eq_one
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : ∃ (a : Fin (n + 1 + 1)), Sᶜ = {a}
obtain : ∀ (j : Fin (n + 1 + 1)) (hS : Sᶜ = {j}), ∃ (j : Fin (n + 1 + 1)), S = {j}ᶜ
⊢ ∃ (j : Fin (n + 1 + 1)), S = {j}ᶜ

Tactic:
obtain ⟨j, hS⟩ := hS
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
j : Fin (n + 1 + 1)
hS : Sᶜ = {j}
⊢ S = {j}ᶜ

Tactic:
simp [← hS]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
j : Fin (n + 1 + 1)
hS : Sᶜ = {j}
⊢ ∃ (j : Fin (n + 1 + 1)), S = {j}ᶜ

Tactic:
exact ⟨j, by simp [← hS]⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : Sᶜ.card = 1
neg :
  ∀ (j : Fin (n + 1 + 1)) (hx : stdSimplex.face {j}ᶜ ≤ A) (hS : Finset.card (α := Fin (n + 1 + 1)) {j}ᶜᶜ = 1),
    stdSimplex.face {j}ᶜ ≤ Λ[n + 1, i]
⊢ stdSimplex.face S ≤ Λ[n + 1, i]

Tactic:
obtain ⟨j, rfl⟩ : ∃ j, S = {j}ᶜ := by
          rw [Finset.card_eq_one] at hS
          obtain ⟨j, hS⟩ := hS
          exact ⟨j, by simp [← hS]⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
hd : n ≤ n
j : Fin (n + 1 + 1)
hx : stdSimplex.face {j}ᶜ ≤ A
hS : Finset.card (α := Fin (n + 1 + 1)) {j}ᶜᶜ = 1
h : ¬stdSimplex.face {j}ᶜ ≤ A
⊢ False

Tactic:
tauto
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
hd : n ≤ n
j : Fin (n + 1 + 1)
hx : stdSimplex.face {j}ᶜ ≤ A
hS : Finset.card (α := Fin (n + 1 + 1)) {j}ᶜᶜ = 1
⊢ stdSimplex.face {j}ᶜ ≤ Λ[n + 1, i]

Tactic:
exact face_le_horn _ _ (by rintro rfl; tauto)

Premises used: SSet.face_le_horn
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
rw : ¬¬{j}ᶜ ≤ S ↔ ¬(S ≠ Finset.univ ∧ S ≠ {j}ᶜ)
⊢ stdSimplex.face S ≤ Λ[n + 1, j] ↔ S ≠ Finset.univ ∧ S ≠ {j}ᶜ

Tactic:
rw [subcomplex_le_horn_iff, stdSimplex.face_le_face_iff, ← not_iff_not]

Premises used: not_iff_not, SSet.subcomplex_le_horn_iff, SSet.stdSimplex.face_le_face_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
simp : {j}ᶜ ⊆ S ↔ S = Finset.univ ∨ S = {j}ᶜ
⊢ ¬¬{j}ᶜ ≤ S ↔ ¬(S ≠ Finset.univ ∧ S ≠ {j}ᶜ)

Tactic:
simp only [Finset.le_eq_subset, Decidable.not_not, ne_eq, not_and_or]

Premises used: ne_eq, not_and_or, Finset.le_eq_subset, Decidable.not_not
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
⊢ S = Finset.univ ∨ S = {j}ᶜ → {j}ᶜ ⊆ S

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
refine : ∀ (h : {j}ᶜ ⊆ S), S = Finset.univ ∨ S = {j}ᶜ
⊢ {j}ᶜ ⊆ S ↔ S = Finset.univ ∨ S = {j}ᶜ

Tactic:
refine ⟨fun h ↦ ?_, by aesop⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
h : {j}ᶜ ⊆ S
⊢ S = Finset.univ ∨ Sᶜ = {j}

Tactic:
rw [← Finset.compl_subset_compl, compl_compl,
    Finset.subset_singleton_iff, Finset.compl_eq_empty_iff] at h

Premises used: compl_compl, Finset.subset_singleton_iff, Finset.compl_subset_compl, Finset.compl_eq_empty_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
h : S = Finset.univ ∨ Sᶜ = {j}
⊢ S = Finset.univ ∨ S = {j}ᶜ

Tactic:
grind [eq_compl_comm]

Premises used: eq_compl_comm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
d : SimplexCategory
f : d ⟶ ⦋n⦌
inst : IsIso f
rw :
  Eq (α := Set (Fin (n + 1)))
    (Set.range (ι := Fin ((unop (op d)).len + 1))
        (⇑(stdSimplex.asOrderHom.{u} ((Equiv.symm stdSimplex.objEquiv : (a : unop (op d) ⟶ ⦋n⦌) → Δ[n].obj (op d)) f)) :
          (a : Fin ((unop (op d)).len + 1)) → Fin (n + 1)) ∪
      {i})
    Set.univ
⊢ ((Equiv.symm stdSimplex.objEquiv : (a : unop (op d) ⟶ ⦋n⦌) → Δ[n].obj (op d)) f : Δ[n].obj (op d)) ∉
    Λ[n, i].obj (op d)

Tactic:
rw [mem_horn_iff, ne_eq, not_not]

Premises used: Classical.not_not, SSet.mem_horn_iff, ne_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
d : SimplexCategory
f : d ⟶ ⦋n⦌
inst : IsIso f
h :
  ∀ (i_1 : Fin (n + 1)),
    Membership.mem (γ := Set (Fin (n + 1)))
        (Set.range (ι := Fin ((unop (op d)).len + 1))
            (⇑(stdSimplex.asOrderHom.{u}
                  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op d) ⟶ ⦋n⦌) → Δ[n].obj (op d)) f)) :
              (a : Fin ((unop (op d)).len + 1)) → Fin (n + 1)) ∪
          {i})
        i_1 ↔
      Membership.mem (γ := Set (Fin (n + 1))) Set.univ i_1
⊢ Eq (α := Set (Fin (n + 1)))
    (Set.range (ι := Fin ((unop (op d)).len + 1))
        (⇑(stdSimplex.asOrderHom.{u} ((Equiv.symm stdSimplex.objEquiv : (a : unop (op d) ⟶ ⦋n⦌) → Δ[n].obj (op d)) f)) :
          (a : Fin ((unop (op d)).len + 1)) → Fin (n + 1)) ∪
      {i})
    Set.univ

Tactic:
ext i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i_1 : Fin (n + 1)
d : SimplexCategory
f : d ⟶ ⦋n⦌
inst : IsIso f
i : Fin (n + 1)
⊢ (stdSimplex.asOrderHom.{u} ((Equiv.symm stdSimplex.objEquiv : (a : d ⟶ ⦋n⦌) → Δ[n].obj (op d)) f) :
        (a : Fin (d.len + 1)) → Fin (n + 1))
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (inv f) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) d)
        i) =
    i

Tactic:
simp [stdSimplex.coe_asOrderHom_objEquiv_symm.{u}]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i_1 : Fin (n + 1)
d : SimplexCategory
f : d ⟶ ⦋n⦌
inst : IsIso f
i : Fin (n + 1)
⊢ Membership.mem (γ := Set (Fin (n + 1)))
      (Set.range (ι := Fin ((unop (op d)).len + 1))
          (⇑(stdSimplex.asOrderHom.{u}
                ((Equiv.symm stdSimplex.objEquiv : (a : unop (op d) ⟶ ⦋n⦌) → Δ[n].obj (op d)) f)) :
            (a : Fin ((unop (op d)).len + 1)) → Fin (n + 1)) ∪
        {i_1})
      i ↔
    Membership.mem (γ := Set (Fin (n + 1))) Set.univ i

Tactic:
simpa using Or.inr ⟨inv f i, by simp [stdSimplex.coe_asOrderHom_objEquiv_symm.{u}]⟩

Premises used: Or.inr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i j : Fin (n + 2)
rw : Ne (α := Finset (Fin (n + 2))) {i}ᶜ Finset.univ ∧ Ne (α := Finset (Fin (n + 2))) {i}ᶜ {j}ᶜ ↔ ¬i = j
⊢ Membership.mem (α := Δ[n + 1] _⦋n⦌) (γ := Set (Δ[n + 1] _⦋n⦌)) (Λ[n + 1, j].obj (op ⦋n⦌))
      ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) : Δ[n + 1] _⦋n⦌) ↔
    ¬i = j

Tactic:
rw [← Subcomplex.ofSimplex_le_iff, ← stdSimplex.face_singleton_compl, face_le_horn_iff]

Premises used: SSet.face_le_horn_iff, SSet.Subcomplex.ofSimplex_le_iff, SSet.stdSimplex.face_singleton_compl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i j : Fin (n + 2)
⊢ Ne (α := Finset (Fin (n + 2))) {i}ᶜ Finset.univ ∧ Ne (α := Finset (Fin (n + 2))) {i}ᶜ {j}ᶜ ↔ ¬i = j

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i j : Fin (n + 2)
⊢ ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) :
        Δ[n + 1] _⦋n⦌) ∉
      Λ[n + 1, j].obj (op ⦋n⦌) ↔
    i = j

Tactic:
simp [objEquiv_symm_δ_mem_horn_iff.{u}]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
obj :
  ∀ (d : ℕ) (j : Δ[n] _⦋d⦌),
    Membership.mem (γ := Set (Δ[n] _⦋d⦌)) ((Λ[n, i].op.preimage (Iso.inv (stdSimplex.opIso ⦋n⦌))).obj (op ⦋d⦌)) j ↔
      Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Λ[n, i.rev].obj (op ⦋d⦌)) j
⊢ Λ[n, i].op.preimage (Iso.inv (stdSimplex.opIso ⦋n⦌)) = Λ[n, i.rev]

Tactic:
ext ⟨⟨d⟩⟩ j
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
obj :
  (∃ (j_1 : Fin (n + 1)),
      ¬j_1 = i ∧ ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1) ↔
    ∃ (j_1 : Fin (n + 1)), ¬j_1 = i.rev ∧ ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) ((Λ[n, i].op.preimage (Iso.inv (stdSimplex.opIso ⦋n⦌))).obj (op ⦋d⦌)) j ↔
    Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Λ[n, i.rev].obj (op ⦋d⦌)) j

Tactic:
simp only [Subcomplex.preimage_obj, Set.mem_preimage, stdSimplex.opIso_inv_app_hom_apply,
    Subcomplex.mem_op_obj_iff, mem_horn_iff_notMem_range, Set.mem_range, not_exists, ne_eq,
    exists_prop, stdSimplex.opObjEquiv_opObjEquiv_symm_apply]

Premises used: Set.mem_range, not_exists, SSet.Subcomplex.mem_op_obj_iff, exists_prop, ne_eq, SSet.Subcomplex.preimage_obj, SSet.mem_horn_iff_notMem_range, SSet.stdSimplex.opObjEquiv_opObjEquiv_symm_apply, Set.mem_preimage, SSet.stdSimplex.opIso_inv_app_hom_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
obj :
  (∃ (j_1 : Fin (n + 1)),
      ¬j_1 = i ∧ ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1) →
    ∃ (j_1 : Fin (n + 1)), ¬j_1 = i.rev ∧ ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1
obj₁ :
  (∃ (j_1 : Fin (n + 1)), ¬j_1 = i.rev ∧ ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1) →
    ∃ (j_1 : Fin (n + 1)), ¬j_1 = i ∧ ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1
⊢ (∃ (j_1 : Fin (n + 1)),
      ¬j_1 = i ∧ ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1) ↔
    ∃ (j_1 : Fin (n + 1)), ¬j_1 = i.rev ∧ ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
h₁ : ¬k = i
h₂ : ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = k
⊢ ¬k.rev = i.rev

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
h₁ : ¬k = i
h₂ : ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = k
l : Fin (d + 1)
hl : (j : (a : Fin (d + 1)) → Fin (n + 1)) l = k.rev
⊢ False

Tactic:
grind [h₂ l.rev]

Premises used: Fin.rev
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
h₁ : ¬k = i
h₂ : ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = k
⊢ ∃ (j_1 : Fin (n + 1)), ¬j_1 = i.rev ∧ ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1

Tactic:
exact ⟨k.rev, by simpa, fun l hl ↦ by grind [h₂ l.rev]⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
h₁ : ¬k = i.rev
h₂ : ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = k
⊢ ¬k.rev = i ∧ ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = k.rev

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
h₁ : ¬k = i.rev
h₂ : ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = k
⊢ ∃ (j_1 : Fin (n + 1)), ¬j_1 = i ∧ ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1

Tactic:
exact ⟨k.rev, by grind⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i k : Fin (n + 3)
m : SimplexCategoryᵒᵖ
⊢ Membership.mem (α := Δ[n + 2] _⦋0⦌) (γ := Set (Δ[n + 2] _⦋0⦌)) (Λ[n + 2, i].obj (op ⦋0⦌))
    ((Equiv.symm stdSimplex.obj₀Equiv : (a : Fin (n + 2 + 1)) → Δ[n + 2] _⦋0⦌) k : Δ[n + 2] _⦋0⦌)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i k : Fin (n + 3)
m : ℕ
a : Fin (m + 1)
⊢ ((↑(const n i k (op ⦋m⦌)) : Δ[n + 2] _⦋m⦌) : (a : Fin (m + 1)) → Fin (n + 2 + 1)) a = k

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : card (α := Fin (n + 1)) {i, a, b} ≤ n
hS : Eq (α := Finset (Fin (n + 1))) {i, a, b} univ
⊢ card (α := Fin (n + 1)) univ ≤ card (α := Fin (n + 1)) {i, a, b}

Tactic:
have := Finset.card_le_card hS.symm.le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : card (α := Fin (n + 1)) {i, a, b} ≤ n
hS : Eq (α := Finset (Fin (n + 1))) {i, a, b} univ
this : card (α := Fin (n + 1)) univ ≤ card (α := Fin (n + 1)) {i, a, b}
⊢ n + 1 ≤ card (α := Fin (n + 1)) {i, a, b}

Tactic:
simp only [card_univ, Fintype.card_fin] at this

Premises used: Finset.card_univ, Fintype.card_fin
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : card (α := Fin (n + 1)) {i, a, b} ≤ n
hS : Eq (α := Finset (Fin (n + 1))) {i, a, b} univ
this : n + 1 ≤ card (α := Fin (n + 1)) {i, a, b}
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : card (α := Fin (n + 1)) {i, a, b} ≤ n
⊢ ¬Eq (α := Finset (Fin (n + 1))) {i, a, b} univ

Tactic:
have hS : ¬ ({i, a, b} = Finset.univ) := fun hS ↦ by
      have := Finset.card_le_card hS.symm.le
      simp only [card_univ, Fintype.card_fin] at this
      lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : card (α := Fin (n + 1)) {i, a, b} ≤ n
hS : ¬Eq (α := Finset (Fin (n + 1))) {i, a, b} univ
⊢ ∃ (x : Fin (n + 1)), x ∉ {i, a, b}

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 a b : Fin (n + 1)
hab : a ≤ b
H : card (α := Fin (n + 1)) {i, a, b} ≤ n
hS : ∃ (x : Fin (n + 1)), x ∉ {i, a, b}
obtain :
  ∀ (k : Fin (n + 1)) (hk : k ∉ {i, a, b}),
    Membership.mem (γ := Set (Δ[n] _⦋1⦌)) (Λ[n, i].obj (op ⦋1⦌)) (stdSimplex.edge n a b hab)
⊢ Membership.mem (γ := Set (Δ[n] _⦋1⦌)) (Λ[n, i].obj (op ⦋1⦌)) (stdSimplex.edge n a b hab)

Tactic:
obtain ⟨k, hk⟩ := hS
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : card (α := Fin (n + 1)) {i, a, b} ≤ n
k : Fin (n + 1)
hk : k ∉ {i, a, b}
⊢ ¬k = i ∧ ¬k = a ∧ ¬k = b

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

Premises used: Finset.mem_singleton, Finset.mem_insert, not_or
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : card (α := Fin (n + 1)) {i, a, b} ≤ n
k : Fin (n + 1)
hk : ¬k = i ∧ ¬k = a ∧ ¬k = b
simp : ∃ (i_1 : Fin (n + 1)), ¬i_1 = i ∧ ∀ (i : Fin 2), ¬(stdSimplex.edge n a b hab : (a : Fin 2) → Fin (n + 1)) i = i_1
⊢ Membership.mem (γ := Set (Δ[n] _⦋1⦌)) (Λ[n, i].obj (op ⦋1⦌)) (stdSimplex.edge n a b hab)

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 a b : Fin (n + 1)
hab : a ≤ b
H : card (α := Fin (n + 1)) {i, a, b} ≤ n
k : Fin (n + 1)
hk : ¬k = i ∧ ¬k = a ∧ ¬k = b
⊢ ∃ (i_1 : Fin (n + 1)), ¬i_1 = i ∧ ∀ (i : Fin 2), ¬(stdSimplex.edge n a b hab : (a : Fin 2) → Fin (n + 1)) i = i_1

Tactic:
⟨k, hk.1, fun a ↦ ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : card (α := Fin (n + 1)) {i, a, b} ≤ n
k : Fin (n + 1)
hk : ¬k = i ∧ ¬k = a ∧ ¬k = b
refine : ∀ (a_1 : Fin 2), ¬(stdSimplex.edge n a b hab : (a : Fin 2) → Fin (n + 1)) a_1 = k
⊢ ∃ (i_1 : Fin (n + 1)), ¬i_1 = i ∧ ∀ (i : Fin 2), ¬(stdSimplex.edge n a b hab : (a : Fin 2) → Fin (n + 1)) i = i_1

Tactic:
refine ⟨k, hk.1, fun a ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i a_1 b : Fin (n + 1)
hab : a_1 ≤ b
H : card (α := Fin (n + 1)) {i, a_1, b} ≤ n
k : Fin (n + 1)
hk : ¬k = i ∧ ¬k = a_1 ∧ ¬k = b
a : Fin 2
0 : ¬(stdSimplex.edge n a_1 b hab : (a : Fin 2) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) = k
1 : ¬(stdSimplex.edge n a_1 b hab : (a : Fin 2) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩) = k
⊢ ¬(stdSimplex.edge n a_1 b hab : (a : Fin 2) → Fin (n + 1)) a = k

Tactic:
fin_cases a
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : card (α := Fin (n + 1)) {i, a, b} ≤ n
k : Fin (n + 1)
hk : ¬k = i ∧ ¬k = a ∧ ¬k = b
⊢ ¬(stdSimplex.edge n a b hab : (a : Fin 2) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) = k

Tactic:
Ne.symm hk.2.1

Premises used: Ne.symm, And.right, And.left
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : card (α := Fin (n + 1)) {i, a, b} ≤ n
k : Fin (n + 1)
hk : ¬k = i ∧ ¬k = a ∧ ¬k = b
⊢ ¬(stdSimplex.edge n a b hab : (a : Fin 2) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) = k

Tactic:
exact Ne.symm hk.2.1

Premises used: Ne.symm, And.right, And.left
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : card (α := Fin (n + 1)) {i, a, b} ≤ n
k : Fin (n + 1)
hk : ¬k = i ∧ ¬k = a ∧ ¬k = b
⊢ ¬(stdSimplex.edge n a b hab : (a : Fin 2) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩) = k

Tactic:
Ne.symm hk.2.2

Premises used: Ne.symm, And.right
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : card (α := Fin (n + 1)) {i, a, b} ≤ n
k : Fin (n + 1)
hk : ¬k = i ∧ ¬k = a ∧ ¬k = b
⊢ ¬(stdSimplex.edge n a b hab : (a : Fin 2) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩) = k

Tactic:
exact Ne.symm hk.2.2

Premises used: Ne.symm, And.right
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
h₀ : 0 < i
hₙ : i < Fin.last n
j : Fin n
refine_1 : j.castSucc ≤ j.succ
refine_2 : card (α := Fin (n + 1)) {i, j.castSucc, j.succ} ≤ n
⊢ Λ[n, i].toSSet _⦋1⦌

Tactic:
refine edge n i j.castSucc j.succ ?_ ?_

Premises used: Fin.succ, SSet.horn.edge, Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
h₀ : 0 < i
hₙ : i < Fin.last n
j : Fin n
⊢ j.castSucc ≤ j.succ

Tactic:
simp only [← Fin.val_fin_le, Fin.val_castSucc, Fin.val_succ, le_add_iff_nonneg_right, zero_le]

Premises used: zero_le, le_add_iff_nonneg_right, Fin.val_succ, Fin.val_castSucc, Fin.val_fin_le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
h₀ : 0 < i
hₙ : i < Fin.last n
j : Fin n
⊢ 0 < (↑i : ℕ)

Tactic:
simp only [← Fin.val_fin_lt, Fin.val_zero, Fin.val_last] at h₀ hₙ

Premises used: Fin.val_fin_lt, Fin.val_zero, Fin.val_last
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
h₀ : 0 < i
hₙ : i < Fin.last n
j : Fin n
h₁ : 0 < (↑i : ℕ)
⊢ (↑i : ℕ) < n

Tactic:
simp only [← Fin.val_fin_lt, Fin.val_zero, Fin.val_last] at h₀ hₙ

Premises used: Fin.val_fin_lt, Fin.val_zero, Fin.val_last