mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
V : C
g : unop (op V) ⟶ U
this :
  Presheaf.imageSieve f
      ((ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj U).map g.op)) (shrinkYonedaObjObjEquiv.symm (𝟙 U))) ∈
    J (unop (op V))
hg :
  (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj (unop (op U))).map g.op))
      (shrinkYonedaObjObjEquiv.symm (𝟙 (unop (op U)))) =
    shrinkYonedaObjObjEquiv.symm (g.op.unop ≫ 𝟙 (unop (op U)))
⊢ Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm g) ∈ J V

Tactic:
simp only [Quiver.Hom.unop_op, Category.comp_id] at hg

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
V : C
g : unop (op V) ⟶ U
this :
  Presheaf.imageSieve f
      ((ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj U).map g.op)) (shrinkYonedaObjObjEquiv.symm (𝟙 U))) ∈
    J (unop (op V))
hg :
  (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj U).map g.op)) (shrinkYonedaObjObjEquiv.symm (𝟙 U)) =
    shrinkYonedaObjObjEquiv.symm g
⊢ Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm g) ∈ J V
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
q : ℕ
hq : (alternatingFaceMapComplex C).map f ≫ P q = P q ≫ (alternatingFaceMapComplex C).map f
⊢ (alternatingFaceMapComplex C).map f ≫ P (q + 1) = P (q + 1) ≫ (alternatingFaceMapComplex C).map f

Tactic:
simp only [P_succ, add_comp, comp_add, assoc, comp_id, hq, reassoc_of% hq]

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
q : ℕ
hq : (alternatingFaceMapComplex C).map f ≫ P q = P q ≫ (alternatingFaceMapComplex C).map f
⊢ P q ≫ (alternatingFaceMapComplex C).map f + P q ≫ (alternatingFaceMapComplex C).map f ≫ Hσ q =
    P q ≫ (alternatingFaceMapComplex C).map f + P q ≫ Hσ q ≫ (alternatingFaceMapComplex C).map f
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
⊢ (if x✝¹ + x✝ = 0 then 0 else exp (-(x✝¹ + x✝).valuation)) ≤
    max (if x✝¹ = 0 then 0 else exp (-x✝¹.valuation)) (if x✝ = 0 then 0 else exp (-x✝.valuation))

Tactic:
by
    split_ifs
    any_goals simp_all [inv_le_inv₀]
    simpa using le_valuation_add ‹_›

Goal state after:
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
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : Isδ₀ i'
⊢ K.d Δ.len Δ'.len ≫ mapMono K i' = 0

Tactic:
mapMono_δ₀' K i' h₄,

Goal state after:
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
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : Isδ₀ i'
⊢ K.d Δ.len Δ'.len ≫ K.d Δ'.len Δ''.len = 0
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
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ (AlgebraicTopology.inclusionOfMooreComplexMap X).f (n + 1) ≫ X.δ j.succ = 0

Tactic:
by
  dsimp [AlgebraicTopology.inclusionOfMooreComplexMap, NormalizedMooreComplex.objX]
  rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ j
    (by simp)), assoc, kernelSubobject_arrow_comp, 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 Δ
⊢ A.e ≫ 𝟙 (unop A.fst) = (𝟙 Δ).unop ≫ A.e

Tactic:
rw [unop_id, comp_id, id_comp]

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
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = (s.cofan (op ⦋n⦌)).inj A ≫ 0

Tactic:
dsimp only [SimplicialObject.σ]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ X.map (SimplexCategory.σ i).op ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) =
    (s.cofan (op ⦋n⦌)).inj A ≫ 0
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ A.epiComp (SimplexCategory.σ i).op ≠ IndexSet.id (op ⦋n + 1⦌)

Tactic:
change ¬(A.epiComp (SimplexCategory.σ i).op).EqId

Goal state after:
case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ ¬(A.epiComp (SimplexCategory.σ i).op).EqId
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
i : ⦋m⦌ ⟶ ⦋m + k + 1 + 1⦌
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
h : Epi i
⊢ False

Tactic:
grind [→ le_of_epi]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : ⦋m⦌ ⟶ ⦋m + k + 1⦌
h : Epi i
⊢ False

Tactic:
grind [→ le_of_epi]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
this : IsIso (F.map f)
⊢ IsIso f

Tactic:
exact isIso_of_reflects_iso f F

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x t : ↑I
ht : t ∈ {0, 1}
⊢ {
        toFun := fun x_1 ↦
          if ↑(x, x_1).2 ≤ 1 / 2 then (F.eval (x, x_1).1).extend (2 * ↑(x, x_1).2)
          else (G.eval (x, x_1).1).extend (2 * ↑(x, x_1).2 - 1),
        continuous_toFun := ⋯ }
      t =
    (p₀.trans p₁).toContinuousMap t

Tactic:
rcases ht with ht | ht
    · norm_num [ht]
    · rw [Set.mem_singleton_iff] at ht
      norm_num [ht]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : ↑I
hx : x ∈ {0, 1}
⊢ { toFun := fun x ↦ p ⟨↑(σ (t, x).1) * ↑(t, x).2 + ↑(t, x).1 * ↑(f (t, x).2), ⋯⟩, continuous_toFun := ⋯ } x =
    p.toContinuousMap x

Tactic:
rcases hx with hx | hx
    · rw [hx]
      simp [hf₀]
    · rw [Set.mem_singleton_iff] at hx
      rw [hx]
      simp [hf₁]

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

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
a✝¹ a✝ : Y
⊢ (∀ (p₁ p₂ : Path a✝¹ a✝), p₁.Homotopic p₂) ↔ Subsingleton (Path.Homotopic.Quotient a✝¹ a✝)

Tactic:
simp [Path.Homotopic.Quotient, Setoid.eq_top_iff]

Goal state after:
Y : Type u_2
inst✝ : TopologicalSpace Y
a✝¹ a✝ : Y
⊢ (∀ (p₁ p₂ : Path a✝¹ a✝), p₁.Homotopic p₂) ↔ ∀ (x y : Path a✝¹ a✝), (Path.Homotopic.setoid a✝¹ a✝) x y
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₀ x₃
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ x₁ = x₃

Tactic:
convert! hp 1 <;> simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
h : L.map f = L.map g
⊢ RightHomotopyRel f g

Tactic:
← RightHomotopyClass.mk_eq_mk_iff

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
h : L.map f = L.map g
⊢ RightHomotopyClass.mk f = RightHomotopyClass.mk g
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
⊢ Function.LeftInverse (Quot.lift (fun f ↦ RightHomotopyClass.mk f.hom) ⋯) (Quot.lift (fun f ↦ toHoCat.map (homMk f)) ⋯)

Tactic:
rintro ⟨f⟩; rfl

Goal state after:
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
⊢ Function.RightInverse (Quot.lift (fun f ↦ RightHomotopyClass.mk f.hom) ⋯)
    (Quot.lift (fun f ↦ toHoCat.map (homMk f)) ⋯)

Tactic:
rintro ⟨f⟩; rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
Y : BifibrantObject C
f g : X.bifibrantResolutionObj ⟶ Y
h :
  RightHomotopyRel (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map f).hom
    (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map g).hom
⊢ BifibrantObject.toHoCat.map f = BifibrantObject.toHoCat.map g

Tactic:
← RightHomotopyClass.mk_eq_mk_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
Y : BifibrantObject C
f g : X.bifibrantResolutionObj ⟶ Y
h :
  RightHomotopyClass.mk (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map f).hom =
    RightHomotopyClass.mk (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map g).hom
⊢ BifibrantObject.toHoCat.map f = BifibrantObject.toHoCat.map g
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
Y : BifibrantObject C
f g : X.bifibrantResolutionObj ⟶ Y
h :
  RightHomotopyClass.mk (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map f).hom =
    RightHomotopyClass.mk (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map g).hom
⊢ RightHomotopyRel f.hom g.hom

Tactic:
← RightHomotopyClass.mk_eq_mk_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
Y : BifibrantObject C
f g : X.bifibrantResolutionObj ⟶ Y
h :
  RightHomotopyClass.mk (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map f).hom =
    RightHomotopyClass.mk (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map g).hom
⊢ RightHomotopyClass.mk f.hom = RightHomotopyClass.mk g.hom
Module: Mathlib.AlgebraicTopology.ModelCategory.Transport

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
⊢ ModelCategory C

Tactic:
have h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor := by
    simp [trivialFibrations, h₂, h₃]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
⊢ ModelCategory C
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_2
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
⊢ A ≤ Λ[n + 1, i]

Tactic:
Subcomplex.le_iff_contains_nonDegenerate

Goal state after:
case refine_2
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
⊢ ∀ (n_1 : ℕ) (x : ↑(Δ[n + 1].nonDegenerate n_1)), ↑x ∈ A.obj (op ⦋n_1⦌) → ↑x ∈ Λ[n + 1, i].obj (op ⦋n_1⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: case refine_2
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : A.toSSet.HasDimensionLT n
⊢ A ≤ ∂Δ[n]

Tactic:
Subcomplex.le_iff_contains_nonDegenerate

Goal state after:
case refine_2
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : A.toSSet.HasDimensionLT n
⊢ ∀ (n_1 : ℕ) (x : ↑(Δ[n].nonDegenerate n_1)), ↑x ∈ A.obj (op ⦋n_1⦌) → ↑x ∈ ∂Δ[n].obj (op ⦋n_1⦌)
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} = Set.univ

Tactic:
by ext (_ | _) <;> tauto

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ yonedaEquiv (ι i j hij) = face i j hij

Tactic:
ι,

Goal state after:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ yonedaEquiv (yonedaEquiv.symm (face i j hij)) = face i j hij
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ ι i j hij ≫ Λ[n + 1, i].ι = stdSimplex.δ j

Tactic:
ι,

Goal state after:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ yonedaEquiv.symm (face i j hij) ≫ Λ[n + 1, i].ι = stdSimplex.δ j
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ yonedaEquiv.symm (face i j hij) ≫ Λ[n + 1, i].ι = stdSimplex.δ j

Tactic:
face,

Goal state after:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ yonedaEquiv.symm (yonedaEquiv (Subfunctor.lift (stdSimplex.δ j) ⋯)) ≫ Λ[n + 1, i].ι = stdSimplex.δ j
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: 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:
constructor
  · apply pushoutCocone_inl_eq_inr_imp_of_iso e
  · apply pushoutCocone_inl_eq_inr_imp_of_iso e.symm

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

Goal state before:
pp: X : SSet
i j : ℕ
h : i ≤ j
⊢ (fun n ↦ ⨆ i, ⨆ x, Subcomplex.ofSimplex ↑x) i ≤ (fun n ↦ ⨆ i, ⨆ x, Subcomplex.ofSimplex ↑x) j

Tactic:
by
    simp only [iSup_le_iff]
    intro k x
    exact le_trans (by exact le_trans (by rfl) (le_iSup _ x))
      (le_iSup _ ⟨k, by lia⟩)

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

Goal state before:
pp: X : SSet
⊢ ⊤ ≤ ⨆ n, X.skeleton n

Tactic:
Subcomplex.le_iff_contains_nonDegenerate

Goal state after:
X : SSet
⊢ ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ ⊤.obj (op ⦋n⦌) → ↑x ∈ (⨆ n, X.skeleton n).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case succ.e_a
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
⊢ stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk

Tactic:
rw [← cancel_mono (Subcomplex.ι _), Category.assoc, Category.assoc, ι_ι, ι_ι,
      Fin.pred_succ, Fin.castPred_castSucc, stdSimplex.δ_comp_δ (by grind)]

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

Goal state before:
pp: case refine_1
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ ∂Δ[d] ≤ ((skeletonOfMono i) d).preimage c.map

Tactic:
Subcomplex.le_iff_contains_nonDegenerate

Goal state after:
case refine_1
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ ∀ (n : ℕ) (x : ↑(Δ[d].nonDegenerate n)),
    ↑x ∈ ∂Δ[d].obj (op ⦋n⦌) → ↑x ∈ (((skeletonOfMono i) d).preimage c.map).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : i.succ.castSucc < j
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i.castSucc) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f) = f.arrow i.castSucc

Tactic:
spineToSimplex_arrow

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : i.succ.castSucc < j
⊢ f.arrow i.castSucc = f.arrow i.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i.succ) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f) = f.arrow i.succ

Tactic:
spineToSimplex_arrow

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
⊢ f.arrow i.succ = f.arrow i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case zero
X : SSet
x : X _⦋0 + 1⦌
⊢ X.spine 0 ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) = (X.spine (0 + 1) x).interval 1 0 ⋯

pp: case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
⊢ X.spine (m + 1) ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) = (X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯

Tactic:
· ext
    simp [spine, Path.vertex, Truncated.Path.vertex,
      Truncated.spine, Path.interval, Truncated.Path.interval,
      Truncated.Hom.tr, ← SimplexCategory.δ_zero_eq_const]
    rfl

Goal state after:
case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
⊢ X.spine (m + 1) ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) = (X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯
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
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i.castSucc).op)) (sx.spineToSimplex f) = f.arrow i.castSucc

Tactic:
spineToSimplex_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
⊢ f.arrow i.castSucc = 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
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i.succ).op)) (sx.spineToSimplex f) = f.arrow i.succ

Tactic:
spineToSimplex_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
⊢ f.arrow i.succ = f.arrow i.succ
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
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (λ_ (𝟙_ V)).inv ≫
        (X ⟶[V] Y) ◁ ((eHomEquiv V) g ⊗ₘ (eHomEquiv V) g') ≫ (X ⟶[V] Y) ◁ eComp V Y Y' Y'' ≫ eComp V X Y Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''

Tactic:
← e_assoc,

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
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (λ_ (𝟙_ V)).inv ≫
        (X ⟶[V] Y) ◁ ((eHomEquiv V) g ⊗ₘ (eHomEquiv V) g') ≫
          (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (Y' ⟶[V] Y'')).inv ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''
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
X X' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ (ρ_ (X' ⟶[V] Y)).inv ≫
      (X' ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        (λ_ ((X' ⟶[V] Y) ⊗ Y ⟶[V] Y')).inv ≫
          (eHomEquiv V) f ▷ ((X' ⟶[V] Y) ⊗ Y ⟶[V] Y') ≫ (X ⟶[V] X') ◁ eComp V X' Y Y' ≫ eComp V X X' Y' =
    (λ_ (X' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫
        eComp V X X' Y ≫ (ρ_ (X ⟶[V] Y)).inv ≫ (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫ eComp V X Y Y'

Tactic:
← e_assoc,

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
X X' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ (ρ_ (X' ⟶[V] Y)).inv ≫
      (X' ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        (λ_ ((X' ⟶[V] Y) ⊗ Y ⟶[V] Y')).inv ≫
          (eHomEquiv V) f ▷ ((X' ⟶[V] Y) ⊗ Y ⟶[V] Y') ≫
            (α_ (X ⟶[V] X') (X' ⟶[V] Y) (Y ⟶[V] Y')).inv ≫ (eComp V X X' Y ▷ Y ⟶[V] Y') ≫ eComp V X Y Y' =
    (λ_ (X' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫
        eComp V X X' Y ≫ (ρ_ (X ⟶[V] Y)).inv ≫ (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫ eComp V X Y Y'