mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
⊢ ((p.trans q).trans r) x =
    ((p.trans (q.trans r)).reparam (fun t ↦ ⟨transAssocReparamAux t, ⋯⟩) trans_assoc_reparam._proof_1 ⋯ ⋯) x

Tactic:
simp only [transAssocReparamAux, Path.trans_apply, Function.comp_apply, Path.coe_reparam]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
⊢ (if h : ↑x ≤ 1 / 2 then if h_1 : 2 * ↑x ≤ 1 / 2 then p ⟨2 * (2 * ↑x), ⋯⟩ else q ⟨2 * (2 * ↑x) - 1, ⋯⟩
    else r ⟨2 * ↑x - 1, ⋯⟩) =
    if h : (if ↑x ≤ 1 / 4 then 2 * ↑x else if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)) ≤ 1 / 2 then
      p ⟨2 * if ↑x ≤ 1 / 4 then 2 * ↑x else if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1), ⋯⟩
    else
      if h_1 : (2 * if ↑x ≤ 1 / 4 then 2 * ↑x else if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2 then
        q ⟨2 * ((2 * if ↑x ≤ 1 / 4 then 2 * ↑x else if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)) - 1), ⋯⟩
      else r ⟨2 * ((2 * if ↑x ≤ 1 / 4 then 2 * ↑x else if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)) - 1) - 1, ⋯⟩
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
L : C ⥤ H := (weakEquivalences C).Q
⊢ (localizerMorphism C).IsLocalizedEquivalence

Tactic:
let F := (localizerMorphism C).localizedFunctor Lcof L

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
F : Hcof ⥤ H := (localizerMorphism C).localizedFunctor Lcof L
⊢ (localizerMorphism C).IsLocalizedEquivalence
Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
⊢ IsConnected ((localizerMorphism C).LeftResolution X)

Tactic:
let R₀ : (localizerMorphism C).LeftResolution X :=
    { X₁ := mk (HoCat.resolutionObj X)
      w := HoCat.pResolutionObj X
      hw := by simpa using mem_weakEquivalences (HoCat.pResolutionObj X) }
  have hR₀ (R) : Nonempty (Zigzag R R₀) := by
    have sq : CommSq (initial.to _) (initial.to _) R₀.w R.w := ⟨by simp⟩
    exact ⟨Zigzag.of_hom { f := homMk (sq.lift) }⟩
  have : Nonempty ((localizerMorphism C).LeftResolution X) := ⟨R₀⟩
  exact zigzag_isConnected (fun R₁ R₂ ↦ (hR₀ R₁).some.trans (hR₀ R₂).some.symm)

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
⊢ {j}ᶜ ⊆ S ↔ S = Finset.univ ∨ S = {j}ᶜ

Tactic:
refine ⟨fun h ↦ ?_, by aesop⟩

Goal state after:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
h : {j}ᶜ ⊆ S
⊢ S = Finset.univ ∨ S = {j}ᶜ
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mpr.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
w✝¹ w✝ : S
h : (ConcreteCategory.hom g) w✝¹ = (ConcreteCategory.hom g) w✝
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) w✝¹)) (Sum.inl ((ConcreteCategory.hom f) w✝))

Tactic:
exact Rel'.inl_inl _ _ h

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

Goal state before:
pp: case inl_inl.inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inl ((ConcreteCategory.hom f) y₀✝))

Tactic:
exact Rel'.inl_inl _ _ h

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

Goal state before:
pp: case inl_inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
z₁ : X₁
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) y₀✝)) (Sum.inl z₁)
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inl z₁)

pp: case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
z₂ : X₂
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) y₀✝)) (Sum.inr z₂)
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inr z₂)

Tactic:
· rw [inl_rel'_inl_iff] at hyz
        obtain rfl | ⟨_, _, h', h'', rfl⟩ := hyz
        · exact Rel'.inl_inl _ _ h
        · obtain rfl := (mono_iff_injective f).1 inferInstance h''
          exact Rel'.inl_inl _ _ (h.trans h')

Goal state after:
case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
z₂ : X₂
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) y₀✝)) (Sum.inr z₂)
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inr z₂)
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 ≫ stdSimplex.δ j.castSucc = stdSimplex.δ j ≫ stdSimplex.δ k.succ

Tactic:
stdSimplex.δ_comp_δ (by grind)

Goal state after:
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 ≫ stdSimplex.δ j.castSucc = stdSimplex.δ k ≫ stdSimplex.δ j.castSucc
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 := ⋯ })))
      ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 0) ⋯ ⋯).op)) (f.arrow i))

Tactic:
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 + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ (X.spine n ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex f))).vertex i = f.vertex i.succ

Tactic:
by
  simp only [SimplicialObject.δ, spine_vertex]
  rw [← Functor.map_comp_apply, ← op_comp, SimplexCategory.const_comp,
    spineToSimplex_vertex]
  simp only [SimplexCategory.δ, Hom.toOrderHom, len_mk, mkHom, Hom.mk,
    OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply]
  rw [Fin.succAbove_of_le_castSucc j i h]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

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

Tactic:
simp [CatEnriched.hComp_id_heq]

Goal state after:
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 ⋯) (Hom.base κ) ≍
    CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
conv => enter [1, 2]; exact ((id_comp _).trans (comp_id _)).symm

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 ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯)
      (𝟙 (homEquiv h) ≫ Hom.base κ ≫ 𝟙 (homEquiv h')) ≍
    CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ G✝ : C ⥤ D
F G A : C ⥤ Type w
a : F ⊗ A ⟶ G
c✝ d✝ : C
φ : c✝ ⟶ d✝
y : A.obj c✝
⊢ (F.map φ ≫ ↾fun x ↦ (ConcreteCategory.hom (a.app d✝)) (x, (ConcreteCategory.hom (A.map φ)) y)) =
    (↾fun x ↦ (ConcreteCategory.hom (a.app c✝)) (x, y)) ≫ G.map φ

Tactic:
ext x
    simpa using! (a.naturality_apply φ) (x, y)

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

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : TransportEnrichment F (ForgetEnrichment V D)
⊢ (forgetEnrichmentEquivFunctor F D e h).map
        ((NatIso.ofComponents (fun x ↦ Iso.refl ((𝟭 (TransportEnrichment F (ForgetEnrichment V D))).obj x)) ⋯).hom.app
          X) ≫
      (NatIso.ofComponents
              (fun x ↦ Iso.refl ((forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h).obj x))
              ⋯).hom.app
        ((forgetEnrichmentEquivFunctor F D e h).obj X) =
    𝟙 ((forgetEnrichmentEquivFunctor F D e h).obj X)

Tactic:
by
    simp only [Functor.id_obj, forgetEnrichmentEquivFunctor_obj, Functor.comp_obj,
      forgetEnrichmentEquivInverse_obj, ForgetEnrichment.to_of, NatIso.ofComponents_hom_app,
      Iso.refl_hom, forgetEnrichmentEquivFunctor_map, h, Category.comp_id]
    rw [← ForgetEnrichment.homOf_eId, TransportEnrichment.eId_eq, ForgetEnrichment.homTo_id]
    rfl

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 : r.degHom f = r.deg Y
⊢ W₁ f

Tactic:
obtain ⟨Z, p, i, hp, hi, fac, h⟩ := r.exists_fac f
  obtain ⟨_⟩ := r.identities_of_prop₂_of_eq hi (by aesop)
  obtain rfl : p = f := by simpa using fac
  exact hp

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

Goal state before:
pp: case zero.comp_of.inl
i : Fin (0 + 1)
X Y : SimplexCategoryGenRel
k : Fin (0 + 2)
hf : faces.multiplicativeClosure (eqToHom ⋯)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (eqToHom ⋯ ≫ δ k) ≫ σ i = e ≫ m

Tactic:
simpa using factor_δ_σ i k

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

Goal state before:
pp: case succ.comp_of.inl
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
hf : faces.multiplicativeClosure (eqToHom ⋯)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (eqToHom ⋯ ≫ δ k) ≫ σ i = e ≫ m

Tactic:
simpa using factor_δ_σ i k

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

Tactic:
isAdmissible_cons_cons_iff,

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✝ ∧ IsAdmissible (m + 1) (y✝ :: xs✝) ∧ 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
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
a : SimplexCategory
ha : a.len ≤ d
b : SimplexCategory
hb : b.len ≤ d
f : { obj := a, property := ha } ⟶ { obj := b, property := hb }
⊢ W f

Tactic:
induction a using SimplexCategory.rec with | _ a

Goal state after:
case mk
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
b : SimplexCategory
hb : b.len ≤ d
a : ℕ
ha : { len := a }.len ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := b, property := hb }
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h : ofSimplex (↑c.s).simplex ≤ (↑(P.p c'.s)).subcomplex
⊢ (↑c.s).toN ≤ (↑(P.p c'.s)).toN

Tactic:
SSet.N.le_iff

Goal state after:
case refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h : ofSimplex (↑c.s).simplex ≤ (↑(P.p c'.s)).subcomplex
⊢ (↑c.s).subcomplex ≤ (↑(P.p c'.s)).subcomplex
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
inst✝² : HasCoproducts C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : ObjectProperty.Small.{w, v, u} P
hP : P.IsStrongGenerator
X : C
this✝ : HasCoproductsOfShape (CostructuredArrow P.ι X) C
this :
  IsColimit
    (Cocone.whisker (Discrete.equivalence (equivShrink (CostructuredArrow P.ι X))).symm.functor
      (Cofan.mk (∐ P.coproductFromFamily X) (Sigma.ι (P.coproductFromFamily X))))
⊢ ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, ExtremalEpi p

Tactic:
refine ⟨_, fun j ↦ ((equivShrink.{w} (CostructuredArrow P.ι X)).symm j).left.1,
    fun j ↦ ((equivShrink.{w} _).symm j).1.2, _,
    (coproductIsCoproduct (P.coproductFromFamily X)).whiskerEquivalence
    (Discrete.equivalence (equivShrink.{w} _)).symm, _, hP.extremalEpi_coproductFrom X⟩

Goal state after:
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
⊢ IsPresentable.{w, v, u} X

Tactic:
obtain ⟨κ, _, _⟩ := IsAccessibleCategory.exists_cardinal C
  obtain ⟨_, _, h⟩ := HasCardinalFilteredGenerator.exists_generator C κ
  apply h.presentable

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: case mpr
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
⊢ (∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty (Arrow.LiftStruct φ)) →
    ∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty (Arrow.LiftStruct φ)

Tactic:
· intro h α
    exact ⟨(adj₂.liftStructEquiv sq₁₂ sq₁₃ α).symm (h _).some⟩

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

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n : ℕ
s : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hds : s.dim = d + 1
is : Fin (d + 1)
hs : IsIndex s hds is.succ
t : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hdt : t.dim = d' + 1
it : Fin (d' + 1)
ht : IsIndex t hdt it.succ
⊢ (pairingCore k n).AncestralRel { x := s, d := d, hd := hds, index := is, isIndex := hs }
      { x := t, d := d', hd := hdt, index := it, isIndex := ht } →
    (pairingCore k n).dim { x := s, d := d, hd := hds, index := is, isIndex := hs } =
        (pairingCore k n).dim { x := t, d := d', hd := hdt, index := it, isIndex := ht } →
      (finset { x := s, d := d, hd := hds, index := is, isIndex := hs }.x ⋯).card <
        (finset { x := t, d := d', hd := hdt, index := it, isIndex := ht }.x ⋯).card

Tactic:
⟨h₁, h₂⟩

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n : ℕ
s : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hds : s.dim = d + 1
is : Fin (d + 1)
hs : IsIndex s hds is.succ
t : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hdt : t.dim = d' + 1
it : Fin (d' + 1)
ht : IsIndex t hdt it.succ
h₁ :
  { x := s, d := d, hd := hds, index := is, isIndex := hs } ≠ { x := t, d := d', hd := hdt, index := it, isIndex := ht }
h₂ :
  (pairingCore k n).type₂ { x := s, d := d, hd := hds, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := t, d := d', hd := hdt, index := it, isIndex := ht }
⊢ (pairingCore k n).dim { x := s, d := d, hd := hds, index := is, isIndex := hs } =
      (pairingCore k n).dim { x := t, d := d', hd := hdt, index := it, isIndex := ht } →
    (finset { x := s, d := d, hd := hds, index := is, isIndex := hs }.x ⋯).card <
      (finset { x := t, d := d', hd := hdt, index := it, isIndex := ht }.x ⋯).card
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: 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₂
i : Fin (d + 2)
hf : Mono (SimplexCategory.δ i)
hδ :
  (ConcreteCategory.hom ((Δ[m + 1] ⊗ Δ[n]).map (SimplexCategory.δ i).op))
      ((pairingCore k n).type₁
          { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }).simplex =
    ((pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }).simplex
⊢ { dim := hs.δ.dim, simplex := hs.δ.simplex } =
    { dim := d,
      simplex :=
        (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) ((Subcomplex.N.mk t ht₁ ht₂).cast ⋯).simplex }

Tactic:
by
      rw [S.ext_iff']
      exact ⟨rfl, hδ.symm⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case inst
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq : G.PullbackObjObj f₁ f₃
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj X₃)
inst✝ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj Y₃)
h : IsInitial X₁
hX₃ : IsTerminal ((G.flip.obj X₃).obj (op X₁)) := ⋯
hY₃ : IsTerminal ((G.flip.obj Y₃).obj (op X₁)) := ⋯
⊢ IsIso ((G.obj (op X₁)).map f₃)

Tactic:
exact isIso_of_isTerminal hX₃ hY₃ _

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

Goal state before:
pp: case fst
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
⊢ ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  (stdSimplex.objEquiv.symm (SimplexCategory.δ i.castSucc.succ ≫ SimplexCategory.σ i.succ))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.succ.succ)).1 =
    ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  (stdSimplex.objEquiv.symm (SimplexCategory.δ i.castSucc.succ ≫ SimplexCategory.σ i.castSucc))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.castSucc.succ)).1

Tactic:
SimplexCategory.δ_comp_σ_succ,

Goal state after:
case fst
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
⊢ ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  (stdSimplex.objEquiv.symm (SimplexCategory.δ i.castSucc.succ ≫ SimplexCategory.σ i.succ))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.succ.succ)).1 =
    ((ConcreteCategory.hom (X.map (stdSimplex.objEquiv (stdSimplex.objEquiv.symm (𝟙 ⦋n + 1⦌))).op)) x,
        (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.castSucc.succ)).1
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit

Goal state before:
pp: X : SSet
s : Cocone X.functorN
m : X.coconeN.pt ⟶ s.pt
hm : ∀ (j : X.N), X.coconeN.ι.app j ≫ m = s.ι.app j
⊢ m = desc s

Tactic:
rw [← cancel_epi (Subcomplex.topIso X).hom]

Goal state after:
X : SSet
s : Cocone X.functorN
m : X.coconeN.pt ⟶ s.pt
hm : ∀ (j : X.N), X.coconeN.ι.app j ≫ m = s.ι.app j
⊢ (Subcomplex.topIso X).hom ≫ m = (Subcomplex.topIso X).hom ≫ desc s
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ yonedaEquiv.symm ((ConcreteCategory.hom (toSSetObjI.app (op ⦋0⦌))) (const 1 0 (op ⦋0⦌))) =
    yonedaEquiv.symm (TopCat.toSSetObj₀Equiv.symm 0)

Tactic:
trans stdSimplex.δ 1 ≫ toSSetObjI

Goal state after:
⊢ yonedaEquiv.symm ((ConcreteCategory.hom (toSSetObjI.app (op ⦋0⦌))) (const 1 0 (op ⦋0⦌))) = stdSimplex.δ 1 ≫ toSSetObjI

⊢ stdSimplex.δ 1 ≫ toSSetObjI = yonedaEquiv.symm (TopCat.toSSetObj₀Equiv.symm 0)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : PartialOrder S
v w : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : Nontrivial R
h : v.IsEquiv w
x : R
⊢ v x ≤ 1 ↔ w x ≤ 1

Tactic:
simpa only [map_one] using h x 1

Goal state after: