mathlib-initiative/mathlib-tactics huggingface dataset:
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
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ PInfty.f (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0

Tactic:
by_cases hj₁ : j₁ = 0

Goal state after:
case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : j₁ = 0
⊢ PInfty.f (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0

case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
⊢ PInfty.f (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0
Module: Mathlib.Combinatorics.Quiver.ReflQuiver

Goal state before:
pp: V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
F G : ReflPrefunctor V W
h_obj : ∀ (X : V), F.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ F = G

Tactic:
obtain ⟨Fpre, Fid⟩ := F

Goal state after:
V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
G : ReflPrefunctor V W
Fpre : V ⥤q W
Fid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
h_obj : ∀ (X : V), { toPrefunctor := Fpre, map_id := Fid }.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), { toPrefunctor := Fpre, map_id := Fid }.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ { toPrefunctor := Fpre, map_id := Fid } = G
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
⊢ { f := { f := fun n ↦ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n, comm' := ⋯ }, comm := ⋯ } ≫
      { f := { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ } =
    𝟙 ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex)

Tactic:
ext n
    simp only [assoc, PInfty_comp_πSummand_id, Karoubi.comp_f, HomologicalComplex.comp_f,
      cofan_inj_πSummand_eq_id]
    rfl

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
⊢ IsIso Γ₂N₂.natTrans

Tactic:
by
  have : ∀ P : Karoubi (SimplicialObject C), IsIso (Γ₂N₂.natTrans.app P) := by
    intro P
    have : IsIso (N₂.map (Γ₂N₂.natTrans.app P)) := by
      have h := identity_N₂_objectwise P
      dsimp only [Functor.id_obj, Functor.comp_obj] at h
      rw [hom_comp_eq_id] at h
      rw [h]
      infer_instance
    exact isIso_of_reflects_iso _ N₂
  apply NatIso.isIso_of_isIso_app

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: G : Type u
inst✝ : Group G
x y : SingleObj G
f : x ⟶ y
⊢ 1 = 𝟙 x

Tactic:
id_as_one

Goal state after:
G : Type u
inst✝ : Group G
x y : SingleObj G
f : x ⟶ y
⊢ 1 = 1
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X✝ Y✝ X Y Z : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ map ▷ I ≫ Homotopy.h (F.fst.trans G.fst) = Homotopy.h (F.snd.trans G.snd) ≫ map

Tactic:
ext ⟨_, _⟩

Goal state after:
X✝ Y✝ X Y Z : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
fst✝ : ↑TopPair.snd
snd✝ : ↑I
⊢ (ConcreteCategory.hom (map ▷ I ≫ Homotopy.h (F.fst.trans G.fst))) (fst✝, snd✝) =
    (ConcreteCategory.hom (Homotopy.h (F.snd.trans G.snd) ≫ map)) (fst✝, snd✝)
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: F : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
f g : f₀.Homotopy f₁
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
    obtain ⟨⟨_, _⟩, _⟩ := g
    congr

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

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ Limits.PreservesLimit (Discrete.functor X) π

Tactic:
apply Limits.preservesLimit_of_preserves_limit_cone (TopCat.piFanIsLimit X)
  apply (Limits.IsLimit.ofConeEquiv (coneDiscreteComp X)).toFun
  simp only [coneDiscreteComp_obj_mapCone]
  apply Limits.IsLimit.ofIsoLimit _ (asIso (piTopToPiCone X)).symm
  exact Grpd.piLimitFanIsLimit _

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

Goal state before:
pp: case mpr
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ (ContinuousMap.id Y).Nullhomotopic → ContractibleSpace Y

Tactic:
rintro ⟨p, h⟩

Goal state after:
case mpr
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : (ContinuousMap.id Y).Homotopic (const Y p)
⊢ ContractibleSpace Y
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
h : PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ SimplyConnectedSpace Y

Tactic:
by
    cases h; rw [simply_connected_iff_unique_homotopic]
    exact ⟨inferInstance, fun x y => ⟨uniqueOfSubsingleton ⟦PathConnectedSpace.somePath x y⟧⟩⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Homotopic.Quotient x y
⊢ γ.cast ⋯ ⋯ = γ

Tactic:
induction γ using Quotient.ind with

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Homotopic.Quotient x y
x' y' : X
hx : x' = x
hy : y' = y
x'' y'' : X
hx' : x'' = x'
hy' : y'' = y'
⊢ (γ.cast hx hy).cast hx' hy' = γ.cast ⋯ ⋯

Tactic:
induction γ using Quotient.ind with

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

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
hx : 2⁻¹ < ↑x
this : p.extend (2 - 2 * ↑x) = p.extend (1 - (2 * ↑x - 1))
⊢ p ⟨if ↑x ≤ 1 / 2 then ↑1 * 2 * ↑x else ↑1 * (2 - 2 * ↑x), ⋯⟩ =
    { toFun := (fun t ↦ if t ≤ 1 / 2 then p.extend (2 * t) else p.symm.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯ }
      x

Tactic:
simpa [hx.not_ge, ← extend_apply]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
X₁ X₂ X₃ X₄ : Over S
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : CommSq t l r b
inst✝ : ⋯.HasLift
sq' : CommSq (Over.Hom.left t) (Over.Hom.left l) (Over.Hom.left r) (Over.Hom.left b) := map (Over.forget S) sq
⊢ sq'.lift ≫ X₂.hom = X₃.hom

Tactic:
rw [← Over.w b, ← sq'.fac_right_assoc, Over.w r]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence X.iBifibrantResolutionObj

Tactic:
rw [weakEquivalence_iff_of_objectProperty]
  infer_instance

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
γ : Homotopic.Quotient x₀ x₁
⊢ (refl x₀).trans γ = γ

Tactic:
induction γ using Quotient.ind with

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
γ : Homotopic.Quotient x₀ x₁
⊢ γ.trans (refl x₁) = γ

Tactic:
induction γ using Quotient.ind with

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
γ : Homotopic.Quotient x₀ x₁
⊢ γ.trans γ.symm = refl x₀

Tactic:
induction γ using Quotient.ind with

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
γ : Homotopic.Quotient x₀ x₁
⊢ γ.symm.trans γ = refl x₁

Tactic:
induction γ using Quotient.ind with

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

Goal state before:
pp: case mp
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
⊢ c.IsColimit →
    (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
        c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
          d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
            d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
      ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x

Tactic:
intro hc

Goal state after:
case mp
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
⊢ (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
      c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
        d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
          d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
    ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this : ∀ (j : Fin (n + 1)), j ≠ i → j ∈ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)
k : Fin (⦋n⦌.len + 1)
⊢ k ∈ Finset.image ⇑(SimplexCategory.Hom.toOrderHom f) ⊤ ∪ {i} ↔ k ∈ ⊤

Tactic:
by_cases k = i <;> aesop

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

Goal state before:
pp: m n : ℕ
h : m < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ stdSimplex.objEquiv.symm f ∈ ∂Δ[n].obj (op ⦋m⦌)

Tactic:
obtain _ | n := n

Goal state after:
case zero
m : ℕ
h : m < 0
f : unop (op ⦋m⦌) ⟶ ⦋0⦌
⊢ stdSimplex.objEquiv.symm f ∈ ∂Δ[0].obj (op ⦋m⦌)

case succ
m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
⊢ stdSimplex.objEquiv.symm f ∈ ∂Δ[n + 1].obj (op ⦋m⦌)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mk.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
m : Pushout f g ⟶ s.pt
h₁ : inl f g ≫ m = s.inl
h₂ : inr f g ≫ m = s.inr
x✝ : Pushout f g
x₂ : X₂
⊢ (ConcreteCategory.hom m).toFun (Quot.mk (Rel f g) (Sum.inr x₂)) =
    (ConcreteCategory.hom
          (↾Quot.lift
              (fun x ↦
                match x with
                | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
                | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂)
              ⋯)).toFun
      (Quot.mk (Rel f g) (Sum.inr x₂))

Tactic:
exact ConcreteCategory.congr_hom h₂ x₂

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₁)

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:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ J Λ[n, i].ι

Tactic:
obtain _ | n := n

Goal state after:
case zero
inst✝ : NeZero 0
i : Fin (0 + 1)
⊢ J Λ[0, i].ι

case succ
n : ℕ
inst✝ : NeZero (n + 1)
i : Fin (n + 1 + 1)
⊢ J Λ[n + 1, i].ι
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ Fibration f ↔ J.rlp f

Tactic:
rw [HomotopicalAlgebra.fibration_iff]
  rfl

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

Goal state before:
pp: S : SSet
inst✝ : S.Quasicategory
n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
σ₀ : Λ[n, i].toSSet ⟶ S
⊢ ∃ σ, σ₀ = Λ[n, i].ι ≫ σ

Tactic:
by
  match n with
  | 0
  | 1 => lia
  | n + 2 => exact Quasicategory.hornFilling' σ₀ h0 hn

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

Goal state before:
pp: n : ℕ
X : SSet
i : Fin (n + 2)
g : Λ[n + 1, i].toSSet ⟶ X
⊢ horn.IsCompatible fun j hj ↦ ι i j hj ≫ g

Tactic:
obtain _ | n := n

Goal state after:
case zero
X : SSet
i : Fin (0 + 2)
g : Λ[0 + 1, i].toSSet ⟶ X
⊢ horn.IsCompatible fun j hj ↦ ι i j hj ≫ g

case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
⊢ horn.IsCompatible fun j hj ↦ ι i j hj ≫ g
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: n : ℕ
X : SSet
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
⊢ ∀ (a : (MultispanShape.ofLinearOrder ↑{i}ᶜ).L),
    (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).fst a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj) =
      ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).snd a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj

Tactic:
obtain _ | n := n

Goal state after:
case zero
X : SSet
i : Fin (0 + 2)
f : (j : Fin (0 + 2)) → j ≠ i → (Δ[0] ⟶ X)
hf : horn.IsCompatible f
⊢ ∀ (a : (MultispanShape.ofLinearOrder ↑{i}ᶜ).L),
    (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).fst a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj) =
      ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).snd a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj

case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
f : (j : Fin (n + 1 + 2)) → j ≠ i → (Δ[n + 1] ⟶ X)
hf : horn.IsCompatible f
⊢ ∀ (a : (MultispanShape.ofLinearOrder ↑{i}ᶜ).L),
    (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).fst a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj) =
      ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).snd a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
⊢ f = g

Tactic:
ext ⟨⟨m, hm⟩⟩ x

Goal state after:
n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
m : SimplexCategory
hm : m.len ≤ n + 1
x : X.obj (op { obj := m, property := hm })
⊢ (ConcreteCategory.hom (f.app (op { obj := m, property := hm }))).toFun x =
    (ConcreteCategory.hom (g.app (op { obj := m, property := hm }))).toFun x
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inr
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
obtain _ | n := n

Goal state after:
case h.inr.inr.zero
X : SSet
sx : X.StrictSegal
i : Fin (0 + 3)
σ₀ : Λ[0 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (0 + 2)
j : Fin (0 + 3)
hj : j ≠ i
k : Fin (0 + 1)
ksucc : Fin (0 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
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 : i.castSucc < j
⊢ f.vertex (j.succAbove i) = f.vertex i.castSucc

Tactic:
rw [Fin.succAbove_of_castSucc_lt j i h]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| ((λ_ (𝟙_ C)).inv ≫ (f ⊗ₘ g) ⊗ₘ h) ≫ (α_ X Y Z).hom

Tactic:
rw [← Category.id_comp h, ← tensorHom_comp_tensorHom, Category.assoc, associator_naturality,
          ← Category.assoc, unitors_inv_equal, tensorHom_id, triangle_assoc_comp_right_inv]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| 𝟙_ C ◁ (λ_ (𝟙_ C)).inv ≫ (f ⊗ₘ g ⊗ₘ h)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a : CatEnrichedOrdinary C
⊢ homEquiv (𝟙 a) = 𝟙 a.toBase

Tactic:
by
  unfold homEquiv
  simp only [Equiv.trans_apply]
  rw [eHomEquiv_id]
  rfl

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
X Y Z Z' : C
g : Z ⟶ Z'
⊢ eComp V X Y Z ≫ (ρ_ (X ⟶[V] Z)).inv ≫ (X ⟶[V] Z) ◁ (eHomEquiv V) g ≫ eComp V X Z Z' =
    (X ⟶[V] Y) ◁ ((ρ_ (Y ⟶[V] Z)).inv ≫ (Y ⟶[V] Z) ◁ (eHomEquiv V) g ≫ eComp V Y Z Z') ≫ eComp V X Y Z'

Tactic:
rightUnitor_inv_naturality_assoc,

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z Z' : C
g : Z ⟶ Z'
⊢ (ρ_ ((X ⟶[V] Y) ⊗ Y ⟶[V] Z)).inv ≫ eComp V X Y Z ▷ 𝟙_ V ≫ (X ⟶[V] Z) ◁ (eHomEquiv V) g ≫ eComp V X Z Z' =
    (X ⟶[V] Y) ◁ ((ρ_ (Y ⟶[V] Z)).inv ≫ (Y ⟶[V] Z) ◁ (eHomEquiv V) g ≫ eComp V Y Z Z') ≫ eComp V X Y Z'
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
v w : ReflQuiv
f : v ⟶ w
⊢ ((ReflQuiv.forgetToQuiv ⋙ free).map f ≫ (FreeRefl.quotientFunctor ↑w).toCatHom).toFunctor =
    ((FreeRefl.quotientFunctor ↑v).toCatHom ≫ freeRefl.map f).toFunctor

Tactic:
exact Paths.ext_functor (V := Quiv.of v) (by cat_disch) (by cat_disch)

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

Goal state before:
pp: X✝ Y✝ : SemiSimplexCategory
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : toSimplexCategory.map a₁✝ = toSimplexCategory.map a₂✝
x✝ : Fin (X✝.len + 1)
⊢ (homEquiv a₁✝) x✝ = (homEquiv a₂✝) x✝

Tactic:
apply ConcreteCategory.congr_hom h

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

Goal state before:
pp: case refine_2
α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsRelUpperSet (Subtype.val '' s) P
a b : { x // P x }
x : a ≤ b
y : a ∈ s
ma : ↑a ∈ Subtype.val '' s
⊢ b ∈ s

Tactic:
simpa only [mem_image, Subtype.coe_inj, exists_eq_right] using (h ma).2 x b.2

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

Goal state before:
pp: case refine_2
α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsRelLowerSet (Subtype.val '' s) P
a b : { x // P x }
x : b ≤ a
y : a ∈ s
ma : ↑a ∈ Subtype.val '' s
⊢ b ∈ s

Tactic:
simpa only [mem_image, Subtype.coe_inj, exists_eq_right] using (h ma).2 x b.2

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

Goal state before:
pp: case pos
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ (if i.castSucc < (S.min' hS).castSucc then 0 else 1) = (ConcreteCategory.hom f) i

Tactic:
split_ifs with h

Goal state after:
case pos
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
h : i.castSucc < (S.min' hS).castSucc
⊢ 0 = (ConcreteCategory.hom f) i

case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
h : ¬i.castSucc < (S.min' hS).castSucc
⊢ 1 = (ConcreteCategory.hom f) i
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ ∀ ⦃b : Finset ι⦄, b ⊆ x → b.Nonempty → b ∈ {s | ∃ v, s = {v}}

Tactic:
· intro t hts ht
        cases Finset.subset_singleton_iff.mp (hv ▸ hts) with
        | inl h => exact (ht.ne_empty h).elim
        | inr h => exact ⟨v, h⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case left.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₁.len + 1)
h : Fin.castAdd (x₂.len + 1) i✝¹ ≤ Fin.castAdd (x₂.len + 1) i✝
⊢ (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      (Fin.castAdd (x₂.len + 1) i✝¹) ≤
    (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      (Fin.castAdd (x₂.len + 1) i✝)

Tactic:
rw [Fin.le_def] at h ⊢

Goal state after:
case left.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₁.len + 1)
h : ↑(Fin.castAdd (x₂.len + 1) i✝¹) ≤ ↑(Fin.castAdd (x₂.len + 1) i✝)
⊢ ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.castAdd (x₂.len + 1) i✝¹)) ≤
    ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.castAdd (x₂.len + 1) i✝))