awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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}
hS : ∃ (x : Fin (n + 3)), x ∉ S
⊢ ∃ (i_1 : Fin (n + 2 + 1)), ¬i_1 = i ∧ ∀ (i : Fin 1), ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) i = i_1
have h : ∀ (k : Fin (n + 3)) (hk : k ∉ S),
  ∃ (i_1 : Fin (n + 2 + 1)), ¬i_1 = i ∧ ∀ (i : Fin 1), ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) i = i_1
Tactic: obtain ⟨k, hk⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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 ∉ S
⊢ ∃ (i_1 : Fin (n + 2 + 1)), ¬i_1 = i ∧ ∀ (i : Fin 1), ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) i = i_1
have hk₁ : ¬k = i ∧ ¬k = (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0
Tactic: simp only [Finset.mem_insert, Finset.mem_singleton, not_or, S] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ ∃ (i_1 : Fin (n + 2 + 1)), ¬i_1 = i ∧ ∀ (i : Fin 1), ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) i = i_1
have h : ∀ (a : Fin 1), ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) a = k
Tactic: refine ⟨k, hk.1, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
a : Fin 1
⊢ ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) a = k
have h : ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) ((fun (i : Fin (⦋0⦌.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 : Fin (n + 1)
m : ℕ
h : m + 1 < n
⊢ Eq (α := Set (Δ[n] _⦋m⦌)) (Λ[n, i].obj (op ⦋m⦌)) Set.univ
have h₁ : ∀ (x : Δ[n] _⦋m⦌),
  Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Λ[n, i].obj (op ⦋m⦌)) x ↔ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) Set.univ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
x : Δ[n] _⦋m⦌
⊢ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Λ[n, i].obj (op ⦋m⦌)) x ↔ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) Set.univ x
have 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⦌)
Tactic: obtain ⟨f, rfl⟩ := stdSimplex.objEquiv.symm.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ ∃ (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))
have 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
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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})
    ⊤
have 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
Tactic: ext k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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)
⊢ 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
have 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)
Tactic: by_cases k = i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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)
⊢ 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
have 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)
Tactic: by_cases k = i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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
⊢ False
have 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})
  ⊤
Tactic: have : Finset.image f.toOrderHom ⊤ ∪ {i} = ⊤ := by ext k; by_cases k = i <;> aesop
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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})
    ⊤
⊢ False
have 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}
Tactic: have := (congr_arg Finset.card this).symm.le.trans (Finset.card_union_le _ _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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}
⊢ False
have 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)
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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)
⊢ False
have this₁ : n ≤ m + 1
Tactic: have : n ≤ m + 1 := by simpa using this.trans Finset.card_image_le
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
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⦌)
have 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⦌)
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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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))
⊢ 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⦌)
have 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
Tactic: have : ∃ j, ¬j = i ∧ ∀ (i : Fin (m + 1)), ¬(stdSimplex.objEquiv.symm.{u} f) i = j :=
    ⟨j, hij, fun k hk ↦ hj ⟨k, hk⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
⊢ A ≤ Λ[n + 1, i] ↔ ¬stdSimplex.face {i}ᶜ ≤ A
have refine_1 : ∀ (hA : A ≤ Λ[n + 1, i]) (h : stdSimplex.face {i}ᶜ ≤ A), False
Tactic: refine ⟨fun hA h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
refine_1 : ∀ (hA : A ≤ Λ[n + 1, i]) (h : stdSimplex.face {i}ᶜ ≤ A), False
⊢ A ≤ Λ[n + 1, i] ↔ ¬stdSimplex.face {i}ᶜ ≤ A
have refine_2 : ∀ (h : ¬stdSimplex.face {i}ᶜ ≤ A), A ≤ Λ[n + 1, i]
Tactic: refine ⟨fun hA h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
hA : A ≤ Λ[n + 1, i]
h : stdSimplex.face {i}ᶜ ≤ A
⊢ False
have h₁ : stdSimplex.face {i}ᶜ ≤ Λ[n + 1, i]
Tactic: replace h := h.trans hA
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
hA : A ≤ Λ[n + 1, i]
h : stdSimplex.face {i}ᶜ ≤ Λ[n + 1, i]
⊢ False
have 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
Tactic: rw [stdSimplex.face_singleton_compl, Subcomplex.ofSimplex_le_iff, mem_horn_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ False
have 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
Tactic: apply h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ 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
have 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
Tactic: rw [stdSimplex.coe_asOrderHom_objEquiv_symm, SimplexCategory.coe_δ,
      Fin.range_succAbove, Set.compl_union_self]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ 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
have refine_1₁ : Set.range i.succAbove ∪ {i} = Set.univ
Tactic: rw [stdSimplex.coe_asOrderHom_objEquiv_symm, SimplexCategory.coe_δ,
      Fin.range_succAbove, Set.compl_union_self]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ 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
have refine_1₂ : Eq (α := Set (Fin (n + 1 + 1))) ({i}ᶜ ∪ {i}) Set.univ
Tactic: rw [stdSimplex.coe_asOrderHom_objEquiv_symm, SimplexCategory.coe_δ,
      Fin.range_succAbove, Set.compl_union_self]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ 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
have refine_1₃ : Eq (α := Set (Fin (n + 1 + 1))) Set.univ Set.univ
Tactic: rw [stdSimplex.coe_asOrderHom_objEquiv_symm, SimplexCategory.coe_δ,
      Fin.range_succAbove, Set.compl_union_self]
-- 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
⊢ A ≤ Λ[n + 1, i]
have 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⦌)
Tactic: rw [Subcomplex.le_iff_contains_nonDegenerate]
-- 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⦌)
⊢ Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (Λ[n + 1, i].obj (op ⦋d⦌)) (↑x : Δ[n + 1] _⦋d⦌)
have pos : ∀ (hd : d < n), Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (Λ[n + 1, i].obj (op ⦋d⦌)) (↑x : Δ[n + 1] _⦋d⦌)
Tactic: by_cases! hd : d < n
-- 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⦌)
pos : ∀ (hd : d < n), 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⦌)
have neg : ∀ (hd : n ≤ d), Membership.mem (γ := Set (Δ[n + 1] _⦋d⦌)) (Λ[n + 1, i].obj (op ⦋d⦌)) (↑x : Δ[n + 1] _⦋d⦌)
Tactic: by_cases! hd : d < n