awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
⊢ False
have pos : ∀ (hk : k = 0), False
Tactic: by_cases hk : k = 0
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
pos : ∀ (hk : k = 0), False
⊢ False
have neg : ∀ (hk : ¬k = 0), False
Tactic: by_cases hk : k = 0
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
hk : k = 0
⊢ False
have h₁ : 0 < n + 2
Tactic: subst hk
Cleared hypotheses: k, h, hS, hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
hk : k = 0
h₁ : 0 < n + 2
⊢ False
have hS₁ : Eq (α := Finset (Fin (n + 4)))
  {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, sorry⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩ : Fin (n + 4)),
    (⟨HAdd.hAdd (α := ℕ) 0 2, sorry⟩ : Fin (n + 4))}
  univ
Tactic: subst hk
Cleared hypotheses: k, h, hS, hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
h : 0 < n + 2
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, ⋯⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 4)),
      (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (n + 4))}
    univ
⊢ False
have this : Membership.mem (γ := Finset (Fin (n + 3 + 1))) univ (Fin.last (n + 3))
Tactic: have := Finset.mem_univ (Fin.last _ : Fin (n + 4))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
h : 0 < n + 2
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, ⋯⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 4)),
      (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (n + 4))}
    univ
this : Membership.mem (γ := Finset (Fin (n + 3 + 1))) univ (Fin.last (n + 3))
⊢ False
have this₁ : Membership.mem (γ := Finset (Fin (n + 3 + 1)))
  {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, sorry⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩ : Fin (n + 4)),
    (⟨HAdd.hAdd (α := ℕ) 0 2, sorry⟩ : Fin (n + 4))}
  (Fin.last (n + 3))
Tactic: rw [← hS] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
h : 0 < n + 2
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, ⋯⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 4)),
      (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (n + 4))}
    univ
this :
  Membership.mem (γ := Finset (Fin (n + 3 + 1)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, ⋯⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 4)),
      (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (n + 4))}
    (Fin.last (n + 3))
⊢ False
have this₁ : n + 3 = i
Tactic: simp only [Fin.zero_eta, zero_add, Fin.mk_one, mem_insert, Fin.ext_iff, Fin.val_last,
        Fin.val_zero, AddLeftCancelMonoid.add_eq_zero, OfNat.ofNat_ne_zero, and_false,
        Fin.val_one, Nat.reduceEqDiff, mem_singleton, or_self, or_false] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
h : 0 < n + 2
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, ⋯⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 4)),
      (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (n + 4))}
    univ
this : n + 3 = i
⊢ False
have hₙ₁ : i < n + 3
Tactic: simp only [Fin.lt_def, Fin.val_last] at hₙ
Cleared hypotheses: hₙ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
hk : ¬k = 0
⊢ False
have this : Membership.mem (γ := Finset (Fin (n + 4))) univ 0
Tactic: have := Finset.mem_univ (0 : Fin (n + 4))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
hk : ¬k = 0
this : Membership.mem (γ := Finset (Fin (n + 4))) univ 0
⊢ False
have this₁ : Membership.mem (γ := 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))} 0
Tactic: rw [← hS] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
hk : ¬k = 0
this :
  Membership.mem (γ := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} 0
⊢ False
have this₁ : 0 = i ∨ 0 = k
Tactic: simp only [mem_insert, Fin.ext_iff, Fin.val_zero, right_eq_add,
        AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, mem_singleton,
        OfNat.ofNat_ne_zero, or_self, or_false] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
hk : ¬k = 0
this : 0 = i ∨ 0 = k
⊢ False
have neg : ∀ (hi : 0 < n + 4) (h₀ : 0 < (⟨0, hi⟩ : Fin (n + 4))) (hₙ : (⟨0, hi⟩ : Fin (n + 4)) < Fin.last (n + 3))
  (hS :
    Eq (α := Finset (Fin (n + 4)))
      {(⟨0, hi⟩ : Fin (n + 4)), (⟨k, sorry⟩ : Fin (n + 4)), (⟨k + 1, sorry⟩ : Fin (n + 4)), (⟨k + 2, sorry⟩ : Fin (n + 4))} univ),
  False
Tactic: obtain rfl | rfl := this
Cleared hypotheses: i, hi, h₀, hₙ, hS, this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < (⟨i, hi⟩ : Fin (n + 4))
hₙ : (⟨i, hi⟩ : Fin (n + 4)) < Fin.last (n + 3)
hS :
  Eq (α := Finset (Fin (n + 4)))
    {(⟨i, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ
hk : ¬k = 0
this : 0 = i ∨ 0 = k
neg :
  ∀ (hi : 0 < n + 4) (h₀ : 0 < (⟨0, hi⟩ : Fin (n + 4))) (hₙ : (⟨0, hi⟩ : Fin (n + 4)) < Fin.last (n + 3))
    (hS :
      Eq (α := Finset (Fin (n + 4)))
        {(⟨0, hi⟩ : Fin (n + 4)), (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))} univ),
    False
⊢ False
have neg₁ : ∀ (h : 0 < n + 2)
  (hS :
    Eq (α := Finset (Fin (n + 4)))
      {(⟨i, hi⟩ : Fin (n + 4)), (⟨0, sorry⟩ : Fin (n + 4)), (⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩ : Fin (n + 4)),
        (⟨HAdd.hAdd (α := ℕ) 0 2, sorry⟩ : Fin (n + 4))}
      univ)
  (hk : ¬Eq (α := ℕ) 0 0), False
Tactic: obtain rfl | rfl := this
Cleared hypotheses: k, h, hS, hk, this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ ∃ (i_1 : Fin (n + 3 + 1)),
    ¬i_1 = i ∧
      ∀ (i : Fin 3),
        ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯
                  ⋯ :
                (a : Fin 3) → Fin (n + 3 + 1))
              i =
            i_1
have hS : ¬Eq (α := Finset (Fin (n + 4))) {i, (⟨k, sorry⟩ : Fin (n + 4)), (⟨k + 1, sorry⟩ : Fin (n + 4)), (⟨k + 2, sorry⟩ : Fin (n + 4))} univ
Tactic: have hS : ¬ ({i, (⟨k, by lia⟩ : Fin (n + 4)), (⟨k + 1, by lia⟩ : Fin (n + 4)),
      (⟨k + 2, by lia⟩ : Fin (n + 4))} = Finset.univ) := fun hS ↦ by
    obtain ⟨i, hi⟩ := i
    by_cases hk : k = 0
    · subst hk
      have := Finset.mem_univ (Fin.last _ : Fin (n + 4))
      rw [← hS] at this
      -- this was produced using `simp? [Fin.ext_iff] at this`
      simp only [Fin.zero_eta, zero_add, Fin.mk_one, mem_insert, Fin.ext_iff, Fin.val_last,
        Fin.val_zero, AddLeftCancelMonoid.add_eq_zero, OfNat.ofNat_ne_zero, and_false,
        Fin.val_one, Nat.reduceEqDiff, mem_singleton, or_self, or_false] at this
      simp only [Fin.lt_def, Fin.val_last] at hₙ
      lia
    · have := Finset.mem_univ (0 : Fin (n + 4))
      rw [← hS] at this
      -- this was produced using `simp? [Fin.ext_iff] at this`
      simp only [mem_insert, Fin.ext_iff, Fin.val_zero, right_eq_add,
        AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, mem_singleton,
        OfNat.ofNat_ne_zero, or_self, or_false] at this
      obtain rfl | rfl := this <;> tauto
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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
⊢ ∃ (i_1 : Fin (n + 3 + 1)),
    ¬i_1 = i ∧
      ∀ (i : Fin 3),
        ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯
                  ⋯ :
                (a : Fin 3) → Fin (n + 3 + 1))
              i =
            i_1
have hS₁ : ∃ (x : Fin (n + 4)), x ∉ {i, (⟨k, sorry⟩ : Fin (n + 4)), (⟨k + 1, sorry⟩ : Fin (n + 4)), (⟨k + 2, sorry⟩ : Fin (n + 4))}
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 : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
hS : ∃ (x : Fin (n + 4)), x ∉ {i, (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))}
⊢ ∃ (i_1 : Fin (n + 3 + 1)),
    ¬i_1 = i ∧
      ∀ (i : Fin 3),
        ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯
                  ⋯ :
                (a : Fin 3) → Fin (n + 3 + 1))
              i =
            i_1
have refine_3 : ∀ (l : Fin (n + 4)) (hl : l ∉ {i, (⟨k, sorry⟩ : Fin (n + 4)), (⟨k + 1, sorry⟩ : Fin (n + 4)), (⟨k + 2, sorry⟩ : Fin (n + 4))}),
  ∃ (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: obtain ⟨l, hl⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
Goal:
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
l : Fin (n + 4)
hl : l ∉ {i, (⟨k, ⋯⟩ : Fin (n + 4)), (⟨k + 1, ⋯⟩ : Fin (n + 4)), (⟨k + 2, ⋯⟩ : Fin (n + 4))}
⊢ ∃ (i_1 : Fin (n + 3 + 1)),
    ¬i_1 = i ∧
      ∀ (i : Fin 3),
        ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯
                  ⋯ :
                (a : Fin 3) → Fin (n + 3 + 1))
              i =
            i_1
have hl₁ : ¬l = i ∧ ¬l = ⟨k, sorry⟩ ∧ ¬l = ⟨k + 1, sorry⟩ ∧ ¬l = ⟨k + 2, sorry⟩
Tactic: simp only [mem_insert, mem_singleton, not_or] at hl
Cleared hypotheses: hl
-- 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
l : Fin (n + 4)
hl : ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩
⊢ ∃ (i_1 : Fin (n + 3 + 1)),
    ¬i_1 = i ∧
      ∀ (i : Fin 3),
        ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯
                  ⋯ :
                (a : Fin 3) → Fin (n + 3 + 1))
              i =
            i_1
have refine_3 : ∀ (a : 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))
        a =
      l
Tactic: refine ⟨l, hl.1, fun a ↦ ?_⟩
-- 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
l : Fin (n + 4)
hl : ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩
a : Fin 3
⊢ ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        a =
      l
have refine_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))
      ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, sorry⟩) =
    l
Tactic: fin_cases a
Cleared hypotheses: a
-- 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
l : Fin (n + 4)
hl : ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩
a : Fin 3
refine_3 :
  ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) =
      l
⊢ ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        a =
      l
have refine_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))
      ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨1, sorry⟩) =
    l
Tactic: fin_cases a
Cleared hypotheses: a
-- 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
l : Fin (n + 4)
hl : ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩
a : Fin 3
refine_3 :
  ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) =
      l
refine_3₁ :
  ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨1, ⋯⟩) =
      l
⊢ ¬(stdSimplex.triangle (⟨k, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⋯ ⋯ :
          (a : Fin 3) → Fin (n + 3 + 1))
        a =
      l
have refine_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))
      ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨2, sorry⟩) =
    l
Tactic: fin_cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    Eq (α := (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₁.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₂.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
⊢ σ₁ = σ₂
have rw : Subfunctor.equalizer σ₁ σ₂ = Λ[n + 1, i]
Tactic: rw [← Subfunctor.equalizer_eq_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    Eq (α := (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₁.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₂.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
⊢ Subfunctor.equalizer σ₁ σ₂ = Λ[n + 1, i]
have apply : Λ[n + 1, i] ≤ Subfunctor.equalizer σ₁ σ₂
Tactic: apply le_antisymm (Subfunctor.equalizer_le σ₁ σ₂)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    Eq (α := (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₁.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₂.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
⊢ Λ[n + 1, i] ≤ Subfunctor.equalizer σ₁ σ₂
have simp : ∀ (a : Fin (n + 1 + 1)) (b : ¬a = i),
  Membership.mem (α := Δ[n + 1] _⦋n⦌) (γ := Set (Δ[n + 1] _⦋n⦌)) ((Subfunctor.equalizer σ₁ σ₂).obj (op ⦋n⦌))
    ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.δ a) : Δ[n + 1] _⦋n⦌)
Tactic: simp only [horn_eq_iSup, iSup_le_iff,
    Subtype.forall, Set.mem_compl_iff, Set.mem_singleton_iff,
    ← stdSimplex.ofSimplex_yonedaEquiv_δ, Subcomplex.ofSimplex_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ (yonedaEquiv : (a : Δ[n] ⟶ Λ[n + 1, i].toSSet) → Λ[n + 1, i].toSSet _⦋n⦌) (ι i j hij) = face i j hij
have rw : (yonedaEquiv : (a : Δ[n] ⟶ Λ[n + 1, i].toSSet) → Λ[n + 1, i].toSSet _⦋n⦌)
    ((Equiv.symm yonedaEquiv : (a : Λ[n + 1, i].toSSet _⦋n⦌) → Δ[n] ⟶ Λ[n + 1, i].toSSet) (face i j hij)) =
  face i j hij
Tactic: rw [ι, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
rw :
  (yonedaEquiv : (a : Δ[n] ⟶ Λ[n + 1, i].toSSet) → Λ[n + 1, i].toSSet _⦋n⦌)
      ((Equiv.symm yonedaEquiv : (a : Λ[n + 1, i].toSSet _⦋n⦌) → Δ[n] ⟶ Λ[n + 1, i].toSSet) (face i j hij)) =
    face i j hij
⊢ (yonedaEquiv : (a : Δ[n] ⟶ Λ[n + 1, i].toSSet) → Λ[n + 1, i].toSSet _⦋n⦌) (ι i j hij) = face i j hij
have rw₁ : face i j hij = face i j hij
Tactic: rw [ι, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ ι i j hij ≫ Λ[n + 1, i].ι = stdSimplex.δ j
have rw : (Equiv.symm yonedaEquiv : (a : Λ[n + 1, i].toSSet _⦋n⦌) → Δ[n] ⟶ Λ[n + 1, i].toSSet) (face i j hij) ≫ Λ[n + 1, i].ι =
  stdSimplex.δ j
Tactic: rw [ι, face, Equiv.symm_apply_apply, Subfunctor.lift_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
rw :
  (Equiv.symm yonedaEquiv : (a : Λ[n + 1, i].toSSet _⦋n⦌) → Δ[n] ⟶ Λ[n + 1, i].toSSet) (face i j hij) ≫ Λ[n + 1, i].ι =
    stdSimplex.δ j
⊢ ι i j hij ≫ Λ[n + 1, i].ι = stdSimplex.δ j
have rw₁ : (Equiv.symm yonedaEquiv : (a : Λ[n + 1, i].toSSet _⦋n⦌) → Δ[n] ⟶ Λ[n + 1, i].toSSet)
      ((yonedaEquiv : (a : Δ[n] ⟶ Λ[n + 1, i].toSSet) → Λ[n + 1, i].toSSet _⦋n⦌) (Subfunctor.lift (stdSimplex.δ j) sorry) :
        Λ[n + 1, i].toSSet _⦋n⦌) ≫
    Λ[n + 1, i].ι =
  stdSimplex.δ j
Tactic: rw [ι, face, Equiv.symm_apply_apply, Subfunctor.lift_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
rw :
  (Equiv.symm yonedaEquiv : (a : Λ[n + 1, i].toSSet _⦋n⦌) → Δ[n] ⟶ Λ[n + 1, i].toSSet) (face i j hij) ≫ Λ[n + 1, i].ι =
    stdSimplex.δ j
rw₁ :
  (Equiv.symm yonedaEquiv : (a : Λ[n + 1, i].toSSet _⦋n⦌) → Δ[n] ⟶ Λ[n + 1, i].toSSet)
        ((yonedaEquiv : (a : Δ[n] ⟶ Λ[n + 1, i].toSSet) → Λ[n + 1, i].toSSet _⦋n⦌)
            (Subfunctor.lift (stdSimplex.δ j) ⋯) :
          Λ[n + 1, i].toSSet _⦋n⦌) ≫
      Λ[n + 1, i].ι =
    stdSimplex.δ j
⊢ ι i j hij ≫ Λ[n + 1, i].ι = stdSimplex.δ j
have rw₂ : Subfunctor.lift (stdSimplex.δ j) sorry ≫ Λ[n + 1, i].ι = stdSimplex.δ j
Tactic: rw [ι, face, Equiv.symm_apply_apply, Subfunctor.lift_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
rw :
  (Equiv.symm yonedaEquiv : (a : Λ[n + 1, i].toSSet _⦋n⦌) → Δ[n] ⟶ Λ[n + 1, i].toSSet) (face i j hij) ≫ Λ[n + 1, i].ι =
    stdSimplex.δ j
rw₁ :
  (Equiv.symm yonedaEquiv : (a : Λ[n + 1, i].toSSet _⦋n⦌) → Δ[n] ⟶ Λ[n + 1, i].toSSet)
        ((yonedaEquiv : (a : Δ[n] ⟶ Λ[n + 1, i].toSSet) → Λ[n + 1, i].toSSet _⦋n⦌)
            (Subfunctor.lift (stdSimplex.δ j) ⋯) :
          Λ[n + 1, i].toSSet _⦋n⦌) ≫
      Λ[n + 1, i].ι =
    stdSimplex.δ j
rw₂ : Subfunctor.lift (stdSimplex.δ j) ⋯ ≫ Λ[n + 1, i].ι = stdSimplex.δ j
⊢ ι i j hij ≫ Λ[n + 1, i].ι = stdSimplex.δ j
have rw₃ : stdSimplex.δ j = stdSimplex.δ j
Tactic: rw [ι, face, Equiv.symm_apply_apply, Subfunctor.lift_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hij = faceι i j hij
have rw : ι i j hij = (stdSimplex.faceSingletonComplIso j).hom ≫ faceι i j hij
Tactic: rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} j).hom, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
⊢ Eq.{u + 1} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}) Λ[2, 0]
have a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}) Λ[2, 0]
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}) Λ[2, 0]
⊢ Eq.{u + 1} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}) Λ[2, 0]
have a₁ : LE.le.{u} (α := Δ[2].Subcomplex) Λ[2, 0] (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}) Λ[2, 0]
have a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 0] ∧
  LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 0]
Tactic: rw [sup_le_iff]