mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

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

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

Tactic:
· exact isIso_of_isInitial hX₂ hY₂ _

Goal state after:
case sq
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj X₂)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj Y₂)
h : IsInitial X₁
hX₂ : IsInitial ((F.flip.obj X₂).obj X₁) := ⋯
hY₂ : IsInitial ((F.flip.obj Y₂).obj X₁) := ⋯
⊢ CommSq ((F.map f₁).app X₂) ((F.obj X₁).map f₂) (𝟙 ((F.obj Y₁).obj X₂))
    ((IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h).to ((F.obj Y₁).obj X₂))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
k : Fin (n + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n] 0)) (stdSimplex.objEquiv.symm (SimplexCategory.σ 0)))).op))
            x,
          (ConcreteCategory.hom (δ Δ[1] 0)) (stdSimplex.objMk₁ 1)).2
      k =
    ((ConcreteCategory.hom (ι₁.app (op ⦋n⦌))) x).2 k

Tactic:
stdSimplex.δ_objMk₁_of_lt _ _ (by tauto)

Goal state after:
case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
k : Fin (n + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n] 0)) (stdSimplex.objEquiv.symm (SimplexCategory.σ 0)))).op))
            x,
          stdSimplex.objMk₁ (Fin.pred 1 ⋯)).2
      k =
    ((ConcreteCategory.hom (ι₁.app (op ⦋n⦌))) x).2 k
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

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

pp: case snd.h
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ i.castSucc.castSucc < j.castSucc.succ.succ

Tactic:
Fin.pred_succ

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

case snd.h
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ i.castSucc.castSucc < j.castSucc.succ.succ
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
n : ℕ
s : Type₁ k.succ n
h : (pairingCore k.succ n).index s = 0
this✝ : s.index = 0
hs : IsIndex s.x ⋯ (Fin.succ 0)
i : Fin ((s.x.cast ⋯).dim + 1)
hi : (s.x.cast ⋯).simplex.1 i = 0
this : (fun j ↦ (s.x.cast ⋯).simplex.1 j) 0 ≤ (fun j ↦ (s.x.cast ⋯).simplex.1 j) i
h₁ : (s.x.cast ⋯).simplex.1 0 = k.succ.castSucc
⊢ False

Tactic:
simp [h₁, hi] at this

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

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₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝ : Arrow C₃
⊢ Arrow.Hom.right
      ({
              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
          ((G.leibnizPullback.obj (op X₁)).obj x✝) ≫
        (G.leibnizPullback.obj (op X₁)).map
          ({
                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
            x✝)) =
    Arrow.Hom.right (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝))

Tactic:
apply pullback.hom_ext <;> simp [← homEquiv_naturality_three]

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

Goal state before:
pp: ⊢ stdSimplex.δ 0 ≫ toSSetObjI = SSet.const (TopCat.toSSetObj₀Equiv.symm 1)

Tactic:
dsimp only [toSSetObjI, toTopObjIsoI, TopCat.stdSimplexHomeomorphI]
  rw [← Adjunction.homEquiv_naturality_left, sSetTopAdj_homEquiv_stdSimplex_zero]
  congr 2
  have : stdSimplexHomeomorphUnitInterval (⦋1⦌.toTopHomeo
      (((toTop.{u}.map (stdSimplex.δ 0)).hom) default)) = 1 := by
    rw [← stdSimplexHomeomorphUnitInterval_one]
    congr 1
    refine (SimplexCategory.toTopHomeo_naturality_apply _ _).trans ?_
    rw [Subsingleton.elim (⦋0⦌.toTopHomeo default) (stdSimplex.vertex 0), stdSimplex.map_vertex]
    rfl
  exact congr_arg ULift.up.{u} this

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: case e'_3
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := (f i).toFinset
I1 : s.card ≤ u.card
⊢ ↑u.card = #↑(f i)

Tactic:
simp only [u, Set.toFinset_card, mk_fintype]

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
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
h_lt : log (v b) / log (w b) < log (v a) / log (w a)
hwa : 1 < w a
hwb : 1 < w b
⊢ False

Tactic:
div_lt_div_iff₀ (log_pos hwb) (log_pos hwa),

Goal state after:
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
h_lt : log (v b) * log (w a) < log (v a) * log (w b)
hwa : 1 < w a
hwb : 1 < w b
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case refine_1
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ (ComposableArrows.mk₁ (nerve.homEquiv (f.map φ))).left =
    ComposableArrows.left ((ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge)

pp: case refine_2
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ (ComposableArrows.mk₁ (nerve.homEquiv (f.map φ))).right =
    ComposableArrows.right ((ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge)

Tactic:
· dsimp [nerveEquiv, ComposableArrows.right]
        simp only [← f.src_eq, NatTrans.naturality_apply]
        rfl

Goal state after:
case refine_2
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ (ComposableArrows.mk₁ (nerve.homEquiv (f.map φ))).right =
    ComposableArrows.right ((ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: ⊢ HasFPowerSeriesAt Real.log (FormalMultilinearSeries.ofScalars ℝ fun n ↦ -(-1) ^ n / ↑n) 1

Tactic:
obtain ⟨r, hp⟩ := hasFPowerSeriesAt_clog_one

Goal state after:
r : ENNReal
hp : HasFPowerSeriesOnBall log (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) 1 r
⊢ HasFPowerSeriesAt Real.log (FormalMultilinearSeries.ofScalars ℝ fun n ↦ -(-1) ^ n / ↑n) 1
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

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

Tactic:
ofScalars_apply_eq'

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
x : 𝔸
⊢ (fun n ↦ ordinaryHypergeometricCoefficient a b c n • x ^ n) = fun n ↦
    ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case succ.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
n : ℕ
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
IH : analyticOrderAt (deriv f) z₀ = ↑n ↔ (∀ k < n, iteratedDeriv (k + 1) f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0
ho : analyticOrderAt f z₀ = ↑(n + 1)
⊢ (∀ k < n + 1, iteratedDeriv k f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0

pp: case succ.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
n : ℕ
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
IH : analyticOrderAt (deriv f) z₀ = ↑n ↔ (∀ k < n, iteratedDeriv (k + 1) f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0
x✝ : (∀ k < n + 1, iteratedDeriv k f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0
hz : ∀ k < n + 1, iteratedDeriv k f z₀ = 0
hnz : iteratedDeriv (n + 1) f z₀ ≠ 0
⊢ analyticOrderAt f z₀ = ↑(n + 1)

Tactic:
· have ⟨h_zero, h_nz⟩ := IH.mp (analyticOrderAt_deriv_of_pos hf ho)
      refine ⟨fun k hk ↦ ?_, h_nz⟩
      match k with
      | 0 => rw [iteratedDeriv_zero, ← hf.analyticOrderAt_ne_zero, ho, Nat.cast_add_one]
             exact Nat.cast_add_one_ne_zero _
      | k + 1 => exact h_zero k (by lia)

Goal state after:
case succ.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
n : ℕ
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
IH : analyticOrderAt (deriv f) z₀ = ↑n ↔ (∀ k < n, iteratedDeriv (k + 1) f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0
x✝ : (∀ k < n + 1, iteratedDeriv k f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0
hz : ∀ k < n + 1, iteratedDeriv k f z₀ = 0
hnz : iteratedDeriv (n + 1) f z₀ ≠ 0
⊢ analyticOrderAt f z₀ = ↑(n + 1)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_4
inst✝⁴ : NormedRing R
inst✝³ : Module R E
inst✝² : IsBoundedSMul R E
x : 𝕜
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : IsScalarTower 𝕜 R E
f : 𝕜 → R
g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x
⊢ MeromorphicAt (f • g) x

Tactic:
refine ⟨m + n, ?_⟩

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_4
inst✝⁴ : NormedRing R
inst✝³ : Module R E
inst✝² : IsBoundedSMul R E
x : 𝕜
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : IsScalarTower 𝕜 R E
f : 𝕜 → R
g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x
⊢ AnalyticAt 𝕜 (fun z ↦ (z - x) ^ (m + n) • (f • g) z) x
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
⊢ MeromorphicAt f x ↔ ∃ n g, AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
by
  refine ⟨fun ⟨n, hn⟩ ↦ ⟨-n, _, ⟨hn, eventually_nhdsWithin_iff.mpr ?_⟩⟩, ?_⟩
  · filter_upwards with z hz
    match_scalars
    simp [sub_ne_zero.mpr hz]
  · refine fun ⟨n, g, hg_an, hg_eq⟩ ↦ MeromorphicAt.congr ?_ (EventuallyEq.symm hg_eq)
    exact (((MeromorphicAt.id x).sub (.const _ x)).zpow _).smul hg_an.meromorphicAt

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun x ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
⊢ Tendsto (fun x ↦ toSpanSingleton ℝ (deriv f x)) (𝓝[t] a) (𝓝 (smulRight 1 e))

Tactic:
exact Tendsto.comp
      (isBoundedBilinearMap_smulRight : IsBoundedBilinearMap ℝ _).continuous_right.continuousAt
      (tendsto_nhdsWithin_mono_left Ioo_subset_Iio_self f_lim')

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

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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
⊢ s ∩ Metric.eball x r = s

Tactic:
exact Set.inter_eq_left.2 h's

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

Goal state before:
pp: case h₀
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z ↦ (p n) fun x_1 ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := fun k ↦ if h : n = k then h ▸ p n else 0
y : E
hy : y ∈ Metric.eball 0 r
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ n → ((q b) fun x ↦ y) = 0

Tactic:
· intro i hi h'i
        simp [q, h'i.symm]

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
x : ℝ
hx : x ∈ Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ)
this : |x| < 1
⊢ (⇑Complex.reCLM ∘ (fun x ↦ 1 / (1 - x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) x = (fun x ↦ 1 / (1 - x) ^ a) x

Tactic:
have : 0 ≤ 1 - x := by grind

Goal state after:
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
x : ℝ
hx : x ∈ Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ)
this✝ : |x| < 1
this : 0 ≤ 1 - x
⊢ (⇑Complex.reCLM ∘ (fun x ↦ 1 / (1 - x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) x = (fun x ↦ 1 / (1 - x) ^ a) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: f g : ℝ → ℝ
f' g' x : ℝ
hf : HasDerivAt f f' x
hg : HasDerivAt g g' x
h : 0 < f x
⊢ HasDerivAt (fun x ↦ f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x

Tactic:
rw [← hasDerivWithinAt_univ] at *
  exact hf.rpow hg h

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 μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst✝ : SecondCountableTopology X
ρ : Measure X
hρ : ρ ≪ μ
⊢ ρ (s \ ⋃ p ∈ h.index, h.covering p) + ρ (⋃ p ∈ h.index, h.covering p) = ∑' (p : ↑h.index), ρ (h.covering ↑p)

Tactic:
rw [hρ h.measure_sdiff_biUnion, zero_add,
        measure_biUnion h.index_countable h.covering_disjoint fun x hx => h.measurableSet_u hx]

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)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun x ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
⊢ ∃ t ∈ g x, t ⊆ closedBall x ε

Tactic:
rcases fset x hx tf with (h't | h't)

Goal state after:
case inl
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun x ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
h't : t ∈ v.setsAt x
⊢ ∃ t ∈ g x, t ⊆ closedBall x ε

case inr
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun x ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
h't : t ∈ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
⊢ ∃ t ∈ g x, t ⊆ closedBall x ε
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: b : ℝ≥0∞
n : ℕ
n_1 : 1 ≤ n
⊢ (b ^ n).log / ↑n = b.log

Tactic:
EReal.div_eq_iff (natCast_ne_bot n) (natCast_ne_top n)
    (zero_lt_one.trans_le (Nat.one_le_cast.2 n_1)).ne.symm,

Goal state after:
b : ℝ≥0∞
n : ℕ
n_1 : 1 ≤ n
⊢ (b ^ n).log = b.log * ↑n
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
⊢ μ t ≤ ∑' (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), μ (u' ↑p ∩ v ↑p ↑q)

Tactic:
by
        refine (measure_iUnion_le _).trans ?_
        refine ENNReal.tsum_le_tsum fun p => ?_
        have := (s_count.mono (s.inter_subset_left (t := Ioi ↑p))).to_subtype
        apply measure_iUnion_le

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

Goal state before:
pp: u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
this : Tendsto (fun n ↦ ↑(m * n) / ↑n) atTop (𝓝 ↑m)
⊢ (linearGrowthInf fun n ↦ u (m * n)) = ↑m * linearGrowthInf u

Tactic:
exact h.linearGrowthInf_comp this (Nat.cast_ne_zero.2 hm) (natCast_ne_top m)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hs₀ : s =ᵐ[μ] ∅
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]

Tactic:
restrict_congr_set (hs₀.union EventuallyEq.rfl),

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hs₀ : s =ᵐ[μ] ∅
⊢ ⨍⁻ (x : α) in ∅ ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]