awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
h : Mono f
h_1 : Epi f
X_1 : SimplexCategoryᵒᵖ
left :
  Function.Injective (α := (fun (X : Type u) ↦ X) (X.obj X_1)) (β := (fun (X : Type u) ↦ X) (Y.obj X_1))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X_1)) :
      (a : (fun (X : Type u) ↦ X) (X.obj X_1)) → (fun (X : Type u) ↦ X) (Y.obj X_1))
right :
  Function.Surjective (α := (fun (X : Type u) ↦ X) (X.obj X_1)) (β := (fun (X : Type u) ↦ X) (Y.obj X_1))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X_1)) :
      (a : (fun (X : Type u) ↦ X) (X.obj X_1)) → (fun (X : Type u) ↦ X) (Y.obj X_1))
⊢ Function.Bijective (α := (fun (X : Type u) ↦ X) (X.obj X_1)) (β := (fun (X : Type u) ↦ X) (Y.obj X_1))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X_1)) :
      (a : (fun (X : Type u) ↦ X) (X.obj X_1)) → (fun (X : Type u) ↦ X) (Y.obj X_1))

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
h : Mono f
h_1 : Epi f
X_1 : SimplexCategoryᵒᵖ
left : Mono (f.app X_1)
⊢ Function.Injective (α := (fun (X : Type u) ↦ X) (X.obj X_1)) (β := (fun (X : Type u) ↦ X) (Y.obj X_1))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X_1)) :
      (a : (fun (X : Type u) ↦ X) (X.obj X_1)) → (fun (X : Type u) ↦ X) (Y.obj X_1))

Tactic:
rw [← mono_iff_injective]

Premises used: CategoryTheory.mono_iff_injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
h : Mono f
h_1 : Epi f
X_1 : SimplexCategoryᵒᵖ
⊢ Mono (f.app X_1)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
h : Mono f
h_1 : Epi f
X_1 : SimplexCategoryᵒᵖ
right : Epi (f.app X_1)
⊢ Function.Surjective (α := (fun (X : Type u) ↦ X) (X.obj X_1)) (β := (fun (X : Type u) ↦ X) (Y.obj X_1))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X_1)) :
      (a : (fun (X : Type u) ↦ X) (X.obj X_1)) → (fun (X : Type u) ↦ X) (Y.obj X_1))

Tactic:
rw [← epi_iff_surjective]

Premises used: CategoryTheory.epi_iff_surjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
h : Mono f
h_1 : Epi f
X_1 : SimplexCategoryᵒᵖ
⊢ Epi (f.app X_1)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
⊢ Mono A.ι

Tactic:
inferInstanceAs (Mono (Subfunctor.ι A))

Premises used: _private.0.SSet.Subcomplex.instMonoι._proof_1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
S₁ S₂ : X.Subcomplex
h : S₁ ≤ S₂
S₃ : X.Subcomplex
h' : S₂ ≤ S₃
⊢ homOfLE h ≫ homOfLE h' = homOfLE ⋯

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, Set.Mem, CategoryTheory.Subfunctor.homOfLe, TypeCat.Fun.comp, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
S₁ S₂ : X.Subcomplex
h : S₁ ≤ S₂
⊢ S₁ ≤ S₁

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
S₁ : X.Subcomplex
⊢ homOfLE ⋯ = 𝟙 S₁.toSSet

Tactic:
rfl

Premises used: CategoryTheory.Subfunctor.homOfLe, TypeCat.Fun.id, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
S₁ S₂ : X.Subcomplex
h : S₁ ≤ S₂
Δ : SimplexCategoryᵒᵖ
x : (↑(S₁.obj Δ) : Type u)
⊢ (↑(({
              toFun := fun (x : (↑(S₁.obj Δ) : Type u)) ↦
                Subtype.mk (p := fun (x : X.obj Δ) ↦ x ∈ S₂.obj Δ) (↑x : X.obj Δ) ⋯ } :
            (a : (↑(S₁.obj Δ) : Type u)) → (↑(S₂.obj Δ) : Type u))
          x) :
      X.obj Δ) =
    (↑x : X.obj Δ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
S₁ S₂ : X.Subcomplex
h : S₁ ≤ S₂
⊢ homOfLE h ≫ S₂.ι = S₁.ι

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, Set.Mem, TypeCat.Fun.comp, CategoryTheory.Subfunctor.ι, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
S₁ S₂ : X.Subcomplex
h : S₁ ≤ S₂
⊢ Mono (homOfLE h)

Tactic:
mono_of_mono_fac (homOfLE_ι h)

Premises used: SSet.Subcomplex.homOfLE_ι, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
⊢ (topIso X).hom = ι ⊤

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, CategoryTheory.Subfunctor.ι, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
⊢ (topIso X).inv ≫ Subfunctor.ι ⊤ = 𝟙 X

Tactic:
rfl

Premises used: TypeCat.Fun.id, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
x x_1 : toSSet (X := X) ⊥ ⟶ Y
w :
  ∀ (n : SimplexCategoryᵒᵖ) (val : X.obj n) (h : Membership.mem (γ := Set (X.obj n)) (Subfunctor.obj ⊥ n) val),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (x.app n)).toFun
        (Subtype.mk (p := fun (x : X.obj n) ↦ Membership.mem (γ := Set (X.obj n)) (Subfunctor.obj ⊥ n) x) val h) =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (x_1.app n)).toFun
        (Subtype.mk (p := fun (x : X.obj n) ↦ Membership.mem (γ := Set (X.obj n)) (Subfunctor.obj ⊥ n) x) val h)
⊢ x = x_1

Tactic:
ext _ ⟨_, h⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
x x_1 : toSSet (X := X) ⊥ ⟶ Y
n : SimplexCategoryᵒᵖ
val : X.obj n
h : Membership.mem (γ := Set (X.obj n)) (Subfunctor.obj ⊥ n) val
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (x.app n)).toFun
      (Subtype.mk (p := fun (x : X.obj n) ↦ Membership.mem (γ := Set (X.obj n)) (Subfunctor.obj ⊥ n) x) val h) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (x_1.app n)).toFun
      (Subtype.mk (p := fun (x : X.obj n) ↦ Membership.mem (γ := Set (X.obj n)) (Subfunctor.obj ⊥ n) x) val h)

Tactic:
tauto
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
x : SimplexCategoryᵒᵖ
x_1 : (toSSet (X := X) ⊥).obj x
val : X.obj x
h : Membership.mem (γ := Set (X.obj x)) (Subfunctor.obj ⊥ x) val
⊢ Y.obj x

Tactic:
tauto
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
x x_1 : SimplexCategoryᵒᵖ
x_2 : x ⟶ x_1
h :
  ∀ (val : X.obj x) (h : Membership.mem (γ := Set (X.obj x)) (Subfunctor.obj ⊥ x) val),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((toSSet (X := X) ⊥).map x_2 ≫
            ↾fun (x : (toSSet (X := X) ⊥).obj x_1) ↦
              match (motive := (toSSet (X := X) ⊥).obj x_1 → Y.obj x_1) x with
              | ⟨val, h⟩ => False.elim ⋯))
        (Subtype.mk (p := fun (x_3 : X.obj x) ↦ Membership.mem (γ := Set (X.obj x)) (Subfunctor.obj ⊥ x) x_3) val h) =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (x_3 : (toSSet (X := X) ⊥).obj x) ↦
              match (motive := (toSSet (X := X) ⊥).obj x → Y.obj x) x_3 with
              | ⟨val, h⟩ => False.elim ⋯) ≫
            Y.map x_2))
        (Subtype.mk (p := fun (x_3 : X.obj x) ↦ Membership.mem (γ := Set (X.obj x)) (Subfunctor.obj ⊥ x) x_3) val h)
⊢ ((toSSet (X := X) ⊥).map x_2 ≫
      ↾fun (x : (toSSet (X := X) ⊥).obj x_1) ↦
        match (motive := (toSSet (X := X) ⊥).obj x_1 → Y.obj x_1) x with
        | ⟨val, h⟩ => False.elim ⋯) =
    (↾fun (x_3 : (toSSet (X := X) ⊥).obj x) ↦
        match (motive := (toSSet (X := X) ⊥).obj x → Y.obj x) x_3 with
        | ⟨val, h⟩ => False.elim ⋯) ≫
      Y.map x_2

Tactic:
ext ⟨_, h⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
x x_1 : SimplexCategoryᵒᵖ
x_2 : x ⟶ x_1
val : X.obj x
h : Membership.mem (γ := Set (X.obj x)) (Subfunctor.obj ⊥ x) val
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((toSSet (X := X) ⊥).map x_2 ≫
          ↾fun (x : (toSSet (X := X) ⊥).obj x_1) ↦
            match (motive := (toSSet (X := X) ⊥).obj x_1 → Y.obj x_1) x with
            | ⟨val, h⟩ => False.elim ⋯))
      (Subtype.mk (p := fun (x_3 : X.obj x) ↦ Membership.mem (γ := Set (X.obj x)) (Subfunctor.obj ⊥ x) x_3) val h) =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x_3 : (toSSet (X := X) ⊥).obj x) ↦
            match (motive := (toSSet (X := X) ⊥).obj x → Y.obj x) x_3 with
            | ⟨val, h⟩ => False.elim ⋯) ≫
          Y.map x_2))
      (Subtype.mk (p := fun (x_3 : X.obj x) ↦ Membership.mem (γ := Set (X.obj x)) (Subfunctor.obj ⊥ x) x_3) val h)

Tactic:
tauto
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
⊢ ∀ (a : toSSet (X := X) ⊥ ⟶ Y),
    a =
      {
        app := fun (x : SimplexCategoryᵒᵖ) ↦
          ↾fun (x_1 : (toSSet (X := X) ⊥).obj x) ↦
            match (motive := (toSSet (X := X) ⊥).obj x → Y.obj x) x_1 with
            | ⟨val, h⟩ => False.elim ⋯,
        naturality := ⋯ }

Tactic:
subsingleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
x : X _⦋0⦌
w :
  ∀ (n : SimplexCategoryᵒᵖ) (u : Opposite.unop n ⟶ Opposite.unop (Opposite.op ⦋0⦌)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((ofSimplex x).ι.app n)).toFun
        (Subtype.mk (p := fun (x_1 : X.obj n) ↦ x_1 ∈ (ofSimplex x).obj n)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Opposite.op u)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X.obj n))
            x)
          ⋯) =
      TypeCat.Fun.toFun (X := (ofSimplex x).toSSet.obj n)
        (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (const x) n))
        (Subtype.mk (p := fun (x_1 : X.obj n) ↦ x_1 ∈ (ofSimplex x).obj n)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Opposite.op u)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X.obj n))
            x)
          ⋯)
⊢ (ofSimplex x).ι = const x

Tactic:
ext n ⟨_, ⟨u⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
x : X _⦋0⦌
n : SimplexCategoryᵒᵖ
u : Opposite.unop n ⟶ Opposite.unop (Opposite.op ⦋0⦌)
w :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((ofSimplex x).ι.app n)).toFun
      (Subtype.mk (p := fun (x_1 : X.obj n) ↦ x_1 ∈ (ofSimplex x).obj n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.map (Opposite.op ((Opposite.unop n).const (Opposite.unop (Opposite.op ⦋0⦌)) 0))) :
            (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X.obj n))
          x)
        ⋯) =
    TypeCat.Fun.toFun (X := (ofSimplex x).toSSet.obj n)
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (const x) n))
      (Subtype.mk (p := fun (x_1 : X.obj n) ↦ x_1 ∈ (ofSimplex x).obj n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.map (Opposite.op ((Opposite.unop n).const (Opposite.unop (Opposite.op ⦋0⦌)) 0))) :
            (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X.obj n))
          x)
        ⋯)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((ofSimplex x).ι.app n)).toFun
      (Subtype.mk (p := fun (x_1 : X.obj n) ↦ x_1 ∈ (ofSimplex x).obj n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Opposite.op u)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X.obj n))
          x)
        ⋯) =
    TypeCat.Fun.toFun (X := (ofSimplex x).toSSet.obj n)
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (const x) n))
      (Subtype.mk (p := fun (x_1 : X.obj n) ↦ x_1 ∈ (ofSimplex x).obj n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Opposite.op u)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X.obj n))
          x)
        ⋯)

Tactic:
obtain rfl := Subsingleton.elim u (SimplexCategory.const _ _ 0)

Premises used: SimplexCategory.const, Subsingleton.elim, OfNat.ofNat, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
x : X _⦋0⦌
n : SimplexCategoryᵒᵖ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((ofSimplex x).ι.app n)).toFun
      (Subtype.mk (p := fun (x_1 : X.obj n) ↦ x_1 ∈ (ofSimplex x).obj n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.map (Opposite.op ((Opposite.unop n).const (Opposite.unop (Opposite.op ⦋0⦌)) 0))) :
            (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X.obj n))
          x)
        ⋯) =
    TypeCat.Fun.toFun (X := (ofSimplex x).toSSet.obj n)
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (const x) n))
      (Subtype.mk (p := fun (x_1 : X.obj n) ↦ x_1 ∈ (ofSimplex x).obj n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.map (Opposite.op ((Opposite.unop n).const (Opposite.unop (Opposite.op ⦋0⦌)) 0))) :
            (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X.obj n))
          x)
        ⋯)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ Membership.mem (γ := Set (X _⦋n⦌)) ((ofSimplex x).obj (Opposite.op ⦋n⦌)) x

Tactic:
Subfunctor.mem_ofSection_obj x

Premises used: Set.Mem, CategoryTheory.Subfunctor.mem_ofSection_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
A : X.Subcomplex
⊢ ofSimplex x ≤ A ↔ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) x

Tactic:
Subfunctor.ofSection_le_iff _ _

Premises used: CategoryTheory.Subfunctor.ofSection_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
y : X.obj m
dsimp :
  (∃ (f : Opposite.op ⦋n⦌ ⟶ m), (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f) : (a : X _⦋n⦌) → X.obj m) x = y) ↔
    ∃ (f : Opposite.unop m ⟶ ⦋n⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋n⦌) → X.obj m) x = y
⊢ y ∈ (ofSimplex x).obj m ↔
    ∃ (f : Opposite.unop m ⟶ ⦋n⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X.obj (Opposite.op (Opposite.unop m))))
          x =
        y

Tactic:
dsimp [ofSimplex, Subfunctor.ofSection]

Premises used: SSet.Subcomplex.ofSimplex, CategoryTheory.Subfunctor.ofSection
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
y : X.obj m
⊢ (∃ (f : Opposite.op ⦋n⦌ ⟶ m), (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f) : (a : X _⦋n⦌) → X.obj m) x = y) ↔
    ∃ (f : Opposite.unop m ⟶ ⦋n⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋n⦌) → X.obj m) x = y

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
x : X _⦋m⦌
simp :
  Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌)) ((ofSimplex x).obj (Opposite.op ⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) x : X _⦋n⦌)
⊢ ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x) ≤
    ofSimplex x

Tactic:
simp only [Subfunctor.ofSection_le_iff]

Premises used: CategoryTheory.Subfunctor.ofSection_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
x : X _⦋m⦌
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) x : X _⦋n⦌)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
x : X _⦋m⦌
⊢ Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌)) ((ofSimplex x).obj (Opposite.op ⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) x : X _⦋n⦌)

Tactic:
exact ⟨f.op, by simp⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
x : X _⦋m⦌
⊢ ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x) =
    ofSimplex x

Tactic:
le_antisymm (ofSimplex_map_le f x) ?_

Premises used: SSet.Subcomplex.ofSimplex_map_le, le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
x : X _⦋m⦌
refine :
  ofSimplex x ≤
    ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x)
⊢ ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x) =
    ofSimplex x

Tactic:
refine le_antisymm (ofSimplex_map_le f x) ?_

Premises used: SSet.Subcomplex.ofSimplex_map_le, le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
x : X _⦋m⦌
simp :
  Membership.mem (γ := Set (X _⦋m⦌))
    (Subfunctor.obj
      (ofSimplex (n := n) ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) x))
      (Opposite.op ⦋m⦌))
    x
⊢ ofSimplex x ≤
    ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x)

Tactic:
simp only [Subfunctor.ofSection_le_iff]

Premises used: CategoryTheory.Subfunctor.ofSection_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
x : X _⦋m⦌
⊢ IsSplitEpi f

Tactic:
have := isSplitEpi_of_epi f
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
x : X _⦋m⦌
this : IsSplitEpi f
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) x : X _⦋n⦌) =
    x

Tactic:
simp [← Functor.map_comp_apply, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
x : X _⦋m⦌
this : IsSplitEpi f
⊢ Membership.mem (γ := Set (X _⦋m⦌))
    (Subfunctor.obj
      (ofSimplex (n := n) ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) x))
      (Opposite.op ⦋m⦌))
    x

Tactic:
exact ⟨(section_ f).op, by simp [← Functor.map_comp_apply, ← op_comp]⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
⊢ toRange f ≫ (range f).ι = f

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
x : X.obj Δ
⊢ Eq (α := Y.obj Δ)
    ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange f).app Δ) :
              (a : X.obj Δ) → (↑(Set.range (⇑(ConcreteCategory.hom (f.app Δ)) : (a : X.obj Δ) → Y.obj Δ)) : Type u))
            x) :
        Y.obj Δ) :
      Y.obj Δ)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ) : (a : X.obj Δ) → Y.obj Δ) x : Y.obj Δ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
⊢ Epi (toRange f)

Tactic:
inferInstanceAs (Epi (Subfunctor.toRange f))

Premises used: _private.0.SSet.Subcomplex.instEpiToRange._proof_1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
⊢ Mono (toRange f)

Tactic:
mono_of_mono_fac (toRange_ι f)

Premises used: SSet.Subcomplex.toRange_ι, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
⊢ IsIso (toRange f)

Tactic:
isIso_of_mono_of_epi _

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
rw : (∀ (x : SimplexCategoryᵒᵖ), (range f).obj x = Subfunctor.obj ⊤ x) ↔ ∀ (k : SimplexCategoryᵒᵖ), Epi (f.app k)
⊢ range f = ⊤ ↔ Epi f

Tactic:
rw [NatTrans.epi_iff_epi_app, Subfunctor.ext_iff, funext_iff]

Premises used: CategoryTheory.NatTrans.epi_iff_epi_app, funext_iff, CategoryTheory.Subfunctor.ext_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
⊢ (∀ (x : SimplexCategoryᵒᵖ), (range f).obj x = Subfunctor.obj ⊤ x) ↔ ∀ (k : SimplexCategoryᵒᵖ), Epi (f.app k)

Tactic:
simp only [epi_iff_surjective, Subfunctor.range_obj, Subfunctor.top_obj,
    Set.top_eq_univ, Set.range_eq_univ]

Premises used: Set.range_eq_univ, CategoryTheory.epi_iff_surjective, Set.top_eq_univ, CategoryTheory.Subfunctor.range_obj, CategoryTheory.Subfunctor.top_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
inst rwa rwa₁ rwa₂ rwa₃ : Epi f
⊢ range f = ⊤

Tactic:
rwa [range_eq_top_iff]

Premises used: SSet.Subcomplex.range_eq_top_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
B : Y.Subcomplex
hf : range f ≤ B
⊢ lift f hf ≫ B.ι = f

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
B : Y.Subcomplex
hf : range f ≤ B
n : SimplexCategoryᵒᵖ
x : X.obj n
⊢ Eq (α := Y.obj n)
    ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((lift f hf).app n) : (a : X.obj n) → (↑(B.obj n) : Type u)) x) :
        Y.obj n) :
      Y.obj n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app n) : (a : X.obj n) → Y.obj n) x : Y.obj n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
p : Y ⟶ X
U V : SimplexCategoryᵒᵖ
f : U ⟶ V
⊢ Subset (α := Set (Y.obj U))
    (Set.preimage (β := X.obj U)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app U)) :
        (a : (fun (X : Type u) ↦ X) (Y.obj U)) → (fun (X : Type u) ↦ X) (X.obj U))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f)) :
          (a : (fun (X : Type u) ↦ X) (X.obj U)) → (fun (X : Type u) ↦ X) (X.obj V)) ⁻¹'
        A.obj V))
    (Set.preimage (β := (fun (X : Type u) ↦ X) (Y.obj V))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f)) :
        (a : (fun (X : Type u) ↦ X) (Y.obj U)) → (fun (X : Type u) ↦ X) (Y.obj V))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app V)) :
          (a : (fun (X : Type u) ↦ X) (Y.obj V)) → (fun (X : Type u) ↦ X) (X.obj V)) ⁻¹'
        A.obj V))

Tactic:
simp [Set.preimage_preimage]

Premises used: Set.preimage_preimage
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A B : X.Subcomplex
p : Y ⟶ X
⊢ (A ⊔ B).preimage p = A.preimage p ⊔ B.preimage p

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, SSet.Subcomplex.preimage, Set.preimage, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A B : X.Subcomplex
p : Y ⟶ X
⊢ (A ⊓ B).preimage p = A.preimage p ⊓ B.preimage p

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, SSet.Subcomplex.preimage, Set.preimage, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
ι : Type u_1
A : ι → X.Subcomplex
p : Y ⟶ X
⊢ preimage (⨆ (i : ι), A i) p = ⨆ (i : ι), (A i).preimage p

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
ι : Type u_1
A : ι → X.Subcomplex
p : Y ⟶ X
⊢ preimage (⨅ (i : ι), A i) p = ⨅ (i : ι), (A i).preimage p

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
A : X.Subcomplex
⊢ A.preimage (𝟙 X) = A

Tactic:
rfl

Premises used: Set.Mem, setOf, SSet.Subcomplex.preimage, Set.preimage, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y Z : SSet
A : Z.Subcomplex
f : X ⟶ Y
g : Y ⟶ Z
⊢ A.preimage (f ≫ g) = (A.preimage g).preimage f

Tactic:
rfl

Premises used: Set.Mem, setOf, SSet.Subcomplex.preimage, Set.preimage, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X : SSet
A : X.Subcomplex
⊢ A.preimage A.ι = ⊤

Tactic:
aesop