mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
h : x₀ = x₁
⊢ eqToHom ⋯ = (Path.Homotopic.Quotient.refl x₁).cast h ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y x' y' : X
p : Path.Homotopic.Quotient x y
hx : x' = x
hy : y' = y
⊢ eqToHom ⋯ ≫ p ≫ eqToHom ⋯ = p.cast hx hy

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
⊢ ∀ {X Y : WalkingMulticospan J} (f : X ⟶ Y),
    (d.map F).multicospan.map f ≫
        (match Y with
          | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
          | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom =
      (match X with
          | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
          | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom ≫
        (d.multicospan ⋙ F).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
j : J.R
⊢ F.map (c.ι (J.fst j)) ≫ (d.map F).fst j = F.map (c.ι (J.snd j)) ≫ (d.map F).snd j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
U✝ V✝ : C
φ : U✝ ⟶ V✝
x : F₁.obj U✝
hx : x ∈ A.obj U✝
h : (ConcreteCategory.hom (f.app U✝)) ⟨x, hx⟩ = (ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩
⊢ (ConcreteCategory.hom (F₂.map φ)) ((ConcreteCategory.hom (f.app U✝)) ⟨x, hx⟩) =
    (ConcreteCategory.hom (F₂.map φ)) ((ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
i : J.L
⊢ (Iso.refl ((Cone.postcompose (d.multicospanMapIso F).inv).obj (F.mapCone c)).pt).hom ≫ (c.map F).ι i =
    ι ((Cone.postcompose (d.multicospanMapIso F).inv).obj (F.mapCone c)) i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
U✝ V✝ : C
φ : U✝ ⟶ V✝
x : F₁.obj U✝
⊢ x ∈
      {x |
        ∃ (hx : x ∈ A.obj U✝), (ConcreteCategory.hom (f.app U✝)) ⟨x, hx⟩ = (ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩} →
    x ∈
      ⇑(ConcreteCategory.hom (F₁.map φ)) ⁻¹'
        {x |
          ∃ (hx : x ∈ A.obj V✝), (ConcreteCategory.hom (f.app V✝)) ⟨x, hx⟩ = (ConcreteCategory.hom (g.app V✝)) ⟨x, hx⟩}

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f : A.toFunctor ⟶ F₂
⊢ Subfunctor.equalizer f f = A

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
i : C
x : A.toFunctor.obj i
⊢ ↑x ∈ (Subfunctor.equalizer f g).obj i ↔ (ConcreteCategory.hom (f.app i)) x = (ConcreteCategory.hom (g.app i)) x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
G : C ⥤ Type w
φ : G ⟶ A.toFunctor
⊢ range (φ ≫ A.ι) ≤ Subfunctor.equalizer f g ↔ φ ≫ f = φ ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
⊢ ∀ {X Y : WalkingMultispan J} (f : X ⟶ Y),
    (d.map F).multispan.map f ≫
        (match Y with
          | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
          | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom =
      (match X with
          | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
          | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom ≫
        (d.multispan ⋙ F).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
j : J.L
⊢ (d.map F).fst j ≫ F.map (c.π (J.fst j)) = (d.map F).snd j ≫ F.map (c.π (J.snd j))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
i : J.R
⊢ π ((Cocone.precompose (d.multispanMapIso F).symm.inv).obj (F.mapCocone c)) i ≫
      (Iso.refl ((Cocone.precompose (d.multispanMapIso F).symm.inv).obj (F.mapCocone c)).pt).hom =
    (c.map F).π i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
⊢ Subfunctor.equalizer f g = A ↔ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
⊢ Mono (equalizer.ι f g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
⊢ ι f g ≫ f = ι f g ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
G : C ⥤ Type w
φ : G ⟶ A.toFunctor
w : φ ≫ f = φ ≫ g
⊢ range (φ ≫ A.ι) ≤ Subfunctor.equalizer f g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
s : Limits.Fork f g
⊢ lift f g s.ι ⋯ ≫ (fork f g).ι = s.ι

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
s : Limits.Fork f g
m : s.pt ⟶ (fork f g).pt
hm : m ≫ (fork f g).ι = s.ι
⊢ m = lift f g s.ι ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
k : J.R
hk : k = J.fst default
⊢ I.right k = I.right (J.fst default)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
k : J.R
hk : ¬k = J.fst default
⊢ k = J.snd default

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
k : J.R
hk : ¬k = J.fst default
⊢ I.right k = I.right (J.snd default)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ ∀ (a : J.L),
    (I.fst a ≫ if hk : J.fst a = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) =
      I.snd a ≫ if hk : J.snd a = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ (multicofork h h' s).π (J.fst default) = s.inl

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ (multicofork h h' s).π (J.snd default) = s.inr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
⊢ c.π (J.fst default) ≫ hc.desc (isPushout.multicofork h h' s) = s.inl

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
⊢ c.π (J.snd default) ≫ hc.desc (isPushout.multicofork h h' s) = s.inr

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
x₁ x₂ x₃ x₄ : T
inst✝ : Lattice T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ x₁ ≤ x₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
x₁ x₂ x₃ x₄ : T
inst✝ : Lattice T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ x₁ ≤ x₃

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
x₁ x₂ x₃ x₄ : T
inst✝ : Lattice T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ x₂ ≤ x₄

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
x₁ x₂ x₃ x₄ : T
inst✝ : Lattice T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ x₃ ≤ x₄

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
inst✝ : CompleteLattice T
ι : Type u_1
x : T
u : ι → T
v : ι → ι → T
d : MulticoequalizerDiagram x u v
x✝ : (MultispanShape.prod ι).L
⊢ (match x✝ with
    | (i, j) => v i j) ≤
    u ((MultispanShape.prod ι).fst x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
inst✝ : CompleteLattice T
ι : Type u_1
x : T
u : ι → T
v : ι → ι → T
d : MulticoequalizerDiagram x u v
x✝ : (MultispanShape.prod ι).L
⊢ (match x✝ with
    | (i, j) => v i j) ≤
    u ((MultispanShape.prod ι).snd x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
inst✝ : CompleteLattice T
ι : Type u_1
x : T
u : ι → T
v : ι → ι → T
d : MulticoequalizerDiagram x u v
i : (MultispanShape.prod ι).R
⊢ d.multispanIndex.right i ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
inst✝ : CompleteLattice T
x₁ x₂ x₃ x₄ : T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ (⨆ i, bif i then x₃ else x₂) = x₄

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
inst✝ : CompleteLattice T
x₁ x₂ x₃ x₄ : T
sq : BicartSq x₁ x₂ x₃ x₄
i j : Bool
⊢ (bif i then bif j then x₃ else x₁ else bif j then x₁ else x₂) = (bif i then x₃ else x₂) ⊓ bif j then x₃ else x₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
⊢ m = hc.desc (isPushout.multicofork h h' s)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
U✝ V✝ : SimplexCategoryᵒᵖ
φ : U✝ ⟶ V✝
s : Δ[n].obj U✝
hs : s ∈ {s | Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}
h : Set.range ⇑(stdSimplex.asOrderHom ((ConcreteCategory.hom (Δ[n].map φ)) s)) ∪ {i} = Set.univ
⊢ Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ Λ[n, i] = ⨆ j, stdSimplex.face {↑j}ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i✝ : Fin (n + 1)
i : ↑{i✝}ᶜ
⊢ {↑i}ᶜ.card ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ Λ[n, i].toSSet.HasDimensionLT n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n d : ℕ
s : Δ[n] _⦋d⦌
i : Fin (n + 1)
⊢ s ∈ Λ[n, i].obj (op ⦋d⦌) ↔ ∃ j, ∃ (_ : j ≠ i), j ∉ Set.range ⇑s

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
h : i ≠ j
⊢ stdSimplex.face {i}ᶜ ≤ Λ[n, j]

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
hS : S = Finset.univ
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
⊢ Λ[n + 2, i].obj (op ⦋0⦌) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
l : J.L
z : d.multispan.obj (WalkingMultispan.left l)
⊢ d.multispan.ιColimitType (WalkingMultispan.right (J.fst l))
      ((ConcreteCategory.hom (d.multispan.map (WalkingMultispan.Hom.fst l))) z) =
    d.multispan.ιColimitType (WalkingMultispan.left l) z

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
r : J.R
z : d.multispan.obj (WalkingMultispan.right r)
⊢ d.multispan.ιColimitType (WalkingMultispan.right r) z = d.multispan.ιColimitType (WalkingMultispan.right r) z

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
x : d.multispan.ColimitType
⊢ ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this : ∀ (j : Fin (n + 1)), j ≠ i → j ∈ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)
⊢ Finset.image ⇑(SimplexCategory.Hom.toOrderHom f) ⊤ ∪ {i} = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
i : J.R
z : d.right i
⊢ c.ι (WalkingMultispan.right i) z =
    d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i) z)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this✝¹ : ∀ (j : Fin (n + 1)), j ≠ i → j ∈ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)
this✝ : Finset.image ⇑(SimplexCategory.Hom.toOrderHom f) ⊤ ∪ {i} = ⊤
this : n ≤ (Finset.image (⇑(SimplexCategory.Hom.toOrderHom f)) Finset.univ).card
⊢ n ≤ m + 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ ∃ j, j ≠ i ∧ j ∉ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
⊢ Λ[n, i].obj (op ⦋m⦌) = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits

Goal state before:
pp: 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:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits

Goal state before:
pp: 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:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits

Goal state before:
pp: X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
n : SimplexCategoryᵒᵖ
⊢ IsColimit
    (((evaluation SimplexCategoryᵒᵖ (Type u)).obj n).mapCocone
      ((CompleteLattice.MulticoequalizerDiagram.multicofork h).map toSSetFunctor))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits

Goal state before:
pp: X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
inst✝ : LinearOrder ι
i j : ι
⊢ (CompleteLattice.MulticoequalizerDiagram.multispanIndex h).left (i, j) =
    (CompleteLattice.MulticoequalizerDiagram.multispanIndex h).left (j, i)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits

Goal state before:
pp: X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
⊢ A₂.obj n ⊔ A₃.obj n = A₄.obj n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
⊢ c.IsColimit ↔
    (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
        c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
          d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
            d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
      ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits

Goal state before:
pp: X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
⊢ A₂.obj n ⊓ A₃.obj n = A₁.obj n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits

Goal state before:
pp: X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
⊢ IsColimit ((PushoutCocone.mk (homOfLE ⋯) (homOfLE ⋯) ⋯).map ((evaluation SimplexCategoryᵒᵖ (Type u)).obj n))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
⊢ ∂Δ[n] = ⨆ i, stdSimplex.face {i}ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ {i}ᶜ.card ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
⊢ ∂Δ[n].toSSet.HasDimensionLT n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n d : ℕ
s : Δ[n] _⦋d⦌
⊢ s ∈ ∂Δ[n].obj (op ⦋d⦌) ↔ ∃ j, j ∉ Set.range ⇑s

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ stdSimplex.face {i}ᶜ ≤ ∂Δ[n]

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
x₂ : X
h₂ : x₂ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₂, h₂⟩
⊢ x₁ = x₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : objMk OrderHom.id ∈ (face {i}ᶜ).obj (op ⦋n⦌)
⊢ i ∈ Finset.image ⇑(SimplexCategory.Hom.toOrderHom (objEquiv (objMk OrderHom.id))) ⊤

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
⊢ objMk OrderHom.id ∉ ∂Δ[n].obj (op ⦋n⦌)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
⊢ ∂Δ[n] ≤ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd✝ : n ≤ d
S : Finset (Fin (n + 1 + 1))
hS : S.card = d + 1
hx : stdSimplex.face S ≤ A
hd : n < d
⊢ n + 1 + 1 ≤ S.card

Tactic:
by

Goal state after: