mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case isSuccLimit
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
hi' : ∀ b < i, Nonempty (Φ.Iteration b)
⊢ Nonempty (Φ.Iteration i)

Tactic:
exact ⟨mkOfLimit hi (fun a ha ↦ (hi' a ha).some)⟩

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case isMin
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : IsMin i
⊢ Subsingleton (d.Extension val₀ i)

Tactic:
obtain rfl : i = ⊥ := by simpa using hi

Goal state after:
case isMin
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
hi : IsMin ⊥
⊢ Subsingleton (d.Extension val₀ ⊥)
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
j : J
hj : ¬IsMax j
sq' : (sqFunctor c p f g).obj (Opposite.op j)
this✝ : ∀ (sq : CommSq sq'.f' (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)), sq.HasLift
this : HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
| F.map (homOfLE ⋯) ≫ sq'.f'

Tactic:
← sq'.sq.fac_left,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
j : J
hj : ¬IsMax j
sq' : (sqFunctor c p f g).obj (Opposite.op j)
this✝ : ∀ (sq : CommSq sq'.f' (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)), sq.HasLift
this : HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
| F.map (homOfLE ⋯) ≫ F.map (homOfLE ⋯) ≫ ⋯.lift
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case isMin
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : IsMin i
⊢ Nonempty (d.Extension val₀ i)

Tactic:
obtain rfl : i = ⊥ := by simpa using hi

Goal state after:
case isMin
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
hi : IsMin ⊥
⊢ Nonempty (d.Extension val₀ ⊥)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), (generatingMonomorphisms G).rlp f → (monomorphisms C).rlp f

Tactic:
Y

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X Y : C
⊢ ∀ (f : X ⟶ Y), (generatingMonomorphisms G).rlp f → (monomorphisms C).rlp 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 : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y),
    I.rlp.llp f → ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.ToType).retracts f

Tactic:
Y

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),
    I.rlp.llp f → ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.ToType).retracts f
Module: Mathlib.NumberTheory.Padics.PadicNorm

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

Tactic:
have : 0 ≤ padicValRat p m := by simp only [of_int, Nat.cast_nonneg]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖⟨k, property✝⟩‖ = 1
⊢ ⟨k, property✝⟩ * inv ⟨k, property✝⟩ = 1

Tactic:
by
    have hk : k ≠ 0 := fun h' => zero_ne_one' ℚ_[p] (by simp [h'] at h)
    unfold PadicInt.inv
    rw [norm_eq_padic_norm] at h
    dsimp only
    rw [dif_pos h]
    apply Subtype.ext_iff.2
    simp [mul_inv_cancel₀ hk]

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

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ exp (-↑(padicValInt p x)) ≤ 1

Tactic:
rw [← le_log_iff_exp_le] <;>
    simp_all

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

Goal state before:
pp: case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ n ≤ x.valuation → ↑p ^ n ∣ x

Tactic:
nth_rewrite 2 [unitCoeff_spec hx]

Goal state after:
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ n ≤ x.valuation → ↑p ^ n ∣ ↑(unitCoeff hx) * ↑p ^ x.valuation
Module: Mathlib.AlgebraicGeometry.Sites.ElladicCohomology

Goal state before:
pp: X : Scheme
ℓ : ℕ
inst✝¹ : Fact (Nat.Prime ℓ)
inst✝ : IsEmpty ↥X
n : ℕ
⊢ IsZero ((sheafCompose (ProEt.topology X) AddCommGrpCat.uliftFunctor).obj (X.ellAdicSheaf ℓ))

Tactic:
exact Functor.map_isZero _ (isZero_ellAdicSheaf_of_isEmpty _ _)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : x.valuation < 0
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
⊢ x.valuation ≤ 0

Tactic:
exact hx.le

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:
by
  simp [lift₃, pullback₃.p₃]

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 : ℕ
⊢ HigherFacesVanish (q + 1) ((P (q + 1)).f (n + 1))

Tactic:
simp only [P_succ]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HigherFacesVanish (q + 1) ((P q ≫ (𝟙 K[X] + Hσ q)).f (n + 1))
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

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

Tactic:
by
    simpa only [← P_is_eventually_constant (show n ≤ n by rfl),
      AlternatingFaceMapComplex.obj_d_eq] using (P (n + 1) : K[X] ⟶ _).comm (n + 1) n

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

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : f - 0 ≈ 0
⊢ ⟦f⟧ = 0

Tactic:
apply Quotient.sound

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : f - 0 ≈ 0
⊢ f ≈ const (padicNorm p) 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 + (X.σ 0 + -X.σ 0 ≫ X.δ 1 ≫ X.σ 0 + (-X.σ 0 ≫ X.σ 1 ≫ X.δ 0 + (X.σ 0 + -X.σ 0))) = 0

Tactic:
← Fin.castSucc_zero (n := 2),

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 + (X.σ 0 + -X.σ 0 ≫ X.δ 1 ≫ X.σ 0 + (-X.σ 0 ≫ X.σ 1 ≫ X.δ (Fin.castSucc 0) + (X.σ 0 + -X.σ 0))) = 0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mpr
Δ fst✝ : SimplexCategoryᵒᵖ
f : unop Δ ⟶ unop fst✝
hf : Epi f
h : fst✝ = Δ
⊢ EqId ⟨fst✝, ⟨f, hf⟩⟩

Tactic:
subst h

Goal state after:
case mpr
fst✝ : SimplexCategoryᵒᵖ
f : unop fst✝ ⟶ unop fst✝
hf : Epi f
⊢ EqId ⟨fst✝, ⟨f, hf⟩⟩
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ Mono A.e

Tactic:
subst h

Goal state after:
case mp
Δ : SimplexCategoryᵒᵖ
⊢ Mono (id Δ).e
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : Δ' = Δ
⊢ eqToHom ⋯ ≫ f.f Δ.len = f.f Δ'.len ≫ eqToHom ⋯

Tactic:
subst h

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' : SimplexCategory
i : Δ' ⟶ Δ'
inst✝ : Mono i
⊢ eqToHom ⋯ ≫ f.f Δ'.len = f.f Δ'.len ≫ eqToHom ⋯
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : ⦋n✝ + 1⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
i : Fin (n✝ + 1)
α : ⦋n✝⦌ ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
⊢ X.map (α.op ≫ (SimplexCategory.σ i).op) ≫ PInfty.f (n✝ + 1) = 0

Tactic:
X.map_comp,

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : ⦋n✝ + 1⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
i : Fin (n✝ + 1)
α : ⦋n✝⦌ ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
⊢ (X.map α.op ≫ X.map (SimplexCategory.σ i).op) ≫ PInfty.f (n✝ + 1) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ Homotopy (P (q + 1)) (𝟙 K[X])

Tactic:
refine
      Homotopy.trans (Homotopy.ofEq ?_)
        (Homotopy.trans
          (Homotopy.add (homotopyPToId q) (Homotopy.compLeft (homotopyHσToZero q) (P q)))
          (Homotopy.ofEq ?_))
    · simp only [P_succ, comp_add, comp_id]
    · simp only [add_zero, comp_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✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B = A
⊢ s.N (unop B.fst).len = s.N (unop A.fst).len

Tactic:
subst h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
B : IndexSet Δ
⊢ s.N (unop B.fst).len = s.N (unop B.fst).len
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

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

pp: case h_p
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).X n).p ≫ eqToHom ?refine_1.refine_1.h_X =
    eqToHom ?refine_1.refine_1.h_X ≫
      (((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                  N₁ ⋙
                    (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                      (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
              P).X
          n).p

Tactic:
· rfl

Goal state after:
case h_p
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).X n).p ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫
      (((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                  N₁ ⋙
                    (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                      (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
              P).X
          n).p
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h : ¬1 ≤ ↑j
⊢ False

Tactic:
exact h₂ (by simpa only [Fin.ext_iff, not_le, Nat.lt_one_iff] using! h)

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

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : n = n'
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n' ≫ X.map i.op

Tactic:
subst h

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n⦌
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n ≫ X.map i.op
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 : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ ((s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ PInfty.f i) ≫ (N₁.obj X).X.d i j =
    ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex).X.d i j ≫
      (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ PInfty.f j

Tactic:
dsimp
            rw [assoc, assoc, assoc, πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty,
              HomologicalComplex.Hom.comm]

Goal state after:
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
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ PInfty.f (unop A.fst).len ≫ X.map (image.ι (θ.unop ≫ A.e)).op ≫ X.map (A.pull θ).e.op =
    PInfty.f (unop A.fst).len ≫ X.map A.e.op ≫ X.map θ

Tactic:
simp only [← X.map_comp]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ PInfty.f (unop A.fst).len ≫ X.map ((image.ι (θ.unop ≫ A.e)).op ≫ (A.pull θ).e.op) =
    PInfty.f (unop A.fst).len ≫ X.map (A.e.op ≫ θ)
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
A : Splitting.IndexSet (op ⦋j⦌)
h : A = Splitting.IndexSet.id (op ⦋j⦌)
⊢ Φ.f (unop A.fst).len ≫ (S₂.s.cofan (op ⦋j⦌)).inj A ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) =
    (S₁.s.cofan (op ⦋j⦌)).inj A ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j

Tactic:
subst h

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 ≫
      (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
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: case nil
U : Type u_1
inst✝ : Quiver U
u : U
hzero : nil.length = 0
⊢ Path.cast ⋯ ⋯ nil = nil

pp: case cons
U : Type u_1
inst✝ : Quiver U
u v b✝ : U
a✝¹ : Path u b✝
a✝ : b✝ ⟶ v
hzero : (a✝¹.cons a✝).length = 0
⊢ Path.cast ⋯ ⋯ (a✝¹.cons a✝) = nil

Tactic:
· rfl

Goal state after:
case cons
U : Type u_1
inst✝ : Quiver U
u v b✝ : U
a✝¹ : Path u b✝
a✝ : b✝ ⟶ v
hzero : (a✝¹.cons a✝).length = 0
⊢ Path.cast ⋯ ⋯ (a✝¹.cons a✝) = nil
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
P : PathObject Y.obj
h : P.RightHomotopy f.hom g.hom
⊢ WeakEquivalence f.hom ↔ WeakEquivalence g.hom

Tactic:
apply h.weakEquivalence_iff

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
F : BifibrantObject C ⥤ D
hF : (weakEquivalences (BifibrantObject C)).IsInvertedBy F
⊢ ∀ (x y : BifibrantObject C) (f₁ f₂ : x ⟶ y), homRel C f₁ f₂ → F.map f₁ = F.map f₂

Tactic:
rwa [inverts_iff_factors] at hF

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ ∀ (y : CofibrantObject C) (f₁ f₂ : X ⟶ y), homRel C f₁ f₂ → bifibrantResolution'.map f₁ = bifibrantResolution'.map f₂

Tactic:
Y

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
⊢ ∀ (f₁ f₂ : X ⟶ Y), homRel C f₁ f₂ → bifibrantResolution'.map f₁ = bifibrantResolution'.map f₂
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : HoCat C
⊢ ∀ ⦃Y : HoCat C⦄ (f : X ⟶ Y), weakEquivalences (HoCat C) f → IsIso (HoCat.bifibrantResolution.map f)

Tactic:
Y

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : HoCat C
⊢ ∀ (f : X ⟶ Y), weakEquivalences (HoCat C) f → IsIso (HoCat.bifibrantResolution.map f)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
h : x₀ = x₁
⊢ eqToHom ⋯ = (Path.Homotopic.Quotient.refl x₁).cast h ⋯

Tactic:
subst h

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x₀ : X
⊢ eqToHom ⋯ = (Path.Homotopic.Quotient.refl x₀).cast ⋯ ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
⊢ m = hc.desc (isPushout.multicofork h h' s)

Tactic:
apply Multicofork.IsColimit.hom_ext hc
      intro k
      have := h.symm.le (Set.mem_univ k)
      push _ ∈ _ at this
      obtain rfl | rfl := this
      · simpa [h₁] using! (hc.fac (isPushout.multicofork h h' s) (.right (J.fst default))).symm
      · simpa [h₂] using! (hc.fac (isPushout.multicofork h h' s) (.right (J.snd default))).symm

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

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
⊢ A ≤ ∂Δ[n] ↔ A ≠ ⊤

Tactic:
refine ⟨fun h ↦ ?_, fun hA ↦ ?_⟩

Goal state after:
case refine_1
n : ℕ
A : Δ[n].Subcomplex
h : A ≤ ∂Δ[n]
⊢ A ≠ ⊤

case refine_2
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
⊢ A ≤ ∂Δ[n]
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
x₁ y₁ : c₁.pt
h : (hom φ) x₁ = (hom φ) y₁
⊢ ∃ j x₁' y₁', x₁ = (hom (c₁.ι.app j)) x₁' ∧ y₁ = (hom (c₁.ι.app j)) y₁'

Tactic:
obtain ⟨j, x₁, rfl⟩ := Types.jointly_surjective_of_isColimit hc₁ x₁

Goal state after:
J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
y₁ : c₁.pt
j : J
x₁ : F₁.obj j
h : (hom φ) ((hom (c₁.ι.app j)) x₁) = (hom φ) y₁
⊢ ∃ j_1 x₁' y₁', (hom (c₁.ι.app j)) x₁ = (hom (c₁.ι.app j_1)) x₁' ∧ y₁ = (hom (c₁.ι.app j_1)) y₁'
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
a : X₁ ⊕ X₂
⊢ Quot.mk (Rel f g) a = Quot.mk (Rel f g) a

pp: case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) x₀)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) y₀))

pp: case inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) s✝)) = Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) s✝))

pp: case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) s✝)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) s✝))

Tactic:
· rfl

Goal state after:
case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) x₀)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) y₀))

case inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) s✝)) = Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) s✝))

case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) s✝)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) s✝))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h : (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂
⊢ (ConcreteCategory.hom c'.inl) x₁ = (ConcreteCategory.hom c'.inr) x₂

Tactic:
by
  convert! congr_arg e.hom.hom h
  · exact ConcreteCategory.congr_hom (e.hom.w WalkingSpan.left).symm x₁
  · exact ConcreteCategory.congr_hom (e.hom.w WalkingSpan.right).symm x₂

Goal state after: