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)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
H :
  ∀ {k k' : K} (φ : k ⟶ k'),
    ∃ j f,
      (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) (z k')
j : {k k' : K} → (k ⟶ k') → J := fun {k k'} φ ↦ ⋯.choose
g : {k k' : K} → (φ : k ⟶ k') → j₀ ⟶ j φ := fun {k k'} φ ↦ ⋯.choose
hg :
  ∀ {k k' : K} (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map (g φ)))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map (g φ)))) (z k')
⊢ ∃ j₁ α β, ∀ ⦃k k' : K⦄ (φ : k ⟶ k'), α = g φ ≫ β φ

Tactic:
let j'' (f : Arrow K) : J := j f.hom
      let ψ (f : Arrow K) : j₀ ⟶ IsCardinalFiltered.max j'' hK :=
        g f.hom ≫ IsCardinalFiltered.toMax j'' hK f
      refine ⟨IsCardinalFiltered.coeq ψ hK, IsCardinalFiltered.toCoeq ψ hK,
        fun k k' φ ↦ IsCardinalFiltered.toMax j'' hK φ ≫ IsCardinalFiltered.coeqHom ψ hK,
        fun k k' φ ↦ ?_⟩
      simpa [ψ] using! (IsCardinalFiltered.coeq_condition ψ hK (Arrow.mk φ)).symm

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 κ).ι
G : C
hG : P G
this✝ : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
⊢ φ₁ ≫ colimit.ι Φ j = φ₂ ≫ colimit.ι Φ j

Tactic:
let obj : (P.colimitsCardinalClosure κ).FullSubcategory :=
        ⟨coequalizer φ₁ φ₂, by
          apply ObjectProperty.prop_colimit
          rintro (_ | _)
          · exact P.le_colimitsCardinalClosure _ _ hG
          · exact j.left.2⟩

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
hG : P G
this✝ : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
obj : (P.colimitsCardinalClosure κ).FullSubcategory := { obj := coequalizer φ₁ φ₂, property := ⋯ }
⊢ φ₁ ≫ colimit.ι Φ j = φ₂ ≫ colimit.ι Φ j
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : Z ⊗ W ⟶ X
⊢ (α_ A Z W).hom ≫ A ◁ h ≫ A ◁ g ≫ pushout.inr (f ▷ X) (A ◁ g) =
    (α_ A Z W).hom ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g)

Tactic:
← MonoidalCategory.whiskerLeft_comp_assoc

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : Z ⊗ W ⟶ X
⊢ (α_ A Z W).hom ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g) =
    (α_ A Z W).hom ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: X : SSet
⊢ ¬X.Nonempty ↔ X.HasDimensionLT 0

Tactic:
simp only [not_nonempty_iff]
  refine ⟨fun _ ↦ ⟨fun n hn ↦ ?_⟩, fun _ ↦ ⟨fun x ↦ ?_⟩⟩
  · have := Function.isEmpty (X.map (⦋0⦌.const ⦋n⦌ 0).op)
    subsingleton
  · exact (lt_self_iff_false _).1 (X.dim_lt_of_nonDegenerate ⟨x, by simp⟩ 0)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

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
x : X _⦋0⦌
⊢ HomologicalComplex.liftCycles (X.chainComplex R) (X.ιChainComplex x) 0
        liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom._proof_1 ⋯ ≫
      HomologicalComplex.homologyπ (X.chainComplex R) 0 ≫ (X.homology₀Iso R).hom =
    Sigma.ι (fun x ↦ R) (π₀.mk x)

Tactic:
by
  simp [homology₀Iso, HomologicalComplex.homologyπ, SSet.homology,
    HomologicalComplex.liftCycles]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: case succ
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.op.PtSimplex (n + 1) (opObjEquiv.symm x)
⊢ ∂Δ[n + 1].ι ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv f.map)) = const ⟨x, ⋯⟩ ≫ (Subcomplex.ofSimplex x).ι

Tactic:
· refine boundary.hom_ext (fun i ↦ ?_)
          simp [stdSimplex.δ_comp_yonedaEquiv_symm,
            δ_opObjEquiv, ← stdSimplex.yonedaEquiv_δ_comp,
            opObjEquiv_yonedaEquiv_const]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ stdSimplex.δ j.succ.succ ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv h.map)) = g.op.map

Tactic:
rw [stdSimplex.δ_comp_yonedaEquiv_symm, op_δ, Equiv.apply_symm_apply,
      ← stdSimplex.yonedaEquiv_δ_comp, opEquiv_symm_apply_map, ← h.δ_castSucc_castSucc_map,
      Fin.rev_succ, Fin.rev_succ, ← hij, Fin.rev_rev]

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

Goal state before:
pp: ⊢ stdSimplexHomeomorphUnitInterval (⦋1⦌.toTopHomeo ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 0))) default)) = 1

Tactic:
rw [← stdSimplexHomeomorphUnitInterval_one]

Goal state after:
⊢ stdSimplexHomeomorphUnitInterval (⦋1⦌.toTopHomeo ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 0))) default)) =
    stdSimplexHomeomorphUnitInterval ⟨Pi.single 1 1, ⋯⟩
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: case inl
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : a < ℵ₀
⊢ #↑t ≤ a

Tactic:
obtain ⟨n, rfl⟩ : ∃ (n : ℕ), a = n := lt_aleph0.1 ha
    apply mk_le_iff_forall_finset_subset_card_le.2 (fun s hs ↦ ?_)
    have A : ∀ x ∈ s, ∀ᶠ i in l, x ∈ f i := fun x hx ↦ ht x (hs hx)
    have B : ∀ᶠ i in l, ∀ x ∈ s, x ∈ f i := (s.eventually_all).2 A
    rcases B.exists with ⟨i, hi⟩
    have : ∀ i, Fintype (f i) := fun i ↦ (lt_aleph0_iff_fintype.1 ((h'f i).trans_lt ha)).some
    let u : Finset α := (f i).toFinset
    have I1 : s.card ≤ u.card := by
      have : s ⊆ u := fun x hx ↦ by simpa only [u, Set.mem_toFinset] using hi x hx
      exact Finset.card_le_card this
    have I2 : (u.card : Cardinal) ≤ n := by
      convert! h'f i; simp only [u, Set.toFinset_card, mk_fintype]
    exact I1.trans (Nat.cast_le.1 I2)

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

Tactic:
obtain ⟨ε, hε, hU⟩ := hU

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : U ∈ 𝓝 0
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / ↑i.factorial) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      z ^ n •
        (fun z ↦
            if z ∈ U then F z
            else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0))
          z

Tactic:
by_cases hz : z ∈ U

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : U ∈ 𝓝 0
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / ↑i.factorial) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
hz : z ∈ U
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      z ^ n •
        (fun z ↦
            if z ∈ U then F z
            else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0))
          z

case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : U ∈ 𝓝 0
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / ↑i.factorial) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
hz : z ∉ U
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      z ^ n •
        (fun z ↦
            if z ∈ U then F z
            else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0))
          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
x : 𝕜
f g : 𝕜 → E
hg : MeromorphicAt g x
⊢ MeromorphicAt (f + g) x ↔ MeromorphicAt f x

Tactic:
rw [add_comm]
  exact meromorphicAt_add_iff_meromorphicAt₁ hg

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ multichoose (r + 1) (k + 1) = multichoose r (k + 1) + multichoose (r + 1) k

Tactic:
by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1))]
  simp only [factorial_nsmul_multichoose_eq_ascPochhammer, smul_add]
  rw [add_comm (smeval (ascPochhammer ℕ (k + 1)) r), ascPochhammer_succ_succ r k]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case neg
R : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
hk : ¬k = 0
⊢ choose 0 k = 0

Tactic:
rw [choose_zero_pos R <| Nat.pos_of_ne_zero hk]

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

Goal state before:
pp: case convert_7
a : ℂ
this : binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
z : ℂ
hz : z ∈ Metric.eball 0 1
⊢ ((fun x ↦ 1) + fun x ↦ x) z ∈ slitPlane

Tactic:
apply Complex.mem_slitPlane_of_norm_lt_one

Goal state after:
case convert_7
a : ℂ
this : binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
z : ℂ
hz : z ∈ Metric.eball 0 1
⊢ ‖(fun x ↦ x) z‖ < 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

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

Tactic:
· exact (isTheta_deriv_ofReal_cpow_const_atTop hc).1

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
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  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
z : ℂ
hz : z ∈ B
⊢ 1 + z ∈ slitPlane

Tactic:
apply Complex.mem_slitPlane_of_norm_lt_one

Goal state after:
case succ
a : ℂ
B : Set ℂ := ⋯
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  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
z : ℂ
hz : z ∈ B
⊢ ‖z‖ < 1
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
k : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 k f s) (p.iteratedFDerivSeries k) s x r

Tactic:
induction k with
  | zero =>
    exact (continuousMultilinearCurryFin0 𝕜 E F).symm
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall h
  | succ k ih =>
    rw [iteratedFDerivWithin_succ_eq_comp_left]
    apply (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (k + 1) ↦ E) F).symm
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall
        (ih.fderivWithin_of_mem_of_analyticOn (h'.iteratedFDerivWithin hs _) hs hx)

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

Goal state before:
pp: case convert_2
a : ℕ
z : ℂ
hz : z ≠ 0
this✝ :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)) ((z⁻¹ • 1) 0) 1
H : 1 / ‖z⁻¹ • 1‖ₑ = ‖z‖ₑ
this :
  HasFPowerSeriesOnBall (fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹)
    ((FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)).compContinuousLinearMap (z⁻¹ • 1)) 0 ‖z‖ₑ
w : ℂ
hw : w ∈ Metric.eball 0 ‖z‖ₑ
⊢ ((z ^ (a + 1))⁻¹ • fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹) w = (fun x ↦ 1 / (z - x) ^ (a + 1)) w

Tactic:
simp [← mul_inv_rev, ← mul_pow, sub_mul, mul_right_comm _ w, hz]

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (z - x) ^ 2)
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (z ^ (n + 2))⁻¹ * (↑n + 1)) 0 ‖z‖ₑ

Tactic:
by
  simpa [add_comm 1] using one_div_sub_pow_hasFPowerSeriesOnBall_zero 1 hz

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

Goal state before:
pp: c : ℂ
t : ℝ
ht : 0 < t
⊢ deriv (fun x ↦ x ^ c.re) t = c.re * t ^ (c.re - 1)

Tactic:
rw [Real.deriv_rpow_const t]

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

Goal state before:
pp: u : ℕ → EReal
⊢ linearGrowthInf (-u) = liminf (-fun n ↦ u n / ↑n) atTop

Tactic:
refine liminf_congr (Eventually.of_forall fun n ↦ ?_)

Goal state after:
u : ℕ → EReal
n : ℕ
⊢ (-u) n / ↑n = (-fun n ↦ u n / ↑n) n
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
⊢ liminf (fun n ↦ (u ⊓ v) n / ↑n) atTop = liminf (fun a ↦ min (u a / ↑a) (v a / ↑a)) atTop

Tactic:
refine liminf_congr (Eventually.of_forall fun n ↦ ?_)

Goal state after:
u v : ℕ → EReal
n : ℕ
⊢ (u ⊓ v) n / ↑n = min (u n / ↑n) (v n / ↑n)
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → EReal
⊢ linearGrowthInf (⨅ i, u i) = ⨅ i, linearGrowthInf (u i)

Tactic:
rw [← iInf_univ, linearGrowthInf_biInf u Set.finite_univ, iInf_univ]

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
⊢ expGrowthInf u⁻¹ = liminf (-fun n ↦ (u n).log / ↑n) atTop

Tactic:
refine liminf_congr (Eventually.of_forall fun n ↦ ?_)

Goal state after:
u : ℕ → ℝ≥0∞
n : ℕ
⊢ (u⁻¹ n).log / ↑n = (-fun n ↦ (u n).log / ↑n) 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
⊢ Measurable f'

Tactic:
fun_prop (disch := simp_all)

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

Goal state before:
pp: u v : ℕ → ℝ≥0∞
⊢ liminf (fun n ↦ ((u ⊓ v) n).log / ↑n) atTop = liminf (fun a ↦ min ((u a).log / ↑a) ((v a).log / ↑a)) atTop

Tactic:
refine liminf_congr (Eventually.of_forall fun n ↦ ?_)

Goal state after:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((u ⊓ v) n).log / ↑n = min ((u n).log / ↑n) ((v n).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 α := ⋯
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := ⋯
f'_meas : Measurable f'
t : Set α := ⋯
μt : μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
x : α
hx : x ∉ t
⊢ ∀ (w : β), f x < w → ∃ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x < w

Tactic:
intro q hq
      obtain ⟨r, ⟨xr, rq⟩, rs⟩ : ∃ r, r ∈ Ioo (f x) q ∩ s :=
        dense_iff_inter_open.1 s_dense (Ioo (f x) q) isOpen_Ioo (nonempty_Ioo.2 hq)
      refine ⟨⟨r, rs⟩, ?_⟩
      have A : x ∈ u' r := mem_biInter fun i _ => (huv r i).2.2.1 xr
      simp only [A, rq, piecewise_eq_of_mem]

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

Goal state before:
pp: case refine_3
α : 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 : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
⊢ ∀ a ∈ t, ∀ b ∈ insert a' u, (B a ∩ B b).Nonempty → ∃ c ∈ insert a' u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c

Tactic:
· -- check that every element `c` of `t` intersecting `u ∪ {a'}` intersects an element of this
    -- family with large `δ`.
    intro c ct b ba'u hcb
    -- if `c` already intersects an element of `u`, then it intersects an element of `u` with
    -- large `δ` by the assumption on `u`, and there is nothing left to do.
    by_cases! H : ∃ d ∈ u, (B c ∩ B d).Nonempty
    · rcases H with ⟨d, du, hd⟩
      rcases hu.prop.2.2 c ct d du hd with ⟨d', d'u, hd'⟩
      exact ⟨d', mem_insert_of_mem _ d'u, hd'⟩
    · -- Otherwise, `c` belongs to `A`. The element of `u ∪ {a'}` that it intersects has to be `a'`.
      -- Moreover, `δ c` is smaller than the maximum `m` of `δ` over `A`, which is `≤ δ a' / τ`
      -- thanks to the good choice of `a'`. This is the desired inequality.
      simp only [← disjoint_iff_inter_eq_empty] at H
      rcases mem_insert_iff.1 ba'u with (rfl | H')
      · refine ⟨b, mem_insert _ _, hcb, ?_⟩
        calc
          δ c ≤ m := le_csSup bddA (mem_image_of_mem _ ⟨ct, H⟩)
          _ = τ * (m / τ) := by field
          _ ≤ τ * δ b := by gcongr
      · rw [← not_disjoint_iff_nonempty_inter] at hcb
        exact (hcb (H _ H')).elim

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)
⊢ (linearGrowthSup fun n ↦ u (m * n)) = ↑m * linearGrowthSup u

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

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)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
n m : ℕ
⊢ MeasurableSet (⨅ a ∈ Finset.Ico n (m + 1), e a)

Tactic:
exact MeasurableSet.biInter (to_countable _) fun i _ => he₁ _

Goal state after: