mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a.notMem.refine_1
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
⊢ s.subcomplex ≤ (↑(P.p { s := t, rank_s := ⋯ }.s)).subcomplex

Tactic:
obtain rfl | rfl := ht

Goal state after:
case a.notMem.refine_1.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
t : ↑P.II
hs : (↑t).subcomplex ≤ c.horn.image c.map
⊢ (↑t).subcomplex ≤ (↑(P.p { s := t, rank_s := ⋯ }.s)).subcomplex

case a.notMem.refine_1.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
t : ↑P.II
hs : (↑(P.p t)).subcomplex ≤ c.horn.image c.map
⊢ (↑(P.p t)).subcomplex ≤ (↑(P.p { s := t, rank_s := ⋯ }.s)).subcomplex
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
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
⊢ (↑t).subcomplex ≤ c.horn.image c.map

Tactic:
obtain rfl | rfl := ht

Goal state after:
case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
t : ↑P.II
hs : (↑t).subcomplex ≤ c.horn.image c.map
⊢ (↑t).subcomplex ≤ c.horn.image c.map

case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
t : ↑P.II
hs : (↑(P.p t)).subcomplex ≤ c.horn.image c.map
⊢ (↑t).subcomplex ≤ c.horn.image c.map
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 G : C ⥤ D
e : F ≅ G
inst✝ : F.IsDense
Y : D
⊢ G.isDenseAt Y

Tactic:
rw [← Functor.congr_isDenseAt e]
    exact ⟨F.denseAt Y⟩

Goal state after:
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 κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
⊢ Mono
    (colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
      (E.coconeAt X))

Tactic:
rw [hS₁.isSeparating.mono_iff]

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 κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
⊢ ∀ (G : C),
    P G →
      ∀
        (g₁ g₂ :
          G ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)),
        g₁ ≫
              colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
                (E.coconeAt X) =
            g₂ ≫
              colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
                (E.coconeAt X) →
          g₁ = g₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X✝ : SSet
A : X✝.Subcomplex
P : A.Pairing
inst✝¹ : P.IsRegular
inst✝ : P.IsInner
j : ℕ
hj : ¬IsMax j
X Y : SSet
c : P.rankFunction.Cell j
⊢ SSet.innerAnodyneExtensions (P.rankFunction.basicCell j c)

Tactic:
have h0 := Fin.pos_iff_ne_zero.mpr (IsInner.ne_zero c.s rfl)

Goal state after:
X✝ : SSet
A : X✝.Subcomplex
P : A.Pairing
inst✝¹ : P.IsRegular
inst✝ : P.IsInner
j : ℕ
hj : ¬IsMax j
X Y : SSet
c : P.rankFunction.Cell j
h0 : 0 < ⋯.index ⋯
⊢ SSet.innerAnodyneExtensions (P.rankFunction.basicCell j c)
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 : ℕ
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₂
s₁ : (range (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝¹ : Epi g₁
hg₁ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₁
g₂ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝ : Epi g₂
hg₂ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₂.op)) s₁.simplex = x₂
⊢ ↑((ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) x₁) = (ConcreteCategory.hom (X.map g₂.op)) ↑⟨(f.mapN s₁).simplex, ⋯⟩

Tactic:
simp [mapN, dsimp% h, ← hg₂, dsimp% NatTrans.naturality_apply (f.b j)]

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 : ℕ
hd : x.dim = d
⊢ (x.cast hd).simplex.1 (min x hd) = k.succ

Tactic:
by
  rw [← mem_finset_iff]
  apply Finset.min'_mem

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.ParametrizedLimits

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
J : Type u_4
inst✝¹ : Category.{v_4, u_4} J
P : J ⥤ C₁ᵒᵖ
inst✝ : ∀ (X₂ : C₂), PreservesColimit P.leftOp (F.flip.obj X₂)
X₃ : C₃
c : Cone P
hc : IsLimit c
cocone : (s : Cone (P ⋙ G.flip.obj X₃)) → Cocone (P.leftOp ⋙ F.flip.obj s.pt) :=
  fun s ↦ { pt := X₃, ι := { app := fun j ↦ adj₂.homEquiv.symm (s.π.app (unop j)), naturality := ⋯ } }
⊢ IsLimit ((G.flip.obj X₃).mapCone c)

Tactic:
let hc' (s : Cone (P ⋙ G.flip.obj X₃)) :=
      isColimitOfPreserves (F.flip.obj s.pt) (isColimitCoconeLeftOpOfCone _ hc)

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
J : Type u_4
inst✝¹ : Category.{v_4, u_4} J
P : J ⥤ C₁ᵒᵖ
inst✝ : ∀ (X₂ : C₂), PreservesColimit P.leftOp (F.flip.obj X₂)
X₃ : C₃
c : Cone P
hc : IsLimit c
cocone : (s : Cone (P ⋙ G.flip.obj X₃)) → Cocone (P.leftOp ⋙ F.flip.obj s.pt) :=
  fun s ↦ { pt := X₃, ι := { app := fun j ↦ adj₂.homEquiv.symm (s.π.app (unop j)), naturality := ⋯ } }
hc' : (s : Cone (P ⋙ G.flip.obj X₃)) → IsColimit ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)) :=
  fun s ↦ isColimitOfPreserves (F.flip.obj s.pt) (isColimitCoconeLeftOpOfCone P hc)
⊢ IsLimit ((G.flip.obj X₃).mapCone c)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
y : Fin (d + 1)
hy : y ∈ finset hl.δ ⋯
⊢ l ≤ y

Tactic:
simp only [mem_finset_iff, Monoidal.tensorObj_obj, S.cast_dim,
      S.cast_simplex_rfl, prod_δ_fst, stdSimplex.δ_apply] at hy
    by_contra!
    rw [Fin.succAbove_of_castSucc_lt _ _ (by grind)] at hy
    grind [(hl.succ_le_simplex_fst_iff y.castSucc).1 hy.symm.le]

Goal state after:
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 : j.castSucc < i.succ.castSucc
⊢ stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x

Tactic:
stdSimplex.δ_comp_σ_of_le_assoc (by grind),

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

Goal state before:
pp: case inr
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
⊢ JoinedIn sᶜ a b

Tactic:
have Ia : c - x = a := by
    simp only [c, x]
    module

Goal state after:
case inr
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
⊢ JoinedIn sᶜ a b
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
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
P : (ι : Type ?u.69) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
⊢ ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1

Tactic:
revert hv h

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
this : Fintype ι
P : (ι : Type ?u.69) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
⊢ (∀ (i : ι), (v i).IsNontrivial) →
    (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
⊢ v.IsEquiv w ↔ IsHomeomorph ⇑(WithAbs.congr v w (RingEquiv.refl F))

Tactic:
rw [isHomeomorph_iff_isEmbedding_surjective]
  refine ⟨fun h ↦ ⟨h.isEmbedding_equivWithAbs, RingEquiv.surjective _⟩, fun ⟨hi, _⟩ ↦ ?_⟩
  refine isEquiv_iff_lt_one_iff.2 fun x ↦ ?_
  conv_lhs => rw [← WithAbs.ofAbs_toAbs v x]
  conv_rhs => rw [← WithAbs.ofAbs_toAbs w x]
  rw [← WithAbs.norm_eq_apply_ofAbs, ← WithAbs.norm_eq_apply_ofAbs,
    ← tendsto_pow_atTop_nhds_zero_iff_norm_lt_one, ← tendsto_pow_atTop_nhds_zero_iff_norm_lt_one]
  exact ⟨fun h ↦ by simpa [Function.comp_def] using (hi.continuous.tendsto 0).comp h, fun h ↦ by
    simpa [Function.comp_def] using (hi.continuous_iff (f := (WithAbs.congr v w (.refl F)).symm)).2
      continuous_id |>.tendsto 0 |>.comp h ⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
b c : 𝕂
k : ℕ
⊢ (ordinaryHypergeometricSeries 𝔸 (-↑k) b c).radius = ⊤

Tactic:
by
  refine FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero _ (1 + k) fun n ↦ ?_
  exact ordinaryHypergeometricSeries_eq_zero_of_neg_nat (-(k : 𝕂)) b c (by aesop) (by lia)

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = g x_1
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (fun z ↦ z - x) x
z : 𝕜
hz : z ∈ {x}ᶜ → f z = g z
hn : z ≠ x
⊢ (z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z

Tactic:
· rw [hz (Set.mem_compl_singleton_iff.mp hn), pow_succ', mul_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hg' : ¬analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : ↑n = analyticOrderAt (fun x_1 ↦ g x_1 - g x) x
h : 𝕜 → 𝕜'
han : AnalyticAt 𝕜 h x
hne : h x ≠ 0
heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z
j : 𝕜' → F := fun z ↦ (z - g x) ^ r • f z
hr : AnalyticAt 𝕜' j (g x)
this : AnalyticAt 𝕜 (fun i ↦ (h i)⁻¹ ^ r • j (g i)) x
z : 𝕜
hz : g z - g x = (z - x) ^ n • h z
hzne : h z ≠ 0
⊢ (g z - g x) ^ r • f (g z) = h z ^ r • (z - x) ^ (n * r) • f (g z)

Tactic:
hz,

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hg' : ¬analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : ↑n = analyticOrderAt (fun x_1 ↦ g x_1 - g x) x
h : 𝕜 → 𝕜'
han : AnalyticAt 𝕜 h x
hne : h x ≠ 0
heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z
j : 𝕜' → F := fun z ↦ (z - g x) ^ r • f z
hr : AnalyticAt 𝕜' j (g x)
this : AnalyticAt 𝕜 (fun i ↦ (h i)⁻¹ ^ r • j (g i)) x
z : 𝕜
hz : g z - g x = (z - x) ^ n • h z
hzne : h z ≠ 0
⊢ ((z - x) ^ n • h z) ^ r • f (g z) = h z ^ r • (z - x) ^ (n * r) • f (g z)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
f : 𝕜 → E
inst✝⁵ : MeasurableSpace 𝕜
inst✝⁴ : SecondCountableTopology 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : MeasurableSpace E
inst✝¹ : CompleteSpace E
inst✝ : BorelSpace E
h : Meromorphic f
s : Set 𝕜 := {z | AnalyticAt 𝕜 f z}
h₁ : sᶜ.Countable
h₁' : Countable ↑sᶜ
⊢ Measurable f

Tactic:
have h₂ : IsOpen s := isOpen_analyticAt 𝕜 f

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
f : 𝕜 → E
inst✝⁵ : MeasurableSpace 𝕜
inst✝⁴ : SecondCountableTopology 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : MeasurableSpace E
inst✝¹ : CompleteSpace E
inst✝ : BorelSpace E
h : Meromorphic f
s : Set 𝕜 := {z | AnalyticAt 𝕜 f z}
h₁ : sᶜ.Countable
h₁' : Countable ↑sᶜ
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Measurable f
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • (descPochhammer ℤ n).smeval r =
    (n.choose k * k.factorial) • choose r k * (descPochhammer ℤ (n - k)).smeval (r - ↑k)

Tactic:
mul_nsmul',

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • (descPochhammer ℤ n).smeval r =
    n.choose k • k.factorial • choose r k * (descPochhammer ℤ (n - k)).smeval (r - ↑k)
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case neg
𝕂 : Type u_1
inst✝² : RCLike 𝕂
𝔸 : Type u_2
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ¬∀ (k : ℕ), a ≠ ↑k
⊢ 1 ≤ (binomialSeries 𝔸 a).radius

Tactic:
push Not at ha
    rcases ha with ⟨k, rfl⟩
    simp [binomialSeries_radius_eq_top_of_nat]

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

Goal state before:
pp: case convert_2
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ 1 / (1 - x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ 1 / (1 - x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))

Tactic:
· intro x hx
    have : |x| < 1 := by simpa [enorm_eq_nnnorm] using! hx
    have : 0 ≤ 1 - x := by grind
    simp [-Complex.inv_re, ← Complex.ofReal_one, ← Complex.ofReal_sub, ← Complex.ofReal_cpow this]

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

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
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
n : ℕ
hn : ↑r < 1 / ↑(‖p n‖₊ ^ (1 / ↑n))
⊢ 0 < n → ‖‖p n‖ * ↑r ^ n‖ ≤ 1

Tactic:
hn₀

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
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
n : ℕ
hn : ↑r < 1 / ↑(‖p n‖₊ ^ (1 / ↑n))
hn₀ : 0 < n
⊢ ‖‖p n‖ * ↑r ^ n‖ ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: f : ℝ → ℝ
f' x p : ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivWithinAt (fun y ↦ f y ^ p) (f' * p * f x ^ (p - 1)) Set.univ x

Tactic:
exact hf.rpow_const hx

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
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun a ↦ |k a ^ z * f a|

Tactic:
by
  refine
    ⟨fun h z => Tendsto.isBoundedUnder_le (Tendsto.abs (h z)), fun h =>
      (superpolynomialDecay_iff_abs_tendsto_zero l k f).2 fun z => ?_⟩
  obtain ⟨m, hm⟩ := h (z + 1)
  have h1 : Tendsto (fun _ : α => (0 : β)) l (𝓝 0) := tendsto_const_nhds
  have h2 : Tendsto (fun a : α => |(k a)⁻¹| * m) l (𝓝 0) :=
    zero_mul m ▸
      Tendsto.mul_const m ((tendsto_zero_iff_abs_tendsto_zero _).1 hk.inv_tendsto_atTop)
  refine
    tendsto_of_tendsto_of_tendsto_of_le_of_le' h1 h2 (Eventually.of_forall fun x => abs_nonneg _)
      ((eventually_map.1 hm).mp ?_)
  refine (hk.eventually_ne_atTop 0).mono fun x hk0 hx => ?_
  refine Eq.trans_le ?_ (mul_le_mul_of_nonneg_left hx <| abs_nonneg (k x)⁻¹)
  rw [← abs_mul, ← mul_assoc, pow_succ', ← mul_assoc, inv_mul_cancel₀ hk0, one_mul]

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 μ
ι : Sort u_2
p : ι → Prop
s : ι → Set X
x : X
h : (𝓝 x).HasBasis p s
⊢ (v.filterAt x).HasBasis p fun i ↦ {t | t ∈ v.setsAt x ∧ t ⊆ s i}

Tactic:
simpa only [← Set.ofPred_inter_eq_sep] using! h.smallSets.inf_principal _

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

Goal state before:
pp: case inr
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ (expGrowthInf fun x ↦ b * v x) ≤ expGrowthInf v

Tactic:
apply (expGrowthInf_mul_le _ _).trans_eq <;> rw [expGrowthSup_const b_pos.ne' hb]
    · exact zero_add (expGrowthInf v)
    · exact .inl zero_ne_bot
    · exact .inl zero_ne_top

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

Goal state before:
pp: case inr
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
b_top : b < ∞
⊢ expGrowthInf u ≤ (expGrowthInf fun x ↦ b) + expGrowthInf u

Tactic:
· rw [expGrowthInf_const hb b_top.ne, zero_add]

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

Goal state before:
pp: case inr
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
b_top : b < ∞
⊢ expGrowthSup u ≤ (expGrowthInf fun x ↦ b) + expGrowthSup u

Tactic:
· rw [expGrowthInf_const hb b_top.ne, zero_add]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
c : ι
⊢ c ∈ u → Disjoint (B a) (B c)

Tactic:
hc

Goal state after:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
c : ι
hc : c ∈ u
⊢ Disjoint (B a) (B c)