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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
j : κ.ord.ToType
⊢ Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ f j).hom) ≫
      Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) =
    𝟙 (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).right.right

Tactic:
have := Arrow.rightFunc.congr_map ((iterationFunctorMapSuccAppArrowIso I κ f j).hom.w)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
j : κ.ord.ToType
this :
  Arrow.rightFunc.map
      (Arrow.Hom.left (iterationFunctorMapSuccAppArrowIso I κ f j).hom ≫
        (Arrow.mk ((ε I.homFamily).app (((iterationFunctor I κ).obj j).obj f))).hom) =
    Arrow.rightFunc.map
      ((Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).hom ≫
        Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ f j).hom)
⊢ Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ f j).hom) ≫
      Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) =
    𝟙 (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).right.right
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ (relativeCellComplexιObjFObjSuccIso I κ f j).hom ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
        (transfiniteCompositionOfShapeιIterationAppRight I κ (Arrow.mk f)).incl.app j =
    (relativeCellComplexιObjFObjSuccIso I κ f j).hom ≫
      (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
        (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ ((iteration I κ).obj (Arrow.mk f)).hom

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ (relativeCellComplexιObjFObjSuccIso I κ f j).hom ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
        (transfiniteCompositionOfShapeιIterationAppRight I κ (Arrow.mk f)).incl.app j =
    (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ ((iteration I κ).obj (Arrow.mk f)).hom
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
⊢ ∀ {f_1 : A ⟶ obj I κ f} {g : B ⟶ Y} (sq : CommSq f_1 i (πObj I κ f) g), sq.HasLift

Tactic:
have := hasColimitsOfShape_discrete I κ

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
⊢ ∀ {f_1 : A ⟶ obj I κ f} {g : B ⟶ Y} (sq : CommSq f_1 i (πObj I κ f) g), sq.HasLift
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A ≠ ⊤
⊢ A < largerSubobject hG A

Tactic:
dsimp only [largerSubobject]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A ≠ ⊤
⊢ A < if hA : A = ⊤ then ⊤ else ⋯.choose
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this✝¹ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this✝ : HasPushouts C
this : PreservesColimit (relativeCellComplexιObj I κ f).F (coyoneda.obj (Opposite.op A))
g : A ⟶ obj I κ f
b : B ⟶ Y
sq : CommSq g i (πObj I κ f) b
j : κ.ord.ToType
t : A ⟶ (relativeCellComplexιObj I κ f).F.obj j
ht : t ≫ (relativeCellComplexιObj I κ f).incl.app j = g
⊢ (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
      πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv =
    (relativeCellComplexιObjFObjSuccIso I κ f j).hom ≫
      (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
        (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
          πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this✝¹ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this✝ : HasPushouts C
this : PreservesColimit (relativeCellComplexιObj I κ f).F (coyoneda.obj (Opposite.op A))
g : A ⟶ obj I κ f
b : B ⟶ Y
sq : CommSq g i (πObj I κ f) b
j : κ.ord.ToType
t : A ⟶ (relativeCellComplexιObj I κ f).F.obj j
ht : t ≫ (relativeCellComplexιObj I κ f).incl.app j = g
⊢ (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
      πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv =
    (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
      πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
h2 : min (padicValRat p (q + r)) (padicValRat p r) ≤ padicValRat p q
h3 : min (padicValRat p (q + r)) (padicValRat p q) ≤ padicValRat p r
⊢ padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)

Tactic:
omega

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (0 + F d)

Tactic:
zero_add

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (F d)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ 1 ≤ ‖x‖ ↔ ‖x‖ = 1

Tactic:
simp [le_antisymm_iff, ← padic_norm_e_of_padicInt, x.prop]

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

Goal state before:
pp: case succ
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n < p → padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
⊢ 0 + padicValNat p (p * m)! = padicValNat p (p * m)!

Tactic:
zero_add

Goal state after:
case succ
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n < p → padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
⊢ padicValNat p (p * m)! = padicValNat p (p * m)!
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ (if hf : f * g ≈ 0 then 0 else padicNorm p (↑(f * g) (stationaryPoint hf))) =
    (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) *
      if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))

Tactic:
simp only [hfg, hf, hg, dite_false]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ padicNorm p (↑(f * g) (stationaryPoint ⋯)) =
    padicNorm p (↑f (stationaryPoint ⋯)) * padicNorm p (↑g (stationaryPoint ⋯))
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
P : Cᵒᵖ ⥤ A
M : A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
f : Φ.presheafFiber.obj P ⟶ M
X : C
x : Φ.fiber.obj X
⊢ (Φ.skyscraperPresheafHomEquiv f).app (op X) ≫ Pi.π (fun x ↦ M) x = Φ.toPresheafFiber X x P ≫ f

Tactic:
by
  simp [skyscraperPresheafHomEquiv_apply_app]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
s₀ : ↥S
hs₀ : s default = s₀
X : S.Etale
t : (pointSmallEtale s).fiber.obj X
⊢ (Over.Hom.left t) default ∈ ⇑X.hom ⁻¹' {s₀}

Tactic:
by
    have := (Over.w t).symm
    cat_disch

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; use N

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

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

pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
⊢ φ ≫ (Hσ q).f (n + 1) = 0

Tactic:
· exact v.of_succ.comp_Hσ_eq_zero hqn

Goal state after:
case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
⊢ φ ≫ (Hσ q).f (n + 1) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case a
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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : ⟨i, hi⟩ ∈ Finset.univ
hia : ⟨i, ⋯⟩ ≤ ⟨a, ⋯⟩.castSucc
pf✝⁴ : IsRightCancelAdd ℕ
pf✝³ : a + 1 < n + 1 + 1
pf✝² : i < n + 1 + 2
pf✝¹ : i < n + 2
pf✝ : a < n + 1
⊢ ((-1) ^ i * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a, pf✝⟩.succ ≫ X.δ ⟨i, pf✝²⟩ +
      ((-1) ^ a * (-1) ^ i) • φ ≫ X.δ ⟨i, pf✝¹⟩ ≫ X.σ ⟨a, pf✝⟩ =
    0

Tactic:
← Fin.castSucc_mk (n + 2) i ‹_›,

Goal state after:
case a
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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : ⟨i, hi⟩ ∈ Finset.univ
hia : ⟨i, ⋯⟩ ≤ ⟨a, ⋯⟩.castSucc
pf✝⁴ : IsRightCancelAdd ℕ
pf✝³ : a + 1 < n + 1 + 1
pf✝² : i < n + 1 + 2
pf✝¹ : i < n + 2
pf✝ : a < n + 1
⊢ ((-1) ^ i * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a, pf✝⟩.succ ≫ X.δ ⟨i, pf✝¹⟩.castSucc +
      ((-1) ^ a * (-1) ^ i) • φ ≫ X.δ ⟨i, pf✝¹⟩ ≫ X.σ ⟨a, pf✝⟩ =
    0
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: 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⦌
v : HigherFacesVanish q φ
hqn : n < q
⊢ φ ≫ (0 + hσ' q (n + 1) (n + 2) ⋯ ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1)) = 0

Tactic:
zero_add

Goal state after:
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⦌
v : HigherFacesVanish q φ
hqn : n < q
⊢ φ ≫ hσ' q (n + 1) (n + 2) ⋯ ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1) = 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

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

Tactic:
zero_add

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

case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ (if y = 0 then ⊤ else ↑y.valuation) ≤ ⊤
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Function.Injective fun A ↦ ⟨⟨(unop A.fst).len, ⋯⟩, ⇑(Hom.toOrderHom A.e)⟩

Tactic:
rintro ⟨⟨Δ₁⟩, α₁⟩ ⟨⟨Δ₂⟩, α₂⟩ h₁

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
Δ₂ : SimplexCategory
α₂ : { α // Epi α }
h₁ :
  (fun A ↦ ⟨⟨(unop A.fst).len, ⋯⟩, ⇑(Hom.toOrderHom A.e)⟩) ⟨op Δ₁, α₁⟩ =
    (fun A ↦ ⟨⟨(unop A.fst).len, ⋯⟩, ⇑(Hom.toOrderHom A.e)⟩) ⟨op Δ₂, α₂⟩
⊢ ⟨op Δ₁, α₁⟩ = ⟨op Δ₂, α₂⟩
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

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

Tactic:
rw [eqId_iff_len_eq]
  constructor
  · intro h
    rw [h]
  · exact le_antisymm (len_le_of_epi A.e)

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

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
⊢ DegeneraciesVanish f ↔ QInfty.f (n + 1) ≫ f = 0

Tactic:
refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
    · simp [QInfty_f, decomposition_Q, Preadditive.sum_comp, hf.σ_comp]
    · have := PInfty_f_add_QInfty_f (n + 1) =≫ f
      rw [Category.id_comp] at this
      rw [degeneraciesVanish_succ_iff, ← this]
      simp [hf]

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

Goal state before:
pp: case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : 0 + f ≫ QInfty.f (n + 1) = f
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Tactic:
zero_add

Goal state after:
case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : f ≫ QInfty.f (n + 1) = f
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
h : f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0
A : IndexSet (op ⦋n⦌)
hA : ¬A.EqId
⊢ f ≫ (s.πSummand A ≫ (s.cofan (op ⦋n⦌)).inj A) ≫ PInfty.f n = 0

Tactic:
· simp only [assoc, s.cofan_inj_comp_PInfty_eq_zero A hA, comp_zero]

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
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq :
  K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) +
      ∑ j_1 ∈ {IndexSet.id (op ⦋j⦌)}ᶜ,
        K[X].d i j ≫ (s.πSummand j_1 ≫ (s.cofan (op ⦋j⦌)).inj j_1) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0
⊢ ∀ x ∈ {IndexSet.id (op ⦋j⦌)}ᶜ,
    K[X].d i j ≫ (s.πSummand x ≫ (s.cofan (op ⦋j⦌)).inj x) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0

Tactic:
intro A hA

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq :
  K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) +
      ∑ j_1 ∈ {IndexSet.id (op ⦋j⦌)}ᶜ,
        K[X].d i j ≫ (s.πSummand j_1 ≫ (s.cofan (op ⦋j⦌)).inj j_1) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0
A : IndexSet (op ⦋j⦌)
hA : A ∈ {IndexSet.id (op ⦋j⦌)}ᶜ
⊢ K[X].d i j ≫ (s.πSummand A ≫ (s.cofan (op ⦋j⦌)).inj A) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0
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 ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X)

Tactic:
rw [Γ₂N₂.natTrans_app_f_app]

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.app X).inv ≫
      (N₂ ⋙ Γ₂).map ((toKaroubi (SimplicialObject C)).obj X).decompId_i ≫
        (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app ((toKaroubi (SimplicialObject C)).obj X).X ≫
          ((toKaroubi (SimplicialObject C)).obj X).decompId_p
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ (F.trans G).symm = G.symm.trans F.symm

Tactic:
by
      ext : 1 <;> exact ContinuousMap.Homotopy.symm_trans _ _

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: J : Type u
f : J → Grpd
j : J
⊢ (piIsoPi J f).hom ≫ Limits.Pi.π f j = Pi.eval (fun i ↦ ↑(f i)) j

Tactic:
simp [piIsoPi]

Goal state after:
J : Type u
f : J → Grpd
j : J
⊢ (piLimitFan f).π.app { as := j } = Pi.eval (fun i ↦ ↑(f i)) j
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a✝ : (i : ι) → Path (as i) (bs i)
⊢ proj i (pi fun i ↦ Quotient.mk (a✝ i)) = Quotient.mk (a✝ i)

Tactic:
rw [proj, pi_lift]

Goal state after:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a✝ : (i : ι) → Path (as i) (bs i)
⊢ (Quotient.mk (Path.pi a✝)).map { toFun := fun p ↦ p i, continuous_toFun := ⋯ } = Quotient.mk (a✝ i)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case mk
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
γ : Path x₀ x₁
⊢ (mk γ).trans (mk γ).symm = refl x₀

Tactic:
simpa [← mk_trans, ← mk_symm, ← mk_refl, eq] using Homotopic.trans_symm γ

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ ∀ (a : J.L),
    (I.fst a ≫ if hk : J.fst a = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) =
      I.snd a ≫ if hk : J.snd a = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr

Tactic:
by
      rw [Unique.forall_iff]
      simpa [h'.symm] using s.condition

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

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

Tactic:
rw [horn_eq_iSup]

Goal state after:
n : ℕ
i j : Fin (n + 1)
h : i ≠ j
⊢ stdSimplex.face {i}ᶜ ≤ ⨆ j_1, stdSimplex.face {↑j_1}ᶜ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case neg.inr
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
⊢ stdSimplex.face {j}ᶜ ≤ Λ[n + 1, i]

Tactic:
exact face_le_horn _ _ (by rintro rfl; tauto)

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ (stdSimplex.faceSingletonComplIso i).hom ≫ (stdSimplex.faceSingletonComplIso i).inv ≫ ι i =
    (stdSimplex.faceSingletonComplIso i).hom ≫ faceι i

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
n : ℕ
i : Fin (n + 2)
⊢ ι i = (stdSimplex.faceSingletonComplIso i).hom ≫ faceι i
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_1
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ ⟨k, ⋯⟩ ≤ ⟨k + 1, ⋯⟩

Tactic:
simp only [Fin.mk_le_mk, le_add_iff_nonneg_right, zero_le]

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ (stdSimplex.faceSingletonComplIso j).hom ≫ (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hij =
    (stdSimplex.faceSingletonComplIso j).hom ≫ faceι i j hij

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ ι i j hij = (stdSimplex.faceSingletonComplIso j).hom ≫ faceι i j hij