mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ : J
h₁ : i₁ ∈ Set.Iic j
i₂ : J
h₂ : i₂ ∈ Set.Iic j
f : ⟨i₁, h₁⟩ ⟶ ⟨i₂, h₂⟩
⊢ (restrictionLE (extendToSucc hj F τ) ⋯).map f ≫ (extendToSuccObjIso hj F τ ↑⟨i₂, h₂⟩ ⋯).hom =
    (extendToSuccObjIso hj F τ ↑⟨i₁, h₁⟩ ⋯).hom ≫ F.map f

Tactic:
apply extendToSuccObjIso_hom_naturality

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
this : Arrow.mk ((Φ.iter (Order.succ j)).F.map (homOfLE ⋯)) = Φ.toSuccArrow ((Φ.iter (Order.succ j)).F.obj ⟨j, ⋯⟩)
⊢ Arrow.mk ((Φ.iterationFunctor J).map (homOfLE ⋯)) = Φ.toSuccArrow ((Φ.iterationFunctor J).obj j)

Tactic:
simp only [Φ.iterationFunctor_obj j (Φ.iter (Order.succ j)) (Order.le_succ j),
      Φ.arrowMk_iterationFunctor_map _ _ (Order.le_succ j) (Φ.iter (Order.succ j)) (by simp),
      this]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: case right
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
this✝² : LocallySmall.{w, v, u} C
this✝¹ : IsSmall.{w, v, u} I
this✝ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts C
X✝ Y✝ : Arrow C ⥤ Arrow C
f✝ : X✝ ⟶ Y✝
F : Arrow C ⥤ Arrow C
f : Arrow C
⊢ isomorphisms C (Arrow.Hom.right (((succStruct I κ).toSucc F).app f))

Tactic:
rw [MorphismProperty.isomorphisms.iff]

Goal state after:
case right
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
this✝² : LocallySmall.{w, v, u} C
this✝¹ : IsSmall.{w, v, u} I
this✝ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts C
X✝ Y✝ : Arrow C ⥤ Arrow C
f✝ : X✝ ⟶ Y✝
F : Arrow C ⥤ Arrow C
f : Arrow C
⊢ IsIso (Arrow.Hom.right (((succStruct I κ).toSucc F).app f))
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
s : ℕ
S' : Finset ℕ
Hnot : s ∉ S'
Hne : S'.Nonempty
Hind : (∀ i ∈ S', padicValRat p (F j) < padicValRat p (F i)) → padicValRat p (F j) < padicValRat p (∑ i ∈ S', F i)
hF : ∀ i ∈ Finset.cons s S' Hnot, padicValRat p (F j) < padicValRat p (F i)
i : ℕ
hi : i ∈ S'
⊢ i = s ∨ i ∈ S'

Tactic:
exact Or.inr hi

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case inl
p : ℕ
hp : p ≠ 1
n : ℕ
⊢ p ^ n ∣ 0 ↔ 0 = 0 ∨ n ≤ padicValNat p 0

Tactic:
exact iff_of_true (dvd_zero _) (Or.inl rfl)

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case pos
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : p ∣ a
⊢ padicValNat p a + p ≤ a

Tactic:
rcases dvd with ⟨k, hk⟩

Goal state after:
case pos
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
⊢ padicValNat p a + p ≤ a
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ ∀ (a b : ℤ_[p]), ‖a‖ < 1 → ‖b‖ < 1 → ‖a + b‖ < 1

Tactic:
exact fun x y => norm_lt_one_add

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
F : Sheaf J AddCommGrpCat
h : Limits.IsZero F
n : ℕ
⊢ Limits.IsZero ((functorH J n).obj F)

Tactic:
exact Functor.map_isZero (functorH J n) h

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ f ≈ 0 → f.norm = 0

Tactic:
intro h
    simp [norm, h]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))
hgen : N ≤ stationaryPoint hne
⊢ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne)) < ε

Tactic:
| inl hgen =>

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

Goal state before:
pp: case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop A.fst).len = (unop Δ).len
⊢ A.fst = Δ

Tactic:
← unop_inj_iff

Goal state after:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop A.fst).len = (unop Δ).len
⊢ unop A.fst = unop Δ
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : SimplicialObject C
s : X.Splitting
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
⊢ f = g

Tactic:
ext ⟨Δ⟩
  apply s.hom_ext'
  intro A
  induction Δ using SimplexCategory.rec with | _ n
  dsimp
  simp only [s.cofan_inj_comp_app, h]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ (PInfty.f n ≫
      (Γ₀.splitting X).desc (op ⦋n⦌) fun A ↦ 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) =
    PInfty.f n

Tactic:
convert! comp_id _

Goal state after:
case e'_2.e'_7
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ ((Γ₀.splitting X).desc (op ⦋n⦌) fun A ↦ 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) =
    𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌))
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
⊢ ∀ [IsIso (N₁.map f)], IsIso f

Tactic:
intro
    -- restating the result in a way that allows induction on the degree n
    suffices ∀ n : ℕ, IsIso (f.app (op ⦋n⦌)) by
      have : ∀ Δ : SimplexCategoryᵒᵖ, IsIso (f.app Δ) := fun Δ => this Δ.unop.len
      apply NatIso.isIso_of_isIso_app
    -- restating the assumption in a more practical form
    have h₁ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.hom_inv_id (N₁.map f)))
    have h₂ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.inv_hom_id (N₁.map f)))
    have h₃ := fun n =>
      Karoubi.HomologicalComplex.p_comm_f_assoc (inv (N₁.map f)) n (f.app (op ⦋n⦌))
    simp only [N₁_map_f, Karoubi.comp_f, HomologicalComplex.comp_f,
      AlternatingFaceMapComplex.map_f, N₁_obj_p, Karoubi.id_f, assoc] at h₁ h₂ h₃
    -- we have to construct an inverse to f in degree n, by induction on n
    intro n
    induction n with
    -- degree 0
    | zero =>
      use (inv (N₁.map f)).f.f 0
      have h₁₀ := h₁ 0
      have h₂₀ := h₂ 0
      dsimp at h₁₀ h₂₀
      simp only [id_comp] at h₁₀ h₂₀
      tauto
    | succ n hn =>
      use φ { a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1)
              b := fun i => inv (f.app (op ⦋n⦌)) ≫ X.σ i }
      simp only [MorphComponents.id, ← id_φ, ← preComp_φ, preComp, ← postComp_φ, postComp,
        PInfty_f_naturality_assoc, IsIso.hom_inv_id_assoc, assoc, IsIso.inv_hom_id_assoc,
        SimplicialObject.σ_naturality, h₁, h₂, h₃, and_self]

Goal state after:
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
n : ℕ
⊢ 𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = PInfty.f n ≫ s.πSummand (IndexSet.id (op ⦋n⦌))

Tactic:
rw [← sub_eq_zero, ← sub_comp, ← comp_PInfty_eq_zero_iff, sub_comp, id_comp, PInfty_f_idem,
    sub_self]

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
⊢ Γ₂N₂ToKaroubiIso.inv.app X ≫
      (Γ₂N₂.natTrans ≫ Γ₂N₂.hom).app ((toKaroubi (SimplicialObject C)).obj X) ≫
        Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X) =
    𝟙 (Γ₂.obj (N₁.obj X))

Tactic:
← Γ₂N₂_inv,

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₂ToKaroubiIso.inv.app X ≫
      (Γ₂N₂.inv ≫ Γ₂N₂.hom).app ((toKaroubi (SimplicialObject C)).obj X) ≫ Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X) =
    𝟙 (Γ₂.obj (N₁.obj X))
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
⊢ (ContinuousMap.id X).Nullhomotopic

Tactic:
obtain ⟨hv⟩ := ContractibleSpace.hequiv_unit X

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
hv : X ≃ₕ Unit
⊢ (ContinuousMap.id X).Nullhomotopic
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X ≃ₜ Y
s : Set Y
⊢ IsSimplyConnected (⇑f ⁻¹' s) ↔ IsSimplyConnected s

Tactic:
← image_symm,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X ≃ₜ Y
s : Set Y
⊢ IsSimplyConnected (⇑f.symm '' s) ↔ IsSimplyConnected s
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (PathConnectedSpace ↑s ∧ ∀ (x : ↑s) (γ : Path x x), γ.Homotopic (Path.refl x)) ↔
    IsPathConnected s ∧
      ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s

Tactic:
← isPathConnected_iff_pathConnectedSpace

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (IsPathConnected s ∧ ∀ (x : ↑s) (γ : Path x x), γ.Homotopic (Path.refl x)) ↔
    IsPathConnected s ∧
      ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (cofibrations C).HasFactorization (trivialFibrations C)
inst✝⁵ : HasPushouts C
inst✝⁴ : (cofibrations C).IsStableUnderComposition
inst✝³ : (cofibrations C).IsStableUnderCobaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (pushout.desc p g ⋯) :=
  (cofibrations C).factorizationData (trivialFibrations C) (pushout.desc p g ⋯)
sq' : CommSq (𝟙 X) (pushout.inl f i ≫ h.i) p h.p
h₁ : WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p)
h₂ : cofibrations C (pushout.inl f i ≫ h.i)
⊢ sq.HasLift

Tactic:
← cofibration_iff

Goal state after:
C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (cofibrations C).HasFactorization (trivialFibrations C)
inst✝⁵ : HasPushouts C
inst✝⁴ : (cofibrations C).IsStableUnderComposition
inst✝³ : (cofibrations C).IsStableUnderCobaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (pushout.desc p g ⋯) :=
  (cofibrations C).factorizationData (trivialFibrations C) (pushout.desc p g ⋯)
sq' : CommSq (𝟙 X) (pushout.inl f i ≫ h.i) p h.p
h₁ : WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p)
h₂ : Cofibration (pushout.inl f i ≫ h.i)
⊢ sq.HasLift
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ Λ[n, i] = ⨆ j, stdSimplex.face {↑j}ᶜ

Tactic:
ext m j
  simp [stdSimplex.face_obj, horn, Set.eq_univ_iff_forall]
  rfl

Goal state after:
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

Goal state after:
case pos
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)
h✝ : k = i
⊢ k ∈ Finset.image ⇑(SimplexCategory.Hom.toOrderHom f) ⊤ ∪ {i} ↔ k ∈ ⊤

case neg
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)
h✝ : ¬k = i
⊢ k ∈ Finset.image ⇑(SimplexCategory.Hom.toOrderHom f) ⊤ ∪ {i} ↔ k ∈ ⊤
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
⊢ stdSimplex.face S ≤ Λ[n + 1, j] ↔ S ≠ Finset.univ ∧ S ≠ {j}ᶜ

Tactic:
rw [subcomplex_le_horn_iff, stdSimplex.face_le_face_iff, ← not_iff_not]

Goal state after:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
⊢ ¬¬{j}ᶜ ⊆ S ↔ ¬(S ≠ Finset.univ ∧ S ≠ {j}ᶜ)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

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

Tactic:
exact Rel'.inl_inl _ _ h.symm

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝ : Cofibration f
⊢ Mono f

Tactic:
← cofibration_iff

Goal state after:
X Y : SSet
f : X ⟶ Y
inst✝ : Cofibration f
⊢ Cofibration f
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
i j : ℕ
h : i ≤ j
k : Fin i
x : ↑(X.nonDegenerate ↑k)
⊢ Subcomplex.ofSimplex ↑x ≤ ⨆ x, Subcomplex.ofSimplex ↑x

Tactic:
exact le_trans (by rfl) (le_iSup _ x)

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

Goal state before:
pp: case «0»
n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨0, ⋯⟩).succ

Tactic:
exact p.arrow_tgt 0

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

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp (𝟙 (𝟙 a)) η ≍ η

Tactic:
id_eq,

Goal state after:
C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp (𝟙 ((eId Cat a).toFunctor.obj { down := { as := () } })) η ≍ η
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp η (𝟙 (𝟙 b)) ≍ η

Tactic:
id_eq,

Goal state after:
C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp η (𝟙 ((eId Cat b).toFunctor.obj { down := { as := () } })) ≍ η
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝⁶ : Category.{v', u'} V
inst✝⁵ : MonoidalCategory V
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : EnrichedOrdinaryCategory V C
W : Type u''
inst✝² : Category.{v'', u''} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ((eHomEquiv V).trans (e (X✝ ⟶[V] Z✝))) (f ≫ g) =
    (λ_ (𝟙_ W)).inv ≫
      (((eHomEquiv V).trans (e (X✝ ⟶[V] Y✝))) f ⊗ₘ ((eHomEquiv V).trans (e (Y✝ ⟶[V] Z✝))) g) ≫ eComp W X✝ Y✝ Z✝

Tactic:
by
    dsimp +instances [instEnrichedCategoryTransportEnrichment]
    rw [h, h, h, ← tensorHom_comp_tensorHom_assoc, eComp_eq, tensorHom_def_assoc,
      whiskerRight_id_assoc, unitors_inv_equal, Iso.inv_hom_id_assoc,
      Functor.LaxMonoidal.μ_natural_assoc, Functor.LaxMonoidal.right_unitality_inv_assoc,
      eHomEquiv_comp, ← F.map_comp, ← F.map_comp, unitors_inv_equal]

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

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : ForgetEnrichment W (TransportEnrichment F D)
⊢ ForgetEnrichment.homOf V
      ((e (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)).symm (ForgetEnrichment.homTo W (𝟙 X))) =
    𝟙 (ForgetEnrichment.of V (ForgetEnrichment.to W X))

Tactic:
← ForgetEnrichment.homOf_eId

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
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : ForgetEnrichment W (TransportEnrichment F D)
⊢ ForgetEnrichment.homOf V
      ((e (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)).symm (ForgetEnrichment.homTo W (𝟙 X))) =
    ForgetEnrichment.homOf V (eId V (ForgetEnrichment.to W X))
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
⊢ forgetToQuiv.map ({ toPrefunctor := e.hom, map_id := h_id } ≫ { toPrefunctor := e.inv, map_id := ⋯ }) =
    forgetToQuiv.map (𝟙 (of V))

Tactic:
exact e.hom_inv_id

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

Goal state before:
pp: case comp_of
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f✝¹ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f✝ : X✝ ⟶ Y✝
x✝ y✝ z✝ : SimplexCategoryGenRel
f : x✝ ⟶ y✝
g : y✝ ⟶ z✝
hf : generators.multiplicativeClosure f
hg : generators g
hrec : P f
⊢ P (f ≫ g)

Tactic:
| comp_of f g hf hg hrec =>

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

Goal state before:
pp: case comp_δ
x y : SimplexCategoryGenRel
n n' : ℕ
f : mk n ⟶ mk n'
j : Fin (n' + 2)
h : ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f = e ≫ m
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ δ j = e ≫ m

Tactic:
| @comp_δ n n' f j h =>

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 ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
ha hb : 0 ≤ d
f : { obj := { len := 0 }, property := ha } ⟶ { obj := { len := 0 }, property := hb }
h : 0 + 0 = 0
i : Fin ({ obj := { len := 0 }, property := ha }.obj.len + 1)
⊢ (Hom.toOrderHom f.hom) i = (Hom.toOrderHom (𝟙 { obj := { len := 0 }, property := ha }).hom) i

Tactic:
apply Subsingleton.elim (α := Fin 1)

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
⊢ (k.pred ⋯).castSucc < i

Tactic:
Fin.castSucc_pred_lt_iff

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 ≤ i
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)
h : i.castSucc < (S.min' hS).castSucc
⊢ 0 = (ConcreteCategory.hom f) i

pp: 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

Tactic:
· have hi : i ∉ S := fun hi ↦ by have := S.min'_le _ hi; grind
      #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` -/
      simp [S] at hi; grind

Goal state after:
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 left
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
⊢ (Finset.image f s').Nonempty

Tactic:
exact Finset.image_nonempty.mpr (K.isRelLowerSet_faces hs').1

Goal state after: