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

Goal state before:
pp: case succ.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf : QInfty.f (n + 1) ≫ f = 0
this : (PInfty.f (n + 1) + QInfty.f (n + 1)) ≫ f = 𝟙 ((AlternatingFaceMapComplex.obj X).X (n + 1)) ≫ f
⊢ DegeneraciesVanish f

Tactic:
rw [Category.id_comp] at this

Goal state after:
case succ.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf : QInfty.f (n + 1) ≫ f = 0
this : (PInfty.f (n + 1) + QInfty.f (n + 1)) ≫ f = f
⊢ DegeneraciesVanish f
Module: Mathlib.Combinatorics.Quiver.SingleObj

Goal state before:
pp: case cons
α : Type u_1
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ pathToList (listToPath (a :: l)) = a :: l

Tactic:
| cons a l ih =>

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : ↑s) (γ : Path x x), γ.Homotopic (Path.refl x)
x : X
p : Path x x
hp : ∀ (t : ↑unitInterval), p t ∈ s
⊢ ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s

Tactic:
lift x to s using by simpa using hp 0

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : ↑s) (γ : Path x x), γ.Homotopic (Path.refl x)
x : { x // x ∈ s }
p : Path ↑x ↑x
hp : ∀ (t : ↑unitInterval), p t ∈ s
⊢ ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
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
⊢ Function.Bijective (rightHomotopyClassToHom L)

Tactic:
wlog _ : IsCofibrant Y generalizing Y

Goal state after:
case inr
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
this : ∀ (Y : C) [IsFibrant Y], IsCofibrant Y → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsCofibrant Y
⊢ Function.Bijective (rightHomotopyClassToHom L)

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
Y : C
inst✝ : IsFibrant Y
h✝ : IsCofibrant Y
⊢ Function.Bijective (rightHomotopyClassToHom L)
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: case refine_2.refine_1
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 : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj ⟶ X.obj
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 X.obj)
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 Y.obj)
⊢ F.map (f ≫ homMk g') = 𝟙 (F.obj X)

Tactic:
← F.map_id

Goal state after:
case refine_2.refine_1
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 : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj ⟶ X.obj
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 X.obj)
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 Y.obj)
⊢ F.map (f ≫ homMk g') = F.map (𝟙 X)
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: case refine_2.refine_2
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 : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj ⟶ X.obj
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 X.obj)
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 Y.obj)
⊢ F.map (homMk g' ≫ f) = 𝟙 (F.obj Y)

Tactic:
← F.map_id

Goal state after:
case refine_2.refine_2
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 : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj ⟶ X.obj
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 X.obj)
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 Y.obj)
⊢ F.map (homMk g' ≫ f) = F.map (𝟙 Y)
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
l : J.L
z : d.multispan.obj (WalkingMultispan.left l)
⊢ d.multispan.ιColimitType (WalkingMultispan.right (J.fst l))
      ((ConcreteCategory.hom (d.multispan.map (WalkingMultispan.Hom.fst l))) z) =
    d.multispan.ιColimitType (WalkingMultispan.left l) z

Tactic:
by rw [ιColimitType_map]

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

Goal state before:
pp: case succ
m n : ℕ
h : m < n + 1
i : Fin (n + 2)
q : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ stdSimplex.objEquiv.symm (q ≫ SimplexCategory.δ i) ∈ (stdSimplex.face {i}ᶜ).obj (op ⦋m⦌)

Tactic:
rw [stdSimplex.face_singleton_compl, stdSimplex.objEquiv_symm_comp,
      ← Subcomplex.ofSimplex_le_iff]

Goal state after:
case succ
m n : ℕ
h : m < n + 1
i : Fin (n + 2)
q : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ Subcomplex.ofSimplex
      ((ConcreteCategory.hom ((stdSimplex.map (SimplexCategory.δ i)).app (op ⦋m⦌))) (stdSimplex.objEquiv.symm q)) ≤
    Subcomplex.ofSimplex (stdSimplex.objEquiv.symm (SimplexCategory.δ i))
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type u''
inst✝ : Category.{v'', u''} J
⊢ (isomorphisms C).functorCategory J = isomorphisms (J ⥤ C)

Tactic:
ext _ _ f
  simp only [functorCategory, isomorphisms.iff, NatTrans.isIso_iff_isIso_app]

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

Goal state before:
pp: case mp.inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
⊢ (ConcreteCategory.hom f) x₀✝ = (ConcreteCategory.hom f) y₀✝ ∨
    ∃ x₀ y₀,
      ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
        (ConcreteCategory.hom f) x₀✝ = (ConcreteCategory.hom f) x₀ ∧
          (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) y₀

Tactic:
exact Or.inr ⟨_, _, h, rfl, rfl⟩

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

Goal state before:
pp: X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
⊢ J.rlp f

Tactic:
apply rlp_of_isIso

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

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

Tactic:
exact ConcreteCategory.congr_hom (e.hom.w WalkingSpan.left).symm x₁

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

Goal state before:
pp: X : SSet
d n : ℕ
h : d < n
⊢ ⊤ ⊆ (X.skeleton n).obj (op ⦋d⦌)

Tactic:
intro x _

Goal state after:
X : SSet
d n : ℕ
h : d < n
x : X _⦋d⦌
a✝ : x ∈ ⊤
⊢ x ∈ (X.skeleton n).obj (op ⦋d⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

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

Tactic:
ext
        exact Subtype.ext_iff.mp
          (Y.unique_nonDegenerate_simplex _ f₁ ⟨_, c₁.nonDegenerate⟩ rfl
            f₂ ⟨_, c₂.nonDegenerate⟩ h)

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

Goal state before:
pp: n : ℕ
X✝ : Truncated (n + 1)
m✝ : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin m
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj Y).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      ((ConcreteCategory.hom (σ.app (op { obj := ⦋1⦌, property := ⋯ }))) (f.arrow i)) =
    (ConcreteCategory.hom (σ.app (op { obj := ⦋0⦌, property := ⋯ }))) (f.vertex i.succ)

Tactic:
simp only [← f.arrow_tgt i]
    exact ConcreteCategory.congr_hom (σ.naturality (tr (δ 0)).op) _ |>.symm

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

Tactic:
rw [mkOfSucc_δ_gt h, spineToSimplex_arrow]

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
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
P Q R S : TransportEnrichment F C
⊢ (α_ (F.obj (P ⟶[V] Q)) (F.obj (Q ⟶[V] R)) (F.obj (R ⟶[V] S))).inv ≫
      (μ F (P ⟶[V] Q) (Q ⟶[V] R) ≫ F.map (eComp V P Q R)) ▷ F.obj (R ⟶[V] S) ≫
        μ F (P ⟶[V] R) (R ⟶[V] S) ≫ F.map (eComp V P R S) =
    F.obj (P ⟶[V] Q) ◁ (μ F (Q ⟶[V] R) (R ⟶[V] S) ≫ F.map (eComp V Q R S)) ≫
      μ F (P ⟶[V] Q) (Q ⟶[V] S) ≫ F.map (eComp V P Q S)

Tactic:
by
    rw [comp_whiskerRight, Category.assoc, μ_natural_left_assoc,
      ← associativity_inv_assoc, ← F.map_comp, ← F.map_comp, e_assoc,
      F.map_comp, MonoidalCategory.whiskerLeft_comp, Category.assoc,
      Functor.LaxMonoidal.μ_natural_right_assoc]

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
hf : W₂ f
h : r.deg X = r.deg Y
⊢ MorphismProperty.identities C f

Tactic:
by_contra
  exact h.not_lt (r.lt₂ _ hf this)

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 (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
this : generators.multiplicativeClosure' ≤ P
⊢ P f

Tactic:
rw [← MorphismProperty.multiplicativeClosure_eq_multiplicativeClosure',
      multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this

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
this : P = ⊤
⊢ P f
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₀ y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge y₀ y₁
z : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) =
    (inverse X (Y ⊗ Z)).map (Prod.mkHom (𝟙 (mk x)) (homMk (e.tensor (Edge.id z))))

Tactic:
inverse_map_mkHom_id_homMk

Goal state after:
X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₀ y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge y₀ y₁
z : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) = homMk ((Edge.id x).tensor (e.tensor (Edge.id z)))
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
hk' : ¬j.castSucc < k
⊢ (j.predAbove k).castSucc < i

Tactic:
· simp only [not_lt] at hk'
      rw [Fin.predAbove_of_le_castSucc _ _ hk']
      exact lt_of_le_of_lt (by simpa) h

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₂ : inr (WithInitial.of x) (WithInitial.of y) ≫ f = inr (WithInitial.of x) (WithInitial.of y) ≫ g
h₁ : inl' x y ≫ f = inl' x y ≫ g
⊢ f = g

Tactic:
change inr' _ _ ≫ f = inr' _ _ ≫ g at h₂

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
⊢ f = g
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
hy : Acc P.AncestralRel y
x : ↑P.II
r : P.AncestralRel x y
⊢ P.rank' ⋯ < P.rank' hy

Tactic:
rw [P.rank'_eq hy, ← Nat.add_one_le_iff]
  exact le_csSup (Finite.bddAbove_range _) ⟨⟨x, r⟩, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.ExtremalEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : ExtremalEpi f
A : Subobject Y
hA : A.Factors f
⊢ IsIso A.arrow

Tactic:
exact isIso f (Subobject.factorThru A f hA) _ (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝¹ : P.IsStrongGenerator
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X : C⦄ (A : Subobject X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤
X Y : C
i : X ⟶ Y
x✝ : Mono i
h : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
⊢ IsIso i

Tactic:
Subobject.isIso_iff_mk_eq_top

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝¹ : P.IsStrongGenerator
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X : C⦄ (A : Subobject X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤
X Y : C
i : X ⟶ Y
x✝ : Mono i
h : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
⊢ Subobject.mk i = ⊤
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: case right
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
X Y : C
f : (𝟭 C).obj X ⟶ (𝟭 C).obj Y
⊢ ∃ a, h.functor.mapArrow.obj a = { left := X, right := Y, hom := f }

Tactic:
obtain ⟨x, rfl⟩ := h.objEquiv.surjective X

Goal state after:
case right
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
Y : C
x : ↑h.obj
f : (𝟭 C).obj (h.objEquiv x) ⟶ (𝟭 C).obj Y
⊢ ∃ a, h.functor.mapArrow.obj a = { left := h.objEquiv x, right := Y, hom := f }
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
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
⊢ IsLimit (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.mapCone (PullbackCone.mk (f.t j) (f.m j) ⋯))

Tactic:
by
    refine (isLimitMapConePullbackConeEquiv _ _).symm
      (IsPullback.isLimit ?_)
    rw [Types.isPullback_iff]
    dsimp
    refine ⟨congr_app (f.w j) (op ⦋d⦌),
      fun a₁ a₂ h ↦ (mono_iff_injective _).mp
        ((NatTrans.mono_iff_mono_app (f.m j)).mp inferInstance _) h.2, fun y b h ↦ ?_⟩
    obtain ⟨x, b, rfl⟩ := f.ιSigmaStdSimplex_jointly_surjective b
    have hb : b ∈ Λ[_, x.index].obj _ := by
      obtain ⟨y, hy⟩ := y
      simp only [← x.preimage_filtration_map]
      rw [Subtype.ext_iff] at h
      dsimp at h
      subst h
      rwa [x.ι_b_app_apply] at hy
    refine ⟨x.ιSigmaHorn.app _ ⟨b, hb⟩, ?_, ?_⟩
    · simpa only [Subfunctor.toFunctor_obj, Subtype.ext_iff,
        x.ι_b_app_apply, x.ι_t_app_apply] using! h.symm
    · rw [← NatTrans.comp_app_apply]
      simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
A : Type u'
inst✝⁴ : Category.{v', u'} A
inst✝³ : HasColimitsOfSize.{w, w, v', u'} A
inst✝² : HasCoproducts A
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
X : C
M : A
inst✝ : IsCardinalPresentable M κ
⊢ IsCardinalPresentable (freeYoneda X M) κ

Tactic:
let e : coyoneda.obj (op (freeYoneda X M)) ≅
      (evaluation Cᵒᵖ A).obj (op X) ⋙ coyoneda.obj (op M) ⋙ uliftFunctor.{u} :=
    NatIso.ofComponents (fun P ↦ Equiv.toIso (freeYonedaHomEquiv.trans Equiv.ulift.symm))

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
A : Type u'
inst✝⁴ : Category.{v', u'} A
inst✝³ : HasColimitsOfSize.{w, w, v', u'} A
inst✝² : HasCoproducts A
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
X : C
M : A
inst✝ : IsCardinalPresentable M κ
e : coyoneda.obj (op (freeYoneda X M)) ≅ (evaluation Cᵒᵖ A).obj (op X) ⋙ coyoneda.obj (op M) ⋙ uliftFunctor.{u, v'} :=
  NatIso.ofComponents (fun P ↦ (freeYonedaHomEquiv.trans Equiv.ulift.symm).toIso) ⋯
⊢ IsCardinalPresentable (freeYoneda X M) κ
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
⊢ isCardinalPresentable C κ X ≤ P.colimitsCardinalClosure κ X

Tactic:
hX

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : isCardinalPresentable C κ X
⊢ P.colimitsCardinalClosure κ X
Module: Mathlib.CategoryTheory.Adjunction.ParametrizedLimits

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
J : Type u_4
inst✝¹ : Category.{v_4, u_4} J
P : J ⥤ C₁ᵒᵖ
inst✝ : ∀ (X₂ : C₂), PreservesColimit P.leftOp (F.flip.obj X₂)
X₃ : C₃
c : Cone P
hc : IsLimit c
cocone : (s : Cone (P ⋙ G.flip.obj X₃)) → Cocone (P.leftOp ⋙ F.flip.obj s.pt) :=
  fun s ↦ { pt := X₃, ι := { app := fun j ↦ adj₂.homEquiv.symm (s.π.app (unop j)), naturality := ⋯ } }
hc' : (s : Cone (P ⋙ G.flip.obj X₃)) → IsColimit ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)) :=
  fun s ↦ isColimitOfPreserves (F.flip.obj s.pt) (isColimitCoconeLeftOpOfCone P hc)
s : Cone (P ⋙ G.flip.obj X₃)
m : s.pt ⟶ ((G.flip.obj X₃).mapCone c).pt
hm : ∀ (j : J), m ≫ ((G.flip.obj X₃).mapCone c).π.app j = s.π.app j
j : Jᵒᵖ
⊢ ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)).ι.app j ≫ adj₂.homEquiv.symm m = (cocone s).ι.app j

Tactic:
simp [cocone, ← hm,
          dsimp% adj₂.homEquiv_symm_naturality_one (c.π.app j.unop).unop]

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

Goal state before:
pp: X : SSet
⊢ X.IsConnected ↔ Nonempty (Unique X.π₀)

Tactic:
rw [isConnected_iff, unique_iff_subsingleton_and_nonempty, π₀.nonempty_iff]

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

Goal state before:
pp: X : SSet
s : Cocone X.functorN
x : X.N
⊢ x.subcomplex.ι ≫ desc s = s.ι.app x

Tactic:
have : x.subcomplex.ι ≫ (Subcomplex.topIso X).inv =
    ((multicoequalizerDiagram X).multicofork.map Subcomplex.toSSetFunctor).π x := rfl
  rw [reassoc_of% this]
  apply Multicofork.IsColimit.fac

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: case succ
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : j.castSucc < i.succ.castSucc
⊢ stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x

Tactic:
rw [stdSimplex.δ_comp_σ_of_le_assoc (by grind), δ_map, comp_const]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.castSucc.castSucc.rev ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.succ.succ ≫ h.map)))

Tactic:
Fin.rev_castSucc,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.castSucc.rev.succ ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.succ.succ ≫ h.map)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.castSucc.rev.succ ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.succ.succ ≫ h.map)))

Tactic:
Fin.rev_castSucc,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.rev.succ.succ ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.succ.succ ≫ h.map)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.castSucc.rev.castSucc ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.castSucc.succ ≫ h.map)))

Tactic:
Fin.rev_castSucc,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.rev.succ.castSucc ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.castSucc.succ ≫ h.map)))
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Field R
inst✝⁴ : Semifield S
inst✝³ : LinearOrder S
v w : AbsoluteValue R S
inst✝² : IsStrictOrderedRing S
inst✝¹ : Archimedean S
inst✝ : ExistsAddOfLE S
hv✝ : v.IsNontrivial
h : ∀ (x : R), v x < 1 → w x < 1
a : R
ha₀ : a ≠ 0
hw : w a < 1
x₀ : R
hx₀ : x₀ ≠ 0 ∧ v x₀ < 1
n : ℕ
hv : 1 ≤ v a
⊢ v x₀ * (v (a ^ n))⁻¹ < 1

Tactic:
map_pow,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : Field R
inst✝⁴ : Semifield S
inst✝³ : LinearOrder S
v w : AbsoluteValue R S
inst✝² : IsStrictOrderedRing S
inst✝¹ : Archimedean S
inst✝ : ExistsAddOfLE S
hv✝ : v.IsNontrivial
h : ∀ (x : R), v x < 1 → w x < 1
a : R
ha₀ : a ≠ 0
hw : w a < 1
x₀ : R
hx₀ : x₀ ≠ 0 ∧ v x₀ < 1
n : ℕ
hv : 1 ≤ v a
⊢ v x₀ * (v a ^ n)⁻¹ < 1