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

Goal state before:
pp: κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
X Y : C
f : X ⟶ Y
⊢ ∀ ⦃a₂ : X ⟶ Y⦄, (fun f ↦ Arrow.mk f) f = (fun f ↦ Arrow.mk f) a₂ → f = a₂

Tactic:
g

Goal state after:
κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
X Y : C
f g : X ⟶ Y
⊢ (fun f ↦ Arrow.mk f) f = (fun f ↦ Arrow.mk f) g → f = g
Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable

Goal state before:
pp: X : SSet
inst✝ : X.Finite
⊢ ∃ Y, ∃ (_ : Y.Finite) (_ : IsFinitelyPresentable Y), ∃ p, Epi p

Tactic:
refine ⟨∐ (fun (s : X.N) ↦ Δ[s.dim]), inferInstance, ?_,
    Sigma.desc (fun s ↦ yonedaEquiv.symm s.simplex), ?_⟩

Goal state after:
case refine_1
X : SSet
inst✝ : X.Finite
⊢ IsFinitelyPresentable (∐ fun s ↦ Δ[s.dim])

case refine_2
X : SSet
inst✝ : X.Finite
⊢ Epi (Sigma.desc fun s ↦ yonedaEquiv.symm s.simplex)
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
⊢ (F.map f₁).app X₂ ≫ adj₂.homEquiv.symm (Arrow.Hom.left β) =
    (F.obj X₁).map f₂ ≫ adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.fst)

Tactic:
have := Arrow.w β =≫ sq₁₃.fst
          dsimp at this
          simp only [Category.assoc, sq₁₃.π_fst] at this
          simp only [← adj₂.homEquiv_symm_naturality_one,
            ← adj₂.homEquiv_symm_naturality_two,
            Arrow.mk_left, Arrow.mk_right, this]

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
i : Fin (d + 2)
hi : i < (min x hd).castSucc
⊢ φ x hd i = (objEquiv (x.cast hd).simplex) (i.castPred ⋯)

Tactic:
φ_of_ne _ _ _ hi.ne,

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 2)
hi : i < (min x hd).castSucc
⊢ (objEquiv (x.cast hd).simplex) ((min x hd).predAbove i) = (objEquiv (x.cast hd).simplex) (i.castPred ⋯)
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.refine_1.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ ((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left ≫
      (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to X.left =
    ((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom ≫ (ρ_ X.left).hom

Tactic:
apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ pushout.inl (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom) ≫
      pushout.desc ((initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to X.left) (ρ_ X.left).hom ⋯ ≫
        (ρ_ X.left).inv ≫
          pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
            (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom) =
    pushout.inl (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom) ≫
      𝟙 (X □ Arrow.mk (initial.to (𝟙_ C))).left

Tactic:
apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ pushout.inl (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom) ≫
      { hom := pushout.desc ((initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to X.left) (ρ_ X.left).hom ⋯,
            inv :=
              (ρ_ X.left).inv ≫
                pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
                  (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom),
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        X.hom =
    pushout.inl (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom) ≫
      (X □ Arrow.mk (initial.to (𝟙_ C))).hom ≫ (ρ_ X.right).hom

Tactic:
apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext

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✝² x✝¹ : Arrow C₃
x✝ : x✝² ⟶ x✝¹
⊢ Arrow.Hom.left
      ((G.leibnizPullback.obj (op X₁) ⋙ F.leibnizPushout.obj X₁).map 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)))
          ⋯) =
    Arrow.Hom.left
      (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)))
          ⋯ ≫
        (𝟭 (Arrow C₃)).map x✝)

Tactic:
apply pushout.hom_ext <;> simp [← homEquiv_symm_naturality_two,
        ← homEquiv_symm_naturality_three]

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

Goal state before:
pp: X : TopCat
⊢ ι₀ ≫
      TopCat.toSSet.obj X ◁ toSSetObjI ≫
        Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I =
    TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I

Tactic:
μ_δ,

Goal state after:
X : TopCat
⊢ ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI ≫ 𝟙 (TopCat.toSSet.obj X ⊗ TopCat.toSSet.obj TopCat.I) =
    TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: X : TopCat
⊢ ι₁ ≫
      TopCat.toSSet.obj X ◁ toSSetObjI ≫
        Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I =
    TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I

Tactic:
μ_δ,

Goal state after:
X : TopCat
⊢ ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI ≫ 𝟙 (TopCat.toSSet.obj X ⊗ TopCat.toSSet.obj TopCat.I) =
    TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv

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
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
this : ∀ᶠ (x : E × E) in 𝓝 a ×ˢ 𝓝 a, ‖f x.1 - f x.2 - f' (x.1 - x.2)‖ ≤ ↑c * ‖x.1 - x.2‖
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c

Tactic:
Filter.Eventually,

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
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
this : {x | ‖f x.1 - f x.2 - f' (x.1 - x.2)‖ ≤ ↑c * ‖x.1 - x.2‖} ∈ 𝓝 a ×ˢ 𝓝 a
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
⊢ ↑n ≤ ↑⋯.choose ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
rw [ENat.natCast_le_natCast]

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
⊢ n ≤ ⋯.choose ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : analyticOrderAt f z₀ ≠ analyticOrderAt g z₀
hgf : analyticOrderAt g z₀ < analyticOrderAt f z₀
⊢ analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g z₀)

Tactic:
simpa [hgf.le] using analyticOrderAt_add_eq_right_of_lt hgf

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

Goal state before:
pp: 𝕜 : 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)
h_zero : ∀ k < n, iteratedDeriv (k + 1) f z₀ = 0
h_nz : iteratedDeriv (n + 1) f z₀ ≠ 0
k : ℕ
hk : 0 < n + 1
⊢ iteratedDeriv 0 f z₀ = 0

Tactic:
| =>

Goal state after:
𝕜 : 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)
h_zero : ∀ k < n, iteratedDeriv (k + 1) f z₀ = 0
h_nz : iteratedDeriv (n + 1) f z₀ ≠ 0
k : ℕ
hk : 0 < n + 1
⊢ iteratedDeriv 0 f z₀ = 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : 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)
h_zero : ∀ k < n, iteratedDeriv (k + 1) f z₀ = 0
h_nz : iteratedDeriv (n + 1) f z₀ ≠ 0
k✝ k : ℕ
hk : k + 1 < n + 1
⊢ iteratedDeriv (k + 1) f z₀ = 0

Tactic:
| =>

Goal state after:
𝕜 : 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)
h_zero : ∀ k < n, iteratedDeriv (k + 1) f z₀ = 0
h_nz : iteratedDeriv (n + 1) f z₀ ≠ 0
k✝ k : ℕ
hk : k + 1 < n + 1
⊢ iteratedDeriv (k + 1) f z₀ = 0
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
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x
⊢ (fun z ↦ (z - x) ^ max m n • (f + g) z) = fun z ↦ (z - x) ^ max m n • f z + (z - x) ^ max m n • g z

Tactic:
Pi.add_apply,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x
⊢ (fun z ↦ (z - x) ^ max m n • (f z + g z)) = fun z ↦ (z - x) ^ max m n • f z + (z - x) ^ max m n • 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
x : 𝕜
f g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x
this :
  (fun z ↦ (z - x) ^ max m n • (f + g) z) = fun z ↦
    (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z
⊢ AnalyticAt 𝕜 (fun z ↦ (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z) x

Tactic:
exact (((analyticAt_id.sub analyticAt_const).pow _).smul hf).add
    (((analyticAt_id.sub analyticAt_const).pow _).smul hg)

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
hf : MeromorphicAt f x
hg : MeromorphicAt g x
z : 𝕜
⊢ f z - g z = (f + -g) z

Tactic:
Pi.add_apply,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
z : 𝕜
⊢ f z - g z = f z + (-g) z
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
hU : IsConnected U
⊢ (∃ u, analyticOrderAt f ↑u ≠ ⊤) ↔ ∀ (u : ↑U), analyticOrderAt f ↑u ≠ ⊤

Tactic:
have : ConnectedSpace U := Subtype.connectedSpace hU

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
hU : IsConnected U
this : ConnectedSpace ↑U
⊢ (∃ u, analyticOrderAt f ↑u ≠ ⊤) ↔ ∀ (u : ↑U), analyticOrderAt f ↑u ≠ ⊤
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
hU : IsConnected U
this : ConnectedSpace ↑U
⊢ (∃ u, analyticOrderAt f ↑u ≠ ⊤) ↔ ∀ (u : ↑U), analyticOrderAt f ↑u ≠ ⊤

Tactic:
obtain ⟨v⟩ : Nonempty U := inferInstance

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
hU : IsConnected U
this : ConnectedSpace ↑U
v : ↑U
⊢ (∃ u, analyticOrderAt f ↑u ≠ ⊤) ↔ ∀ (u : ↑U), analyticOrderAt f ↑u ≠ ⊤
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: ⊢ logDeriv rexp = 1

Tactic:
ext
  rw [logDeriv, Real.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
⊢ (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)

Tactic:
induction k with
  | zero =>
    rw [descPochhammer_zero, Nat.descFactorial_zero, Nat.cast_one, smeval_one, npow_zero, one_smul]
  | succ k ih =>
    rw [descPochhammer_succ_right, Nat.descFactorial_succ, smeval_mul, ih, mul_comm, Nat.cast_mul,
      smeval_sub, smeval_X, smeval_natCast, npow_one, npow_zero, nsmul_one]
    by_cases! h : n < k
    · simp only [Nat.descFactorial_eq_zero_iff_lt.mpr h, Nat.cast_zero, zero_mul]
    · rw [Nat.cast_sub h]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
ih : (ascPochhammer ℕ k).smeval (-r) = (↑k).negOnePow • (descPochhammer ℤ k).smeval r
⊢ (ascPochhammer ℕ (k + 1)).smeval (-r) = (↑(k + 1)).negOnePow • (descPochhammer ℤ (k + 1)).smeval r

Tactic:
simp only [ascPochhammer_succ_right, smeval_mul, ih, descPochhammer_succ_right, sub_eq_add_neg]

Goal state after:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
ih : (ascPochhammer ℕ k).smeval (-r) = (↑k).negOnePow • (descPochhammer ℤ k).smeval r
⊢ (↑k).negOnePow • (descPochhammer ℤ k).smeval r * (X + ↑k).smeval (-r) =
    (↑(k + 1)).negOnePow • ((descPochhammer ℤ k).smeval r * (X + -↑k).smeval r)
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 g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₁ : ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x = g x
h₂ : EqOn f g Uᶜ
x : 𝕜
hx : x ∈ U
⊢ f =ᶠ[𝓝[≠] x] g

Tactic:
Filter.Eventually,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₁ : {x | f x = g x} ∈ codiscreteWithin U
h₂ : EqOn f g Uᶜ
x : 𝕜
hx : x ∈ U
⊢ f =ᶠ[𝓝[≠] x] g
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 g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₁ : ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x = g x
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
⊢ f =ᶠ[𝓝[≠] x] g

Tactic:
Filter.Eventually,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₁ : {x | f x = g x} ∈ codiscreteWithin U
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
⊢ f =ᶠ[𝓝[≠] x] g
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: 𝕂 : Type u
inst✝⁵ : Field 𝕂
inst✝⁴ : CharZero 𝕂
𝔸 : Type v
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b : 𝕂
h : ∀ (k : ℕ), ↑k ≠ -b
⊢ (FormalMultilinearSeries.ofScalars 𝔸 fun x ↦ Ring.choose a x) =
    FormalMultilinearSeries.ofScalars 𝔸 fun k ↦ (-1) ^ k * ordinaryHypergeometricCoefficient (-a) b b k

Tactic:
congr! with n

Goal state after:
𝕂 : Type u
inst✝⁵ : Field 𝕂
inst✝⁴ : CharZero 𝕂
𝔸 : Type v
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b : 𝕂
h : ∀ (k : ℕ), ↑k ≠ -b
n : ℕ
⊢ Ring.choose a n = (-1) ^ n * ordinaryHypergeometricCoefficient (-a) b b n
Module: Mathlib.Analysis.Analytic.Polynomial

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
s : Set E
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p✝ p q : A[X]
hp : AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) p) s z
hq : AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) q) s z
⊢ AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) (p + q)) s z

pp: case refine_3
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
s : Set E
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p✝ : A[X]
p : ℕ
i : A
hp : AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) (C i * X ^ p)) s z
⊢ AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) (C i * X ^ (p + 1))) s z

Tactic:
· simp_rw [aeval_add]; exact hp.add hq

Goal state after:
case refine_3
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
s : Set E
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p✝ : A[X]
p : ℕ
i : A
hp : AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) (C i * X ^ p)) s z
⊢ AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) (C i * X ^ (p + 1))) s z
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
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : p n = 0
⊢ iteratedFDerivWithin 𝕜 n f s x = 0

Tactic:
have : iteratedFDerivWithin 𝕜 n f s x = p.iteratedFDerivSeries n 0 (fun _ ↦ 0) :=
    ((h.iteratedFDerivWithin h' n hu hx).coeff_zero _).symm
  rw [this, p.iteratedFDerivSeries_eq_zero (p.congr_zero (Nat.zero_add n).symm hn), zero_apply]

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
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
m : ℕ
hm : n + 1 ≤ m
⊢ q m = 0

Tactic:
have : n ≠ m := by lia

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
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
m : ℕ
hm : n + 1 ≤ m
this : n ≠ m
⊢ q m = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inr.inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ 0 < (x * y).toReal

Tactic:
toReal_mul

Goal state after:
case inr.inr.inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ 0 < x.toReal * y.toReal
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
n : ℕ
⊢ ((fun n ↦ u n / ↑n) + fun n ↦ v n / ↑n) n = (u + v) n / ↑n

Tactic:
Pi.add_apply,

Goal state after:
u v : ℕ → EReal
n : ℕ
⊢ u n / ↑n + v n / ↑n = (u + v) n / ↑n