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
this✝¹ : HasIterationOfShape κ.ord.ToType C
this✝ : NoMaxOrder κ.ord.ToType
this :
  (((succStruct I κ).iterationFunctor κ.ord.ToType).map (homOfLE ⋯)).app f =
    ((succStruct I κ).toSucc (((succStruct I κ).iterationFunctor κ.ord.ToType).obj j)).app f ≫
      ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).inv.app f
⊢ Arrow.homMk (ιFunctorObj I.homFamily ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f).hom)
      (𝟙 ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f).right) ⋯ =
    (((succStruct I κ).iterationFunctor κ.ord.ToType).map (homOfLE ⋯)).app f ≫
      ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).hom.app f

Tactic:
this,

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✝¹ : HasIterationOfShape κ.ord.ToType C
this✝ : NoMaxOrder κ.ord.ToType
this :
  (((succStruct I κ).iterationFunctor κ.ord.ToType).map (homOfLE ⋯)).app f =
    ((succStruct I κ).toSucc (((succStruct I κ).iterationFunctor κ.ord.ToType).obj j)).app f ≫
      ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).inv.app f
⊢ Arrow.homMk (ιFunctorObj I.homFamily ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f).hom)
      (𝟙 ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f).right) ⋯ =
    (((succStruct I κ).toSucc (((succStruct I κ).iterationFunctor κ.ord.ToType).obj j)).app f ≫
        ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).inv.app f) ≫
      ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).hom.app f
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
⊢ A ≤ largerSubobject hG A

Tactic:
by
  by_cases hA : A = ⊤
  · subst hA
    simp only [largerSubobject_top, le_refl]
  · exact (lt_largerSubobject hG A hA).le

Goal state after:
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
l : (↑⟨Arrow.mk i, hi⟩).right ⟶ (relativeCellComplexιObj I κ f).F.obj (Order.succ j)
hl₁ : i ≫ l = t ≫ (relativeCellComplexιObj I κ f).F.map (homOfLE ⋯)
hl₂ : l ≫ (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ πObj I κ f = b
⊢ i ≫ l ≫ (relativeCellComplexιObj I κ f).incl.app (Order.succ j) = g

Tactic:
simp [reassoc_of% hl₁, ← ht]

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

Goal state before:
pp: case mpr
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ (↑p)⁻¹ < padicNorm p ↑m → padicNorm p ↑m = 1

Tactic:
simp only [padicNorm]

Goal state after:
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ ((↑p)⁻¹ < if ↑m = 0 then 0 else ↑p ^ (-padicValRat p ↑m)) → (if ↑m = 0 then 0 else ↑p ^ (-padicValRat p ↑m)) = 1
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ↑m = 0
⊢ (↑p)⁻¹ < 0 → 0 = 1

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
⊢ (↑p)⁻¹ < ↑p ^ (-padicValRat p ↑m) → ↑p ^ (-padicValRat p ↑m) = 1

Tactic:
· rw [inv_lt_zero, ← Nat.cast_zero, Nat.cast_lt]
      intro h
      exact (Nat.not_lt_zero p h).elim

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
⊢ (↑p)⁻¹ < ↑p ^ (-padicValRat p ↑m) → ↑p ^ (-padicValRat p ↑m) = 1
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
f : CauSeq ℤ_[p] norm
hqn : ‖(cauSeq_to_rat_cauSeq f).lim‖ ≤ 1
ε : ℝ
⊢ ε > 0 → ∃ i, ∀ j ≥ i, ‖↑(f - CauSeq.const norm ⟨(cauSeq_to_rat_cauSeq f).lim, hqn⟩) j‖ < ε

Tactic:
simpa [norm, norm_def] using! CauSeq.equiv_lim (cauSeq_to_rat_cauSeq f) ε

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

Goal state before:
pp: case ha
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑p ≠ 0

Tactic:
· exact NeZero.ne _

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

Goal state before:
pp: p n k b : ℕ
hp : Fact (Nat.Prime p)
hnb : log p (n + k) < b
⊢ padicValNat p ((n + k).choose k) = #({i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})

Tactic:
by
  exact_mod_cast (padicValNat_eq_emultiplicity (p := p) <| choose_ne_zero <|
    Nat.le_add_left k n) ▸ Prime.emultiplicity_choose' hp.out hnb

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

Goal state before:
pp: case coe.ofAdd.inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
hx : x < 0
⊢ ∃ a,
    { toFun := fun x ↦ if x = 0 then 0 else ↑(Multiplicative.ofAdd (-padicValRat p x)), map_zero' := ⋯ } a =
      ↑(Multiplicative.ofAdd x)

Tactic:
· exact ⟨p ^ x.natAbs, by simp [hp.out.ne_zero, padicValRat.pow, abs_eq_neg_self.2 hx.le]⟩

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ≠ 0

Tactic:
· exact NeZero.ne _

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 G : Sheaf J AddCommGrpCat
n : ℕ
f g : F ⟶ G
x : F.H n
⊢ (map (f + g) n) x = (map f n) x + (map g n) x

Tactic:
simp [map, Ext.mk₀_add]

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

Goal state before:
pp: case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ ?a.b✝

pp: case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ ?a.b✝ ≤ max v1 (max v2 (stationaryPoint hf))

pp: case a.b
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ ℕ

Tactic:
· apply le_max_right v2

Goal state after:
case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ max v2 (stationaryPoint hf) ≤ max v1 (max v2 (stationaryPoint hf))
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
exact if hf : f ≈ 0 then by
    have hg : g ≈ 0 := Setoid.trans (Setoid.symm hfg) hf
    simp [norm, hf, hg]
  else by
    have hg : ¬g ≈ 0 := hf ∘ Setoid.trans hfg
    unfold norm; split_ifs; exact norm_eq_of_equiv hf hg hfg

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
Φ : P.FullSubcategory
i : ι
y : Φ.obj.fiber.obj (U i)
this :
  (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app X))
      ((ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y) =
    (ConcreteCategory.hom (Φ.obj.presheafFiber.map (shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)
⊢ (ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.ι (fun i ↦ shrinkYoneda.{w, v, u}.obj (U i)) i)))
        ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app X))
      ((ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y)

Tactic:
this,

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
Φ : P.FullSubcategory
i : ι
y : Φ.obj.fiber.obj (U i)
this :
  (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app X))
      ((ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y) =
    (ConcreteCategory.hom (Φ.obj.presheafFiber.map (shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)
⊢ (ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.ι (fun i ↦ shrinkYoneda.{w, v, u}.obj (U i)) i)))
        ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)) =
    (ConcreteCategory.hom (Φ.obj.presheafFiber.map (shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
⊢ ∃ l,
    ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj.left),
      l ≫ Pi.π (fun x ↦ M) ((ConcreteCategory.hom (Φ.fiber.map j.obj.hom)) y) = s.π.app (op j) ≫ Pi.π (fun t ↦ M) y

Tactic:
by
  suffices ∀ (x : Φ.fiber.obj X), ∃ (l : s.pt ⟶ M),
      ∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R g) (y : Φ.fiber.obj Y) (hy : Φ.fiber.map g y = x),
        s.π.app (op (Presieve.categoryMk _ _ hg)) ≫ Pi.π _ y = l by
    choose l hl using this
    exact ⟨Pi.lift l, fun j y ↦ by simpa using! (hl _ j.obj.hom  j.property y rfl).symm⟩
  intro x
  obtain ⟨Y₁, f₁, hf₁, y₁, hy₁⟩ := Φ.jointly_surjective _ hR x
  refine ⟨s.π.app (op (Presieve.categoryMk _ _ hf₁)) ≫ Pi.π _ y₁,
    fun Y₂ f₂ hf₂ y₂ hy₂ ↦ ?_⟩
  obtain ⟨Z, p₁, p₂, z, fac, hz₁, hz₂⟩ :
      ∃ (Z : C) (p₁ : Z ⟶ Y₁) (p₂ : Z ⟶ Y₂) (z : Φ.fiber.obj Z), p₁ ≫ f₁ = p₂ ≫ f₂ ∧
        Φ.fiber.map p₁ z = y₁ ∧ Φ.fiber.map p₂ z = y₂ := by
    let α₁ : Φ.fiber.elementsMk _ y₁ ⟶ Φ.fiber.elementsMk _ x := ⟨f₁, hy₁⟩
    let α₂ : Φ.fiber.elementsMk _ y₂ ⟶ Φ.fiber.elementsMk _ x := ⟨f₂, hy₂⟩
    obtain ⟨z, q₁, q₂, fac⟩ := IsCofiltered.cospan α₁ α₂
    rw [Subtype.ext_iff] at fac
    refine ⟨z.1, q₁.1, q₂.1, z.2, fac, ?_, ?_⟩
    all_goals rw [CategoryOfElements.map_snd] -- was `simp`
  let φ₁ : Presieve.categoryMk _ _ (R.downward_closed hf₁ p₁) ⟶
      Presieve.categoryMk _ _ hf₁ :=
    ObjectProperty.homMk (Over.homMk p₁)
  let φ₂ : Presieve.categoryMk _ _ (R.downward_closed hf₁ p₁) ⟶
      Presieve.categoryMk _ _ hf₂ :=
    ObjectProperty.homMk (Over.homMk p₂)
  simpa [hz₁, hz₂, φ₁, φ₂] using!
    (Cone.w s φ₂.op =≫ Pi.π _ z).trans (Cone.w s φ₁.op =≫ Pi.π _ z).symm

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
this : max f.norm g.norm = g.norm
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
this,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
this : max f.norm g.norm = g.norm
⊢ (f + g).norm ≤ g.norm
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
this : max f.norm g.norm = f.norm
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
this,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
this : max f.norm g.norm = f.norm
⊢ (f + g).norm ≤ f.norm
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑f (max N N2) - ↑(limSeq f (max N N2))) < ε / 3

Tactic:
apply mod_cast hN (max N N2)

Goal state after:
case h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ max N N2 ≥ N
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
⊢ ∃ N, ∀ i ≥ N, padicNormE (lim f - ↑f i) < ε

Tactic:
obtain ⟨N, hN⟩ := exi_rat_seq_conv f (half_pos hε)
    obtain ⟨N2, hN2⟩ := padicNormE.defn (lim' f) (half_pos hε)
    refine ⟨max N N2, fun i hi ↦ ?_⟩
    rw [← sub_add_sub_cancel _ (lim' f i : ℚ_[p]) _]
    refine (padicNormE.add_le _ _).trans_lt ?_
    rw [← add_halves ε]
    apply _root_.add_lt_add
    · apply hN2 _ (le_of_max_le_right hi)
    · rw [padicNormE.map_sub]
      exact hN _ (le_of_max_le_left hi)

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

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

Tactic:
norm_p

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (↑p)⁻¹ < 1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
norm_p

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ (↑p)⁻¹ < 1
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 x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
q : ℕ
hq : (alternatingFaceMapComplex C).map f ≫ P q = P q ≫ (alternatingFaceMapComplex C).map f
⊢ (alternatingFaceMapComplex C).map f ≫ P (q + 1) = P (q + 1) ≫ (alternatingFaceMapComplex C).map f

Tactic:
simp only [P_succ, add_comp, comp_add, assoc, comp_id, hq, reassoc_of% hq]
      -- `erw` is needed to see through `natTransHσ q).app = Hσ q`
      erw [(natTransHσ q).naturality f]
      rfl

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
⊢ X.σ i ≫ (P (q + 1)).f (n + 1 + 1) = 0

Tactic:
rw [← id_comp (X.σ i), ← (P_add_Q_f q n.succ : _ = 𝟙 (X.obj _)), add_comp, add_comp,
          P_succ]

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
⊢ ((P q).f n.succ ≫ X.σ i) ≫ (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)).f (n + 1 + 1) +
      ((Q q).f n.succ ≫ X.σ i) ≫ (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)).f (n + 1 + 1) =
    0
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 U : C
g : T ⟶ U
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf : DegeneraciesVanish f
⊢ DegeneraciesVanish (f ≫ g)

Tactic:
simp [degeneraciesVanish_succ_iff, hf.σ_comp_assoc]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac :
  factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫
      image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e) =
    (θ' ≫ θ).unop ≫ A.e
⊢ colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K (θ' ≫ θ) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K θ' ≫ Obj.map K θ

Tactic:
simp only [Obj.map_on_summand₀'_assoc K A θ', Obj.map_on_summand₀' K _ θ,
      Obj.Termwise.mapMono_comp_assoc, Obj.map_on_summand₀ K A fac]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac :
  factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫
      image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e) =
    (θ' ≫ θ).unop ≫ A.e
⊢ Obj.Termwise.mapMono K (image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e)) ≫
      Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk (factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)))) =
    Obj.Termwise.mapMono K (image.ι (θ.unop ≫ (A.pull θ').e) ≫ image.ι (θ'.unop ≫ A.e)) ≫
      Sigma.ι (Obj.summand K Δ) ((A.pull θ').pull θ)
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ ((splitting K).cofan Δ).inj A ≫ (obj K).map θ =
    Termwise.mapMono K i ≫ ((splitting K).cofan Δ').inj (Splitting.IndexSet.mk e)

Tactic:
dsimp [Splitting.cofan]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ ((splitting K).ι (unop A.fst).len ≫ map K A.e.op) ≫ map K θ =
    Termwise.mapMono K i ≫ (splitting K).ι Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op
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
X : ChainComplex C ℕ
⊢ (N₂Γ₂ToKaroubiIso.hom.app X).f = PInfty

Tactic:
ext n
  dsimp [N₂Γ₂ToKaroubiIso]
  simp only [comp_id, assoc, PInfty_f_idem]
  conv_rhs =>
    rw [← PInfty_f_idem]
  congr 1
  apply (Γ₀.splitting X).hom_ext'
  intro A
  rw [Splitting.ι_desc_assoc, assoc]
  apply id_comp

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

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

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
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Tactic:
· dsimp at h
      rw [comp_id] at h
      rw [h, zero_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor =
    karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
      N₁ ⋙
        (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
          (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)

Tactic:
by
  refine CategoryTheory.Functor.ext (fun P => ?_) fun P Q f => ?_
  · refine HomologicalComplex.ext ?_ ?_
    · ext n
      · rfl
      · dsimp
        simp only [karoubi_PInfty_f, comp_id, PInfty_f_naturality, id_comp]
    · rintro _ n (rfl : n + 1 = _)
      ext
      have h := (AlternatingFaceMapComplex.map P.p).comm (n + 1) n
      dsimp [N₂, karoubiChainComplexEquivalence,
        KaroubiHomologicalComplexEquivalence.Functor.obj] at h ⊢
      simp only [assoc, Karoubi.eqToHom_f, eqToHom_refl, comp_id,
        karoubi_alternatingFaceMapComplex_d, karoubi_PInfty_f,
        ← HomologicalComplex.Hom.comm_assoc, ← h, app_idem_assoc]
  · ext n
    dsimp [KaroubiKaroubi.inverse, Functor.mapHomologicalComplex]
    simp only [karoubi_PInfty_f, HomologicalComplex.eqToHom_f, Karoubi.eqToHom_f,
      assoc, comp_id, PInfty_f_naturality, app_p_comp,
      karoubiChainComplexEquivalence_functor_obj_X_p, N₂_obj_p_f, eqToHom_refl,
      PInfty_f_naturality_assoc, app_comp_p, PInfty_f_idem_assoc]

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
⊢ s.toKaroubiNondegComplexIsoN₁.hom.f ≫ s.toKaroubiNondegComplexIsoN₁.inv.f = 𝟙 s.nondegComplex

Tactic:
rw [← dsimp% [-Karoubi.comp_f] Karoubi.comp_f s.toKaroubiNondegComplexIsoN₁.hom
    s.toKaroubiNondegComplexIsoN₁.inv, Iso.hom_inv_id]
  simp

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
⊢ (toKaroubi (ChainComplex C ℕ)).map (PInfty ≫ s.toNondegComplex) = (toKaroubi (ChainComplex C ℕ)).map s.toNondegComplex

Tactic:
simp [toNondegComplex]

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀✝ f₁✝ f₂ : C(X, Y)
S : Set X
f₀ f₁ g₀ g₁ : C(X, Y)
F : f₀.HomotopyRel f₁ S
h₀ : f₀ = g₀
h₁ : f₁ = g₁
t : ↑I
x : X
hx : x ∈ S
⊢ { toFun := fun x ↦ (F.cast h₀ h₁).toFun (t, x), continuous_toFun := ⋯ } x = g₀ x

Tactic:
by simpa only [← h₀, ← h₁] using! F.prop t x hx

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ ((h₁.invFun.comp h₂.invFun).comp (h₂.toFun.comp h₁.toFun)).Homotopic (ContinuousMap.id X)

Tactic:
refine Homotopic.trans ?_ h₁.left_inv

Goal state after:
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ ((h₁.invFun.comp h₂.invFun).comp (h₂.toFun.comp h₁.toFun)).Homotopic (h₁.invFun.comp h₁.toFun)