mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => ⋯.choose ≫ e (Exists.choose hT),
          naturality := ⋯ } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
this :
  π a ≫ H.desc { pt := W, ι := { app := fun x ↦ ⋯.choose ≫ e (Exists.choose ⋯), naturality := ⋯ } } =
    ⋯.choose ≫ e (Exists.choose ⋯)
⊢ ⋯.choose ≫ e (Exists.choose ⋯) = e a

Tactic:
clear this

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => ⋯.choose ≫ e (Exists.choose hT),
          naturality := ⋯ } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ ⋯.choose ≫ e (Exists.choose ⋯) = e a
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type w
inst✝² : PartialOrder J✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
⊢ IsColimit ((Set.principalSegIio m).cocone (⋯.functor ⋙ F))

Tactic:
have hf : Monotone f := fun _ _ h ↦ h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type w
inst✝² : PartialOrder J✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
hf : Monotone f
⊢ IsColimit ((Set.principalSegIio m).cocone (⋯.functor ⋙ F))
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ i ≠ ⊤

Tactic:
by simpa using hi

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ i ≠ ⊥

Tactic:
by simpa using hi

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ MapEq F G i₁ i₃ ⋯ h₃

Tactic:
simp only [MapEq, arrowMap, Arrow.mk_eq_mk_iff]
  refine ⟨m₁₂.src, m₂₃.tgt, ?_⟩
  rw [← homOfLE_comp (y := ⟨i₂, h₂₃.trans h₃⟩) h₁₂ h₂₃]
  simp [-homOfLE_comp, m₁₂.w, m₂₃.w]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case isSuccLimit.inr
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this✝ : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j), k₂ < j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
⊢ MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃

Tactic:
by_cases h₅ : k₁ < j

Goal state after:
case pos
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this✝ : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j), k₂ < j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
h₅ : k₁ < j
⊢ MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃

case neg
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this✝ : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j), k₂ < j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
h₅ : ¬k₁ < j
⊢ MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inl
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi₁✝¹ : i < Order.succ j
hi₁✝ : i ≤ j
hi₁ : i < j
⊢ Φ.toSuccArrow (iter.F.obj ⟨i, ⋯⟩) = Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))).obj ⟨i, ⋯⟩)

Tactic:
extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i hi₁.le

Goal state after:
case inl
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi₁✝¹ : i < Order.succ j
hi₁✝ : i ≤ j
hi₁ : i < j
⊢ Φ.toSuccArrow (iter.F.obj ⟨i, ⋯⟩) = Φ.toSuccArrow (iter.F.obj ⟨i, ⋯⟩)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inl.e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
pf✝⁵ : l₁ ∈ Set.Iic i
pf✝⁴ : l₂ ∈ Set.Iic i
pf✝³ : ⟨l₁, pf✝⁵⟩ ≤ ⟨l₂, pf✝⁴⟩
pf✝² : l₁ ∈ Set.Iic j
pf✝¹ : l₂ ∈ Set.Iic j
pf✝ : ⟨l₁, pf✝²⟩ ≤ ⟨l₂, pf✝¹⟩
⊢ arrowMap (iter i hij).F (↑⟨l₁, pf✝⁵⟩) (↑⟨l₂, pf✝⁴⟩) pf✝³ pf✝⁴ = arrowMap (iter l₂ ⋯).F l₁ l₂ pf✝ ⋯

Tactic:
apply congr_arrowMap

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : IsMin i
⊢ i = ⊥

Tactic:
by simpa using hi

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : IsMin i
⊢ i = ⊥

Tactic:
by simpa using hi

Goal state after:
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
inst✝ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject X)))
this : Nonempty κ.ord.ToType
⊢ ∃ o j, transfiniteIterate (largerSubobject hG) j A₀ = ⊤

Tactic:
have := WellFoundedLT.toOrderBot κ.ord.ToType

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X : C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject X)))
this✝ : Nonempty κ.ord.ToType
this : OrderBot κ.ord.ToType
⊢ ∃ o j, transfiniteIterate (largerSubobject hG) j A₀ = ⊤
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ padicValRat p q⁻¹ = -padicValRat p q

Tactic:
by_cases hq : q = 0
  · simp [hq]
  · rw [eq_neg_iff_add_eq_zero, ← padicValRat.mul (inv_ne_zero hq) hq, inv_mul_cancel₀ hq,
      padicValRat.one]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject G) κ
this✝ : Fact κ.IsRegular
this : Nonempty κ.ord.ToType
⊢ (generatingMonomorphisms G).HasSmallObjectArgument

Tactic:
have := WellFoundedLT.toOrderBot κ.ord.ToType

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject G) κ
this✝¹ : Fact κ.IsRegular
this✝ : Nonempty κ.ord.ToType
this : OrderBot κ.ord.ToType
⊢ (generatingMonomorphisms G).HasSmallObjectArgument
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject G) κ
this✝² : Fact κ.IsRegular
this✝¹ : Nonempty κ.ord.ToType
this✝ : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf : HomotopicalAlgebra.RelativeCellComplex (fun x ↦ (generatingMonomorphisms G).homFamily) f
j : κ.ord.ToType
hj : ¬IsMax j
this : (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts (hf.F.map (homOfLE ⋯))
⊢ generatingMonomorphisms G ≤ monomorphisms C

Tactic:
exact generatingMonomorphisms_le_monomorphisms G

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
X : C
fac : (monomorphisms C).MapFactorizationData (monomorphisms C).rlp 0 := monoMapFactorizationDataRlp 0
⊢ Injective (monoMapFactorizationDataRlp 0).Z

Tactic:
simpa only [injective_iff_rlp_monomorphisms_zero,
    (isZero_zero C).eq_of_tgt fac.p 0] using fac.hp

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
key : ‖↑r.num‖ < 1
this : ↑p ∣ r.num ∧ ↑p ∣ ↑r.den
⊢ p ∣ 1

Tactic:
rwa [← r.reduced.gcd_eq_one, Nat.dvd_gcd_iff, ← Int.natCast_dvd, ← Int.natCast_dvd_natCast]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ f.norm = padicNorm p (↑f (stationaryPoint hf))

Tactic:
simp [norm, hf]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ Epi f ↔ IsIso c.inl

Tactic:
rw [epi_iff_inl_eq_inr hc]
  constructor
  · intro h
    obtain ⟨φ, hφ₁, hφ₂⟩ := PushoutCocone.IsColimit.desc' hc (𝟙 Y) (𝟙 Y) (by simp)
    refine ⟨φ, hφ₁, PushoutCocone.IsColimit.hom_ext hc ?_ ?_⟩
    · simp only [comp_id, reassoc_of% hφ₁]
    · simp only [comp_id, h, reassoc_of% hφ₂]
  · intro
    obtain ⟨φ, hφ₁, hφ₂⟩ := PushoutCocone.IsColimit.desc' hc (𝟙 Y) (𝟙 Y) (by simp)
    have : IsSplitMono φ := IsSplitMono.mk ⟨SplitMono.mk c.inl (by
      rw [← cancel_epi c.inl, reassoc_of% hφ₁, comp_id])⟩
    rw [← cancel_mono φ, hφ₁, hφ₂]

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

Goal state before:
pp: A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} A'
inst✝¹ : Category.{v_3, u_3} B
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
⊢ (equivalence₂ eB hF).counitIso = equivalence₂CounitIso eB hF

Tactic:
by
  ext Y'
  simp [equivalence₂, equivalence₁CounitIso_eq]

Goal state after:
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 a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ φ ≫
      ((AlternatingFaceMapComplex.obj X).d (n + 1) n ≫ ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯ +
        (((-1) ^ (a + 1) • X.σ ⟨a + 1, ⋯⟩) ≫ eqToHom ⋯) ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1)) =
    -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩

Tactic:
simp only [AlternatingFaceMapComplex.obj_d_eq, eqToHom_refl, comp_id, comp_sum, sum_comp,
    comp_add]

Goal state after:
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
⊢ ∑ j, φ ≫ ((-1) ^ ↑j • X.δ j) ≫ ((-1) ^ a • X.σ ⟨a, ⋯⟩) +
      ∑ j, φ ≫ ((-1) ^ (a + 1) • X.σ ⟨a + 1, ⋯⟩) ≫ ((-1) ^ ↑j • X.δ j) =
    -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: case succ
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) φ
⊢ φ ≫ (P (q + 1)).f (n + 1) = φ

Tactic:
simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
      comp_id, ← assoc, hq v.of_succ, add_eq_left]

Goal state after:
case succ
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) φ
⊢ φ ≫ (Hσ q).f (n + 1) = 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 a✝ q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a✝ + q
hnaq_shift : ∀ (d : ℕ), n + d = a✝ + d + q
a b : Y ⟶ X _⦋n + 1⦌
⊢ ∀ (c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f

Tactic:
c

Goal state after:
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
a b c : Y ⟶ X _⦋n + 1⦌
⊢ ∀ (d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑(p - 1)‖ = 1

Tactic:
rw [norm_natCast_eq_one_iff]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ p.Coprime (p - 1)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : SimplicialObject C
s : X.Splitting
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ f.app Δ = s.φ f (unop A.fst).len ≫ Y.map A.e.op

Tactic:
simp only [cofan_inj_eq_assoc, φ, assoc]
  rw [NatTrans.naturality]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ K.d (n + 1) n =
    ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      ((-1) ^ ↑0 • (Γ₀.obj K).δ 0) ≫ (Γ₀.splitting K).πSummand (Splitting.IndexSet.id (op ⦋n⦌))

pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ∀ (x : Fin (n + 2)),
    x ≠ 0 →
      ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
          ((-1) ^ ↑x • (Γ₀.obj K).δ x) ≫ (Γ₀.splitting K).πSummand (Splitting.IndexSet.id (op ⦋n⦌)) =
        0

Tactic:
· simp only [Fin.val_zero, pow_zero, one_zsmul]
        rw [δ, Γ₀.Obj.mapMono_on_summand_id_assoc, Γ₀.Obj.Termwise.mapMono_δ₀,
          Splitting.cofan_inj_πSummand_eq_id]
        dsimp only [Γ₀.splitting, Splitting.summand.eq_1, Splitting.IndexSet.id_fst]
        rw [comp_id]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ∀ (x : Fin (n + 2)),
    x ≠ 0 →
      ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
          ((-1) ^ ↑x • (Γ₀.obj K).δ x) ≫ (Γ₀.splitting K).πSummand (Splitting.IndexSet.id (op ⦋n⦌)) =
        0
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ Φ.f j =
    (S₁.s.cofan (op ⦋j⦌)).inj (Splitting.IndexSet.id (op ⦋j⦌)) ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j

Tactic:
Splitting.cofan_inj_πSummand_eq_id_assoc

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ Φ.f j = Φ.f j
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
⊢ (F.trans G).symm = G.symm.trans F.symm

Tactic:
ext ⟨t, _⟩
  rw [trans_apply, symm_apply, trans_apply]
  simp only [coe_symm_eq, symm_apply]
  split_ifs with h₁ h₂ h₂
  · have ht : (t : ℝ) = 1 / 2 := by linarith
    norm_num [ht]
  · congr 2
    apply Subtype.ext
    simp only [coe_symm_eq]
    linarith
  · congr 2
    apply Subtype.ext
    simp only [coe_symm_eq]
    linarith
  · exfalso
    linarith

Goal state after:
Module: Mathlib.Topology.Homotopy.Product

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

Tactic:
← Path.Homotopic.Quotient.mk_trans,

Goal state after:
case h.h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ Quotient.mk ((Path.pi a✝).trans (Path.pi a)) = pi fun i ↦ Quotient.mk (a✝ i) ⬝ Quotient.mk (a i)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : SimplyConnectedSpace X
x y : X
⊢ Nonempty (Unique (Path.Homotopic.Quotient x y))

Tactic:
by
    rw [simply_connected_iff_unique_homotopic] at *; tauto

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

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

Tactic:
by
  rw [trivialCofibrations_op, fibrations_op, ]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (terminal.from X.obj) :=
  (trivialCofibrations C).factorizationData (fibrations C) (terminal.from X.obj)
⊢ ∃ Y i, Cofibration (ι.map i) ∧ WeakEquivalence (ι.map i)

Tactic:
have := isCofibrant_of_cofibration h.i

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (terminal.from X.obj) :=
  (trivialCofibrations C).factorizationData (fibrations C) (terminal.from X.obj)
this : IsCofibrant h.Z
⊢ ∃ Y i, Cofibration (ι.map i) ∧ WeakEquivalence (ι.map i)
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
⊢ Fibration f ↔ Fibration (Over.Hom.left f)

Tactic:
by
  simp only [fibration_iff, fibrations_over_def, MorphismProperty.over_iff]

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

Goal state before:
pp: case mk.mk.mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
W✝ X✝ Y✝ Z✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient W✝.as X✝.as
f : Path W✝.as X✝.as
g✝ : Path.Homotopic.Quotient X✝.as Y✝.as
g : Path X✝.as Y✝.as
h✝ : Path.Homotopic.Quotient Y✝.as Z✝.as
h : Path Y✝.as Z✝.as
⊢ (Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid W✝.as X✝.as)) f)
          (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) g)).trans
      (Quot.mk (⇑(Path.Homotopic.setoid Y✝.as Z✝.as)) h) =
    Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid W✝.as X✝.as)) f)
      (Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) g)
        (Quot.mk (⇑(Path.Homotopic.setoid Y✝.as Z✝.as)) h))

Tactic:
exact Quotient.sound ⟨Path.Homotopy.transAssoc f g h⟩

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

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
⊢ IsColimit (c.multicofork.map Set.functorToTypes)

Tactic:
let e := (c.multispanIndex.map Set.functorToTypes).multispan

Goal state after:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
⊢ IsColimit (c.multicofork.map Set.functorToTypes)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
a : Δ[n] _⦋i⦌
ha : a ∈ A.obj (op ⦋i⦌)
⊢ a ∈ Δ[n].degenerate i

Tactic:
obtain hi | rfl := hi.lt_or_eq

Goal state after:
case inl
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi✝ : n ≤ i
a : Δ[n] _⦋i⦌
ha : a ∈ A.obj (op ⦋i⦌)
hi : n < i
⊢ a ∈ Δ[n].degenerate i

case inr
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
a : Δ[n] _⦋n⦌
ha : a ∈ A.obj (op ⦋n⦌)
⊢ a ∈ Δ[n].degenerate n
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X Y : SSet
p : X ⟶ Y
inst✝ : InnerFibration p
hY : Y.Quasicategory
⊢ X.Quasicategory

Tactic:
by
  rw [quasicategory_iff_innerFibration] at hY ⊢
  rw [Subsingleton.elim (terminal.from X) (p ≫ terminal.from Y), innerFibration_iff]
  refine innerFibrations.comp_mem _ _ InnerFibration.mem hY.mem

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

Goal state before:
pp: case refine_1
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ IsPullback (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (t i d))
    (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (l i d)) (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (r i d))
    (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))

Tactic:
exact (isPullback i d).map ((evaluation _ _).obj _)

Goal state after: