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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst✝ : LocallySmall.{w, v, u} C
X : C
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
⊢ ∃ κ', ∃ (_ : Fact κ'.IsRegular) (_ : κ ≤ κ'), HasCardinalLT (Arrow J) κ'

Tactic:
obtain ⟨κ', h₁, h₂⟩ := HasCardinalLT.exists_regular_cardinal_forall.{w}
      (Sum.elim (fun (_ : Unit) ↦ Arrow J) (fun (_ : Unit) ↦ κ.ord.ToType))

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst✝ : LocallySmall.{w, v, u} C
X : C
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
κ' : Cardinal.{w}
h₁ : κ'.IsRegular
h₂ : ∀ (i : Unit ⊕ Unit), HasCardinalLT (Sum.elim (fun x ↦ Arrow J) (fun x ↦ κ.ord.ToType) i) κ'
⊢ ∃ κ', ∃ (_ : Fact κ'.IsRegular) (_ : κ ≤ κ'), HasCardinalLT (Arrow J) κ'
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₁
⊢ ∃ j' α, (ConcreteCategory.hom (c.pt.map (X.map α))) x₁ = (ConcreteCategory.hom (c.pt.map (X.map α))) x₂

Tactic:
let y₂ := Types.isLimitEquivSections (hc (X.obj j)) x₂

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₂
⊢ ∃ j' α, (ConcreteCategory.hom (c.pt.map (X.map α))) x₁ = (ConcreteCategory.hom (c.pt.map (X.map α))) 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 : ℕ
⊢ IsPullback (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:
Types.isPullback_iff

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 : ℕ
⊢ CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.t j) ≫
        CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (homOfLE ⋯) =
      CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j) ≫
        CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j) ∧
    (∀ (x₁ y₁ : (fun X ↦ X) (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaHorn j))),
        (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.t j))) x₁ =
              (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.t j))) y₁ ∧
            (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j))) x₁ =
              (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j))) y₁ →
          x₁ = y₁) ∧
      ∀ (x₂ : (fun X ↦ X) (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.filtration j).toSSet))
        (x₃ : (fun X ↦ X) (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j))),
        (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (homOfLE ⋯))) x₂ =
            (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₃ →
          ∃ x₁,
            (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.t j))) x₁ = x₂ ∧
              (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j))) x₁ = 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 X κ
⊢ (P.colimitsCardinalClosure κ).retractClosure X

Tactic:
obtain ⟨j, φ, hφ⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ
    ((P.colimitsCardinalClosure κ).ι.denseAt X) (𝟙 X)

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 κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ : X ⟶ (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι).obj j
hφ : φ ≫ ((Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv).coconeAt X).ι.app j = 𝟙 X
⊢ (P.colimitsCardinalClosure κ).retractClosure 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 = Set.univ

Tactic:
simp [← Set.preimage_union, P.union]

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

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₁ 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 sq₁₂.ι ⟶ Arrow.mk f₃
l : Arrow.LiftStruct α
⊢ (Arrow.mk f₂).hom ≫ adj₂.homEquiv l.l = Arrow.Hom.left ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)

Tactic:
by
        have := l.fac_left
        dsimp at this ⊢
        simp only [← adj₂.homEquiv_naturality_two, ← this,
          sq₁₂.inl_ι_assoc]

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

Goal state before:
pp: case inr.inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) l.castSucc)) (x.cast hd).simplex
⊢ l.castSucc = l.castSucc ∨ l.castSucc = l.succ

Tactic:
exact Or.inl rfl

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

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : j.castSucc < i
⊢ (ConcreteCategory.hom (SimplicialObject.δ Δ[1] j)) (objMk₁ i) = objMk₁ (i.pred ⋯)

Tactic:
ext k : 1
  exact ConcreteCategory.congr_hom (SimplexCategory.δ_comp_toMk₁_of_lt _ _ h) k

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f : RelativeMorphism A B φ
⊢ A ≤ B.preimage f.map

Tactic:
simpa only [← Subcomplex.image_le_iff] using f.image_le

Goal state after:
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
inst✝¹ : CategoryWithHomology C
n d : ℕ
inst✝ : X.HasDimensionLT d
h : d ≤ n
⊢ IsZero (X.homology R n)

Tactic:
rw [← exactAt_iff_isZero_homology]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCoproducts C
inst✝² : Preadditive C
X : SSet
R : C
inst✝¹ : CategoryWithHomology C
n d : ℕ
inst✝ : X.HasDimensionLT d
h : d ≤ n
⊢ ExactAt (X.chainComplex R) n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: case fst
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
⊢ ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  ((ConcreteCategory.hom (δ Δ[n + 1] i.succ))
                    (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] i.succ)) (stdSimplex.objMk₁ j.castSucc.castSucc.succ)).1 =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
          (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
        stdSimplex.objMk₁ j.castSucc.succ).1

Tactic:
simp [SimplexCategory.δ_comp_σ_of_gt hij, SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}]

Goal state after:
case fst
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom (X.map (SimplexCategory.σ j).op)) ((ConcreteCategory.hom (X.map (SimplexCategory.δ i).op)) x) =
    (ConcreteCategory.hom (X.map (SimplexCategory.σ j).op)) ((ConcreteCategory.hom (δ X i)) x)
Module: Mathlib.Order.NonemptyFiniteChains

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : X
ha' : a ∈ s.finset
ha : f a ∈ Finset.image (⇑f) s.finset
b : X
hb' : b ∈ s.finset
hb : f b ∈ Finset.image (⇑f) s.finset
⊢ ⟨f a, ha⟩ ≤ ⟨f b, hb⟩ ∨ ⟨f b, hb⟩ ≤ ⟨f a, ha⟩

Tactic:
obtain h | h := s.comparable ⟨_, ha'⟩ ⟨_, hb'⟩

Goal state after:
case inl
X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : X
ha' : a ∈ s.finset
ha : f a ∈ Finset.image (⇑f) s.finset
b : X
hb' : b ∈ s.finset
hb : f b ∈ Finset.image (⇑f) s.finset
h : ⟨a, ha'⟩ ≤ ⟨b, hb'⟩
⊢ ⟨f a, ha⟩ ≤ ⟨f b, hb⟩ ∨ ⟨f b, hb⟩ ≤ ⟨f a, ha⟩

case inr
X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : X
ha' : a ∈ s.finset
ha : f a ∈ Finset.image (⇑f) s.finset
b : X
hb' : b ∈ s.finset
hb : f b ∈ Finset.image (⇑f) s.finset
h : ⟨b, hb'⟩ ≤ ⟨a, ha'⟩
⊢ ⟨f a, ha⟩ ≤ ⟨f b, hb⟩ ∨ ⟨f b, hb⟩ ≤ ⟨f a, ha⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: case succ
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : i.castSucc.succ < j.succ
⊢ stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x

Tactic:
rw [stdSimplex.δ_comp_σ_of_gt_assoc (by grind), δ_map, comp_const]

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

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
⊢ ⇑m.toTopHomeo ∘ ⇑(ConcreteCategory.hom (SSet.toTop.map (SSet.stdSimplex.map f))) =
    stdSimplex.map ⇑(ConcreteCategory.hom f) ∘ ⇑n.toTopHomeo

Tactic:
by
  ext x : 1
  exact ULift.up_injective (ConcreteCategory.congr_hom ((forget TopCat).congr_map
    (toTopSimplex.hom.naturality f)) x)

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
inst✝¹ : Archimedean S
inst✝ : ExistsAddOfLE S
hv✝ : v.IsNontrivial
h : ∀ (x : R), v x < 1 → w x < 1
a : R
ha₀ : a ≠ 0
hw : w a < 1
x₀ : R
hx₀ : x₀ ≠ 0 ∧ v x₀ < 1
n : ℕ
hv : 1 ≤ v a
⊢ v (x₀ * (a ^ n)⁻¹) < 1

Tactic:
map_mul,

Goal state after:
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
inst✝¹ : Archimedean S
inst✝ : ExistsAddOfLE S
hv✝ : v.IsNontrivial
h : ∀ (x : R), v x < 1 → w x < 1
a : R
ha₀ : a ≠ 0
hw : w a < 1
x₀ : R
hx₀ : x₀ ≠ 0 ∧ v x₀ < 1
n : ℕ
hv : 1 ≤ v a
⊢ v x₀ * v (a ^ n)⁻¹ < 1
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1

Tactic:
have hcⱼ (j : ι) (hj : j ≠ i) : atTop.Tendsto (fun n ↦ v j (c n)) (𝓝 0) := by
    have : 1 < v j a⁻¹ := map_inv₀ (v j) _ ▸
      (one_lt_inv₀ <| (v j).pos fun h ↦ by linarith [map_zero (v _) ▸ h ▸ ha]).2 (haj j hj)
    simpa [c] using (tendsto_div_one_add_pow_nhds_zero this).mul_const _

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
hcⱼ : ∀ (j : ι), j ≠ i → Tendsto (fun n ↦ (v j) (c n)) atTop (𝓝 0)
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : u = w
⊢ (v u) (a u)⁻¹ < 1

Tactic:
simpa [← inv_pow, inv_lt_one_iff₀] using Or.inr (hx u).1

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
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall (f 0) R, ∃ a, f a = y

Tactic:
have hc' : (0 : ℝ) < N⁻¹ - c := by rw [sub_pos]; exact hc

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
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
hc' : 0 < ↑‖↑f'.symm‖₊⁻¹ - ↑c
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall (f 0) R, ∃ a, f a = y
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case top
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
h : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = f x
⊢ ⊤ = 1

Tactic:
refine (hf' ?_).elim

Goal state after:
case top
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
h : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = f x
⊢ deriv f x = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: f : ℂ → ℂ
x : ℂ
h₁ : DifferentiableAt ℂ f x
h₂ : f x ∈ slitPlane
⊢ deriv (log ∘ f) x = logDeriv f x

Tactic:
have A := (HasDerivAt.clog h₁.hasDerivAt h₂).deriv

Goal state after:
f : ℂ → ℂ
x : ℂ
h₁ : DifferentiableAt ℂ f x
h₂ : f x ∈ slitPlane
A : deriv (fun t ↦ log (f t)) x = deriv f x / f x
⊢ deriv (log ∘ f) x = logDeriv f x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: n : ℕ
x : ℂ
hx : x ∈ slitPlane
h_eq : deriv log =ᶠ[𝓝 x] Inv.inv
⊢ iteratedDeriv (n + 1) log x = (-1) ^ n * ↑n.factorial * x ^ (-↑n - 1)

Tactic:
iteratedDeriv_succ',

Goal state after:
n : ℕ
x : ℂ
hx : x ∈ slitPlane
h_eq : deriv log =ᶠ[𝓝 x] Inv.inv
⊢ iteratedDeriv n (deriv log) x = (-1) ^ n * ↑n.factorial * x ^ (-↑n - 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
x : C
⊢ homEquiv ((edgeMk (𝟙 x)).toTruncated.map φ) =
    𝟙 (nerveEquiv ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _proof_11 }))) (nerveEquiv.symm x)))

Tactic:
by
    rw [edgeMk_id, SSet.Edge.toTruncated_id, SSet.Truncated.Edge.map_id]
    exact nerve.homEquiv_id _

Goal state after:
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 : 𝕂
n : ℕ
⊢ ((ordinaryHypergeometricSeries 𝔸 a b c n) fun x ↦ 0) = Pi.single 0 1 n

Tactic:
rw [ordinaryHypergeometricSeries, ofScalars_apply_eq, ordinaryHypergeometricCoefficient]

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n : ℕ
⊢ ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      0 ^ n =
    Pi.single 0 1 n
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
⊢ {u | analyticOrderAt f ↑u = 0 ∨ analyticOrderAt f ↑u = ⊤} ∈ codiscrete ↑U

Tactic:
by
  simp_rw [mem_codiscrete_subtype_iff_mem_codiscreteWithin, mem_codiscreteWithin,
    disjoint_principal_right]
  intro x hx
  rcases (hf x hx).eventually_eq_zero_or_eventually_ne_zero with h₁f | h₁f
  · filter_upwards [eventually_nhdsWithin_of_eventually_nhds h₁f.eventually_nhds] with a ha
    simp [analyticOrderAt_eq_top, ha]
  · filter_upwards [h₁f] with a ha
    simp +contextual [(hf a _).analyticOrderAt_eq_zero, ha]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (n + 1) sin = iteratedDeriv n cos

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]

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:
by
  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.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_9
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y ↦ (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * cexp (↑π * I * r)) x
⊢ (-↑x) ^ r * cexp (↑π * I * r) = (r + 1) * (-↑x) ^ r * cexp (↑π * I * r) / (r + 1)

Tactic:
conv_rhs => rw [mul_assoc, mul_comm, mul_div_cancel_right₀ _ hr]

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

Goal state before:
pp: a : ℂ
this : binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
⊢ HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ a) (binomialSeries ℂ a) 0 1

Tactic:
by
    convert! AnalyticOn.hasFPowerSeriesOnSubball _ _ _
    · norm_num
    · -- TODO: use `fun_prop` for this subgoal
      apply AnalyticOn.cpow (analyticOn_const.add analyticOn_id) analyticOn_const
      intro z hz
      apply Complex.mem_slitPlane_of_norm_lt_one
      rw [← ENNReal.ofReal_one, Metric.eball_ofReal] at hz
      simpa using hz
    · rw [← this]
      exact binomialSeries_radius_ge_one

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: c : ℂ
⊢ (deriv fun x ↦ ↑x ^ c) =O[atTop] fun x ↦ x ^ (c.re - 1)

Tactic:
obtain rfl | hc := eq_or_ne c 0
  · simp_rw [cpow_zero, deriv_const', Asymptotics.isBigO_zero]
  · exact (isTheta_deriv_ofReal_cpow_const_atTop hc).1

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    k.factorial • (choose r x.1 * choose s x.2)

Tactic:
rw [← Nat.choose_mul_factorial_mul_factorial (HasAntidiagonal.antidiagonal.fst_le hx),
    tsub_eq_of_eq_add_rev (List.Nat.mem_antidiagonal.mp hx).symm, mul_assoc, nsmul_eq_mul,
    Nat.cast_mul, Nat.cast_mul, ← mul_assoc _ (x.1.factorial : R), mul_assoc _ (x.2.factorial : R),
    ← mul_assoc (x.2.factorial : R), Nat.cast_commute x.2.factorial,
    mul_assoc _ (x.2.factorial : R), ← nsmul_eq_mul x.2.factorial]

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    ↑(k.choose x.1) * ↑x.1.factorial * (choose r x.1 * x.2.factorial • choose s x.2)