mathlib-initiative/mathlib-tactics huggingface dataset:
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 sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty (Arrow.LiftStruct φ)) ↔
    ∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty (Arrow.LiftStruct φ)

Tactic:
constructor

Goal state after:
case mp
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 sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty (Arrow.LiftStruct φ)) →
    ∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty (Arrow.LiftStruct φ)

case mpr
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₁₃.π), Nonempty (Arrow.LiftStruct φ)) →
    ∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty (Arrow.LiftStruct φ)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case pos.fst
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ (k.castSucc, (s.δ.cast ⋯).simplex.2 (min s.δ ⋯)).1 = ((objEquiv (s.x.cast ⋯).simplex) s.index.castSucc).1

Tactic:
simp [← s.isIndex.simplex_fst_castSucc]

Goal state after:
case pos.fst
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ (s.x.cast ⋯).simplex.1 s.index.castSucc = (s.x.cast ⋯).simplex.1 s.index.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne

Goal state before:
pp: case refine_2.inr
p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
hs✝ : (s₁, objMk₁ (Fin.last (p + 1)).succ) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
hs : orderHomOfSimplex (s₁, objMk₁ (Fin.last (p + 1)).succ) ⋯ = OrderHom.id
⊢ ∃ a,
    (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) a =
      ⟨(s₁, objMk₁ (Fin.last (p + 1)).succ), hs✝⟩

Tactic:
have := DFunLike.congr_fun hs (Fin.last _)
        simp only [Fin.succ_last, orderHomOfSimplex_coe,
          OrderHom.id_coe, id_eq, Fin.ext_iff, Fin.val_last,
          stdSimplex.objMk₁_of_castSucc_lt (Fin.last (p + 2))
            (Fin.last (p + 1)) (by simp),
          Fin.coe_ofNat_eq_mod, Nat.zero_mod, add_zero] at this
        lia

Goal state after:
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₂
adj₂ : F ⊣₂ G
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₁✝ Y₁✝ : Arrow C₁
x✝ : X₁✝ ⟶ Y₁✝
⊢ (LeibnizAdjunction.adj F G adj₂ X₁✝).unit ≫ whiskerRight (F.leibnizPushout.map x✝) (G.leibnizPullback.obj (op X₁✝)) =
    (LeibnizAdjunction.adj F G adj₂ Y₁✝).unit ≫ (F.leibnizPushout.obj Y₁✝).whiskerLeft (G.leibnizPullback.map x✝.op)

Tactic:
ext

Goal state after:
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
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₁✝ Y₁✝ : Arrow C₁
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : Arrow C₂
⊢ Arrow.Hom.left
      (((LeibnizAdjunction.adj F G adj₂ X₁✝).unit ≫
            whiskerRight (F.leibnizPushout.map x✝¹) (G.leibnizPullback.obj (op X₁✝))).app
        x✝) =
    Arrow.Hom.left
      (((LeibnizAdjunction.adj F G adj₂ Y₁✝).unit ≫
            (F.leibnizPushout.obj Y₁✝).whiskerLeft (G.leibnizPullback.map x✝¹.op)).app
        x✝)

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
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₁✝ Y₁✝ : Arrow C₁
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : Arrow C₂
⊢ Arrow.Hom.right
      (((LeibnizAdjunction.adj F G adj₂ X₁✝).unit ≫
            whiskerRight (F.leibnizPushout.map x✝¹) (G.leibnizPullback.obj (op X₁✝))).app
        x✝) =
    Arrow.Hom.right
      (((LeibnizAdjunction.adj F G adj₂ Y₁✝).unit ≫
            (F.leibnizPushout.obj Y₁✝).whiskerLeft (G.leibnizPullback.map x✝¹.op)).app
        x✝)
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

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

Tactic:
ext

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

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

Tactic:
ext

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Subsingleton (ZerothHomotopy ↑X) ∧ Nonempty (ZerothHomotopy ↑X)

Tactic:
constructor

Goal state after:
case left
X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Subsingleton (ZerothHomotopy ↑X)

case right
X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Nonempty (ZerothHomotopy ↑X)
Module: Mathlib.Analysis.Normed.Field.WithAbs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
inst✝³ : Field R
T : Type u_3
inst✝² : Field T
v : AbsoluteValue R S
inst✝¹ : Algebra R T
inst✝ : Algebra.IsSeparable R T
⊢ (algebraMap (WithAbs v) T).comp ↑(equiv v).symm = (↑(RingEquiv.refl T)).comp (algebraMap R T)

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
inst✝³ : Field R
T : Type u_3
inst✝² : Field T
v : AbsoluteValue R S
inst✝¹ : Algebra R T
inst✝ : Algebra.IsSeparable R T
x✝ : R
⊢ ((algebraMap (WithAbs v) T).comp ↑(equiv v).symm) x✝ = ((↑(RingEquiv.refl T)).comp (algebraMap R T)) x✝
Module: Mathlib.Analysis.Normed.Module.Connected

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

Tactic:
simp only [c, x]

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

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

Tactic:
simp only [c, x]

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

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
hcₙ : Tendsto (fun n ↦ w (c n)) atTop (𝓝 (w b))
hcⱼ : ∀ (j : ι), j ≠ i → ∀ s ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}, 0 ∈ s → ∃ a, ∀ (b : ℕ), a ≤ b → (v j) (c b) ∈ s
r₁ : ℕ
hr₁ : ∀ (b : ℕ), r₁ ≤ b → 1 < (v i) (c b)
rₙ : (j : ι) → j ≠ i → ℕ
hrₙ : ∀ (j : ι) (hj : j ≠ i) (b : ℕ), rₙ j hj ≤ b → (v j) (c b) ∈ Set.Iio 1
rN : ℕ
hrN : ∀ (b : ℕ), rN ≤ b → w (c b) < 1
this : Fintype ι
r : ℕ := max (Finset.univ.sup fun j ↦ if h : j = i then r₁ else rₙ j h) rN
⊢ w (c r) < 1

Tactic:
exact hrN _ <| le_max_iff.2 (.inr le_rfl)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 (deriv f x) hf')
hfd : HasStrictFDerivAt f (↑i) x
R : OpenPartialHomeomorph 𝕜 𝕜 := HasStrictFDerivAt.toOpenPartialHomeomorph f hfd
hx : x ∈ R.source
⊢ FormalMultilinearSeries.ofScalars 𝕜 (fun n ↦ iteratedDeriv n f x / ↑n.factorial) 1 =
    (continuousMultilinearCurryFin1 𝕜 𝕜 𝕜).symm ↑i

Tactic:
ext

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := ⋯
hfd : HasStrictFDerivAt f (↑i) x
R : OpenPartialHomeomorph 𝕜 𝕜 := ⋯
hx : x ∈ R.source
⊢ ((FormalMultilinearSeries.ofScalars 𝕜 (fun n ↦ iteratedDeriv n f x / ↑n.factorial) 1) fun x ↦ 1) =
    ((continuousMultilinearCurryFin1 𝕜 𝕜 𝕜).symm ↑i) fun x ↦ 1
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ 0 • g z) ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0

Tactic:
constructor

Goal state after:
case pos.mp
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ 0 • g z) → ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0

case pos.mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0 → ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ 0 • g z
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : analyticOrderAt f z₀ = ⊤
⊢ analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀

Tactic:
simp [analyticOrderAt_smul_eq_top_of_left, *]

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
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
⊢ ¬↑s + 1 = 0

Tactic:
by norm_cast

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasDerivAt (fun t ↦ log (f t)) (f' / f x) x

Tactic:
by
  rw [div_eq_inv_mul]; exact (hasStrictDerivAt_log h₂).hasDerivAt.comp x h₁

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
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
⊢ AnalyticAt 𝕜 (fun z ↦ ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0) 0

Tactic:
refine Finset.analyticAt_fun_sum _ fun i hi ↦ ?_

Goal state after:
𝕜 : 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 i : ℕ
hi : i ∈ Finset.range n
⊢ AnalyticAt 𝕜 (fun z ↦ (z ^ i / ↑i.factorial) • iteratedDeriv i f 0) 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
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
⊢ ∃ F,
    AnalyticAt 𝕜 F 0 ∧
      ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z

Tactic:
by
  simp only [← sub_eq_iff_eq_add']
  have : AnalyticAt 𝕜
      (fun z : 𝕜 ↦ ∑ i ∈ .range n, (z ^ i / i.factorial) • iteratedDeriv i f 0) 0 := by
    refine Finset.analyticAt_fun_sum _ fun i hi ↦ ?_
    fun_prop
  convert! (natCast_le_analyticOrderAt (hf.fun_sub this)).mp ?_
  · simp
  · rw [natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero (hf.fun_sub this)]
    intro i hi
    rw [iteratedDeriv_fun_sub (AnalyticAt.contDiffAt <| by fun_prop) this.contDiffAt]
    simp (disch := fun_prop) only [iteratedDeriv_fun_sum, iteratedDeriv_smul_const,
      iteratedDeriv_div_const, iteratedDeriv_fun_pow_zero]
    simp [ite_div, Finset.sum_ite_eq_of_mem _ _ _ (Finset.mem_range.mpr hi)]

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

Goal state before:
pp: case inl
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -a
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0

Tactic:
ext

Goal state after:
case inl
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -a
x✝ : Fin n → 𝔸
⊢ (ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) x✝ = 0 x✝
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case inr.inl
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -b
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0

Tactic:
ext

Goal state after:
case inr.inl
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -b
x✝ : Fin n → 𝔸
⊢ (ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) x✝ = 0 x✝
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case inr.inr
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -c
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0

Tactic:
ext

Goal state after:
case inr.inr
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -c
x✝ : Fin n → 𝔸
⊢ (ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) x✝ = 0 x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X Y : SSet
m : ℕ
⊢ prodComparison hoFunctor X Δ[m] =
    hoFunctor.map (prod.braiding X Δ[m]).hom ≫
      prodComparison hoFunctor Δ[m] X ≫ (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)).hom

Tactic:
ext

Goal state after:
case h₁
X Y : SSet
m : ℕ
⊢ (prodComparison hoFunctor X Δ[m] ≫ prod.fst).toFunctor =
    ((hoFunctor.map (prod.braiding X Δ[m]).hom ≫
          prodComparison hoFunctor Δ[m] X ≫ (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)).hom) ≫
        prod.fst).toFunctor

case h₂
X Y : SSet
m : ℕ
⊢ (prodComparison hoFunctor X Δ[m] ≫ prod.snd).toFunctor =
    ((hoFunctor.map (prod.braiding X Δ[m]).hom ≫
          prodComparison hoFunctor Δ[m] X ≫ (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)).hom) ≫
        prod.snd).toFunctor
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:
exact h_zero k (by lia)

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

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : EventuallyConst g (𝓝 z₀)
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀

Tactic:
have := hg_nc.comp f

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : EventuallyConst g (𝓝 z₀)
this : EventuallyConst (f ∘ g) (𝓝 z₀)
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) 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
⊢ IsClopen {u | analyticOrderAt f ↑u = ⊤}

Tactic:
constructor

Goal state after:
case left
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
⊢ IsClosed[instTopologicalSpaceSubtype] {u | analyticOrderAt f ↑u = ⊤}

case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
⊢ IsOpen[instTopologicalSpaceSubtype] {u | analyticOrderAt f ↑u = ⊤}
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case left
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
⊢ IsClosed[instTopologicalSpaceSubtype] {u | analyticOrderAt f ↑u = ⊤}

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_forall_mem_open]

Goal state after:
case left
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
⊢ ∀ x ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ,
    ∃ t ⊆ {u | analyticOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ x ∈ t
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
⊢ Subtype.val ⁻¹' t' ⊆ {u | analyticOrderAt f ↑u = ⊤}ᶜ ∧
    IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t') ∧ z ∈ Subtype.val ⁻¹' t'

Tactic:
constructor

Goal state after:
case h.left
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
⊢ Subtype.val ⁻¹' t' ⊆ {u | analyticOrderAt f ↑u = ⊤}ᶜ

case h.right
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t') ∧ z ∈ Subtype.val ⁻¹' t'
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case h.right
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t') ∧ z ∈ Subtype.val ⁻¹' t'

Tactic:
· exact ⟨isOpen_induced h₂t', h₃t'⟩

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

Goal state before:
pp: case zero
⊢ iteratedDeriv (0 + 1) cos = -iteratedDeriv 0 sin

Tactic:
ext

Goal state after:
case zero
x✝ : ℂ
⊢ iteratedDeriv (0 + 1) cos x✝ = (-iteratedDeriv 0 sin) x✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: case zero
⊢ iteratedDeriv (0 + 1) cos = -iteratedDeriv 0 sin

Tactic:
ext

Goal state after:
case zero
x✝ : ℝ
⊢ iteratedDeriv (0 + 1) cos x✝ = (-iteratedDeriv 0 sin) x✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: ⊢ logDeriv sin = cot

Tactic:
ext

Goal state after:
x✝ : ℂ
⊢ logDeriv sin x✝ = x✝.cot
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: ⊢ logDeriv sin = cot

Tactic:
ext

Goal state after:
x✝ : ℝ
⊢ logDeriv sin x✝ = x✝.cot
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: ⊢ logDeriv cos = -tan

Tactic:
ext

Goal state after:
x✝ : ℂ
⊢ logDeriv cos x✝ = (-tan) x✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: ⊢ logDeriv cos = -tan

Tactic:
ext

Goal state after:
x✝ : ℝ
⊢ logDeriv cos x✝ = (-tan) x✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: ⊢ logDeriv cexp = 1

Tactic:
ext

Goal state after:
x✝ : ℂ
⊢ logDeriv cexp x✝ = 1 x✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: ⊢ logDeriv rexp = 1

Tactic:
ext

Goal state after:
x✝ : ℝ
⊢ logDeriv rexp x✝ = 1 x✝
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case negSucc
k n : ℕ
⊢ ↑(↑k).negOnePow * ↑((n + 1).choose k * k.factorial) = (ascPochhammer ℕ k).smeval -[n+1]

Tactic:
mul_comm _ (k.factorial),

Goal state after:
case negSucc
k n : ℕ
⊢ ↑(↑k).negOnePow * ↑(k.factorial * (n + 1).choose k) = (ascPochhammer ℕ k).smeval -[n+1]