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

Goal state before:
pp: case inr.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
hi✝ : i ≤ j
c : f.Cell i
hx : x ∈ (↑(P.p c.s)).subcomplex.obj d
hi : i < j
⊢ (x ∈ A.obj d ∨ ∃ i < j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b j).app d)) y) = x

pp: case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
c : f.Cell i
hx : x ∈ (↑(P.p c.s)).subcomplex.obj d
hi : i ≤ i
⊢ (x ∈ A.obj d ∨ ∃ i_1 < i, ∃ i, x ∈ (↑(P.p i.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b i).app d)) y) = x

Tactic:
· exact Or.inl (Or.inr ⟨i, hi, c, hx⟩)

Goal state after:
case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
c : f.Cell i
hx : x ∈ (↑(P.p c.s)).subcomplex.obj d
hi : i ≤ i
⊢ (x ∈ A.obj d ∨ ∃ i_1 < i, ∃ i, x ∈ (↑(P.p i.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b i).app d)) y) = x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
left✝ : Mono f
P : (Subcomplex.range f).Pairing
h✝ : P.IsRegular
⊢ anodyneExtensions f

Tactic:
← Subfunctor.toRange_ι f

Goal state after:
X Y : SSet
f : X ⟶ Y
left✝ : Mono f
P : (Subcomplex.range f).Pairing
h✝ : P.IsRegular
⊢ anodyneExtensions (Subfunctor.toRange f ≫ (Subfunctor.range f).ι)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
left✝ : Mono f
P : (Subcomplex.range f).Pairing
w✝ : P.IsRegular
h✝ : P.IsInner
⊢ innerAnodyneExtensions f

Tactic:
← Subfunctor.toRange_ι f

Goal state after:
X Y : SSet
f : X ⟶ Y
left✝ : Mono f
P : (Subcomplex.range f).Pairing
w✝ : P.IsRegular
h✝ : P.IsInner
⊢ innerAnodyneExtensions (Subfunctor.toRange f ≫ (Subfunctor.range f).ι)
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
⊢ isCardinalPresentable C κ ≤ P.colimitsCardinalClosure κ

Tactic:
have := hS₁.isDense_colimitsCardinalClosure_ι hS₂

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
⊢ isCardinalPresentable C κ ≤ P.colimitsCardinalClosure κ
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasColimitsOfSize.{w, w, v, u} C
inst✝ : LocallySmall.{w, v, u} C
x✝ : ∃ P, ∃ (_ : ObjectProperty.Small.{w, v, u} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
P : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
⊢ IsCardinalLocallyPresentable C κ

Tactic:
have := hS₁.isDense_colimitsCardinalClosure_ι hS₂

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasColimitsOfSize.{w, w, v, u} C
inst✝ : LocallySmall.{w, v, u} C
x✝ : ∃ P, ∃ (_ : ObjectProperty.Small.{w, v, u} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
P : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
⊢ IsCardinalLocallyPresentable C κ
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: 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 φ)

Tactic:
intro h

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₃
h : ∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty (Arrow.LiftStruct φ)
⊢ ∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty (Arrow.LiftStruct φ)
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: 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 φ)

Tactic:
intro h

Goal state after:
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₃
h : ∀ (φ : 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 inl.inr.refine_3
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
⊢ (objEquiv (x.cast hd).simplex) i.castSucc ≠ (k.castSucc, (x.cast hd).simplex.2 (min x hd))

Tactic:
intro h

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x y : WalkingIso
x✝ : x ⟶ y
⊢ WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y y

Tactic:
induction x <;> induction y

Goal state after:
case zero.zero
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x✝ : zero ⟶ zero
⊢ WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y zero

case zero.one
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x✝ : zero ⟶ one
⊢ WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y one

case one.zero
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x✝ : one ⟶ zero
⊢ WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y zero

case one.one
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x✝ : one ⟶ one
⊢ WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y one
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst✝ : Y.HasDimensionLT n
⊢ Subcomplex.range φ ≠ ⊤

Tactic:
intro h

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst✝ : Y.HasDimensionLT n
h : Subcomplex.range φ = ⊤
⊢ False
Module: Mathlib.Analysis.Normed.Field.WithAbs

Goal state before:
pp: R : Type u_1
inst✝ : Field R
v : AbsoluteValue R ℝ
a : R
ha : v a < 1
⊢ Filter.Tendsto (fun e ↦ ‖1⁻¹ + toAbs v a ^ e - 1‖) Filter.atTop (𝓝 0)

Tactic:
by simpa using! ha

Goal state after:
Module: Mathlib.Analysis.Convex.Contractible

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
h : StarConvex ℝ x s
hne : s.Nonempty
p : ↑unitInterval × ↑s
⊢ ↑p.1 • x + (1 - ↑p.1) • ↑p.2 ∈ s

Tactic:
exact h p.2.2 p.1.2.1 (sub_nonneg.2 p.1.2.2) (add_sub_cancel _ _)

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

Goal state before:
pp: 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
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1

Tactic:
choose r₁ hr₁ using Filter.eventually_atTop.1 <| Filter.Tendsto.eventually_const_lt hb hcᵢ

Goal state after:
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)
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: case inl
𝕜 : 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 : (↑f'symm.nnnorm)⁻¹ ≤ ↑c
this : dist y (f b) ≤ 0
⊢ f b = y

Tactic:
simp only [dist_le_zero] at this

Goal state after:
case inl
𝕜 : 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 : (↑f'symm.nnnorm)⁻¹ ≤ ↑c
this : y = f b
⊢ f b = y
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : ¬u = w
⊢ 1 < ((v u) (a w))⁻¹

Tactic:
refine one_lt_inv_iff₀.mpr ⟨(v u).pos_iff.mpr fun ha ↦ ?_, (hx w).2 u hw⟩

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : ¬u = w
ha : a w = 0
⊢ False
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case coe.e_a
𝕜 : 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 - f x = (z - x) ^ (s + 1) • F z
⊢ analyticOrderAt (deriv f) x = ↑s

Tactic:
simp only [sub_eq_iff_eq_add] at hfF

Goal state after:
case coe.e_a
𝕜 : 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
⊢ analyticOrderAt (deriv f) x = ↑s
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case succ.refine_2
𝕜 : 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
x✝ : (∀ k < n + 1, iteratedDeriv k f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0
hz : ∀ k < n + 1, iteratedDeriv k f z₀ = 0
hnz : iteratedDeriv (n + 1) f z₀ ≠ 0
⊢ analyticOrderAt f z₀ = ↑(n + 1)

Tactic:
exact (analyticOrderAt_deriv_eq_iff hf <| by simpa using hz 0 (by lia)).mpr <|
        IH.mpr ⟨fun j _ ↦ hz (j + 1) (by lia), hnz⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : analyticOrderAt f z₀ ≠ ⊤
hg' : analyticOrderAt g z₀ ≠ ⊤
⊢ analyticOrderNatAt (f * g) z₀ = analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀

Tactic:
by
  simp [analyticOrderNatAt, analyticOrderAt_mul, ENat.toNat_add, *]

Goal state after:
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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : ∃ g_1, AnalyticAt 𝕜 g_1 (g z₀) ∧ g_1 (g z₀) ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • g_1 z
s : ℕ
hs : ↑s = analyticOrderAt (fun x ↦ g x - g z₀) z₀
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z

Tactic:
rcases hr with ⟨F, hFa, hFne, hfF⟩

Goal state after:
case neg
𝕜 : 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 : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
hs : ↑s = analyticOrderAt (fun x ↦ g x - g z₀) z₀
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
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 δ
u v : E
u_in : (u, v).1 ∈ B ∩ s
v_in : (u, v).2 ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
h : z ∈ s → dist z x < δ → ‖fderiv ℝ f z - f'‖ < ε
⊢ ‖fderivWithin ℝ f (B ∩ s) z - f'‖ ≤ ε

Tactic:
have : fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z := by
        have op : IsOpen (B ∩ s) := isOpen_ball.inter s_open
        rw [DifferentiableAt.fderivWithin _ (op.uniqueDiffOn z z_in)]
        exact (diff z z_in).differentiableAt (IsOpen.mem_nhds op z_in)

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

Goal state before:
pp: R : Type u_1
inst✝² : AddCommMonoid R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ multichoose r 1 = r ^ 1

Tactic:
by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero 1),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_one, smeval_X, Nat.factorial_one,
    one_smul]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n : ℕ
⊢ (-1) ^ n * (-1 + -↑n) * ↑n.factorial = (-1) ^ (n + 1) * ↑(n + 1).factorial

Tactic:
show (-1 + -↑n = (-1 : ℤ) * (n + 1)) by lia,

Goal state after:
n : ℕ
⊢ (-1) ^ n * (-1 * (↑n + 1)) * ↑n.factorial = (-1) ^ (n + 1) * ↑(n + 1).factorial
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₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x | f x = g x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
⊢ f =ᶠ[𝓝[≠] x] g

Tactic:
filter_upwards [this, h₁ x hx] with a h₁a h₂a

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₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x | f x = g x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
a : 𝕜
h₁a : a ∈ U
h₂a : a ∈ (U \ {x | f x = g x})ᶜ
⊢ f a = g a
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₁ : f =ᶠ[codiscreteWithin U] g
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ MeromorphicOn g U

Tactic:
intro x hx
  apply (hf x hx).congr
  simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin,
    disjoint_principal_right] at h₁
  have : U ∈ 𝓝[≠] x := by
    apply mem_nhdsWithin.mpr
    use U, h₂, hx, Set.inter_subset_left
  filter_upwards [this, h₁ x hx] with a h₁a h₂a
  simp only [Set.mem_compl_iff, Set.mem_sdiff, Set.mem_ofPred_eq, not_and] at h₂a
  tauto

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
⊢ ?m.43 ≠ -1

Tactic:
rwa [ne_eq, sub_eq_neg_self]

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
p : FormalMultilinearSeries 𝕜 E F
k n : ℕ
h : p (n + k) = 0
⊢ p.iteratedFDerivSeries k n = 0

Tactic:
induction k generalizing n with
  | zero =>
    ext
    have : p n = 0 := p.congr_zero rfl h
    simp [FormalMultilinearSeries.iteratedFDerivSeries, this]
  | succ k ih =>
    ext
    simp only [iteratedFDerivSeries, Nat.succ_eq_add_one,
      ContinuousLinearMap.compFormalMultilinearSeries_apply,
      ContinuousLinearMap.compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe,
      LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply,
      continuousMultilinearCurryLeftEquiv_symm_apply, _root_.zero_apply,
      derivSeries_eq_zero _ (ih (p.congr_zero (Nat.succ_add_eq_add_succ _ _).symm h))]

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
⊢ insert x s ∩ Metric.eball x r = s

Tactic:
rw [Set.insert_eq_of_mem hx]

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
⊢ s ∩ Metric.eball x r = s
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a b : ℂ
⊢ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ a * ↑n + b) =
    (b - a) • FormalMultilinearSeries.ofScalars ℂ 1 + a • FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑n + 1

Tactic:
· ext; simp; ring

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

Goal state before:
pp: case e'_10
a b : ℝ
⊢ (FormalMultilinearSeries.ofScalars ℝ fun x ↦ a * ↑x + b) =
    (b - a) • FormalMultilinearSeries.ofScalars ℝ 1 + a • FormalMultilinearSeries.ofScalars ℝ fun n ↦ ↑n + 1

Tactic:
· ext; simp; ring

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : 0 ≤ z
⊢ Filter.map (fun a ↦ k a ^ z * f a) l ≤ 𝓝 0

Tactic:
lift z to ℕ using hz

Goal state after:
case pos
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℕ
⊢ Filter.map (fun a ↦ k a ^ ↑z * f a) l ≤ 𝓝 0