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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : LocallySmall.{w, v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
inst✝² : HasLimitsOfShape Kᵒᵖ (Type w)
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
e : C ≌ ShrinkHoms.{u} C := ShrinkHoms.equivalence C
this : ∀ (k : K), IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ
⊢ IsCardinalPresentable c.pt κ

Tactic:
rw [← isCardinalPresentable_iff_of_isEquivalence c.pt κ e.functor]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : LocallySmall.{w, v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
inst✝² : HasLimitsOfShape Kᵒᵖ (Type w)
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
e : C ≌ ShrinkHoms.{u} C := ShrinkHoms.equivalence C
this : ∀ (k : K), IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ
⊢ IsCardinalPresentable (e.functor.obj c.pt) κ
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : LocallySmall.{w, v, u} C
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : EssentiallySmall.{w, v', u'} J
F : J ⥤ C
inst✝³ : F.IsDense
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : ∀ (j : J), IsCardinalPresentable (F.obj j) κ
inst✝ : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
X : C
⊢ ∃ J_1 x, ∃ (_ : IsCardinalFiltered J_1 κ), (⊤.map F).colimitsOfShape J_1 X

Tactic:
have ip := F.denseAt X
    let e := equivSmallModel.{w} (CostructuredArrow F X)
    exact ⟨SmallModel.{w} (CostructuredArrow F X), inferInstance,
      IsCardinalFiltered.of_equivalence κ e,
      ⟨{  diag := _
          ι := _
          isColimit := (F.denseAt X).whiskerEquivalence e.symm
          prop_diag_obj j := ⟨_, by simp, ⟨Iso.refl _⟩⟩ }⟩⟩

Goal state after:
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 : ℕ
⊢ IsColimit
    (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.mapCocone (PushoutCocone.mk (homOfLE ⋯) (f.b j) ⋯))

Tactic:
refine (isColimitMapCoconePushoutCoconeEquiv _ _).symm
      (IsPushout.isColimit ?_)
    refine Types.isPushout_of_isPullback_of_mono'
      ((f.isPullback j).map ((CategoryTheory.evaluation _ _).obj _))
      (f.range_homOfLE_app_union_range_b_app _ _) (fun x₁ x₂ hx₁ hx₂ h ↦ ?_)
    obtain ⟨s₁, g₁, _, hg₁⟩ := (Subcomplex.range (f.m j)).existsN x₁ hx₁
    obtain ⟨s₂, g₂, _, hg₂⟩ := (Subcomplex.range (f.m j)).existsN x₂ hx₂
    obtain rfl : s₁ = s₂ := f.isPushout_aux₃ (by
      dsimp
      rw [S.eq_iff_ofSimplex_eq, ← Subcomplex.ofSimplex_map_of_epi g₁,
        ← Subcomplex.ofSimplex_map_of_epi g₂]
      · simp [← dsimp% (f.b j).naturality_apply, hg₁, hg₂, dsimp% h]
      all_goals
      · rw [Subcomplex.mem_nonDegenerate_iff]
        apply f.isPushout_aux₁)
    obtain rfl := X.unique_nonDegenerate_map (x := (((f.b _)).app _ x₁).val)
      g₁ ⟨_, f.isPushout_aux₁ s₁⟩
        (by simp [mapN, ← hg₁, dsimp% NatTrans.naturality_apply (f.b j)])
      g₂ ⟨_, f.isPushout_aux₁ s₁⟩
        (by simp [mapN, dsimp% h, ← hg₂, dsimp% NatTrans.naturality_apply (f.b j)])
    rw [← hg₁, hg₂]

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 + 1
l : Fin (d + 1)
isIndex : IsIndex x hd l.succ
hs :
  min { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x ⋯ =
    { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.index.succ
l' : Fin (d + 1)
hd' : { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x.dim = d + 1
isIndex' : IsIndex { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x hd' l'.succ
ht :
  min
      { x := { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x, d := d, hd := hd', index := l',
          isIndex := isIndex' }.x
      ⋯ =
    { x := { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x, d := d, hd := hd', index := l',
          isIndex := isIndex' }.index.succ
⊢ { x := x, d := d, hd := hd, index := l, isIndex := isIndex } =
    { x := { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x, d := d, hd := hd', index := l',
      isIndex := isIndex' }

Tactic:
obtain rfl : l = l' := by grind

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
isIndex : IsIndex x hd l.succ
hs :
  min { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x ⋯ =
    { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.index.succ
hd' : { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x.dim = d + 1
isIndex' : IsIndex { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x hd' l.succ
ht :
  min
      { x := { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x, d := d, hd := hd', index := l,
          isIndex := isIndex' }.x
      ⋯ =
    { x := { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x, d := d, hd := hd', index := l,
          isIndex := isIndex' }.index.succ
⊢ { x := x, d := d, hd := hd, index := l, isIndex := isIndex } =
    { x := { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x, d := d, hd := hd', index := l,
      isIndex := isIndex' }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inl.inr.refine_3
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
h₁ : (x.cast hd).simplex.1 i.castSucc = k.castSucc
h₂ : (x.cast hd).simplex.2 i.castSucc = (x.cast hd).simplex.2 (min x hd)
this : φ x hd (min x hd).succ = (objEquiv (x.cast hd).simplex) (min x hd)
⊢ (x.cast hd).simplex.1 i.succ = ((objEquiv (x.cast hd).simplex) (min x hd)).1

Tactic:
hi

Goal state after:
case inl.inr.refine_3
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
h₁ : (x.cast hd).simplex.1 i.castSucc = k.castSucc
h₂ : (x.cast hd).simplex.2 i.castSucc = (x.cast hd).simplex.2 (min x hd)
this : φ x hd (min x hd).succ = (objEquiv (x.cast hd).simplex) (min x hd)
⊢ (x.cast hd).simplex.1 (min x hd) = ((objEquiv (x.cast hd).simplex) (min x hd)).1
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X : SSet
motive : X.π₀ → Prop
mk : ∀ (x : X _⦋0⦌), motive (π₀.mk x)
x : X.π₀
⊢ motive x

Tactic:
obtain ⟨x, rfl⟩ := x.mk_surjective

Goal state after:
X : SSet
motive : X.π₀ → Prop
mk : ∀ (x : X _⦋0⦌), motive (π₀.mk x)
x : X _⦋0⦌
⊢ motive (π₀.mk x)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

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₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq : G.PullbackObjObj f₁ f₃
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj X₃)
inst✝ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj Y₃)
h : IsInitial X₁
hX₃ : IsTerminal ((G.flip.obj X₃).obj (op X₁)) := IsTerminal.isTerminalObj (G.flip.obj X₃) (op X₁) (IsInitial.op C₁ h)
⊢ IsPullback ((IsTerminal.isTerminalObj (G.flip.obj X₃) (op X₁) (IsInitial.op C₁ h)).from ((G.obj (op Y₁)).obj Y₃))
    (𝟙 ((G.obj (op Y₁)).obj Y₃)) ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)

Tactic:
let hY₃ := IsTerminal.isTerminalObj (G.flip.obj Y₃) _ h.op

Goal state after:
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 : G.PullbackObjObj f₁ f₃
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj X₃)
inst✝ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj Y₃)
h : IsInitial X₁
hX₃ : IsTerminal ((G.flip.obj X₃).obj (op X₁)) := IsTerminal.isTerminalObj (G.flip.obj X₃) (op X₁) (IsInitial.op C₁ h)
hY₃ : IsTerminal ((G.flip.obj Y₃).obj (op X₁)) := IsTerminal.isTerminalObj (G.flip.obj Y₃) (op X₁) (IsInitial.op C₁ h)
⊢ IsPullback ((IsTerminal.isTerminalObj (G.flip.obj X₃) (op X₁) (IsInitial.op C₁ h)).from ((G.obj (op Y₁)).obj Y₃))
    (𝟙 ((G.obj (op Y₁)).obj Y₃)) ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.degenerate (n + 1)
⊢ X.ιChainComplex x ≫ PInfty.f (n + 1) = 0

Tactic:
simp only [degenerate_eq_iUnion_range_σ, Set.mem_iUnion, Set.mem_range] at hx
    let X' := ((SimplicialObject.whiskering _ _).obj (sigmaConst.obj R)).obj X
    obtain ⟨i, y, rfl⟩ := hx
    trans X.ιChainComplex y ≫ X'.σ i ≫ (PInfty (X := X')).f _
    · simp [ιChainComplex, X']
    · simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SingularHomology.HomologyZero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
X : TopCat
R : C
⊢ ((X.singularHomology₀Iso R).hom ≫ Sigma.desc fun x ↦ 𝟙 R) = X.singularHomology₀ε R

Tactic:
dsimp only [singularHomology₀Iso, singularHomology₀ε, SSet.homology₀ε]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
X : TopCat
R : C
⊢ (((toSSet.obj X).homology₀Iso R ≪≫ (sigmaConst.obj R).mapIso zerothHomotopyEquiv.toIso.symm).hom ≫
      Sigma.desc fun x ↦ 𝟙 R) =
    ((toSSet.obj X).homology₀Iso R).hom ≫ Sigma.desc fun x ↦ 𝟙 R
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : PartialOrder S
v w : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : Nontrivial R
h : v.IsEquiv w
x : R
⊢ 1 ≤ v x ↔ 1 ≤ w x

Tactic:
simpa only [map_one] using h 1 x

Goal state after:
Module: Mathlib.Analysis.Complex.OperatorNorm

Goal state before:
pp: ⊢ ‖reCLM‖ₑ = 1

Tactic:
simp [← ofReal_norm]

Goal state after:
Module: Mathlib.Analysis.Complex.OperatorNorm

Goal state before:
pp: ⊢ ‖imCLM‖ₑ = 1

Tactic:
simp [← ofReal_norm]

Goal state after:
Module: Mathlib.Analysis.Complex.OperatorNorm

Goal state before:
pp: ⊢ ‖↑conjCLE‖ₑ = 1

Tactic:
simp [← ofReal_norm]

Goal state after:
Module: Mathlib.Analysis.Complex.OperatorNorm

Goal state before:
pp: ⊢ ‖ofRealCLM‖ₑ = 1

Tactic:
simp [← ofReal_norm]

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: case inr
𝕜 : 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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
⊢ y ∈ f '' closedBall b ε

Tactic:
have A : ∀ z, dist (g z) z ≤ f'symm.nnnorm * dist (f z) y := by
    intro z
    rw [dist_eq_norm, hg, add_sub_cancel_left, dist_eq_norm']
    exact f'symm.bound _

Goal state after:
case inr
𝕜 : 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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
⊢ y ∈ f '' closedBall b ε
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

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

Tactic:
refine IsInducing.isEmbedding <| isInducing_iff_nhds_zero.2 <| Filter.ext fun U ↦
    ⟨fun hU ↦ ?_, fun hU ↦ ?_⟩

Goal state after:
case refine_1
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : U ∈ 𝓝 0
⊢ U ∈ Filter.comap (⇑(WithAbs.congr v w (RingEquiv.refl F))) (𝓝 0)

case refine_2
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : U ∈ Filter.comap (⇑(WithAbs.congr v w (RingEquiv.refl F))) (𝓝 0)
⊢ U ∈ 𝓝 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
⊢ (fun z ↦ ↑(s + 1) • F z) x ≠ 0

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
y : 𝕜
⊢ (s + 1) • (y - x) ^ s • F y = (y - x) ^ s • (fun z ↦ ↑(s + 1) • F z) y

Tactic:
· simpa using ⟨by norm_cast, hFne⟩

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
y : 𝕜
⊢ (s + 1) • (y - x) ^ s • F y = (y - x) ^ s • (fun z ↦ ↑(s + 1) • F z) y
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
z₀ : 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
n : ℕ
IH : ∀ {f : 𝕜 → E}, AnalyticAt 𝕜 f z₀ → (↑n ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0)
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hfz : f z₀ = 0
⊢ analyticOrderAt (deriv f) z₀ + 1 = analyticOrderAt f z₀

Tactic:
simpa [hfz] using hf.analyticOrderAt_deriv_add_one

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

Goal state before:
pp: case convert_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 : ℕ
this : AnalyticAt 𝕜 (fun z ↦ ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0) 0
i : ℕ
⊢ i < n →
    iteratedDeriv i (fun i ↦ f i - ∑ i_1 ∈ Finset.range n, (i ^ i_1 / ↑i_1.factorial) • iteratedDeriv i_1 f 0) 0 = 0

Tactic:
hi

Goal state after:
case convert_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 : ℕ
this : AnalyticAt 𝕜 (fun z ↦ ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0) 0
i : ℕ
hi : i < n
⊢ iteratedDeriv i (fun i ↦ f i - ∑ i_1 ∈ Finset.range n, (i ^ i_1 / ↑i_1.factorial) • iteratedDeriv i_1 f 0) 0 = 0
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case empty
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_5
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ σ ∈ ∅, MeromorphicAt (F σ) x
⊢ MeromorphicAt (∏ i ∈ ∅, F i) x

Tactic:
rw [Finset.prod_empty]
    apply MeromorphicAt.const

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

Goal state before:
pp: case empty
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
ι : Type u_5
s : Finset ι
G : ι → 𝕜 → E
x : 𝕜
h : ∀ σ ∈ ∅, MeromorphicAt (G σ) x
⊢ MeromorphicAt (∑ n ∈ ∅, G n) x

Tactic:
simp only [Finset.sum_empty]
    exact analyticAt_const.meromorphicAt

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
x : 𝕜
f g : 𝕜 → E
hg : MeromorphicAt g x
⊢ MeromorphicAt (f + g) x ↔ MeromorphicAt f x

Tactic:
rw [add_comm]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hg : MeromorphicAt g x
⊢ MeromorphicAt (g + f) x ↔ MeromorphicAt f x
Module: Mathlib.RingTheory.Binomial

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

Tactic:
by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1)),
    factorial_nsmul_multichoose_eq_ascPochhammer, smul_zero, ascPochhammer_succ_left,
    smeval_X_mul, zero_mul]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: r n : ℕ
⊢ (r + n - 1).descFactorial n = Polynomial.eval r (ascPochhammer ℕ n)

Tactic:
ascPochhammer_nat_eq_descFactorial

Goal state after:
r n : ℕ
⊢ (r + n - 1).descFactorial n = (r + n - 1).descFactorial n
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case ofNat
k n : ℕ
⊢ ↑((n + k - 1).descFactorial k) = ↑(Polynomial.eval n (ascPochhammer ℕ k))

Tactic:
ascPochhammer_nat_eq_descFactorial

Goal state after:
case ofNat
k n : ℕ
⊢ ↑((n + k - 1).descFactorial k) = ↑((n + k - 1).descFactorial k)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: p : ℂ × ℂ
hp : p.1 ∈ slitPlane
A : p.1 ≠ 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ cexp (log x.1 * x.2)
⊢ HasStrictFDerivAt (fun x ↦ x.1 ^ x.2)
    ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℂ ℂ ℂ) p

Tactic:
cpow_sub _ _ A,

Goal state after:
p : ℂ × ℂ
hp : p.1 ∈ slitPlane
A : p.1 ≠ 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ cexp (log x.1 * x.2)
⊢ HasStrictFDerivAt (fun x ↦ x.1 ^ x.2)
    ((p.2 * (p.1 ^ p.2 / p.1 ^ 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ +
      (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℂ ℂ ℂ)
    p
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ⋯
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
v_in : v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun y ↦ ε * ‖y.2 - y.1‖) (𝓝 (u, v)) (𝓝 (ε * ‖v - u‖))

Tactic:
rw [nhds_prod_eq]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
v_in : v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun y ↦ ε * ‖y.2 - y.1‖) (𝓝 u ×ˢ 𝓝 v) (𝓝 (ε * ‖v - u‖))
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
⊢ choose 0 k = if k = 0 then 1 else 0

Tactic:
by
  split_ifs with hk
  · rw [hk, choose_zero_right]
  · 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_6
a : ℂ
this : binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
⊢ 0 < 1

Tactic:
norm_num

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

Goal state before:
pp: 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
⊢ iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B

Tactic:
ext z

Goal state after:
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
z : ℂ
⊢ iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B z =
    derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B z