awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
Z : Y.Subcomplex
⊢ A.image f ≤ Z ↔ A ≤ Z.preimage f

Tactic:
simp [Subfunctor.le_def]

Premises used: CategoryTheory.Subfunctor.le_def
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
⊢ image ⊤ f = range f

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

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
Z : SSet
g : Y ⟶ Z
⊢ A.image (f ≫ g) = (A.image f).image g

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
Z : SSet
g : Y ⟶ Z
⊢ range (f ≫ g) = (range f).image g

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ A.image f = range (A.ι ≫ f)

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
ι : Type u_1
S : ι → X.Subcomplex
f : X ⟶ Y
⊢ image (⨆ (i : ι), S i) f = ⨆ (i : ι), (S i).image f

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
⊢ (range f).preimage f ≤ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
rw : image ⊤ f ≤ range f
rw₁ rw₂ : range f ≤ range f
⊢ ⊤ ≤ (range f).preimage f

Tactic:
rw [← image_le_iff, image_top]

Premises used: SSet.Subcomplex.image_le_iff, SSet.Subcomplex.image_top
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ A.image f ≤ range f

Tactic:
simp [image_le_iff, preimage_range, le_top]

Premises used: SSet.Subcomplex.preimage_range, SSet.Subcomplex.image_le_iff, le_top
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
a :
  (ofSimplex x).image f ≤
    ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x)
a₁ :
  ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x) ≤
    (ofSimplex x).image f
⊢ (ofSimplex x).image f =
    ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
a :
  Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (γ := Set ((fun (X : Type u) ↦ X) (Y _⦋n⦌)))
    (Subfunctor.obj
      (ofSimplex (n := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x))
      (Opposite.op ⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.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⦌))
⊢ (ofSimplex x).image f ≤
    ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x)

Tactic:
rw [image_le_iff, ofSimplex_le_iff, preimage_obj, Set.mem_preimage]

Premises used: SSet.Subcomplex.image_le_iff, SSet.Subcomplex.preimage_obj, SSet.Subcomplex.ofSimplex_le_iff, Set.mem_preimage
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (γ := Set ((fun (X : Type u) ↦ X) (Y _⦋n⦌)))
    (Subfunctor.obj
      (ofSimplex (n := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x))
      (Opposite.op ⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.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 mem_ofSimplex_obj

Premises used: SSet.Subcomplex.mem_ofSimplex_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
a :
  Membership.mem (α := Y _⦋n⦌) (γ := Set (Y _⦋n⦌)) (((ofSimplex x).image f).obj (Opposite.op ⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.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⦌))
⊢ ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x) ≤
    (ofSimplex x).image f

Tactic:
rw [ofSimplex_le_iff]

Premises used: SSet.Subcomplex.ofSimplex_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ Membership.mem (α := Y _⦋n⦌) (γ := Set (Y _⦋n⦌)) (((ofSimplex x).image f).obj (Opposite.op ⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.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:
⟨x, mem_ofSimplex_obj _, rfl⟩

Premises used: Set.Mem, setOf, And.intro, SSet.Subcomplex.mem_ofSimplex_obj, Exists.intro, Set.image, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ Membership.mem (α := Y _⦋n⦌) (γ := Set (Y _⦋n⦌)) (((ofSimplex x).image f).obj (Opposite.op ⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.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:
exact ⟨x, mem_ofSimplex_obj _, rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
rw rw₁ : range (A.ι ≫ f) ≤ range (A.ι ≫ f)
⊢ range (A.ι ≫ f) ≤ A.image f

Tactic:
rw [image_eq_range]

Premises used: SSet.Subcomplex.image_eq_range
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ A.toImage f ≫ (A.image f).ι = A.ι ≫ f

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, SSet.Subcomplex.toImage, TypeCat.Fun.comp, CategoryTheory.Subfunctor.ι, SSet.Subcomplex.lift, CategoryTheory.Subfunctor.lift, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
rw : range (A.toImage f) = ⊤
⊢ Epi (A.toImage f)

Tactic:
rw [← range_eq_top_iff]

Premises used: SSet.Subcomplex.range_eq_top_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ range (A.toImage f) ≤ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
apply : ⊤ ≤ range (A.toImage f)
⊢ range (A.toImage f) = ⊤

Tactic:
apply le_antisymm (by simp)

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
m : SimplexCategoryᵒᵖ
y : X.obj m
hy : y ∈ A.obj m
h :
  Membership.mem (α := (A.image f).toSSet.obj m) (γ := Set ((A.image f).toSSet.obj m)) (Subfunctor.obj ⊤ m)
    (Subtype.mk (p := fun (x : Y.obj m) ↦ x ∈ (A.image f).obj m)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app m) :
            (a : (fun (X : Type u) ↦ X) (X.obj m)) → (fun (X : Type u) ↦ X) (Y.obj m))
          y)
        ⋯ :
      { x : Y.obj m // x ∈ (A.image f).obj m })
⊢ Membership.mem (α := (A.image f).toSSet.obj m) ((range (A.toImage f)).obj m)
    (Subtype.mk (p := fun (x : Y.obj m) ↦ x ∈ (A.image f).obj m)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app m) :
            (a : (fun (X : Type u) ↦ X) (X.obj m)) → (fun (X : Type u) ↦ X) (Y.obj m))
          y)
        ⋯ :
      { x : Y.obj m // x ∈ (A.image f).obj m })

Tactic:
⟨⟨y, hy⟩, rfl⟩

Premises used: Set.Mem, setOf, Subtype.mk, Exists.intro, Set.range, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
m : SimplexCategoryᵒᵖ
y : X.obj m
hy : y ∈ A.obj m
h :
  Membership.mem (α := (A.image f).toSSet.obj m) (γ := Set ((A.image f).toSSet.obj m)) (Subfunctor.obj ⊤ m)
    (Subtype.mk (p := fun (x : Y.obj m) ↦ x ∈ (A.image f).obj m)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app m) :
            (a : (fun (X : Type u) ↦ X) (X.obj m)) → (fun (X : Type u) ↦ X) (Y.obj m))
          y)
        ⋯ :
      { x : Y.obj m // x ∈ (A.image f).obj m })
⊢ Membership.mem (α := (A.image f).toSSet.obj m) ((range (A.toImage f)).obj m)
    (Subtype.mk (p := fun (x : Y.obj m) ↦ x ∈ (A.image f).obj m)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app m) :
            (a : (fun (X : Type u) ↦ X) (X.obj m)) → (fun (X : Type u) ↦ X) (Y.obj m))
          y)
        ⋯ :
      { x : Y.obj m // x ∈ (A.image f).obj m })

Tactic:
exact ⟨⟨y, hy⟩, rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
S T : X.Subcomplex
h : S ≤ T
rw : S ≤ preimage ((fun (S : X.Subcomplex) ↦ S.image f) T) f
⊢ LE.le.{u} (α := Y.Subcomplex) ((fun (S : X.Subcomplex) ↦ S.image f) S) ((fun (S : X.Subcomplex) ↦ S.image f) T)

Tactic:
rw [image_le_iff]

Premises used: SSet.Subcomplex.image_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
S T : X.Subcomplex
h : S ≤ T
rw rw₁ : T.image f ≤ T.image f
⊢ T ≤ preimage ((fun (S : X.Subcomplex) ↦ S.image f) T) f

Tactic:
rw [← image_le_iff]

Premises used: SSet.Subcomplex.image_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
S T : X.Subcomplex
h : S ≤ T
⊢ S ≤ preimage ((fun (S : X.Subcomplex) ↦ S.image f) T) f

Tactic:
exact h.trans (by rw [← image_le_iff])

Premises used: LE.le.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
B : X.Subcomplex
f : Y ⟶ X
rw : B.preimage f = ⊤ ↔ image ⊤ f ≤ B
rw₁ : B.preimage f = ⊤ ↔ ⊤ ≤ B.preimage f
rw₂ rw₃ : B.preimage f = ⊤ ↔ B.preimage f = ⊤
⊢ B.preimage f = ⊤ ↔ range f ≤ B

Tactic:
rw [← image_top, image_le_iff, top_le_iff]

Premises used: SSet.Subcomplex.image_le_iff, SSet.Subcomplex.image_top, top_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
B : X.Subcomplex
f : Y ⟶ X
rw rw₁ : B.preimage f ≤ B.preimage f
⊢ (B.preimage f).image f ≤ B

Tactic:
rw [image_le_iff]

Premises used: SSet.Subcomplex.image_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
B : Y.Subcomplex
inst : IsIso f
apply : B ≤ (B.preimage f).image f
⊢ (B.preimage f).image f = B

Tactic:
apply le_antisymm (B.image_preimage_le f)

Premises used: SSet.Subcomplex.image_preimage_le, le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
B : Y.Subcomplex
inst : IsIso f
n : SimplexCategoryᵒᵖ
y : Y.obj n
hy : y ∈ B.obj n
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) (X.obj n)) ((B.preimage f).obj n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((inv f).app n) :
            (a : (fun (X : Type u) ↦ X) (Y.obj n)) → (fun (X : Type u) ↦ X) (X.obj n))
          y :
        (fun (X : Type u) ↦ X) (X.obj n)) ∧
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app n) :
          (a : (fun (X : Type u) ↦ X) (X.obj n)) → (fun (X : Type u) ↦ X) (Y.obj n))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((inv f).app n) :
              (a : (fun (X : Type u) ↦ X) (Y.obj n)) → (fun (X : Type u) ↦ X) (X.obj n))
            y :
          (fun (X : Type u) ↦ X) (X.obj n)) =
      y

Tactic:
simpa [← NatIso.isIso_inv_app, ← NatTrans.comp_app_apply]

Premises used: CategoryTheory.NatTrans.comp_app_apply, CategoryTheory.NatIso.isIso_inv_app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
B : Y.Subcomplex
inst : IsIso f
n : SimplexCategoryᵒᵖ
y : Y.obj n
hy : y ∈ B.obj n
⊢ y ∈ ((B.preimage f).image f).obj n

Tactic:
exact ⟨(inv f).app _ y, by simpa [← NatIso.isIso_inv_app, ← NatTrans.comp_app_apply]⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst : IsIso f
obj : ∀ (x : SimplexCategoryᵒᵖ) (x_1 : Y.obj x), x_1 ∈ (A.preimage (inv f)).obj x ↔ x_1 ∈ (A.image f).obj x
⊢ A.preimage (inv f) = A.image f

Tactic:
ext _ x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst : IsIso f
x_1 : SimplexCategoryᵒᵖ
x : Y.obj x_1
obj :
  Membership.mem (α := X.obj x_1) (A.obj x_1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (inv (f.app x_1)) : (a : Y.obj x_1) → X.obj x_1) x : X.obj x_1) ↔
    ∃ x_2 ∈ A.obj x_1, (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x_1) : (a : X.obj x_1) → Y.obj x_1) x_2 = x
⊢ x ∈ (A.preimage (inv f)).obj x_1 ↔ x ∈ (A.image f).obj x_1

Tactic:
simp only [preimage_obj, NatIso.isIso_inv_app, Set.mem_preimage, image_obj, Set.mem_image]

Premises used: SSet.Subcomplex.image_obj, Set.mem_image, SSet.Subcomplex.preimage_obj, CategoryTheory.NatIso.isIso_inv_app, Set.mem_preimage
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst : IsIso f
x_1 : SimplexCategoryᵒᵖ
x : Y.obj x_1
hx :
  Membership.mem (α := X.obj x_1) (A.obj x_1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (inv (f.app x_1)) : (a : Y.obj x_1) → X.obj x_1) x : X.obj x_1)
⊢ Membership.mem (α := X.obj x_1) (A.obj x_1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((inv f).app x_1) :
            (a : (fun (X : Type u) ↦ X) (Y.obj x_1)) → (fun (X : Type u) ↦ X) (X.obj x_1))
          x :
        (fun (X : Type u) ↦ X) (X.obj x_1)) ∧
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x_1) : (a : X.obj x_1) → Y.obj x_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((inv f).app x_1) :
              (a : (fun (X : Type u) ↦ X) (Y.obj x_1)) → (fun (X : Type u) ↦ X) (X.obj x_1))
            x :
          (fun (X : Type u) ↦ X) (X.obj x_1)) =
      x

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst : IsIso f
x_1 : SimplexCategoryᵒᵖ
x : X.obj x_1
hx : x ∈ A.obj x_1
⊢ Membership.mem (α := X.obj x_1) (A.obj x_1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (inv (f.app x_1)) : (a : Y.obj x_1) → X.obj x_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x_1) : (a : X.obj x_1) → Y.obj x_1) x : Y.obj x_1) :
      X.obj x_1)

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst : IsIso f
x_1 : SimplexCategoryᵒᵖ
x : Y.obj x_1
⊢ Membership.mem (α := X.obj x_1) (A.obj x_1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (inv (f.app x_1)) : (a : Y.obj x_1) → X.obj x_1) x : X.obj x_1) ↔
    ∃ x_2 ∈ A.obj x_1, (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x_1) : (a : X.obj x_1) → Y.obj x_1) x_2 = x

Tactic:
exact ⟨fun hx ↦ ⟨(inv f).app _ x, by simpa⟩, by rintro ⟨x, hx, rfl⟩; simpa⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : Y.Subcomplex
f : X ⟶ Y
inst : IsIso f
⊢ A.image (inv f) = A.preimage f

Tactic:
simp [← preimage_inv]

Premises used: SSet.Subcomplex.preimage_inv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
p : Y ⟶ X
⊢ range ((A.preimage p).ι ≫ p) ≤ A

Tactic:
simp [range_comp]

Premises used: SSet.Subcomplex.range_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
A : X.Subcomplex
p : Y ⟶ X
⊢ A.fromPreimage p ≫ A.ι = (A.preimage p).ι ≫ p

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, CategoryTheory.Subfunctor.ι, SSet.Subcomplex.lift, SSet.Subcomplex.fromPreimage, CategoryTheory.Subfunctor.lift, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
Goal:
X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
n : SimplexCategoryᵒᵖ
⊢ ⨆ (i : ι), (U i).obj n = A.obj n

Tactic:
simp [← h.iSup_eq]

Premises used: CompleteLattice.MulticoequalizerDiagram.iSup_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
Goal:
X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
n : SimplexCategoryᵒᵖ
⊢ ∀ (i j : ι), (V i j).obj n = (U i).obj n ⊓ (U j).obj n

Tactic:
simp [h.eq_inf]

Premises used: CompleteLattice.MulticoequalizerDiagram.eq_inf
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
Goal:
X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
n : SimplexCategoryᵒᵖ
⊢ CompleteLattice.MulticoequalizerDiagram (A.obj n) (fun (i : ι) ↦ (U i).obj n) fun (i j : ι) ↦ (V i j).obj n

Tactic:
have h' : CompleteLattice.MulticoequalizerDiagram (A.obj n) (fun i ↦ (U i).obj n)
        (fun i j ↦ (V i j).obj n) :=
      { eq_inf := by simp [h.eq_inf]
        iSup_eq := by simp [← h.iSup_eq] }
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
Goal:
X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
n : SimplexCategoryᵒᵖ
h' : CompleteLattice.MulticoequalizerDiagram (A.obj n) (fun (i : ι) ↦ (U i).obj n) fun (i j : ι) ↦ (V i j).obj n
⊢ IsColimit (F :=
    ((CompleteLattice.MulticoequalizerDiagram.multispanIndex h).map toSSetFunctor).multispan ⋙
      Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u)) n)
    (Functor.mapCocone (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u)) n)
      ((CompleteLattice.MulticoequalizerDiagram.multicofork h).map toSSetFunctor))

Tactic:
exact (Multicofork.isColimitMapEquiv _ _).2
      (Types.isColimitOfMulticoequalizerDiagram h')

Premises used: CategoryTheory.Limits.Types.isColimitOfMulticoequalizerDiagram, CategoryTheory.Limits.Multicofork.isColimitMapEquiv, Equiv.invFun
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
Goal:
X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
inst : LinearOrder ι
i j : ι
dsimp : V i j = V j i
⊢ (CompleteLattice.MulticoequalizerDiagram.multispanIndex h).left (i, j) =
    (CompleteLattice.MulticoequalizerDiagram.multispanIndex h).left (j, i)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
Goal:
X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
inst : LinearOrder ι
i j : ι
rw : U i ⊓ U j = V j i
rw₁ : U i ⊓ U j = U j ⊓ U i
rw₂ rw₃ : U j ⊓ U i = U j ⊓ U i
⊢ V i j = V j i

Tactic:
rw [h.eq_inf, h.eq_inf, inf_comm]

Premises used: CompleteLattice.MulticoequalizerDiagram.eq_inf, inf_comm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
Goal:
X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
rw : A₂.obj n ⊔ A₃.obj n = (A₂ ⊔ A₃).obj n
⊢ A₂.obj n ⊔ A₃.obj n = A₄.obj n

Tactic:
rw [← sq.sup_eq]

Premises used: Lattice.BicartSq.sup_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
Goal:
X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
⊢ A₂.obj n ⊔ A₃.obj n = (A₂ ⊔ A₃).obj n

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
Goal:
X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
rw : A₂.obj n ⊓ A₃.obj n = (A₂ ⊓ A₃).obj n
⊢ A₂.obj n ⊓ A₃.obj n = A₁.obj n

Tactic:
rw [← sq.inf_eq]

Premises used: Lattice.BicartSq.inf_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
Goal:
X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
⊢ A₂.obj n ⊓ A₃.obj n = (A₂ ⊓ A₃).obj n

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
Goal:
X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
⊢ Lattice.BicartSq (A₁.obj n) (A₂.obj n) (A₃.obj n) (A₄.obj n)

Tactic:
have h : Lattice.BicartSq (A₁.obj n) (A₂.obj n) (A₃.obj n) (A₄.obj n) :=
          { sup_eq := by
              rw [← sq.sup_eq]
              rfl
            inf_eq := by
              rw [← sq.inf_eq]
              rfl }
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
Goal:
X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
h : Lattice.BicartSq (A₁.obj n) (A₂.obj n) (A₃.obj n) (A₄.obj n)
⊢ IsColimit (F :=
    span (X := Functor.obj (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u)) n) A₁.toSSet)
      (CategoryTheory.Functor.map (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u)) n) (homOfLE ⋯))
      (CategoryTheory.Functor.map (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u)) n) (homOfLE ⋯)))
    (PushoutCocone.map (PushoutCocone.mk (homOfLE ⋯) (homOfLE ⋯) ⋯)
      (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u)) n))

Tactic:
exact (Types.isPushout_of_bicartSq h).isColimit

Premises used: CategoryTheory.Limits.Types.isPushout_of_bicartSq, CategoryTheory.IsPushout.isColimit
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexOp
Goal:
X : SSet
A : X.Subcomplex
d : SimplexCategoryᵒᵖ
x : X.op.obj d
⊢ x ∈ A.op.obj d ↔ Membership.mem (α := X.obj d) (A.obj d) ((opObjEquiv : (a : X.op.obj d) → X.obj d) x : X.obj d)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subdivision
Goal:
⊢ sd.IsLeftAdjoint

Tactic:
sdExAdjunction.isLeftAdjoint

Premises used: CategoryTheory.Adjunction.isLeftAdjoint, SSet.sdExAdjunction
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subdivision
Goal:
⊢ ex.IsRightAdjoint

Tactic:
sdExAdjunction.isRightAdjoint

Premises used: CategoryTheory.Adjunction.isRightAdjoint, SSet.sdExAdjunction
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subdivision
Goal:
⊢ sd.IsLeftKanExtension stdSimplex.sdIso.inv

Tactic:
inferInstanceAs (Functor.IsLeftKanExtension _
    (SSet.stdSimplex.leftKanExtensionUnit SimplexCategory.sd.{u}))

Premises used: _private.0.SSet.instIsLeftKanExtensionSimplexCategorySdInvFunctorSdIso._proof_1