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 κ
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
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
      (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f)) =
    (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 ≫
            (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫
              Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f))

Tactic:
Iso.inv_hom_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
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
      (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f)) =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        πObj I κ f ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f))
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).F.map (homOfLE ⋯) ≫ (relativeCellComplexιObjFObjSuccIso I κ f j).hom =
    (Iso.refl ((relativeCellComplexιObj I κ f).F.obj j)).hom ≫
      ιFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom

Tactic:
by dsimp; rw [ιFunctorObj_eq, id_comp]

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
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
⊢ monomorphisms C (hf.F.map (homOfLE ⋯))

Tactic:
have := (hf.attachCells j hj).pushouts_coproducts

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
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} (ofHoms (generatingMonomorphisms G).homFamily)).pushouts (hf.F.map (homOfLE ⋯))
⊢ monomorphisms C (hf.F.map (homOfLE ⋯))
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
this : (↑p)⁻¹ < 1
⊢ ↑p ∈ nonunits ℤ_[p]

Tactic:
rwa [← norm_p, ← mem_nonunits] at this

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ maximalIdeal ℤ_[p] = Ideal.span {↑p}

Tactic:
by
  apply le_antisymm
  · intro x hx
    simp only [IsLocalRing.mem_maximalIdeal, mem_nonunits] at hx
    rwa [Ideal.mem_span_singleton, ← norm_lt_one_iff_dvd]
  · rw [Ideal.span_le, Set.singleton_subset_iff]
    exact p_nonunit

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

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ‖x‖ ≤ 1
⊢ x * (algebraMap ℤ_[p] ℚ_[p]) ↑(⟨x, hx⟩, 1).2 = (algebraMap ℤ_[p] ℚ_[p]) (⟨x, hx⟩, 1).1

Tactic:
rw [Submonoid.coe_one, map_one, mul_one, PadicInt.algebraMap_apply, Subtype.coe_mk]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ f.valuation = g.valuation ↔ f.norm = g.norm

Tactic:
norm_eq_zpow_neg_valuation hf,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ f.valuation = g.valuation ↔ ↑p ^ (-f.valuation) = g.norm
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
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p (↑(f - g) i) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
⊢ padicNorm p (↑f i) ≠ padicNorm p (-↑g i)

Tactic:
rwa [← padicNorm.neg (g i)] at h

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
a✝ : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ c.inl = c.inr

Tactic:
have : IsSplitMono φ := IsSplitMono.mk ⟨SplitMono.mk c.inl (by
      rw [← cancel_epi c.inl, reassoc_of% hφ₁, comp_id])⟩

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
a✝ : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
this : IsSplitMono φ
⊢ c.inl = c.inr
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝⁶ : Category.{v', u'} A
inst✝⁵ : LocallySmall.{w, v, u} C
inst✝⁴ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst✝³ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory A FC
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
hJ : J.HasSheafCompose (forget A)
K L : Sheaf J A
f : K ⟶ L
x✝ : ∀ (i : P.FullSubcategory), IsIso (i.obj.sheafFiber.map f)
⊢ IsIso f

Tactic:
rw [← isIso_iff_of_reflects_iso _ (sheafCompose J (forget A)),
      hP.jointlyReflectIsomorphisms_type.isIso_iff]
    exact fun Φ ↦ ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso
        (Φ.obj.sheafFiberCompIso (forget A))).app (Arrow.mk f))).2
          (inferInstanceAs (IsIso ((forget A).map (Φ.obj.sheafFiber.map f))))

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

Goal state before:
pp: case refine_1
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 : Sieve.ofArrows U f ∈ J X
Φ : P.FullSubcategory
Z Y : C
i : ι
p : Z ⟶ U i
z : Φ.obj.fiber.obj Z
⊢ ∃ i_1 y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i_1))) y = (ConcreteCategory.hom (Φ.obj.fiber.map (p ≫ f i))) z

Tactic:
exact ⟨i, Φ.obj.fiber.map p z, by simp⟩

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

Goal state before:
pp: case refine_1
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
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : Sieve.ofArrows U f ∈ J X
Φ : P.FullSubcategory
Z Y : C
i : ι
p : Z ⟶ U i
z : Φ.obj.fiber.obj Z
⊢ ∃ i_1 y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i_1))) y = (ConcreteCategory.hom (Φ.obj.fiber.map (p ≫ f i))) z

Tactic:
exact ⟨i, Φ.obj.fiber.map p z, by simp⟩

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ i ≥ N, padicNormE (Padic.mk f - ↑(↑f i)) < ε

Tactic:
by
  dsimp [padicNormE]
  -- `change ∃ N, ∀ i ≥ N, (f - const _ (f i)).norm < ε` also works, but is very slow
  suffices hyp : ∃ N, ∀ i ≥ N, (f - const _ (f i)).norm < ε by peel hyp with N; use N
  by_contra! h
  obtain ⟨N, hN⟩ := cauchy₂ f hε
  rcases h N with ⟨i, hi, hge⟩
  have hne : ¬f - const (padicNorm p) (f i) ≈ 0 := fun h ↦ by
    rw [PadicSeq.norm, dif_pos h] at hge
    exact not_lt_of_ge hge hε
  unfold PadicSeq.norm at hge; split_ifs at hge
  apply not_le_of_gt _ hge
  cases _root_.le_total N (stationaryPoint hne) with
  | inl hgen =>
    exact hN _ hgen _ hi
  | inr hngen =>
    have := stationaryPoint_spec hne le_rfl hngen
    rw [← this]
    exact hN _ le_rfl _ hi

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

Goal state before:
pp: case hbc
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 (↑(limSeq f j) - ↑f (max N N2)) + padicNormE (↑f (max N N2) - ↑(limSeq f (max N N2))) < ε

Tactic:
rw [← add_thirds ε]

Goal state after:
case hbc
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 (↑(limSeq f j) - ↑f (max N N2)) + padicNormE (↑f (max N N2) - ↑(limSeq f (max N N2))) <
    ε / 3 + ε / 3 + ε / 3
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ⇑padicNormE ↑f
q : ℚ_[p]
hq : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ ↑ε' < ε
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε'
i : ℕ
⊢ i ≥ N → ‖↑(f - const norm q) i‖ < ε

Tactic:
hi

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ⇑padicNormE ↑f
q : ℚ_[p]
hq : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ ↑ε' < ε
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε'
i : ℕ
hi : i ≥ N
⊢ ‖↑(f - const norm q) i‖ < ε
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : n < q
⊢ φ ≫ X.δ j.succ = 0

Tactic:
v j (by lia)

Goal state after:
case pos
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 φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : n < q
⊢ 0 = 0
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 ≫ (P 0).f 1 +
      (X.σ 0 ≫ (P 0).f 1 ≫ (∑ i, (-1) ^ ↑i • X.δ i) ≫ hσ' 0 0 1 ⋯ +
        X.σ 0 ≫ (P 0).f 1 ≫ hσ' 0 1 2 ⋯ ≫ ∑ i, (-1) ^ ↑i • X.δ i) =
    0

Tactic:
rw [hσ'_eq' (zero_add 0).symm, hσ'_eq' (add_zero 1).symm]

Goal state after:
case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 ≫ (P 0).f 1 +
      (X.σ 0 ≫ (P 0).f 1 ≫ (∑ i, (-1) ^ ↑i • X.δ i) ≫ ((-1) ^ 0 • X.σ ⟨0, ⋯⟩) +
        X.σ 0 ≫ (P 0).f 1 ≫ ((-1) ^ 1 • X.σ ⟨1, ⋯⟩) ≫ ∑ i, (-1) ^ ↑i • X.δ i) =
    0
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
⊢ ((P q).f (n + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) +
      ((Q q).f (n + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0

Tactic:
rw [← assoc, v.comp_P_eq_self, Preadditive.comp_add,
          comp_id, v.comp_Hσ_eq hi, assoc, ← Fin.succ_mk _ _ i.2,
          SimplicialObject.δ_comp_σ_succ_assoc,
          Fin.eta, decomposition_Q n q, sum_comp, sum_comp, Finset.sum_eq_zero, add_zero,
          add_neg_eq_zero]

Goal state after:
case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
⊢ ∀ x ∈ {i | ↑i < q},
    (((P ↑x).f (n + 1) ≫ X.δ x.rev.succ ≫ X.σ x.rev) ≫ X.σ i) ≫
        (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
      0
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: n : ℕ
j : Fin (n + 2)
inst✝ : Mono (SimplexCategory.δ j)
hi : j = 0
⊢ SimplexCategory.δ j = SimplexCategory.δ 0

Tactic:
hi

Goal state after:
n : ℕ
j : Fin (n + 2)
inst✝ : Mono (SimplexCategory.δ j)
hi : j = 0
⊢ SimplexCategory.δ 0 = SimplexCategory.δ 0
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).Factors ((P (n + 1)).f (n + 1))

Tactic:
finset_inf_factors

Goal state after:
case succ
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ ∀ i ∈ Finset.univ, (kernelSubobject (X.δ i.succ)).Factors ((P (n + 1)).f (n + 1))
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ᵒᵖ
A : Splitting.IndexSet Δ
⊢ Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) A ≫
      𝟙 (colimit (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) =
    Sigma.ι (Obj.summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ Obj.map K A.e.op

Tactic:
rw [comp_id, Γ₀.Obj.map_on_summand₀ K (SimplicialObject.Splitting.IndexSet.id A.1)
        (show A.e ≫ 𝟙 _ = A.e.op.unop ≫ 𝟙 _ by rfl), Γ₀.Obj.Termwise.mapMono_id]

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ᵒᵖ
A : Splitting.IndexSet Δ
⊢ Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) A =
    𝟙 (K.X (unop A.fst).len) ≫ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e)
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 : ℕ
i : Fin (n + 2)
⊢ i ≠ 0 →
    ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
        ((-1) ^ ↑i • (Γ₀.obj K).δ i) ≫ (Γ₀.splitting K).πSummand (Splitting.IndexSet.id (op ⦋n⦌)) =
      0

Tactic:
hi

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ Hom.cast ⋯ ⋯ e = e'

Tactic:
rw [Hom.cast_eq_iff_heq]
  exact hom_heq_of_cons_eq_cons h

Goal state after:
Module: Mathlib.Combinatorics.Quiver.SingleObj

Goal state before:
pp: α : Type u_1
l : List α
⊢ pathToList (listToPath l) = l

Tactic:
induction l with

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₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ ∀ (x : X), F (σ (1, x).1, (1, x).2) = f₀ x

Tactic:
norm_num

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)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : X
⊢ (if ↑(0, x).1 ≤ 1 / 2 then (F.extend (2 * ↑(0, x).1)) (0, x).2 else (G.extend (2 * ↑(0, x).1 - 1)) (0, x).2) = f₀ x

Tactic:
norm_num

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)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : X
⊢ (if ↑(1, x).1 ≤ 1 / 2 then (F.extend (2 * ↑(1, x).1)) (1, x).2 else (G.extend (2 * ↑(1, x).1 - 1)) (1, x).2) = f₂ x

Tactic:
norm_num

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
t : ↑I
⊢ 0 ≤ 1 / 2

Tactic:
norm_num

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
t : ↑I
⊢ 1 / 2 ≤ 1

Tactic:
norm_num

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
t : ↑I
⊢ (if ↑(t, ⟨1 / 2, ⋯⟩).2 ≤ 1 / 2 then (F.eval (t, ⟨1 / 2, ⋯⟩).1).extend (2 * ↑(t, ⟨1 / 2, ⋯⟩).2)
    else (G.eval (t, ⟨1 / 2, ⋯⟩).1).extend (2 * ↑(t, ⟨1 / 2, ⋯⟩).2 - 1)) =
    x₁

Tactic:
norm_num

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : ↑I
⊢ p ⟨↑(σ (0, x).1) * ↑(0, x).2 + ↑(0, x).1 * ↑(f (0, x).2), ⋯⟩ = p.toContinuousMap x

Tactic:
norm_num

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : ↑I
⊢ p ⟨↑(σ (1, x).1) * ↑(1, x).2 + ↑(1, x).1 * ↑(f (1, x).2), ⋯⟩ = (p.reparam f hf hf₀ hf₁).toContinuousMap x

Tactic:
norm_num

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
h : L.map f = L.map g
⊢ RightHomotopyClass.mk f = RightHomotopyClass.mk g

Tactic:
exact (bijective_rightHomotopyClassToHom L X Y).1 (by simpa)

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)
⊢ (trivialFibrations C).op.HasFactorization (fibrations Cᵒᵖ)

Tactic:
fibrations_op,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (cofibrations C).HasFactorization (trivialFibrations C)
⊢ (trivialFibrations C).op.HasFactorization (cofibrations C).op
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
γ : Homotopic.Quotient x₀ x₁
⊢ (refl x₀).trans γ = γ

Tactic:
induction γ using Quotient.ind with | mk γ =>
  simpa [← mk_trans, ← mk_refl, eq] using Homotopic.refl_trans γ

Goal state after: