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

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev =
    ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev - (P q).f (n + 1) ≫ (Hσ q).f (n + 1)

Tactic:
conv_rhs => rw [sub_eq_add_neg, add_comm]

Goal state after:
case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev =
    -(P q).f (n + 1) ≫ (Hσ q).f (n + 1) + ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ
i : Δ ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

Tactic:
simp only [SimplexCategory.eq_id_of_mono i, comp_id, id_comp, mapMono_id K]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ (toKaroubi (ChainComplex C ℕ)).whiskerLeft N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom

Tactic:
let e : _ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 _ := N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
e : toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 (Karoubi (ChainComplex C ℕ)) :=
  N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀
⊢ (toKaroubi (ChainComplex C ℕ)).whiskerLeft N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ natTrans.app P = (N₂ ⋙ Γ₂).map P.decompId_i ≫ (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app P.X ≫ P.decompId_p

Tactic:
dsimp only [natTrans]
  simp only [whiskeringLeft_obj_preimage_app, Functor.id_map]

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 : C
f : X ⟶ Y
⊢ WeakEquivalence (resolutionMap f) ↔ WeakEquivalence f

Tactic:
rw [← weakEquivalence_postcomp_iff _ (pResolutionObj Y),
    HoCat.resolutionMap_fac, weakEquivalence_precomp_iff]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithFibrations C
inst✝ : (fibrations C).IsStableUnderRetracts
⊢ (fibrations (Over S)).IsStableUnderRetracts

Tactic:
rw [fibrations_over_def, MorphismProperty.over_eq_inverseImage]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithFibrations C
inst✝ : (fibrations C).IsStableUnderRetracts
⊢ ((fibrations C).inverseImage (Over.forget S)).IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
γ₀ : Homotopic.Quotient x₀ x₁
γ₁ : Homotopic.Quotient x₁ x₂
γ₂ : Homotopic.Quotient x₂ x₃
⊢ (γ₀.trans γ₁).trans γ₂ = γ₀.trans (γ₁.trans γ₂)

Tactic:
induction γ₀ using Quotient.ind with | mk γ₀ =>
  induction γ₁ using Quotient.ind with | mk γ₁ =>
  induction γ₂ using Quotient.ind with | mk γ₂ =>
  simpa [← mk_trans, eq] using Homotopic.trans_assoc γ₀ γ₁ γ₂

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

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
ha : objEquiv.symm (𝟙 (unop (op ⦋n⦌))) ∈ A.obj (op ⦋n⦌)
⊢ ⊤ ≤ A

Tactic:
simpa [← ofSimplex_objEquiv_symm_id]

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

Goal state after:
case hinj
J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
i j : J
x : X
hx : x ∈ F.obj i
y : X
hy : y ∈ F.obj j
h :
  (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) ⟨x, hx⟩ =
    (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app j)) ⟨y, hy⟩
⊢ ∃ k f g,
    (ConcreteCategory.hom ((F ⋙ functorToTypes).map f)) ⟨x, hx⟩ =
      (ConcreteCategory.hom ((F ⋙ functorToTypes).map g)) ⟨y, hy⟩
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
⊢ (ConcreteCategory.hom c'.inl) x₁ = (ConcreteCategory.hom c'.inr) x₂ →
    (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂

Tactic:
· apply pushoutCocone_inl_eq_inr_imp_of_iso e.symm

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

Goal state before:
pp: case some.left
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 (some WalkingPair.left)
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom (h.cocone.ι.app (some WalkingPair.left))) x) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom (h.cocone.ι.app (some WalkingPair.left))) x

pp: case some.right
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 (some WalkingPair.right)
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom (h.cocone.ι.app (some WalkingPair.right))) x) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom (h.cocone.ι.app (some WalkingPair.right))) x

Tactic:
· exact Or.inl ⟨x, rfl⟩

Goal state after:
case some.right
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 (some WalkingPair.right)
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom (h.cocone.ι.app (some WalkingPair.right))) x) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom (h.cocone.ι.app (some WalkingPair.right))) x
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X : SSet
⊢ X.Quasicategory ↔ InnerFibration (terminal.from X)

Tactic:
by
  rw [quasicategory_iff_hasLiftingProperty.{u} _ terminalIsTerminal, innerFibration_iff]
  exact ⟨fun h _ _ _ ⟨i, h0, hn⟩ ↦ h h0 hn,
    fun h _ _ h0 hn ↦ h _ (horn_ι_mem_innerHornInclusions h0 hn)⟩

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

Goal state before:
pp: case h.inr.inr.zero.«0»
X : SSet
sx : X.StrictSegal
j : Fin (0 + 3)
ksucc : Fin (0 + 1 + 1 + 1) := (Fin.succ 0).castSucc
heq : j = ksucc
σ₀ : Λ[0 + 2, (fun i ↦ i) ⟨0, ⋯⟩].toSSet ⟶ X
h₀ : 0 < (fun i ↦ i) ⟨0, ⋯⟩
hₙ : (fun i ↦ i) ⟨0, ⋯⟩ < Fin.last (0 + 2)
hj : j ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j))
        (sx.spineToSimplex ((horn.spineId ((fun i ↦ i) ⟨0, ⋯⟩) h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, (fun i ↦ i) ⟨0, ⋯⟩].toSSet.map (mkOfSucc 0).op ≫ σ₀.app (Opposite.op ⦋1⦌)))
      (horn.face ((fun i ↦ i) ⟨0, ⋯⟩) j hj)

Tactic:
contradiction

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

Goal state before:
pp: case h.inr.inr.zero.«1»
X : SSet
sx : X.StrictSegal
j : Fin (0 + 3)
ksucc : Fin (0 + 1 + 1 + 1) := (Fin.succ 0).castSucc
heq : j = ksucc
σ₀ : Λ[0 + 2, (fun i ↦ i) ⟨1, ⋯⟩].toSSet ⟶ X
h₀ : 0 < (fun i ↦ i) ⟨1, ⋯⟩
hₙ : (fun i ↦ i) ⟨1, ⋯⟩ < Fin.last (0 + 2)
hj : j ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j))
        (sx.spineToSimplex ((horn.spineId ((fun i ↦ i) ⟨1, ⋯⟩) h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, (fun i ↦ i) ⟨1, ⋯⟩].toSSet.map (mkOfSucc 0).op ≫ σ₀.app (Opposite.op ⦋1⦌)))
      (horn.face ((fun i ↦ i) ⟨1, ⋯⟩) j hj)

Tactic:
contradiction

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

Goal state before:
pp: case h.inr.inr.zero.«2»
X : SSet
sx : X.StrictSegal
j : Fin (0 + 3)
ksucc : Fin (0 + 1 + 1 + 1) := (Fin.succ 0).castSucc
heq : j = ksucc
σ₀ : Λ[0 + 2, (fun i ↦ i) ⟨2, ⋯⟩].toSSet ⟶ X
h₀ : 0 < (fun i ↦ i) ⟨2, ⋯⟩
hₙ : (fun i ↦ i) ⟨2, ⋯⟩ < Fin.last (0 + 2)
hj : j ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j))
        (sx.spineToSimplex ((horn.spineId ((fun i ↦ i) ⟨2, ⋯⟩) h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, (fun i ↦ i) ⟨2, ⋯⟩].toSSet.map (mkOfSucc 0).op ≫ σ₀.app (Opposite.op ⦋1⦌)))
      (horn.face ((fun i ↦ i) ⟨2, ⋯⟩) j hj)

Tactic:
contradiction

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

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ range ((S.unionProd T).ι ≫ (β_ X Y).hom) ≤ T.unionProd S

Tactic:
by simp [range_comp]

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

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ range ((T.unionProd S).ι ≫ (β_ Y X).hom) ≤ S.unionProd T

Tactic:
by simp [range_comp]

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

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : ForgetEnrichment W (TransportEnrichment F D)
⊢ (e (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)).symm (ForgetEnrichment.homTo W (𝟙 X)) =
    eId V (ForgetEnrichment.to W X)

Tactic:
apply Equiv.injective (e _)

Goal state after:
V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : ForgetEnrichment W (TransportEnrichment F D)
⊢ (e (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X))
      ((e (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)).symm (ForgetEnrichment.homTo W (𝟙 X))) =
    (e (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)) (eId V (ForgetEnrichment.to W X))
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : ForgetEnrichment W (TransportEnrichment F D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W (f ≫ g)) =
    (λ_ (𝟙_ V)).inv ≫
      ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)).symm (ForgetEnrichment.homTo W f) ⊗ₘ
          (e (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W g)) ≫
        eComp V (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)

Tactic:
apply Equiv.injective (e _)

Goal state after:
V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : ForgetEnrichment W (TransportEnrichment F D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Z✝))
      ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W (f ≫ g))) =
    (e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Z✝))
      ((λ_ (𝟙_ V)).inv ≫
        ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)).symm (ForgetEnrichment.homTo W f) ⊗ₘ
            (e (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W g)) ≫
          eComp V (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝))
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
x y : V
e : x ⟶ y
⊢ MorphismProperty.ofHoms (fun e ↦ homMk e.snd.snd) (homMk e)

Tactic:
rw [MorphismProperty.ofHoms_iff]

Goal state after:
V : Type u_1
inst✝ : ReflQuiver V
x y : V
e : x ⟶ y
⊢ ∃ i, Arrow.mk (homMk e) = Arrow.mk (homMk i.snd.snd)
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
⊢ ⊤ ≤ (morphismPropertyHomMk V).multiplicativeClosure

Tactic:
intro _ _ f hf

Goal state after:
V : Type u_1
inst✝ : ReflQuiver V
X✝ Y✝ : FreeRefl V
f : X✝ ⟶ Y✝
hf : ⊤ f
⊢ (morphismPropertyHomMk V).multiplicativeClosure f
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x₀ x₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e' : Edge x₀ y₁
h : e.edge = e'.edge
⊢ x₁ = y₁

Tactic:
← e.tgt_eq,

Goal state after:
V : Truncated 2
x₀ x₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e' : Edge x₀ y₁
h : e.edge = e'.edge
⊢ (ConcreteCategory.hom (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op)) e.edge = y₁
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x y
⊢ MorphismProperty.ofHoms (fun e ↦ homMk e.snd.snd) (homMk e)

Tactic:
rw [MorphismProperty.ofHoms_iff]

Goal state after:
V : Truncated 2
x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x y
⊢ ∃ i, Arrow.mk (homMk e) = Arrow.mk (homMk i.snd.snd)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
W : MorphismProperty V.HomotopyCategory
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} (e : Edge x y), W (homMk e)
X Y : V.HomotopyCategory
fst✝¹ fst✝ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge fst✝¹ fst✝
⊢ W (homMk ⟨fst✝¹, ⟨fst✝, e⟩⟩.snd.snd)

Tactic:
exact hW e

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f : a ⟶ b
⊢ generators.multiplicativeClosure ≤ P

Tactic:
intro _ _ f hf

Goal state after:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
hf : generators.multiplicativeClosure f
⊢ P f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
⊢ generators.multiplicativeClosure' ≤ P

Tactic:
intro _ _ f hf

Goal state after:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
hf : generators.multiplicativeClosure' f
⊢ P f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ mk (n + 1) ⟶ mk n

Tactic:
induction i using Fin.lastCases with

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ IsSplitMono m

Tactic:
induction hm with
  | of x hx => cases hx; infer_instance
  | id => infer_instance
  | comp_of _ _ _ h => cases h; infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
⊢ W = ⊤

Tactic:
by
  have hW (d : ℕ) : W.inverseImage (Truncated.inclusion d) = ⊤ :=
    Truncated.morphismProperty_eq_top _ (fun _ _ i ↦ δ_mem i)
      (fun _ _ i ↦ σ_mem i)
  ext a b f
  simp only [MorphismProperty.top_apply, iff_true]
  change W.inverseImage (Truncated.inclusion (max a.len b.len))
    (Truncated.Hom.tr f (ha := by simp) (hb := by simp))
  simp only [hW, MorphismProperty.top_apply]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
H :
  ∀ {k k' : K} (φ : k ⟶ k'),
    ∃ j f,
      (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) (z k')
j : {k k' : K} → (k ⟶ k') → J := fun {k k'} φ ↦ ⋯.choose
g : {k k' : K} → (φ : k ⟶ k') → j₀ ⟶ j φ := fun {k k'} φ ↦ ⋯.choose
⊢ ∃ j₁ α,
    ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')

Tactic:
have hg {k k' : K} (φ : k ⟶ k') :
        (F.obj k').map (X.map (g φ)) ((F.map φ).app _ (z k)) =
          (F.obj k').map (X.map (g φ)) (z k') := (H φ).choose_spec.choose_spec

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
H :
  ∀ {k k' : K} (φ : k ⟶ k'),
    ∃ j f,
      (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) (z k')
j : {k k' : K} → (k ⟶ k') → J := fun {k k'} φ ↦ ⋯.choose
g : {k k' : K} → (φ : k ⟶ k') → j₀ ⟶ j φ := fun {k k'} φ ↦ ⋯.choose
hg :
  ∀ {k k' : K} (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map (g φ)))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map (g φ)))) (z k')
⊢ ∃ j₁ α,
    ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c x' : f.Cell j
y : Δ[x'.dim + 1] _⦋c.dim + 1⦌
hy' : y ∈ x'.horn.obj (op ⦋c.dim + 1⦌)
hy :
  (ConcreteCategory.hom (x'.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)))
      ((ConcreteCategory.hom (x'.horn.ι.app (op ⦋c.dim + 1⦌))) ⟨y, hy'⟩) =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)))
      (stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋c.dim + 1⦌))))
⊢ False

Tactic:
ιSigmaStdSimplex_eq_iff

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c x' : f.Cell j
y : Δ[x'.dim + 1] _⦋c.dim + 1⦌
hy' : y ∈ x'.horn.obj (op ⦋c.dim + 1⦌)
hy :
  ∃ (h : x' = c),
    stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋c.dim + 1⦌))) =
      cast ⋯ ((ConcreteCategory.hom (x'.horn.ι.app (op ⦋c.dim + 1⦌))) ⟨y, hy'⟩)
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c x' : f.Cell j
y : Δ[x'.dim + 1] _⦋c.dim⦌
hy' : y ∈ x'.horn.obj (op ⦋c.dim⦌)
hy :
  (ConcreteCategory.hom (x'.ιSigmaStdSimplex.app (op ⦋c.dim⦌)))
      ((ConcreteCategory.hom (x'.horn.ι.app (op ⦋c.dim⦌))) ⟨y, hy'⟩) =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index))
⊢ False

Tactic:
ιSigmaStdSimplex_eq_iff

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c x' : f.Cell j
y : Δ[x'.dim + 1] _⦋c.dim⦌
hy' : y ∈ x'.horn.obj (op ⦋c.dim⦌)
hy :
  ∃ (h : x' = c),
    stdSimplex.objEquiv.symm (SimplexCategory.δ c.index) =
      cast ⋯ ((ConcreteCategory.hom (x'.horn.ι.app (op ⦋c.dim⦌))) ⟨y, hy'⟩)
⊢ False