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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : LocallySmall.{t, v, u} C
inst✝ : Small.{t, w} I
⊢ Small.{t, max v w} (attachCellsιFunctorObj f πX).ι

Tactic:
dsimp
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
⊢ arrowMap (extendToSucc hj F τ) i₁ i₂ hi ⋯ = arrowMap F i₁ i₂ hi hi₂

Tactic:
by
  simp [arrowMap, extendToSucc_map hj F τ i₁ i₂ hi hi₂,
    extendToSuccObjIso, extendToSucc.objIso]

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

Goal state before:
pp: case e_x
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
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
      (d.lift j hj
        ⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e (Order.succ i) ⋯).val

Tactic:
rw [d.map_lift _ _ _ _ hi]

Goal state after:
case e_x
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
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ ↑⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩
      (op ⟨i, hi⟩) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e (Order.succ i) ⋯).val
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
k k' : ↑(Set.Iic j)
h : k ⟶ k'
⊢ (⋯.functor ⋙ functor hG A₀ J).map h ≫ (functor hG A₀ J).map (homOfLE ⋯) =
    (functor hG A₀ J).map (homOfLE ⋯) ≫ ((Functor.const ↑(Set.Iic j)).obj ((functor hG A₀ J).obj j)).map h

Tactic:
by simp [MonoOver.forget]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
X : C
⊢ Injective (monoMapFactorizationDataRlp 0).Z

Tactic:
let fac := (monoMapFactorizationDataRlp (0 : X ⟶ 0))

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
X : C
fac : (monomorphisms C).MapFactorizationData (monomorphisms C).rlp 0 := monoMapFactorizationDataRlp 0
⊢ Injective (monoMapFactorizationDataRlp 0).Z
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : 1 < p
⊢ padicNorm p ↑p = (↑p)⁻¹

Tactic:
by
  simp [padicNorm, (pos_of_gt hp).ne', padicValNat.self hp]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ z ≠ 0

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ 1 < ↑p

Tactic:
· exact_mod_cast hz

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ 1 < ↑p
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ 0 < (p.digits n).sum

Tactic:
have hnil : p.digits n ≠ [] := Nat.digits_ne_nil_iff_ne_zero.mpr hn

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
hnil : p.digits n ≠ []
⊢ 0 < (p.digits n).sum
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ 0 < (Int.padicValuation p) ↑x.den

Tactic:
· simp [zero_lt_iff]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ IsPullback (𝟙 X) (𝟙 X) f f → Mono f

Tactic:
intro hf
    exact (mono_iff_fst_eq_snd hf.isLimit).2 rfl

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

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

Tactic:
rw [← cancel_mono φ, hφ₁, hφ₂]

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))
Φ : P.FullSubcategory
u : Φ.obj.fiber.obj U
V : C
v : Φ.obj.fiber.obj V
y : ToType (F₁.obj (op V))
hx₁ :
  (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u
t : unop (op V) ⟶ U
ht : shrinkYonedaObjObjEquiv.symm t = (ConcreteCategory.hom (f.app (op V))) y
⊢ (ConcreteCategory.hom (Φ.obj.toPresheafFiber V v (shrinkYoneda.{w, v, u}.obj U))) (shrinkYonedaObjObjEquiv.symm t) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u

Tactic:
rw [← hx₁]

Goal state after:
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))
Φ : P.FullSubcategory
u : Φ.obj.fiber.obj U
V : C
v : Φ.obj.fiber.obj V
y : ToType (F₁.obj (op V))
hx₁ :
  (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u
t : unop (op V) ⟶ U
ht : shrinkYonedaObjObjEquiv.symm t = (ConcreteCategory.hom (f.app (op V))) y
⊢ (ConcreteCategory.hom (Φ.obj.toPresheafFiber V v (shrinkYoneda.{w, v, u}.obj U))) (shrinkYonedaObjObjEquiv.symm t) =
    (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y)
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.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k

Tactic:
by
  have : (p : ℝ) ^ (-n : ℤ) = (p : ℚ) ^ (-n : ℤ) := by simp
  rw [show (k : ℚ_[p]) = ((k : ℚ) : ℚ_[p]) by norm_cast, eq_padicNorm, this]
  norm_cast
  rw [← padicNorm.dvd_iff_norm_le]

Goal state after:
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:
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.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty ≫ QInfty = 0

Tactic:
by
  ext n
  apply PInfty_f_comp_QInfty_f

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 ≈ const (padicNorm p) 0

Tactic:
simpa using hf

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

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

Tactic:
mul_zero,

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : y = 0
⊢ (if 0 = 0 then ⊤ else ↑(valuation 0)) = (if x = 0 then ⊤ else ↑x.valuation) + ⊤
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 ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Sigma.ι (summand K Δ) A ≫ map K θ = Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)

Tactic:
by
  simp only [map, colimit.ι_desc, Cofan.mk_ι_app]
  obtain rfl := SimplexCategory.image_eq fac
  congr
  · exact SimplexCategory.image_ι_eq fac
  · dsimp only [SimplicialObject.Splitting.IndexSet.pull]
    congr
    exact SimplexCategory.factorThruImage_eq fac

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

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty.f 0 =
    (((dNext 0) fun i j ↦ (homotopyPToId X (j + 1)).hom i j) + (prevD 0) fun i j ↦ (homotopyPToId X (j + 1)).hom i j) +
      (𝟙 K[X]).f 0

pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f (n + 1) =
    (((dNext (n + 1)) fun i j ↦ (homotopyPToId X (j + 1)).hom i j) +
        (prevD (n + 1)) fun i j ↦ (homotopyPToId X (j + 1)).hom i j) +
      (𝟙 K[X]).f (n + 1)

Tactic:
· simpa only [Homotopy.dNext_zero_chainComplex, Homotopy.prevD_chainComplex,
        PInfty_f, P_f_0_eq, zero_add] using (homotopyPToId X 2).comm 0

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f (n + 1) =
    (((dNext (n + 1)) fun i j ↦ (homotopyPToId X (j + 1)).hom i j) +
        (prevD (n + 1)) fun i j ↦ (homotopyPToId X (j + 1)).hom i j) +
      (𝟙 K[X]).f (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 : ℕ
⊢ s.πSummand (IndexSet.id (op ⦋n⦌)) ≫ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n = PInfty.f n

Tactic:
conv_rhs => rw [← id_comp (PInfty.f n)]
  dsimp only [AlternatingFaceMapComplex.obj_X]
  rw [s.decomposition_id, Preadditive.sum_comp]
  rw [Fintype.sum_eq_single (IndexSet.id (op ⦋n⦌)), assoc]
  rintro A (hA : ¬A.EqId)
  rw [assoc, s.cofan_inj_comp_PInfty_eq_zero A hA, 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
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ Φ.f i ≫
      (S₂.s.cofan (op ⦋i⦌)).inj (Splitting.IndexSet.id (op ⦋i⦌)) ≫
        K[S₂.X].d i j ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) =
    ((S₁.s.cofan (op ⦋i⦌)).inj (Splitting.IndexSet.id (op ⦋i⦌)) ≫
        K[S₁.X].d i j ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) ≫
      Φ.f j

Tactic:
← cofan_inj_naturality_symm_assoc Φ (Splitting.IndexSet.id (op ⦋i⦌)),

Goal state after:
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
⊢ (S₁.s.cofan (op ⦋i⦌)).inj (Splitting.IndexSet.id (op ⦋i⦌)) ≫
      Φ.F.app (op ⦋i⦌) ≫ K[S₂.X].d i j ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) =
    ((S₁.s.cofan (op ⦋i⦌)).inj (Splitting.IndexSet.id (op ⦋i⦌)) ≫
        K[S₁.X].d i j ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) ≫
      Φ.f j
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → (f i).HomotopyRel (g i) S
t : ↑unitInterval
x : A
hx : x ∈ S
⊢ (Homotopy.pi fun i ↦ (homotopies i).toHomotopy).toContinuousMap (t, x) = fun i ↦ (f i) x

Tactic:
simp only [funext_iff]

Goal state after:
I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → (f i).HomotopyRel (g i) S
t : ↑unitInterval
x : A
hx : x ∈ S
⊢ ∀ (x_1 : I), (Homotopy.pi fun i ↦ (homotopies i).toHomotopy).toContinuousMap (t, x) x_1 = (f x_1) x
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
⊢ p ⟨reflTransSymmAux (1, x), ⋯⟩ = (p.trans p.symm).toContinuousMap x

Tactic:
by
    simp only [reflTransSymmAux, Path.trans]
    cases le_or_gt (x : ℝ) 2⁻¹ with
    | inl hx => simp [hx, ← extend_apply]
    | inr hx =>
      have : p.extend (2 - 2 * ↑x) = p.extend (1 - (2 * ↑x - 1)) := by ring_nf
      simpa [hx.not_ge, ← extend_apply]

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✝ Y : C
inst✝¹ : IsFibrant Y
h✝¹ : IsCofibrant Y
X : C
inst✝ : IsCofibrant X
h✝ : IsFibrant X
E : BifibrantObject.HoCat C ≌ H :=
  Localization.uniq BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject C))
e : BifibrantObject.toHoCat ⋙ E.functor ≅ BifibrantObject.ι ⋙ L :=
  Localization.compUniqFunctor BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject C))
f : X ⟶ Y
⊢ rightHomotopyClassToHom L (RightHomotopyClass.mk f) =
    (BifibrantObject.HoCat.homEquivRight.trans
        (E.fullyFaithfulFunctor.homEquiv.trans
          ((e.app (BifibrantObject.mk X)).homCongr (e.app (BifibrantObject.mk Y)))))
      (RightHomotopyClass.mk f)

Tactic:
exact (NatIso.naturality_1 e (BifibrantObject.homMk f)).symm

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

Goal state before:
pp: case refine_1
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
H : (weakEquivalences (BifibrantObject C)).IsInvertedBy F
K L : BifibrantObject C
f g : K ⟶ L
h : homRel C f g
⊢ F.map f = F.map g

pp: case refine_2
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
h : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : weakEquivalences (BifibrantObject C) f
⊢ IsIso (F.map f)

Tactic:
· obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_pathObject
    have := isCofibrant_of_cofibration P.ι
    have : IsIso (F.map (homMk P.ι)) := H _ (by
      rw [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]
      exact inferInstanceAs (WeakEquivalence P.ι))
    simp only [show f = homMk h.h ≫ homMk P.p₀ by cat_disch,
      show g = homMk h.h ≫ homMk P.p₁ by cat_disch, Functor.map_comp]
    congr 1
    simp [← cancel_epi (F.map (homMk P.ι)), ← Functor.map_comp]

Goal state after:
case refine_2
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
h : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : weakEquivalences (BifibrantObject C) f
⊢ IsIso (F.map f)
Module: Mathlib.CategoryTheory.LiftingProperties.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
X₁ X₂ X₃ X₄ : Over S
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : CommSq t l r b
inst✝ : ⋯.HasLift
sq' : CommSq (Over.Hom.left t) (Over.Hom.left l) (Over.Hom.left r) (Over.Hom.left b) := map (Over.forget S) sq
⊢ sq'.lift ≫ X₂.hom = X₃.hom

Tactic:
← Over.w b,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
X₁ X₂ X₃ X₄ : Over S
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : CommSq t l r b
inst✝ : ⋯.HasLift
sq' : CommSq (Over.Hom.left t) (Over.Hom.left l) (Over.Hom.left r) (Over.Hom.left b) := map (Over.forget S) sq
⊢ sq'.lift ≫ X₂.hom = Over.Hom.left b ≫ X₄.hom
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 : BifibrantObject C
⊢ ∀ ⦃L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → toHoCat.map f = toHoCat.map g

Tactic:
L

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 L : BifibrantObject C
⊢ ∀ (f g : K ⟶ L), homRel C f g → toHoCat.map f = toHoCat.map g
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)
j : J
x₁ : F₁.obj j
l : J
y₁ : F₁.obj l
h : (hom φ) ((hom (c₁.ι.app j)) x₁) = (hom φ) ((hom (c₁.ι.app l)) y₁)
⊢ ∃ j_1 x₁' y₁', (hom (c₁.ι.app j)) x₁ = (hom (c₁.ι.app j_1)) x₁' ∧ (hom (c₁.ι.app l)) y₁ = (hom (c₁.ι.app j_1)) y₁'

Tactic:
exact ⟨_,  _, _, congr_hom (c₁.w (IsFiltered.leftToMax j l)).symm _,
        congr_hom (c₁.w (IsFiltered.rightToMax j l)).symm _⟩

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
| CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯)
      (𝟙 (homEquiv h) ≫ Hom.base κ ≫ 𝟙 (homEquiv h')) ≍
    CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
enter [2, 1]; exact ((id_comp _).trans (comp_id _)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F X✝ Y✝ : C ⥤ Type (max w v u)
f : X✝ ⟶ Y✝
X : C
a : (F.functorHom X✝).obj X
c✝ d✝ : C
g : c✝ ⟶ d✝
h : (Opposite.unop (coyoneda.rightOp.obj X)).obj c✝
⊢ F.map g ≫ a.app d✝ ((ConcreteCategory.hom ((Opposite.unop (coyoneda.rightOp.obj X)).map g)) h) ≫ f.app d✝ =
    (a.app c✝ h ≫ f.app c✝) ≫ Y✝.map g

Tactic:
by
      have := a.naturality g h
      change (F.map g ≫ a.app _ (h ≫ g)) ≫ _ = _
      aesop

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i < n
⊢ (ConcreteCategory.hom (X.map (mkOfSucc ⟨i, hi⟩).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩) fac_aux₁._proof_1))) x

Tactic:
by
  dsimp [lift]
  rw [spineToSimplex_arrow]
  rfl

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

Goal state before:
pp: V : Truncated 2
motive : V.HomotopyCategory → Prop
h : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), motive (mk x)
x : V.HomotopyCategory
⊢ motive x

Tactic:
obtain ⟨x', rfl⟩ := mk_surjective x

Goal state after:
V : Truncated 2
motive : V.HomotopyCategory → Prop
h : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), motive (mk x)
x' : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ motive (mk x')
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
hf : W₂ f
⊢ r.deg X ≤ r.deg Y

Tactic:
by
  by_cases hf' : MorphismProperty.identities C f
  · cases hf'
    rfl
  · exact (r.lt₂ f hf hf').le

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case inl.inl
n : ℕ
i i' : Fin (n + 2)
h✝ : i.succ ≤ i'.succ
h : i.succ < i'.succ
⊢ δ i'.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.succ ≫ σ i = σ j ≫ δ j'

Tactic:
rw [Fin.succ_lt_succ_iff] at h

Goal state after:
case inl.inl
n : ℕ
i i' : Fin (n + 2)
h✝ : i.succ ≤ i'.succ
h : i < i'
⊢ δ i'.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.succ ≫ σ i = σ j ≫ δ j'
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case succ.inr
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
j : Fin (n + 1)
j' : Fin (n + 2)
h : δ i' ≫ σ i = σ j ≫ δ j'
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
· exact ⟨_, _, _, P_σ.σ _, P_δ.δ _, h⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_σ.comp_of.succ.inr
x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
j' : Fin (n + 1)
j'' : Fin (n + 2)
h' : δ i ≫ σ j = σ j' ≫ δ j''
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m

Tactic:
obtain ⟨_, _, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' f hf

Goal state after:
case comp_σ.comp_of.succ.inr
x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
j' : Fin (n + 1)
j'' : Fin (n + 2)
h' : δ i ≫ σ j = σ j' ≫ δ j''
w✝¹ : SimplexCategoryGenRel
w✝ : z ⟶ w✝¹
m₁ : w✝¹ ⟶ mk n
he₁ : P_σ w✝
hm₁ : P_δ m₁
h₁ : f ≫ σ j' = w✝ ≫ m₁
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
⊢ W = ⊤

Tactic:
have hW (d : ℕ) : W.inverseImage (Truncated.inclusion d) = ⊤ :=
    Truncated.morphismProperty_eq_top _ (fun _ _ i ↦ δ_mem i)
      (fun _ _ i ↦ σ_mem i)
  ext a b f
  simp only [MorphismProperty.top_apply, iff_true]
  change W.inverseImage (Truncated.inclusion (max a.len b.len))
    (Truncated.Hom.tr f (ha := by simp) (hb := by simp))
  simp only [hW, MorphismProperty.top_apply]

Goal state after: