mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ PInfty ≫ PInftyToNormalizedMooreComplex X = PInftyToNormalizedMooreComplex X

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : ⦋n✝ + 1⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ PInfty.f (n✝ + 1) = 0

Tactic:
obtain ⟨i, α, h⟩ := SimplexCategory.eq_σ_comp_of_not_injective θ hθ
    rw [h, op_comp, X.map_comp, assoc, ← SimplicialObject.σ_def,
      σ_comp_PInfty, comp_zero]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac : A.e ≫ 𝟙 (unop A.fst) = (𝟙 Δ).unop ≫ A.e
⊢ Obj.Termwise.mapMono K (𝟙 (unop A.fst)) ≫ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ A) { as := A } ≫ 𝟙 (Obj.obj₂ K Δ)

Tactic:
Obj.Termwise.mapMono_id,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac : A.e ≫ 𝟙 (unop A.fst) = (𝟙 Δ).unop ≫ A.e
⊢ 𝟙 (K.X (unop A.fst).len) ≫ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ A) { as := A } ≫ 𝟙 (Obj.obj₂ K Δ)
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
hij : ¬c.Rel i j
⊢ P.p.f i ≫ P.X.d i j = 0

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : HomologicalComplex (Karoubi C) c
⊢ ((inverse ⋙ functor).obj P).X = ((𝟭 (HomologicalComplex (Karoubi C) c)).obj P).X

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
⊢ ∀ (X Y : HomologicalComplex (Karoubi C) c) (f : X ⟶ Y),
    (inverse ⋙ functor).map f = eqToHom ⋯ ≫ (𝟭 (HomologicalComplex (Karoubi C) c)).map f ≫ eqToHom ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ (X : Karoubi C), (𝟭 (Karoubi C)).obj X = (toKaroubi (Karoubi C) ⋙ inverse C).obj X

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
s : X.Splitting
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬A.EqId
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ PInfty.f n = 0

Tactic:
rw [SimplicialObject.Splitting.IndexSet.eqId_iff_mono] at hA
  rw [SimplicialObject.Splitting.cofan_inj_eq, assoc, degeneracy_comp_PInfty X n A.e hA, comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M G : Type u
inst✝² : Monoid M
inst✝¹ : Group G
N : Type v
inst✝ : Monoid N
⊢ Function.LeftInverse (fun f ↦ { toFun := fun x ↦ f.map ((toEnd M) x), map_one' := ⋯, map_mul' := ⋯ }) fun f ↦
    { obj := id, map := fun {X Y} ↦ ⇑f, map_id := ⋯, map_comp := ⋯ }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M G : Type u
inst✝² : Monoid M
inst✝¹ : Group G
N : Type v
inst✝ : Monoid N
⊢ Function.RightInverse (fun f ↦ { toFun := fun x ↦ f.map ((toEnd M) x), map_one' := ⋯, map_mul' := ⋯ }) fun f ↦
    { obj := id, map := fun {X Y} ↦ ⇑f, map_id := ⋯, map_comp := ⋯ }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X✝¹ Y✝¹ X✝ Y✝ Z : TopPair
X Y : TopPair
f : X ⟶ Y
⊢ ((𝟭 TopPair).map f ≫ ofHom (𝟙 fst) map ⋯).right = (ofHom (𝟙 fst) map ⋯ ≫ (proj₁ ⋙ diag).map f).right

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X Y : TopPair
f g : X ⟶ Y
H : Homotopy f g
x : ↑TopPair.snd
t : ↑unitInterval
this :
  H.fst (I.homeomorph (x, I.homeomorph.symm t).2, (ConcreteCategory.hom map) (x, I.homeomorph.symm t).1) =
    (ConcreteCategory.hom map) (H.snd (I.homeomorph (x, I.homeomorph.symm t).2, (x, I.homeomorph.symm t).1))
⊢ H.fst (t, (ConcreteCategory.hom map) x) = (ConcreteCategory.hom map) (H.snd (t, x))

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X Y : TopPair
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
⊢ F.symm.symm = F

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X✝ Y✝ X Y Z : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
fst✝ : ↑TopPair.snd
snd✝ : ↑I
⊢ (if h : ↑(I.homeomorph ((ConcreteCategory.hom (map ▷ I)) (fst✝, snd✝)).2) ≤ 1 / 2 then
      F.fst
        (⟨2 * ↑(I.homeomorph ((ConcreteCategory.hom (map ▷ I)) (fst✝, snd✝)).2), ⋯⟩,
          ((ConcreteCategory.hom (map ▷ I)) (fst✝, snd✝)).1)
    else
      G.fst
        (⟨2 * ↑(I.homeomorph ((ConcreteCategory.hom (map ▷ I)) (fst✝, snd✝)).2) - 1, ⋯⟩,
          ((ConcreteCategory.hom (map ▷ I)) (fst✝, snd✝)).1)) =
    (ConcreteCategory.hom map)
      (if h : ↑(I.homeomorph snd✝) ≤ 1 / 2 then F.snd (⟨2 * ↑(I.homeomorph snd✝), ⋯⟩, fst✝)
      else G.snd (⟨2 * ↑(I.homeomorph snd✝) - 1, ⋯⟩, fst✝))

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → (f i).HomotopyRel (g i) S
t : ↑unitInterval
x : A
hx : x ∈ S
i : I
⊢ (Homotopy.pi fun i ↦ (homotopies i).toHomotopy).toContinuousMap (t, x) i = (f i) x

Tactic:
exact (homotopies i).prop' t x hx

Goal state after:
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
p : Homotopic.Quotient as bs
⊢ (pi fun i ↦ proj i p) = p

Tactic:
induction p using Quotient.inductionOn
  simp only [Quotient.mk''_eq_mk, ← Path.Homotopic.Quotient.mk_map, pi_lift]
  congr

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

Goal state before:
pp: case h_map
A : TopCat
B : TopCat
x₀ : ↑(π.obj A)
x₁ : ↑(π.obj B)
y₀ : ↑(π.obj A)
y₁ : ↑(π.obj B)
f₀ : (x₀, x₁).1 ⟶ (y₀, y₁).1
f₁ : (x₀, x₁).2 ⟶ (y₀, y₁).2
this :
  Path.Homotopic.projLeft ((prodToProdTop A B).map (f₀, f₁)) = f₀ ∧
    Path.Homotopic.projRight ((prodToProdTop A B).map (f₀, f₁)) = f₁
⊢ (prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).map (f₀, f₁) ≍ (𝟭 (↑(π.obj A) × ↑(π.obj B))).map (f₀, f₁)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
⊢ F.eval 0 = p₀

Tactic:
by
  ext t
  simp

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
⊢ F.eval 1 = p₁

Tactic:
by
  ext t
  simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f g : X ⟶ Y
h✝ : homRel C f g
P : PathObject Y.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject C ⥤ (weakEquivalences (CofibrantObject C)).Localization := (weakEquivalences (CofibrantObject C)).Q
this : L.map (homMk P.p₀) = L.map (homMk P.p₁)
⊢ f = homMk h.h ≫ homMk P.p₀

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f g : X ⟶ Y
h✝ : homRel C f g
P : PathObject Y.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject C ⥤ (weakEquivalences (CofibrantObject C)).Localization := (weakEquivalences (CofibrantObject C)).Q
this : L.map (homMk P.p₀) = L.map (homMk P.p₁)
⊢ g = homMk h.h ≫ homMk P.p₁

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
H : (weakEquivalences (BifibrantObject C)).IsInvertedBy F
K L : BifibrantObject C
f g : K ⟶ L
h✝ : homRel C f g
P : PathObject L.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this✝ : IsCofibrant P.P
this : IsIso (F.map (homMk P.ι))
⊢ f = homMk h.h ≫ homMk P.p₀

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
H : (weakEquivalences (BifibrantObject C)).IsInvertedBy F
K L : BifibrantObject C
f g : K ⟶ L
h✝ : homRel C f g
P : PathObject L.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this✝ : IsCofibrant P.P
this : IsIso (F.map (homMk P.ι))
⊢ g = homMk h.h ≫ homMk P.p₁

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (cofibrations C).HasFactorization (trivialFibrations C)
inst✝⁵ : HasPushouts C
inst✝⁴ : (cofibrations C).IsStableUnderComposition
inst✝³ : (cofibrations C).IsStableUnderCobaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (pushout.desc p g ⋯) :=
  (cofibrations C).factorizationData (trivialFibrations C) (pushout.desc p g ⋯)
sq' : CommSq (𝟙 X) (pushout.inl f i ≫ h.i) p h.p
h₁ : WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p)
h₂ : cofibrations C (pushout.inl f i ≫ h.i)
⊢ sq.HasLift

Tactic:
rw [← cofibration_iff] at h₂

Goal state after:
C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (cofibrations C).HasFactorization (trivialFibrations C)
inst✝⁵ : HasPushouts C
inst✝⁴ : (cofibrations C).IsStableUnderComposition
inst✝³ : (cofibrations C).IsStableUnderCobaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (pushout.desc p g ⋯) :=
  (cofibrations C).factorizationData (trivialFibrations C) (pushout.desc p g ⋯)
sq' : CommSq (𝟙 X) (pushout.inl f i ≫ h.i) p h.p
h₁ : WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p)
h₂ : Cofibration (pushout.inl f i ≫ h.i)
⊢ sq.HasLift
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X₁ X₂ : CofibrantObject C
f : X₁ ⟶ X₂
sq :
  CommSq (ι.map (f ≫ X₂.iBifibrantResolutionObj)) X₁.iBifibrantResolutionObj.hom
    (terminal.from (ι.obj (BifibrantObject.ιCofibrantObject.obj X₂.bifibrantResolutionObj)))
    (terminal.from (BifibrantObject.ιCofibrantObject.obj X₁.bifibrantResolutionObj).obj)
⊢ X₁.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map (BifibrantObject.homMk sq.lift) =
    f ≫ X₂.iBifibrantResolutionObj

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : BifibrantObject C
⊢ adjUnit.app (BifibrantObject.HoCat.ιCofibrantObject.obj (BifibrantObject.toHoCat.obj X)) =
    BifibrantObject.HoCat.ιCofibrantObject.map (adjCounitIso.inv.app (BifibrantObject.toHoCat.obj X))

Tactic:
cat_disch

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ {X_1 Y : FundamentalGroupoid X} (f : Path.Homotopic.Quotient X_1.as Y.as),
    f.trans (Quotient.lift (fun f ↦ ⟦f.symm⟧) ⋯ f) = ⟦Path.refl X_1.as⟧

Tactic:
rintro _ _ ⟨f⟩; exact Quotient.sound ⟨(Path.Homotopy.reflTransSymm f).symm⟩

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

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

Tactic:
rw [horn_eq_iSup, hasDimensionLT_iSup_iff]

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ ∀ (i_1 : ↑{i}ᶜ), (stdSimplex.face {↑i_1}ᶜ).toSSet.HasDimensionLT n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case neg
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
x : ↑(Δ[n + 1].nonDegenerate d)
hx : ↑x ∈ A.obj (op ⦋d⦌)
hd : n ≤ d
⊢ ↑x ∈ Λ[n + 1, i].obj (op ⦋d⦌)

Tactic:
obtain ⟨⟨S, hS⟩, rfl⟩ := stdSimplex.nonDegenerateEquiv'.symm.surjective x

Goal state after:
case neg
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 ∈ {S | S.card = d + 1}
hx : ↑(stdSimplex.nonDegenerateEquiv'.symm ⟨S, hS⟩) ∈ A.obj (op ⦋d⦌)
⊢ ↑(stdSimplex.nonDegenerateEquiv'.symm ⟨S, hS⟩) ∈ Λ[n + 1, i].obj (op ⦋d⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
X : SSet
inst✝ : IsFilteredOrEmpty J
F : J ⥤ X.Subcomplex
j : SimplexCategoryᵒᵖ
⊢ (Preorder.colimitCoconeOfIsLUB (F ⋙ evaluation X j) ⋯).cocone.pt = (Preorder.colimitCoconeOfIsLUB F ⋯).cocone.pt.obj j

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
K : Type u'
inst✝⁶ : LinearOrder K
inst✝⁵ : SuccOrder K
inst✝⁴ : OrderBot K
inst✝³ : WellFoundedLT K
inst✝² : W.IsStableUnderTransfiniteCompositionOfShape K
J : Type u''
inst✝¹ : Category.{v'', u''} J
inst✝ : HasIterationOfShape K C
X Y : J ⥤ C
f : X ⟶ Y
hf : (W.functorCategory J).TransfiniteCompositionOfShape K f
j : J
⊢ W (f.app j)

Tactic:
have : W.functorCategory J ≤ W.inverseImage ((evaluation _ _).obj j) := fun _ _ _ h ↦ h _

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
K : Type u'
inst✝⁶ : LinearOrder K
inst✝⁵ : SuccOrder K
inst✝⁴ : OrderBot K
inst✝³ : WellFoundedLT K
inst✝² : W.IsStableUnderTransfiniteCompositionOfShape K
J : Type u''
inst✝¹ : Category.{v'', u''} J
inst✝ : HasIterationOfShape K C
X Y : J ⥤ C
f : X ⟶ Y
hf : (W.functorCategory J).TransfiniteCompositionOfShape K f
j : J
this : W.functorCategory J ≤ W.inverseImage ((evaluation J C).obj j)
⊢ W (f.app j)
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
W : MorphismProperty C
J : Type u''
inst✝⁷ : Category.{v'', u''} J
K : Type u'
inst✝⁶ : LinearOrder K
inst✝⁵ : SuccOrder K
inst✝⁴ : OrderBot K
inst✝³ : WellFoundedLT K
inst✝² : (monomorphisms C).IsStableUnderTransfiniteCompositionOfShape K
inst✝¹ : HasPullbacks C
inst✝ : HasIterationOfShape K C
⊢ (monomorphisms (J ⥤ C)).IsStableUnderTransfiniteCompositionOfShape K

Tactic:
rw [← functorCategory_monomorphisms]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u''
inst✝³ : Category.{v'', u''} J
K' : Type u'
inst✝² : (monomorphisms C).IsStableUnderCoproductsOfShape K'
inst✝¹ : HasCoproductsOfShape K' C
inst✝ : HasPullbacks C
⊢ (monomorphisms (J ⥤ C)).IsStableUnderCoproductsOfShape K'

Tactic:
rw [← functorCategory_monomorphisms]
  infer_instance

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

Goal state before:
pp: ⊢ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2} = Λ[2, 2]

Tactic:
apply le_antisymm
    · rw [sup_le_iff]
      constructor
      · exact face_le_horn (1 : Fin 3) 2 (by simp)
      · exact face_le_horn (0 : Fin 3) 2 (by simp)
    · rw [horn_eq_iSup, iSup_le_iff]
      rintro i
      fin_cases i
      · exact le_sup_right
      · exact le_sup_left

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

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
⊢ pushout.inl t l ≫ φ ≫ k = r'

Tactic:
cat_disch

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

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
⊢ pushout.inr t l ≫ φ ≫ k = b'

Tactic:
cat_disch

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

Goal state before:
pp: X : SSet
n : ℕ
f : X.Path n
j l : ℕ
k' : Fin l
k : Fin n
h : j + l ≤ n
hkk' : j + ↑k' = ↑k
⊢ (f.interval j l h).arrow k' = f.arrow k

Tactic:
dsimp [interval, arrow, Truncated.Path.interval, Truncated.Path.arrow]

Goal state after:
X : SSet
n : ℕ
f : X.Path n
j l : ℕ
k' : Fin l
k : Fin n
h : j + l ≤ n
hkk' : j + ↑k' = ↑k
⊢ f.arrow ⟨j + ↑k', ⋯⟩ = f.arrow k
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
⊢ ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
    (((coyoneda.obj (op (𝟙_ C))).map f ⊗ₘ (coyoneda.obj (op (𝟙_ C))).map g) ≫ ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) =
      (↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫ (coyoneda.obj (op (𝟙_ C))).map (f ⊗ₘ g)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
n : ℕ
f : nerve C _⦋1⦌
s : nerve C _⦋n⦌
h :
  (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) f =
    (ConcreteCategory.hom ((nerve C).map (⦋0⦌.const ⦋n⦌ 0).op)) s
⊢ ComposableArrows.hom
      ((ConcreteCategory.hom ((nerve C).map (mkOfSucc 0).op))
        (ComposableArrows.precomp s (ComposableArrows.hom f ≫ eqToHom ⋯))) =
    eqToHom ⋯ ≫ ComposableArrows.hom f ≫ eqToHom ⋯

Tactic:
cat_disch

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i✝ : SimplexCategoryᵒᵖ
a✝ : X.obj i✝
val✝ : (X ⊗ Y).obj i✝
left✝ : val✝.1 ∈ A.obj i✝
right✝ : val✝.2 ∈ B.obj i✝
h✝ : (ConcreteCategory.hom (((A.prod B).ι ≫ fst X Y).app i✝)) ⟨val✝, ⋯⟩ = a✝
⊢ a✝ ∈ A.obj i✝

Tactic:
cat_disch

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i✝ : SimplexCategoryᵒᵖ
a✝ : Y.obj i✝
val✝ : (X ⊗ Y).obj i✝
left✝ : val✝.1 ∈ A.obj i✝
right✝ : val✝.2 ∈ B.obj i✝
h✝ : (ConcreteCategory.hom (((A.prod B).ι ≫ snd X Y).app i✝)) ⟨val✝, ⋯⟩ = a✝
⊢ a✝ ∈ B.obj i✝

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C✝ : Type u₁
inst✝² : EnrichedCategory V C✝
C : Type v
inst✝¹ : EnrichedCategory (Type v) C
D : Type v
inst✝ : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
⊢ ∀ {X Y : Type vᵒᵖ} (f : X ⟶ Y),
    (enrichedNatTransYoneda F G).map f ≫
        { hom := ↾fun σ ↦ ↾fun x ↦ { app := fun X ↦ (ConcreteCategory.hom (σ.app X)) x, naturality := ⋯ },
            inv := ↾fun σ ↦ { app := fun X ↦ ↾fun x ↦ ((TypeCat.Hom.hom σ) x).app X, naturality := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom =
      { hom := ↾fun σ ↦ ↾fun x ↦ { app := fun X_1 ↦ (ConcreteCategory.hom (σ.app X_1)) x, naturality := ⋯ },
            inv := ↾fun σ ↦ { app := fun X_1 ↦ ↾fun x ↦ ((TypeCat.Hom.hom σ) x).app X_1, naturality := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        (yoneda.obj (enrichedFunctorTypeEquivFunctor F ⟶ enrichedFunctorTypeEquivFunctor G)).map f

Tactic:
cat_disch

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

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : (X ⊗ Y).obj n
⊢ x ∈ {p | p.1 ∈ Set.univ ∧ p.2 ∈ T.obj n} ∪ {p | p.1 ∈ S.obj n ∧ p.2 ∈ Set.univ} ↔ x.2 ∈ T.obj n ∨ x.1 ∈ S.obj n

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_3
W : Type u_4
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
F : V ⥤rq W
⊢ ∀ (a b : V) (e : a ⟶ b),
    (FreeRefl.quotientFunctor V ⋙ freeReflMap F).map e.toPath =
      eqToHom ⋯ ≫ (freeMap F.toPrefunctor ⋙ FreeRefl.quotientFunctor W).map e.toPath ≫ eqToHom ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
v w : ReflQuiv
f : v ⟶ w
⊢ ((ReflQuiv.forgetToQuiv ⋙ free).map f ≫ (FreeRefl.quotientFunctor ↑w).toCatHom).toFunctor.obj =
    ((FreeRefl.quotientFunctor ↑v).toCatHom ≫ freeRefl.map f).toFunctor.obj

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
v w : ReflQuiv
f : v ⟶ w
⊢ ∀ (a b : ↑(Quiv.of ↑v)) (e : a ⟶ b),
    ((ReflQuiv.forgetToQuiv ⋙ free).map f ≫ (FreeRefl.quotientFunctor ↑w).toCatHom).toFunctor.map e.toPath =
      eqToHom ⋯ ≫ ((FreeRefl.quotientFunctor ↑v).toCatHom ≫ freeRefl.map f).toFunctor.map e.toPath ≫ eqToHom ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : ReflQuiver W
inst✝² : ReflQuiver V
C : Type u_3
D : Type u_4
inst✝¹ : Category.{v_1, u_3} C
inst✝ : Category.{v_2, u_4} D
F : Cat.FreeRefl V ⥤ C
⊢ ∀ (v : V),
    (Cat.FreeRefl.lift ((fun F ↦ Cat.toFreeRefl V ⋙rq F.toReflPrefunctor) F)).obj (Cat.FreeRefl.mk v) =
      F.obj (Cat.FreeRefl.mk v)

Tactic:
cat_disch

Goal state after: