awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
X Y : SSet
m : ℕ
h :
  Eq (α := hoFunctor.obj (X ⨯ Δ[m]) ⟶ hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m])
    (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
      (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
        (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))
⊢ IsIso (X := hoFunctor.obj (X ⨯ Δ[m])) (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m])
have convert_to : IsIso (X := hoFunctor.obj (X ⨯ Δ[m])) (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m])
  (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
    (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
      (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))
Tactic: convert_to IsIso (hoFunctor.map (prod.braiding _ _).hom ≫
    prodComparison hoFunctor Δ[m] X ≫ (prod.braiding _ _).hom)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
X Y : SSet
m : ℕ
⊢ Eq (α := hoFunctor.obj (X ⨯ Δ[m]) ⟶ hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m])
    (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
      (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
        (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))
have h : Eq (α := (↑(hoFunctor.obj (X ⨯ Δ[m])) : Type u) ⥤ (↑(hoFunctor.obj X) : Type u))
  (Cat.Hom.toFunctor
    (CategoryStruct.comp (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m]) prod.fst))
  (Cat.Hom.toFunctor
    (CategoryStruct.comp (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m])
      (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
        (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
          (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))
      prod.fst))
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
X Y : SSet
m : ℕ
h :
  Eq (α := (↑(hoFunctor.obj (X ⨯ Δ[m])) : Type u) ⥤ (↑(hoFunctor.obj X) : Type u))
    (Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m]) prod.fst))
    (Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m])
        (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
          (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
            (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))
        prod.fst))
⊢ Eq (α := hoFunctor.obj (X ⨯ Δ[m]) ⟶ hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m])
    (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
      (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
        (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))
have h₁ : Eq (α := (↑(hoFunctor.obj (X ⨯ Δ[m])) : Type u) ⥤ (↑(hoFunctor.obj Δ[m]) : Type u))
  (Cat.Hom.toFunctor
    (CategoryStruct.comp (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m]) prod.snd))
  (Cat.Hom.toFunctor
    (CategoryStruct.comp (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m])
      (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
        (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
          (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))
      prod.snd))
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
X Y : SSet
m : ℕ
⊢ IsIso (X := hoFunctor.obj (X ⨯ Δ[m])) (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m])
    (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
      (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
        (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))
have suffices : IsIso (X := hoFunctor.obj (Δ[m] ⨯ X)) (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
Tactic: suffices IsIso (prodComparison hoFunctor Δ[m] X) by infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
⊢ Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
      (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
          (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
      s ↔
    s.obj i.castSucc = s.obj i.succ
have mp : Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
    (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
        (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
    s →
  s.obj i.castSucc = s.obj i.succ
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
mp :
  Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
      (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
          (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
      s →
    s.obj i.castSucc = s.obj i.succ
⊢ Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
      (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
          (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
      s ↔
    s.obj i.castSucc = s.obj i.succ
have mpr : s.obj i.castSucc = s.obj i.succ →
  Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
    (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
        (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
    s
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
⊢ Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
    (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
        (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
    s
have mpr : (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i) :
      (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve X) i.castSucc) :
          (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
        s :
      (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) =
  s
Tactic: refine ⟨(nerve X).δ i.castSucc s, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i) :
        (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve X) i.castSucc) :
            (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
          s :
        (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) =
    s
have mpr : ∀ (j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)),
  Functor.obj
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i) :
          (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve X) i.castSucc) :
              (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
            s :
          (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)))
      j =
    s.obj j
Tactic: ext j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
⊢ Functor.obj
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i) :
          (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve X) i.castSucc) :
              (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
            s :
          (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)))
      j =
    s.obj j
have mpr : s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j
Tactic: rw [nerve.σ_obj, nerve.δ_obj]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
⊢ s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j
have pos : ∀ (h₁ : i.castSucc < j), s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j
Tactic: by_cases h₁ : i.castSucc < j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
pos : ∀ (h₁ : i.castSucc < j), s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j
⊢ s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j
have neg : ∀ (h₁ : ¬i.castSucc < j), s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j
Tactic: by_cases h₁ : i.castSucc < j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
h₁ : i.castSucc < j
⊢ s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j
have pos : ∀ (j : Fin (n + 1)) (h₁ : i.castSucc < j.succ), s.obj (i.castSucc.succAbove (i.predAbove j.succ)) = s.obj j.succ
Tactic: obtain ⟨j, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h₁)
Cleared hypotheses: j, h₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin (n + 1)
h₁ : i.castSucc < j.succ
⊢ s.obj (i.castSucc.succAbove (i.predAbove j.succ)) = s.obj j.succ
have pos : s.obj (i.castSucc.succAbove (j.succ.pred sorry)) = s.obj j.succ
Tactic: rw [Fin.predAbove_of_castSucc_lt _ _ h₁, Fin.pred_succ,
        Fin.succAbove_of_le_castSucc _ _ (Fin.le_castSucc_iff.2 h₁)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin (n + 1)
h₁ : i.castSucc < j.succ
pos : s.obj (i.castSucc.succAbove (j.succ.pred ⋯)) = s.obj j.succ
⊢ s.obj (i.castSucc.succAbove (i.predAbove j.succ)) = s.obj j.succ
have pos₁ : s.obj (i.castSucc.succAbove j) = s.obj j.succ
Tactic: rw [Fin.predAbove_of_castSucc_lt _ _ h₁, Fin.pred_succ,
        Fin.succAbove_of_le_castSucc _ _ (Fin.le_castSucc_iff.2 h₁)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin (n + 1)
h₁ : i.castSucc < j.succ
pos : s.obj (i.castSucc.succAbove (j.succ.pred ⋯)) = s.obj j.succ
pos₁ : s.obj (i.castSucc.succAbove j) = s.obj j.succ
⊢ s.obj (i.castSucc.succAbove (i.predAbove j.succ)) = s.obj j.succ
have pos₂ : s.obj j.succ = s.obj j.succ
Tactic: rw [Fin.predAbove_of_castSucc_lt _ _ h₁, Fin.pred_succ,
        Fin.succAbove_of_le_castSucc _ _ (Fin.le_castSucc_iff.2 h₁)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (hypothesis)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
h₁ : ¬i.castSucc < j
⊢ s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j
have h₂ : j ≤ i.castSucc
Tactic: simp only [not_lt] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
hi : s.obj i.castSucc = s.obj i.succ
⊢ Membership.mem (γ := Set (nerve X _⦋n + 1⦌)) ((nerve X).degenerate (n + 1)) s
have simp : ∃ (i : Fin (n + 1)),
  Membership.mem (γ := Set (ComposableArrows X (n + 1)))
    (Set.range (ι := ComposableArrows X n)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
        (a : ComposableArrows X n) → ComposableArrows X (n + 1)))
    s
Tactic: simp only [nerve_obj, SSet.degenerate_eq_iUnion_range_σ, Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
hi : s.obj i.castSucc = s.obj i.succ
⊢ Membership.mem (γ := Set (ComposableArrows X (n + 1)))
    (Set.range (ι := ComposableArrows X n)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
        (a : ComposableArrows X n) → ComposableArrows X (n + 1)))
    s
have rwa : ∀
  (hi :
    Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
      (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
          (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
      s),
  Membership.mem (γ := Set (ComposableArrows X (n + 1)))
    (Set.range (ι := ComposableArrows X n)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
        (a : ComposableArrows X n) → ComposableArrows X (n + 1)))
    s
Tactic: rwa [← mem_range_nerve_σ_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
⊢ Membership.mem (γ := Set (nerve X _⦋n⦌)) ((nerve X).nonDegenerate n) s ↔ StrictMono s.obj
have zero : ∀ (s : nerve X _⦋0⦌), Membership.mem (γ := Set (nerve X _⦋0⦌)) ((nerve X).nonDegenerate 0) s ↔ StrictMono s.obj
Tactic: obtain _ | n := n
Cleared hypotheses: n, s
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
zero : ∀ (s : nerve X _⦋0⦌), Membership.mem (γ := Set (nerve X _⦋0⦌)) ((nerve X).nonDegenerate 0) s ↔ StrictMono s.obj
⊢ Membership.mem (γ := Set (nerve X _⦋n⦌)) ((nerve X).nonDegenerate n) s ↔ StrictMono s.obj
have succ : ∀ (n : ℕ) (s : nerve X _⦋n + 1⦌),
  Membership.mem (γ := Set (nerve X _⦋n + 1⦌)) ((nerve X).nonDegenerate (n + 1)) s ↔ StrictMono s.obj
Tactic: obtain _ | n := n
Cleared hypotheses: n, s
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ Membership.mem (γ := Set (nerve X _⦋n + 1⦌)) ((nerve X).nonDegenerate (n + 1)) s ↔ StrictMono s.obj
have succ : (∃ (i : Fin (n + 1)),
    Membership.mem (γ := Set (nerve X _⦋n + 1⦌))
      (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
          (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
      s) ↔
  ¬∀ (i : Fin (Opposite.unop (Opposite.op ⦋n + 1⦌)).len), s.obj i.castSucc < s.obj i.succ
Tactic: rw [← not_iff_not, ← SSet.mem_degenerate_iff_notMem_nonDegenerate,
      Fin.strictMono_iff_lt_succ, SSet.degenerate_eq_iUnion_range_σ, Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ (∃ (i : Fin (n + 1)),
      Membership.mem (γ := Set (nerve X _⦋n + 1⦌))
        (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
            (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
        s) ↔
    ¬∀ (i : Fin (Opposite.unop (Opposite.op ⦋n + 1⦌)).len), s.obj i.castSucc < s.obj i.succ
have succ : (∃ (i : Fin (n + 1)), s.obj i.castSucc = s.obj i.succ) ↔ ∃ (x : Fin (n + 1)), ¬s.obj x.castSucc < s.obj x.succ
Tactic: simp only [mem_range_nerve_σ_iff, not_forall]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ (∃ (i : Fin (n + 1)), s.obj i.castSucc = s.obj i.succ) ↔ ∃ (x : Fin (n + 1)), ¬s.obj x.castSucc < s.obj x.succ
have succ : ∀ (a : Fin (n + 1)), s.obj a.castSucc = s.obj a.succ ↔ ¬s.obj a.castSucc < s.obj a.succ
Tactic: apply exists_congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (hypothesis)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
⊢ s.obj i.castSucc = s.obj i.succ ↔ ¬s.obj i.castSucc < s.obj i.succ
have this : s.obj i.castSucc ≤ s.obj i.succ
Tactic: have := s.monotone i.castSucc_le_succ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
⊢ Membership.mem (γ := Set (nerve X _⦋n⦌)) ((nerve X).nonDegenerate n) s ↔ Function.Injective s.obj
have rw : StrictMono s.obj ↔ Function.Injective s.obj
Tactic: rw [mem_nerve_nonDegenerate_iff_strictMono]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
⊢ StrictMono s.obj ↔ Function.Injective s.obj
have refine : ∀ (h : Function.Injective s.obj) (i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)) (hij : i < j),
  s.obj i < s.obj j
Tactic: refine ⟨fun h ↦ h.injective, fun h i j hij ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
⊢ s.obj i < s.obj j
have inl : ∀ (h' : s.obj i < s.obj j), s.obj i < s.obj j
Tactic: obtain h' | h' := (s.monotone hij.le).lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate (goal)
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
inl : ∀ (h' : s.obj i < s.obj j), s.obj i < s.obj j
⊢ s.obj i < s.obj j
have inr : ∀ (h' : s.obj i = s.obj j), s.obj i < s.obj j
Tactic: obtain h' | h' := (s.monotone hij.le).lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.N
⊢ x ≤ y ↔
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (_ : Mono f),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
          y.simplex =
        x.simplex
have simp : (∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex) ↔
  ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (_ : Mono f),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex
Tactic: simp only [le_iff, CategoryTheory.Subfunctor.ofSection_le_iff,
    Subcomplex.mem_ofSimplex_obj_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.N
⊢ (∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (_ : Mono f),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex) →
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex
have tauto : ∀ (w : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
  Mono w →
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map w.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex →
      ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (hypothesis)
Goal:
X : SSet
x y : X.N
h : x ≤ y
⊢ x.dim ≤ y.dim
have h₁ : ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (_ : Mono f),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
      y.simplex =
    x.simplex
Tactic: rw [le_iff_exists_mono] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.N
h :
  ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (_ : Mono f),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
        y.simplex =
      x.simplex
⊢ x.dim ≤ y.dim
have obtain : ∀ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (hf : Mono f),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
        y.simplex =
      x.simplex →
    x.dim ≤ y.dim
Tactic: obtain ⟨f, hf, _⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.N
h : x < y
⊢ x.dim < y.dim
have inl : ∀ (h' : x.dim < y.dim), x.dim < y.dim
Tactic: obtain h' | h' := (dim_le_of_le h.le).lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.N
h : x < y
inl : ∀ (h' : x.dim < y.dim), x.dim < y.dim
⊢ x.dim < y.dim
have inr : ∀ (h' : x.dim = y.dim), x.dim < y.dim
Tactic: obtain h' | h' := (dim_le_of_le h.le).lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.N
h : x < y
h' : x.dim = y.dim
⊢ x.dim < y.dim
have inr : ∀ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
  Mono f →
    ∀
      (hf :
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
            y.simplex =
          x.simplex),
      x.dim < y.dim
Tactic: obtain ⟨f, _, hf⟩ := le_iff_exists_mono.1 h.le