mathlib-initiative/mathlib-tactics huggingface dataset:
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)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂
this : IsFiltered J
y₁ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₁
y₂ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₂
hy₁ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁
hy₂ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₂ = x₂
k : K
⊢ (ConcreteCategory.hom (((F.obj k).mapCocone cX).ι.app j))
      ((ConcreteCategory.hom ((((evaluation C (Type w')).obj (X.obj j)).mapCone c).π.app k)) x₁) =
    (ConcreteCategory.hom (((F.obj k).mapCocone cX).ι.app j))
      ((ConcreteCategory.hom ((((evaluation C (Type w')).obj (X.obj j)).mapCone c).π.app k)) x₂)

Tactic:
dsimp at h ⊢

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)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂
this : IsFiltered J
y₁ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₁
y₂ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₂
hy₁ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁
hy₂ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₂ = x₂
k : K
⊢ (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j))) ((ConcreteCategory.hom ((c.π.app k).app (X.obj j))) x₁) =
    (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j))) ((ConcreteCategory.hom ((c.π.app k).app (X.obj 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ᵒᵖ
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

Tactic:
simp only [filtration_def, Order.lt_succ_iff, Subfunctor.max_obj, Subfunctor.iSup_obj,
    Set.mem_union, Set.mem_iUnion, exists_prop, Subfunctor.toFunctor_obj, Subfunctor.homOfLe_app,
    TypeCat.hom_ofHom, TypeCat.Fun.coe_mk, Set.sup_eq_union, Set.mem_range, Subtype.ext_iff,
    Subtype.exists, exists_eq_right, Set.mem_univ, iff_true] at 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 ∈ A.obj d ∨ ∃ i ≤ j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d
⊢ (x ∈ A.obj d ∨ ∃ i < j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b j).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 : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
⊢ IsPushout (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.t j))
    (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j))
    (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (homOfLE ⋯))
    (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))

Tactic:
refine Types.isPushout_of_isPullback_of_mono'
      ((f.isPullback j).map ((CategoryTheory.evaluation _ _).obj _))
      (f.range_homOfLE_app_union_range_b_app _ _) (fun x₁ x₂ hx₁ hx₂ h ↦ ?_)

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 : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
h :
  (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₁ =
    (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₂
⊢ x₁ = x₂
Module: Mathlib.CategoryTheory.Presentable.Presheaf

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
A : Type u'
inst✝⁴ : Category.{v', u'} A
inst✝³ : HasColimitsOfSize.{w, w, v', u'} A
inst✝² : HasCoproducts A
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
X : C
M : A
inst✝ : IsCardinalPresentable M κ
e : coyoneda.obj (op (freeYoneda X M)) ≅ (evaluation Cᵒᵖ A).obj (op X) ⋙ coyoneda.obj (op M) ⋙ uliftFunctor.{u, v'} := ⋯
⊢ autoParam
    (∀ (J : Type w) [inst : SmallCategory J] [IsCardinalFiltered J κ],
      PreservesColimitsOfShape J (coyoneda.obj (op (freeYoneda X M))))
    Functor.IsCardinalAccessible.preservesColimitOfShape._autoParam

Tactic:
intro J

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
A : Type u'
inst✝⁴ : Category.{v', u'} A
inst✝³ : HasColimitsOfSize.{w, w, v', u'} A
inst✝² : HasCoproducts A
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
X : C
M : A
inst✝ : IsCardinalPresentable M κ
e : coyoneda.obj (op (freeYoneda X M)) ≅ (evaluation Cᵒᵖ A).obj (op X) ⋙ coyoneda.obj (op M) ⋙ uliftFunctor.{u, v'} :=
  NatIso.ofComponents (fun P ↦ (freeYonedaHomEquiv.trans Equiv.ulift.symm).toIso) ⋯
J : Type w
⊢ ∀ [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J (coyoneda.obj (op (freeYoneda X M)))
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 : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
⊢ k.succ ≤ (x.cast hd).simplex.1 i ↔ l.succ ≤ i

Tactic:
refine ⟨fun hi ↦ ?_, fun hi ↦ ?_⟩

Goal state after:
case refine_1
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
hi : k.succ ≤ (x.cast hd).simplex.1 i
⊢ l.succ ≤ i

case refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
hi : l.succ ≤ i
⊢ k.succ ≤ (x.cast hd).simplex.1 i
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: case h₀
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₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
⊢ sq₁₂.inl ≫
      ⋯.desc (adj₂.homEquiv.symm (Arrow.Hom.left β)) (adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.fst)) ⋯ ≫
        (Arrow.mk f₃).hom =
    sq₁₂.inl ≫ (Arrow.mk sq₁₂.ι).hom ≫ adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.snd)

pp: case h₁
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₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
⊢ sq₁₂.inr ≫
      ⋯.desc (adj₂.homEquiv.symm (Arrow.Hom.left β)) (adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.fst)) ⋯ ≫
        (Arrow.mk f₃).hom =
    sq₁₂.inr ≫ (Arrow.mk sq₁₂.ι).hom ≫ adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.snd)

Tactic:
· have := Arrow.w β =≫ sq₁₃.snd
          dsimp at this
          simp only [Category.assoc, sq₁₃.π_snd] at this
          simp [← adj₂.homEquiv_symm_naturality_two,
            ← adj₂.homEquiv_symm_naturality_three, this]

Goal state after:
case h₁
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₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
⊢ sq₁₂.inr ≫
      ⋯.desc (adj₂.homEquiv.symm (Arrow.Hom.left β)) (adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.fst)) ⋯ ≫
        (Arrow.mk f₃).hom =
    sq₁₂.inr ≫ (Arrow.mk sq₁₂.ι).hom ≫ adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.snd)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: case refine_1
X : SSet
x✝ : IsEmpty (X _⦋0⦌)
n : ℕ
hn : 0 ≤ n
⊢ X.degenerate n = ⊤

pp: case refine_2
X : SSet
x✝ : X.HasDimensionLT 0
x : X _⦋0⦌
⊢ False

Tactic:
· have := Function.isEmpty (X.map (⦋0⦌.const ⦋n⦌ 0).op)
    subsingleton

Goal state after:
case refine_2
X : SSet
x✝ : X.HasDimensionLT 0
x : X _⦋0⦌
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case neg.succ
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
i : Fin (d + 1 + 1)
hx : IsIndex x ⋯ i
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }

Tactic:
· obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (i := i) (by rintro rfl; simp at hx)
        refine ⟨{ x := x, d := d, hd := hd, index := i, isIndex := hx }, Or.inl ?_⟩
        dsimp
        rw [S.ext_iff']
        exact ⟨hd, rfl⟩

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Field R
inst✝² : Semifield S
inst✝¹ : LinearOrder S
v w : AbsoluteValue R S
inst✝ : IsStrictOrderedRing S
⊢ v.IsEquiv w ↔ ∀ (x : R), v x < 1 ↔ w x < 1

Tactic:
by
  refine ⟨fun h _ ↦ h.lt_one_iff, fun h x y ↦ ?_⟩
  rcases eq_or_ne (v x) 0 with (_ | hy₀)
  · simp_all
  rw [le_iff_le_iff_lt_iff_lt, ← one_mul (v x), ← mul_inv_lt_iff₀ (by simp_all), ← one_mul (w x),
    ← mul_inv_lt_iff₀ (by simp_all), ← map_inv₀, ← map_mul, ← map_inv₀, ← map_mul]
  exact h _

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : w a ≠ 1
hwa : 1 < w a
⊢ 0 < log (w a) / log (v a)

Tactic:
exact div_pos (log_pos <| hwa) (log_pos (h.one_lt_iff.2 hwa))

Goal state after:
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
⊢ ∃ ε > 0, Metric.ball 0 ε ⊆ ⇑(WithAbs.congr v w (RingEquiv.refl F)) '' U

Tactic:
obtain ⟨c, hc, hvw⟩ := isEquiv_iff_exists_rpow_eq.1 h

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
⊢ ∃ ε > 0, Metric.ball 0 ε ⊆ ⇑(WithAbs.congr v w (RingEquiv.refl F)) '' U
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case coe
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
⊢ analyticOrderAt (deriv f) x + 1 = ↑r

Tactic:
have hrne : r ≠ 0 := by
      intro hr
      rw [hr, ENat.natCast_zero, AnalyticAt.analyticOrderAt_eq_zero (by fun_prop)] at h
      grind

Goal state after:
case coe
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
hrne : r ≠ 0
⊢ analyticOrderAt (deriv f) x + 1 = ↑r
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CharZero 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
horder : analyticOrderAt f z₀ = ↑n + 1
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg₀ : g z₀ ≠ 0
hfg : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ (fun x1 x2 ↦ x1 + x2) n 1 • g z
⊢ analyticOrderAt (deriv f) z₀ = ↑n

Tactic:
have hz₀ : f z₀ = 0 := by
    simpa [sub_self, zero_pow, zero_smul] using Filter.Eventually.self_of_nhds hfg

Goal state after:
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CharZero 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
horder : analyticOrderAt f z₀ = ↑n + 1
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg₀ : g z₀ ≠ 0
hfg : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ (fun x1 x2 ↦ x1 + x2) n 1 • g z
hz₀ : f z₀ = 0
⊢ analyticOrderAt (deriv f) z₀ = ↑n
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : Category.{u, u} C
inst✝ : Category.{u, u} D
this : IsIso (prodComparison (hoFunctor ⋙ nerveFunctor) (nerve C) (nerve D))
⊢ IsIso (nerveFunctor.map (prodComparison hoFunctor (nerve C) (nerve D)))

Tactic:
exact IsIso.of_isIso_fac_right (prodComparison_comp hoFunctor nerveFunctor).symm

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

Goal state before:
pp: case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑z ∈ t
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x

Tactic:
obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz

Goal state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
t' : Set 𝕜
h₁t' : ∀ y ∈ t', f y = 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
a : 𝕜
ha : f a ≠ 0
⊢ a ∈ (U \ Subtype.val '' {u | analyticOrderAt f ↑u = 0 ∨ analyticOrderAt f ↑u = ⊤})ᶜ

Tactic:
simp +contextual [(hf a _).analyticOrderAt_eq_zero, ha]

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
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
a : 𝕜
ha : f a ≠ 0
⊢ a ∈ (U \ {u | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ

Tactic:
simp +contextual [(hf a _).analyticOrderAt_eq_zero, ha]

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
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
⊢ MeromorphicAt (deriv f) x

Tactic:
rw [MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt] at h
  obtain ⟨n, g, h₁g, h₂g⟩ := h
  have : _root_.deriv (fun z ↦ (z - x) ^ n • g z)
      =ᶠ[𝓝[≠] x] fun z ↦ (n * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • _root_.deriv g z := by
    filter_upwards [eventually_nhdsWithin_of_eventually_nhds h₁g.eventually_analyticAt,
      eventually_nhdsWithin_of_forall fun _ a ↦ a] with z₀ h₁ h₂
    rw [deriv_fun_smul (DifferentiableAt.zpow (by fun_prop) (by simp_all [sub_ne_zero_of_ne h₂]))
      (by fun_prop), add_comm, deriv_comp_sub_const (f := (· ^ n))]
    aesop
  rw [MeromorphicAt.meromorphicAt_congr (Filter.EventuallyEq.nhdsNE_deriv h₂g),
    MeromorphicAt.meromorphicAt_congr this]
  fun_prop

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

Goal state before:
pp: case succ
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
⊢ Set.EqOn (iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B)
    (fun x ↦ (descPochhammer ℤ (n + 1)).smeval a * (1 + x) ^ (a - ↑(n + 1))) B

Tactic:
have : iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B =
        derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B := by
      ext z
      rw [iteratedDerivWithin_succ]
    rw [this]
    have : Set.EqOn (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
        (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B := by
      intro z hz
      rw [derivWithin_congr (fun _ hz ↦ ih hz) (ih hz)]
    apply Set.EqOn.trans this
    intro z hz
    simp only [Nat.cast_add, Nat.cast_one, B, derivWithin_of_isOpen Metric.isOpen_ball hz,
      deriv_const_mul_field']
    rw [_root_.deriv_cpow_const (by fun_prop), deriv_const_add_id, mul_one,
      show a - (n + 1) = a - n - 1 by ring, ← mul_assoc]
    · congr
      simp [descPochhammer_succ_right, Polynomial.smeval_mul, Polynomial.smeval_natCast]
    · apply Complex.mem_slitPlane_of_norm_lt_one
      simpa [B] using hz

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
n : ℕ
⊢ Tendsto (fun a ↦ k a ^ n * f a) l (𝓝 0)

Tactic:
simpa only [zpow_natCast] using! h (n : ℤ)

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
⊢ ∀ (s : Set X) (f : X → Set (Set X)),
    (∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}) →
      (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε) →
        ∃ t, (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p ↦ p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0

Tactic:
by
    intro s f fset ffine
    let g : X → Set (Set X) := fun x => f x ∩ v.setsAt x
    have : ∀ x ∈ s, ∀ ε : ℝ, ε > 0 → ∃ t ∈ g x, t ⊆ closedBall x ε := by
      intro x hx ε εpos
      obtain ⟨t, tf, ht⟩ : ∃ t ∈ f x, t ⊆ closedBall x (min ε δ) :=
        ffine x hx (min ε δ) (lt_min εpos δpos)
      rcases fset x hx tf with (h't | h't)
      · exact ⟨t, ⟨tf, h't⟩, ht.trans (closedBall_subset_closedBall (min_le_left _ _))⟩
      · refine False.elim (h't.2.2 ?_)
        exact ht.trans (closedBall_subset_closedBall (min_le_right _ _))
    rcases v.covering s g (fun x _ => inter_subset_right) this with ⟨t, ts, tdisj, tg, μt⟩
    exact ⟨t, ts, tdisj, fun p hp => (tg p hp).1, μt⟩

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
⊢ ∀ᶠ (t : Set X) in v.filterAt x, MeasurableSet t

Tactic:
filter_upwards [v.eventually_filterAt_mem_setsAt x] with _ ha using v.measurableSet _ _ ha

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
⊢ ∑' (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), μ (u' ↑p ∩ v ↑p ↑q) ≤ ∑' (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), μ (u ↑p ↑q ∩ v ↑p ↑q)

Tactic:
gcongr with p q
        exact biInter_subset_of_mem q.2

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
d_Inter :
  ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋂ n, s n)))
⊢ ∃ s,
    MeasurableSet s ∧
      (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t

Tactic:
have bdd_c : BddAbove c := by
    use (μ univ).toNNReal
    rintro r ⟨s, _hs, rfl⟩
    refine le_trans (sub_le_self _ <| NNReal.coe_nonneg _) ?_
    rw [NNReal.coe_le_coe, ← ENNReal.coe_le_coe, to_nnreal_μ, to_nnreal_μ]
    exact measure_mono (subset_univ _)

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
d_Inter :
  ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋂ n, s n)))
bdd_c : BddAbove c
⊢ ∃ s,
    MeasurableSet s ∧
      (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t