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

Goal state before:
pp: case neg.e_a.e_s
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
i : ℕ
hi : i < n + 1
⊢ ⟨i, hi⟩ ≠ q' ∧ ⟨i, hi⟩ ∈ {i | ↑i < q + 1} ↔ ⟨i, hi⟩ ∈ {i | ↑i < q}

Tactic:
Finset.mem_filter_univ,

Goal state after:
case neg.e_a.e_s
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
i : ℕ
hi : i < n + 1
⊢ ⟨i, hi⟩ ≠ q' ∧ i < q + 1 ↔ i < q
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
h : Z ⟶ Z'
⊢ (f.postComp h).φ = f.φ ≫ h

Tactic:
unfold φ postComp
  simp only [add_comp, sum_comp, assoc]

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

Goal state before:
pp: Δ : SimplexCategoryᵒᵖ
A₁ A₂ : IndexSet Δ
h₁ : A₁.fst = A₂.fst
h₂ : A₁.e ≫ eqToHom ⋯ = A₂.e
⊢ A₁ = A₂

Tactic:
rcases A₁ with ⟨Δ₁, ⟨α₁, hα₁⟩⟩
  rcases A₂ with ⟨Δ₂, ⟨α₂, hα₂⟩⟩
  simp only at h₁
  subst h₁
  simp only [eqToHom_refl, comp_id, IndexSet.e] at h₂
  simp only [h₂]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X✝ Y✝ Z✝ : Split C
Φ₁₂ : X✝.Hom Y✝
Φ₂₃ : Y✝.Hom Z✝
n : ℕ
⊢ X✝.s.ι n ≫ (Φ₁₂.F ≫ Φ₂₃.F).app (op ⦋n⦌) = (Φ₁₂.f n ≫ Φ₂₃.f n) ≫ Z✝.s.ι n

Tactic:
dsimp
        simp only [assoc, Split.Hom.comm_assoc, Split.Hom.comm]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
⊢ Δ ≠ Δ''

Tactic:
by_contra h
    simp only [left_eq_add, h, add_eq_zero, and_false, reduceCtorEq] at eq

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi (Karoubi C)
⊢ P.p.f ≫ P.p.f = P.p.f

Tactic:
by
  simpa only [hom_ext_iff, comp_f] using P.idem

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

Goal state before:
pp: case mk.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : ⦋n⦌.len = ⦋m⦌.len + (k + 1) + 1
⊢ PInfty.f n ≫ X.map i.op = 0

Tactic:
simp only [← add_assoc] at hk

Goal state after:
case mk.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : n = m + k + 1 + 1
⊢ PInfty.f n ≫ X.map i.op = 0
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
⊢ (Γ₂N₁.inv ≫ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom).app X = (𝟙 (N₁ ⋙ Γ₂)).app X

Tactic:
NatTrans.comp_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
⊢ Γ₂N₁.inv.app X ≫ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom.app X = (𝟙 (N₁ ⋙ Γ₂)).app X
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
⊢ Compatibility.υ isoN₁ = Γ₂N₁

Tactic:
by
  dsimp only [isoN₁]
  ext1
  rw [← cancel_epi Γ₂N₁.inv, Iso.inv_hom_id]
  ext X : 2
  rw [NatTrans.comp_app, Γ₂N₁_inv, compatibility_Γ₂N₁_Γ₂N₂_natTrans X, Compatibility.υ_hom_app,
    Preadditive.DoldKan.equivalence_unitIso, Iso.app_inv, assoc]
  dsimp only [Functor.comp_obj, Preadditive.DoldKan.equivalence_inverse, Preadditive.DoldKan.Γ.eq_1,
    toKaroubiEquivalence, Functor.asEquivalence_functor, Preadditive.DoldKan.N.eq_1,
    NatTrans.id_app]
  rw [← NatTrans.comp_app_assoc, ← Γ₂N₂_inv, Iso.inv_hom_id, NatTrans.id_app, id_comp,
    Γ₂N₂ToKaroubiIso_inv_app, ← Γ₂.map_comp, Iso.inv_hom_id_app, Γ₂.map_id]

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

Goal state before:
pp: case pos.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∀ b ∈ Finset.univ, b ≠ 0 → PInfty.f (n + 1) ≫ ((-1) ^ ↑b • X.δ b) = 0

Tactic:
intro b

Goal state after:
case pos.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
⊢ b ∈ Finset.univ → b ≠ 0 → PInfty.f (n + 1) ≫ ((-1) ^ ↑b • X.δ b) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ⦋n'⦌ ≠ ⦋n⦌

Tactic:
by_contra h'

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
h' : ⦋n'⦌ = ⦋n⦌
⊢ False
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
⊢ (toKaroubi (ChainComplex C ℕ)).map (PInfty ≫ s.toNondegComplex) = (toKaroubi (ChainComplex C ℕ)).map s.toNondegComplex

Tactic:
by simp [toNondegComplex]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ (𝟙 N₂ ◫ N₂Γ₂.inv) ≫ (N₂.associator Γ₂ N₂).inv ≫ Γ₂N₂.natTrans ◫ 𝟙 N₂ = 𝟙 N₂

Tactic:
ext P : 2

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ ((𝟙 N₂ ◫ N₂Γ₂.inv) ≫ (N₂.associator Γ₂ N₂).inv ≫ Γ₂N₂.natTrans ◫ 𝟙 N₂).app P = (𝟙 N₂).app P
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 : 1 ≤ t
x : X
⊢ (F.extend t) x = f₁ x

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

Goal state after:
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : f₀.Homotopy f₁
G : g₀.Homotopy g₁
x : A
⊢ (F (0, x), G (0, x)) = (f₀.prodMk g₀) x

Tactic:
simp only [prod_eval, Homotopy.apply_zero]

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

Goal state before:
pp: I : Type u
X : I → TopCat
x : (i : I) → ↑(π.obj (X i))
⊢ Path.Homotopic.pi (𝟙 x) = 𝟙 { as := fun i ↦ (x i).as }

Tactic:
change (Path.Homotopic.pi fun i => Path.Homotopic.Quotient.mk _) = _
    simp only [Path.Homotopic.pi_lift]
    rfl

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

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
⊢ ∀ (X : ↑(π.obj (TopCat.of (↑A × ↑B)))),
    ((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X = (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X

pp: case h_map
A : TopCat
B : TopCat
⊢ ∀ (X Y : ↑(π.obj (TopCat.of (↑A × ↑B)))) (f : X ⟶ Y),
    ((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).map f ≍ (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).map f

Tactic:
· intros; apply FundamentalGroupoid.ext; apply Prod.ext <;> simp <;> rfl

Goal state after:
case h_map
A : TopCat
B : TopCat
⊢ ∀ (X Y : ↑(π.obj (TopCat.of (↑A × ↑B)))) (f : X ⟶ Y),
    ((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).map f ≍ (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).map f
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₀ x₃
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ x₁ = x₃

Tactic:
by convert! hp 1 <;> simp

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

Goal state before:
pp: V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ (ρ_ (F.obj (X ⟶[V] Y))).inv ≫
      F.obj (X ⟶[V] Y) ◁ (ε F ≫ F.map (eId V Y)) ≫ μ F (X ⟶[V] Y) (Y ⟶[V] Y) ≫ F.map (eComp V X Y Y) =
    𝟙 (F.obj (X ⟶[V] Y))

Tactic:
simp only [MonoidalCategory.whiskerLeft_comp, Category.assoc,
      Functor.LaxMonoidal.μ_natural_right_assoc,
      Functor.LaxMonoidal.right_unitality_inv_assoc]

Goal state after:
V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ F.map (ρ_ (X ⟶[V] Y)).inv ≫ F.map ((X ⟶[V] Y) ◁ eId V Y) ≫ F.map (eComp V X Y Y) = 𝟙 (F.obj (X ⟶[V] Y))
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ FreeSimplexQuiver.homRel
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i.succ) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ i))
    (𝟙 (mk n).as)

Tactic:
exact FreeSimplexQuiver.homRel.δ_comp_σ_succ

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

Goal state before:
pp: x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ IsSplitEpi e

Tactic:
induction he with

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

Goal state before:
pp: x✝² x✝¹ x✝ : Truncated 2
⊢ (iso x✝² x✝¹).symm.hom ▷ hoFunctor₂.obj x✝ ≫ (iso (x✝² ⊗ x✝¹) x✝).symm.hom ≫ hoFunctor₂.map (α_ x✝² x✝¹ x✝).hom =
    (α_ (hoFunctor₂.obj x✝²) (hoFunctor₂.obj x✝¹) (hoFunctor₂.obj x✝)).hom ≫
      hoFunctor₂.obj x✝² ◁ (iso x✝¹ x✝).symm.hom ≫ (iso x✝² (x✝¹ ⊗ x✝)).symm.hom

Tactic:
ext; apply associativity

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

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

Tactic:
Fin.predAbove_of_castSucc_lt _ _ hk',

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
hk' : j.castSucc < k
⊢ (k.pred ⋯).castSucc < i
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: case mp
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
left✝¹ : { dim := d + 1, simplex := y }.dim = { dim := d, simplex := x }.dim + 1
f : ⦋{ dim := d, simplex := x }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y }.dim⦌
h₂ :
  ∀ (y_1 : ⦋{ dim := d, simplex := x }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y }.dim⦌),
    (fun f ↦
          Mono f ∧
            (ConcreteCategory.hom (X.map f.op)) { dim := d + 1, simplex := y }.simplex =
              { dim := d, simplex := x }.simplex)
        y_1 →
      y_1 = f
left✝ : Mono f
h₁ : (ConcreteCategory.hom (X.map f.op)) { dim := d + 1, simplex := y }.simplex = { dim := d, simplex := x }.simplex
⊢ ∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x

Tactic:
obtain ⟨i, rfl⟩ := SimplexCategory.eq_δ_of_mono f

Goal state after:
case mp
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
left✝¹ : { dim := d + 1, simplex := y }.dim = { dim := d, simplex := x }.dim + 1
i : Fin ({ dim := d, simplex := x }.dim + 2)
h₂ :
  ∀ (y_1 : ⦋{ dim := d, simplex := x }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y }.dim⦌),
    (fun f ↦
          Mono f ∧
            (ConcreteCategory.hom (X.map f.op)) { dim := d + 1, simplex := y }.simplex =
              { dim := d, simplex := x }.simplex)
        y_1 →
      y_1 = SimplexCategory.δ i
left✝ : Mono (SimplexCategory.δ i)
h₁ :
  (ConcreteCategory.hom (X.map (SimplexCategory.δ i).op)) { dim := d + 1, simplex := y }.simplex =
    { dim := d, simplex := x }.simplex
⊢ ∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: case mpr
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
⊢ (∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x) →
    { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }

Tactic:
rintro ⟨i, h₁, h₂⟩
    refine ⟨rfl, SimplexCategory.δ i, ⟨inferInstance, h₁⟩, fun f ⟨h₃, h₄⟩ ↦ ?_⟩
    obtain ⟨j, rfl⟩ := SimplexCategory.eq_δ_of_mono f
    obtain rfl : j = i := h₂ _ h₄
    rfl

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

Goal state before:
pp: p q n : ℕ
z₁ z₂ : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
h : (↑z₁).1 = (↑z₂).1
hn : p + q = n
⊢ z₁ = z₂

Tactic:
by
  ext
  apply objEquiv.injective
  ext i : 3
  · exact DFunLike.congr_fun h i
  · have h₁ := z₁.2
    have h₂ := z₂.2
    rw [nonDegenerate_max_dim_iff] at h₁ h₂
    simpa only [orderHomOfSimplex_coe, h, Fin.ext_iff, add_right_inj]
      using! DFunLike.congr_fun (h₁.trans h₂.symm) i

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.PairingCore
inst✝ : P.IsProper
⊢ P.pairing.IsRegular ↔ Nonempty (P.RankFunction ℕ)

Tactic:
Pairing.isRegular_iff_nonempty_rankFunction

Goal state after:
X : SSet
A : X.Subcomplex
P : A.PairingCore
inst✝ : P.IsProper
⊢ Nonempty (P.pairing.RankFunction ℕ) ↔ Nonempty (P.RankFunction ℕ)
Module: Mathlib.CategoryTheory.Presentable.Retracts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalPresentable X κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this✝ : EssentiallySmall.{w, w, w} J
this : IsFiltered J
j : J
f₁ f₂ : Y ⟶ F.obj j
hf : f₁ ≫ c.ι.app j = f₂ ≫ c.ι.app j
k : J
u : j ⟶ k
hj : (h.r ≫ f₁) ≫ F.map u = (h.r ≫ f₂) ≫ F.map u
⊢ f₁ ≫ F.map u = f₂ ≫ F.map u

Tactic:
simpa [← cancel_epi h.r] using hj

Goal state after:
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.IsDense
⊢ F.leftKanExtensionUnit F ≫ F.whiskerLeft (leftKanExtensionIso F).hom = F.rightUnitor.inv

Tactic:
by
  simp [Functor.IsDense.leftKanExtensionIso]

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 ι
inst✝⁴ : P.IsProper
inst✝³ : SuccOrder ι
inst✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
⊢ IsLUB (Set.range ⋯.functor.obj) ⊤

Tactic:
rw [← f.iSup_filtration]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁵ : LinearOrder ι
f : P.RankFunction ι
inst✝⁴ : P.IsProper
inst✝³ : SuccOrder ι
inst✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
⊢ IsLUB (Set.range ⋯.functor.obj) (⨆ i, f.filtration i)
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: 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 sq₁₂.ι ⟶ Arrow.mk f₃
⊢ (fun β ↦
        Arrow.homMk
          (⋯.desc (adj₂.homEquiv.symm (Arrow.Hom.left β)) (adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.fst)) ⋯)
          (adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.snd)) ⋯)
      ((fun α ↦
          Arrow.homMk (adj₂.homEquiv (sq₁₂.inl ≫ Arrow.Hom.left α))
            (⋯.lift (adj₂.homEquiv (sq₁₂.inr ≫ Arrow.Hom.left α)) (adj₂.homEquiv (Arrow.Hom.right α)) ⋯) ⋯)
        α) =
    α

Tactic:
by
    ext
    · apply sq₁₂.isPushout.hom_ext <;> simp
    · simp

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 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₂
f : ⦋d⦌ ⟶ ⦋d + 1⦌
hf : Mono f
hδ :
  (ConcreteCategory.hom ((Δ[m + 1] ⊗ Δ[n]).map f.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
⊢ (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 := ⋯, index := it, isIndex := ht }.x ⋯).card

Tactic:
obtain ⟨i, rfl⟩ := SimplexCategory.eq_δ_of_mono f

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 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
⊢ (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 := ⋯, index := it, isIndex := ht }.x ⋯).card
Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism

Goal state before:
pp: X Y Z : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f✝ g : RelativeMorphism A B φ
C : Z.Subcomplex
ψ : B.toSSet ⟶ C.toSSet
f' g' : RelativeMorphism B C ψ
h : f'.Homotopy g'
f : RelativeMorphism A B φ
φψ : A.toSSet ⟶ C.toSSet
fac : φ ≫ ψ = φψ
⊢ A.ι ▷ Δ[1] ≫ f.map ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φψ ≫ C.ι

Tactic:
rw [← fac, Category.assoc, ← comp_whiskerRight_assoc, f.comm,
      comp_whiskerRight_assoc, h.rel, whiskerRight_fst_assoc]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n⦌
⊢ X.ιNormalizedChainComplex x ≫ (X.fromNormalizedChainComplex R).f n = X.ιChainComplex x ≫ PInfty.f n

Tactic:
dsimp [ιNormalizedChainComplex]
  rw [Category.assoc, toNormalizedChainComplex_f_fromNormalizedChainComplex_f]

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.succ.castSucc ≫ SimplexCategory.σ i.succ))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] i.succ.castSucc)) (stdSimplex.objMk₁ i.succ.castSucc.succ)).1 =
    ((ConcreteCategory.hom (X.map (stdSimplex.objEquiv (stdSimplex.objEquiv.symm (𝟙 ⦋n + 1⦌))).op)) x,
        (ConcreteCategory.hom (δ Δ[1] i.succ.castSucc)) (stdSimplex.objMk₁ i.castSucc.castSucc.succ)).1

Tactic:
SimplexCategory.δ_comp_σ_self

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 (𝟙 ⦋n + 1⦌))).op)) x,
        (ConcreteCategory.hom (δ Δ[1] i.succ.castSucc)) (stdSimplex.objMk₁ i.succ.castSucc.succ)).1 =
    ((ConcreteCategory.hom (X.map (stdSimplex.objEquiv (stdSimplex.objEquiv.symm (𝟙 ⦋n + 1⦌))).op)) x,
        (ConcreteCategory.hom (δ Δ[1] i.succ.castSucc)) (stdSimplex.objMk₁ i.castSucc.castSucc.succ)).1
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case h₁
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₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝ : Arrow C₃
⊢ Arrow.Hom.left
      ({
              app := fun X₂ ↦
                Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                  (pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                    (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj X₂).right))) ⋯)
                  ⋯,
              naturality := ⋯ }.app
          ((G.leibnizPullback.obj (op X₁)).obj x✝) ≫
        (G.leibnizPullback.obj (op X₁)).map
          ({
                app := fun X₃ ↦
                  Arrow.homMk
                    (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj X₃).left))
                      (adj₂.homEquiv.symm
                        (pullback.fst ((G.obj (op (unop (op X₁)).left)).map X₃.hom)
                          ((G.map (unop (op X₁)).hom.op).app X₃.right)))
                      ⋯)
                    (adj₂.homEquiv.symm
                      (pullback.snd ((G.obj (op (unop (op X₁)).left)).map X₃.hom)
                        ((G.map (unop (op X₁)).hom.op).app X₃.right)))
                    ⋯,
                naturality := ⋯ }.app
            x✝)) =
    Arrow.Hom.left (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝))

Tactic:
simp [← homEquiv_naturality_three]

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

Goal state before:
pp: ⊢ (monomorphisms SSet).IsStableUnderCobaseChange

Tactic:
change (monomorphisms (_ ⥤ _)).IsStableUnderCobaseChange
  rw [← functorCategory_monomorphisms]
  infer_instance

Goal state after: