mathlib-initiative/mathlib-tactics huggingface dataset:
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⟩
    have : padicValNat p k < k := by calc
      _ ≤ log p k := padicValNat_le_nat_log k
      _ < _ := log_lt_self p (by lia)
    rw [hk, padicValNat.mul (by lia) (by lia), padicValNat_self]
    calc
      _ ≤ p + k := by lia
      _ ≤ _ := Nat.add_le_mul hp.out.two_le (by lia)

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

Goal state before:
pp: p n : ℕ
hn : n ≠ 0
⊢ Finset.image (fun x ↦ p ^ x) (Finset.range (padicValNat p n + 1)) ⊆ n.divisors

Tactic:
intro t ht
  simp only [Finset.mem_image, Finset.mem_range] at ht
  obtain ⟨k, hk, rfl⟩ := ht
  rw [Nat.mem_divisors]
  exact ⟨(pow_dvd_pow p <| by lia).trans pow_padicValNat_dvd, hn⟩

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 : ℕ
⊢ Subsingleton (F.H n)

Tactic:
rw [← functorH_obj_coe]

Goal state after:
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 : ℕ
⊢ Subsingleton ↑((functorH J n).obj F)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
⊢ f.norm = g.norm

Tactic:
have hg : ¬g ≈ 0 := hf ∘ Setoid.trans hfg

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ f.norm = g.norm
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
x : ↥X
a : S.residueField (f x) ⟶ CommRingCat.of Ω
hx : f x = ((SpecToEquivOfField Ω S).symm ⟨f x, a⟩) default
⊢ ∃ l, l ≫ f = (SpecToEquivOfField Ω S).symm ⟨f x, a⟩ ∧ l default = x

Tactic:
let m := (f.residueFieldMap x).hom

Goal state after:
X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
x : ↥X
a : S.residueField (f x) ⟶ CommRingCat.of Ω
hx : f x = ((SpecToEquivOfField Ω S).symm ⟨f x, a⟩) default
m : ↑(S.residueField (f x)) →+* ↑(X.residueField x) := CommRingCat.Hom.hom (Hom.residueFieldMap f x)
⊢ ∃ l, l ≫ f = (SpecToEquivOfField Ω S).symm ⟨f x, a⟩ ∧ l default = x
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case hf.hj₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ n + 2 ≤ ↑((Fin.cast ⋯ (Fin.natAdd (a + 3) ⟨k, hk⟩)).pred ⋯) + q

pp: case hf
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ ⟨a + 1, ⋯⟩.succ < Fin.cast ⋯ (Fin.natAdd (a + 3) ⟨k, hk⟩)

Tactic:
· dsimp [Fin.cast, Fin.pred]
      rw [Nat.add_right_comm, Nat.add_sub_assoc (by simp : 1 ≤ 3)]
      lia

Goal state after:
case hf
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ ⟨a + 1, ⋯⟩.succ < Fin.cast ⋯ (Fin.natAdd (a + 3) ⟨k, hk⟩)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
calc
      _ ≤ ‖(p : ℚ_[p])‖ * 1 :=
        mul_le_mul le_rfl (by simpa using norm_int_le_one _) (norm_nonneg _) (norm_nonneg _)
      _ < 1 := by
        rw [mul_one, norm_p]
        exact inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt

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

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ↑p ^ (-x⁻¹.valuation) = (↑p ^ (-x.valuation))⁻¹
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ x⁻¹.valuation = -x.valuation

Tactic:
← zpow_neg,

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ↑p ^ (-x⁻¹.valuation) = ↑p ^ (- -x.valuation)
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ x⁻¹.valuation = -x.valuation
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
⊢ (x ^ Int.negSucc n).valuation = Int.negSucc n * x.valuation

Tactic:
by simp [← neg_mul]; simp [Int.negSucc_eq]

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

Goal state before:
pp: Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId ↔ (unop A.fst).len = (unop Δ).len

Tactic:
by
  rw [eqId_iff_eq]
  constructor
  · intro h
    rw [h]
  · intro h
    rw [← unop_inj_iff]
    ext
    exact h

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

Goal state before:
pp: case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = ⟨↑i, ⋯⟩.castSucc
eq : X.σ j.rev.succ ≫ (P q).f (n + 1 + 1) = 0
⊢ (P ↑j).f (n + 1) ≫
      X.δ j.rev.succ ≫ X.σ j.rev ≫ X.σ i ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0

Tactic:
hi',

Goal state after:
case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = ⟨↑i, ⋯⟩.castSucc
eq : X.σ j.rev.succ ≫ (P q).f (n + 1 + 1) = 0
⊢ (P ↑j).f (n + 1) ≫
      X.δ j.rev.succ ≫
        X.σ j.rev ≫ X.σ ⟨↑i, ⋯⟩.castSucc ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0
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:
← sub_eq_zero,

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 _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) - PInfty.f n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ PInfty.f (n + 1) ≫ K[X].d (n + 1) n = PInfty.f (n + 1) ≫ X.map i.op

Tactic:
AlternatingFaceMapComplex.obj_d_eq

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ PInfty.f (n + 1) ≫ ∑ i, (-1) ^ ↑i • X.δ i = PInfty.f (n + 1) ≫ X.map i.op
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✝⁶ : (trivialCofibrations C).HasFactorization (fibrations C)
inst✝⁵ : HasPullbacks C
inst✝⁴ : (fibrations C).IsStableUnderComposition
inst✝³ : (fibrations C).IsStableUnderBaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (pullback.lift f i ⋯) :=
  (trivialCofibrations C).factorizationData (fibrations C) (pullback.lift f i ⋯)
sq' : CommSq h.i i (h.p ≫ pullback.snd p g) (𝟙 B)
h₁ : WeakEquivalence (h.i ≫ h.p ≫ pullback.snd p g)
h₂ : Fibration (h.p ≫ pullback.snd p g)
this : WeakEquivalence (h.p ≫ pullback.snd p g)
⊢ (sq'.lift ≫ h.p ≫ pullback.fst p g) ≫ p = g

Tactic:
rw [assoc, assoc, pullback.condition, reassoc_of% sq'.fac_right]

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h : (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂
⊢ (ConcreteCategory.hom c'.inl) x₁ = (ConcreteCategory.hom c'.inr) x₂

Tactic:
convert! congr_arg e.hom.hom h
  · exact ConcreteCategory.congr_hom (e.hom.w WalkingSpan.left).symm x₁
  · exact ConcreteCategory.congr_hom (e.hom.w WalkingSpan.right).symm x₂

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

Goal state before:
pp: case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
c₁ : Cell i d
f₁ : ⦋n⦌ ⟶ ⦋d⦌
w✝¹ : Epi f₁
hx₁ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
f₂ : ⦋n⦌ ⟶ ⦋d⦌
w✝ : Epi f₂
hx₂ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
h : (ConcreteCategory.hom (Y.map f₁.op)) c₁.simplex = (ConcreteCategory.hom (Y.map f₂.op)) c₁.simplex
⊢ (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) =
    (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)

Tactic:
obtain rfl : f₁ = f₂ :=
        Y.unique_nonDegenerate_map _ f₁ ⟨_, c₁.nonDegenerate⟩ rfl
          f₂ ⟨_, c₁.nonDegenerate⟩ h

Goal state after:
case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
c₁ : Cell i d
f₁ : ⦋n⦌ ⟶ ⦋d⦌
w✝¹ : Epi f₁
hx₁ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
w✝ : Epi f₁
hx₂ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
h : (ConcreteCategory.hom (Y.map f₁.op)) c₁.simplex = (ConcreteCategory.hom (Y.map f₁.op)) c₁.simplex
⊢ (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) =
    (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ (ConcreteCategory.hom (X.map (tr (intervalEdge j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f) =
    (ConcreteCategory.hom (X.map (tr (diag l) ⋯ ⋯ ≫ tr (subinterval j l hjl) ⋯ ?h).op)) (sx.spineToSimplex m ?h f)

pp: case h
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ m ≤ n + 1

Tactic:
← tr_comp,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ (ConcreteCategory.hom (X.map (tr (intervalEdge j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f) =
    (ConcreteCategory.hom (X.map (tr (diag l ≫ subinterval j l hjl) ⋯ h).op)) (sx.spineToSimplex m ?h f)

case h
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ m ≤ n + 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : i.castSucc < j
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯).op))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.vertex i.castSucc

Tactic:
← tr_comp,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : i.castSucc < j
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ i ≫ SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f) =
    f.vertex i.castSucc
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inl
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
hlt : ksucc < j
⊢ (stdSimplex.spineId (n + 2)).arrow k.castSucc =
    (ConcreteCategory.hom (Δ[n + 2].map (mkOfSucc k).op)) (yonedaEquiv (stdSimplex.map (SimplexCategory.δ j)))

Tactic:
stdSimplex.map_apply,

Goal state after:
case h.inl
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
hlt : ksucc < j
⊢ (stdSimplex.spineId (n + 2)).arrow k.castSucc =
    stdSimplex.objEquiv.symm
      ((mkOfSucc k).op.unop ≫ stdSimplex.objEquiv (yonedaEquiv (stdSimplex.map (SimplexCategory.δ j))))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯).op))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.vertex i.succ

Tactic:
← tr_comp,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ i ≫ SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f) =
    f.vertex i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : i.succ.castSucc < j
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯).op))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.castSucc

Tactic:
← tr_comp,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : i.succ.castSucc < j
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i ≫ SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.castSucc
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)
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋l⦌ i) ⋯ ⋯ ≫ tr (subinterval j l h) ⋯ hₘ).op)) Δ =
    Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ,
        arrow := fun i ↦ (X.spine m hₘ Δ).arrow ⟨j + ↑i, ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
      i

Tactic:
← tr_comp,

Goal state after:
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)
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋l⦌ i ≫ subinterval j l h) ⋯ hₘ).op)) Δ =
    Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ,
        arrow := fun i ↦ (X.spine m hₘ Δ).arrow ⟨j + ↑i, ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
      i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯).op))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ

Tactic:
← tr_comp,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i ≫ SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inl
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
hgt : j < ksucc
⊢ (stdSimplex.spineId (n + 2)).arrow k.succ =
    (ConcreteCategory.hom (Δ[n + 2].map (mkOfSucc k).op)) (yonedaEquiv (stdSimplex.map (SimplexCategory.δ j)))

Tactic:
stdSimplex.map_apply,

Goal state after:
case h.inr.inl
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
hgt : j < ksucc
⊢ (stdSimplex.spineId (n + 2)).arrow k.succ =
    stdSimplex.objEquiv.symm
      ((mkOfSucc k).op.unop ≫ stdSimplex.objEquiv (yonedaEquiv (stdSimplex.map (SimplexCategory.δ j))))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯).op))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i) 2 ⋯)

Tactic:
← tr_comp,

Goal state after:
n : ℕ
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i ≫ SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i) 2 ⋯)
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) ⋯ ⋯ ≫ 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:
← tr_comp,

Goal state after:
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 ≫ 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
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: 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
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
z : Fin (1 + 1)
⊢ ((ConcreteCategory.hom (Δ[n + 1 + 2].map (diag 2).op)) ↑triangle) z =
    ((ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc k).op)) (yonedaEquiv (stdSimplex.δ j))) z

Tactic:
stdSimplex.map_apply,

Goal state after:
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
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
z : Fin (1 + 1)
⊢ (stdSimplex.objEquiv.symm ((diag 2).op.unop ≫ stdSimplex.objEquiv ↑triangle)) z =
    ((ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc k).op)) (yonedaEquiv (stdSimplex.δ j))) z
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: 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
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
z : Fin (1 + 1)
⊢ (stdSimplex.objEquiv.symm (diag 2 ≫ stdSimplex.objEquiv ↑triangle)) z =
    ((ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc k).op)) (yonedaEquiv (stdSimplex.δ j))) z

Tactic:
stdSimplex.map_apply,

Goal state after:
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
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
z : Fin (1 + 1)
⊢ (stdSimplex.objEquiv.symm (diag 2 ≫ stdSimplex.objEquiv ↑triangle)) z =
    (stdSimplex.objEquiv.symm ((mkOfSucc k).op.unop ≫ stdSimplex.objEquiv (yonedaEquiv (stdSimplex.δ j)))) z
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X : C
⊢ (eId (Type v) X ≫ ↾fun f ↦ F.map f) = eId (Type v) (F.obj X)

Tactic:
ext ⟨⟩; exact F.map_id X

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

Goal state before:
pp: case comp_of.inr.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
h' : x✝.len < (mk n✝).len
⊢ x✝.len < (mk (n✝ + 1)).len

Tactic:
· exact Nat.lt_succ_of_lt h'

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

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

Tactic:
rw [← Fin.le_castSucc_iff] at h

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