mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.Retracts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalPresentable X κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
⊢ IsColimit ((coyoneda.obj (Opposite.op Y)).mapCocone c)

Tactic:
have := essentiallySmallSelf J

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalPresentable X κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this : EssentiallySmall.{max ?u.47 w, w, w} J
⊢ IsColimit ((coyoneda.obj (Opposite.op Y)).mapCocone c)
Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : isCardinalPresentable C κ X
⊢ P.retractClosure X

Tactic:
rw [isCardinalPresentable_iff] at hX

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : IsCardinalPresentable X κ
⊢ P.retractClosure X
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
⊢ ∃ h, Nonempty (categoryFamily Ω h ≌ C)

Tactic:
let f₂ (X Y) := (Cardinal.lift_mk_le'.1 (h₂ X Y)).some

Goal state after:
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
f₂ : (X Y : C) → (X ⟶ Y) ↪ Ω := fun X Y ↦ ⋯.some
⊢ ∃ h, Nonempty (categoryFamily Ω h ≌ C)
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
⊢ ∃ S, Nonempty (categoryFamily κ S ≌ C)

Tactic:
let f₂ (X Y) := (Cardinal.lift_mk_le'.1 (h₂ X Y)).some

Goal state after:
κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
f₂ : (X Y : C) → (X ⟶ Y) ↪ Ω := fun X Y ↦ ⋯.some
⊢ ∃ S, Nonempty (categoryFamily κ S ≌ C)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
c : f.Cell i
hx : x ∈ (range (c.mapToSucc ≫ (f.filtration (Order.succ i)).ι)).obj d
hi : i ≤ i
⊢ (x ∈ A.obj d ∨ ∃ i_1 < i, ∃ i, x ∈ (↑(P.p i.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b i).app d)) y) = x

Tactic:
← c.ι_b_assoc

Goal state after:
case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
c : f.Cell i
hx : x ∈ (range (c.ιSigmaStdSimplex ≫ f.b i ≫ (f.filtration (Order.succ i)).ι)).obj d
hi : i ≤ i
⊢ (x ∈ A.obj d ∨ ∃ i_1 < i, ∃ i, x ∈ (↑(P.p i.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b i).app d)) y) = 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 : ι
c : f.Cell j
⊢ ↑((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⦌)))) =
    ((↑(P.p c.s)).cast ⋯).simplex

Tactic:
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.Presentable.Presheaf

Goal state before:
pp: C : Type u
inst✝² : SmallCategory C
inst✝¹ : HasColimitsOfSize.{w, w, max u u', max (u + 1) (u' + 1)} (Type (max u u'))
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
X : C
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J (coyoneda.obj (op (uliftYoneda.{u', u, u}.obj X)))

Tactic:
let e : (coyoneda.obj (op (uliftYoneda.{u'}.obj X))) ≅
        (evaluation _ _).obj (op X) ⋙ uliftFunctor :=
      NatIso.ofComponents (fun P ↦ Equiv.toIso (uliftYonedaEquiv.trans Equiv.ulift.symm))

Goal state after:
C : Type u
inst✝² : SmallCategory C
inst✝¹ : HasColimitsOfSize.{w, w, max u u', max (u + 1) (u' + 1)} (Type (max u u'))
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
X : C
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
e : coyoneda.obj (op (uliftYoneda.{u', u, u}.obj X)) ≅
  (evaluation Cᵒᵖ (Type (max u' u))).obj (op X) ⋙ uliftFunctor.{max u u', max u u'} :=
  NatIso.ofComponents (fun P ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯
⊢ PreservesColimitsOfShape J (coyoneda.obj (op (uliftYoneda.{u', u, u}.obj X)))
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : isCardinalPresentable C κ X
⊢ P.colimitsCardinalClosure κ X

Tactic:
rw [isCardinalPresentable_iff] at hX

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : IsCardinalPresentable X κ
⊢ P.colimitsCardinalClosure κ X
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
⊢ ⇑N.opEquiv ⁻¹' P.I ∩ ⇑N.opEquiv ⁻¹' P.II = ∅

Tactic:
simp [← Set.preimage_inter, P.inter]

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

Goal state before:
pp: 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
hi✝ : i.succ ≤ min x hd
hi : i.succ < min x hd
⊢ ↑i.castSucc < ↑(i.castSucc.succ.castPred ⋯)

Tactic:
dsimp; grind

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

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
⊢ hx.simplex hd ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)

Tactic:
rw [nonDegenerate_iff_strictMono_objEquiv, Equiv.apply_symm_apply]

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
⊢ StrictMono ⇑{ toFun := φ x hd, monotone' := ⋯ }
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.degenerate n
⊢ X.ιNormalizedChainComplex x ≫ (X.fromNormalizedChainComplex R).f n = 0

Tactic:
ιNormalizedChainComplex_fromNormalizedChainComplex_f

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.degenerate n
⊢ X.ιChainComplex x ≫ PInfty.f n = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: 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₂
adj₂ : F ⊣₂ G
X₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝ : Arrow C₂
⊢ (F.leibnizPushout.obj X₁).map
        ({
              app := fun X₂ ↦
                Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                  (pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                    (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj X₂).right))) ⋯)
                  ⋯,
              naturality := ⋯ }.app
          x✝) ≫
      {
            app := fun X₃ ↦
              Arrow.homMk
                (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj X₃).left))
                  (adj₂.homEquiv.symm
                    (pullback.fst ((G.obj (op (unop (op X₁)).left)).map X₃.hom)
                      ((G.map (unop (op X₁)).hom.op).app X₃.right)))
                  ⋯)
                (adj₂.homEquiv.symm
                  (pullback.snd ((G.obj (op (unop (op X₁)).left)).map X₃.hom)
                    ((G.map (unop (op X₁)).hom.op).app X₃.right)))
                ⋯,
            naturality := ⋯ }.app
        ((F.leibnizPushout.obj X₁).obj x✝) =
    𝟙 ((F.leibnizPushout.obj X₁).obj x✝)

Tactic:
by
    ext
    · apply pushout.hom_ext <;> simp [← homEquiv_symm_naturality_two, ofHasPushout_pt]
    · simp [← homEquiv_symm_naturality_two]

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

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 2)
n : ℕ
hk : k = Fin.last (m + 1)
⊢ (Λ[m + 1, Fin.castSucc 0].unionProd ∂Δ[n]).op.preimage
      (((stdSimplex.opIso ⦋m + 1⦌).symm ⊗ᵢ (stdSimplex.opIso ⦋n⦌).symm) ≪≫
          Functor.Monoidal.μIso opFunctor Δ[m + 1] Δ[n]).hom =
    Λ[m + 1, k].unionProd ∂Δ[n]

Tactic:
by
          dsimp
          rw [hk, Subcomplex.preimage_comp,
            Subcomplex.preimage_op_unionProd,
            Subcomplex.preimage_unionProd,
            op_boundary, op_horn, Fin.rev_zero]

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : CharZero 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
⊢ AnalyticAt 𝕜 g (f x)

Tactic:
let r := hf.hasStrictDerivAt.localInverse _ _ _ hf'

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : CharZero 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
⊢ AnalyticAt 𝕜 g (f x)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
c : ℝ
hc : 0 < c
hvw : (fun x ↦ v x ^ c) = ⇑w
x : WithAbs w
hx : w x.ofAbs < ε ^ c
⊢ (WithAbs.congr v w (RingEquiv.refl F)).symm x ∈ Metric.ball 0 ε

Tactic:
← funext_iff.1 hvw,

Goal state after:
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
c : ℝ
hc : 0 < c
hvw : (fun x ↦ v x ^ c) = ⇑w
x : WithAbs w
hx : v x.ofAbs ^ c < ε ^ c
⊢ (WithAbs.congr v w (RingEquiv.refl F)).symm x ∈ Metric.ball 0 ε
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z₀ = ↑n ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
by
  unfold analyticOrderAt
  split_ifs with h
  · simp only [ENat.top_ne_natCast, false_iff]
    contrapose h
    rw [← hf.exists_eventuallyEq_pow_smul_nonzero_iff]
    exact ⟨n, h⟩
  · rw [← hf.exists_eventuallyEq_pow_smul_nonzero_iff] at h
    refine ⟨fun hn ↦ (WithTop.coe_inj.mp hn : h.choose = n) ▸ h.choose_spec, fun h' ↦ ?_⟩
    rw [AnalyticAt.unique_eventuallyEq_pow_smul_nonzero h.choose_spec h']

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

Goal state before:
pp: case refine_2.succ.zero.«0»
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
H :
  ∀ (x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })) (y : Y.obj (op { obj := ⦋2⦌, property := _proof_14 })),
    f₁ ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x) =
        (ConcreteCategory.hom (Y.map (δ₂ 2 _proof_12 _proof_15).op)) y →
      f₁ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_12 _proof_15).op)) y →
        f₁ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_12 _proof_15).op)) y
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
hn : 0 + 1 < 2
x✝ : X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ })
⊢ (ConcreteCategory.hom
          (X.map (σ 2 ((fun i ↦ i) ⟨0, ⋯⟩) ⋯ ⋯).op ≫
            app f₀ f₁ hδ₁ hδ₀ hY (op { obj := ⦋0 + 1 + 1⦌, property := ⋯ }))).toFun
      x✝ =
    (ConcreteCategory.hom
          (app f₀ f₁ hδ₁ hδ₀ hY (op { obj := ⦋0 + 1⦌, property := ⋯ }) ≫ Y.map (σ 2 ((fun i ↦ i) ⟨0, ⋯⟩) ⋯ ⋯).op)).toFun
      x✝

Tactic:
apply hσ'₀ f₀ f₁ hδ₁ hδ₀ hσ 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, f y = 0
h₂t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h₃t : z₀ ∈ t
⊢ ∃ t, (∀ y ∈ t, (f • g) y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t

Tactic:
exact ⟨t, fun y hy ↦ by simp [h₁t y hy], h₂t, h₃t⟩

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
⊢ ∃ t, (∀ y ∈ t, (f • g) y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t

Tactic:
exact ⟨t, fun y hy ↦ by simp [h₁t y hy], h₂t, h₃t⟩

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖↑A.symm (f x') - ↑A.symm (f y') - ↑f'.symm (f x' - f y')‖ ≤
    ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖f x' - f y'‖

Tactic:
rw [← Af x', ← Af y', A.left_inv x's, A.left_inv y's]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖x' - y' - ↑f'.symm (↑A x' - ↑A y')‖ ≤ ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖↑A x' - ↑A y'‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * - -1 - cexp (x * I) * (1 * I) * I) * 2⁻¹

Tactic:
neg_neg,

Goal state after:
case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * 1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ⋯
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
v_in : v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ContinuousWithinAt (fun y ↦ ‖f y.2 - f y.1 - (f' y.2 - f' y.1)‖) (s ×ˢ s) (u, v)

Tactic:
simp only [ContinuousWithinAt]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
v_in : v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun y ↦ ‖f y.2 - f y.1 - (f' y.2 - f' y.1)‖) (𝓝[s ×ˢ s] (u, v)) (𝓝 ‖f v - f u - (f' v - f' u)‖)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝² : AddCommMonoid R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ multichoose r 0 = r ^ 0

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero 0),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_zero, smeval_one, Nat.factorial]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ⋯
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
v_in : v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ContinuousWithinAt (fun y ↦ ε * ‖y.2 - y.1‖) (s ×ˢ s) (u, v)

Tactic:
simp only [ContinuousWithinAt]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
v_in : v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun y ↦ ε * ‖y.2 - y.1‖) (𝓝[s ×ˢ s] (u, v)) (𝓝 (ε * ‖v - u‖))
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: r : ℤ
k : ℕ
⊢ (k.factorial •
      match r with
      | ofNat n => ↑((n + k - 1).choose k)
      | -[n+1] => ↑(↑k).negOnePow * ↑((n + 1).choose k)) =
    (ascPochhammer ℕ k).smeval r

Tactic:
nsmul_eq_mul

Goal state after:
r : ℤ
k : ℕ
⊢ (↑k.factorial *
      match r with
      | ofNat n => ↑((n + k - 1).choose k)
      | -[n+1] => ↑(↑k).negOnePow * ↑((n + 1).choose k)) =
    (ascPochhammer ℕ k).smeval r