mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X✝ : C
x : F.obj X✝
X : (fromOverFunctor F x).Elements
⊢ { obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
            map := fun {X Y} f ↦
              Over.homMk
                (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                  (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                  (Over.Hom.left ↑f) ⋯)
                ⋯,
            map_id := ⋯, map_comp := ⋯ }.map
        ((Iso.refl (𝟭 (fromOverFunctor F x).Elements)).hom.app X) ≫
      (Iso.refl
              ({ obj := fun u ↦ (fromOverFunctor F x).elementsMk (Over.mk ↑u.hom) ⟨u.left.snd, ⋯⟩,
                  map := fun {X Y} f ↦
                    homMk ((fromOverFunctor F x).elementsMk (Over.mk ↑X.hom) ⟨X.left.snd, ⋯⟩)
                      ((fromOverFunctor F x).elementsMk (Over.mk ↑Y.hom) ⟨Y.left.snd, ⋯⟩)
                      (Over.homMk ↑(Over.Hom.left f) ⋯) ⋯,
                  map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
                  map := fun {X Y} f ↦
                    Over.homMk
                      (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                        (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                        (Over.Hom.left ↑f) ⋯)
                      ⋯,
                  map_id := ⋯, map_comp := ⋯ })).hom.app
        ({ obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
              map := fun {X Y} f ↦
                Over.homMk
                  (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                    (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                    (Over.Hom.left ↑f) ⋯)
                  ⋯,
              map_id := ⋯, map_comp := ⋯ }.obj
          X) =
    𝟙
      ({ obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
            map := fun {X Y} f ↦
              Over.homMk
                (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                  (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                  (Over.Hom.left ↑f) ⋯)
                ⋯,
            map_id := ⋯, map_comp := ⋯ }.obj
        X)

Tactic:
simp_all

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X✝ : C
x : F.obj X✝
X : (fromOverFunctor F x).Elements
⊢ Over.homMk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X.fst.left ↑X.snd) (𝟙 X.fst.left) ⋯) ⋯ =
    𝟙 (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯))
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝⁸ : Category.{v', u'} A
inst✝⁷ : LocallySmall.{w, v, u} C
inst✝⁶ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁵ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory A FC
inst✝³ : (forget A).ReflectsIsomorphisms
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
hJ : J.HasSheafCompose (forget A)
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝¹ : HasWeakSheafify J A
inst✝ : HasProducts A
⊢ J.W f ↔ ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map f)

Tactic:
rw [GrothendieckTopology.W_iff, (hP.jointlyReflectIsomorphisms A).isIso_iff]
  exact forall_congr'
    (fun Φ ↦ (MorphismProperty.isomorphisms A).arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso
        (Φ.obj.presheafToSheafCompSheafFiberIso A)).app (Arrow.mk f)))

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:
exact hN _ hgen _ hi

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
⊢ ∃ q', ‖q‖ = ↑q'

Tactic:
exact if h : q = 0 then ⟨0, by simp [h]⟩
  else
    let ⟨n, hn⟩ := padicNormE.image h
    ⟨_, hn⟩

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑p‖ * 1 < 1

Tactic:
rw [mul_one, norm_p]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ (↑p)⁻¹ < 1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ⇑padicNormE ↑f
q : ℚ_[p]
hq : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ↑ε' ∧ ↑ε' < ε
⊢ ∃ i, ∀ j ≥ i, ‖↑(f - const norm q) j‖ < ε

Tactic:
norm_cast at hε'

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ⇑padicNormE ↑f
q : ℚ_[p]
hq : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ ↑ε' < ε
⊢ ∃ i, ∀ j ≥ i, ‖↑(f - const norm q) j‖ < ε
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
⊢ addValuation x = ↑x.valuation

Tactic:
simp only [Padic.addValuation, AddValuation.of_apply, addValuationDef, if_neg hx]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).factorThru (PInfty.f (n + 1)) ⋯ ≫
      (NormalizedMooreComplex.objX X (n + 1)).arrow ≫ ((alternatingFaceMapComplex A).obj X).d (n + 1) n =
    K[X].d (n + 1) n ≫ PInfty.f n

Tactic:
factorThru_arrow_assoc,

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ PInfty.f (n + 1) ≫ ((alternatingFaceMapComplex A).obj X).d (n + 1) n = K[X].d (n + 1) n ≫ PInfty.f n
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac : A.e ≫ 𝟙 (unop A.fst) = (𝟙 Δ).unop ≫ A.e
⊢ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ A) { as := A } ≫ 𝟙 (∐ fun A ↦ Obj.summand K Δ A)

Tactic:
rw [comp_id]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac : A.e ≫ 𝟙 (unop A.fst) = (𝟙 Δ).unop ≫ A.e
⊢ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ A) { as := A }
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
K : ChainComplex C ℕ
n : ℕ
⊢ K.d (n + 1) n = K.d (n + 1) n ≫ 𝟙 (K.X n)

Tactic:
rw [comp_id]

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 ℕ
inst✝¹ : HasFiniteCoproducts C
Δ Δ' : SimplexCategory
e : Δ' ⟶ Δ
inst✝ : Epi e
⊢ ((splitting K).cofan (op Δ)).inj (Splitting.IndexSet.id (op Δ)) ≫ (obj K).map e.op =
    ((splitting K).cofan (op Δ')).inj (Splitting.IndexSet.mk e)

Tactic:
simpa only [Γ₀.Obj.map_on_summand K (Splitting.IndexSet.id (op Δ)) e.op
      (rfl : e ≫ 𝟙 Δ = e ≫ 𝟙 Δ),
    Γ₀.Obj.Termwise.mapMono_id] using! id_comp _

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 : ℕ
⊢ s.πSummand (IndexSet.id (op ⦋n⦌)) ≫ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n =
    ∑ j, (s.πSummand j ≫ (s.cofan (op ⦋n⦌)).inj j) ≫ PInfty.f n

Tactic:
rw [Fintype.sum_eq_single (IndexSet.id (op ⦋n⦌)), assoc]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ ∀ (x : IndexSet (op ⦋n⦌)), x ≠ IndexSet.id (op ⦋n⦌) → (s.πSummand x ≫ (s.cofan (op ⦋n⦌)).inj x) ≫ PInfty.f n = 0
Module: Mathlib.AlgebraicTopology.EilenbergSteenrod

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Limits.HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
HP✝ HP'✝ HP HP' X✝¹ Y✝¹ : HomologyPretheory C c
e : X✝¹ ≅ Y✝¹
x✝¹ : isHomotopyInvariant C c X✝¹
X✝ Y✝ : TopPair
f✝ g✝ : X✝ ⟶ Y✝
F : Homotopy f✝ g✝
x✝ : ι
⊢ (Y✝¹.Hₚ x✝).map f✝ = (Y✝¹.Hₚ x✝).map g✝

Tactic:
by
    simp only [← cancel_epi ((e.hom.homₚ _).app _), ← NatTrans.naturality,
      map_eq_of_homotopy _ F _]

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

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

Tactic:
intro ⟨hpc, hloops⟩
    refine ⟨hpc, fun {x y} p₁ p₂ => ?_⟩
    -- Work in the quotient where structural steps can be done by simp
    rw [← eq]
    replace hloops : ∀ (x : Y) (γ : Path x x),
        (⟦γ⟧ : Path.Homotopic.Quotient x x) = ⟦Path.refl x⟧ :=
      fun x γ => Quotient.sound (hloops x γ)
    have h : trans ⟦p₁⟧ (symm ⟦p₂⟧) = refl x := by
      simpa using hloops x (p₁.trans p₂.symm)
    calc ⟦p₁⟧
      _ = trans (trans ⟦p₁⟧ (symm ⟦p₂⟧)) ⟦p₂⟧ := by simp
      _ = ⟦p₂⟧ := by grind

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (cofibrations C).HasFactorization (trivialFibrations C)
⊢ (trivialCofibrations Cᵒᵖ).HasFactorization (fibrations Cᵒᵖ)

Tactic:
rw [trivialCofibrations_op, fibrations_op, ]
  infer_instance

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

Goal state before:
pp: 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
⊢ m =
    ↾Quot.lift
        (fun x ↦
          match x with
          | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
          | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂)
        ⋯

Tactic:
by
      ext ⟨x₁ | x₂⟩
      · exact ConcreteCategory.congr_hom h₁ x₁
      · exact ConcreteCategory.congr_hom h₂ x₂

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

Goal state before:
pp: case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
x₂ : X₂
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) → ∃ s, x₁ = (ConcreteCategory.hom f) s ∧ x₂ = (ConcreteCategory.hom g) s

pp: case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
x₂ : X₂
⊢ (∃ s, x₁ = (ConcreteCategory.hom f) s ∧ x₂ = (ConcreteCategory.hom g) s) → Rel' f g (Sum.inl x₁) (Sum.inr x₂)

Tactic:
· rintro ⟨_⟩
    exact ⟨_, rfl, rfl⟩

Goal state after:
case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
x₂ : X₂
⊢ (∃ s, x₁ = (ConcreteCategory.hom f) s ∧ x₂ = (ConcreteCategory.hom g) s) → Rel' f g (Sum.inl x₁) (Sum.inr x₂)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
a b : X₁ ⊕ X₂
⊢ Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Rel' f g a b

Tactic:
← (equivalence_rel' f g).quot_mk_eq_iff

Goal state after:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
a b : X₁ ⊕ X₂
⊢ Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Quot.mk (Rel' f g) a = Quot.mk (Rel' f g) b
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
i j : ℕ
h : i ≤ j
⊢ (fun n ↦ ⨆ i, ⨆ x, Subcomplex.ofSimplex ↑x) i ≤ (fun n ↦ ⨆ i, ⨆ x, Subcomplex.ofSimplex ↑x) j

Tactic:
simp only [iSup_le_iff]
    intro k x
    exact le_trans (by exact le_trans (by rfl) (le_iSup _ x))
      (le_iSup _ ⟨k, by lia⟩)

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

Goal state before:
pp: case inl.inl
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)
x₂ y₂ : X₂
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom r) x₂) = (ConcreteCategory.hom k) ((ConcreteCategory.hom r) y₂)
⊢ (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom r) y₂

Tactic:
obtain rfl : x₂ = y₂ := hr' eq
    rfl

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

Goal state before:
pp: n : ℕ
X : SSet
i : Fin (n + 2)
f g : Λ[n + 1, i].toSSet ⟶ X
h : ∀ (j : Fin (n + 2)) (hj : j ≠ i), ι i j hj ≫ f = ι i j hj ≫ g
⊢ f = g

Tactic:
refine Multicofork.IsColimit.hom_ext (isColimit i) (fun ⟨j, hj⟩ ↦ ?_)
  simpa only [faceSingletonComplIso_inv_ι_assoc] using!
    (stdSimplex.faceSingletonComplIso j).inv ≫= h j hj

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

Goal state before:
pp: case refine_1
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
c : Cell i d
y : Δ[d] _⦋n⦌
hx : (ConcreteCategory.hom (c.map.app (op ⦋n⦌))) y ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ y ∈ (((skeletonOfMono i) d).preimage c.map).obj (op ⦋n⦌)

Tactic:
Subcomplex.preimage_obj,

Goal state after:
case refine_1
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
c : Cell i d
y : Δ[d] _⦋n⦌
hx : (ConcreteCategory.hom (c.map.app (op ⦋n⦌))) y ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ y ∈ ⇑(ConcreteCategory.hom (c.map.app (op ⦋n⦌))) ⁻¹' ((skeletonOfMono i) d).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case «1»
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.δ 1) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨1, ⋯⟩).castSucc

Tactic:
exact (q.arrow_src 0).trans h.symm

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

Goal state before:
pp: case hᵥ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin (l + 1)
⊢ (X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ)).vertex i =
    ((X.spine m hₘ Δ).interval j l h).vertex i

Tactic:
dsimp only [spine_vertex, Path.interval]
    rw [← Functor.map_comp_apply, ← op_comp, ← tr_comp,
      const_subinterval_eq]

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

Goal state before:
pp: case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin l
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ ⋯).op))
      ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ) =
    Path.arrow
      { vertex := fun i ↦ (X.spine m hₘ Δ).vertex ⟨j + ↑i, ⋯⟩,
        arrow := fun i ↦ (ConcreteCategory.hom (X.map (tr (mkOfSucc ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ, arrow_src := ⋯,
        arrow_tgt := ⋯ }
      i

Tactic:
rw [← Functor.map_comp_apply, ← op_comp, ← tr_comp,
      mkOfSucc_subinterval_eq]

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 : a✝ ⟶ b✝
g : b✝ ⟶ c✝
⊢ (eqToIso ⋯).hom ≫ hComp (𝟙 f) (eqToIso ⋯).hom = hComp (eqToIso ⋯).hom (𝟙 g)

Tactic:
by
    generalize_proofs h1 h2 h3; revert h1 h2 h3
    generalize 𝟙 _ ≫ g = g, f ≫ 𝟙 _ = f
    rintro _ rfl rfl; 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:
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 : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp (𝟙 (𝟙 a)) η ≍ η

Tactic:
simp [id_hComp]

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 : CatEnrichedOrdinary C} {f g : a ⟶ b} (η : f ⟶ g), hComp (𝟙 (𝟙 a)) η = (eqToIso ⋯).hom ≫ η ≫ (eqToIso ⋯).inv

Tactic:
simp [id_hComp]

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

Goal state before:
pp: S T : Truncated 2
f : S ⟶ T
x : OneTruncation₂ S
⊢ Truncated.Edge.map (𝟙rq x) f = 𝟙rq ((ConcreteCategory.hom (f.app (op { obj := ⦋0⦌, property := _proof_1 }))) x)

Tactic:
ext; simp [← NatTrans.naturality_apply, reflQuiver_id]

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

Goal state before:
pp: V : Truncated 2
x₀ x₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e' : Edge x₀ y₁
h : e.edge = e'.edge
⊢ (ConcreteCategory.hom (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op)) e.edge = y₁

Tactic:
← e'.tgt_eq,

Goal state after:
V : Truncated 2
x₀ x₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e' : Edge x₀ y₁
h : e.edge = e'.edge
⊢ (ConcreteCategory.hom (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op)) e.edge =
    (ConcreteCategory.hom (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op)) e'.edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x y : V.HomotopyCategory
f : x.as ⟶ y.as
x✝ : ⊤ ((quotientFunctor V).map f)
⊢ (morphismPropertyHomMk V).multiplicativeClosure ((quotientFunctor V).map f)

Tactic:
morphismPropertyHomMk_eq_strictMap

Goal state after:
V : Truncated 2
x y : V.HomotopyCategory
f : x.as ⟶ y.as
x✝ : ⊤ ((quotientFunctor V).map f)
⊢ ((Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).strictMap (quotientFunctor V)).multiplicativeClosure
    ((quotientFunctor V).map f)
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f f' : Edge x y
g g' : Edge y z
h h' : Edge x z
s : f.CompStruct g h
s' : f'.CompStruct g' h'
hf : HomotopicL f f'
hg : HomotopicL g g'
⊢ HomotopicL h h'

Tactic:
by
  rcases hg.homotopicR with ⟨hg⟩
  rcases hf with ⟨hf⟩
  let ⟨s₁⟩ := Quasicategory₂.fill32 hf (idComp g') s'
  let ⟨s₂⟩ := Quasicategory₂.fill31 (compId f) hg s₁
  exact Quasicategory₂.fill31 s (compId g) s₂

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

Goal state before:
pp: case inl.inr
n : ℕ
i : Fin (n + 2)
h : i.succ ≤ i.succ
⊢ δ i.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i.succ ≫ σ i = σ j ≫ δ j'

Tactic:
exact Or.inl δ_comp_σ_succ

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ homMk (Edge.id y) ≫
      𝟙
        (mk
          ((ConcreteCategory.hom
              (snd (X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
                (Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))))
            (x₁, y))) =
    𝟙
      (mk
        ((ConcreteCategory.hom
            (snd (X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
              (Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))))
          (x₀, y)))

Tactic:
exact homMk_id y

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

Goal state before:
pp: case mk.mk.zero
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 ⋯ ⋯)
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = 0
⊢ W f

Tactic:
obtain rfl : a = 0 := by lia

Goal state after:
case mk.mk.zero
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 ⋯ ⋯)
b : ℕ
hb : b ≤ d
ha : 0 ≤ d
f : { obj := { len := 0 }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : 0 + b = 0
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg.«_@».Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne.3003013004._hygCtx._hyg.53.«0»
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
hj : (ConcreteCategory.hom f) i = (fun i ↦ i) ⟨0, ⋯⟩
⊢ 0 = (ConcreteCategory.hom f) i

Tactic:
simp_all

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

Goal state before:
pp: case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
⊢ (∀ i < y, (f i).castSucc < x) → ∀ b ∈ finset f x, y.castSucc ≤ b

Tactic:
· intro h' i hi
    obtain ⟨i, rfl⟩ | rfl := i.eq_castSucc_or_eq_last
    · simp only [Fin.castSucc_le_castSucc_iff]
      by_contra!
      exact (h' i this).not_ge (by simpa using hi)
    · apply Fin.le_last

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

Goal state before:
pp: x✝ y z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y ⟶ z✝
x z : SimplexCategory
f g : WithInitial.of x ⊗ WithInitial.star ⟶ WithInitial.of z
h₁ : inl (WithInitial.of x) WithInitial.star ≫ f = inl (WithInitial.of x) WithInitial.star ≫ g
h₂ : inr (WithInitial.of x) WithInitial.star ≫ f = inr (WithInitial.of x) WithInitial.star ≫ g
⊢ f = g

Tactic:
by
      simp only [inl, Category.assoc, Iso.cancel_iso_inv_left, Limits.IsInitial.to_self,
        whiskerLeft_id_star] at h₁
      simpa [Category.id_comp f, Category.id_comp g] using h₁

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

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
Y : SSet
e : X ≅ Y
d : ℕ
hd : x.dim = d
⊢ ⋯.index hd = hxy.index hd

Tactic:
by
  obtain ⟨dx, x, rfl⟩ := x.mk_surjective
  obtain ⟨dy, y, rfl⟩ := y.mk_surjective
  obtain rfl : dy = dx + 1 := hxy.dim_eq
  obtain rfl : dx = d := hd
  symm
  simp [← (hxy.of_iso e).δ_eq_iff rfl,
    ← SSet.δ_naturality_apply, dsimp% hxy.δ_index rfl]

Goal state after: