awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
A : X.Subcomplex
d : ℕ
h : X.HasDimensionLT d
i : ℕ
hi : i < d
apply :
  Function.Injective (β := X _⦋i⦌) fun (a : (↑(A.toSSet.nonDegenerate i) : Type u)) ↦ (↑(↑a : A.toSSet _⦋i⦌) : X _⦋i⦌)
⊢ Finite.{u + 1} (↑(A.toSSet.nonDegenerate i) : Type u)

Tactic:
apply Finite.of_injective (f := fun a ↦ a.1.1)

Premises used: Finite.of_injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
A : X.Subcomplex
d : ℕ
h : X.HasDimensionLT d
i : ℕ
hi : i < d
x : X _⦋i⦌
property : Membership.mem (γ := Set (X _⦋i⦌)) (A.obj (Opposite.op ⦋i⦌)) x
property_1 :
  Membership.mem (γ := Set (A.toSSet _⦋i⦌)) (A.toSSet.nonDegenerate i)
    (Subtype.mk (p := fun (x : X _⦋i⦌) ↦ Membership.mem (γ := Set (X _⦋i⦌)) (A.obj (Opposite.op ⦋i⦌)) x) x property)
property_2 :
  Membership.mem (γ := Set (X _⦋i⦌)) (A.obj (Opposite.op ⦋i⦌))
    ((fun (a : (↑(A.toSSet.nonDegenerate i) : Type u)) ↦ (↑(↑a : A.toSSet _⦋i⦌) : X _⦋i⦌))
      (Subtype.mk (p := fun (x : A.toSSet _⦋i⦌) ↦
        Membership.mem (γ := Set (A.toSSet _⦋i⦌)) (A.toSSet.nonDegenerate i) x)
        (Subtype.mk (p := fun (x : X _⦋i⦌) ↦ Membership.mem (γ := Set (X _⦋i⦌)) (A.obj (Opposite.op ⦋i⦌)) x) x property)
        property_1))
property_3 :
  Membership.mem (γ := Set (A.toSSet _⦋i⦌)) (A.toSSet.nonDegenerate i)
    (Subtype.mk (p := fun (x : X _⦋i⦌) ↦ Membership.mem (γ := Set (X _⦋i⦌)) (A.obj (Opposite.op ⦋i⦌)) x)
      ((fun (a : (↑(A.toSSet.nonDegenerate i) : Type u)) ↦ (↑(↑a : A.toSSet _⦋i⦌) : X _⦋i⦌))
        (Subtype.mk (p := fun (x : A.toSSet _⦋i⦌) ↦
          Membership.mem (γ := Set (A.toSSet _⦋i⦌)) (A.toSSet.nonDegenerate i) x)
          (Subtype.mk (p := fun (x : X _⦋i⦌) ↦ Membership.mem (γ := Set (X _⦋i⦌)) (A.obj (Opposite.op ⦋i⦌)) x) x
            property)
          property_1))
      property_2)
⊢ Subtype.mk (p := fun (x : A.toSSet _⦋i⦌) ↦ Membership.mem (γ := Set (A.toSSet _⦋i⦌)) (A.toSSet.nonDegenerate i) x)
      (Subtype.mk (p := fun (x : X _⦋i⦌) ↦ Membership.mem (γ := Set (X _⦋i⦌)) (A.obj (Opposite.op ⦋i⦌)) x) x property)
      property_1 =
    Subtype.mk (p := fun (x : A.toSSet _⦋i⦌) ↦ Membership.mem (γ := Set (A.toSSet _⦋i⦌)) (A.toSSet.nonDegenerate i) x)
      (Subtype.mk (p := fun (x : X _⦋i⦌) ↦ Membership.mem (γ := Set (X _⦋i⦌)) (A.obj (Opposite.op ⦋i⦌)) x)
        ((fun (a : (↑(A.toSSet.nonDegenerate i) : Type u)) ↦ (↑(↑a : A.toSSet _⦋i⦌) : X _⦋i⦌))
          (Subtype.mk (p := fun (x : A.toSSet _⦋i⦌) ↦
            Membership.mem (γ := Set (A.toSSet _⦋i⦌)) (A.toSSet.nonDegenerate i) x)
            (Subtype.mk (p := fun (x : X _⦋i⦌) ↦ Membership.mem (γ := Set (X _⦋i⦌)) (A.obj (Opposite.op ⦋i⦌)) x) x
              property)
            property_1))
        property_2)
      property_3

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
inst : Y.Finite
f : X ⟶ Y
hf : Mono f
obtain : ∀ (d : ℕ), Y.HasDimensionLT d → X.Finite
⊢ X.Finite

Tactic:
obtain ⟨d, _⟩ := Y.hasDimensionLT_of_finite

Premises used: SSet.hasDimensionLT_of_finite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
inst : Y.Finite
f : X ⟶ Y
hf : Mono f
d : ℕ
h : Y.HasDimensionLT d
⊢ X.HasDimensionLT d

Tactic:
have := hasDimensionLT_of_mono f d
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
inst : Y.Finite
f : X ⟶ Y
hf : Mono f
d : ℕ
h : Y.HasDimensionLT d
this : X.HasDimensionLT d
⊢ X.Finite

Tactic:
finite_of_hasDimensionLT _ d
    (fun _ _ ↦ Finite.of_injective _
      ((injective_of_mono (f.app _)).comp Subtype.val_injective))

Premises used: CategoryTheory.ConcreteCategory.hom, Subtype.val_injective, SSet.finite_of_hasDimensionLT, Function.comp, Function.Injective.comp, SimplexCategory.mk, Opposite.op, CategoryTheory.injective_of_mono, Subtype.val, DFunLike.coe, CategoryTheory.NatTrans.app, Finite.of_injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
inst : Y.Finite
f : X ⟶ Y
hf : Mono f
d : ℕ
h : Y.HasDimensionLT d
this : X.HasDimensionLT d
⊢ X.Finite

Tactic:
exact finite_of_hasDimensionLT _ d
    (fun _ _ ↦ Finite.of_injective _
      ((injective_of_mono (f.app _)).comp Subtype.val_injective))

Premises used: CategoryTheory.ConcreteCategory.hom, Subtype.val_injective, SSet.finite_of_hasDimensionLT, Function.comp, Function.Injective.comp, SimplexCategory.mk, Opposite.op, CategoryTheory.injective_of_mono, Subtype.val, DFunLike.coe, CategoryTheory.NatTrans.app, Finite.of_injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
hf : Epi f
obtain : ∀ (d : ℕ), X.HasDimensionLT d → Y.Finite
⊢ Y.Finite

Tactic:
obtain ⟨d, _⟩ := X.hasDimensionLT_of_finite

Premises used: SSet.hasDimensionLT_of_finite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h : X.HasDimensionLT d
⊢ Y.HasDimensionLT d

Tactic:
have := hasDimensionLT_of_epi f d
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h : X.HasDimensionLT d
this : Y.HasDimensionLT d
⊢ Y.Finite

Tactic:
finite_of_hasDimensionLT _ d (fun i hi ↦ ?_)

Premises used: SSet.finite_of_hasDimensionLT
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h : X.HasDimensionLT d
this : Y.HasDimensionLT d
refine : ∀ (i : ℕ) (hi : i < d), Finite.{u + 1} (↑(Y.nonDegenerate i) : Type u)
⊢ Y.Finite

Tactic:
refine finite_of_hasDimensionLT _ d (fun i hi ↦ ?_)

Premises used: SSet.finite_of_hasDimensionLT
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
rw :
  ∀ (hf : ∀ (k : SimplexCategoryᵒᵖ), Epi (f.app k)) (d : ℕ),
    X.HasDimensionLT d → ∀ (this : Y.HasDimensionLT d) (i : ℕ) (hi : i < d), Finite.{u + 1} (Y _⦋i⦌)
⊢ Finite.{u + 1} (Y _⦋i⦌)

Tactic:
rw [NatTrans.epi_iff_epi_app] at hf

Premises used: CategoryTheory.NatTrans.epi_iff_epi_app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
hf : ∀ (k : SimplexCategoryᵒᵖ), Epi (f.app k)
d : ℕ
h : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
⊢ ∀ (k : SimplexCategoryᵒᵖ),
    Function.Surjective (α := X.obj k) (β := Y.obj k)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app k)) : (a : X.obj k) → Y.obj k)

Tactic:
simp only [epi_iff_surjective] at hf

Premises used: CategoryTheory.epi_iff_surjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
d : ℕ
h : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
hf :
  ∀ (k : SimplexCategoryᵒᵖ),
    Function.Surjective (α := X.obj k) (β := Y.obj k)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app k)) : (a : X.obj k) → Y.obj k)
⊢ Finite.{u + 1} (Y _⦋i⦌)

Tactic:
Finite.of_surjective _ (hf _)

Premises used: Finite.of_surjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
d : ℕ
h : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
hf :
  ∀ (k : SimplexCategoryᵒᵖ),
    Function.Surjective (α := X.obj k) (β := Y.obj k)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app k)) : (a : X.obj k) → Y.obj k)
⊢ Finite.{u + 1} (Y _⦋i⦌)

Tactic:
exact Finite.of_surjective _ (hf _)

Premises used: Finite.of_surjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
⊢ Finite.{u + 1} (Y _⦋i⦌)

Tactic:
have : Finite (Y _⦋i⦌) := by
    rw [NatTrans.epi_iff_epi_app] at hf
    simp only [epi_iff_surjective] at hf
    exact Finite.of_surjective _ (hf _)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h : X.HasDimensionLT d
this_1 : Y.HasDimensionLT d
i : ℕ
hi : i < d
this : Finite.{u + 1} (Y _⦋i⦌)
⊢ Finite.{u + 1} (↑(Y.nonDegenerate i) : Type u)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
e : X ≅ Y
inst : X.Finite
⊢ Y.Finite

Tactic:
finite_of_mono e.inv

Premises used: SSet.finite_of_mono, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
e : X ≅ Y
⊢ X.Finite ↔ Y.Finite

Tactic:
⟨fun _ ↦ finite_of_iso e, fun _ ↦ finite_of_iso e.symm⟩

Premises used: Iff.intro, CategoryTheory.Iso.symm, SSet.finite_of_iso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
⊢ SSet.Finite.{u} (Subcomplex.toSSet (X := X) ⊤) ↔ X.Finite

Tactic:
finite_iff_of_iso (Subcomplex.topIso X)

Premises used: SSet.finite_iff_of_iso, SSet.Subcomplex.topIso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X Y : SSet
f : Y ⟶ X
inst : Y.Finite
⊢ SSet.Finite.{u} (Subcomplex.range f).toSSet

Tactic:
finite_of_epi (Subcomplex.toRange f)

Premises used: SSet.Subcomplex.toRange, SSet.finite_of_epi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
⊢ SSet.Finite.{u} (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)) ↔ ∀ (i : ι), SSet.Finite.{u} (A i).toSSet

Tactic:
⟨fun h i ↦ finite_of_mono (Subcomplex.homOfLE (le_iSup A i)), fun h ↦ ⟨?_⟩⟩

Premises used: SSet.finite_of_mono, le_iSup, SSet.Finite.mk, SSet.Subcomplex.homOfLE, Iff.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
refine : ∀ (h : ∀ (i : ι), SSet.Finite.{u} (A i).toSSet), Finite.{u + 1} (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N
⊢ SSet.Finite.{u} (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)) ↔ ∀ (i : ι), SSet.Finite.{u} (A i).toSSet

Tactic:
refine ⟨fun h i ↦ finite_of_mono (Subcomplex.homOfLE (le_iSup A i)), fun h ↦ ⟨?_⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), SSet.Finite.{u} (A i).toSSet
x : (i : ι) × (A i).toSSet.N
i : ι
s : (A i).toSSet.N
⊢ Membership.mem (α := Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋s.dim⦌) (γ :=
    Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋s.dim⦌))
    ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate s.dim)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) ((A i).toSSet _⦋s.dim⦌)) → (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))
        s.simplex :
      (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))

Tactic:
simpa only [nonDegenerate_iff_of_mono] using s.nonDegenerate

Premises used: SSet.nonDegenerate_iff_of_mono, SSet.N.nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), SSet.Finite.{u} (A i).toSSet
refine :
  Function.Surjective (β := (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N) fun (x : (i : ι) × (A i).toSSet.N) ↦
    match (motive := (i : ι) × (A i).toSSet.N → (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N) x with
    | ⟨i, s⟩ =>
      N.mk
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌)) :
            (a : (fun (X : Type u) ↦ X) ((A i).toSSet _⦋s.dim⦌)) → (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))
          s.simplex)
        ⋯
⊢ Finite.{u + 1} (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N

Tactic:
refine Finite.of_surjective (f := fun (⟨i, s⟩ : Σ (i : ι), (A i).toSSet.N) ↦
    N.mk ((Subcomplex.homOfLE (le_iSup A i)).app _ s.simplex)
      (by simpa only [nonDegenerate_iff_of_mono] using s.nonDegenerate)) ?_

Premises used: Finite.of_surjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), SSet.Finite.{u} (A i).toSSet
s : (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N
obtain :
  ∀ (d : ℕ) (s : X _⦋d⦌) (h₁ : Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) s)
    (h₂ :
      Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
        ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d)
        (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
          Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁)),
    ∃ (a : (i : ι) × (A i).toSSet.N),
      (fun (x : (i : ι) × (A i).toSSet.N) ↦
            (match (motive := (i : ι) × (A i).toSSet.N → (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N) x with
              | ⟨i, s⟩ =>
                N.mk
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌)) :
                      (a : (fun (X : Type u) ↦ X) ((A i).toSSet _⦋s.dim⦌)) →
                        (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))
                    s.simplex)
                  ⋯ :
              (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N))
          a =
        N.mk
          (↑(Subtype.mk (p := fun (x : Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌) ↦
                Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
                  ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d) x)
                (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
                  Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁)
                h₂) :
            (⨆ (i : ι), A i).toSSet _⦋d⦌)
          ⋯
⊢ ∃ (a : (i : ι) × (A i).toSSet.N),
    (fun (x : (i : ι) × (A i).toSSet.N) ↦
          (match (motive := (i : ι) × (A i).toSSet.N → (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N) x with
            | ⟨i, s⟩ =>
              N.mk
                ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌)) :
                    (a : (fun (X : Type u) ↦ X) ((A i).toSSet _⦋s.dim⦌)) →
                      (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))
                  s.simplex)
                ⋯ :
            (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N))
        a =
      s

Tactic:
obtain ⟨d, ⟨⟨s, h₁⟩, h₂⟩, rfl⟩ := s.mk_surjective

Premises used: SSet.N.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), SSet.Finite.{u} (A i).toSSet
d : ℕ
s : X _⦋d⦌
h₁ : Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) s
h₂ :
  Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
    ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d)
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
      Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁)
⊢ ∃ (i : ι), Membership.mem (γ := Set (X _⦋d⦌)) ((A i).obj (Opposite.op ⦋d⦌)) s

Tactic:
simp only [Subfunctor.iSup_obj, Set.mem_iUnion] at h₁

Premises used: Set.mem_iUnion, CategoryTheory.Subfunctor.iSup_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), SSet.Finite.{u} (A i).toSSet
d : ℕ
s : X _⦋d⦌
h₁_1 : Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) s
h₂ :
  Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
    ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d)
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
      Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁_1)
h₁ : ∃ (i : ι), Membership.mem (γ := Set (X _⦋d⦌)) ((A i).obj (Opposite.op ⦋d⦌)) s
obtain :
  ∀ (i : ι) (hi : Membership.mem (γ := Set (X _⦋d⦌)) ((A i).obj (Opposite.op ⦋d⦌)) s),
    ∃ (a : (i : ι) × (A i).toSSet.N),
      (fun (x : (i : ι) × (A i).toSSet.N) ↦
            (match (motive := (i : ι) × (A i).toSSet.N → (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N) x with
              | ⟨i, s⟩ =>
                N.mk
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌)) :
                      (a : (fun (X : Type u) ↦ X) ((A i).toSSet _⦋s.dim⦌)) →
                        (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))
                    s.simplex)
                  ⋯ :
              (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N))
          a =
        N.mk
          (↑(Subtype.mk (p := fun (x : Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌) ↦
                Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
                  ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d) x)
                (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
                  Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁_1)
                h₂) :
            (⨆ (i : ι), A i).toSSet _⦋d⦌)
          ⋯
⊢ ∃ (a : (i : ι) × (A i).toSSet.N),
    (fun (x : (i : ι) × (A i).toSSet.N) ↦
          (match (motive := (i : ι) × (A i).toSSet.N → (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N) x with
            | ⟨i, s⟩ =>
              N.mk
                ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌)) :
                    (a : (fun (X : Type u) ↦ X) ((A i).toSSet _⦋s.dim⦌)) →
                      (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))
                  s.simplex)
                ⋯ :
            (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N))
        a =
      N.mk
        (↑(Subtype.mk (p := fun (x : Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌) ↦
              Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
                ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d) x)
              (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
                Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁_1)
              h₂) :
          (⨆ (i : ι), A i).toSSet _⦋d⦌)
        ⋯

Tactic:
obtain ⟨i, hi⟩ := h₁
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), SSet.Finite.{u} (A i).toSSet
d : ℕ
s : X _⦋d⦌
h₁ : Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) s
h₂_1 :
  Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
    ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d)
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
      Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁)
h₂ :
  (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦
          Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁) :
      X _⦋d⦌) ∈
    X.nonDegenerate d
i : ι
hi : Membership.mem (γ := Set (X _⦋d⦌)) ((A i).obj (Opposite.op ⦋d⦌)) s
rwa rwa₁ rwa₂ rwa₃ :
  (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ Membership.mem (γ := Set (X _⦋d⦌)) ((A i).obj (Opposite.op ⦋d⦌)) x) s hi) :
      X _⦋d⦌) ∈
    X.nonDegenerate d
⊢ Membership.mem (γ := Set ((A i).toSSet _⦋d⦌)) ((A i).toSSet.nonDegenerate d)
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦ Membership.mem (γ := Set (X _⦋d⦌)) ((A i).obj (Opposite.op ⦋d⦌)) x) s hi)

Tactic:
rwa [Subcomplex.mem_nonDegenerate_iff]

Premises used: SSet.Subcomplex.mem_nonDegenerate_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), SSet.Finite.{u} (A i).toSSet
d : ℕ
s : X _⦋d⦌
h₁ : Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) s
h₂_1 :
  Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
    ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d)
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
      Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁)
h₂ :
  (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦
          Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁) :
      X _⦋d⦌) ∈
    X.nonDegenerate d
i : ι
hi : Membership.mem (γ := Set (X _⦋d⦌)) ((A i).obj (Opposite.op ⦋d⦌)) s
⊢ ∃ (a : (i : ι) × (A i).toSSet.N),
    (fun (x : (i : ι) × (A i).toSSet.N) ↦
          (match (motive := (i : ι) × (A i).toSSet.N → (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N) x with
            | ⟨i, s⟩ =>
              N.mk
                ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌)) :
                    (a : (fun (X : Type u) ↦ X) ((A i).toSSet _⦋s.dim⦌)) →
                      (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))
                  s.simplex)
                ⋯ :
            (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N))
        a =
      N.mk
        (↑(Subtype.mk (p := fun (x : Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌) ↦
              Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
                ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d) x)
              (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
                Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁)
              h₂_1) :
          (⨆ (i : ι), A i).toSSet _⦋d⦌)
        ⋯

Tactic:
exact ⟨⟨i, N.mk ⟨s, hi⟩ (by rwa [Subcomplex.mem_nonDegenerate_iff])⟩, rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K : SSet
Δ : SimplexCategoryᵒᵖ
x : (tensorObj (𝒞 := Functor.category) ((𝟙_ SSet) (𝒞 := Functor.category)) K).obj Δ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (λ_ (K.obj Δ))) : (a : 𝟙_ (Type u) ⊗ K.obj Δ) → K.obj Δ) x = x.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K : SSet
Δ : SimplexCategoryᵒᵖ
x : K.obj Δ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (λ_ (K.obj Δ))) : (a : K.obj Δ) → 𝟙_ (Type u) ⊗ K.obj Δ) x =
    (PUnit.unit, x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K : SSet
Δ : SimplexCategoryᵒᵖ
x : (tensorObj (𝒞 := Functor.category) K ((𝟙_ SSet) (𝒞 := Functor.category))).obj Δ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (ρ_ (K.obj Δ))) : (a : K.obj Δ ⊗ 𝟙_ (Type u)) → K.obj Δ) x = x.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K : SSet
Δ : SimplexCategoryᵒᵖ
x : K.obj Δ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (ρ_ (K.obj Δ))) : (a : K.obj Δ) → K.obj Δ ⊗ 𝟙_ (Type u)) x =
    (x, PUnit.unit)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K K' L L' : SSet
f : K ⟶ K'
g : L ⟶ L'
Δ : SimplexCategoryᵒᵖ
x : (tensorObj (𝒞 := Functor.category) K L).obj Δ
⊢ Eq (α := tensorObj (𝒞 := types) (K'.obj Δ) (L'.obj Δ))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ ⊗ₘ g.app Δ) : (a : K.obj Δ ⊗ L.obj Δ) → K'.obj Δ ⊗ L'.obj Δ) x :
      tensorObj (𝒞 := types) (K'.obj Δ) (L'.obj Δ))
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ) : (a : K.obj Δ) → K'.obj Δ) x.1,
        (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app Δ) : (a : L.obj Δ) → L'.obj Δ) x.2) :
      K'.obj Δ × L'.obj Δ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K L L' : SSet
g : L ⟶ L'
Δ : SimplexCategoryᵒᵖ
x : (tensorObj (𝒞 := Functor.category) K L).obj Δ
⊢ Eq (α := tensorObj (𝒞 := types) (K.obj Δ) (L'.obj Δ))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.obj Δ ◁ g.app Δ) : (a : K.obj Δ ⊗ L.obj Δ) → K.obj Δ ⊗ L'.obj Δ) x :
      tensorObj (𝒞 := types) (K.obj Δ) (L'.obj Δ))
    ((x.1, (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app Δ) : (a : L.obj Δ) → L'.obj Δ) x.2) : K.obj Δ × L'.obj Δ)

Tactic:
rfl

Premises used: rfl