mathlib-initiative/mathlib-tactics huggingface dataset:
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
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : ForgetEnrichment W (TransportEnrichment F D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Z✝))
      ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W (f ≫ g))) =
    (e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Z✝))
      ((λ_ (𝟙_ V)).inv ≫
        ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)).symm (ForgetEnrichment.homTo W f) ⊗ₘ
            (e (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W g)) ≫
          eComp V (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝))

Tactic:
rw [Equiv.apply_symm_apply, h]

Goal state after:
V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : ForgetEnrichment W (TransportEnrichment F D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homTo W (f ≫ g) =
    Functor.LaxMonoidal.ε F ≫
      F.map
        ((λ_ (𝟙_ V)).inv ≫
          ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)).symm (ForgetEnrichment.homTo W f) ⊗ₘ
              (e (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W g)) ≫
            eComp V (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝))
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
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : TransportEnrichment F (ForgetEnrichment V D)
⊢ ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V (𝟙 X))) =
    𝟙 (ForgetEnrichment.of W X)

Tactic:
← ForgetEnrichment.homOf_eId,

Goal state after:
V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : TransportEnrichment F (ForgetEnrichment V D)
⊢ ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V (𝟙 X))) =
    ForgetEnrichment.homOf W (eId W X)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: case comp_of.inl
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f✝¹ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f✝ : X✝ ⟶ Y✝
x✝ X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 2)
f : x✝ ⟶ mk n✝
hf : generators.multiplicativeClosure f
hrec : P f
⊢ P (f ≫ δ i)

pp: case comp_of.inr
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f✝¹ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f✝ : X✝ ⟶ Y✝
x✝ X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 1)
f : x✝ ⟶ mk (n✝ + 1)
hf : generators.multiplicativeClosure f
hrec : P f
⊢ P (f ≫ σ i)

Tactic:
· simpa using! (comp_δ f i hrec)

Goal state after:
case comp_of.inr
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f✝¹ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f✝ : X✝ ⟶ Y✝
x✝ X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 1)
f : x✝ ⟶ mk (n✝ + 1)
hf : generators.multiplicativeClosure f
hrec : P f
⊢ P (f ≫ σ i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ x₂ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
y : Y.HomotopyCategory
⊢ (mkNatTrans (fun y ↦ homMk (e₀₁.tensor (Edge.id y))) ⋯ ≫ mkNatTrans (fun y ↦ homMk (e₁₂.tensor (Edge.id y))) ⋯).app
      y =
    (mkNatTrans (fun y ↦ homMk (e₀₂.tensor (Edge.id y))) ⋯).app y

Tactic:
obtain ⟨y, rfl⟩ := mk_surjective y

Goal state after:
X X' Y Y' Z : Truncated 2
x₀ x₁ x₂ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ (mkNatTrans (fun y ↦ homMk (e₀₁.tensor (Edge.id y))) ⋯ ≫ mkNatTrans (fun y ↦ homMk (e₁₂.tensor (Edge.id y))) ⋯).app
      (mk y) =
    (mkNatTrans (fun y ↦ homMk (e₀₂.tensor (Edge.id y))) ⋯).app (mk y)
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
hk' : ¬j.castSucc < k
⊢ (j.predAbove k).castSucc < i

Tactic:
simp only [not_lt] at hk'
      rw [Fin.predAbove_of_le_castSucc _ _ hk']
      exact lt_of_le_of_lt (by simpa) h

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case left
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : ⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ f)) = ⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ g))
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j✝ : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j✝
j : Fin (x.len + 1)
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j))) =
    ↑((ConcreteCategory.hom g) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j)))

Tactic:
simpa [← inl'_eval, ConcreteCategory.hom, Fin.ext_iff] using congrFun h₁ j

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
⊢ ∀ k ∈ ⇑f '' I.I, { as := f i.as }.as ≤ k

Tactic:
by rintro _ ⟨k, hk, rfl⟩; exact f.monotone (I.left_le k hk)

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

Goal state before:
pp: case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
a b : Fin (n + 1)
hab : (objEquiv z) a = (objEquiv z) b
h : ∀ (x : Fin (n + 1)), ⟨↑(z.1 x) + ↑(z.2 x), ⋯⟩ = x
⊢ ⟨↑(z.1 a) + ↑(z.2 a), ⋯⟩ = b

Tactic:
← h b,

Goal state after:
case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
a b : Fin (n + 1)
hab : (objEquiv z) a = (objEquiv z) b
h : ∀ (x : Fin (n + 1)), ⟨↑(z.1 x) + ↑(z.2 x), ⋯⟩ = x
⊢ ⟨↑(z.1 a) + ↑(z.2 a), ⋯⟩ = ⟨↑(z.1 b) + ↑(z.2 b), ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsRegular
⊢ WellFounded h.pairing.AncestralRel

Tactic:
have := IsRegular.wf h

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsRegular
this : WellFounded h.AncestralRel
⊢ WellFounded h.pairing.AncestralRel
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
φ : T → U
hφ : ∀ (t : T), ψ (φ t) = (↑↑t).toS
t₁ : T
⊢ ∀ ⦃a₂ : T⦄, φ t₁ = φ a₂ → t₁ = a₂

Tactic:
t₂

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
φ : T → U
hφ : ∀ (t : T), ψ (φ t) = (↑↑t).toS
t₁ t₂ : T
⊢ φ t₁ = φ t₂ → t₁ = t₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ f.filtration i = ⨆ j, ⨆ (_ : j < i), f.filtration j

Tactic:
by
  apply le_antisymm
  · conv_lhs => rw [filtration_def]
    simp only [sup_le_iff, iSup_le_iff]
    refine ⟨?_, fun j hj c ↦ ?_⟩
    · refine le_trans ?_ (le_iSup _ ⊥)
      exact le_trans (by simp) (le_iSup _ hi.bot_lt)
    · refine le_trans ?_ (le_iSup _ (Order.succ j))
      refine le_trans ?_ (le_iSup _
        (by rwa [← Order.IsSuccLimit.succ_lt_iff hi] at hj))
      exact f.subcomplex_le_filtration _ (Order.lt_succ_of_not_isMax hj.not_isMax)
  · simp only [iSup_le_iff]
    intro j hj
    exact f.filtration_monotone hj.le

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
⊢ ∃ j x', x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j)) x'

Tactic:
obtain ⟨j₀, z, hz⟩ : ∃ (j₀ : J) (z : (k : K) → (F.obj k).obj (X.obj j₀)),
      ∀ (k : K), y.1 k = (F.obj k).map (cX.ι.app j₀) (z k) := by
    have H (k : K) := Types.jointly_surjective_of_isColimit (hF k) (y.1 k)
    let j (k : K) : J := (H k).choose
    let z (k : K) : (F.obj k).obj (X.obj (j k)) := (H k).choose_spec.choose
    have hz (k : K) : (F.obj k).map (cX.ι.app (j k)) (z k) = y.1 k :=
      (H k).choose_spec.choose_spec
    exact ⟨IsCardinalFiltered.max j (hasCardinalLT_of_hasCardinalLT_arrow hK),
      fun k ↦ (F.obj k).map (X.map (IsCardinalFiltered.toMax j _ k)) (z k),
        fun k ↦ by rw [← hz, ← comp_apply, ← Functor.map_comp, cX.w]; rfl⟩

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
⊢ ∃ j x', x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j)) x'
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
⊢ Set.range ⇑(ConcreteCategory.hom ((homOfLE ⋯).app d)) ⊔ Set.range ⇑(ConcreteCategory.hom ((f.b j).app d)) = Set.univ

Tactic:
ext ⟨x, hx⟩

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
hx : x ∈ (f.filtration (Order.succ j)).obj d
⊢ ⟨x, hx⟩ ∈ Set.range ⇑(ConcreteCategory.hom ((homOfLE ⋯).app d)) ⊔ Set.range ⇑(ConcreteCategory.hom ((f.b j).app d)) ↔
    ⟨x, hx⟩ ∈ Set.univ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ { dim := c.dim + 1,
      simplex :=
        ↑((ConcreteCategory.hom ((f.b j).app (op ⦋c.dim + 1⦌)))
            ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)))
              (stdSimplex.objEquiv.symm (𝟙 ⦋c.dim + 1⦌)))) } =
    { dim := (↑c.s).dim + 1, simplex := ((↑(P.p c.s)).cast ⋯).simplex }

Tactic:
rw [S.ext_iff, c.ι_b_app_apply]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ ↑((ConcreteCategory.hom (c.mapToSucc.app (op ⦋c.dim + 1⦌))) (stdSimplex.objEquiv.symm (𝟙 ⦋c.dim + 1⦌))) =
    ((↑(P.p c.s)).cast ⋯).simplex
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj s.pt :=
  fun s ↦
    {
      app := fun x ↦
        match x with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
X : C
x : (yoneda.obj (F.obj j.left)).obj (F.op.obj (op X))
α : CostructuredArrow.mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x) ⋯
this : (CostructuredArrow.proj F Y ⋙ F).map α ≫ s.ι.app j = s.ι.app (CostructuredArrow.mk (x ≫ j.hom))
⊢ (ConcreteCategory.hom (((restrictedULiftYoneda F).map j.hom ≫ φ s).app (op X))).toFun { down := x } =
    (ConcreteCategory.hom (((restrictedULiftYoneda F).map (s.ι.app j)).app (op X))).toFun { down := x }

Tactic:
dsimp [uliftYoneda, φ, α] at this ⊢

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj s.pt :=
  fun s ↦
    {
      app := fun x ↦
        match x with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
X : C
x : (yoneda.obj (F.obj j.left)).obj (F.op.obj (op X))
α : CostructuredArrow.mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x) ⋯
this : F.map (F.preimage x) ≫ s.ι.app j = s.ι.app (CostructuredArrow.mk (x ≫ j.hom))
⊢ { down := s.ι.app (CostructuredArrow.mk (x ≫ j.hom)) } = { down := x ≫ s.ι.app j }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: ⊢ strongAnodyneExtensions ≤ anodyneExtensions

Tactic:
rintro X Y f ⟨_, P, _⟩
  rw [← Subfunctor.toRange_ι f]
  exact comp_mem _ _ _ (.of_isIso _) P.anodyneExtensions

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
inst✝ : CategoryWithHomology C
H : Homotopy f g
n : ℕ
⊢ (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n).map ((alternatingFaceMapComplex C).map f) =
    (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n).map ((alternatingFaceMapComplex C).map g)

Tactic:
simpa using! (H.toChainHomotopy).homologyMap_eq n

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ (tensorLeft X₁.left).map
        (pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom)) ≫
      ((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left ≫
        Arrow.Hom.left (whiskerLeftIso X₂ X₃).hom ≫
          pushout.desc
            (pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
              (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
            (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                X₃.right ≫
              pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
            ⋯ =
    (tensorLeft X₁.left).map
        (pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom)) ≫
      ((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom ≫
        (α_ X₁.left X₂.right X₃.right).inv ≫
          pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
              X₃.right ≫
            pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
              (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom)

Tactic:
simp [whisker_exchange_assoc,
            Limits.pushout.associator_inv_naturality_right_condition, ← whiskerLeft_comp_assoc]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inr.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin (d + 1)
hi : min x hd < i
⊢ (objEquiv (x.cast hd).simplex) (i.castSucc.pred ⋯) < (objEquiv (x.cast hd).simplex) (i.succ.pred ⋯)

Tactic:
exact hx' (by grind)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case inst
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj X₂)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj Y₂)
h : IsInitial X₁
hX₂ : IsInitial ((F.flip.obj X₂).obj X₁) := ⋯
hY₂ : IsInitial ((F.flip.obj Y₂).obj X₁) := ⋯
⊢ IsIso ((F.obj X₁).map f₂)

Tactic:
exact isIso_of_isInitial hX₂ hY₂ _

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
hn : n ≠ 1
⊢ (X.chainComplex R).d n 0 ≫ fromChainComplexXZero X R = 0

Tactic:
rw [HomologicalComplex.shape _ _ _ (by simp; lia), zero_comp]

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
t : Set 𝕜
h₁t : ∀ y ∈ t, f y = 0
h₂t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h₃t : z₀ ∈ t
y : 𝕜
hy : y ∈ t
⊢ (f • g) y = 0

Tactic:
by simp [h₁t y hy]

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
t : Set 𝕜
h₁t : ∀ y ∈ t, g y = 0
h₂t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h₃t : z₀ ∈ t
y : 𝕜
hy : y ∈ t
⊢ (f • g) y = 0

Tactic:
by simp [h₁t y hy]

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case succ
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
inst✝ : CharZero 𝕜
n' : ℕ
hk : ∀ {n : ℕ}, ↑n = analyticOrderAt f z₀ → n ≠ 0 → n' ≤ n → analyticOrderAt (deriv^[n'] f) z₀ = ↑(n - n')
n : ℕ
⊢ ↑n = analyticOrderAt f z₀ → n ≠ 0 → n' + 1 ≤ n → analyticOrderAt (deriv^[n' + 1] f) z₀ = ↑(n - (n' + 1))

Tactic:
intro Hn

Goal state after:
case succ
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
inst✝ : CharZero 𝕜
n' : ℕ
hk : ∀ {n : ℕ}, ↑n = analyticOrderAt f z₀ → n ≠ 0 → n' ≤ n → analyticOrderAt (deriv^[n'] f) z₀ = ↑(n - n')
n : ℕ
Hn : ↑n = analyticOrderAt f z₀
⊢ n ≠ 0 → n' + 1 ≤ n → analyticOrderAt (deriv^[n' + 1] f) z₀ = ↑(n - (n' + 1))
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
x : 𝔸
n : ℕ
⊢ ((ordinaryHypergeometricSeries 𝔸 a b c n) fun x_1 ↦ x) =
    ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n

Tactic:
rw [ordinaryHypergeometricSeries, ofScalars_apply_eq]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : f =ᶠ[𝓝[≠] x] g
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (fun z ↦ z - x) x
⊢ AnalyticAt 𝕜 (fun z ↦ (z - x) ^ (m + 1) • g z) x

Tactic:
refine (this.fun_smul hf).congr ?_

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : f =ᶠ[𝓝[≠] x] g
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (fun z ↦ z - x) x
⊢ (fun i ↦ (i - x) • (i - x) ^ m • f i) =ᶠ[𝓝 x] fun z ↦ (z - x) ^ (m + 1) • g z