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

Goal state before:
pp: case mk
X : Type u_1
inst✝ : TopologicalSpace X
x y : FundamentalGroupoid X
x✝ : x ⟶ y
p : Path x.as y.as
⊢ Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as)) p) (ContinuousMap.id X) =
    Quot.mk (⇑(Path.Homotopic.setoid x.as y.as)) p

Tactic:
rfl

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

Goal state before:
pp: case mk
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
Z : Type u_3
inst✝ : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
x y : FundamentalGroupoid X
x✝ : x ⟶ y
p : Path x.as y.as
⊢ Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as)) p) (g.comp f) =
    { obj := fun x ↦ { as := g x.as }, map := fun {X Y_1} p ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
          map_comp := ⋯ }.map
      ({ obj := fun x ↦ { as := f x.as }, map := fun {X_1 Y_1} p ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
            map_comp := ⋯ }.map
        (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as)) p))

Tactic:
rfl

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

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

Tactic:
rfl

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)
hk : ¬J.snd default = J.fst default
⊢ I.right (J.snd default) = I.right (J.snd default)

Tactic:
rfl

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : SimplexCategoryᵒᵖ
j : Δ[n].obj m
⊢ (∃ x, ¬x = i ∧ ∀ (x_1 : Fin ((unop m).len + 1)), ¬(stdSimplex.asOrderHom j) x_1 = x) ↔
    ∃ i_1, ¬i_1 = i ∧ ∀ (x : Fin ((unop m).len + 1)), ¬(SimplexCategory.Hom.toOrderHom (stdSimplex.objEquiv j)) x = i_1

Tactic:
rfl

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₂ ⊔ A₃).obj n

Tactic:
rfl

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₂ ⊓ A₃).obj n

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
h₁ : ¬k = i.rev
h₂ : ∀ (x : Fin (d + 1)), ¬j x = k
⊢ ¬k.rev = i ∧ ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = k.rev

Tactic:
grind

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

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

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Set

Goal state before:
pp: case hinj
J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
⊢ ∀ (i j : J) (xi : (fun X ↦ X) ((F ⋙ functorToTypes).obj i)) (xj : (fun X ↦ X) ((F ⋙ functorToTypes).obj j)),
    (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) xi =
        (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ functorToTypes).map f)) xi = (ConcreteCategory.hom ((F ⋙ functorToTypes).map g)) xj

Tactic:
· intro i j ⟨x, hx⟩ ⟨y, hy⟩ h
      obtain rfl : x = y := by simpa using h
      exact ⟨IsFiltered.max i j, IsFiltered.leftToMax i j, IsFiltered.rightToMax i j, rfl⟩

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ ι i = (stdSimplex.faceSingletonComplIso i).hom ≫ faceι i

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ ι i j hij = (stdSimplex.faceSingletonComplIso j).hom ≫ faceι i j hij

Tactic:
rfl

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

Goal state before:
pp: case mpr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
⊢ Rel' f g (Sum.inl x₁) (Sum.inl x₁)

pp: case mpr.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
w✝¹ w✝ : S
h : (ConcreteCategory.hom g) w✝¹ = (ConcreteCategory.hom g) w✝
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) w✝¹)) (Sum.inl ((ConcreteCategory.hom f) w✝))

Tactic:
· apply Rel'.refl

Goal state after:
case mpr.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
w✝¹ w✝ : S
h : (ConcreteCategory.hom g) w✝¹ = (ConcreteCategory.hom g) w✝
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) w✝¹)) (Sum.inl ((ConcreteCategory.hom f) w✝))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mp.refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ : X₂
⊢ x₂ = x₂

Tactic:
rfl

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

Goal state before:
pp: case refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x : X₁ ⊕ X₂
⊢ Rel' f g x x

pp: case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) y₀✝)) (Sum.inl ((ConcreteCategory.hom f) x₀✝))

pp: case inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inl ((ConcreteCategory.hom f) s✝))

pp: case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s✝)) (Sum.inr ((ConcreteCategory.hom g) s✝))

Tactic:
· apply Rel'.refl

Goal state after:
case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) y₀✝)) (Sum.inl ((ConcreteCategory.hom f) x₀✝))

case inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inl ((ConcreteCategory.hom f) s✝))

case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s✝)) (Sum.inr ((ConcreteCategory.hom g) s✝))
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
j : J
x₁ y₁ : F₁.obj j
h : (hom φ) ((hom (c₁.ι.app j)) x₁) = (hom φ) ((hom (c₁.ι.app j)) y₁)
⊢ (hom (c₁.ι.app j)) x₁ = (hom (c₁.ι.app j)) y₁

Tactic:
simp only [Functor.const_obj_obj, hφ] at h

Goal state after:
J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
j : J
x₁ y₁ : F₁.obj j
h : (hom (c₂.ι.app j)) ((hom (f.app j)) x₁) = (hom (c₂.ι.app j)) ((hom (f.app j)) y₁)
⊢ (hom (c₁.ι.app j)) x₁ = (hom (c₁.ι.app j)) y₁
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
i₁ : T
x₁ : X₁ i₁
hx : (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₁) = (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₁)
⊢ (hom (Sigma.ι X₁ i₁)) x₁ = (hom (Sigma.ι X₁ i₁)) x₁

Tactic:
rfl

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ cofibrations SSet f ↔ Mono f

Tactic:
rfl

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ fibrations SSet f ↔ J.rlp f

Tactic:
rfl

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

Goal state before:
pp: case refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
a : X₁ ⊕ X₂
⊢ Quot.mk (Rel f g) a = Quot.mk (Rel f g) a

Tactic:
rfl

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

Goal state before:
pp: case mk
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x✝ : Pushout f g
x : X₁ ⊕ X₂
⊢ Quot.lift (Quot.mk (Rel f g)) ⋯ (Quot.lift (Quot.mk (Rel' f g)) ⋯ (Quot.mk (Rel f g) x)) = Quot.mk (Rel f g) x

Tactic:
rfl

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

Goal state before:
pp: case mk
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x✝ : Pushout' f g
x : X₁ ⊕ X₂
⊢ Quot.lift (Quot.mk (Rel' f g)) ⋯ (Quot.lift (Quot.mk (Rel f g)) ⋯ (Quot.mk (Rel' f g) x)) = Quot.mk (Rel' f g) x

Tactic:
rfl

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

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x : (span t l).obj none
⊢ (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom (t ≫ r)) x

Tactic:
rfl

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

Goal state before:
pp: S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
j : Fin (n + 1 + 2)
hj : j ≠ i
⊢ (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
    (ConcreteCategory.hom (Λ[n + 2, i].ι.app (Opposite.op ⦋n + 1⦌) ≫ (yonedaEquiv.symm σ).app (Opposite.op ⦋n + 1⦌)))
      (horn.face i j hj)

Tactic:
rfl

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

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
ht : Function.Injective ⇑(ConcreteCategory.hom t)
x₂ : (fun X ↦ X) X₂
x₃ : (fun X ↦ X) X₃
hx : (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom b) x₃
this : ∃ s, (ConcreteCategory.hom t) s = x₂ ∧ (ConcreteCategory.hom l) s = x₃
⊢ ∃ x₁, (ConcreteCategory.hom t) x₁ = x₂ ∧ (ConcreteCategory.hom l) x₁ = x₃

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: case zero
i : Fin (0 + 1)
h0 : 0 < i
hn : i < Fin.last 0
⊢ innerHornInclusions Λ[0, i].ι

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: case succ.zero
i : Fin (0 + 1 + 1)
h0 : 0 < i
hn : i < Fin.last (0 + 1)
⊢ innerHornInclusions Λ[0 + 1, i].ι

Tactic:
grind

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

Goal state before:
pp: X : SSet
i j : ℕ
h : i ≤ j
k : Fin i
x : ↑(X.nonDegenerate ↑k)
⊢ Subcomplex.ofSimplex ↑x ≤ Subcomplex.ofSimplex ↑x

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X Y : SSet
p : X ⟶ Y
hY : IsTerminal Y
⊢ X.Quasicategory ↔ InnerFibration p

Tactic:
simp only [quasicategory_iff_innerFibration, innerFibration_iff]

Goal state after:
X Y : SSet
p : X ⟶ Y
hY : IsTerminal Y
⊢ innerFibrations (terminal.from X) ↔ innerFibrations p
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
i n : ℕ
hi : i < n
j : ℕ
f : ⦋i⦌ ⟶ ⦋j⦌
w✝ : Epi f
y : ↑(X.nonDegenerate j)
⊢ Subcomplex.ofSimplex ↑y ≤ Subcomplex.ofSimplex ↑y

Tactic:
rfl

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

Goal state before:
pp: case inl.inl
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₂ : X₂
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom r) x₂) = (ConcreteCategory.hom k) ((ConcreteCategory.hom r) x₂)
⊢ (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom r) x₂

Tactic:
rfl

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

Goal state before:
pp: case a.right
⊢ stdSimplex.face {1, 2} ≤ Λ[2, 2]

Tactic:
exact face_le_horn (0 : Fin 3) 2 (by simp)

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

Goal state before:
pp: X : SSet
d : ℕ
hd✝ : d < d + 1
hd : d ≤ d
x : ↑(X.nonDegenerate ↑⟨d, hd✝⟩)
⊢ Subcomplex.ofSimplex ↑x ≤ Subcomplex.ofSimplex ↑x

Tactic:
rfl

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

Goal state before:
pp: case inr.inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₃ : X₃
hx₃ hy₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃)
⊢ (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom b) x₃

Tactic:
rfl

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
n : ℕ
x : ↑(Y.nonDegenerate n)
hx : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ Subcomplex.ofSimplex ↑x ≤ Subcomplex.ofSimplex ↑x

Tactic:
rfl

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
⊢ j ≤ k

Tactic:
grind

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

Goal state before:
pp: case zero
X : SSet
i : Fin (0 + 2)
f : (j : Fin (0 + 2)) → j ≠ i → (Δ[0] ⟶ X)
hf : horn.IsCompatible f
a b : ↑{i}ᶜ
hab : (a, b) ∈ {x | x.1 < x.2}
⊢ (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst
        ⟨(a, b), hab⟩ ≫
      match (MultispanShape.ofLinearOrder ↑{i}ᶜ).fst ⟨(a, b), hab⟩ with
      | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj) =
    ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd
        ⟨(a, b), hab⟩ ≫
      match (MultispanShape.ofLinearOrder ↑{i}ᶜ).snd ⟨(a, b), hab⟩ with
      | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj

Tactic:
grind

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

Goal state before:
pp: case refine_1
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
c : Cell i d
y : Δ[d] _⦋n⦌
hx : (ConcreteCategory.hom (c.map.app (op ⦋n⦌))) y ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ y ∈ ∂Δ[d].obj (op ⦋n⦌)

Tactic:
rwa [← c.preimage_map, Subcomplex.preimage_obj, Set.mem_preimage]

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

Goal state before:
pp: case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
c₁ : Cell i d
f₁ : ⦋n⦌ ⟶ ⦋d⦌
w✝¹ : Epi f₁
hx₁ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
w✝ : Epi f₁
hx₂ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
h : (ConcreteCategory.hom (Y.map f₁.op)) c₁.simplex = (ConcreteCategory.hom (Y.map f₁.op)) c₁.simplex
⊢ (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) =
    (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁)

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
h : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := h })
i : Fin m
⊢ (ConcreteCategory.hom (X.map (ObjectProperty.homMk (SimplexCategory.δ 1)).op))
      ((ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ h).op)) Δ) =
    (ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 1) ⋯ ⋯).op))
      ((ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ h).op)) Δ)

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
h : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := h })
i : Fin m
⊢ (ConcreteCategory.hom (X.map (ObjectProperty.homMk (SimplexCategory.δ 0)).op))
      ((ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ h).op)) Δ) =
    (ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 0) ⋯ ⋯).op))
      ((ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ h).op)) Δ)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
⊢ (stdSimplex.spineId (n + 2)).arrow k.castSucc = stdSimplex.objEquiv.symm (mkOfSucc k.castSucc)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
⊢ (stdSimplex.spineId (n + 2)).arrow k.succ = stdSimplex.objEquiv.symm (mkOfSucc k.succ)

Tactic:
rfl

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

Goal state before:
pp: case zero
X : SSet
x : X _⦋0 + 1⦌
⊢ (ConcreteCategory.hom (𝟙 (((truncation 1).obj X).obj (op { obj := ⦋0⦌, property := ⋯ }))))
      ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) =
    (ConcreteCategory.hom (((truncation 2).obj X).map (ObjectProperty.homMk (δ 0)).op)) x

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
⊢ ↑k < n + 2

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: case h_obj
C : Type u
inst✝ : Category.{v, u} C
x✝ : ↑chosenTerminal ⥤ C
X✝ : ↑chosenTerminal
⊢ ((Functor.const ↑chosenTerminal).obj ((fun F ↦ F.obj { down := { as := () } }) x✝)).obj X✝ = x✝.obj X✝

Tactic:
rfl

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

Goal state before:
pp: case «0»
n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 2)
⊢ ↑(((stdSimplex.spineId (n + 2)).arrow j) ((fun i ↦ i) ⟨0, ⋯⟩)) = ↑(↑(primitiveEdge h₀ hₙ j) ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
rfl

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

Goal state before:
pp: case «1»
n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 2)
⊢ ↑(((stdSimplex.spineId (n + 2)).arrow j) ((fun i ↦ i) ⟨1, ⋯⟩)) = ↑(↑(primitiveEdge h₀ hₙ j) ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ ↑k + 2 ≤ n + 1 + 2

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: X Y : Cat
x✝⁴ : BinaryFan X Y
x✝³ : x✝⁴.pt ⟶ of (↑X × ↑Y)
h1 : x✝³ ≫ (Prod.fst ↑X ↑Y).toCatHom = x✝⁴.fst
h2 : x✝³ ≫ (Prod.snd ↑X ↑Y).toCatHom = x✝⁴.snd
x✝² x✝¹ : ↑x✝⁴.pt
x✝ : x✝² ⟶ x✝¹
⊢ x✝³.toFunctor.map x✝ ≍
    Prod.mkHom ((x✝³ ≫ (Prod.fst ↑X ↑Y).toCatHom).toFunctor.map x✝) ((x✝³ ≫ (Prod.snd ↑X ↑Y).toCatHom).toFunctor.map x✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case «0».«0»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow ((fun i ↦ i) ⟨0, ⋯⟩)) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc ((fun i ↦ i) ⟨0, ⋯⟩)).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after: