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

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ φ ≫ X.δ j.succ + (φ ≫ (Hσ q).f (n + 1)) ≫ X.δ j.succ = 0

Tactic:
rw [v.comp_Hσ_eq (show n = a + q by lia), neg_comp, add_neg_eq_zero, assoc, assoc]

Goal state after:
case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ ≫ X.δ j.succ
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
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ mapMono K i ≫ f.f Δ.len = f.f Δ'.len ≫ mapMono K' i

Tactic:
by
  unfold mapMono
  split_ifs with h
  · subst h
    simp only [id_comp, eqToHom_refl, comp_id]
  · rw [HomologicalComplex.Hom.comm]
  · rw [zero_comp, comp_zero]

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

Goal state before:
pp: case h₂
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ ¬Isδ₀ (SimplexCategory.δ i)

Tactic:
· simpa only [Isδ₀.iff] using hi

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
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₁ : ∀ (i : ℕ), (N₁.map f ≫ inv (N₁.map f)).f.f i = (𝟙 (N₁.obj X)).f.f i
h₂ : ∀ (i : ℕ), (inv (N₁.map f) ≫ N₁.map f).f.f i = (𝟙 (N₁.obj Y)).f.f i
⊢ ∀ (n : ℕ), IsIso (f.app (op ⦋n⦌))

Tactic:
have h₃ := fun n =>
      Karoubi.HomologicalComplex.p_comm_f_assoc (inv (N₁.map f)) n (f.app (op ⦋n⦌))

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₁ : ∀ (i : ℕ), (N₁.map f ≫ inv (N₁.map f)).f.f i = (𝟙 (N₁.obj X)).f.f i
h₂ : ∀ (i : ℕ), (inv (N₁.map f) ≫ N₁.map f).f.f i = (𝟙 (N₁.obj Y)).f.f i
h₃ :
  ∀ (n : ℕ),
    (N₁.obj Y).p.f n ≫ (inv (N₁.map f)).f.f n ≫ f.app (op ⦋n⦌) =
      (inv (N₁.map f)).f.f n ≫ (N₁.obj X).p.f n ≫ f.app (op ⦋n⦌)
⊢ ∀ (n : ℕ), IsIso (f.app (op ⦋n⦌))
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n =
    ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))

Tactic:
PInfty_f

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ (P n).f n =
    ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)

Tactic:
simply_connected_iff_paths_homotopic'

Goal state after:
Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ (PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂) ↔
    PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
x✝³ x✝² : BifibrantObject C
x✝¹ x✝ : x✝³ ⟶ x✝²
h : homRel C x✝¹ x✝
⊢ (BifibrantObject.ιFibrantObject ⋙ FibrantObject.toHoCat).map x✝¹ =
    (BifibrantObject.ιFibrantObject ⋙ FibrantObject.toHoCat).map x✝

Tactic:
by
      simpa [FibrantObject.toHoCat_map_eq_iff, FibrantObject.homRel_iff_leftHomotopyRel,
        homRel_iff_leftHomotopyRel] using h

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Subcomplex.range (stdSimplex.map (SimplexCategory.δ i)) ≤ ∂Δ[n + 1]

Tactic:
simp only [Subcomplex.range_eq_ofSimplex]
    refine le_trans ?_ (face_singleton_compl_le_boundary i)
    rw [stdSimplex.face_singleton_compl, yonedaEquiv_map]

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

Goal state before:
pp: S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
j : Fin (n + 1 + 2)
hj : j ≠ i
⊢ (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j hj) =
    (ConcreteCategory.hom ((Λ[n + 2, i].ι ≫ yonedaEquiv.symm σ).app (Opposite.op ⦋n + 1⦌))) (horn.face i j hj)

Tactic:
rw [← h j hj, NatTrans.comp_app]

Goal state after:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
j : Fin (n + 1 + 2)
hj : j ≠ i
⊢ (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
    (ConcreteCategory.hom (Λ[n + 2, i].ι.app (Opposite.op ⦋n + 1⦌) ≫ (yonedaEquiv.symm σ).app (Opposite.op ⦋n + 1⦌)))
      (horn.face i j hj)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
n : ℕ
⊢ X.skeleton (n + 1) = X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x

Tactic:
apply le_antisymm
  · conv_lhs => dsimp [skeleton]
    simp only [iSup_le_iff]
    rintro ⟨d, hd⟩ x
    rw [Nat.lt_succ_iff] at hd
    obtain hd | rfl := hd.lt_or_eq
    · exact (X.ofSimplex_le_skeleton _ hd).trans le_sup_left
    · exact le_trans (le_trans (by rfl) (le_iSup _ x)) le_sup_right
  · simp only [sup_le_iff, iSup_le_iff]
    constructor
    · exact X.skeleton.monotone (by simp)
    · intro x
      apply X.ofSimplex_le_skeleton _ (by simp)

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

Goal state before:
pp: V W x✝ : Truncated 2
⊢ (mapHomotopyCategory (𝟙 x✝)).toCatHom.toFunctor = (𝟙 (Cat.of x✝.HomotopyCategory)).toFunctor

Tactic:
exact HomotopyCategory.functor_ext (by simp) (by cat_disch)

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

Goal state before:
pp: V W X✝ Y✝ Z✝ : Truncated 2
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (mapHomotopyCategory (x✝¹ ≫ x✝)).toCatHom.toFunctor =
    ((mapHomotopyCategory x✝¹).toCatHom ≫ (mapHomotopyCategory x✝).toCatHom).toFunctor

Tactic:
exact HomotopyCategory.functor_ext (by simp) (by cat_disch)

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
⊢ σ j ≫ toMk₁ i = toMk₁ i.succ

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
  change toMk₁ i (j.predAbove k) = _
  by_cases! hk : i < k
  · #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
    It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
    canonicalizer; a minimization would help. The original proof was:
    `grind [Fin.predAbove_of_castSucc_lt, toMk₁_of_le_castSucc]` -/
    simp; grind [Fin.predAbove_of_castSucc_lt, toMk₁_of_le_castSucc]
  · dsimp
    rw [toMk₁_of_castSucc_lt i.succ k (by simpa), toMk₁_of_castSucc_lt]
    by_cases hk' : j.castSucc < k
    · rwa [Fin.predAbove_of_castSucc_lt _ _ hk', Fin.castSucc_pred_lt_iff]
    · 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.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
⊢ StrictMono ⇑(orderHomOfSimplex x hm) ↔ StrictMono ⇑(objEquiv x)

Tactic:
have (a b : Fin (p + 1) × Fin (q + 1)) (hab : a ≤ b) :
      a < b ↔ ((a.1 : ℕ) + a.2 < (b.1 : ℕ) + b.2) := by
    obtain ⟨h₁, h₂⟩ := hab
    rw [Prod.lt_iff]
    lia

Goal state after:
p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
this : ∀ (a b : Fin (p + 1) × Fin (q + 1)), a ≤ b → (a < b ↔ ↑a.1 + ↑a.2 < ↑b.1 + ↑b.2)
⊢ StrictMono ⇑(orderHomOfSimplex x hm) ↔ StrictMono ⇑(objEquiv x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx✝ : x ∈ X.nonDegenerate n
hx : (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.nonDegenerate n
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx✝⟩)

Tactic:
have := mono' _ 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
hx : (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.nonDegenerate n
this : Mono (yonedaEquiv.symm ((ConcreteCategory.hom (f.app (op ⦋n⦌))) x))
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx✝⟩)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i : Fin (n + 2)
⊢ (ConcreteCategory.hom (SimplicialObject.δ X i)) x ∈ X.nonDegenerate n

Tactic:
by
  have := Nonsingular.mono' x hx
  have : X.δ i x = (yonedaEquiv.symm x).app _
    (stdSimplex.objEquiv.symm (SimplexCategory.δ i)) := rfl
  rw [this, nonDegenerate_iff_of_mono, stdSimplex.mem_nonDegenerate_iff_mono,
    Equiv.apply_symm_apply]
  infer_instance

Goal state after:
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 ι
j : ι
c : f.Cell j
⊢ ¬(↑c.s).subcomplex ≤ f.filtration j

Tactic:
simp only [ofSimplex_le_iff, filtration_def, Subfunctor.max_obj, Subfunctor.iSup_obj,
    Set.mem_union, Set.mem_iUnion, not_or, not_exists]
  refine ⟨c.s.val.notMem, fun i hi c' h ↦ ?_⟩
  rw [← c.rank_s, ← c'.rank_s] at hi
  refine lt_irrefl _ (hi.trans (f.lt ?_))
  refine ⟨fun hxy ↦ ?_, lt_of_le_of_ne ?_ ((P.ne _ _).symm)⟩
  · rw [hxy] at hi
    exact (lt_irrefl _ hi).elim
  · rw [← ofSimplex_le_iff] at h
    rwa [Subcomplex.N.le_iff, SSet.N.le_iff]

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

Goal state before:
pp: case a.notMem
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
⊢ s.subcomplex ≤ f.filtration j

Tactic:
← c.rank_s

Goal state after:
case a.notMem
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
⊢ s.subcomplex ≤ f.filtration (f.rank c.s)
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
j₁ : J
α : j₀ ⟶ j₁
hα :
  ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
⊢ ∃ j x', x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j)) x'

Tactic:
let s : (F ⋙ (evaluation C (Type w')).obj (X.obj j₁)).sections :=
    { val k := (F.obj k).map (X.map α) (z k)
      property {k k'} φ := by
        dsimp
        rw [NatTrans.naturality_apply, ← hα φ] }

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
j₁ : J
α : j₀ ⟶ j₁
hα :
  ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
s : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j₁)).sections :=
  ⟨fun k ↦ (ConcreteCategory.hom ((F.obj k).map (X.map α))) (z k), ⋯⟩
⊢ ∃ j x', x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j)) x'
Module: Mathlib.CategoryTheory.Presentable.Presheaf

Goal state before:
pp: A : Type u'
inst✝⁴ : Category.{v', u'} A
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalLocallyPresentable A κ
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
⊢ IsCardinalLocallyPresentable (Cᵒᵖ ⥤ A) κ

Tactic:
by
  have hA := (IsCardinalLocallyPresentable.iff_exists_isStrongGenerator A κ).1 inferInstance
  obtain ⟨P, _, hP₁, hP₂⟩ := hA
  rw [IsCardinalLocallyPresentable.iff_exists_isStrongGenerator]
  refine ⟨_, inferInstance, isStrongGenerator hP₁ C, ?_⟩
  rintro _ ⟨X, G, hG⟩
  have := hP₂ _ hG
  rw [isCardinalPresentable_iff] at this ⊢
  infer_instance

Goal state after:
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 κ
⊢ isCardinalPresentable C κ = P.colimitsCardinalClosure κ

Tactic:
refine le_antisymm ?_ (P.colimitsCardinalClosure_le_isCardinalPresentable hS₂)
  have := hS₁.isDense_colimitsCardinalClosure_ι hS₂
  intro X hX
  rw [isCardinalPresentable_iff] at hX
  rw [← (P.colimitsCardinalClosure κ).retractClosure_eq_self]
  obtain ⟨j, φ, hφ⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ
    ((P.colimitsCardinalClosure κ).ι.denseAt X) (𝟙 X)
  exact ⟨_, j.left.2, ⟨{ i := _, r := _, retract := hφ }⟩⟩

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.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ {
          hom :=
            pushout.desc
              ((α_ X₁.right X₂.right X₃.left).hom ≫
                X₁.right ◁
                    pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left)
                      (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                  pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                    (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
              (Arrow.Hom.left (whiskerRightIso X₁ X₂).hom ≫
                pushout.desc
                  (X₁.right ◁
                      pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left)
                        (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                    pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                      (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                  (pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                    (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                  ⋯)
              ⋯,
          inv :=
            pushout.desc
              (Arrow.Hom.left (whiskerLeftIso X₂ X₃).hom ≫
                pushout.desc
                  (pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                    (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                  (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left)
                        (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                      X₃.right ≫
                    pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                      (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                  ⋯)
              ((α_ X₁.left X₂.right X₃.right).inv ≫
                pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                    X₃.right ≫
                  pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                    (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
              ⋯,
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      (X₁ □ X₂ □ X₃).hom =
    ((X₁ □ X₂) □ X₃).hom ≫ (α_ X₁.right X₂.right X₃.right).hom

Tactic:
· apply pushout.hom_ext (by simp [← MonoidalCategory.whiskerLeft_comp])
    · apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
      · simp [← MonoidalCategory.whiskerLeft_comp, ← MonoidalCategory.comp_whiskerRight_assoc]
      · simp [← MonoidalCategory.comp_whiskerRight_assoc]

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

Goal state before:
pp: X Y Z : SSet
T : Type u_1
f : X _⦋0⦌ → T
hf : ∀ ⦃x₀ x₁ : X _⦋0⦌⦄ (x : Edge x₀ x₁), f x₀ = f x₁
⊢ ∀ (a b : X _⦋0⦌), π₀Rel a b → f a = f b

Tactic:
by rintro x y ⟨e⟩; exact hf e

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 d : ℕ
is : Fin (d + 1)
ds : ℕ
s : (Δ[m + 1] ⊗ Δ[n]) _⦋ds⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate ds
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋ds⦌)
hds : (Subcomplex.N.mk s hs₁ hs₂).dim = d + 1
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) hds is.succ
dt : ℕ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋dt⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate dt
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋dt⦌)
it : Fin (d + 1)
hdt : (Subcomplex.N.mk t ht₁ ht₂).dim = d + 1
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) hdt it.succ
h₁ :
  { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := hds, index := is, isIndex := hs } ≠
    { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := hdt, index := it, isIndex := ht }
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := hds, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := hdt, index := it, isIndex := ht }
⊢ (finset { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := hds, index := is, isIndex := hs }.x ⋯).card <
    (finset { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := hdt, index := it, isIndex := ht }.x ⋯).card

Tactic:
obtain rfl : ds = d + 1 := hds

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is : Fin (d + 1)
dt : ℕ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋dt⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate dt
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋dt⦌)
it : Fin (d + 1)
hdt : (Subcomplex.N.mk t ht₁ ht₂).dim = d + 1
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) hdt it.succ
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
h₁ :
  { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } ≠
    { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := hdt, index := it, isIndex := ht }
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 := hdt, index := it, isIndex := ht }
⊢ (finset { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }.x ⋯).card <
    (finset { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := hdt, index := it, isIndex := ht }.x ⋯).card
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne

Goal state before:
pp: case pos
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : j ≤ i.castSucc
⊢ ↑((stdSimplex.objEquiv.symm (SimplexCategory.σ i)) j) + 0 % 2 = ↑j

Tactic:
Nat.zero_mod,

Goal state after:
case pos
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : j ≤ i.castSucc
⊢ ↑((stdSimplex.objEquiv.symm (SimplexCategory.σ i)) j) + 0 = ↑j
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 : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
⊢ stdSimplex.δ j.castSucc.castSucc ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv h.map)) = g.map

Tactic:
simp [stdSimplex.δ_comp_yonedaEquiv_symm, δ_opObjEquiv,
      ← stdSimplex.yonedaEquiv_δ_comp, ← hij, Fin.rev_castSucc]

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

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
⊢ ⇑m.toTopHomeo ∘ ⇑(ConcreteCategory.hom (SSet.toTop.map (SSet.stdSimplex.map f))) =
    stdSimplex.map ⇑(ConcreteCategory.hom f) ∘ ⇑n.toTopHomeo

Tactic:
ext x : 1

Goal state after:
n m : SimplexCategory
f : n ⟶ m
x : ↑(SSet.toTop.obj (SSet.stdSimplex.obj n))
⊢ (⇑m.toTopHomeo ∘ ⇑(ConcreteCategory.hom (SSet.toTop.map (SSet.stdSimplex.map f)))) x =
    (stdSimplex.map ⇑(ConcreteCategory.hom f) ∘ ⇑n.toTopHomeo) x