awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (Λ[n + 1, i].obj (op ⦋d⦌)) (↑x : Δ[n + 1] _⦋d⦌)
have 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⦌)
Tactic: obtain ⟨⟨S, hS⟩, rfl⟩ := stdSimplex.nonDegenerateEquiv'.symm.surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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⦌)
⊢ 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⦌)
have neg : ∀ (hx : stdSimplex.face S ≤ A), stdSimplex.face S ≤ Λ[n + 1, i]
Tactic: simp only [stdSimplex.nonDegenerateEquiv'_symm_mem_iff_face_le] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ stdSimplex.face S ≤ Λ[n + 1, i]
have neg : ∀ (hd : n < d), stdSimplex.face S ≤ Λ[n + 1, i]
Tactic: obtain hd | rfl := hd.lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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]
⊢ stdSimplex.face S ≤ Λ[n + 1, i]
have neg₁ : ∀ (hd : n ≤ n) (hS : S.card = n + 1), stdSimplex.face S ≤ Λ[n + 1, i]
Tactic: obtain hd | rfl := hd.lt_or_eq
Cleared hypotheses: d, hd, hS
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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 = Finset.univ
have rw : S.card = n + 1 + 1
Tactic: rw [← Finset.card_eq_iff_eq_univ, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ stdSimplex.face S ≤ Λ[n + 1, i]
have 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]
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)
Cleared hypotheses: S, hS, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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
have this : Sᶜ.card + S.card = Fintype.card (Fin (n + 1 + 1))
Tactic: have := S.card_compl_add_card
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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 = 1
have this₁ : Sᶜ.card + S.card = n + 1 + 1
Tactic: rw [Fintype.card_fin] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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
⊢ stdSimplex.face S ≤ Λ[n + 1, i]
have hS₁ : Sᶜ.card = 1
Tactic: replace hS : Sᶜ.card = 1 := by
          have := S.card_compl_add_card
          rw [Fintype.card_fin] at this
          lia
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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
⊢ ∃ (j : Fin (n + 1 + 1)), S = {j}ᶜ
have hS₁ : ∃ (a : Fin (n + 1 + 1)), Sᶜ = {a}
Tactic: rw [Finset.card_eq_one] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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}
⊢ ∃ (j : Fin (n + 1 + 1)), S = {j}ᶜ
have obtain : ∀ (j : Fin (n + 1 + 1)) (hS : Sᶜ = {j}), ∃ (j : Fin (n + 1 + 1)), S = {j}ᶜ
Tactic: obtain ⟨j, hS⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ stdSimplex.face S ≤ Λ[n + 1, i]
have 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]
Tactic: obtain ⟨j, rfl⟩ : ∃ j, S = {j}ᶜ := by
          rw [Finset.card_eq_one] at hS
          obtain ⟨j, hS⟩ := hS
          exact ⟨j, by simp [← hS]⟩
Cleared hypotheses: S, hx, hS
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
⊢ stdSimplex.face S ≤ Λ[n + 1, j] ↔ S ≠ Finset.univ ∧ S ≠ {j}ᶜ
have rw : ¬¬{j}ᶜ ≤ S ↔ ¬(S ≠ Finset.univ ∧ S ≠ {j}ᶜ)
Tactic: rw [subcomplex_le_horn_iff, stdSimplex.face_le_face_iff, ← not_iff_not]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
⊢ ¬¬{j}ᶜ ≤ S ↔ ¬(S ≠ Finset.univ ∧ S ≠ {j}ᶜ)
have simp : {j}ᶜ ⊆ S ↔ S = Finset.univ ∨ S = {j}ᶜ
Tactic: simp only [Finset.le_eq_subset, Decidable.not_not, ne_eq, not_and_or]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
⊢ {j}ᶜ ⊆ S ↔ S = Finset.univ ∨ S = {j}ᶜ
have refine : ∀ (h : {j}ᶜ ⊆ S), S = Finset.univ ∨ S = {j}ᶜ
Tactic: refine ⟨fun h ↦ ?_, by aesop⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
h : {j}ᶜ ⊆ S
⊢ S = Finset.univ ∨ S = {j}ᶜ
have h₁ : S = Finset.univ ∨ Sᶜ = {j}
Tactic: rw [← Finset.compl_subset_compl, compl_compl,
    Finset.subset_singleton_iff, Finset.compl_eq_empty_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 1)
d : SimplexCategory
f : d ⟶ ⦋n⦌
inst : IsIso f
⊢ ((Equiv.symm stdSimplex.objEquiv : (a : unop (op d) ⟶ ⦋n⦌) → Δ[n].obj (op d)) f : Δ[n].obj (op d)) ∉
    Λ[n, i].obj (op d)
have 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
Tactic: rw [mem_horn_iff, ne_eq, not_not]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 1)
d : SimplexCategory
f : d ⟶ ⦋n⦌
inst : IsIso f
⊢ 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
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
⊢ 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
have rw : Ne (α := Finset (Fin (n + 2))) {i}ᶜ Finset.univ ∧ Ne (α := Finset (Fin (n + 2))) {i}ᶜ {j}ᶜ ↔ ¬i = j
Tactic: rw [← Subcomplex.ofSimplex_le_iff, ← stdSimplex.face_singleton_compl, face_le_horn_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ Λ[n, i].op.preimage (Iso.inv (stdSimplex.opIso ⦋n⦌)) = Λ[n, i.rev]
have 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
Tactic: ext ⟨⟨d⟩⟩ j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 1)
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
have 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
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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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
⊢ False
have this : card (α := Fin (n + 1)) univ ≤ card (α := Fin (n + 1)) {i, a, b}
Tactic: have := Finset.card_le_card hS.symm.le
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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}
⊢ False
have this₁ : n + 1 ≤ card (α := Fin (n + 1)) {i, a, b}
Tactic: simp only [card_univ, Fintype.card_fin] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : card (α := Fin (n + 1)) {i, a, b} ≤ n
⊢ Membership.mem (γ := Set (Δ[n] _⦋1⦌)) (Λ[n, i].obj (op ⦋1⦌)) (stdSimplex.edge n a b hab)
have hS : ¬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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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
⊢ Membership.mem (γ := Set (Δ[n] _⦋1⦌)) (Λ[n, i].obj (op ⦋1⦌)) (stdSimplex.edge n a b hab)
have hS₁ : ∃ (x : Fin (n + 1)), x ∉ {i, a, b}
Tactic: rw [Finset.eq_univ_iff_forall, not_forall] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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}
⊢ Membership.mem (γ := Set (Δ[n] _⦋1⦌)) (Λ[n, i].obj (op ⦋1⦌)) (stdSimplex.edge n a b hab)
have 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)
Tactic: obtain ⟨k, hk⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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}
⊢ Membership.mem (γ := Set (Δ[n] _⦋1⦌)) (Λ[n, i].obj (op ⦋1⦌)) (stdSimplex.edge n a b hab)
have hk₁ : ¬k = i ∧ ¬k = a ∧ ¬k = b
Tactic: simp only [mem_insert, mem_singleton, not_or] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ Membership.mem (γ := Set (Δ[n] _⦋1⦌)) (Λ[n, i].obj (op ⦋1⦌)) (stdSimplex.edge n a b hab)
have 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
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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
have refine : ∀ (a_1 : Fin 2), ¬(stdSimplex.edge n a b hab : (a : Fin 2) → Fin (n + 1)) a_1 = k
Tactic: refine ⟨k, hk.1, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ ¬(stdSimplex.edge n a_1 b hab : (a : Fin 2) → Fin (n + 1)) a = k
have 0 : ¬(stdSimplex.edge n a_1 b hab : (a : Fin 2) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, sorry⟩) = k
Tactic: fin_cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ ¬(stdSimplex.edge n a_1 b hab : (a : Fin 2) → Fin (n + 1)) a = k
have 1 : ¬(stdSimplex.edge n a_1 b hab : (a : Fin 2) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, sorry⟩) = k
Tactic: fin_cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 1)
h₀ : 0 < i
hₙ : i < Fin.last n
j : Fin n
⊢ Λ[n, i].toSSet _⦋1⦌
have refine_1 : j.castSucc ≤ j.succ
Tactic: refine edge n i j.castSucc j.succ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 1)
h₀ : 0 < i
hₙ : i < Fin.last n
j : Fin n
refine_1 : j.castSucc ≤ j.succ
⊢ Λ[n, i].toSSet _⦋1⦌
have refine_2 : card (α := Fin (n + 1)) {i, j.castSucc, j.succ} ≤ n
Tactic: refine edge n i j.castSucc j.succ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n : ℕ
i : Fin (n + 1)
h₀ : 0 < i
hₙ : i < Fin.last n
j : Fin n
⊢ card (α := Fin (n + 1)) {i, j.castSucc, j.succ} ≤ n
have h₁ : 0 < (↑i : ℕ)
Tactic: simp only [← Fin.val_fin_lt, Fin.val_zero, Fin.val_last] at h₀ hₙ
Cleared hypotheses: h₀, hₙ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n : ℕ
i : Fin (n + 1)
h₀ : 0 < i
hₙ : i < Fin.last n
j : Fin n
h₁ : 0 < (↑i : ℕ)
⊢ card (α := Fin (n + 1)) {i, j.castSucc, j.succ} ≤ n
have hₙ₁ : (↑i : ℕ) < n
Tactic: simp only [← Fin.val_fin_lt, Fin.val_zero, Fin.val_last] at h₀ hₙ
Cleared hypotheses: h₀, hₙ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < (↑i : ℕ)
hₙ : (↑i : ℕ) < n
⊢ n = 2 ∨ 2 < n
have rw : 2 ≤ n
Tactic: rw [eq_comm, or_comm, ← le_iff_lt_or_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < (↑i : ℕ)
hₙ : (↑i : ℕ) < n
⊢ card (α := Fin (n + 1)) {i, j.castSucc, j.succ} ≤ n
have 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
Tactic: obtain rfl | hn : n = 2 ∨ 2 < n := by
    rw [eq_comm, or_comm, ← le_iff_lt_or_eq]; lia
Cleared hypotheses: n, i, j, h₀, hₙ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ card (α := Fin (n + 1)) {i, j.castSucc, j.succ} ≤ n
have refine_2₁ : ∀ (hn : 2 < 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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
have 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
Tactic: revert i j
Cleared hypotheses: i, j, h₀, hₙ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ Λ[n + 3, i].toSSet _⦋2⦌
have refine_1 : (⟨k, sorry⟩ : Fin (n + 3 + 1)) ≤ ⟨k + 1, sorry⟩
Tactic: refine ⟨stdSimplex.triangle
    (n := n+3) ⟨k, by lia⟩ ⟨k+1, by lia⟩ ⟨k+2, by lia⟩ ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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, ⋯⟩
⊢ Λ[n + 3, i].toSSet _⦋2⦌
have refine_2 : (⟨k + 1, sorry⟩ : Fin (n + 3 + 1)) ≤ ⟨k + 2, sorry⟩
Tactic: refine ⟨stdSimplex.triangle
    (n := n+3) ⟨k, by lia⟩ ⟨k+1, by lia⟩ ⟨k+2, by lia⟩ ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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, ⋯⟩
⊢ Λ[n + 3, i].toSSet _⦋2⦌
have refine_3 : Membership.mem (γ := Set (Δ[n + 3] _⦋2⦌)) (Λ[n + 3, i].obj (op ⦋2⦌))
  (stdSimplex.triangle (⟨k, sorry⟩ : Fin (n + 3 + 1)) (⟨k + 1, sorry⟩ : Fin (n + 3 + 1)) (⟨k + 2, sorry⟩ : Fin (n + 3 + 1)) sorry sorry)
Tactic: refine ⟨stdSimplex.triangle
    (n := n+3) ⟨k, by lia⟩ ⟨k+1, by lia⟩ ⟨k+2, by lia⟩ ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ 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)) ⋯ ⋯)
have refine_3 : ∃ (i_1 : Fin (n + 3 + 1)),
  ¬i_1 = i ∧
    ∀ (i : Fin 3),
      ¬(stdSimplex.triangle (⟨k, sorry⟩ : Fin (n + 3 + 1)) (⟨k + 1, sorry⟩ : Fin (n + 3 + 1)) (⟨k + 2, sorry⟩ : Fin (n + 3 + 1)) sorry
                sorry :
              (a : Fin 3) → Fin (n + 3 + 1))
            i =
          i_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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ False
have 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, sorry⟩ : Fin (n + 4)), (⟨k + 1, sorry⟩ : Fin (n + 4)), (⟨k + 2, sorry⟩ : Fin (n + 4))} univ),
  False
Tactic: obtain ⟨i, hi⟩ := i
Cleared hypotheses: i, h₀, hₙ, hS