awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}
k : Fin (n + 3)
hk : ¬k = i ∧ ¬k = (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0
⊢ ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) = k

Tactic:
Ne.symm hk.2

Premises used: Ne.symm, And.right
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}
k : Fin (n + 3)
hk : ¬k = i ∧ ¬k = (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0
⊢ ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) = k

Tactic:
exact Ne.symm hk.2

Premises used: Ne.symm, And.right
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
h₁ :
  ∀ (x : Δ[n] _⦋m⦌),
    Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Λ[n, i].obj (op ⦋m⦌)) x ↔ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) Set.univ x
⊢ Eq (α := Set (Δ[n] _⦋m⦌)) (Λ[n, i].obj (op ⦋m⦌)) Set.univ

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
x : Δ[n] _⦋m⦌
h₁ :
  ∀ (f : unop (op ⦋m⦌) ⟶ ⦋n⦌),
    Membership.mem (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (Λ[n, i].obj (op ⦋m⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌) ↔
      Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) Set.univ
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌)
⊢ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Λ[n, i].obj (op ⦋m⦌)) x ↔ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) Set.univ x

Tactic:
obtain ⟨f, rfl⟩ := stdSimplex.objEquiv.symm.surjective x

Premises used: Equiv.surjective, Equiv.symm, SSet.stdSimplex.objEquiv, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
by_contra! :
  ∀
    (this :
      ∀ (j : Fin (n + 1)) (_ : j ≠ i),
        Membership.mem (γ := Set (Fin (⦋n⦌.len + 1)))
          (Set.range (ι := Fin ((unop (op ⦋m⦌)).len + 1))
            (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)))
          j),
    False
⊢ ∃ (j : Fin (n + 1)),
    j ≠ i ∧
      j ∉
        Set.range (ι := Fin ((unop (op ⦋m⦌)).len + 1))
          (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))

Tactic:
by_contra!
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this :
  ∀ (j : Fin (n + 1)) (_ : j ≠ i),
    Membership.mem (γ := Set (Fin (⦋n⦌.len + 1)))
      (Set.range (ι := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)))
      j
h₁ :
  ∀ (k : Fin (⦋n⦌.len + 1)),
    Membership.mem (γ := Finset (Fin (⦋n⦌.len + 1)))
        (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
            (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) ⊤ ∪
          {i})
        k ↔
      Membership.mem (γ := Finset (Fin (⦋n⦌.len + 1))) ⊤ k
⊢ Eq (α := Finset (Fin (⦋n⦌.len + 1)))
    (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) ⊤ ∪
      {i})
    ⊤

Tactic:
ext k
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this :
  ∀ (j : Fin (n + 1)) (_ : j ≠ i),
    Membership.mem (γ := Set (Fin (⦋n⦌.len + 1)))
      (Set.range (ι := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)))
      j
k : Fin (⦋n⦌.len + 1)
pos :
  k = i →
    (Membership.mem (γ := Finset (Fin (⦋n⦌.len + 1)))
        (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
            (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) ⊤ ∪
          {i})
        k ↔
      Membership.mem (γ := Finset (Fin (⦋n⦌.len + 1))) ⊤ k)
neg :
  ¬k = i →
    (Membership.mem (γ := Finset (Fin (⦋n⦌.len + 1)))
        (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
            (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) ⊤ ∪
          {i})
        k ↔
      Membership.mem (γ := Finset (Fin (⦋n⦌.len + 1))) ⊤ k)
⊢ Membership.mem (γ := Finset (Fin (⦋n⦌.len + 1)))
      (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
          (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) ⊤ ∪
        {i})
      k ↔
    Membership.mem (γ := Finset (Fin (⦋n⦌.len + 1))) ⊤ k

Tactic:
by_cases k = i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this :
  ∀ (j : Fin (n + 1)) (_ : j ≠ i),
    Membership.mem (γ := Set (Fin (⦋n⦌.len + 1)))
      (Set.range (ι := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)))
      j
k : Fin (⦋n⦌.len + 1)
h_1 : k = i
⊢ Membership.mem (γ := Finset (Fin (⦋n⦌.len + 1)))
      (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
          (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) ⊤ ∪
        {i})
      k ↔
    Membership.mem (γ := Finset (Fin (⦋n⦌.len + 1))) ⊤ k

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this :
  ∀ (j : Fin (n + 1)) (_ : j ≠ i),
    Membership.mem (γ := Set (Fin (⦋n⦌.len + 1)))
      (Set.range (ι := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)))
      j
k : Fin (⦋n⦌.len + 1)
h_1 : ¬k = i
⊢ Membership.mem (γ := Finset (Fin (⦋n⦌.len + 1)))
      (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
          (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) ⊤ ∪
        {i})
      k ↔
    Membership.mem (γ := Finset (Fin (⦋n⦌.len + 1))) ⊤ k

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this :
  ∀ (j : Fin (n + 1)) (_ : j ≠ i),
    Membership.mem (γ := Set (Fin (⦋n⦌.len + 1)))
      (Set.range (ι := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)))
      j
⊢ Eq (α := Finset (Fin (⦋n⦌.len + 1)))
    (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) ⊤ ∪
      {i})
    ⊤

Tactic:
have : Finset.image f.toOrderHom ⊤ ∪ {i} = ⊤ := by ext k; by_cases k = i <;> aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this_1 :
  ∀ (j : Fin (n + 1)) (_ : j ≠ i),
    Membership.mem (γ := Set (Fin (⦋n⦌.len + 1)))
      (Set.range (ι := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)))
      j
this :
  Eq (α := Finset (Fin (⦋n⦌.len + 1)))
    (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) ⊤ ∪
      {i})
    ⊤
⊢ Finset.card (α := Fin (⦋n⦌.len + 1)) ⊤ ≤
    Finset.card (α := Fin (⦋n⦌.len + 1))
        (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
          (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) ⊤) +
      Finset.card (α := Fin (⦋n⦌.len + 1)) {i}

Tactic:
have := (congr_arg Finset.card this).symm.le.trans (Finset.card_union_le _ _)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this_1 :
  ∀ (j : Fin (n + 1)) (_ : j ≠ i),
    Membership.mem (γ := Set (Fin (⦋n⦌.len + 1)))
      (Set.range (ι := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)))
      j
this_2 :
  Eq (α := Finset (Fin (⦋n⦌.len + 1)))
    (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) ⊤ ∪
      {i})
    ⊤
this :
  Finset.card (α := Fin (⦋n⦌.len + 1)) ⊤ ≤
    Finset.card (α := Fin (⦋n⦌.len + 1))
        (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
          (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) ⊤) +
      Finset.card (α := Fin (⦋n⦌.len + 1)) {i}
⊢ n ≤
    Finset.card (α := Fin (n + 1))
      (Finset.image (α := Fin (m + 1)) (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (m + 1)) → Fin (n + 1))
        Finset.univ)

Tactic:
simp only [SimplexCategory.len_mk, Finset.top_eq_univ, Finset.card_univ, Fintype.card_fin,
      Finset.card_singleton, add_le_add_iff_right] at this

Premises used: Finset.card_univ, SimplexCategory.len_mk, Fintype.card_fin, Finset.top_eq_univ, add_le_add_iff_right, Finset.card_singleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this_1 :
  ∀ (j : Fin (n + 1)) (_ : j ≠ i),
    Membership.mem (γ := Set (Fin (⦋n⦌.len + 1)))
      (Set.range (ι := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)))
      j
this_2 :
  Eq (α := Finset (Fin (⦋n⦌.len + 1)))
    (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) ⊤ ∪
      {i})
    ⊤
this :
  n ≤
    Finset.card (α := Fin (n + 1))
      (Finset.image (α := Fin (m + 1)) (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (m + 1)) → Fin (n + 1))
        Finset.univ)
⊢ n ≤ m + 1

Tactic:
simpa using this.trans Finset.card_image_le

Premises used: Finset.card_image_le, LE.le.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this_1 :
  ∀ (j : Fin (n + 1)) (_ : j ≠ i),
    Membership.mem (γ := Set (Fin (⦋n⦌.len + 1)))
      (Set.range (ι := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)))
      j
this_2 :
  Eq (α := Finset (Fin (⦋n⦌.len + 1)))
    (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) ⊤ ∪
      {i})
    ⊤
this :
  n ≤
    Finset.card (α := Fin (n + 1))
      (Finset.image (α := Fin (m + 1)) (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (m + 1)) → Fin (n + 1))
        Finset.univ)
⊢ n ≤ m + 1

Tactic:
have : n ≤ m + 1 := by simpa using this.trans Finset.card_image_le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this_1 :
  ∀ (j : Fin (n + 1)) (_ : j ≠ i),
    Membership.mem (γ := Set (Fin (⦋n⦌.len + 1)))
      (Set.range (ι := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)))
      j
this_2 :
  Eq (α := Finset (Fin (⦋n⦌.len + 1)))
    (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) ⊤ ∪
      {i})
    ⊤
this_3 :
  n ≤
    Finset.card (α := Fin (n + 1))
      (Finset.image (α := Fin (m + 1)) (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (m + 1)) → Fin (n + 1))
        Finset.univ)
this : n ≤ m + 1
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁ :
  ∀ (j : Fin (n + 1)) (hij : j ≠ i)
    (hj :
      j ∉
        Set.range (ι := Fin ((unop (op ⦋m⦌)).len + 1))
          (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))),
    Membership.mem (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (Λ[n, i].obj (op ⦋m⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌) ↔
      Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) Set.univ
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌)
⊢ Membership.mem (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (Λ[n, i].obj (op ⦋m⦌))
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌) ↔
    Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) Set.univ
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌)

Tactic:
obtain ⟨j, hij, hj⟩ : ∃ (j : Fin (n + 1)), j ≠ i ∧ j ∉ Set.range f.toOrderHom := by
    by_contra!
    have : Finset.image f.toOrderHom ⊤ ∪ {i} = ⊤ := by ext k; by_cases k = i <;> aesop
    have := (congr_arg Finset.card this).symm.le.trans (Finset.card_union_le _ _)
    simp only [SimplexCategory.len_mk, Finset.top_eq_univ, Finset.card_univ, Fintype.card_fin,
      Finset.card_singleton, add_le_add_iff_right] at this
    have : n ≤ m + 1 := by simpa using this.trans Finset.card_image_le
    lia

Premises used: HAdd.hAdd, SimplexCategory.Hom.toOrderHom, Set.range, OfNat.ofNat, Fin, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
j : Fin (n + 1)
hij : j ≠ i
hj :
  j ∉
    Set.range (ι := Fin ((unop (op ⦋m⦌)).len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
⊢ ∃ (j : Fin (n + 1)),
    ¬j = i ∧
      ∀ (i : Fin (m + 1)),
        ¬(((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌) :
                (a : Fin (m + 1)) → Fin (n + 1))
              i =
            j

Tactic:
have : ∃ j, ¬j = i ∧ ∀ (i : Fin (m + 1)), ¬(stdSimplex.objEquiv.symm.{u} f) i = j :=
    ⟨j, hij, fun k hk ↦ hj ⟨k, hk⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
j : Fin (n + 1)
hij : j ≠ i
hj :
  j ∉
    Set.range (ι := Fin ((unop (op ⦋m⦌)).len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
this :
  ∃ (j : Fin (n + 1)),
    ¬j = i ∧
      ∀ (i : Fin (m + 1)),
        ¬(((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌) :
                (a : Fin (m + 1)) → Fin (n + 1))
              i =
            j
⊢ Membership.mem (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (Λ[n, i].obj (op ⦋m⦌))
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌) ↔
    Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) Set.univ
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌)

Tactic:
simpa [horn_eq_iSup] using this

Premises used: SSet.horn_eq_iSup
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
⊢ A ≤ Λ[n + 1, i] ↔ ¬stdSimplex.face {i}ᶜ ≤ A

Tactic:
⟨fun hA h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
refine_1 : ∀ (hA : A ≤ Λ[n + 1, i]) (h : stdSimplex.face {i}ᶜ ≤ A), False
refine_2 : ∀ (h : ¬stdSimplex.face {i}ᶜ ≤ A), A ≤ Λ[n + 1, i]
⊢ A ≤ Λ[n + 1, i] ↔ ¬stdSimplex.face {i}ᶜ ≤ A

Tactic:
refine ⟨fun hA h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
hA : A ≤ Λ[n + 1, i]
h : stdSimplex.face {i}ᶜ ≤ A
⊢ stdSimplex.face {i}ᶜ ≤ Λ[n + 1, i]

Tactic:
replace h := h.trans hA
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
hA : A ≤ Λ[n + 1, i]
h : stdSimplex.face {i}ᶜ ≤ Λ[n + 1, i]
⊢ Ne (α := Set (Fin (n + 1 + 1)))
    (Set.range (ι := Fin ((unop (op ⦋n⦌)).len + 1))
        (⇑(stdSimplex.asOrderHom.{u}
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌)
                (SimplexCategory.δ i))) :
          (a : Fin ((unop (op ⦋n⦌)).len + 1)) → Fin (n + 1 + 1)) ∪
      {i})
    Set.univ

Tactic:
rw [stdSimplex.face_singleton_compl, Subcomplex.ofSimplex_le_iff, mem_horn_iff] at h

Premises used: SSet.mem_horn_iff, SSet.Subcomplex.ofSimplex_le_iff, SSet.stdSimplex.face_singleton_compl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
hA : A ≤ Λ[n + 1, i]
h :
  Ne (α := Set (Fin (n + 1 + 1)))
    (Set.range (ι := Fin ((unop (op ⦋n⦌)).len + 1))
        (⇑(stdSimplex.asOrderHom.{u}
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌)
                (SimplexCategory.δ i))) :
          (a : Fin ((unop (op ⦋n⦌)).len + 1)) → Fin (n + 1 + 1)) ∪
      {i})
    Set.univ
refine_1 :
  Eq (α := Set (Fin (n + 1 + 1)))
    (Set.range (ι := Fin ((unop (op ⦋n⦌)).len + 1))
        (⇑(stdSimplex.asOrderHom.{u}
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌)
                (SimplexCategory.δ i))) :
          (a : Fin ((unop (op ⦋n⦌)).len + 1)) → Fin (n + 1 + 1)) ∪
      {i})
    Set.univ
⊢ False

Tactic:
apply h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
hA : A ≤ Λ[n + 1, i]
h :
  Ne (α := Set (Fin (n + 1 + 1)))
    (Set.range (ι := Fin ((unop (op ⦋n⦌)).len + 1))
        (⇑(stdSimplex.asOrderHom.{u}
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌)
                (SimplexCategory.δ i))) :
          (a : Fin ((unop (op ⦋n⦌)).len + 1)) → Fin (n + 1 + 1)) ∪
      {i})
    Set.univ
refine_1 :
  Eq (α := Set (Fin (n + 1 + 1)))
    (Set.range (ι := Fin ((unop (op ⦋n⦌)).len + 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)) (SimplexCategory.δ i)) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) →
            (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n + 1⦌) ∪
      {i})
    Set.univ
refine_1₁ : Set.range i.succAbove ∪ {i} = Set.univ
refine_1₂ : Eq (α := Set (Fin (n + 1 + 1))) ({i}ᶜ ∪ {i}) Set.univ
refine_1₃ refine_1₄ : Eq (α := Set (Fin (n + 1 + 1))) Set.univ Set.univ
⊢ Eq (α := Set (Fin (n + 1 + 1)))
    (Set.range (ι := Fin ((unop (op ⦋n⦌)).len + 1))
        (⇑(stdSimplex.asOrderHom.{u}
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌)
                (SimplexCategory.δ i))) :
          (a : Fin ((unop (op ⦋n⦌)).len + 1)) → Fin (n + 1 + 1)) ∪
      {i})
    Set.univ

Tactic:
rw [stdSimplex.coe_asOrderHom_objEquiv_symm, SimplexCategory.coe_δ,
      Fin.range_succAbove, Set.compl_union_self]

Premises used: SimplexCategory.coe_δ, Fin.range_succAbove, SSet.stdSimplex.coe_asOrderHom_objEquiv_symm, Set.compl_union_self
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
refine_2 :
  ∀ (n_1 : ℕ) (x : (↑(Δ[n + 1].nonDegenerate n_1) : Type u)),
    Membership.mem (γ := Set (Δ[n + 1] _⦋n_1⦌)) (A.obj (op ⦋n_1⦌)) (↑x : Δ[n + 1] _⦋n_1⦌) →
      Membership.mem (γ := Set (Δ[n + 1] _⦋n_1⦌)) (Λ[n + 1, i].obj (op ⦋n_1⦌)) (↑x : Δ[n + 1] _⦋n_1⦌)
⊢ A ≤ Λ[n + 1, i]

Tactic:
rw [Subcomplex.le_iff_contains_nonDegenerate]

Premises used: SSet.Subcomplex.le_iff_contains_nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
x : (↑(Δ[n + 1].nonDegenerate d) : Type u)
hx : Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (A.obj (op ⦋d⦌)) (↑x : Δ[n + 1] _⦋d⦌)
pos : ∀ (hd : d < n), Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (Λ[n + 1, i].obj (op ⦋d⦌)) (↑x : Δ[n + 1] _⦋d⦌)
neg : ∀ (hd : n ≤ d), Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (Λ[n + 1, i].obj (op ⦋d⦌)) (↑x : Δ[n + 1] _⦋d⦌)
⊢ Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (Λ[n + 1, i].obj (op ⦋d⦌)) (↑x : Δ[n + 1] _⦋d⦌)

Tactic:
by_cases! hd : d < n
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
x : (↑(Δ[n + 1].nonDegenerate d) : Type u)
hx : Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (A.obj (op ⦋d⦌)) (↑x : Δ[n + 1] _⦋d⦌)
hd : d < n
⊢ Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (Λ[n + 1, i].obj (op ⦋d⦌)) (↑x : Δ[n + 1] _⦋d⦌)

Tactic:
simp [horn_obj_eq_univ i d]

Premises used: SSet.horn_obj_eq_univ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
x : (↑(Δ[n + 1].nonDegenerate d) : Type u)
hx : Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (A.obj (op ⦋d⦌)) (↑x : Δ[n + 1] _⦋d⦌)
hd : n ≤ d
neg :
  ∀ (S : Finset (Fin (n + 1 + 1)))
    (hS : Membership.mem (γ := Set (Finset (Fin (n + 1 + 1)))) {S : Finset (Fin (n + 1 + 1)) | S.card = d + 1} S)
    (hx :
      Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (A.obj (op ⦋d⦌))
        (↑((Equiv.symm stdSimplex.nonDegenerateEquiv' :
                (a : (↑{S : Finset (Fin (n + 1 + 1)) | S.card = d + 1} : Type)) →
                  (↑(Δ[n + 1].nonDegenerate d) : Type u))
              (Subtype.mk (p := fun (x : Finset (Fin (n + 1 + 1))) ↦
                Membership.mem (γ := Set (Finset (Fin (n + 1 + 1)))) {S : Finset (Fin (n + 1 + 1)) | S.card = d + 1} x)
                S hS)) :
          Δ[n + 1] _⦋d⦌)),
    Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (Λ[n + 1, i].obj (op ⦋d⦌))
      (↑((Equiv.symm stdSimplex.nonDegenerateEquiv' :
              (a : (↑{S : Finset (Fin (n + 1 + 1)) | S.card = d + 1} : Type)) → (↑(Δ[n + 1].nonDegenerate d) : Type u))
            (Subtype.mk (p := fun (x : Finset (Fin (n + 1 + 1))) ↦
              Membership.mem (γ := Set (Finset (Fin (n + 1 + 1)))) {S : Finset (Fin (n + 1 + 1)) | S.card = d + 1} x) S
              hS)) :
        Δ[n + 1] _⦋d⦌)
⊢ Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (Λ[n + 1, i].obj (op ⦋d⦌)) (↑x : Δ[n + 1] _⦋d⦌)

Tactic:
obtain ⟨⟨S, hS⟩, rfl⟩ := stdSimplex.nonDegenerateEquiv'.symm.surjective x

Premises used: SSet.S, SSet.stdSimplex.nonDegenerateEquiv', Equiv.surjective, Equiv.symm, rfl
-- 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 :
  Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (A.obj (op ⦋d⦌))
    (↑((Equiv.symm stdSimplex.nonDegenerateEquiv' :
            (a : (↑{S : Finset (Fin (n + 1 + 1)) | S.card = d + 1} : Type)) → (↑(Δ[n + 1].nonDegenerate d) : Type u))
          (Subtype.mk (p := fun (x : Finset (Fin (n + 1 + 1))) ↦
            Membership.mem (γ := Set (Finset (Fin (n + 1 + 1)))) {S : Finset (Fin (n + 1 + 1)) | S.card = d + 1} x) S
            hS)) :
      Δ[n + 1] _⦋d⦌)
neg : ∀ (hx : stdSimplex.face S ≤ A), stdSimplex.face S ≤ Λ[n + 1, i]
⊢ Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (Λ[n + 1, i].obj (op ⦋d⦌))
    (↑((Equiv.symm stdSimplex.nonDegenerateEquiv' :
            (a : (↑{S : Finset (Fin (n + 1 + 1)) | S.card = d + 1} : Type)) → (↑(Δ[n + 1].nonDegenerate d) : Type u))
          (Subtype.mk (p := fun (x : Finset (Fin (n + 1 + 1))) ↦
            Membership.mem (γ := Set (Finset (Fin (n + 1 + 1)))) {S : Finset (Fin (n + 1 + 1)) | S.card = d + 1} x) S
            hS)) :
      Δ[n + 1] _⦋d⦌)

Tactic:
simp only [stdSimplex.nonDegenerateEquiv'_symm_mem_iff_face_le] at hx ⊢

Premises used: SSet.stdSimplex.nonDegenerateEquiv'_symm_mem_iff_face_le