mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| multiplicity (↑p) n₁ + multiplicity (↑p) d₂ ≤ multiplicity (↑p) d₁ + multiplicity (↑p) n₂

Tactic:
← multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf1,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| multiplicity (↑p) (n₁ * d₂) ≤ multiplicity (↑p) d₁ + multiplicity (↑p) n₂
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValNat p (p * (n / p))! = padicValNat p n !

Tactic:
nth_rw 2 [← div_add_mod n p]
  exact (padicValNat_factorial_mul_add (n / p) <| mod_lt n hp.out.pos).symm

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

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
n : ℕ
⊢ n ≥ stationaryPoint hf → padicNorm p (↑f n) < ε

Tactic:
hn

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
n : ℕ
hn : n ≥ stationaryPoint hf
⊢ padicNorm p (↑f n) < ε
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
⊢ Presheaf.IsSheaf J (Φ.skyscraperPresheaf M)

Tactic:
by
  rw [Presheaf.isSheaf_iff_isLimit]
  intro X R hR
  exact ⟨{
    lift s := (isSheaf_skyscraperPresheaf_aux R hR s).choose
    fac s j := by
      dsimp
      ext y
      simpa using! (isSheaf_skyscraperPresheaf_aux R hR s).choose_spec _ y
    uniq s m hm := by
      dsimp at hm ⊢
      ext x
      obtain ⟨Y, g, hg, y, rfl⟩ := Φ.jointly_surjective _ hR x
      simpa [← hm (op (Presieve.categoryMk _ _ hg))] using!
        ((isSheaf_skyscraperPresheaf_aux R hR s).choose_spec (Presieve.categoryMk _ _ hg) y).symm }⟩

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
hyp : ∃ N, ∀ i ≥ N, (f - const (padicNorm p) (↑f i)).norm < ε
⊢ ∃ N, ∀ i ≥ N, { toFun := Quotient.lift PadicSeq.norm ⋯, map_mul' := ⋯ } (Padic.mk f - ↑(↑f i)) < ε

Tactic:
peel hyp with N

Goal state after:
case h.h.h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
hyp : ∃ N, ∀ i ≥ N, (f - const (padicNorm p) (↑f i)).norm < ε
N✝ i✝ : ℕ
a✝ : i✝ ≥ N✝
N : (f - const (padicNorm p) (↑f i✝)).norm < ε
⊢ { toFun := Quotient.lift PadicSeq.norm ⋯, map_mul' := ⋯ } (Padic.mk f - ↑(↑f i✝)) < ε
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: case refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X✝ Y : D
P : MorphismProperty C
inst✝² : F✝.Faithful
inst✝¹ : F✝.Full
inst✝ : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F✝ P f
hg : relative F✝ P g
Z X : C
p : F✝.obj Z ⟶ H
fst : F✝.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F✝.map snd) (f ≫ g) p
⊢ IsPullback fst (F✝.map (⋯.lift (fst ≫ f) snd ⋯) ≫ F✝.map (⋯.snd p)) (f ≫ g) p

pp: case refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X✝ Y : D
P : MorphismProperty C
inst✝² : F✝.Faithful
inst✝¹ : F✝.Full
inst✝ : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F✝ P f
hg : relative F✝ P g
Z X : C
p : F✝.obj Z ⟶ H
fst : F✝.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F✝.map snd) (f ≫ g) p
⊢ fst ≫ f = F✝.map (⋯.lift (fst ≫ f) snd ⋯) ≫ ⋯.fst p

Tactic:
· rw [← Functor.map_comp, lift_snd]
      exact h

Goal state after:
case refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X✝ Y : D
P : MorphismProperty C
inst✝² : F✝.Faithful
inst✝¹ : F✝.Full
inst✝ : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F✝ P f
hg : relative F✝ P g
Z X : C
p : F✝.obj Z ⟶ H
fst : F✝.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F✝.map snd) (f ≫ g) p
⊢ fst ≫ f = F✝.map (⋯.lift (fst ≫ f) snd ⋯) ≫ ⋯.fst p
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ¬p ∣ (↑z).den

Tactic:
by simp [hp.1.ne_one]

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ᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e) =
    Termwise.mapMono K i ≫
      Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K (Splitting.IndexSet.mk e).e.op

Tactic:
dsimp only [Splitting.IndexSet.id_fst, Splitting.IndexSet.mk, op_unop, Splitting.IndexSet.e]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') ⟨op Δ'', ⟨e, ⋯⟩⟩ =
    Termwise.mapMono K i ≫ Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K e.op
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ cast hu hv e = _root_.cast ⋯ e

Tactic:
by
  subst_vars
  rfl

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' u'' v'' : U
e : u ⟶ v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
⊢ cast hu' hv' (cast hu hv e) = cast ⋯ ⋯ e

Tactic:
by
  subst_vars
  rfl

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ cast hu hv e ≍ e

Tactic:
by
  subst_vars
  rfl

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ cast hu hv p = _root_.cast ⋯ p

Tactic:
by
  subst_vars
  rfl

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' u'' v'' : U
p : Path u v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
⊢ cast hu' hv' (cast hu hv p) = cast ⋯ ⋯ p

Tactic:
by
  subst_vars
  rfl

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u u' : U
hu : u = u'
⊢ cast hu hu nil = nil

Tactic:
by
  subst_vars
  rfl

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v w u' w' : U
p : Path u v
e : v ⟶ w
hu : u = u'
hw : w = w'
⊢ cast hu hw (p.cons e) = (cast hu ⋯ p).cons (Hom.cast ⋯ hw e)

Tactic:
by
  subst_vars
  rfl

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
h : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : weakEquivalences (BifibrantObject C) f
⊢ IsIso (F.map f)

Tactic:
rw [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty] at hf
    obtain ⟨g', h₁, h₂⟩ := RightHomotopyClass.whitehead f.hom
    refine ⟨F.map (homMk g'), ?_, ?_⟩
    all_goals
      rw [← F.map_comp, ← F.map_id]
      apply h
      assumption

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
⊢ (weakEquivalences (BifibrantObject C)).IsInvertedBy F ↔
    ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g

Tactic:
by
  refine ⟨fun H K L f g h ↦ ?_, fun h X Y f hf ↦ ?_⟩
  · obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_pathObject
    have := isCofibrant_of_cofibration P.ι
    have : IsIso (F.map (homMk P.ι)) := H _ (by
      rw [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]
      exact inferInstanceAs (WeakEquivalence P.ι))
    simp only [show f = homMk h.h ≫ homMk P.p₀ by cat_disch,
      show g = homMk h.h ≫ homMk P.p₁ by cat_disch, Functor.map_comp]
    congr 1
    simp [← cancel_epi (F.map (homMk P.ι)), ← Functor.map_comp]
  · rw [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty] at hf
    obtain ⟨g', h₁, h₂⟩ := RightHomotopyClass.whitehead f.hom
    refine ⟨F.map (homMk g'), ?_, ?_⟩
    all_goals
      rw [← F.map_comp, ← F.map_id]
      apply h
      assumption

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K L : BifibrantObject C
f g : K ⟶ L
h : homRel C f g
⊢ toHoCat.map f = toHoCat.map g

Tactic:
exact CategoryTheory.Quotient.sound _ h

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithFibrations C
X Y : Over S
f : X ⟶ Y
inst✝ : Fibration f
⊢ Fibration (Over.Hom.left f)

Tactic:
← fibrations_over_iff

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithFibrations C
X Y : Over S
f : X ⟶ Y
inst✝ : Fibration f
⊢ Fibration f
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : C
w✝ : IsCofibrant X
⊢ toHoCat.map (toHoCat.obj (mk X)).as.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map (bifibrantResolution.map (adjUnit.app (toHoCat.obj (mk X)))) =
    toHoCat.map (toHoCat.obj (mk X)).as.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map
        (BifibrantObject.toHoCat.map
          (BifibrantObject.homMk (mk (mk X).bifibrantResolutionObj.obj).iBifibrantResolutionObj.hom))

Tactic:
apply bifibrantResolutionMap_fac'

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

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
hd : n ≤ n
j : Fin (n + 1 + 1)
hx : stdSimplex.face {j}ᶜ ≤ A
hS : {j}ᶜᶜ.card = 1
⊢ j ≠ i

Tactic:
by rintro rfl; tauto

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

Goal state before:
pp: case neg
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : A.toSSet.HasDimensionLT n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : x ∈ Δ[n].nonDegenerate m
h₂ : x ∈ A.obj (op ⦋m⦌)
h₃ : n ≤ m
⊢ x ∈ ∂Δ[n].obj (op ⦋m⦌)

Tactic:
simp [← A.mem_nonDegenerate_iff ⟨x, h₂⟩,
        nonDegenerate_eq_empty_of_hasDimensionLT _ _ _ h₃] at h₁

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

Goal state before:
pp: case mp.inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ ∃ s,
    (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) s ∧ (ConcreteCategory.hom g) s✝ = (ConcreteCategory.hom g) s

Tactic:
exact ⟨_, rfl, rfl⟩

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

Goal state before:
pp: case succ
n : ℕ
inst✝ : NeZero (n + 1)
i : Fin (n + 1 + 1)
⊢ ∃ i_1, ofHoms (fun i ↦ Λ[i_1 + 1, i].ι) Λ[n + 1, i].ι

Tactic:
exact ⟨n, ⟨i⟩⟩

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

Goal state before:
pp: case mp.inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
⊢ ∃ s,
    (ConcreteCategory.hom f) s = (ConcreteCategory.hom f) s✝ ∧ (ConcreteCategory.hom g) s = (ConcreteCategory.hom g) s✝

Tactic:
exact ⟨_, rfl, rfl⟩

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

Goal state before:
pp: case a
⊢ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2} ≤ Λ[2, 2]

Tactic:
rw [sup_le_iff]
      constructor
      · exact face_le_horn (1 : Fin 3) 2 (by simp)
      · exact face_le_horn (0 : Fin 3) 2 (by simp)

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
⊢ ⊤ ≤ ⨆ n, (skeletonOfMono i) n

Tactic:
← Y.iSup_skeleton,

Goal state after:
X Y : SSet
i : X ⟶ Y
⊢ ⨆ n, Y.skeleton n ≤ ⨆ n, (skeletonOfMono i) n
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case «1»
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

pp: case «2»
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨2, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨2, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
· dsimp
        simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 1 2 (by simp)).hom,
          ← Category.assoc]
        convert! h₁₂ <;> decide

Goal state after:
case «2»
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨2, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨2, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case «1»
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

pp: case «2»
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
· dsimp
        simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 1 2 (by simp)).hom,
          ← Category.assoc]
        convert! h₁₂ <;> decide

Goal state after:
case «2»
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: case h_map
C : Type u
inst✝ : Category.{v, u} C
x✝ : ↑chosenTerminal ⥤ C
⊢ autoParam
    (∀ (X Y : ↑chosenTerminal) (f : X ⟶ Y),
      ((Functor.const ↑chosenTerminal).obj ((fun F ↦ F.obj { down := { as := () } }) x✝)).map f =
        eqToHom ⋯ ≫ x✝.map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
rintro ⟨⟨⟨⟩⟩⟩ ⟨⟨⟨⟩⟩⟩ ⟨⟨⟨⟨⟩⟩⟩⟩
      simp only [eqToHom_refl, Category.comp_id, Category.id_comp]
      exact (Functor.map_id _ _).symm

Goal state after:
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 : Edge x y
g : Edge y z
h : Edge x z
fac : homMk f ≫ homMk g = homMk h
⊢ f.CompStruct g h

Tactic:
dsimp [homMk, CategoryStruct.comp] at fac
  rw [Quotient.eq_iff_equiv] at fac
  exact (Quasicategory₂.fill32 (compStruct f g) (compId g) fac.some).some

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

Goal state before:
pp: case last
n : ℕ
⊢ δ (Fin.last (n + 1)) ≫ Fin.lastCases (σ (Fin.last n)) (fun i ↦ σ i) (Fin.last (n + 1)) = 𝟙 (mk n)

Tactic:
simp only [Fin.lastCases_last]

Goal state after:
case last
n : ℕ
⊢ δ (Fin.last (n + 1)) ≫ σ (Fin.last n) = 𝟙 (mk n)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case cast
n : ℕ
i✝ : Fin (n + 1)
⊢ δ i✝.castSucc ≫ Fin.lastCases (σ (Fin.last n)) (fun i ↦ σ i) i✝.castSucc = 𝟙 (mk n)

Tactic:
simp only [Fin.lastCases_castSucc]

Goal state after:
case cast
n : ℕ
i✝ : Fin (n + 1)
⊢ δ i✝.castSucc ≫ σ i✝ = 𝟙 (mk n)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case neg
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁ : hL.head.castSucc < t
h₂ : ¬a < ↑t
⊢ ↑(t.pred ⋯) = ↑t

pp: case pos
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁ : ¬hL.head.castSucc < t
h₂ : a < ↑t
⊢ ↑(t.castPred ⋯) = ↑t - 1

pp: case neg
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁ : ¬hL.head.castSucc < t
h₂ : ¬a < ↑t
⊢ ↑(t.castPred ⋯) = ↑t

Tactic:
· simp only [Fin.lt_def, Fin.val_castSucc, IsAdmissible.head_val] at h₁; grind

Goal state after:
case pos
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁ : ¬hL.head.castSucc < t
h₂ : a < ↑t
⊢ ↑(t.castPred ⋯) = ↑t - 1

case neg
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁ : ¬hL.head.castSucc < t
h₂ : ¬a < ↑t
⊢ ↑(t.castPred ⋯) = ↑t
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
⊢ { toFunctor := functor X Y } ≫ { toFunctor := inverse X Y } = 𝟙 (Cat.of (X ⊗ Y).HomotopyCategory)

Tactic:
by ext; exact functor_comp_inverse X Y

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

Goal state before:
pp: case neg
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
⊢ standardσ (a :: simplicialInsert (j + 1) L) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)

Tactic:
· have : ∀ (j k : ℕ) (h : j < (k + 1)), Fin.ofNat (k + 1) j = j := by simp -- helps grind below
      have : a < m + 2 := by grind -- helps grind below
      have : σ (Fin.ofNat (m + 2) a) ≫ σ (.ofNat _ j) = σ (.ofNat _ (j + 1)) ≫ σ (.ofNat _ a) := by
        convert! σ_comp_σ_nat (n := m) a j (by grind) (by grind) (by grind) <;> grind
      grind [standardσ_cons]

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

Goal state before:
pp: n : ℕ
j i : Fin (n + 2)
h✝ : i.castSucc ≤ j.castSucc
h : i ≤ j
⊢ δ j ≫ toMk₁ i.castSucc = toMk₁ i

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Goal state after:
n : ℕ
j i : Fin (n + 2)
h✝ : i.castSucc ≤ j.castSucc
h : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ (ConcreteCategory.hom (δ j ≫ toMk₁ i.castSucc)) k = (ConcreteCategory.hom (toMk₁ i)) k