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

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
⊢ (presheafMap data G₀ g ≫ restriction data G₀ f) ≫ G₀.obj.map (d.op ≫ c.op) =
    restriction data G₀ (f ≫ g) ≫ G₀.obj.map (d.op ≫ c.op)

Tactic:
rw [assoc, ← op_comp, restriction_map (i := Sieve.ofArrows.i hd)
    (p := F.map c ≫ Sieve.ofArrows.h hd) (fac := by simp; grind),
    restriction_map (i := Sieve.ofArrows.i hc) (p := Sieve.ofArrows.h hc) (fac := by simp; grind),
    presheafMap_π_assoc]

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
⊢ restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd) =
    presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ F.map p₁ ≫ Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map (p₁ ≫ a)

Tactic:
ha',

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ F.map p₁ ≫ F.map a = F.map (p₁ ≫ a)
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: case inr
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
n : ℕ
F : ComposableArrows C n
hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))
hj : ¬IsMax (Fin.last n)
⊢ W ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))

Tactic:
rw [isMax_iff_eq_top] at hj

Goal state after:
case inr
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
n : ℕ
F : ComposableArrows C n
hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))
hj : ¬Fin.last n = ⊤
⊢ W ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iic j) ⥤ C
i : J
hi : i ≤ j
⊢ arrowMap F i i ⋯ hi = Arrow.mk (𝟙 (F.obj ⟨i, hi⟩))

Tactic:
simp [arrowMap]

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₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₃ : 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
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃

Tactic:
· obtain rfl : j = k₂ := le_antisymm (by simpa using h₄) h₃
        have : restrictionLT iter₁.F le_rfl = restrictionLT iter₂.F le_rfl :=
          Arrow.functor_ext (fun _ l _ ↦ this _ _ _ _ l.2)
        by_cases h₅ : k₁ < j
        · dsimp [MapEq]
          simp_rw [arrowMap_limit _ _ h₁ _ _ h₅, this]
        · obtain rfl : k₁ = j := le_antisymm h₁₂ (by simpa using h₅)
          apply mapEq_refl
          simp only [obj_limit _ _ h₁, this]

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

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
div : p ∣ n
⊢ 1 ≤ padicValNat p n

Tactic:
← ENat.natCast_le_natCast,

Goal state after:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
div : p ∣ n
⊢ ↑1 ≤ ↑(padicValNat p n)
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:
rw [norm_eq_zpow_neg_valuation hf, norm_eq_zpow_neg_valuation hg, ← neg_inj, zpow_right_inj₀]
  · exact mod_cast (Fact.out : p.Prime).pos
  · exact mod_cast (Fact.out : p.Prime).ne_one

Goal state after:
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
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
this : Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm (𝟙 U)) ∈ J U
⊢ ∀ {U_1 : C} (s : ToType ((shrinkYoneda.{w, v, u}.obj U).obj (op U_1))), Presheaf.imageSieve f s ∈ J U_1

Tactic:
by
    intro V g
    obtain ⟨g, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective g
    replace this := J.pullback_stable g this
    rw [Presheaf.pullback_imageSieve] at this
    have hg := shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm g.op (𝟙 _)
    simp only [Quiver.Hom.unop_op, Category.comp_id] at hg
    simpa [← hg]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : MorphismProperty C
G : Cᵒᵖ ⥤ Type v₁
hP : P ≤ monomorphisms C
X : C
f : yoneda.obj X ⟶ G
hf : P.presheaf f
this : Mono f
⊢ yoneda.map (⋯.fst' f) = yoneda.map (⋯.snd f)

Tactic:
← cancel_mono f,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : MorphismProperty C
G : Cᵒᵖ ⥤ Type v₁
hP : P ≤ monomorphisms C
X : C
f : yoneda.obj X ⟶ G
hf : P.presheaf f
this : Mono f
⊢ yoneda.map (⋯.fst' f) ≫ f = yoneda.map (⋯.snd f) ≫ f
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
a : C
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
pbIso : Limits.pullback ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
    ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) ≅
  F.obj (limit (pair a a)) :=
  pullback.congrHom ⋯ ⋯ ≪≫
    (prodIsoPullback (F.obj a) (F.obj a)).symm ≪≫
      (HasLimit.isoOfNatIso (pairComp a a F)).symm ≪≫ (preservesLimitIso F (pair a a)).symm
⊢ F.relativelyRepresentable (pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯)

Tactic:
rw [← comp_id (pullback.lift _ _), ← pbIso.hom_inv_id, ← Category.assoc]

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
a : C
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
pbIso : Limits.pullback ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
    ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) ≅
  F.obj (limit (pair a a)) :=
  pullback.congrHom ⋯ ⋯ ≪≫
    (prodIsoPullback (F.obj a) (F.obj a)).symm ≪≫
      (HasLimit.isoOfNatIso (pairComp a a F)).symm ≪≫ (preservesLimitIso F (pair a a)).symm
⊢ F.relativelyRepresentable ((pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯ ≫ pbIso.hom) ≫ pbIso.inv)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
rw [norm_p]
  exact inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
⊢ ∃ q', ‖q‖ = ↑q'

Tactic:
by
  classical
  exact if h : q = 0 then ⟨0, by simp [h]⟩
  else
    let ⟨n, hn⟩ := padicNormE.image h
    ⟨_, hn⟩

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

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

Tactic:
rcases n with (_ | n)

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ (P q).f 0 ≫ (P q).f 0 = (P q).f 0

case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ (P q).f (n + 1) ≫ (P q).f (n + 1) = (P q).f (n + 1)
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ Q q ≫ Q q = Q q

Tactic:
by
  ext n
  exact Q_f_idem q n

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

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

Tactic:
simp [hf, hg, PadicSeq.valuation]

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

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑(padicNorm p q) = ↑↑p ^ (-padicValRat p q)

Tactic:
← Rat.cast_zpow,

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑(padicNorm p q) = ↑(↑p ^ (-padicValRat p q))
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ ≫ X.δ j.succ

Tactic:
rw [X.δ_comp_σ_of_gt', j.pred_succ]

Goal state after:
case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)

case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
⊢ ⟨a, ⋯⟩.succ < j.succ
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.succ ≫ X.σ i + ((P q).f n.succ ≫ X.σ i) ≫ (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:
v.comp_Hσ_eq hi,

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)
⊢ (P q).f n.succ ≫ X.σ i + -((P q).f n.succ ≫ X.σ i) ≫ X.δ ⟨↑i + 1, ⋯⟩ ≫ X.σ ⟨↑i, ⋯⟩ +
      ((Q q).f (n + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

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

Tactic:
by
  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.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).factorThru (PInfty.f (n + 1)) ⋯ ≫
      N[X].d (n + 1) n ≫ (inclusionOfMooreComplexMap X).f n =
    K[X].d (n + 1) n ≫ PInfty.f n

Tactic:
NormalizedMooreComplex.obj_d,

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).factorThru (PInfty.f (n + 1)) ⋯ ≫
      ChainComplex.of.d (fun n ↦ underlying.obj (NormalizedMooreComplex.objX X n)) (NormalizedMooreComplex.objD X)
          (n + 1) n ≫
        (inclusionOfMooreComplexMap X).f n =
    K[X].d (n + 1) n ≫ PInfty.f n
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
h : (unop A.fst).len ≤ (unop (op ⦋n⦌)).len
⊢ ¬(unop (A.epiComp (SimplexCategory.σ i).op).fst).len = (unop (op ⦋n + 1⦌)).len

Tactic:
dsimp at h ⊢

Goal state after:
case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
h : (unop A.fst).len ≤ n
⊢ ¬(unop A.fst).len = n + 1
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
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Tactic:
by
  apply s.hom_ext'
  intro A
  dsimp only [SimplicialObject.σ]
  rw [comp_zero, s.cofan_inj_epi_naturality_assoc A (SimplexCategory.σ i).op,
    cofan_inj_πSummand_eq_zero]
  rw [ne_comm]
  change ¬(A.epiComp (SimplexCategory.σ i).op).EqId
  rw [IndexSet.eqId_iff_len_eq]
  have h := SimplexCategory.len_le_of_epi A.e
  dsimp at h ⊢
  lia

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

Goal state before:
pp: case pos.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∀ b ∈ Finset.univ, b ≠ 0 → PInfty.f (n + 1) ≫ ((-1) ^ ↑b • X.δ b) = 0

Tactic:
intro b _ hb
      rw [Preadditive.comp_zsmul, SimplicialObject.δ,
        PInfty_comp_map_mono_eq_zero X (SimplexCategory.δ b) h
          (by
            rw [Isδ₀.iff]
            exact hb),
        zsmul_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
n : ℕ
⊢ ({ f := { f := fun n ↦ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n, comm' := ⋯ }, comm := ⋯ } ≫
            { f := { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ }).f.f
      n =
    (𝟙 ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex)).f.f n

Tactic:
simp only [assoc, PInfty_comp_πSummand_id, Karoubi.comp_f, HomologicalComplex.comp_f,
      cofan_inj_πSummand_eq_id]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ 𝟙 (summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌))) = (𝟙 ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex)).f.f n
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 : ℕ
⊢ (Γ₀.splitting K[X]).ι n ≫
      ((Γ₀.splitting K[X]).desc (op ⦋n⦌) fun A ↦
          PInfty.f (unop A.fst).len ≫ ((Γ₀.splitting K[X]).cofan (op ⦋n⦌)).inj A) ≫
        ((Γ₀.splitting K[X]).desc (op ⦋n⦌) fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op) ≫ 𝟙 (X _⦋n⦌) =
    (Γ₀.splitting K[X]).ι n ≫ (Γ₀.splitting K[X]).desc (op ⦋n⦌) fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op

Tactic:
simp only [← Splitting.cofan_inj_id, Splitting.ι_desc, comp_id, Splitting.ι_desc_assoc,
          assoc, PInfty_f_idem_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
⊢ projRight (prod q₁ q₂) = q₂

Tactic:
induction q₁, q₂ using Path.Homotopic.Quotient.ind₂
  rw [projRight, prod_lift, ← Path.Homotopic.Quotient.mk_map]
  congr

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Nonempty Y
inst✝ : IndiscreteTopology Y
f : C(X, Y)
⊢ f.Nullhomotopic

Tactic:
by
  inhabit Y
  use default
  exact homotopic_of_indiscrete _ _

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

Goal state before:
pp: case intro
Y : Type u_2
inst✝ : TopologicalSpace Y
left✝ : PathConnectedSpace Y
right✝ : ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ SimplyConnectedSpace Y

Tactic:
rw [simply_connected_iff_unique_homotopic]

Goal state after:
case intro
Y : Type u_2
inst✝ : TopologicalSpace Y
left✝ : PathConnectedSpace Y
right✝ : ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ Nonempty Y ∧ ∀ (x y : Y), Nonempty (Unique (Path.Homotopic.Quotient x y))
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y x' y' : X
hx : x' = x
hy : y' = y
γ : Homotopic.Quotient x y
⊢ γ.cast hx hy ≍ γ

Tactic:
cases hx; cases hy; exact heq_of_eq γ.cast_rfl_rfl

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

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)

Tactic:
rw [simply_connected_iff_paths_homotopic']
  constructor
  · -- Forward: all paths homotopic implies all loops null-homotopic
    intro ⟨hpc, hall⟩
    exact ⟨hpc, fun x γ => hall γ (Path.refl x)⟩
  · -- Backward: all loops null-homotopic implies all paths homotopic
    intro ⟨hpc, hloops⟩
    refine ⟨hpc, fun {x y} p₁ p₂ => ?_⟩
    -- Work in the quotient where structural steps can be done by simp
    rw [← eq]
    replace hloops : ∀ (x : Y) (γ : Path x x),
        (⟦γ⟧ : Path.Homotopic.Quotient x x) = ⟦Path.refl x⟧ :=
      fun x γ => Quotient.sound (hloops x γ)
    have h : trans ⟦p₁⟧ (symm ⟦p₂⟧) = refl x := by
      simpa using hloops x (p₁.trans p₂.symm)
    calc ⟦p₁⟧
      _ = trans (trans ⟦p₁⟧ (symm ⟦p₂⟧)) ⟦p₂⟧ := by simp
      _ = ⟦p₂⟧ := by grind

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : C
f : X ⟶ Y
sq : CommSq (initial.to (resolutionObj Y)) (initial.to (resolutionObj X)) (pResolutionObj Y) (pResolutionObj X ≫ f)
⊢ ∃ g, g ≫ pResolutionObj Y = pResolutionObj X ≫ f

Tactic:
exact ⟨sq.lift, sq.fac_right⟩

Goal state after: