mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
e : J ≃o J'
⊢ W.IsStableUnderTransfiniteCompositionOfShape J ↔ W.IsStableUnderTransfiniteCompositionOfShape J'

Tactic:
simp only [isStableUnderTransfiniteCompositionOfShape_iff,
    W.transfiniteCompositionsOfShape_eq_of_orderIso e]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: case inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃

Tactic:
obtain hi₂₃ | rfl := hi'.lt_or_eq

Goal state after:
case inl.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃

case inl.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₁₂ : i₁ < i₂
hi' : i₂ ≤ i₂
hi₃ : i₂ ≤ j
⊢ map c i₁ i₂ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₂ hi' hi₃
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case inr
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k : J
h₁ : k ≤ j₁
h₂ : k ≤ j₂
this :
  ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂),
    j₁ ≤ j₂ → iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩
h : ¬j₁ ≤ j₂
⊢ iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩

Tactic:
exact (this iter₂ iter₁ h₂ h₁ (le_of_lt (by simpa using h))).symm

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
⊢ n * (↑p).valuation + c.valuation = n + c.valuation

Tactic:
valuation_p,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
⊢ n * 1 + c.valuation = n + c.valuation
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝⁸ : Category.{v', u'} A
inst✝⁷ : LocallySmall.{w, v, u} C
inst✝⁶ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁵ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory A FC
inst✝³ : (forget A).ReflectsIsomorphisms
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
hJ : J.HasSheafCompose (forget A)
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝¹ : HasWeakSheafify J A
inst✝ : HasProducts A
⊢ J.W f ↔ ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map f)

Tactic:
GrothendieckTopology.W_iff,

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝⁸ : Category.{v', u'} A
inst✝⁷ : LocallySmall.{w, v, u} C
inst✝⁶ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁵ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory A FC
inst✝³ : (forget A).ReflectsIsomorphisms
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
hJ : J.HasSheafCompose (forget A)
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝¹ : HasWeakSheafify J A
inst✝ : HasProducts A
⊢ IsIso ((presheafToSheaf J A).map f) ↔ ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map f)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
this : padicNormE (↑(limSeq f j) - ↑f (max N N2) + (↑f (max N N2) - ↑(limSeq f (max N N2)))) < ε
⊢ padicNorm p (limSeq f j - limSeq f (max N N2)) < ε

Tactic:
ring_nf at this

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
this : padicNormE (↑(limSeq f j) - ↑(limSeq f (max N N2))) < ε
⊢ padicNorm p (limSeq f j - limSeq f (max N N2)) < ε
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation 1 = 0

Tactic:
← Nat.cast_one,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (↑1).valuation = 0
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
q' : Fin (n + 1) := ⟨q, ⋯⟩
⊢ ∑ 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

Tactic:
rw [← @Finset.add_sum_erase _ _ _ _ _ _ q' (by simp [q'])]

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
q' : Fin (n + 1) := ⟨q, ⋯⟩
⊢ (P ↑q').f (n + 1) ≫ X.δ q'.rev.succ ≫ X.σ q'.rev +
      ∑ x ∈ {i | ↑i < q + 1}.erase q', (P ↑x).f (n + 1) ≫ X.δ x.rev.succ ≫ X.σ x.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 h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ ⦋n + 1⦌ ≠ ⦋n⦌

Tactic:
intro h
    exact (Nat.succ_ne_self n) (congr_arg SimplexCategory.len h)

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

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

Tactic:
← PInfty.comm j k,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬Mono A.e
⊢ (s.cofan (op ⦋j⦌)).inj A ≫ PInfty.f j ≫ K[X].d j k = 0
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
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ ((Γ₀.splitting K[X]).ι n ≫
      ((Γ₀.splitting K[X]).desc (op ⦋n⦌) fun A ↦
          (PInfty.f (unop A.fst).len ≫ f.app A.fst) ≫ ((Γ₀.splitting K[Y]).cofan (op ⦋n⦌)).inj A) ≫
        (Γ₀.splitting K[Y]).desc (op ⦋n⦌) fun A ↦ PInfty.f (unop A.fst).len ≫ Y.map A.e.op) =
    (Γ₀.splitting K[X]).ι n ≫
      ((Γ₀.splitting K[X]).desc (op ⦋n⦌) fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op) ≫ f.app (op ⦋n⦌)

Tactic:
simp only [← Splitting.cofan_inj_id, Splitting.ι_desc, Splitting.ι_desc_assoc, assoc,
      PInfty_f_idem_assoc, PInfty_f_naturality_assoc,
      NatTrans.naturality, Splitting.IndexSet.id_fst, unop_op, len_mk]

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: G : Type u
inst✝ : Group G
x y : SingleObj G
f : x ⟶ y
⊢ inv f = f⁻¹

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Goal state after:
G : Type u
inst✝ : Group G
x y : SingleObj G
f : x ⟶ y
⊢ f ≫ f⁻¹ = 𝟙 x
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hcof : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lcofπ : HoCat C ⥤ Hcof := (weakEquivalences (HoCat C)).Q
Lcof : CofibrantObject C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := (weakEquivalences C).Localization
⊢ (localizerMorphism C).IsLocalizedEquivalence

Tactic:
let L : C ⥤ H := (weakEquivalences C).Q

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hcof : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lcofπ : HoCat C ⥤ Hcof := (weakEquivalences (HoCat C)).Q
Lcof : CofibrantObject C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
⊢ (localizerMorphism C).IsLocalizedEquivalence
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
x✝¹ x✝ : X ⟶ Y
h : RightHomotopyRel x✝¹ x✝
⊢ toHoCat.map (homMk x✝¹) = toHoCat.map (homMk x✝)

Tactic:
toHoCat_map_eq_iff

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
x✝¹ x✝ : X ⟶ Y
h : RightHomotopyRel x✝¹ x✝
⊢ homRel C (homMk x✝¹) (homMk x✝)
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

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

Tactic:
have := (ObjectProperty.ι _).congr_map
          (bifibrantResolutionMap_fac (CofibrantObject.homMk f.hom)).symm

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X₁ X₂ : BifibrantObject C
f : X₁ ⟶ X₂
this :
  (cofibrantObjects C).ι.map (homMk f.hom ≫ (mk X₂.obj).iBifibrantResolutionObj) =
    (cofibrantObjects C).ι.map ((mk X₁.obj).iBifibrantResolutionObj ≫ homMk (bifibrantResolutionMap (homMk f.hom)).hom)
⊢ f ≫ BifibrantObject.homMk (mk X₂.obj).iBifibrantResolutionObj.hom =
    BifibrantObject.homMk (mk X₁.obj).iBifibrantResolutionObj.hom ≫
      bifibrantResolutionMap (BifibrantObject.ιCofibrantObject.map f)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 3)
⊢ ∀ (k : Fin (n + 3)) (hj : j ≠ i) (hk : k ≠ i) (hjk : j < k),
    (stdSimplex.δ (k.pred ⋯) ≫ ι i j hj) ≫ g = (stdSimplex.δ (j.castPred ⋯) ≫ ι i k hk) ≫ g

Tactic:
k

Goal state after:
case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j k : Fin (n + 3)
⊢ ∀ (hj : j ≠ i) (hk : k ≠ i) (hjk : j < k),
    (stdSimplex.δ (k.pred ⋯) ≫ ι i j hj) ≫ g = (stdSimplex.δ (j.castPred ⋯) ≫ ι i k hk) ≫ g
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: 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 ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)) ∈
    ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ ∃ x₁,
    (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) x₁ =
        ⟨↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)),
          hx⟩ ∧
      (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) x₁ = (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y

Tactic:
refine ⟨c.ιSigmaBoundary.app _ ⟨y, ?_⟩, ?_, ?_⟩

Goal state after:
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 ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)) ∈
    ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ y ∈ ∂Δ[d].obj (op ⦋n⦌)

case refine_2
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 ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)) ∈
    ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ (ConcreteCategory.hom ((t i d).app (op ⦋n⦌)))
      ((ConcreteCategory.hom (c.ιSigmaBoundary.app (op ⦋n⦌))) ⟨y, ?refine_1⟩) =
    ⟨↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)), hx⟩

case refine_3
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 ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)) ∈
    ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ (ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
      ((ConcreteCategory.hom (c.ιSigmaBoundary.app (op ⦋n⦌))) ⟨y, ?refine_1⟩) =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ horn.faceι 1 0 ι₀._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀

Tactic:
exact (horn.isColimit 1).fac _ (.right ⟨0, by simp⟩)

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

Goal state before:
pp: X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ι₃ ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = f₃

Tactic:
rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 3).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]
  exact (horn.isColimit 1).fac _ (.right ⟨3, by simp⟩)

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ₘ })
a : ℕ
hₐ : a ≤ n + 1
φ : { obj := ⦋a⦌, property := hₐ } ⟶ { obj := ⦋m⦌, property := hₘ }
i : Fin (a + 1)
⊢ (X.spine a hₐ ((ConcreteCategory.hom (X.map φ.op)) Δ)).vertex i = (X.spine m hₘ Δ).vertex ((Hom.toOrderHom φ.hom) i)

Tactic:
by
  dsimp only [spine_vertex]
  rw [← Functor.map_comp_apply, ← op_comp, ← tr_comp',
    SimplexCategory.const_comp]

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ (X.spine n ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex f))).arrow i = f.arrow i.castSucc

Tactic:
simp only [SimplicialObject.δ, spine_arrow]

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i).op)) ((ConcreteCategory.hom (X.map (δ j).op)) (sx.spineToSimplex f)) =
    f.arrow i.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ (X.spine n ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex f))).arrow i = f.arrow i.succ

Tactic:
simp only [SimplicialObject.δ, spine_arrow]

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i).op)) ((ConcreteCategory.hom (X.map (δ j).op)) (sx.spineToSimplex f)) =
    f.arrow i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ (X.spine n ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex f))).arrow i =
    sx.spineToDiagonal (f.interval (↑i) 2 ⋯)

Tactic:
simp only [SimplicialObject.δ, spine_arrow]

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i).op)) ((ConcreteCategory.hom (X.map (δ j).op)) (sx.spineToSimplex f)) =
    sx.spineToDiagonal (f.interval (↑i) 2 ⋯)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp (𝟙 (𝟙 a)) η ≍ η

Tactic:
rw [id_eq, ← Functor.map_id]

Goal state after:
C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp ((eId Cat a).toFunctor.map (𝟙 { down := { as := () } })) η ≍ η
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp η (𝟙 (𝟙 b)) ≍ η

Tactic:
rw [id_eq, ← Functor.map_id]

Goal state after:
C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp η ((eId Cat b).toFunctor.map (𝟙 { down := { as := () } })) ≍ η
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
⊢ 𝟙 ((X.fst ⊗ Y.fst) ⊗ U ⊗ U') ⊗≫
      X.fst ◁ (Y.snd.β U).hom ▷ U' ⊗≫
        ((X.fst ⊗ U) ◁ (Y.snd.β U').hom ≫ (X.snd.β U).hom ▷ (U' ⊗ Y.fst)) ⊗≫
          U ◁ (X.snd.β U').hom ▷ Y.fst ⊗≫ 𝟙 ((U ⊗ U') ⊗ X.fst ⊗ Y.fst) =
    (α_ (X.fst ⊗ Y.fst) U U').inv ≫
      ((α_ X.fst Y.fst U).hom ≫
            X.fst ◁ (Y.snd.β U).hom ≫ (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom) ▷
          U' ≫
        (α_ U (X.fst ⊗ Y.fst) U').hom ≫
          U ◁
              ((α_ X.fst Y.fst U').hom ≫
                X.fst ◁ (Y.snd.β U').hom ≫
                  (α_ X.fst U' Y.fst).inv ≫ (X.snd.β U').hom ▷ Y.fst ≫ (α_ U' X.fst Y.fst).hom) ≫
            (α_ U U' (X.fst ⊗ Y.fst)).inv

Tactic:
by rw [whisker_exchange]; monoidal

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.fst ⊗ U) ◁ f.f ≫ (X.snd.β U).hom ▷ Y₂.fst) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    ((α_ X.fst Y₁.fst U).hom ≫
        X.fst ◁ (Y₁.snd.β U).hom ≫ (α_ X.fst U Y₁.fst).inv ≫ (X.snd.β U).hom ▷ Y₁.fst ≫ (α_ U X.fst Y₁.fst).hom) ≫
      U ◁ X.fst ◁ f.f

Tactic:
by rw [whisker_exchange]; monoidal

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

Goal state before:
pp: case h.comp.δ
x y : SimplexCategoryGenRel
x✝ y✝ : Paths FreeSimplexQuiver
u✝ : FreeSimplexQuiver
n✝ : ℕ
i✝ : Fin (n✝ + 2)
p✝ : (Paths.of FreeSimplexQuiver).obj u✝ ⟶ (Paths.of FreeSimplexQuiver).obj (FreeSimplexQuiver.mk n✝)
h : generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p✝)
⊢ generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map
      (p✝ ≫ (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i✝)))

pp: case h.comp.σ
x y : SimplexCategoryGenRel
x✝ y✝ : Paths FreeSimplexQuiver
u✝ : FreeSimplexQuiver
n✝ : ℕ
i✝ : Fin (n✝ + 1)
p✝ : (Paths.of FreeSimplexQuiver).obj u✝ ⟶ (Paths.of FreeSimplexQuiver).obj (FreeSimplexQuiver.mk (n✝ + 1))
h : generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p✝)
⊢ generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map
      (p✝ ≫ (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ i✝)))

Tactic:
· exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .δ _

Goal state after:
case h.comp.σ
x y : SimplexCategoryGenRel
x✝ y✝ : Paths FreeSimplexQuiver
u✝ : FreeSimplexQuiver
n✝ : ℕ
i✝ : Fin (n✝ + 1)
p✝ : (Paths.of FreeSimplexQuiver).obj u✝ ⟶ (Paths.of FreeSimplexQuiver).obj (FreeSimplexQuiver.mk (n✝ + 1))
h : generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p✝)
⊢ generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map
      (p✝ ≫ (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ i✝)))
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: case h.comp.σ
x y : SimplexCategoryGenRel
x✝ y✝ : Paths FreeSimplexQuiver
u✝ : FreeSimplexQuiver
n✝ : ℕ
i✝ : Fin (n✝ + 1)
p✝ : (Paths.of FreeSimplexQuiver).obj u✝ ⟶ (Paths.of FreeSimplexQuiver).obj (FreeSimplexQuiver.mk (n✝ + 1))
h : generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p✝)
⊢ generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map
      (p✝ ≫ (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ i✝)))

Tactic:
exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .σ _

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

Goal state before:
pp: case comp_of
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
h' : (∃ (h : x✝ = y✝), i = eqToHom h) ∨ x✝.len < y✝.len
⊢ (∃ (h : x✝ = z✝), i ≫ u = eqToHom h) ∨ x✝.len < z✝.len

Tactic:
rcases h' with ⟨e, _⟩ | h' <;>
    apply Or.inr <;>
    cases hg

Goal state after:
case comp_of.inl.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
e : x✝ = mk n✝
h✝ : i = eqToHom e
⊢ x✝.len < (mk (n✝ + 1)).len

case comp_of.inr.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
h' : x✝.len < (mk n✝).len
⊢ x✝.len < (mk (n✝ + 1)).len
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons_cons
x✝ y✝ : ℕ
xs✝ : List ℕ
a✝ :
  ∀ {m : ℕ},
    IsAdmissible m xs✝ ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) xs✝ ∧ ∀ (k : ℕ) (h : k < xs✝.length), xs✝[k] ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs✝) ↔
      List.IsChain (fun x1 x2 ↦ x1 < x2) (y :: xs✝) ∧ ∀ (k : ℕ) (h : k < (y :: xs✝).length), (y :: xs✝)[k] ≤ m + k
m : ℕ
⊢ x✝ < y✝ ∧
      (List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝) ∧
          ∀ (k : ℕ) (h : k < (y✝ :: xs✝).length), (y✝ :: xs✝)[k] ≤ m + 1 + k) ∧
        x✝ ≤ m ↔
    List.IsChain (fun x1 x2 ↦ x1 < x2) (x✝ :: y✝ :: xs✝) ∧
      ∀ (k : ℕ) (h : k < (x✝ :: y✝ :: xs✝).length), (x✝ :: y✝ :: xs✝)[k] ≤ m + k

Tactic:
List.length_cons,

Goal state after:
case cons_cons
x✝ y✝ : ℕ
xs✝ : List ℕ
a✝ :
  ∀ {m : ℕ},
    IsAdmissible m xs✝ ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) xs✝ ∧ ∀ (k : ℕ) (h : k < xs✝.length), xs✝[k] ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs✝) ↔
      List.IsChain (fun x1 x2 ↦ x1 < x2) (y :: xs✝) ∧ ∀ (k : ℕ) (h : k < (y :: xs✝).length), (y :: xs✝)[k] ≤ m + k
m : ℕ
⊢ x✝ < y✝ ∧
      (List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝) ∧
          ∀ (k : ℕ) (h : k < xs✝.length + 1), (y✝ :: xs✝)[k] ≤ m + 1 + k) ∧
        x✝ ≤ m ↔
    List.IsChain (fun x1 x2 ↦ x1 < x2) (x✝ :: y✝ :: xs✝) ∧
      ∀ (k : ℕ) (h : k < xs✝.length + 1 + 1), (x✝ :: y✝ :: xs✝)[k] ≤ m + k