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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X Y : SSet
f : X ⟶ Y
R : C
n : ℕ
x : X _⦋n⦌
⊢ X.ιChainComplex x ≫ (chainComplexMap f R).f n = Y.ιChainComplex ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x)

Tactic:
by
  dsimp [chainComplexMap, chainComplexFunctor, ιChainComplex, Sigma.map',
    chainComplex, chainComplexFunctor]
  simp

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 m : ℕ
k : Fin (m + 2)
n : ℕ
hk : k = Fin.last (m + 1)
⊢ (Λ[m + 1, 0].unionProd ∂Δ[n]).op.preimage
      (((stdSimplex.opIso ⦋m + 1⦌).inv ⊗ₘ (stdSimplex.opIso ⦋n⦌).inv) ≫ Functor.LaxMonoidal.μ opFunctor Δ[m + 1] Δ[n]) =
    Λ[m + 1, k].unionProd ∂Δ[n]

Tactic:
rw [hk, Subcomplex.preimage_comp,
            Subcomplex.preimage_op_unionProd,
            Subcomplex.preimage_unionProd,
            op_boundary, op_horn, Fin.rev_zero]

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 = TopCat.toSSet.map TopCat.ι₀

Tactic:
rw [← cancel_mono (μIso _ _ _).inv, Category.assoc, Category.assoc, μIso_inv,
    μ_δ, Category.comp_id]
  apply CartesianMonoidalCategory.hom_ext <;> simp [← Functor.map_comp]

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 = TopCat.toSSet.map TopCat.ι₁

Tactic:
rw [← cancel_mono (μIso _ _ _).inv, Category.assoc, Category.assoc, μIso_inv,
    μ_δ, Category.comp_id]
  apply CartesianMonoidalCategory.hom_ext <;> simp [← Functor.map_comp]

Goal state after:
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
Ib : c + x = b
⊢ x ≠ 0

Tactic:
simpa [x] using sub_ne_zero.2 hab.symm

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case refine_2.inr.inl
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
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a = 1
⊢ ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1

Tactic:
let ⟨c, hc⟩ := exists_one_lt_lt_one_pi_of_eq_one ha.1 ha.2 ha₁ hb.1 (hb.2 ⟨j, .inr rfl⟩
        (by grind))

Goal state after:
case refine_2.inr.inl
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
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc✝ : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a = 1
c : R
hc :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) c ∧
    (∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) c < 1) ∧ (v j) c < 1
⊢ ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
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
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)⁻¹
⊢ 0 < (↑f'symm.nnnorm)⁻¹

Tactic:
exact (NNReal.coe_nonneg _).trans_lt hc

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

Goal state before:
pp: case refine_1.succ.zero.«2»
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
hn : 0 + 1 < 2
⊢ naturalityProperty f₀ f₁ hδ₁ hδ₀ hY (δ 2 ((fun i ↦ i) ⟨2, ⋯⟩) ⋯ ⋯)

Tactic:
· ext; apply hδ'₂ f₀ f₁ hδ₁ hδ₀ hY

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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h✝ : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
x✝ : ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne : ⋯.choose < n
this : ContinuousAt (fun z ↦ (z - z₀) ^ (n - m) • h z) z₀
z : 𝕜
hz : z ∈ {z₀}ᶜ
hf' : ((z - z₀) ^ n * ((z - z₀) ^ ⋯.choose)⁻¹) • h z = g z
hf'' : f z = (z - z₀) ^ n • h z
⊢ g z = (z - z₀) ^ (n - m) • h z

Tactic:
rw [pow_sub₀ _ (sub_ne_zero_of_ne hz) (by lia), ← hf']

Goal state after:
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
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑‖↑f'.symm‖₊ * (↑c * (↑(‖↑f'.symm‖₊⁻¹ - c)⁻¹ * ‖↑A y' - ↑A x'‖)) =
    ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖↑A x' - ↑A y'‖

Tactic:
simp only [norm_sub_rev, NNReal.coe_mul]

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
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑‖↑f'.symm‖₊ * (↑c * (↑(‖↑f'.symm‖₊⁻¹ - c)⁻¹ * ‖↑A x' - ↑A y'‖)) =
    ↑‖↑f'.symm‖₊ * ↑(‖↑f'.symm‖₊⁻¹ - c)⁻¹ * ↑c * ‖↑A x' - ↑A y'‖
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
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
⊢ E ≃ₜ F

Tactic:
refine
    (hf.toOpenPartialHomeomorph _ _ hc isOpen_univ).toHomeomorphOfSourceEqUnivTargetEqUniv rfl ?_
  rw [toOpenPartialHomeomorph_target, image_univ, range_eq_univ]
  exact hf.surjective hc

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:
rw [div_eq_inv_mul]; exact (hasStrictDerivAt_log h₂).hasDerivAt.comp x h₁

Goal state after:
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

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

Tactic:
· ext <;> simp [← Functor.map_comp]

Goal state after:
X Y : SSet
m : ℕ
⊢ IsIso
    (hoFunctor.map (prod.braiding X Δ[m]).hom ≫
      prodComparison hoFunctor Δ[m] X ≫ (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)).hom)
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖↑n !‖ ≠ 0

Tactic:
rw [norm_ne_zero_iff]

Goal state after:
case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ↑n ! ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖ ≠ 0

Tactic:
rw [norm_ne_zero_iff]

Goal state after:
case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ Polynomial.eval c (ascPochhammer 𝕂 n) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ ≠ 0

Tactic:
rw [norm_ne_zero_iff]

Goal state after:
case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ Polynomial.eval b (ascPochhammer 𝕂 n) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ ≠ 0

Tactic:
rw [norm_ne_zero_iff]

Goal state after:
case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ Polynomial.eval a (ascPochhammer 𝕂 n) ≠ 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
ι : Type u_5
s : Finset ι
G : ι → 𝕜 → E
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (G σ) x
⊢ MeromorphicAt (∑ n ∈ s, G n) x

Tactic:
induction s using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty]
    exact analyticAt_const.meromorphicAt
  | insert σ s hσ hind =>
    rw [Finset.sum_insert hσ]
    apply (h σ (Finset.mem_insert_self σ s)).add
      (hind (fun τ hτ ↦ h τ (Finset.mem_insert_of_mem 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
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
⊢ IsClopen {u | analyticOrderAt f ↑u = ⊤}

Tactic:
constructor
  · rw [← isOpen_compl_iff, isOpen_iff_forall_mem_open]
    intro z hz
    rcases (hf z.1 z.2).eventually_eq_zero_or_eventually_ne_zero with h | h
    · -- Case: f is locally zero in a punctured neighborhood of z
      rw [← analyticOrderAt_eq_top] at h
      tauto
    · -- Case: f is locally nonzero in a punctured neighborhood of z
      obtain ⟨t', h₁t', h₂t', h₃t'⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h)
      use Subtype.val ⁻¹' t'
      constructor
      · intro w hw
        push _ ∈ _
        by_cases h₁w : w = z
        · rwa [h₁w]
        · rw [(hf _ w.2).analyticOrderAt_eq_zero.2 ((h₁t' w hw) (Subtype.coe_ne_coe.mpr h₁w))]
          exact ENat.zero_ne_top
      · exact ⟨isOpen_induced h₂t', h₃t'⟩
  · apply isOpen_iff_forall_mem_open.mpr
    intro z hz
    conv =>
      arg 1; intro; left; right; arg 1; intro
      rw [analyticOrderAt_eq_top, eventually_nhds_iff]
    simp only [mem_ofPred_eq] at hz
    rw [analyticOrderAt_eq_top, eventually_nhds_iff] at hz
    obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz
    use Subtype.val ⁻¹' t'
    simp only [isOpen_induced h₂t', mem_preimage, h₃t', and_self, and_true]
    grind

Goal state after:
Module: Mathlib.RingTheory.Binomial

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

Tactic:
Nat.cast_sub h

Goal state after:
case neg
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
h : k ≤ n
⊢ ↑(n.descFactorial k) * (↑n - ↑k) = ↑(n.descFactorial k) * (↑n - ↑k)
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₂ : EqOn f g Uᶜ
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x | f x = g x})ᶜ ∈ 𝓝[≠] x
⊢ f =ᶠ[𝓝[≠] x] g

Tactic:
filter_upwards [h₁ x hx] with a ha

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₂ : EqOn f g Uᶜ
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x | f x = g x})ᶜ ∈ 𝓝[≠] x
a : 𝕜
ha : a ∈ (U \ {x | f x = g x})ᶜ
⊢ f a = g a
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicOn (f ∘ fun x ↦ x + c) U
y : 𝕜
hy : y ∈ U + {c}
⊢ MeromorphicAt f y

Tactic:
rw [add_singleton, mem_image] at hy
    obtain ⟨x, h₁x, h₂x⟩ := hy
    simpa [← h₂x, ← meromorphicAt_comp_add_const_iff_meromorphicAt] using h x h₁x

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

Goal state before:
pp: case neg
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : ¬UniqueDiffWithinAt ℂ s x
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

Tactic:
derivWithin_zero_of_not_uniqueDiffWithinAt h,

Goal state after:
case neg
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : ¬UniqueDiffWithinAt ℂ s x
⊢ 0 = log c * derivWithin f s x * c ^ f x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case neg
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : ¬UniqueDiffWithinAt ℂ s x
⊢ 0 = log c * derivWithin f s x * c ^ f x

Tactic:
derivWithin_zero_of_not_uniqueDiffWithinAt h,

Goal state after:
case neg
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : ¬UniqueDiffWithinAt ℂ s x
⊢ 0 = log c * 0 * c ^ f x
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (descPochhammer ℤ (k + 1)).smeval (r + 1) = (k + 1).factorial • choose r k + (descPochhammer ℤ (k + 1)).smeval r

Tactic:
Nat.factorial_succ,

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (descPochhammer ℤ (k + 1)).smeval (r + 1) = ((k + 1) * k.factorial) • choose r k + (descPochhammer ℤ (k + 1)).smeval r
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • (descPochhammer ℤ (n - k + k)).smeval r =
    n.choose k • ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k))

Tactic:
rw [add_comm, ← descPochhammer_mul, smeval_mul, smeval_comp, smeval_sub, smeval_X,
    ← C_eq_natCast, smeval_C, npow_one, npow_zero, zsmul_one, Int.cast_natCast, nsmul_eq_mul]

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

Goal state before:
pp: case e'_10
a : ℕ
z : ℂ
hz : z ≠ 0
this✝ :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)) ((z⁻¹ • 1) 0) 1
H : 1 / ‖z⁻¹ • 1‖ₑ = ‖z‖ₑ
this :
  HasFPowerSeriesOnBall (fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹)
    ((FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)).compContinuousLinearMap (z⁻¹ • 1)) 0 ‖z‖ₑ
n : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℂ (fun n ↦ (z ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) n) fun x ↦ 1) =
    (z ^ (a + 1))⁻¹ • (FormalMultilinearSeries.ofScalars ℂ (fun n ↦ ↑((a + n).choose a)) n) (⇑(z⁻¹ • 1) ∘ fun x ↦ 1)

Tactic:
simp [add_assoc, pow_add _ _ (a + 1), mul_assoc]

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

Goal state before:
pp: r : ℝ
hr : r < 1
hr' : r ≠ 0
h : DifferentiableAt ℝ (fun x ↦ x ^ r) 0
y : ℝ := deriv (fun x ↦ x ^ r) 0
x : ℝ
hx : 0 < x
⊢ x⁻¹ * x ^ r = x ^ (r - 1)

Tactic:
field_simp

Goal state after:
r : ℝ
hr : r < 1
hr' : r ≠ 0
h : DifferentiableAt ℝ (fun x ↦ x ^ r) 0
y : ℝ := deriv (fun x ↦ x ^ r) 0
x : ℝ
hx : 0 < x
⊢ x ^ r = x * x ^ (r - 1)
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: ⊢ exp 0 = 1

Tactic:
simp [exp, ← coe_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
hg : SuperpolynomialDecay l k g
z : ℕ
⊢ Tendsto (fun a ↦ k a ^ z * (f * g) a) l (𝓝 0)

Tactic:
simpa only [mul_assoc, one_mul, mul_zero, pow_zero] using! (hf z).mul (hg 0)

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
⊢ ∀ (x : X),
    ∀ ε > 0, ∃ s ∈ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}, s ⊆ closedBall x ε

Tactic:
by
    intro x ε εpos
    rcases v.nontrivial x ε εpos with ⟨s, hs, h's⟩
    exact ⟨s, mem_union_left _ hs, h's⟩

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

Goal state before:
pp: α : Type u_1
u : α → ℕ → EReal
s : Set α
hs : s.Finite
this : linearGrowthSupBotHom (hs.toFinset.sup u) = hs.toFinset.sup (⇑linearGrowthSupBotHom ∘ u)
⊢ linearGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, linearGrowthSup (u x)

Tactic:
simpa only [linearGrowthSupBotHom, SupBotHom.coe_mk, SupHom.coe_mk, Finset.sup_eq_iSup,
    hs.mem_toFinset, comp_apply]

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

Goal state before:
pp: case inr
u : ℕ → EReal
h : Monotone u
m : ℕ
hm : ¬u m = ⊥ m
m_n : ∀ᶠ (n : ℕ) in atTop, u m ≤ u n
hm' : u m ≠ ⊤
⊢ 0 ≤ linearGrowthInf u

Tactic:
· rw [← linearGrowthInf_const hm hm']
    exact linearGrowthInf_eventually_monotone m_n

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hs₀ : ¬μ s = 0
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]

Tactic:
refine
      ⟨μ s / (μ s + μ t), μ t / (μ s + μ t), zero_le, zero_le, ?_, (laverage_union hd ht).symm⟩
    rw [← ENNReal.add_div,
      ENNReal.div_self (add_eq_zero.not.2 fun h => hs₀ h.1) (add_ne_top.2 ⟨hsμ, htμ⟩)]

Goal state after: