mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: n : ℕ
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
H :
  ∀ (x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })) (y : Y.obj (op { obj := ⦋2⦌, property := _proof_14 })),
    f₁ ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x) =
        (ConcreteCategory.hom (Y.map (δ₂ 2 _proof_12 _proof_15).op)) y →
      f₁ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_12 _proof_15).op)) y →
        f₁ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_12 _proof_15).op)) y
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x✝¹ x✝ : (SimplexCategory.Truncated 2)ᵒᵖ
φ : x✝¹ ⟶ x✝
⊢ ⊤ φ.unop

Tactic:
simp

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

Goal state before:
pp: X : Truncated 2
C : Type u
inst✝ : SmallCategory C
X' : Truncated 2
ψ : X ⟶ X'
φ : X' ⟶ (truncation 2).obj (nerve C)
x✝ : X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ (descOfTruncation (ψ ≫ φ)).obj (mk x✝) = (mapHomotopyCategory ψ ⋙ descOfTruncation φ).obj (mk x✝)

Tactic:
simp

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

Goal state before:
pp: case neg.refine_1
𝕜 : 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₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
f' : 𝕜 → 𝕜
h₁f' : AnalyticAt 𝕜 f' z₀
h₂f' : f' z₀ ≠ 0
h₃f' : f =ᶠ[𝓝 z₀] fun z ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z
g' : 𝕜 → E
h₁g' : AnalyticAt 𝕜 g' z₀
h₂g' : g' z₀ ≠ 0
h₃g' : g =ᶠ[𝓝 z₀] fun z ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z
⊢ (f' • g') z₀ ≠ 0

Tactic:
simp

Goal state after:
case neg.refine_1
𝕜 : 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₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
f' : 𝕜 → 𝕜
h₁f' : AnalyticAt 𝕜 f' z₀
h₂f' : f' z₀ ≠ 0
h₃f' : f =ᶠ[𝓝 z₀] fun z ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z
g' : 𝕜 → E
h₁g' : AnalyticAt 𝕜 g' z₀
h₂g' : g' z₀ ≠ 0
h₃g' : g =ᶠ[𝓝 z₀] fun z ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z
⊢ ¬f' z₀ = 0 ∧ ¬g' z₀ = 0
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

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
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
hc' : 0 < ↑‖↑f'.symm‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R ↦ closedBall (f 0) R ⊆ range f
hp : ∀ᶠ (r : ℝ) in atTop, p ((↑‖↑f'.symm‖₊⁻¹ - ↑c) * r)
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall (f 0) R, ∃ a, f a = y

Tactic:
refine ((tendsto_id.const_mul_atTop hc').frequently hp.frequently).mono ?_

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
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
hc' : 0 < ↑‖↑f'.symm‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R ↦ closedBall (f 0) R ⊆ range f
hp : ∀ᶠ (r : ℝ) in atTop, p ((↑‖↑f'.symm‖₊⁻¹ - ↑c) * r)
⊢ ∀ (x : ℝ), p x → ∀ y ∈ closedBall (f 0) x, ∃ a, f a = 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
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
this : analyticOrderAt (fun y ↦ (s + 1) • (y - x) ^ s • F y) x = ↑s
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ (s + 1) • deriv F z = (z - x) ^ (s + 1) • deriv F z

Tactic:
simp

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

Goal state before:
pp: case zero
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
z₀ : 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
⊢ ↑0 ≤ analyticOrderAt f z₀ ↔ ∀ i < 0, iteratedDeriv i f z₀ = 0

Tactic:
simp

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
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
⊢ 0 ≤ n

Tactic:
simp

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

Goal state before:
pp: X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
x : X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ (descOfTruncation (homToNerveMk F)).obj (mk x) = F.obj (mk x)

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
inst✝ : CharZero 𝕜
n' : ℕ
hk : ∀ {n : ℕ}, ↑n = analyticOrderAt f z₀ → n ≠ 0 → n' ≤ n → analyticOrderAt (deriv^[n'] f) z₀ = ↑(n - n')
n : ℕ
Hn : ↑n = analyticOrderAt f z₀
Hpos : n ≠ 0
Hk : n' + 1 ≤ n
this : n - n'.succ + 1 = n - n'
⊢ ↑(n - n'.succ + 1) = ↑n - ↑n'.succ + 1

Tactic:
simp

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

Goal state before:
pp: case e'_5
𝕜 : 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
x✝¹ : 𝕜 → E
x✝ : 𝕜
⊢ x✝ = x✝ - 0

Tactic:
simp

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

Goal state before:
pp: this :
  (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n log 1 / ↑n.factorial
⊢ 1 ∈ slitPlane

Tactic:
simp

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

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
x : C
⊢ ⦋0⦌.len ≤ 2

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ -(-1) ^ 0 / ↑0 = iteratedDeriv 0 log 1 / ↑(Nat.factorial 0)

Tactic:
simp

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

Goal state before:
pp: r : ENNReal
hp : HasFPowerSeriesOnBall log (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) 1 r
this :
  HasFPowerSeriesOnBall log
    (FormalMultilinearSeries.restrictScalars ℝ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n))
    (ofRealCLM 1) r
n : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℝ (fun n ↦ -(-1) ^ n / ↑n) n) fun x ↦ 1) =
    reCLM
      ((FormalMultilinearSeries.restrictScalars ℝ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) n)
        (⇑ofRealCLM ∘ fun x ↦ 1))

Tactic:
simp

Goal state after:
r : ENNReal
hp : HasFPowerSeriesOnBall log (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) 1 r
this :
  HasFPowerSeriesOnBall log
    (FormalMultilinearSeries.restrictScalars ℝ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n))
    (ofRealCLM 1) r
n : ℕ
⊢ -(-1) ^ n / ↑n = -((-1) ^ n).re / ↑n
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case zero
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
⊢ ((↑0!)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 0) * Polynomial.eval b (ascPochhammer 𝕂 0) *
        (Polynomial.eval c (ascPochhammer 𝕂 0))⁻¹) •
      0 ^ 0 =
    Pi.single 0 1 0

Tactic:
simp

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

Goal state before:
pp: case succ
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n✝ : ℕ
⊢ ((↑(n✝ + 1)!)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 (n✝ + 1)) * Polynomial.eval b (ascPochhammer 𝕂 (n✝ + 1)) *
        (Polynomial.eval c (ascPochhammer 𝕂 (n✝ + 1)))⁻¹) •
      0 ^ (n✝ + 1) =
    Pi.single 0 1 (n✝ + 1)

Tactic:
simp

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

Goal state before:
pp: case top
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
n m : ℕ
⊢ ⊤ = ↑m ↔ ↑m ≤ ⊤ ∧ ¬↑m + 1 ≤ ⊤

Tactic:
simp

Goal state after:
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 := ball x δ
this✝ :
  ∀
    p ∈
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s) ×ˢ
        closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s),
    ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
y : E
y_in : y ∈ B ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
this :
  B ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s)
⊢ (x, y) ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s) ×ˢ
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s)

Tactic:
exact ⟨this ⟨mem_ball_self δ_pos, hx⟩, this y_in⟩

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

Goal state before:
pp: case e'_3.e'_5.e'_6
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
x✝ : ℕ
⊢ ↑x✝ = 1 * ↑x✝

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_6.e'_6
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
x✝ : ℕ
⊢ ↑x✝ = 1 * ↑x✝

Tactic:
simp

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

Goal state before:
pp: case e'_5
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
⊢ 1 = 1 / 1

Tactic:
simp

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

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

Tactic:
simp

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
ι : Type u_5
s : Finset ι
G : ι → 𝕜 → E
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (G σ) x
x✝ : 𝕜
⊢ ∑ n ∈ s, G n x✝ = (∑ n ∈ s, G n) x✝

Tactic:
simp

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

Goal state before:
pp: 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'
w : ↑U
⊢ w ∈ Subtype.val ⁻¹' t' → w ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ

Tactic:
hw

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'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
⊢ w ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
m : ℕ
z : 𝕜
hfg : ∀ᶠ (x : 𝕜) in 𝓝 z, x ∈ {z}ᶜ → f x = g x
hf : AnalyticAt 𝕜 (fun z_1 ↦ (z_1 - z) ^ m • f z_1) z
this : AnalyticAt 𝕜 (fun z_1 ↦ z_1 - z) z
hz : z ∈ {z}ᶜ → f z = g z
⊢ (z - z) • (z - z) ^ m • f z = (z - z) ^ (m + 1) • g z

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Prod

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_1
E' : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableAt 𝕜 (fun x ↦ φ x i) x
⊢ (ContinuousLinearMap.pi fun i ↦ fderiv 𝕜 (fun x ↦ φ x i) x) 1 = fun i ↦ (fderiv 𝕜 (fun x ↦ φ x i) x) 1

Tactic:
simp

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

Goal state before:
pp: case inl
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
m n : ℕ
g : 𝕜 → 𝕜'
z : 𝕜
hg_ne' : g z ≠ 0
hf : AnalyticAt 𝕜 (fun z_1 ↦ (z_1 - z) ^ m • f z_1) z
h_eq : ¬(fun z_1 ↦ (z_1 - z) ^ m • f z_1) =ᶠ[𝓝 z] 0
hg_an : AnalyticAt 𝕜 g z
hg_ne : g z ≠ 0
hg_eq : ∀ᶠ (z_1 : 𝕜) in 𝓝 z, (z_1 - z) ^ m • f z_1 = (z_1 - z) ^ n • g z_1
this : AnalyticAt 𝕜 (fun z_1 ↦ (z_1 - z) ^ (m + 1)) z
hfg : (z - z) ^ m • f z = (z - z) ^ n • g z
⊢ (z - z) ^ (m + 1) • g⁻¹ z = (z - z) ^ (n + 1) • f⁻¹ z

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case succ
n : ℕ
ih : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
x : ℂ
⊢ -deriv (iteratedDeriv n sin) x = (-deriv (iteratedDeriv n sin)) x

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ iteratedDeriv (2 * 0) sin = (-1) ^ 0 * sin

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ iteratedDeriv (2 * 0) cos = (-1) ^ 0 * cos

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n + 1) sin = (-1) ^ n * cos

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 0 sin)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 1 sin)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 0 cos)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 1 cos)

Tactic:
simp

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

Goal state before:
pp: n✝ n : ℕ
⊢ Differentiable ℂ (iteratedDeriv (n + 2) cos)

Tactic:
by simp [differentiable_iteratedDeriv_cos]

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

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

Tactic:
simp

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

Goal state before:
pp: case succ
n : ℕ
ih : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
x : ℝ
⊢ -deriv (iteratedDeriv n sin) x = (-deriv (iteratedDeriv n sin)) x

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 0 sin)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 1 sin)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 0 cos)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 1 cos)

Tactic:
simp

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

Goal state before:
pp: n✝ n : ℕ
⊢ Differentiable ℝ (iteratedDeriv (n + 2) cos)

Tactic:
by simp [differentiable_iteratedDeriv_cos]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
x : 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : y ∈ {x}ᶜ
⊢ AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y → AnalyticAt 𝕜 f y

Tactic:
hf

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
x : 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : y ∈ {x}ᶜ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
⊢ AnalyticAt 𝕜 f y
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case zero
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
⊢ multichoose 2 0 = ↑0 + 1

Tactic:
multichoose_zero_right,

Goal state after:
case zero
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
⊢ 1 = ↑0 + 1
Module: Mathlib.RingTheory.Binomial

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

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ Nat.factorial 0 • multichoose (r - ↑0 + 1) 0 = Nat.factorial 0 • (r + 1) ^ 0

Tactic:
simp

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

Goal state before:
pp: f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : (𝓝[s \ {x}] x).NeBot
hc : c = 0
⊢ ¬{0, 1}.Infinite

Tactic:
simp

Goal state after:
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
n : ℕ
⊢ Polynomial.eval (1 + a - ↑n) (ascPochhammer 𝕂 n) * (↑n !)⁻¹ =
    Polynomial.eval (1 + a - ↑n) (ascPochhammer 𝕂 n) * (↑n !)⁻¹ * (-1) ^ (n * 2)

Tactic:
simp

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

Goal state before:
pp: 𝕂 : Type v
inst✝² : RCLike 𝕂
𝔸 : Type u
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a : ℕ
⊢ ∀ (k : ℕ), ¬False

Tactic:
simp

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

Goal state before:
pp: 𝕂 : Type v
inst✝² : RCLike 𝕂
𝔸 : Type u
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ ↑k
⊢ ∀ (k : ℕ), ¬False

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
⊢ (descPochhammer ℤ 0).smeval (r + s) =
    ∑ ij ∈ antidiagonal 0, ↑(Nat.choose 0 ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)

Tactic:
simp

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

Goal state before:
pp: a : ℂ
n : ℕ
B : Set ℂ := Metric.ball 0 1
this : iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B 0 = (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) 0
⊢ 0 ∈ Metric.ball 0 1

Tactic:
simp

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

Goal state before:
pp: p : ℝ × ℝ
hp : 0 < p.1
⊢ 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:
have : (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) :=
    (continuousAt_fst.eventually (lt_mem_nhds hp)).mono fun p hp => rpow_def_of_pos hp _
  refine HasStrictFDerivAt.congr_of_eventuallyEq ?_ this.symm
  convert! ((hasStrictFDerivAt_fst.log hp.ne').fun_mul hasStrictFDerivAt_snd).exp using 1
  rw [rpow_sub_one hp.ne', ← rpow_def_of_pos hp, smul_add, smul_smul, mul_div_left_comm,
    div_eq_mul_inv, smul_smul, smul_smul, mul_assoc, add_comm]

Goal state after: