mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ (P q).f 0 = 𝟙 (K[X].X 0)

Tactic:
induction q with
  | zero => rfl
  | succ q hq =>
    simp only [P_succ, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
      HomologicalComplex.id_f, id_comp, hq, Hσ_eq_zero, add_zero]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ (↑p)⁻¹ < 1

Tactic:
exact inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt

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

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
⊢ φ ≫ (P q).f (n + 1) = φ → HigherFacesVanish q φ

Tactic:
intro hφ

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
hφ : φ ≫ (P q).f (n + 1) = φ
⊢ HigherFacesVanish q φ
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
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: p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ≤ ‖z1 + z2‖

Tactic:
rw [add_eq_max_of_ne hne]; apply le_max_left

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
n : ℕ
⊢ PInfty.f n = G.map (PInfty.f n)

Tactic:
simp only [PInfty_f, map_P]

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : f ≈ 0
⊢ PadicSeq.valuation f = PadicSeq.valuation g

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
⊢ PadicSeq.valuation f = PadicSeq.valuation g

Tactic:
· have hg : g ≈ 0 := Setoid.trans (Setoid.symm h) hf
      simp [hf, hg, PadicSeq.valuation]

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
⊢ PadicSeq.valuation f = PadicSeq.valuation g
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then ⊤ else ↑(x * y).valuation) =
    (if x = 0 then ⊤ else ↑x.valuation) + if y = 0 then ⊤ else ↑y.valuation

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then ⊤ else ↑(x * y).valuation) =
    (if x = 0 then ⊤ else ↑x.valuation) + if y = 0 then ⊤ else ↑y.valuation

Tactic:
· rw [hy, if_pos rfl, mul_zero, if_pos rfl, WithTop.add_top]

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then ⊤ else ↑(x * y).valuation) =
    (if x = 0 then ⊤ else ↑x.valuation) + if y = 0 then ⊤ else ↑y.valuation
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    (Γ₂N₂ToKaroubiIso.app X).inv ≫
      Γ₂.map (N₂.map (𝟙 ((toKaroubi (SimplicialObject C)).obj X))) ≫
        (Γ₂N₂ToKaroubiIso.hom.app ((toKaroubi (SimplicialObject C)).obj X).X ≫
            Γ₂N₁.natTrans.app ((toKaroubi (SimplicialObject C)).obj X).X) ≫
          𝟙
            { X := ((toKaroubi (SimplicialObject C)).obj X).X, p := 𝟙 ((toKaroubi (SimplicialObject C)).obj X).X,
              idem := ⋯ }

Tactic:
rw [N₂.map_id, Γ₂.map_id, Iso.app_inv]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    Γ₂N₂ToKaroubiIso.inv.app X ≫
      𝟙 (Γ₂.obj (N₂.obj ((toKaroubi (SimplicialObject C)).obj X))) ≫
        (Γ₂N₂ToKaroubiIso.hom.app ((toKaroubi (SimplicialObject C)).obj X).X ≫
            Γ₂N₁.natTrans.app ((toKaroubi (SimplicialObject C)).obj X).X) ≫
          𝟙
            { X := ((toKaroubi (SimplicialObject C)).obj X).X, p := 𝟙 ((toKaroubi (SimplicialObject C)).obj X).X,
              idem := ⋯ }
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v : U
p : Path u v
hzero : p.length = 0
⊢ Path.cast ⋯ ⋯ p = nil

Tactic:
cases p
  · rfl
  · simp only [Nat.succ_ne_zero, length_cons] at hzero

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

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ Limits.IsLimit (Limits.Fan.mk (π.obj (TopCat.of ((i : I) → ↑(X i)))) (proj X))

Tactic:
apply Limits.IsLimit.ofIsoLimit _ (asIso (piTopToPiCone X)).symm

Goal state after:
I : Type u
X : I → TopCat
⊢ Limits.IsLimit (Grpd.piLimitFan fun i ↦ π.obj (X i))
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ map (ContinuousMap.id X) = 𝟭 (FundamentalGroupoid X)

Tactic:
simp only [map]; congr; ext x y ⟨p⟩; rfl

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
Z : Type u_3
inst✝ : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
⊢ map (g.comp f) = map f ⋙ map g

Tactic:
simp only [map]; congr; ext x y ⟨p⟩; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
⊢ Subfunctor.equalizer f g = A ↔ f = g

Tactic:
by
  have := range_le_equalizer_iff f g (𝟙 _)
  simp only [Category.id_comp, range_ι] at this
  rw [← this]
  constructor
  · intro h
    rw [h]
  · intro h
    exact le_antisymm (equalizer_le f g) h

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

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

Tactic:
obtain ⟨i₂, a₂, rfl⟩ := this x₂

Goal state after:
case mpr.refine_1
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
h₁ :
  ∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
    c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
      d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
h₂ : ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x
i₁ : J.R
a₁ : d.right i₁
i₂ : J.R
a₂ : d.right i₂
h :
  d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i₁) a₁) =
    d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i₂) a₂)
⊢ d.multispan.ιColimitType (WalkingMultispan.right i₁) a₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) a₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
hf : Function.Surjective ⇑(SimplexCategory.Hom.toOrderHom f)
⊢ False

Tactic:
rw [← SimplexCategory.epi_iff_surjective] at hf
      have : n + 1 ≤ m := SimplexCategory.len_le_of_epi f
      lia

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ Mono (faceι i)

Tactic:
by
  dsimp [faceι]; 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₂
inst✝ : Mono f
⊢ ∀ {x y z : X₁ ⊕ X₂}, Rel' f g x y → Rel' f g y z → Rel' f g x z

Tactic:
by
    rintro x y z (_ | ⟨_, _, h⟩ | s | _) hyz
    · exact hyz
    · obtain z₁ | z₂ := z
      · rw [inl_rel'_inl_iff] at hyz
        obtain rfl | ⟨_, _, h', h'', rfl⟩ := hyz
        · exact Rel'.inl_inl _ _ h
        · obtain rfl := (mono_iff_injective f).1 inferInstance h''
          exact Rel'.inl_inl _ _ (h.trans h')
      · rw [inl_rel'_inr_iff] at hyz
        obtain ⟨s, hs, rfl⟩ := hyz
        obtain rfl := (mono_iff_injective f).1 inferInstance hs
        rw [← h]
        apply Rel'.inl_inr
    · obtain z₁ | z₂ := z
      · replace hyz := hyz.symm
        rw [inl_rel'_inr_iff] at hyz
        obtain ⟨s', rfl, hs'⟩ := hyz
        exact Rel'.inl_inl _ _ hs'
      · rw [inr_rel'_inr_iff] at hyz
        subst hyz
        apply Rel'.inl_inr
    · obtain z₁ | z₂ := z
      · rw [inl_rel'_inl_iff] at hyz
        obtain rfl | ⟨_, _, h, h', rfl⟩ := hyz
        · apply Rel'.inr_inl
        · obtain rfl := (mono_iff_injective f).1 inferInstance h'
          rw [h]
          apply Rel'.inr_inl
      · rw [inl_rel'_inr_iff] at hyz
        obtain ⟨s, hs, rfl⟩ := hyz
        obtain rfl := (mono_iff_injective f).1 inferInstance hs
        apply Rel'.refl

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

Goal state before:
pp: case refine_1
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
h : innerHornInclusions f✝
⊢ (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι) f✝

Tactic:
obtain @⟨n, i, h0, hn⟩ := h

Goal state after:
case refine_1
X Y : SSet
n : ℕ
i : Fin (n + 3)
h0 : 0 < i
hn : i < Fin.last (n + 2)
⊢ (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι) Λ[n + 2, i].ι
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:
by exact le_trans (by rfl) (le_iSup _ x)

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

Goal state before:
pp: X : SSet
i : ℕ
x : X _⦋i⦌
n : ℕ
hi : i < n
⊢ Subcomplex.ofSimplex x ≤ X.skeleton n

Tactic:
simpa using X.mem_skeleton x hi

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

Goal state before:
pp: case inr.inr
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₃ : X₃
hx₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
y₃ : X₃
hy₃ : y₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) ((ConcreteCategory.hom b) y₃)
⊢ (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom b) y₃

Tactic:
· obtain rfl := H x₃ y₃ hx₃ hy₃ eq
    rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (inclusion n).op.HasRightKanExtension F
inst✝ : X.IsCoskeletal n
⊢ IsIso ((coskAdj n).unit.app X)

Tactic:
rw [← isCoskeletal_iff_isIso]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
X✝ Y✝ : FreeRefl V
f : X✝ ⟶ Y✝
⊢ (morphismPropertyHomMk V).multiplicativeClosure f

Tactic:
induction f using hom_induction with

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : MorphismProperty (FreeRefl V)
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V} (e : x ⟶ y), W (homMk e)
⊢ (morphismPropertyHomMk V).multiplicativeClosure ≤ W

Tactic:
MorphismProperty.multiplicativeClosure_le_iff

Goal state after:
V : Type u_1
inst✝¹ : ReflQuiver V
W : MorphismProperty (FreeRefl V)
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V} (e : x ⟶ y), W (homMk e)
⊢ morphismPropertyHomMk V ≤ W
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V✝ : Type u_1
inst✝³ : ReflQuiver V✝
V : Type u_2
inst✝² : ReflQuiver V
inst✝¹ : Unique V
inst✝ : (x y : V) → Unique (x ⟶ y)
x y : FreeRefl V
f : x ⟶ y
⊢ f = homMk default

Tactic:
induction f using hom_induction with

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

Goal state before:
pp: V : Truncated 2
W : MorphismProperty V.HomotopyCategory
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} (e : Edge x y), W (homMk e)
⊢ (morphismPropertyHomMk V).multiplicativeClosure ≤ W

Tactic:
MorphismProperty.multiplicativeClosure_le_iff

Goal state after:
V : Truncated 2
W : MorphismProperty V.HomotopyCategory
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} (e : Edge x y), W (homMk e)
⊢ morphismPropertyHomMk V ≤ W
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
⊢ ∀ (hij : i ≤ j) (hj : j ≤ n),
    i + (k + 1) = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x

Tactic:
hij

Goal state after:
case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
⊢ ∀ (hj : j ≤ n),
    i + (k + 1) = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ δ i ≫ δ j.succ = δ j ≫ δ i.castSucc

Tactic:
apply CategoryTheory.Quotient.sound

Goal state after:
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ FreeSimplexQuiver.homRel
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ j.succ))
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ j) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i.castSucc))
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ δ i.castSucc ≫ σ j.succ = σ j ≫ δ i

Tactic:
apply CategoryTheory.Quotient.sound

Goal state after:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ FreeSimplexQuiver.homRel
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i.castSucc) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ j.succ))
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ j) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i))
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ δ i.castSucc ≫ σ i = 𝟙 (mk n)

Tactic:
apply CategoryTheory.Quotient.sound

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ FreeSimplexQuiver.homRel
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i.castSucc) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ i))
    (𝟙 (mk n).as)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ δ i.succ ≫ σ i = 𝟙 (mk n)

Tactic:
apply CategoryTheory.Quotient.sound

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ FreeSimplexQuiver.homRel
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i.succ) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ i))
    (𝟙 (mk n).as)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ δ i.succ ≫ σ j.castSucc = σ j ≫ δ i

Tactic:
apply CategoryTheory.Quotient.sound

Goal state after:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ FreeSimplexQuiver.homRel
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i.succ) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ j.castSucc))
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ j) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i))
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ σ i.castSucc ≫ σ j = σ j.succ ≫ σ i

Tactic:
apply CategoryTheory.Quotient.sound

Goal state after:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ FreeSimplexQuiver.homRel
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ i.castSucc) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ j))
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ j.succ) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ i))
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₁
⊢ (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).map (homMk e) ≫
      (mkNatIso
          (fun y ↦
            Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).obj (mk x₁)).obj (mk y)))
          ⋯).hom =
    (mkNatIso
          (fun y ↦
            Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).obj (mk x₀)).obj (mk y)))
          ⋯).hom ≫
      (Functor.curry.obj (CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory)).map (homMk e)

Tactic:
by
      ext y
      obtain ⟨y, rfl⟩ := y.mk_surjective
      dsimp
      simp only [Category.comp_id]
      exact homMk_id y

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

Goal state before:
pp: case neg
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 ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : ¬Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f

pp: case pos
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 ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f

Tactic:
· obtain _ | a := a
      · exact (h₂ (Function.injective_of_subsingleton (α := Fin 1) _)).elim
      · obtain ⟨i, g', hf'⟩ := eq_σ_comp_of_not_injective _ h₂
        replace hf' : f = Hom.tr (SimplexCategory.σ i) ≫ Hom.tr g' :=
          InducedCategory.hom_ext hf'
        rw [hf']
        exact W.comp_mem _ _ (σ_mem _ (by lia) _) (hc _ _ _ _ _ (by lia))

Goal state after:
case pos
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 ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
⊢ (ConcreteCategory.hom (toMk₁ i)) j = 0 ↔ j.castSucc < i

Tactic:
simp [toMk₁_apply]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
⊢ (ConcreteCategory.hom (toMk₁ i)) j = 1 ↔ i ≤ j.castSucc

Tactic:
simp [toMk₁_apply]

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

Goal state before:
pp: case right.inl
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x✝
a✝ : Finset ι
ht : a✝ ∈ ⋃ K ∈ x✝, K.faces
⊢ a✝ ∈ (fun K ↦ K.faces) L

Tactic:
simp only [Set.mem_iUnion] at ht

Goal state after:
case right.inl
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x✝
a✝ : Finset ι
ht : ∃ i, ∃ (_ : i ∈ x✝), a✝ ∈ i.faces
⊢ a✝ ∈ (fun K ↦ K.faces) L
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
x y : A.N
⊢ x = y ↔ { dim := x.dim, simplex := x.simplex } = { dim := y.dim, simplex := y.simplex }

Tactic:
N.ext_iff,

Goal state after:
X : SSet
A : X.Subcomplex
x y : A.N
⊢ x.toN = y.toN ↔ { dim := x.dim, simplex := x.simplex } = { dim := y.dim, simplex := y.simplex }
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx✝ : x ∈ (nerve T).nonDegenerate n
hx : Function.Injective x.obj
k : ℕ
i j : Δ[n] _⦋k⦌
⊢ (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) i =
      (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) j →
    i = j

Tactic:
hij

Goal state after:
X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx✝ : x ∈ (nerve T).nonDegenerate n
hx : Function.Injective x.obj
k : ℕ
i j : Δ[n] _⦋k⦌
hij :
  (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) i =
    (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) j
⊢ i = j
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
x✝ :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim + 1, simplex := ((↑(P.p t)).cast ⋯).simplex }
⊢ ↑(P.p s) = ↑(P.p t)

Tactic:
N.ext_iff,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
x✝ :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim + 1, simplex := ((↑(P.p t)).cast ⋯).simplex }
⊢ (↑(P.p s)).toN = (↑(P.p t)).toN