mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j k i : ι
⊢ ⋯.symmetry ⋯ =
    𝟙
      (match (i, i) with
      | (i, j) => ⋯.pullback (f j))

Tactic:
apply (hf i).rep.hom_ext'

Goal state after:
case h₁
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j k i : ι
⊢ ⋯.symmetry ⋯ ≫ ⋯.fst' (f i) =
    𝟙
        (match (i, i) with
        | (i, j) => ⋯.pullback (f j)) ≫
      ⋯.fst' (f i)

case h₂
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j k i : ι
⊢ ⋯.symmetry ⋯ ≫ ⋯.snd (f i) =
    𝟙
        (match (i, i) with
        | (i, j) => ⋯.pullback (f j)) ≫
      ⋯.snd (f i)
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: ι : Type u_1
S : Scheme
Ω : ι → Type u
inst✝¹ : (i : ι) → Field (Ω i)
inst✝ : ∀ (i : ι), IsSepClosed (Ω i)
s : (i : ι) → Spec (CommRingCat.of (Ω i)) ⟶ S
hs : ⋃ i, Set.range ⇑(s i) = Set.univ
X : S.Etale
α : Type (u + 1)
T : α → S.Etale
f : (i : α) → T i ⟶ X
hR :
  ∀ (Φ : (ObjectProperty.ofObj fun i ↦ pointSmallEtale (s i)).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : (Sieve.ofArrows T f).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
x : ↥X.left
⊢ ∃ i y, (f i).left y = x

Tactic:
obtain ⟨i, hi⟩ : ∃ i, s i default = X.hom x := by
      have := Set.mem_univ (X.hom x)
      simp only [← hs, Functor.id_obj, Set.mem_iUnion, Set.mem_range] at this
      obtain ⟨i, y, hy⟩ := this
      obtain rfl := Subsingleton.elim y default
      exact ⟨i, hy⟩

Goal state after:
ι : Type u_1
S : Scheme
Ω : ι → Type u
inst✝¹ : (i : ι) → Field (Ω i)
inst✝ : ∀ (i : ι), IsSepClosed (Ω i)
s : (i : ι) → Spec (CommRingCat.of (Ω i)) ⟶ S
hs : ⋃ i, Set.range ⇑(s i) = Set.univ
X : S.Etale
α : Type (u + 1)
T : α → S.Etale
f : (i : α) → T i ⟶ X
hR :
  ∀ (Φ : (ObjectProperty.ofObj fun i ↦ pointSmallEtale (s i)).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : (Sieve.ofArrows T f).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
x : ↥X.left
i : ι
hi : (s i) default = X.hom x
⊢ ∃ i y, (f i).left y = x
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X Y : D
P : MorphismProperty C
inst✝² : F✝.Faithful
inst✝¹ : F✝.Full
inst✝ : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F✝ P f
hg : relative F✝ P g
⊢ relative F✝ P (f ≫ g)

Tactic:
by
    refine ⟨comp_mem _ _ _ hf.1 hg.1, fun Z X p fst snd h ↦ ?_⟩
    rw [← hg.1.lift_snd (fst ≫ f) snd (by simpa using h.w)]
    refine comp_mem _ _ _ (hf.property (hg.1.fst p) fst _
      (IsPullback.of_bot ?_ ?_ (hg.1.isPullback p))) (hg.property_snd p)
    · rw [← Functor.map_comp, lift_snd]
      exact h
    · symm
      apply hg.1.lift_fst

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a : ℕ
ha : n = a + q
⊢ hσ' q n (n + 1) ⋯ = (-1) ^ a • X.σ ⟨a, ⋯⟩

Tactic:
hσ'_eq ha rfl,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a : ℕ
ha : n = a + q
⊢ ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯ = (-1) ^ a • X.σ ⟨a, ⋯⟩
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ ∀ ε > 0, ∃ k, dist x ↑k < ε

Tactic:
exact fun _ ↦ Padic.rat_dense _ x

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

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ DegeneraciesVanish (PInfty.f (n + 1))

Tactic:
· simp [degeneraciesVanish_succ_iff]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂.map (toKaroubiCompN₂IsoN₁.inv.app X ≫ toKaroubiCompN₂IsoN₁.hom.app X) = 𝟙 (Γ₂.obj (N₁.obj X))

Tactic:
Iso.inv_hom_id_app,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂.map (𝟙 (N₁.obj X)) = 𝟙 (Γ₂.obj (N₁.obj X))
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq :
  K[X].d i j ≫
      s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
        (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫
      K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0

Tactic:
eq,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq :
  K[X].d i j ≫
      s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
        (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ 0 = 0
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : t ≤ 0
x : X
⊢ (F.extend t) x = f₀ x

Tactic:
rw [← F.apply_zero]
  exact ContinuousMap.congr_fun (Set.IccExtend_of_le_left (zero_le_one' ℝ) F.curry ht) x

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

Goal state before:
pp: case mpr
Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
hloops : ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
x y : Y
p₁ p₂ : Path x y
⊢ p₁.Homotopic p₂

Tactic:
rw [← eq]

Goal state after:
case mpr
Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
hloops : ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
x y : Y
p₁ p₂ : Path x y
⊢ mk p₁ = mk p₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
hS : ¬S = Finset.univ
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 1), ¬j i = i_1

Tactic:
Finset.eq_univ_iff_forall,

Goal state after:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
hS : ¬∀ (x : Fin (n + 3)), x ∈ S
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 1), ¬j i = i_1
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: case refine_1
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
eq₁ :
  e.ιColimitType (WalkingMultispan.right ((MultispanShape.prod ι).fst (i₁, i₂)))
      ((ConcreteCategory.hom (e.map (WalkingMultispan.Hom.fst (i₁, i₂)))) ⟨x₁, ⋯⟩) =
    e.ιColimitType (WalkingMultispan.left (i₁, i₂)) ⟨x₁, ⋯⟩
eq₂ :
  e.ιColimitType (WalkingMultispan.right ((MultispanShape.prod ι).snd (i₁, i₂)))
      ((ConcreteCategory.hom (e.map (WalkingMultispan.Hom.snd (i₁, i₂)))) ⟨x₁, ⋯⟩) =
    e.ιColimitType (WalkingMultispan.left (i₁, i₂)) ⟨x₁, ⋯⟩
⊢ (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₂) ⟨x₁, h₂⟩

Tactic:
dsimp [e] at eq₁ eq₂

Goal state after:
case refine_1
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
eq₁ :
  (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₁) ⟨x₁, ⋯⟩ =
    (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.left (i₁, i₂)) ⟨x₁, ⋯⟩
eq₂ :
  (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₂) ⟨x₁, ⋯⟩ =
    (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.left (i₁, i₂)) ⟨x₁, ⋯⟩
⊢ (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
hS : ¬{i, a, b} = univ
⊢ stdSimplex.edge n a b hab ∈ Λ[n, i].obj (op ⦋1⦌)

Tactic:
Finset.eq_univ_iff_forall,

Goal state after:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
hS : ¬∀ (x : Fin (n + 1)), x ∈ {i, a, b}
⊢ stdSimplex.edge n a b hab ∈ Λ[n, i].obj (op ⦋1⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_3
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
hS : ¬{i, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩} = univ
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 3), ¬(stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯) i = i_1

Tactic:
Finset.eq_univ_iff_forall,

Goal state after:
case refine_3
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
hS : ¬∀ (x : Fin (n + 4)), x ∈ {i, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩}
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 3), ¬(stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯) i = i_1
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w : ∀ (x : ToType X₁), (ConcreteCategory.hom (t ≫ r)) x = (ConcreteCategory.hom (l ≫ b)) x
⊢ Function.Injective ⇑(ConcreteCategory.hom k)

Tactic:
simp only [comp_apply] at w

Goal state after:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
⊢ Function.Injective ⇑(ConcreteCategory.hom k)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
d : ℕ
x : ↑(X.nonDegenerate d)
n : ℕ
⊢ ↑x ∈ (X.skeleton n).obj (op ⦋d⦌) ↔ d < n

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ X.mem_skeleton _⟩

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

Goal state before:
pp: case a.left
X : SSet
n : ℕ
⊢ X.skeleton n ≤ X.skeleton (n + 1)

Tactic:
exact X.skeleton.monotone (by simp)

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

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b c : CatEnriched C
f f' : a ⟶ b
α : f = f'
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom α) (eqToHom β) = eqToHom ⋯

Tactic:
cases α; cases β; simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
α : f = g
⊢ base (eqToHom α) = eqToHom ⋯

Tactic:
by cases α; rfl

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 : CatEnrichedOrdinary C
f f' : a ⟶ b
α : f = f'
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom α) (eqToHom β) = eqToHom ⋯

Tactic:
cases α; cases β; simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:

Tactic:
_ = 𝟙 _ ⊗≫
      X.fst ◁ (f.f ▷ U ≫ (HalfBraiding.β Y₂.snd U).hom) ⊗≫
        (HalfBraiding.β X.snd U).hom ▷ Y₂.fst ⊗≫ 𝟙 _ := by monoidal
    _ = 𝟙 _ ⊗≫
      X.fst ◁ (HalfBraiding.β Y₁.snd U).hom ⊗≫
        ((X.fst ⊗ U) ◁ f.f ≫ (HalfBraiding.β X.snd U).hom ▷ Y₂.fst) ⊗≫ 𝟙 _ := by
      rw [f.comm]; monoidal
    _ = _ := by rw [whisker_exchange]; monoidal

Goal state after:
Module: Mathlib.CategoryTheory.Functor.CurryingThree

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_4
E : Type u_9
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_4} C₃
inst✝ : Category.{v_9, u_9} E
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (((currying₃.unitIso.inv.app F).app X₁).app X₂).app X₃ =
    𝟙 (((((currying₃.functor ⋙ currying₃.inverse).obj F).obj X₁).obj X₂).obj X₃)

Tactic:
simp [currying₃, Equivalence.unitInv]

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

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

Tactic:
by
  apply CategoryTheory.Quotient.sound
  exact FreeSimplexQuiver.homRel.δ_comp_σ_of_gt H

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
⊢ { len := n }.len ≤ d

Tactic:
by dsimp; lia

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
⊢ { len := n + 1 }.len ≤ d

Tactic:
by dsimp; lia

Goal state after:
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 ⋯ ⋯)
n : ℕ
hn : n < d
i : Fin (n + 1)
⊢ { len := n + 1 }.len ≤ d

Tactic:
by dsimp; lia

Goal state after:
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 ⋯ ⋯)
n : ℕ
hn : n < d
i : Fin (n + 1)
⊢ { len := n }.len ≤ d

Tactic:
by dsimp; lia

Goal state after:
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.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
z₀ z₁ : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge z₀ z₁
⊢ (mapHomotopyCategory (α_ X Y Z).hom).map
      ((inverse (X ⊗ Y) Z).map (Prod.mkHom ((inverse X Y).map (𝟙 (mk x, mk y))) (homMk e))) =
    (inverse X (Y ⊗ Z)).map (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (𝟙 (mk y), homMk e)))

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.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
z₀ z₁ : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge z₀ z₁
⊢ (mapHomotopyCategory (α_ X Y Z).hom).map
      ((inverse (X ⊗ Y) Z).map (Prod.mkHom ((inverse X Y).map (𝟙 (mk x, mk y))) (homMk e))) =
    (inverse X (Y ⊗ Z)).map (Prod.mkHom (𝟙 (mk x)) (homMk ((Edge.id y).tensor e)))
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.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
z₀ z₁ : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge z₀ z₁
⊢ (mapHomotopyCategory (α_ X Y Z).hom).map
      ((inverse (X ⊗ Y) Z).map (Prod.mkHom ((inverse X Y).map (𝟙 (mk x, mk y))) (homMk e))) =
    (inverse X (Y ⊗ Z)).map (Prod.mkHom (𝟙 (mk x)) (homMk ((Edge.id y).tensor e)))

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.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
z₀ z₁ : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge z₀ z₁
⊢ (mapHomotopyCategory (α_ X Y Z).hom).map
      ((inverse (X ⊗ Y) Z).map (Prod.mkHom ((inverse X Y).map (𝟙 (mk x, mk y))) (homMk e))) =
    homMk ((Edge.id x).tensor ((Edge.id y).tensor e))
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
hij : i < j
⊢ ↑j ≤ ⦋n⦌.len + 1

Tactic:
by dsimp; lia

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

Goal state before:
pp: X : SSet
n : ℕ
s : X _⦋n⦌
A : X.Subcomplex
hs : s ∉ A.obj (Opposite.op ⦋n⦌)
⊢ ∃ x f, Epi f ∧ (ConcreteCategory.hom (X.map f.op)) x.simplex = s

Tactic:
by
  refine ⟨⟨(S.mk s).toN, fun h ↦ hs ?_⟩, ⟨(S.mk s).toNπ, inferInstance, S.map_toNπ_op_apply _⟩⟩
  simp only [← ofSimplex_le_iff] at h ⊢
  simpa using h

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
⊢ ∃ y, x = ↑y ∨ x = ↑(P.p y)

Tactic:
have := Set.mem_univ x
  rw [← P.union, Set.mem_union] at this
  obtain h | h := this
  · obtain ⟨y, hy⟩ := P.p.surjective ⟨x, h⟩
    exact ⟨y, Or.inr (by rw [hy])⟩
  · exact ⟨⟨_, h⟩, Or.inl rfl⟩

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x y : X.N
h : x ≤ y
⊢ ∃ x_1, Mono x_1 ∧ (ConcreteCategory.hom (X.map x_1.op)) y.simplex = x.simplex

Tactic:
by
    obtain ⟨f, _, hf⟩ := le_iff_exists_mono.1 h
    exact ⟨f, inferInstance, hf⟩

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
⊢ h.I ∩ h.II = ∅

Tactic:
ext s
    simp only [I, II, Set.mem_inter_iff, Set.mem_range, Set.mem_empty_iff_false,
      iff_false, not_and, not_exists, forall_exists_index]
    rintro t rfl s
    exact (h.type₁_ne_type₂ t s).symm

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : HasLimitsOfShape Jᵒᵖ (Type w)
hJ : HasCardinalLT (Arrow J) κ
X : C
hX : (isCardinalPresentable C κ).ColimitOfShape J X
this : ∀ (j : J), IsCardinalPresentable (hX.diag.obj j) κ
⊢ IsCardinalPresentable X κ

Tactic:
exact isCardinalPresentable_of_isColimit _ hX.isColimit κ hJ

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

Goal state before:
pp: C : Type u
inst✝² : SmallCategory C
inst✝¹ : HasColimitsOfSize.{w, w, max u u', max (u + 1) (u' + 1)} (Type (max u u'))
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
X : C
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J (coyoneda.obj (op (uliftYoneda.{u', u, u}.obj X)))

Tactic:
by
    let e : (coyoneda.obj (op (uliftYoneda.{u'}.obj X))) ≅
        (evaluation _ _).obj (op X) ⋙ uliftFunctor :=
      NatIso.ofComponents (fun P ↦ Equiv.toIso (uliftYonedaEquiv.trans Equiv.ulift.symm))
    exact preservesColimitsOfShape_of_natIso e.symm

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

Goal state before:
pp: case refine_1
X : SSet
inst✝ : X.Finite
⊢ IsFinitelyPresentable (∐ fun s ↦ Δ[s.dim])

Tactic:
apply +allowSynthFailures isCardinalPresentable_of_isColimit' _ (coproductIsCoproduct _)

Goal state after:
case refine_1.hK
X : SSet
inst✝ : X.Finite
⊢ HasCardinalLT (Arrow (Discrete X.N)) Cardinal.aleph0

case inst
X : SSet
inst✝ : X.Finite
⊢ ∀ (k : Discrete X.N), IsCardinalPresentable ((Discrete.functor fun s ↦ Δ[s.dim]).obj k) Cardinal.aleph0
Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable

Goal state before:
pp: case refine_1
X : SSet
inst✝ : X.Finite
⊢ IsFinitelyPresentable (∐ fun s ↦ Δ[s.dim])

pp: case refine_2
X : SSet
inst✝ : X.Finite
⊢ Epi (Sigma.desc fun s ↦ yonedaEquiv.symm s.simplex)

Tactic:
· apply +allowSynthFailures isCardinalPresentable_of_isColimit' _ (coproductIsCoproduct _)
    · exact hasCardinalLT_of_finite _ _ (by rfl)
    · rintro s
      dsimp
      infer_instance

Goal state after:
case refine_2
X : SSet
inst✝ : X.Finite
⊢ Epi (Sigma.desc fun s ↦ yonedaEquiv.symm s.simplex)
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
Q : C
⊢ Q ◁ f ≫ Q ◁ inl = Q ◁ g ≫ Q ◁ inr

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp, hP.w]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H✝ H : Homotopy f g
n : ℕ
⊢ ((alternatingFaceMapComplex C).map f).f n =
    (dNext n) (ToChainHomotopy.hom H) + (prevD n) (ToChainHomotopy.hom H) + ((alternatingFaceMapComplex C).map g).f n

Tactic:
cases n with
    | zero =>
      rw [prevD_eq (j' := 1) (w := by simp), dNext_eq_zero _ _ (by simp), zero_add]
      simp [ToChainHomotopy.comm_zero H]
    | succ n =>
      rw [dNext_eq (i' := n) (w := by simp), prevD_eq (j' := n + 2) (w := by simp)]
      simp [ToChainHomotopy.comm_succ H]

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 : ℕ
hd : x.dim = d
⊢ (φ x hd (min x hd).succ).2 = (φ x hd (min x hd).castSucc).2

Tactic:
have := φ_succAbove x hd (min x hd)

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
this : φ x hd ((min x hd).castSucc.succAbove (min x hd)) = (objEquiv (x.cast hd).simplex) (min x hd)
⊢ (φ x hd (min x hd).succ).2 = (φ x hd (min x hd).castSucc).2