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

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
W₀ : C₀
c : W₀ ⟶ Z₀
hc : (↑⟨(data X).sieve₁₀ b₁ b₂, ⋯⟩).arrows c
⊢ ((presheafObjπ data G₀ X h₁.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ h₁.q) ≫ G₀.obj.map a.op) ≫ G₀.obj.map c.op =
    ((presheafObjπ data G₀ X h₂.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ h₂.q) ≫ G₀.obj.map a.op) ≫ G₀.obj.map c.op

Tactic:
simp only [assoc, IsDenseSubsite.mapPreimage_comp_map]

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
W₀ : C₀
c : W₀ ⟶ Z₀
hc : (↑⟨(data X).sieve₁₀ b₁ b₂, ⋯⟩).arrows c
⊢ presheafObjπ data G₀ X h₁.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ F.map a ≫ h₁.q) =
    presheafObjπ data G₀ X h₂.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ F.map a ≫ h₂.q)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
⊢ restriction.res data G₀ ⋯.some ≫ G₀.obj.map p₁.op = restriction.res data G₀ ⋯.some ≫ G₀.obj.map p₂.op

Tactic:
rw [restriction.res_eq_res data G₀ _ h₁, restriction.res_eq_res data G₀ _ h₂]

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
⊢ restriction.res data G₀ h₁ ≫ G₀.obj.map p₁.op = restriction.res data G₀ h₂ ≫ G₀.obj.map p₂.op
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ Y₀ : C₀
f : F.obj Y₀ ⟶ F.obj X₀
⊢ inv data G₀ X₀ ≫ restriction data G₀ f = IsDenseSubsite.mapPreimage J F G₀ f

Tactic:
by
  refine Presheaf.IsSheaf.hom_ext G₀.property
    ⟨_, IsDenseSubsite.imageSieve_mem J₀ J F f⟩ _ _ ?_
  rintro ⟨W₀, a, b, fac₁⟩
  refine Presheaf.IsSheaf.hom_ext G₀.property
    ⟨_, J₀.pullback_stable b (cover_lift F J₀ _ (data (F.obj X₀)).mem₀)⟩ _ _ ?_
  rintro ⟨T₀, c, _, d, _, ⟨i⟩, fac₂⟩
  dsimp at i d fac₂ ⊢
  simp only [assoc, ← Functor.map_comp, ← op_comp]
  rw [restriction_map data G₀ f (c ≫ a) d
    (by rw [fac₂, map_comp, map_comp_assoc, fac₁]), inv_π_assoc,
    ← IsDenseSubsite.mapPreimage_comp, fac₂,
    IsDenseSubsite.mapPreimage_comp_map J F G₀, map_comp,
      map_comp_assoc, fac₁]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁵ : LinearOrder J
inst✝⁴ : SuccOrder J
inst✝³ : OrderBot J
inst✝² : HasIterationOfShape J C
inst✝¹ : WellFoundedLT J
j : J
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
⊢ G.obj ⟨k₂, h₂⟩ = F.obj ⟨k₂, h₂⟩

Tactic:
rw [h.tgt]

Goal state after:
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)
b✝ : FunctorObjIndex f πX
⊢ Sigma.ι (functorObjSrcFamily f πX) b✝ ≫ functorObjTop f πX ≫ πX =
    Sigma.ι (functorObjSrcFamily f πX) b✝ ≫ functorObjLeft f πX ≫ π'FunctorObj f πX

Tactic:
simp [π'FunctorObj]

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
⊢ ∀ {X_1 Y : ↑(Set.Iic j)} (f : X_1 ⟶ Y),
    (restrictionLE (extendToSucc hj F τ) ⋯).map f ≫ (extendToSuccObjIso hj F τ ↑Y ⋯).hom =
      (extendToSuccObjIso hj F τ ↑X_1 ⋯).hom ≫ F.map f

Tactic:
by
    rintro ⟨i₁, h₁⟩ ⟨i₂, h₂⟩ f
    apply extendToSuccObjIso_hom_naturality

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

Goal state before:
pp: case inr
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
hi : Order.IsSuccLimit (Order.succ j)
hij : Order.succ j ≤ Order.succ j
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op)) (d.succ j hj e.val) =
    d.lift (Order.succ j) hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val),
        ⋯⟩

Tactic:
· exfalso
      exact hj hi.isMax

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

Goal state before:
pp: case inl
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 : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
this : (e i hij').val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e i hij').val, ⋯⟩
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩) =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩), ⋯⟩

Tactic:
rw [d.map_lift _ _ _ _ hij']

Goal state after:
case inl
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 : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
this : (e i hij').val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e i hij').val, ⋯⟩
⊢ ↑⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩ (op ⟨i, hij'⟩) =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩), ⋯⟩
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 Y A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this✝ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts C
⊢ ∀ {f_1 : A ⟶ obj I κ f} {g : B ⟶ Y} (sq : CommSq f_1 i (πObj I κ f) g), sq.HasLift

Tactic:
have := preservesColimit I κ i hi _ (relativeCellComplexιObj I κ f)

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 A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this✝¹ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this✝ : HasPushouts C
this : PreservesColimit (relativeCellComplexιObj I κ f).F (coyoneda.obj (Opposite.op A))
⊢ ∀ {f_1 : A ⟶ obj I κ f} {g : B ⟶ Y} (sq : CommSq f_1 i (πObj I κ f) g), sq.HasLift
Module: Mathlib.NumberTheory.Padics.PadicIntegers

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

Tactic:
by
  rw [norm_eq_zpow_neg_valuation hx, zpow_le_zpow_iff_right₀, neg_le_neg_iff, Nat.cast_le]
  exact mod_cast hp.out.one_lt

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
hx : 0 ≤ x
⊢ { toFun := fun x ↦ if x = 0 then 0 else ↑(Multiplicative.ofAdd (-padicValRat p x)), map_zero' := ⋯ }
      (↑p ^ x.natAbs)⁻¹ =
    ↑(Multiplicative.ofAdd x)

Tactic:
by simp [hp.out.ne_zero, hx]

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

Goal state before:
pp: case inr.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this✝ : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : stationaryPoint hne' ≤ N
this : padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) = 0
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε

Tactic:
simpa only [this]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnm : c.Rel m n
⊢ X _⦋n + 1⦌ = K[X].X m

Tactic:
by congr

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
⊢ X _⦋n + 1⦌ = K[X].X m

Tactic:
by congr

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

Goal state before:
pp: case neg
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
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ (Q q - P q ≫ Hσ q).f (n + 1) = ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Tactic:
HomologicalComplex.sub_f_apply,

Goal state after:
case neg
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
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ (Q q).f (n + 1) - (P q ≫ Hσ q).f (n + 1) = ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
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
h✝ : Δ = Δ'
⊢ K.X Δ.len = K.X Δ'.len

Tactic:
by congr

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

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.map (Γ₂N₂.hom.app P) ≫ N₂Γ₂.hom.app (N.obj P) = 𝟙 (N.obj P)

Tactic:
let α := N.mapIso (Γ₂N₂.app P)
    let β := N₂Γ₂.app (N.obj P)
    symm
    change 𝟙 _ = α.hom ≫ β.hom
    rw [← Iso.inv_comp_eq, comp_id, ← comp_id β.hom, ← Iso.inv_comp_eq]
    exact AlgebraicTopology.DoldKan.identity_N₂_objectwise P

Goal state after:
Module: Mathlib.Combinatorics.Quiver.SingleObj

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : SingleObj α ⥤q SingleObj β
g : SingleObj β ⥤q SingleObj γ
⊢ toPrefunctor.symm (f ⋙q g) = toPrefunctor.symm g ∘ toPrefunctor.symm f

Tactic:
by
  simp only [Equiv.symm_apply_eq, toPrefunctor_comp, Equiv.apply_symm_apply]

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

Goal state before:
pp: case h_map
I : Type u
X : I → TopCat
⊢ autoParam
    (∀ (X_1 Y : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))) (f : X_1 ⟶ Y),
      (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f =
        CategoryTheory.eqToHom ⋯ ≫ (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫ CategoryTheory.eqToHom ⋯)
    CategoryTheory.Functor.ext._auto_1

Tactic:
intro _ _ f
      suffices Path.Homotopic.pi ((CategoryTheory.Functor.pi' (proj X)).map f) = f by simpa
      change Path.Homotopic.pi (fun i => (CategoryTheory.Functor.pi' (proj X)).map f i) = _
      simp

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

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
⊢ ∀ (X : ↑(π.obj (TopCat.of (↑A × ↑B)))),
    ((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X = (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X

Tactic:
intros; apply FundamentalGroupoid.ext; apply Prod.ext <;> simp <;> rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : C
w✝ : IsCofibrant X
⊢ toHoCat.map (toHoCat.obj (mk X)).as.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map (bifibrantResolution.map (adjUnit.app (toHoCat.obj (mk X)))) =
    toHoCat.map (toHoCat.obj (mk X)).as.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map
        (adjCounitIso.inv.app (BifibrantObject.toHoCat.obj (mk X).bifibrantResolutionObj))

Tactic:
simp only [HoCat.adjCounitIso_inv_app]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : C
w✝ : IsCofibrant X
⊢ toHoCat.map (toHoCat.obj (mk X)).as.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map (bifibrantResolution.map (adjUnit.app (toHoCat.obj (mk X)))) =
    toHoCat.map (toHoCat.obj (mk X)).as.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map
        (BifibrantObject.toHoCat.map
          (BifibrantObject.homMk (mk (mk X).bifibrantResolutionObj.obj).iBifibrantResolutionObj.hom))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this✝ : ∀ (j : Fin (n + 1)), j ≠ i → j ∈ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)
this : Finset.image ⇑(SimplexCategory.Hom.toOrderHom f) ⊤ ∪ {i} = ⊤
⊢ False

Tactic:
have := (congr_arg Finset.card this).symm.le.trans (Finset.card_union_le _ _)

Goal state after:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this✝¹ : ∀ (j : Fin (n + 1)), j ≠ i → j ∈ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)
this✝ : Finset.image ⇑(SimplexCategory.Hom.toOrderHom f) ⊤ ∪ {i} = ⊤
this : ⊤.card ≤ (Finset.image ⇑(SimplexCategory.Hom.toOrderHom f) ⊤).card + {i}.card
⊢ False
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: case mpr.refine_1
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
h₁ :
  ∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
    c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
      d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
h₂ : ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x
x₁ x₂ : d.multispan.ColimitType
h : d.multispan.descColimitType c x₁ = d.multispan.descColimitType c x₂
⊢ x₁ = x₂

Tactic:
obtain ⟨i₁, a₁, rfl⟩ := this x₁

Goal state after:
case mpr.refine_1
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
h₁ :
  ∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
    c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
      d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
h₂ : ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x
x₂ : d.multispan.ColimitType
i₁ : J.R
a₁ : d.right i₁
h :
  d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i₁) a₁) =
    d.multispan.descColimitType c x₂
⊢ d.multispan.ιColimitType (WalkingMultispan.right i₁) a₁ = x₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits

Goal state before:
pp: X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
⊢ IsColimit ((PushoutCocone.mk (homOfLE ⋯) (homOfLE ⋯) ⋯).map ((evaluation SimplexCategoryᵒᵖ (Type u)).obj n))

Tactic:
have h : Lattice.BicartSq (A₁.obj n) (A₂.obj n) (A₃.obj n) (A₄.obj n) :=
          { sup_eq := by
              rw [← sq.sup_eq]
              rfl
            inf_eq := by
              rw [← sq.inf_eq]
              rfl }

Goal state after:
X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
h : Lattice.BicartSq (A₁.obj n) (A₂.obj n) (A₃.obj n) (A₄.obj n)
⊢ IsColimit ((PushoutCocone.mk (homOfLE ⋯) (homOfLE ⋯) ⋯).map ((evaluation SimplexCategoryᵒᵖ (Type u)).obj n))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

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

Tactic:
by
  refine ⟨fun h ↦ ?_, fun hA ↦ ?_⟩
  · rintro rfl
    exact lt_irrefl _ (lt_of_le_of_lt h (boundary_lt_top n))
  · have := subcomplex_hasDimensionLT_of_neq_top A hA
    rw [Subcomplex.le_iff_contains_nonDegenerate]
    rintro m ⟨x, h₁⟩ h₂
    dsimp at h₂ ⊢
    by_cases! h₃ : m < n
    · simp [boundary_obj_eq_univ m n h₃]
    · simp [← A.mem_nonDegenerate_iff ⟨x, h₂⟩,
        nonDegenerate_eq_empty_of_hasDimensionLT _ _ _ h₃] at h₁

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

Goal state before:
pp: case refine_2
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
h : ((skeletonOfMono i) d).preimage c.map = ⊤
this : stdSimplex.objEquiv.symm (𝟙 ⦋d⦌) ∈ (((skeletonOfMono i) d).preimage c.map).obj (op ⦋d⦌)
⊢ c.simplex ∈ Set.range ⇑(ConcreteCategory.hom (i.app (op ⦋d⦌)))

Tactic:
simpa [mem_skeletonOfMono_obj_iff]

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

Goal state before:
pp: n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
⊢ sy.spineToSimplex (m + 1) ⋯ (f.map σ) =
    (ConcreteCategory.hom (σ.app (op { obj := ⦋m + 1⦌, property := ⋯ }))) (sx.spineToSimplex (m + 1) ⋯ f)

Tactic:
apply sy.spineInjective (m + 1)
  ext k
  dsimp only [spineEquiv, Equiv.coe_fn_mk, spine_arrow]
  rw [← types_comp_apply (σ.app _) (Y.map _), ← σ.naturality]
  simp [-NatTrans.naturality]

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

Goal state before:
pp: case «2»
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ (((stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 1).inv) ≫ f₁ =
    (((stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv) ≫ f₃

Tactic:
convert! h₀₂

Goal state after:
case e'_2
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 1).inv =
    stdSimplex.δ 2

case e'_3
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv =
    stdSimplex.δ 1
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inr.zero
X : SSet
sx : X.StrictSegal
i : Fin (0 + 3)
σ₀ : Λ[0 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (0 + 2)
j : Fin (0 + 3)
hj : j ≠ i
k : Fin (0 + 1)
ksucc : Fin (0 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

pp: case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
· /- The only inner horn of `Δ[2]` does not contain the diagonal edge. -/
      obtain rfl : k = 0 := by omega
      fin_cases i <;> contradiction

Goal state after:
case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ G✝ : C ⥤ D
F G A : C ⥤ Type w
a : F ⊗ A ⟶ G
c✝ d✝ : C
φ : c✝ ⟶ d✝
y : A.obj c✝
⊢ (F.map φ ≫ ↾fun x ↦ (ConcreteCategory.hom (a.app d✝)) (x, (ConcreteCategory.hom (A.map φ)) y)) =
    (↾fun x ↦ (ConcreteCategory.hom (a.app c✝)) (x, y)) ≫ G.map φ

Tactic:
by
    ext x
    simpa using! (a.naturality_apply φ) (x, y)

Goal state after: