mathlib-initiative/mathlib-tactics huggingface dataset:
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₁₄ :
  (𝟙 (KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌) ≫ PInfty.f n) ≫ 𝟙 (KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌) =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      ((𝟙 (KaroubiFunctorCategoryEmbedding.obj { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } _⦋n⦌) ≫ PInfty.f n) ≫
          𝟙 (KaroubiFunctorCategoryEmbedding.obj { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } _⦋n⦌)) ≫
        (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n

Tactic:
id_comp,

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.obj Y _⦋n⦌) =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      ((𝟙 (KaroubiFunctorCategoryEmbedding.obj { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } _⦋n⦌) ≫ PInfty.f n) ≫
          𝟙 (KaroubiFunctorCategoryEmbedding.obj { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } _⦋n⦌)) ≫
        (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n
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.obj Y _⦋n⦌) =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      ((𝟙 (KaroubiFunctorCategoryEmbedding.obj { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } _⦋n⦌) ≫ PInfty.f n) ≫
          𝟙 (KaroubiFunctorCategoryEmbedding.obj { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } _⦋n⦌)) ≫
        (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n

Tactic:
id_comp,

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.obj Y _⦋n⦌) =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      (PInfty.f n ≫ 𝟙 (KaroubiFunctorCategoryEmbedding.obj { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } _⦋n⦌)) ≫
        (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ min (if x = 0 then ⊤ else ↑x.valuation) (if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Tactic:
rw [hx, if_pos rfl, min_eq_right, zero_add]
      exact le_top

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

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
⊢ (Q (q + 1)).f (n + 1) = ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Tactic:
by_cases! hqn : n < q
    · rw [Q_is_eventually_constant (show n + 1 ≤ q by lia), hq]
      congr 1
      ext ⟨x, hx⟩
      simp_rw [Finset.mem_filter_univ]
      lia
    · obtain ⟨a, ha⟩ := Nat.le.dest hqn
      rw [Q_succ, HomologicalComplex.sub_f_apply, HomologicalComplex.comp_f, hq]
      symm
      conv_rhs => rw [sub_eq_add_neg, add_comm]
      let q' : Fin (n + 1) := ⟨q, Nat.lt_succ_of_le hqn⟩
      rw [← @Finset.add_sum_erase _ _ _ _ _ _ q' (by simp [q'])]
      congr
      · have hnaq' : n = a + q := by lia
        simp only [(HigherFacesVanish.of_P q n).comp_Hσ_eq hnaq', q'.rev_eq hnaq', neg_neg]
        rfl
      · ext ⟨i, hi⟩
        simp_rw [Finset.mem_erase, Finset.mem_filter_univ, q', ne_eq, Fin.mk.injEq]
        lia

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

Tactic:
· simp [hx0, norm_zero, aux, le_of_lt (aux _)]

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
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)
j : Fin (n + 1)
hj : j ∈ {i | ↑i < 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:
simp only [Finset.mem_univ, Finset.mem_filter] at hj

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)
j : Fin (n + 1)
hj : True ∧ ↑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
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 : ℕ
⊢ 𝟙 (X _⦋n⦌) ≫ PInfty.f n - PInfty.f n ≫ PInfty.f n = 0

Tactic:
id_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ PInfty.f n - PInfty.f n ≫ PInfty.f n = 0
Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₂ToKaroubiIso.inv.app X ≫
      𝟙 ((N₂ ⋙ Γ₂).obj ((toKaroubi (SimplicialObject C)).obj X)) ≫ Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X) =
    𝟙 (Γ₂.obj (N₁.obj X))

Tactic:
id_comp,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₂ToKaroubiIso.inv.app X ≫ Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X) = 𝟙 (Γ₂.obj (N₁.obj X))
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 : ℕ
⊢ 𝟙 (s.N n) ≫ ((s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n) ≫ PInfty.f n =
    (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n

Tactic:
id_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ ((s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n) ≫ PInfty.f n =
    (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.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
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ (N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂N₂.natTrans.app P)).f.f n = (𝟙 (N₂.obj P)).f.f n

Tactic:
have eq₂ : ((Γ₀.splitting (N₂.obj P).X).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
      (N₂.map (Γ₂N₂.natTrans.app P)).f.f n = PInfty.f n ≫ P.p.app (op ⦋n⦌) := by
    dsimp
    rw [PInfty_on_Γ₀_splitting_summand_eq_self_assoc, Γ₂N₂.natTrans_app_f_app]
    dsimp
    rw [Γ₂N₂ToKaroubiIso_hom_app, assoc, Splitting.ι_desc_assoc, assoc, assoc]
    dsimp [toKaroubi]
    rw [Splitting.ι_desc_assoc]
    simp [Splitting.IndexSet.e]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
eq₂ :
  ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
      (N₂.map (Γ₂N₂.natTrans.app P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌)
⊢ (N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂N₂.natTrans.app P)).f.f n = (𝟙 (N₂.obj P)).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
P : Karoubi (SimplicialObject C)
⊢ N₂Γ₂.inv.app (N₂.obj P) ≫
      𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ 𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ N₂.map (Γ₂N₂.natTrans.app P) =
    𝟙 (N₂.obj P)

Tactic:
id_comp,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ N₂Γ₂.inv.app (N₂.obj P) ≫ 𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ N₂.map (Γ₂N₂.natTrans.app P) = 𝟙 (N₂.obj P)
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)
⊢ N₂Γ₂.inv.app (N₂.obj P) ≫ 𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ N₂.map (Γ₂N₂.natTrans.app P) = 𝟙 (N₂.obj P)

Tactic:
id_comp,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂N₂.natTrans.app P) = 𝟙 (N₂.obj P)
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X✝ Y✝ X Y Z : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ map ▷ I ≫ Homotopy.h (F.fst.trans G.fst) = Homotopy.h (F.snd.trans G.snd) ≫ map

Tactic:
by
    ext ⟨_, _⟩
    simp only [TopCat.comp_app, Homotopy.h_hom_apply, ContinuousMap.Homotopy.trans_apply]
    cat_disch

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
H : f.Homotopy g
⊢ ∀ ⦃X_1 Y_1 : FundamentalGroupoid X⦄ (f_1 : X_1 ⟶ Y_1),
    (map f).map f_1 ≫ ⟦H.evalAt Y_1.as⟧ = ⟦H.evalAt X_1.as⟧ ≫ (map g).map f_1

Tactic:
rintro ⟨x⟩ ⟨y⟩ p
    rcases Path.Homotopic.Quotient.mk_surjective p with ⟨p, rfl⟩
    simp only [map_map, Path.Homotopic.Quotient.mk''_eq_mk, comp_eq,
      ← Path.Homotopic.Quotient.mk_map, ← Path.Homotopic.Quotient.mk_trans]
    rw [Path.Homotopic.Quotient.eq]
    exact .map_trans_evalAt _ _

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: case e_a
C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
x✝ : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
⊢ G.map f₁ = G.map f₂

Tactic:
rw [← cancel_epi (G.map s), ← G.map_comp, ← G.map_comp, h]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
R₀ : (localizerMorphism C).LeftResolution X :=
  { X₁ := mk (HoCat.resolutionObj X), w := HoCat.pResolutionObj X, hw := ⋯ }
R : (localizerMorphism C).LeftResolution X
⊢ Nonempty (Zigzag R R₀)

Tactic:
have sq : CommSq (initial.to _) (initial.to _) R₀.w R.w := ⟨by simp⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
R₀ : (localizerMorphism C).LeftResolution X :=
  { X₁ := mk (HoCat.resolutionObj X), w := HoCat.pResolutionObj X, hw := ⋯ }
R : (localizerMorphism C).LeftResolution X
sq :
  CommSq (initial.to ((localizerMorphism C).functor.obj R₀.X₁)) (initial.to ((localizerMorphism C).functor.obj R.X₁))
    R₀.w R.w
⊢ Nonempty (Zigzag R R₀)
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
⊢ Function.Surjective L.map

Tactic:
by
  intro f
  obtain ⟨⟨f⟩, rfl⟩ := (bijective_leftHomotopyClassToHom L X Y).2 f
  exact ⟨f, rfl⟩

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

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

Tactic:
rw [weakEquivalences_op]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
⊢ (weakEquivalences C).op.HasTwoOutOfThreeProperty
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

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

Tactic:
rw [weakEquivalences_op]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (weakEquivalences C).op.IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.ModelCategory.Transport

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this✝ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ (fibrations C).IsStableUnderRetracts

Tactic:
rw [h₂]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this✝ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ ((fibrations D).inverseImage e.functor).IsStableUnderRetracts
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
⊢ ∀ {X Y : WalkingMultispan J} (f : X ⟶ Y),
    (d.map F).multispan.map f ≫
        (match Y with
          | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
          | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom =
      (match X with
          | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
          | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom ≫
        (d.multispan ⋙ F).map f

Tactic:
rintro _ _ (_ | _) <;> simp

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

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
⊢ A.toSSet.degenerate i = ⊤

Tactic:
by
    ext ⟨a, ha⟩
    rw [A.mem_degenerate_iff]
    simp only [Set.top_eq_univ, Set.mem_univ, iff_true]
    obtain hi | rfl := hi.lt_or_eq
    · simp [Δ[n].degenerate_eq_univ_of_hasDimensionLT (n + 1) i]
    · rw [mem_degenerate_iff_notMem_nonDegenerate, nonDegenerate_top_dim]
      rintro rfl
      exact h (le_antisymm (by simp) (by simpa [← ofSimplex_objEquiv_symm_id]))

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

Goal state before:
pp: case hinj
J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
i j : J
⊢ ∀ (xi : (fun X ↦ X) ((F ⋙ functorToTypes).obj i)) (xj : (fun X ↦ X) ((F ⋙ functorToTypes).obj j)),
    (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) xi =
        (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ functorToTypes).map f)) xi = (ConcreteCategory.hom ((F ⋙ functorToTypes).map g)) xj

Tactic:
⟨x, hx⟩

Goal state after:
case hinj
J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
i j : J
x : X
hx : x ∈ F.obj i
⊢ ∀ (xj : (fun X ↦ X) ((F ⋙ functorToTypes).obj j)),
    (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) ⟨x, hx⟩ =
        (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ functorToTypes).map f)) ⟨x, hx⟩ =
          (ConcreteCategory.hom ((F ⋙ functorToTypes).map g)) xj
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ Cofibration f ↔ Mono f

Tactic:
by
  rw [HomotopicalAlgebra.cofibration_iff]
  rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X Y : SSet
p : X ⟶ Y
hY : IsTerminal Y
⊢ X.Quasicategory ↔ InnerFibration p

Tactic:
simp only [quasicategory_iff_innerFibration, innerFibration_iff]
  symm
  apply innerFibrations.arrow_mk_iso_iff
  exact Arrow.isoMk (Iso.refl _) (Limits.IsTerminal.uniqueUpToIso hY Limits.terminalIsTerminal)

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

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

Tactic:
quasicategory_iff_innerFibration

Goal state after:
X Y : SSet
p : X ⟶ Y
inst✝ : InnerFibration p
hY : InnerFibration (terminal.from Y)
⊢ InnerFibration (terminal.from X)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
⊢ horn.IsCompatible fun j hj ↦ ι i j hj ≫ g

Tactic:
simp only [isCompatible_iff, ← Category.assoc]
    intro j k hj hk hjk
    congr 1
    obtain ⟨j, rfl⟩ := j.eq_castSucc_of_ne_last (Fin.ne_last_of_lt hjk)
    obtain ⟨k, rfl⟩ := k.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hjk)
    rw [← cancel_mono (Subcomplex.ι _), Category.assoc, Category.assoc, ι_ι, ι_ι,
      Fin.pred_succ, Fin.castPred_castSucc, stdSimplex.δ_comp_δ (by grind)]

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
⊢ 0 < i →
    i < Fin.last (n + 2) →
      ∃ σ,
        ∀ (j : Fin (n + 3)) (h : j ≠ i),
          (ConcreteCategory.hom (SimplicialObject.δ X j)) σ =
            (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)

Tactic:
h₀

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
⊢ i < Fin.last (n + 2) →
    ∃ σ,
      ∀ (j : Fin (n + 3)) (h : j ≠ i),
        (ConcreteCategory.hom (SimplicialObject.δ X j)) σ =
          (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a : CatEnrichedOrdinary C
⊢ homEquiv (𝟙 a) = 𝟙 a.toBase

Tactic:
unfold homEquiv
  simp only [Equiv.trans_apply]
  rw [eHomEquiv_id]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ eHomWhiskerRight V (f ≫ f') Y = eHomWhiskerRight V f' Y ≫ eHomWhiskerRight V f Y

Tactic:
dsimp [eHomWhiskerRight]
  rw [assoc, assoc, eHomEquiv_comp, comp_whiskerRight_assoc, comp_whiskerRight_assoc, ← e_assoc',
    tensorHom_def', comp_whiskerRight_assoc, id_whiskerLeft, comp_whiskerRight_assoc,
    ← comp_whiskerRight_assoc, Iso.inv_hom_id, id_whiskerRight_assoc,
    comp_whiskerRight_assoc, leftUnitor_inv_whiskerRight_assoc,
    ← associator_inv_naturality_left_assoc, Iso.inv_hom_id_assoc,
    ← whisker_exchange_assoc, id_whiskerLeft_assoc, Iso.inv_hom_id_assoc]

Goal state after: