awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
A B : X.Subcomplex
h : A ≤ B
d : ℕ
inst : HasDimensionLT.{u} B.toSSet d
⊢ HasDimensionLT.{u} A.toSSet d

Tactic:
hasDimensionLT_of_mono (Subcomplex.homOfLE h) d

Premises used: SSet.Subcomplex.homOfLE, SSet.hasDimensionLT_of_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X Y : SSet
f : X ⟶ Y
inst : Epi f
d : ℕ
inst_1 : X.HasDimensionLT d
n : ℕ
hn : d ≤ n
h : ∀ (y : Y _⦋n⦌), y ∈ Y.degenerate n ↔ Membership.mem (γ := Set (Y _⦋n⦌)) ⊤ y
⊢ Y.degenerate n = ⊤

Tactic:
ext y
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X Y : SSet
f : X ⟶ Y
inst : Epi f
d : ℕ
inst_1 : X.HasDimensionLT d
n : ℕ
hn : d ≤ n
y : Y _⦋n⦌
h : y ∈ Y.degenerate n
⊢ y ∈ Y.degenerate n ↔ Membership.mem (γ := Set (Y _⦋n⦌)) ⊤ y

Tactic:
simp only [Set.top_eq_univ, Set.mem_univ, iff_true]

Premises used: iff_true, Set.top_eq_univ, Set.mem_univ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X Y : SSet
f : X ⟶ Y
inst : Epi f
d : ℕ
inst_1 : X.HasDimensionLT d
n : ℕ
hn : d ≤ n
y : Y _⦋n⦌
h :
  ∀ (x : X _⦋n⦌),
    Membership.mem (α := Y _⦋n⦌) (Y.degenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌))
⊢ y ∈ Y.degenerate n

Tactic:
obtain ⟨x, rfl⟩ := epi_iff_surjective (f := (f.app (op ⦋n⦌))).1 inferInstance y

Premises used: CategoryTheory.epi_iff_surjective, inferInstance, SimplexCategory.mk, Opposite.op, Iff.mp, CategoryTheory.NatTrans.app, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X Y : SSet
f : X ⟶ Y
inst : Epi f
d : ℕ
inst_1 : X.HasDimensionLT d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
h : x ∈ X.degenerate n
⊢ Membership.mem (α := Y _⦋n⦌) (Y.degenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))

Tactic:
apply degenerate_app_apply

Premises used: SSet.degenerate_app_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X Y : SSet
f : X ⟶ Y
inst : Epi f
d : ℕ
inst_1 : X.HasDimensionLT d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
⊢ x ∈ X.degenerate n

Tactic:
simp [X.degenerate_eq_univ_of_hasDimensionLT d n hn]

Premises used: SSet.degenerate_eq_univ_of_hasDimensionLT
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X Y : SSet
e : X ≅ Y
d : ℕ
⊢ X.HasDimensionLT d ↔ Y.HasDimensionLT d

Tactic:
⟨fun _ ↦ hasDimensionLT_of_epi e.hom d, fun _ ↦ hasDimensionLT_of_epi e.inv d⟩

Premises used: SSet.hasDimensionLT_of_epi, Iff.intro, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X Y : SSet
f : X ⟶ Y
d : ℕ
inst : X.HasDimensionLT d
⊢ HasDimensionLT.{u} (Subcomplex.range f).toSSet d

Tactic:
hasDimensionLT_of_epi (Subcomplex.toRange f) d

Premises used: SSet.hasDimensionLT_of_epi, SSet.Subcomplex.toRange
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
ι : Type u_1
A : ι → X.Subcomplex
d : ℕ
simp :
  (∀ (n : ℕ) (hn : d ≤ n),
      X.degenerate n ⊓ Subfunctor.obj (⨆ (i : ι), A i) (op ⦋n⦌) = Subfunctor.obj (⨆ (i : ι), A i) (op ⦋n⦌)) ↔
    ∀ (i : ι) (n : ℕ) (hn : d ≤ n), X.degenerate n ⊓ (A i).obj (op ⦋n⦌) = (A i).obj (op ⦋n⦌)
⊢ HasDimensionLT.{u} (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)) d ↔ ∀ (i : ι), HasDimensionLT.{u} (A i).toSSet d

Tactic:
simp only [hasDimensionLT_iff, Subcomplex.degenerate_eq_top_iff]

Premises used: SSet.Subcomplex.degenerate_eq_top_iff, SSet.hasDimensionLT_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
ι : Type u_1
A : ι → X.Subcomplex
d : ℕ
⊢ (∀ (n : ℕ) (hn : d ≤ n),
      X.degenerate n ⊓ Subfunctor.obj (⨆ (i : ι), A i) (op ⦋n⦌) = Subfunctor.obj (⨆ (i : ι), A i) (op ⦋n⦌)) ↔
    ∀ (i : ι) (n : ℕ) (hn : d ≤ n), X.degenerate n ⊓ (A i).obj (op ⦋n⦌) = (A i).obj (op ⦋n⦌)

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
d : ℕ
⊢ HasDimensionLT.{u} (Subcomplex.toSSet (X := X) ⊤) d ↔ X.HasDimensionLT d

Tactic:
hasDimensionLT_iff_of_iso (Subcomplex.topIso X) _

Premises used: SSet.Subcomplex.topIso, SSet.hasDimensionLT_iff_of_iso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
n k : ℕ
hk : n ≤ k
h :
  ∀ (x : X _⦋k⦌) (hx : Membership.mem (γ := Set (X _⦋k⦌)) (Subfunctor.obj ⊥ (op ⦋k⦌)) x),
    Membership.mem (γ := Set (Subcomplex.toSSet (X := X) ⊥ _⦋k⦌)) ((Subcomplex.toSSet (X := X) ⊥).degenerate k)
        (Subtype.mk (p := fun (x : X _⦋k⦌) ↦ Membership.mem (γ := Set (X _⦋k⦌)) (Subfunctor.obj ⊥ (op ⦋k⦌)) x) x hx) ↔
      Membership.mem (γ := Set (Subcomplex.toSSet (X := X) ⊥ _⦋k⦌)) ⊤
        (Subtype.mk (p := fun (x : X _⦋k⦌) ↦ Membership.mem (γ := Set (X _⦋k⦌)) (Subfunctor.obj ⊥ (op ⦋k⦌)) x) x hx)
⊢ Eq.{u + 1} (α := Set (Subcomplex.toSSet (X := X) ⊥ _⦋k⦌)) ((Subcomplex.toSSet (X := X) ⊥).degenerate k) ⊤

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
n k : ℕ
hk : n ≤ k
x : X _⦋k⦌
hx : Membership.mem (γ := Set (X _⦋k⦌)) (Subfunctor.obj ⊥ (op ⦋k⦌)) x
⊢ Membership.mem (γ := Set (Subcomplex.toSSet (X := X) ⊥ _⦋k⦌)) ((Subcomplex.toSSet (X := X) ⊥).degenerate k)
      (Subtype.mk (p := fun (x : X _⦋k⦌) ↦ Membership.mem (γ := Set (X _⦋k⦌)) (Subfunctor.obj ⊥ (op ⦋k⦌)) x) x hx) ↔
    Membership.mem (γ := Set (Subcomplex.toSSet (X := X) ⊥ _⦋k⦌)) ⊤
      (Subtype.mk (p := fun (x : X _⦋k⦌) ↦ Membership.mem (γ := Set (X _⦋k⦌)) (Subfunctor.obj ⊥ (op ⦋k⦌)) x) x hx)

Tactic:
tauto
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
obj :
  ∀ (n : SimplexCategoryᵒᵖ) (x : Functor.obj c.1 n),
    Membership.mem (γ := Set (Functor.obj c.1 n)) (Subfunctor.obj (⨆ (j : J), Subcomplex.range (c.ι.app j)) n) x ↔
      Membership.mem (γ := Set (Functor.obj c.1 n)) (Subfunctor.obj ⊤ n) x
⊢ Eq.{u + 1} (α := Subcomplex c.1) (⨆ (j : J), Subcomplex.range (c.ι.app j)) ⊤

Tactic:
ext n x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
n : SimplexCategoryᵒᵖ
x : Functor.obj c.1 n
obj :
  ∃ (i : J) (y : (F.obj i).obj n),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((c.ι.app i).app n) : (a : (F.obj i).obj n) → c.1.obj n) y = x
⊢ Membership.mem (γ := Set (Functor.obj c.1 n)) (Subfunctor.obj (⨆ (j : J), Subcomplex.range (c.ι.app j)) n) x ↔
    Membership.mem (γ := Set (Functor.obj c.1 n)) (Subfunctor.obj ⊤ n) x

Tactic:
simp only [Subfunctor.iSup_obj, Subfunctor.range_obj, Set.mem_iUnion, Set.mem_range,
    Subfunctor.top_obj, Set.top_eq_univ, Set.mem_univ, iff_true]

Premises used: Set.mem_range, Set.mem_iUnion, iff_true, Set.top_eq_univ, CategoryTheory.Subfunctor.range_obj, Set.mem_univ, CategoryTheory.Subfunctor.top_obj, CategoryTheory.Subfunctor.iSup_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
n : SimplexCategoryᵒᵖ
x : Functor.obj c.1 n
⊢ ∃ (i : J) (y : (F.obj i).obj n),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((c.ι.app i).app n) : (a : (F.obj i).obj n) → c.1.obj n) y = x

Tactic:
Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves ((evaluation _ _).obj n) hc) x

Premises used: CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, CategoryTheory.evaluation, CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
n : SimplexCategoryᵒᵖ
x : Functor.obj c.1 n
⊢ ∃ (i : J) (y : (F.obj i).obj n),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((c.ι.app i).app n) : (a : (F.obj i).obj n) → c.1.obj n) y = x

Tactic:
exact Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves ((evaluation _ _).obj n) hc) x

Premises used: CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, CategoryTheory.evaluation, CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
X : SSet
φ : c.pt ⟶ X
rw : Subcomplex.range (𝟙 c.pt ≫ φ)
| Subcomplex.range φ

Tactic:
rw [← Category.id_comp φ]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
X : SSet
φ : c.pt ⟶ X
conv_lhs : Subcomplex.range (𝟙 c.pt ≫ φ) = ⨆ (j : J), Subcomplex.range (c.ι.app j ≫ φ)
⊢ Subcomplex.range φ = ⨆ (j : J), Subcomplex.range (c.ι.app j ≫ φ)

Tactic:
conv_lhs => rw [← Category.id_comp φ]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
X : SSet
φ : c.pt ⟶ X
simp_rw : (Subcomplex.range (𝟙 c.pt)).image φ = ⨆ (j : J), (Subcomplex.range (c.ι.app j)).image φ
simp_rw₁ : Subcomplex.image ⊤ φ = ⨆ (j : J), (Subcomplex.range (c.ι.app j)).image φ
simp_rw₂ :
  Subcomplex.image (⨆ (j : J), Subcomplex.range (c.ι.app j)) φ = ⨆ (j : J), (Subcomplex.range (c.ι.app j)).image φ
⊢ Subcomplex.range (𝟙 c.pt ≫ φ) = ⨆ (j : J), Subcomplex.range (c.ι.app j ≫ φ)

Tactic:
simp_rw [Subcomplex.range_comp, Subcomplex.range_eq_top, ← iSup_range_eq_top_of_isColimit hc,
    Subcomplex.image_iSup]

Premises used: SSet.Subcomplex.range_eq_top, SSet.Subcomplex.range_comp, SSet.iSup_range_eq_top_of_isColimit, SSet.Subcomplex.image_iSup
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
n : ℕ
h : ∀ (j : J), HasDimensionLT.{u} (F.obj j) n
rw : ∀ (i : J), HasDimensionLT.{u} (Subcomplex.range (c.ι.app i)).toSSet n
⊢ HasDimensionLT.{u} c.pt n

Tactic:
rw [← hasDimensionLT_subcomplex_top_iff, ← iSup_range_eq_top_of_isColimit hc,
    hasDimensionLT_iSup_iff]

Premises used: SSet.hasDimensionLT_subcomplex_top_iff, SSet.hasDimensionLT_iSup_iff, SSet.iSup_range_eq_top_of_isColimit
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
n : ℕ
h : ∀ (j : J), HasDimensionLT.{u} (F.obj j) n
⊢ ∀ (i : J), HasDimensionLT.{u} (Subcomplex.range (c.ι.app i)).toSSet n

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
inst_2 : Finite J
h : ∀ (j : J), SSet.Finite.{u} (F.obj j)
rw : ∀ (i : J), SSet.Finite.{u} (Subcomplex.range (c.ι.app i)).toSSet
⊢ SSet.Finite.{u} c.pt

Tactic:
rw [← finite_subcomplex_top_iff, ← iSup_range_eq_top_of_isColimit hc, finite_iSup_iff]

Premises used: SSet.finite_iSup_iff, SSet.iSup_range_eq_top_of_isColimit, SSet.finite_subcomplex_top_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
inst_2 : Finite J
h : ∀ (j : J), SSet.Finite.{u} (F.obj j)
⊢ ∀ (i : J), SSet.Finite.{u} (Subcomplex.range (c.ι.app i)).toSSet

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{?u.10772, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
apply : ∀ (j : Discrete PEmpty.{1}), SSet.Finite.{u} (Functor.obj (Functor.empty SSet) j)
⊢ SSet.Finite.{u} (⊥_ SSet)

Tactic:
apply finite_of_isColimit (initialIsInitial (C := SSet.{u}))
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{?u.11777, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst_2 : X.Finite
inst_3 : Y.Finite
apply : ∀ (j : Discrete WalkingPair), SSet.Finite.{u} (Functor.obj (pair X Y) j)
⊢ SSet.Finite.{u} (X ⨿ Y)

Tactic:
apply finite_of_isColimit (coprodIsCoprod X Y)

Premises used: CategoryTheory.Limits.coprodIsCoprod, SSet.finite_of_isColimit
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{?u.11777, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst_2 : X.Finite
inst_3 : Y.Finite
left : X.Finite
⊢ SSet.Finite.{u} (Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{?u.11777, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst_2 : X.Finite
inst_3 right : Y.Finite
⊢ SSet.Finite.{u} (Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{?u.11777, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst_2 : X.Finite
inst_3 : Y.Finite
⊢ X.Finite

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{?u.11777, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst_2 : X.Finite
inst_3 : Y.Finite
⊢ Y.Finite

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{?u.13010, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst_2 : Finite ι
X : ι → SSet
inst_3 : HasCoproduct X
inst_4 : ∀ (j : ι), SSet.Finite.{u} (X j)
obtain : ∀ (n : ℕ) (e : ι ≃ Fin n), HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
⊢ HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{?u.13010, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst_2 : Finite ι
X : ι → SSet
inst_3 : HasCoproduct X
inst_4 : ∀ (j : ι), SSet.Finite.{u} (X j)
n : ℕ
e : ι ≃ Fin n
⊢ HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)

Tactic:
hasColimitsOfShape_of_equivalence (Discrete.equivalence e.symm)

Premises used: CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, Equiv.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{?u.13010, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst_2 : Finite ι
X : ι → SSet
inst_3 : HasCoproduct X
inst_4 : ∀ (j : ι), SSet.Finite.{u} (X j)
n : ℕ
e : ι ≃ Fin n
⊢ HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)

Tactic:
exact hasColimitsOfShape_of_equivalence (Discrete.equivalence e.symm)

Premises used: CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, Equiv.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{?u.13010, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst_2 : Finite ι
X : ι → SSet
inst_3 : HasCoproduct X
inst_4 : ∀ (j : ι), SSet.Finite.{u} (X j)
⊢ HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)

Tactic:
have : HasColimitsOfShape (Discrete ι) (Type u) := by
    obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι
    exact hasColimitsOfShape_of_equivalence (Discrete.equivalence e.symm)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{?u.13010, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst_2 : Finite ι
X : ι → SSet
inst_3 : HasCoproduct X
inst_4 : ∀ (j : ι), SSet.Finite.{u} (X j)
this : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
x : Discrete ι
j : ι
dsimp : SSet.Finite.{u} (X j)
⊢ SSet.Finite.{u} (Functor.obj (Discrete.functor X) { as := j : Discrete ι })

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{?u.13010, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst_2 : Finite ι
X : ι → SSet
inst_3 : HasCoproduct X
inst_4 : ∀ (j : ι), SSet.Finite.{u} (X j)
this : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
x : Discrete ι
j : ι
⊢ SSet.Finite.{u} (X j)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
J : Type u_1
inst : Category.{?u.13010, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst_2 : Finite ι
X : ι → SSet
inst_3 : HasCoproduct X
inst_4 : ∀ (j : ι), SSet.Finite.{u} (X j)
this : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
⊢ SSet.Finite.{u} (∐ X)

Tactic:
exact finite_of_isColimit (coproductIsCoproduct X) (fun ⟨j⟩ ↦ by dsimp; infer_instance)

Premises used: _private.0.SSet.instFiniteSigmaObjOfFinite.match_1, CategoryTheory.Discrete.functor, SSet.finite_of_isColimit, CategoryTheory.Limits.coproductIsCoproduct, SSet.Finite, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
ι : Type v
inst : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst_1 : HasCoproduct X
f : ∐ X ⟶ Y
rw :
  Eq.{u + 1} (α := Y.Subcomplex) (⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f))
    (⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f))
⊢ Subcomplex.range f = ⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f)

Tactic:
rw [range_eq_iSup_of_isColimit (coproductIsCoproduct X) f]

Premises used: CategoryTheory.Limits.coproductIsCoproduct, SSet.range_eq_iSup_of_isColimit
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
ι : Type v
inst : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst_1 : HasCoproduct X
f : ∐ X ⟶ Y
⊢ Eq.{u + 1} (α := Y.Subcomplex) (⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f))
    (⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
ι : Type v
inst : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst_1 : HasCoproduct X
f : ∐ X ⟶ Y
refine_1 :
  LE.le.{u} (α := Y.Subcomplex) (⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f))
    (⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f))
refine_2 :
  LE.le.{u} (α := Y.Subcomplex) (⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f))
    (⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f))
⊢ Eq.{u + 1} (α := Y.Subcomplex) (⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f))
    (⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f))

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
ι : Type v
inst : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst_1 : HasCoproduct X
f : ∐ X ⟶ Y
refine_1 :
  ∀ (a' : ι),
    Subcomplex.range (X := Functor.obj (Discrete.functor X) { as := a' : Discrete ι })
        ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app { as := a' : Discrete ι } ≫ f) ≤
      ⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f)
⊢ LE.le.{u} (α := Y.Subcomplex) (⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f))
    (⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f))

Tactic:
simp only [iSup_le_iff, Discrete.forall]

Premises used: CategoryTheory.Discrete.forall, iSup_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
ι : Type v
inst : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst_1 : HasCoproduct X
f : ∐ X ⟶ Y
i : ι
⊢ Subcomplex.range (X := Functor.obj (Discrete.functor X) { as := i : Discrete ι })
      ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app { as := i : Discrete ι } ≫ f) ≤
    Subcomplex.range (X := Functor.obj (Discrete.functor X) { as := i : Discrete ι })
      ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app { as := i } ≫ f)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
ι : Type v
inst : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst_1 : HasCoproduct X
f : ∐ X ⟶ Y
i : ι
⊢ Subcomplex.range (X := Functor.obj (Discrete.functor X) { as := i : Discrete ι })
      ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app { as := i : Discrete ι } ≫ f) ≤
    ⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f)

Tactic:
exact le_trans (by rfl) (le_iSup _ i)

Premises used: le_iSup, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
ι : Type v
inst : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst_1 : HasCoproduct X
f : ∐ X ⟶ Y
refine_2 :
  ∀ (i : ι),
    Subcomplex.range (Sigma.ι X i ≫ f) ≤ ⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f)
⊢ LE.le.{u} (α := Y.Subcomplex) (⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f))
    (⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f))

Tactic:
simp only [iSup_le_iff]

Premises used: iSup_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
ι : Type v
inst : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst_1 : HasCoproduct X
f : ∐ X ⟶ Y
i : ι
⊢ Subcomplex.range (Sigma.ι X i ≫ f) ≤ Subcomplex.range (Sigma.ι X i ≫ f)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
Goal:
ι : Type v
inst : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst_1 : HasCoproduct X
f : ∐ X ⟶ Y
i : ι
⊢ Subcomplex.range (Sigma.ι X i ≫ f) ≤ ⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f)

Tactic:
exact le_trans (by rfl) (le_iSup _ ⟨i⟩)

Premises used: le_iSup, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
obj :
  ∀ (m : SimplexCategoryᵒᵖ) (x₁ : X₁.obj m) (x₂ : X₂.obj m),
    Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) X₁ X₂).obj m))
        (Subfunctor.obj
          (⨆ (x₁ : X₁.N), ⨆ (x₂ : X₂.N), (Subcomplex.ofSimplex x₁.simplex).prod (Subcomplex.ofSimplex x₂.simplex)) m)
        (x₁, x₂) ↔
      Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) X₁ X₂).obj m)) (Subfunctor.obj ⊤ m) (x₁, x₂)
⊢ Eq.{u + 1} (α := (tensorObj (𝒞 := Functor.category) X₁ X₂).Subcomplex)
    (⨆ (x₁ : X₁.N), ⨆ (x₂ : X₂.N), (Subcomplex.ofSimplex x₁.simplex).prod (Subcomplex.ofSimplex x₂.simplex)) ⊤

Tactic:
ext m ⟨x₁, x₂⟩