mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯)
      (𝟙 (homEquiv h) ≫ Hom.base κ ≫ 𝟙 (homEquiv h')) ≍
    CatEnriched.hComp (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
← CatEnriched.hComp_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ CatEnriched.hComp (eqToHom ⋯) (𝟙 (homEquiv h)) ≫
      CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ ≫ 𝟙 (homEquiv h')) ≍
    CatEnriched.hComp (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ eqToHom ⋯ ≫
      CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ ≫ 𝟙 (homEquiv h')) ≍
    CatEnriched.hComp (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
← CatEnriched.hComp_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ eqToHom ⋯ ≫
      CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫
        CatEnriched.hComp (eqToHom ⋯) (𝟙 (homEquiv h')) ≍
    CatEnriched.hComp (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯ ≍
    CatEnriched.hComp (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
← CatEnriched.hComp_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯ ≍
    CatEnriched.hComp (𝟙 (homEquiv f)) (eqToHom ⋯) ≫
      CatEnriched.hComp (Hom.base η ≫ 𝟙 (homEquiv f')) (CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯ ≍
    eqToHom ⋯ ≫
      CatEnriched.hComp (Hom.base η ≫ 𝟙 (homEquiv f')) (CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
← CatEnriched.hComp_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯ ≍
    eqToHom ⋯ ≫
      CatEnriched.hComp (Hom.base η) (CatEnriched.hComp (Hom.base θ) (Hom.base κ)) ≫
        CatEnriched.hComp (𝟙 (homEquiv f')) (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : MorphismProperty (FreeRefl V)
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V} (e : x ⟶ y), W (homMk e)
X Y : FreeRefl V
h : (x : V) × (y : V) × (x ⟶ y)
⊢ W (homMk h.snd.snd)

Tactic:
apply hW

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

Goal state before:
pp: V : Truncated 2
motive : V.HomotopyCategory → Prop
h : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), motive (mk x)
x : V.HomotopyCategory
⊢ motive x

Tactic:
by
  obtain ⟨x', rfl⟩ := mk_surjective x
  exact h x'

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

Goal state before:
pp: x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ IsSplitEpi (toSimplexCategory.map e)

Tactic:
constructor
  constructor
  apply SplitEpi.map
  exact isSplitEpi_P_σ he |>.exists_splitEpi.some

Goal state after:
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 < 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

Tactic:
and_assoc,

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
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 < xs✝.length + 1), (y✝ :: xs✝)[k] ≤ m + 1 + k) ∧ x✝ ≤ m ↔
    (x✝ < y✝ ∧ List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝)) ∧
      ∀ (k : ℕ) (h : k < xs✝.length + 1 + 1), (x✝ :: y✝ :: xs✝)[k] ≤ m + k

Tactic:
and_assoc,

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 ↔
    x✝ < y✝ ∧
      List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝) ∧
        ∀ (k : ℕ) (h : k < xs✝.length + 1 + 1), (x✝ :: y✝ :: xs✝)[k] ≤ m + k
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (Functor.curry.obj (inverse X Y ⋙ functor X Y)).map (homMk e) ≫
      (mkNatIso (fun y ↦ Iso.refl (((Functor.curry.obj (inverse X Y ⋙ functor X Y)).obj (mk x₁)).obj (mk y))) ⋯).hom =
    (mkNatIso (fun y ↦ Iso.refl (((Functor.curry.obj (inverse X Y ⋙ functor X Y)).obj (mk x₀)).obj (mk y))) ⋯).hom ≫
      (Functor.curry.obj (𝟭 (X.HomotopyCategory × Y.HomotopyCategory))).map (homMk e)

Tactic:
by
        ext y : 2
        obtain ⟨y, rfl⟩ := y.mk_surjective
        cat_disch

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
⊢ (fun j ↦ if j.castSucc < i then 0 else 1) j₁ ≤ (fun j ↦ if j.castSucc < i then 0 else 1) j₂

Tactic:
dsimp
        split_ifs <;> grind

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case refine_1
α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsLowerSet s
a : α
x : a ∈ Subtype.val '' s
⊢ P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ Subtype.val '' s

Tactic:
obtain ⟨a, ma, rfl⟩ := x
    exact ⟨a.2, fun b x y ↦ by simpa [h (show ⟨b, y⟩ ≤ a by exact x) ma]⟩

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

Goal state before:
pp: case hₐ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin i
⊢ ((sx.spineEquiv i)
          ((ConcreteCategory.hom (X.map (op f)))
            (sx.spineToSimplex
              { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
                arrow := fun i ↦
                  (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
                arrow_src := ⋯, arrow_tgt := ⋯ }))).arrow
      k =
    ((sx.spineEquiv i) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))) x)).arrow k

Tactic:
· dsimp only [spineEquiv, Equiv.coe_fn_mk, spine_arrow]
      rw [← Functor.map_comp_apply]
      let α : strArrowMk₂ f ⟶ strArrowMk₂ (mkOfSucc k ≫ f) :=
        StructuredArrow.homMk (Hom.tr (mkOfSucc k)).op (by simp)
      exact (isPointwiseRightKanExtensionAt.fac_aux₃ _ _ _ _).trans
        (ConcreteCategory.congr_hom (s.w α).symm x)

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : Y.Nonsingular
n : ℕ
⊢ ∀ (x : ↑(X.nonDegenerate n)), Mono (yonedaEquiv.symm ↑x)

Tactic:
⟨x, hx⟩

Goal state after:
X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx⟩)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
⊢ ∀ (x : ↑((nerve T).nonDegenerate n)), Mono (yonedaEquiv.symm ↑x)

Tactic:
⟨x, hx⟩

Goal state after:
X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx : x ∈ (nerve T).nonDegenerate n
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx⟩)
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 ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
g : unop (op ⦋(↑c.s).dim⦌) ⟶ ⦋c.dim + 1⦌
h₁ : stdSimplex.objEquiv.symm g ∈ c.horn.obj (op ⦋(↑c.s).dim⦌)
h₂ : (ConcreteCategory.hom (X.map g.op)) ((↑(P.p c.s)).cast ⋯).simplex = (↑c.s).simplex
⊢ False

Tactic:
have := mono_of_nonDegenerate (x := ⟨_, c.s.val.nonDegenerate⟩) _ _ _ h₂

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
g : unop (op ⦋(↑c.s).dim⦌) ⟶ ⦋c.dim + 1⦌
h₁ : stdSimplex.objEquiv.symm g ∈ c.horn.obj (op ⦋(↑c.s).dim⦌)
h₂ : (ConcreteCategory.hom (X.map g.op)) ((↑(P.p c.s)).cast ⋯).simplex = (↑c.s).simplex
this : Mono g
⊢ False
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.colimitsOfShape J X
X Y : C
i : X ⟶ Y
x✝ : Mono i
hi : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
J : Type w
w✝ : Category.{w', w} J
p : P.ColimitOfShape J Y
φ : (j : J) → p.diag.obj j ⟶ X
hφ : ∀ (j : J), φ j ≫ i = p.ι.app j
c : Cocone p.diag := { pt := X, ι := { app := φ, naturality := ⋯ } }
j : J
⊢ p.ι.app j ≫ p.isColimit.desc c ≫ i = p.ι.app j ≫ 𝟙 Y

Tactic:
p.isColimit.fac_assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.colimitsOfShape J X
X Y : C
i : X ⟶ Y
x✝ : Mono i
hi : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
J : Type w
w✝ : Category.{w', w} J
p : P.ColimitOfShape J Y
φ : (j : J) → p.diag.obj j ⟶ X
hφ : ∀ (j : J), φ j ≫ i = p.ι.app j
c : Cocone p.diag := { pt := X, ι := { app := φ, naturality := ⋯ } }
j : J
⊢ c.ι.app j ≫ i = p.ι.app j ≫ 𝟙 Y
Module: Mathlib.CategoryTheory.Presentable.LocallyPresentable

Goal state before:
pp: C : Type u
hC : Category.{v, u} C
inst✝ : IsAccessibleCategory.{w, v, u} C
X : C
κ : Cardinal.{w}
w✝ : Fact κ.IsRegular
h✝ : IsCardinalAccessibleCategory C κ
⊢ IsPresentable.{w, v, u} X

Tactic:
obtain ⟨_, _, h⟩ := HasCardinalFilteredGenerator.exists_generator C κ

Goal state after:
C : Type u
hC : Category.{v, u} C
inst✝ : IsAccessibleCategory.{w, v, u} C
X : C
κ : Cardinal.{w}
w✝² : Fact κ.IsRegular
h✝ : IsCardinalAccessibleCategory C κ
w✝¹ : ObjectProperty C
w✝ : ObjectProperty.EssentiallySmall.{w, v, u} w✝¹
h : w✝¹.IsCardinalFilteredGenerator κ
⊢ IsPresentable.{w, v, u} X
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 κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
⊢ (P.colimitsCardinalClosure κ).ι.isDenseAt X

Tactic:
have : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C :=
      hasColimitsOfShape_of_equivalence
        (equivSmallModel.{w} (CostructuredArrow (P.colimitsCardinalClosure κ).ι X)).symm

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 κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
⊢ (P.colimitsCardinalClosure κ).ι.isDenseAt X
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
⊢ ∀ ⦃X Y_1 : Cᵒᵖ⦄ (f : X ⟶ Y_1),
    (((restrictedULiftYoneda F).obj Y).map f ≫
        match Y_1 with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) }) =
      (match X with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) }) ≫
        ((restrictedULiftYoneda F).obj s.pt).map f

Tactic:
rintro ⟨X₁⟩ ⟨X₂⟩ ⟨f⟩
          ext ⟨x⟩
          let α : CostructuredArrow.mk (F.map f ≫ x) ⟶ CostructuredArrow.mk x :=
            CostructuredArrow.homMk f
          exact ULift.down_injective (s.w α).symm

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
h₁ : P.IsRegular
h₂ : P.IsInner
⊢ A.preimage (Iso.refl X).hom = range A.ι

Tactic:
by simp only [Iso.refl_hom, preimage_id, Subfunctor.range_ι]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X✝ : SSet
A : X✝.Subcomplex
P : A.Pairing
inst✝¹ : P.IsRegular
inst✝ : P.IsInner
j : ℕ
hj : ¬IsMax j
X Y : SSet
c : P.rankFunction.Cell j
h0 : 0 < ⋯.index ⋯
hn : ⋯.index ⋯ < Fin.last ((↑c.s).dim + 1)
⊢ SSet.innerAnodyneExtensions (P.rankFunction.basicCell j c)

Tactic:
have : NeZero c.dim := ⟨by grind⟩

Goal state after:
X✝ : SSet
A : X✝.Subcomplex
P : A.Pairing
inst✝¹ : P.IsRegular
inst✝ : P.IsInner
j : ℕ
hj : ¬IsMax j
X Y : SSet
c : P.rankFunction.Cell j
h0 : 0 < ⋯.index ⋯
hn : ⋯.index ⋯ < Fin.last ((↑c.s).dim + 1)
this : NeZero c.dim
⊢ SSet.innerAnodyneExtensions (P.rankFunction.basicCell j c)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin (d + 1)
⊢ φ x hd i.castSucc < φ x hd i.succ

Tactic:
obtain hi | rfl | hi := lt_trichotomy i (min x hd)

Goal state after:
case inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin (d + 1)
hi : i < min x hd
⊢ φ x hd i.castSucc < φ x hd i.succ

case inr.inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
⊢ φ x hd (min x hd).castSucc < φ x hd (min x hd).succ

case inr.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin (d + 1)
hi : min x hd < i
⊢ φ x hd i.castSucc < φ x hd i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
⊢ (fun j ↦ if j.castSucc < i then 0 else 1) j₁ ≤ (fun j ↦ if j.castSucc < i then 0 else 1) j₂

Tactic:
dsimp
        split_ifs <;> grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inr.left
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
⊢ Ss.card = Sδ.card

Tactic:
suffices Ss = Finset.image is.castSucc.succAbove Sδ by
          rw [this]
          exact Finset.card_image_of_injective _ Fin.succAbove_right_injective
        ext i
        obtain rfl | ⟨i, rfl⟩ := is.castSucc.eq_self_or_eq_succAbove i
        · have : is.castSucc ∉ Ss := fun h ↦ by
            have : s.1 is.castSucc ≤ k.castSucc := by
              simpa using (hs.simplex_fst_le_castSucc_iff is.castSucc).2 (by simp)
            simp_all [Ss]
          simpa
        · simp [hSs]

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

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
⊢ (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j.castSucc)) ≫
      δ Y i.succ =
    δ X i ≫
      ↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j)

Tactic:
ext x
    simp only [TypeCat.Fun.toFun_apply, types_comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      ← SSet.δ_naturality_apply]
    dsimp
    apply congr_arg
    ext k : 2
    · simp [SimplexCategory.δ_comp_σ_of_gt hij, SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}]
      rfl
    · rw [stdSimplex.δ_objMk₁_of_le _ _ (by simpa using! Fin.le_of_lt hij)]
      rfl

Goal state after:
Module: Mathlib.Order.NonemptyFiniteChains

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : Y
ha✝ : a ∈ Finset.image (⇑f) s.finset
b : Y
hb✝ : b ∈ Finset.image (⇑f) s.finset
ha : ∃ a_1 ∈ s.finset, f a_1 = a
hb : ∃ a ∈ s.finset, f a = b
⊢ ⟨a, ha✝⟩ ≤ ⟨b, hb✝⟩ ∨ ⟨b, hb✝⟩ ≤ ⟨a, ha✝⟩

Tactic:
obtain ⟨a, ha', rfl⟩ := ha

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
b : Y
hb✝ : b ∈ Finset.image (⇑f) s.finset
hb : ∃ a ∈ s.finset, f a = b
a : X
ha' : a ∈ s.finset
ha : f a ∈ Finset.image (⇑f) s.finset
⊢ ⟨f a, ha⟩ ≤ ⟨b, hb✝⟩ ∨ ⟨b, hb✝⟩ ≤ ⟨f a, ha⟩
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1

Tactic:
let c : ℕ → R := fun n ↦ a ^ n * b
  have hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop := by
    simpa [c] using Tendsto.atTop_mul_const (by linarith) (tendsto_pow_atTop_atTop_of_one_lt ha)
  have hcⱼ (j : ι) (hj : j ≠ i) : Tendsto (fun n ↦ (v j) (c n)) atTop (𝓝 0) := by
    simpa [c] using (tendsto_pow_atTop_nhds_zero_of_lt_one ((v j).nonneg _) (haj j hj)).mul_const _
  simp_rw +instances [OrderTopology.topology_eq_generate_intervals,
    TopologicalSpace.tendsto_nhds_generateFrom_iff, mem_atTop_sets, Set.mem_preimage] at hcⱼ
  choose r₁ hr₁ using tendsto_atTop_atTop.1 hcᵢ 2
  choose rₙ hrₙ using fun j hj ↦ hcⱼ j hj (.Iio 1) (by simpa using ⟨1, .inr rfl⟩) (by simp)
  have := Fintype.ofFinite ι
  let r := Finset.univ.sup fun j ↦ if h : j = i then r₁ else rₙ j h
  refine ⟨c r, lt_of_lt_of_le (by linarith) (hr₁ r ?_), fun j hj ↦ ?_, by simpa [c, haw]⟩
  · exact Finset.le_sup_dite_pos (p := fun j ↦ j = i) (f := fun _ _ ↦ r₁) (Finset.mem_univ _) rfl
  · simpa using hrₙ j hj _ <| Finset.le_sup_dite_neg (fun j ↦ j = i) (Finset.mem_univ j) _

Goal state after: