mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
X✝ : Sheaf J A
Y✝ Y'✝ : A
f : Φ.sheafFiber.obj X✝ ⟶ Y✝
g : Y✝ ⟶ Y'✝
⊢ (Φ.skyscraperPresheafHomEquiv.trans (fullyFaithfulSheafToPresheaf J A).homEquiv.symm) (f ≫ g) =
    (Φ.skyscraperPresheafHomEquiv.trans (fullyFaithfulSheafToPresheaf J A).homEquiv.symm) f ≫
      Φ.skyscraperSheafFunctor.map g

Tactic:
by
        ext : 1
        exact Φ.skyscraperPresheafHomEquiv_naturality_right f g

Goal state after:
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✝² : F.Full
inst✝¹ : HasPullbacks C
a b : C
f : a ⟶ b
inst✝ : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
c : C
g : F.obj c ⟶ F.obj b
⊢ ∃ b_1 snd fst, IsPullback fst (F.map snd) (F.map f) g

Tactic:
obtain ⟨g, rfl⟩ := F.map_surjective g
  refine ⟨Limits.pullback f g, Limits.pullback.snd f g, F.map (Limits.pullback.fst f g), ?_⟩
  apply F.map_isPullback <| IsPullback.of_hasPullback f g

Goal state after:
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✝² : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst✝¹ : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst✝ : F.Faithful
Z : C
x₁ : Z ⟶ A₁
x₂ : Z ⟶ A₂
x₃ : Z ⟶ A₃
h₁₂ : F.map x₁ ≫ f₁ = F.map x₂ ≫ f₂
h₁₃ : F.map x₁ ≫ f₁ = F.map x₃ ≫ f₃
⊢ hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃ ≫ pullback₃.p₂ hf₁ f₂ f₃ = x₂

Tactic:
simp [lift₃, pullback₃.p₂]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
⊢ (x * y).valuation = x.valuation + y.valuation

Tactic:
have hp_pos : (0 : ℝ) < p := mod_cast NeZero.pos _

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ (x * y).valuation = x.valuation + y.valuation
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
hp_ne_one : ↑p ≠ 1
⊢ x⁻¹.valuation = -x.valuation

Tactic:
have hp_pos : (0 : ℝ) < p := mod_cast NeZero.pos _

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ x⁻¹.valuation = -x.valuation
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  PInfty.f n =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
π : Y₄ ⟶ Y₄ := (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p
eq : (π.app (op ⦋n⦌) ≫ PInfty.f n).f = (PInfty.f n ≫ π.app (op ⦋n⦌)).f
⊢ Y.p.app (op ⦋n⦌) ≫ (PInfty.f n).f ≫ Y.p.app (op ⦋n⦌) = Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f

Tactic:
simp only [Karoubi.comp_f] at eq

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  PInfty.f n =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
π : Y₄ ⟶ Y₄ := (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p
eq : (π.app (op ⦋n⦌)).f ≫ (PInfty.f n).f = (PInfty.f n).f ≫ (π.app (op ⦋n⦌)).f
⊢ Y.p.app (op ⦋n⦌) ≫ (PInfty.f n).f ≫ Y.p.app (op ⦋n⦌) = Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + (q + 1)
h : n + 1 ≤ ↑i + q
⊢ (X.σ i ≫ (P q).f (n + 1)) ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q).f (n + 1) = 0

Tactic:
hq i h,

Goal state after:
case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + (q + 1)
h : n + 1 ≤ ↑i + q
⊢ 0 ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q).f (n + 1) = 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.succ ≫ X.σ i + -(P q).f n.succ ≫ X.σ i +
      ∑ j with ↑j < q,
        (((P ↑j).f (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
          (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0

Tactic:
Finset.sum_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)
⊢ (P q).f n.succ ≫ X.σ i + -(P q).f n.succ ≫ X.σ i + 0 = 0

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: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
⊢ K.X Δ.len ⟶ K.X Δ'.len

Tactic:
by_cases Δ = Δ'
  · exact eqToHom (by congr)
  · by_cases Isδ₀ i
    · exact K.d Δ.len Δ'.len
    · exact 0

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 : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
⊢ ¬Isδ₀ (i' ≫ i)

pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = 0

Tactic:
· by_contra h
    simp only [h.1, add_right_inj] at eq
    lia

Goal state after:
case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = 0
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 =
    K.d (n + 1) n ≫
      ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
        (Γ₀.splitting K).πSummand (Splitting.IndexSet.id (op ⦋n⦌))

Tactic:
Splitting.cofan_inj_πSummand_eq_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 : ℕ
⊢ K.d (n + 1) n = K.d (n + 1) n ≫ 𝟙 (Splitting.summand (Γ₀.splitting K).N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)))
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₁ : ∀ (i : ℕ), (N₁.map f ≫ inv (N₁.map f)).f.f i = (𝟙 (N₁.obj X)).f.f i
⊢ ∀ (n : ℕ), IsIso (f.app (op ⦋n⦌))

Tactic:
have h₂ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.inv_hom_id (N₁.map f)))

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₁ : ∀ (i : ℕ), (N₁.map f ≫ inv (N₁.map f)).f.f i = (𝟙 (N₁.obj X)).f.f i
h₂ : ∀ (i : ℕ), (inv (N₁.map f) ≫ N₁.map f).f.f i = (𝟙 (N₁.obj Y)).f.f i
⊢ ∀ (n : ℕ), IsIso (f.app (op ⦋n⦌))
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq :
  K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) +
      ∑ j_1 ∈ {IndexSet.id (op ⦋j⦌)}ᶜ,
        K[X].d i j ≫ (s.πSummand j_1 ≫ (s.cofan (op ⦋j⦌)).inj j_1) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫
      K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0

Tactic:
Finset.sum_eq_zero,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq :
  K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) +
      0 =
    0
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫
      K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0

C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq :
  K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) +
      ∑ j_1 ∈ {IndexSet.id (op ⦋j⦌)}ᶜ,
        K[X].d i j ≫ (s.πSummand j_1 ≫ (s.cofan (op ⦋j⦌)).inj j_1) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0
⊢ ∀ x ∈ {IndexSet.id (op ⦋j⦌)}ᶜ,
    K[X].d i j ≫ (s.πSummand x ≫ (s.cofan (op ⦋j⦌)).inj x) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0
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 ≫ PInfty = s.toKaroubiNondegComplexIsoN₁.hom.f

Tactic:
by
  simpa using s.toKaroubiNondegComplexIsoN₁.hom.comm

Goal state after:
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 (unop (Splitting.IndexSet.id (op ⦋j⦌)).fst).len ≫
      (S₂.s.cofan (op ⦋j⦌)).inj (Splitting.IndexSet.id (op ⦋j⦌)) ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋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

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 (unop (Splitting.IndexSet.id (op ⦋j⦌)).fst).len ≫
      𝟙 (Splitting.summand S₂.s.N (op ⦋j⦌) (Splitting.IndexSet.id (op ⦋j⦌))) =
    (S₁.s.cofan (op ⦋j⦌)).inj (Splitting.IndexSet.id (op ⦋j⦌)) ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j
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
P : Karoubi (SimplicialObject C)
h : N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂N₂.natTrans.app P) = 𝟙 (N₂.obj P)
⊢ IsIso (N₂.map (Γ₂N₂.natTrans.app P))

Tactic:
rw [hom_comp_eq_id] at h

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
h : N₂.map (Γ₂N₂.natTrans.app P) = inv (N₂Γ₂.inv.app (N₂.obj P))
⊢ IsIso (N₂.map (Γ₂N₂.natTrans.app P))
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: ⊢ {J : Type u} → (f : J → Grpd) → Limits.Fan f

Tactic:
by apply piLimitFan

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

Goal state before:
pp: case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : ↑I
hx : x ∈ {1}
⊢ { toFun := fun x ↦ F ((t, x).1, σ (t, x).2), continuous_toFun := ⋯ } x = p.symm.toContinuousMap x

Tactic:
· rw [Set.mem_singleton_iff] at hx
      rw [hx]
      simp

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

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
a✝ : X
⊢ (∀ (x y : FundamentalGroupoid X), Nonempty (Unique (x ⟶ y))) ↔
    ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))

Tactic:
exact ⟨fun h _ _ => h _ _, fun h _ _ => h _ _⟩

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 : CofibrantObject C
f g : X ⟶ Y
h✝ : homRel C f g
P : PathObject Y.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject C ⥤ (weakEquivalences (CofibrantObject C)).Localization := (weakEquivalences (CofibrantObject C)).Q
⊢ weakEquivalences (CofibrantObject C) (homMk P.ι)

Tactic:
by
    simp only [← weakEquivalence_iff, weakEquivalence_homMk_iff]
    infer_instance

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 : LeftHomotopyClass X Y
⊢ leftHomotopyClassToHom L f = (rightHomotopyClassToHom L ∘ ⇑leftHomotopyClassEquivRightHomotopyClass) f

Tactic:
obtain ⟨f, rfl⟩ := f.mk_surjective

Goal state after:
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 : X ⟶ Y
⊢ leftHomotopyClassToHom L (LeftHomotopyClass.mk f) =
    (rightHomotopyClassToHom L ∘ ⇑leftHomotopyClassEquivRightHomotopyClass) (LeftHomotopyClass.mk f)
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
this✝ : ∀ (Y : C) [IsFibrant Y], IsCofibrant Y → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsCofibrant Y
Y' : C
w✝ : IsCofibrant Y'
p : Y' ⟶ Y
left✝ : Fibration p
right✝ : WeakEquivalence p
x✝ : IsFibrant Y'
hY' : Function.Bijective (leftHomotopyClassToHom L)
this : IsIso (L.map p)
f : LeftHomotopyClass X Y'
⊢ (leftHomotopyClassToHom L ∘ fun f ↦ f.postcomp p) f =
    (⇑((Iso.refl (L.obj X)).homCongr (asIso (L.map p))) ∘ leftHomotopyClassToHom L) f

Tactic:
obtain ⟨f, rfl⟩ := f.mk_surjective

Goal state after:
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
this✝ : ∀ (Y : C) [IsFibrant Y], IsCofibrant Y → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsCofibrant Y
Y' : C
w✝ : IsCofibrant Y'
p : Y' ⟶ Y
left✝ : Fibration p
right✝ : WeakEquivalence p
x✝ : IsFibrant Y'
hY' : Function.Bijective (leftHomotopyClassToHom L)
this : IsIso (L.map p)
f : X ⟶ Y'
⊢ (leftHomotopyClassToHom L ∘ fun f ↦ f.postcomp p) (LeftHomotopyClass.mk f) =
    (⇑((Iso.refl (L.obj X)).homCongr (asIso (L.map p))) ∘ leftHomotopyClassToHom L) (LeftHomotopyClass.mk f)
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
Y : C
inst✝ : IsFibrant Y
h✝¹ : IsCofibrant Y
this✝ : ∀ (X : C) [IsCofibrant X], IsFibrant X → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsFibrant X
X' : C
i : X ⟶ X'
left✝¹ : Cofibration i
left✝ : WeakEquivalence i
right✝ : IsFibrant X'
x✝ : IsCofibrant X'
hX' : Function.Bijective (rightHomotopyClassToHom L)
this : IsIso (L.map i)
f : RightHomotopyClass X' Y
⊢ (rightHomotopyClassToHom L ∘ fun g ↦ g.precomp i) f =
    (⇑((asIso (L.map i)).homCongr (Iso.refl (L.obj Y))).symm ∘ rightHomotopyClassToHom L) f

Tactic:
obtain ⟨f, rfl⟩ := f.mk_surjective

Goal state after:
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
Y : C
inst✝ : IsFibrant Y
h✝¹ : IsCofibrant Y
this✝ : ∀ (X : C) [IsCofibrant X], IsFibrant X → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsFibrant X
X' : C
i : X ⟶ X'
left✝¹ : Cofibration i
left✝ : WeakEquivalence i
right✝ : IsFibrant X'
x✝ : IsCofibrant X'
hX' : Function.Bijective (rightHomotopyClassToHom L)
this : IsIso (L.map i)
f : X' ⟶ Y
⊢ (rightHomotopyClassToHom L ∘ fun g ↦ g.precomp i) (RightHomotopyClass.mk f) =
    (⇑((asIso (L.map i)).homCongr (Iso.refl (L.obj Y))).symm ∘ rightHomotopyClassToHom L) (RightHomotopyClass.mk f)
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

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

Tactic:
rw [cofibrations_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
D : Type u_1
inst✝ : Category.{v_1, u_1} D
⊢ ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → toHoCat.map f = toHoCat.map g

Tactic:
intro K

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K : BifibrantObject C
⊢ ∀ ⦃L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → toHoCat.map f = toHoCat.map g
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence (HoCat.adjUnit.app (toHoCat.obj X))

Tactic:
HoCat.adjUnit_app,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence (toHoCat.map X.iBifibrantResolutionObj)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

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

Tactic:
exact Quotient.sound ⟨Path.Homotopy.reflTrans f⟩

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

Goal state before:
pp: case mp
n d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1) → ∃ j_1, ∀ (x : Fin (d + 1)), ¬j x = j_1

Tactic:
· rintro ⟨k, hk⟩
    exact ⟨k.rev, fun l _ ↦ hk l.rev (by aesop)⟩

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

Goal state before:
pp: case mpr
n d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ∀ (x : Fin (d + 1)), ¬j x = j_1) → ∃ j_1, ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1

Tactic:
· rintro ⟨k, hk⟩
    exact ⟨k.rev, fun l _ ↦ hk l.rev (by aesop)⟩

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Mono (stdSimplex.δ i)

Tactic:
by
  rw [← ι_ι]
  infer_instance

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

Goal state before:
pp: case a.right
⊢ stdSimplex.face {0, 2} ≤ Λ[2, 0]

Tactic:
exact face_le_horn (1 : Fin 3) 0 (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
⊢ (α_ X.fst Y.fst (U ⊗ U')).hom ≫
      X.fst ◁
          ((α_ Y.fst U U').inv ≫
            (Y.snd.β U).hom ▷ U' ≫ (α_ U Y.fst U').hom ≫ U ◁ (Y.snd.β U').hom ≫ (α_ U U' Y.fst).inv) ≫
        (α_ X.fst (U ⊗ U') Y.fst).inv ≫
          ((α_ X.fst U U').inv ≫
                (X.snd.β U).hom ▷ U' ≫ (α_ U X.fst U').hom ≫ U ◁ (X.snd.β U').hom ≫ (α_ U U' X.fst).inv) ▷
              Y.fst ≫
            (α_ (U ⊗ U') X.fst Y.fst).hom =
    𝟙 ((X.fst ⊗ Y.fst) ⊗ U ⊗ U') ⊗≫
      X.fst ◁ (Y.snd.β U).hom ▷ U' ⊗≫
        ((X.fst ⊗ U) ◁ (Y.snd.β U').hom ≫ (X.snd.β U).hom ▷ (U' ⊗ Y.fst)) ⊗≫
          U ◁ (X.snd.β U').hom ▷ Y.fst ⊗≫ 𝟙 ((U ⊗ U') ⊗ X.fst ⊗ Y.fst)

Tactic:
by monoidal

Goal state after: