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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.snd.β U).hom ▷ Y₁.fst ≫ (U ⊗ X.fst) ◁ f.f) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    ((α_ X.fst Y₁.fst U).hom ≫
        X.fst ◁ (Y₁.snd.β U).hom ≫ (α_ X.fst U Y₁.fst).inv ≫ (X.snd.β U).hom ▷ Y₁.fst ≫ (α_ U X.fst Y₁.fst).hom) ≫
      U ◁ X.fst ◁ f.f

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ : Center C
f : X₁ ⟶ X₂
Y : Center C
U : C
⊢ f.f ▷ Y.fst ▷ U ≫
      (α_ X₂.fst Y.fst U).hom ≫
        X₂.fst ◁ (Y.snd.β U).hom ≫ (α_ X₂.fst U Y.fst).inv ≫ (X₂.snd.β U).hom ▷ Y.fst ≫ (α_ U X₂.fst Y.fst).hom =
    𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      (f.f ▷ (Y.fst ⊗ U) ≫ X₂.fst ◁ (Y.snd.β U).hom) ⊗≫ (X₂.snd.β U).hom ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ : Center C
f : X₁ ⟶ X₂
Y : Center C
U : C
⊢ 𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      (X₁.fst ◁ (Y.snd.β U).hom ≫ f.f ▷ (U ⊗ Y.fst)) ⊗≫ (X₂.snd.β U).hom ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst) =
    𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X₁.fst ◁ (Y.snd.β U).hom ⊗≫ (f.f ▷ U ≫ (X₂.snd.β U).hom) ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ : Center C
f : X₁ ⟶ X₂
Y : Center C
U : C
⊢ 𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X₁.fst ◁ (Y.snd.β U).hom ⊗≫ ((X₁.snd.β U).hom ≫ U ◁ f.f) ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst) =
    ((α_ X₁.fst Y.fst U).hom ≫
        X₁.fst ◁ (Y.snd.β U).hom ≫ (α_ X₁.fst U Y.fst).inv ≫ (X₁.snd.β U).hom ▷ Y.fst ≫ (α_ U X₁.fst Y.fst).hom) ≫
      U ◁ f.f ▷ Y.fst

Tactic:
monoidal

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : generators.multiplicativeClosure ≤ P
⊢ P f

Tactic:
rw [multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this
    rw [this]
    apply MorphismProperty.top_apply

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: case of.inl
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 2)
⊢ P (δ i)

Tactic:
simpa using! (comp_δ (𝟙 _) i id)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case right
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
L₁ : List ℕ
h₁' : mk (m + 1) = mk (m + 1)
hL₁ : IsAdmissible (m + 1) L₁
hg : degeneracies.multiplicativeClosure (standardσ L₁ ⋯)
⊢ standardσ L₁ ⋯ ≫ σ k = standardσ (simplicialInsert (↑k) L₁) ⋯

Tactic:
have := standardσ (m₁ := m + 1 + L₁.length) [] (by grind) ≫=
      (standardσ_simplicialInsert L₁ hL₁ k k.prop _ rfl).symm

Goal state after:
case right
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
L₁ : List ℕ
h₁' : mk (m + 1) = mk (m + 1)
hL₁ : IsAdmissible (m + 1) L₁
hg : degeneracies.multiplicativeClosure (standardσ L₁ ⋯)
this :
  standardσ [] ⋯ ≫ standardσ L₁ ⋯ ≫ σ (Fin.ofNat (m + 1) ↑k) = standardσ [] ⋯ ≫ standardσ (simplicialInsert (↑k) L₁) ⋯
⊢ standardσ L₁ ⋯ ≫ σ k = standardσ (simplicialInsert (↑k) L₁) ⋯
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
⊢ ↑((ConcreteCategory.hom f) i) = ↑((ConcreteCategory.hom g) i)

Tactic:
let j : Fin ((x.len + 1) + (y.len + 1)) := i.cast (Nat.succ_add x.len (y.len + 1)).symm

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
⊢ ↑((ConcreteCategory.hom f) i) = ↑((ConcreteCategory.hom g) i)
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i : SimplicialThickening J
⊢ eId SSet i ≫ nerveMap (functorMap f i i) = eId SSet { as := f i.as }

Tactic:
ext
    simp only [eId, EnrichedCategory.id]
    exact Functor.ext (by cat_disch)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg.left
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ x ≤ i.predAbove x.castSucc

pp: case neg.right
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ ∀ i_1 < x.castSucc, i.predAbove i_1 < x

Tactic:
· simp only [i.predAbove_of_le_castSucc x.castSucc (by simpa),
          Fin.castPred_castSucc, le_refl]

Goal state after:
case neg.right
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ ∀ i_1 < x.castSucc, i.predAbove i_1 < x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : h.IsProper
f : h.RankFunction α
⊢ h.IsRegular

Tactic:
← isRegular_pairing_iff

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : h.IsProper
f : h.RankFunction α
⊢ h.pairing.IsRegular
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : h.IsProper
f : h.WeakRankFunction α
⊢ h.IsRegular

Tactic:
← isRegular_pairing_iff

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : h.IsProper
f : h.WeakRankFunction α
⊢ h.pairing.IsRegular
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
Y : C
⊢ h.functor.essImage Y

Tactic:
obtain ⟨X, rfl⟩ := h.objEquiv.surjective Y
    exact ⟨_, ⟨Iso.refl _⟩⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ X.ιNormalizedChainComplex x = Sigma.ι (fun x ↦ R) ⟨x, hx⟩

Tactic:
by
  dsimp [ιNormalizedChainComplex, ιChainComplex]
  rw [← cancel_mono ((X.fromNormalizedChainComplex R).f n), Category.assoc,
    toNormalizedChainComplex_f_fromNormalizedChainComplex_f]
  simp [fromNormalizedChainComplex, SimplicialObject.Splitting.fromNondegComplex_f]

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 : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop
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₁ : ∀ (a : ℕ), r₁ ≤ a → 2 ≤ (v i) (c a)
rₙ : (j : ι) → j ≠ i → ℕ
hrₙ : ∀ (j : ι) (hj : j ≠ i) (b : ℕ), rₙ j hj ≤ b → (v j) (c b) ∈ Set.Iio 1
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1

Tactic:
have := Fintype.ofFinite ι

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 : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop
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₁ : ∀ (a : ℕ), r₁ ≤ a → 2 ≤ (v i) (c a)
rₙ : (j : ι) → j ≠ i → ℕ
hrₙ : ∀ (j : ι) (hj : j ≠ i) (b : ℕ), rₙ j hj ≤ b → (v j) (c b) ∈ Set.Iio 1
this : Fintype ι
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1
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
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
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1

Tactic:
have := Fintype.ofFinite ι

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)
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 ι
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1
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
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
⊢ ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1

Tactic:
have := Fintype.ofFinite ι

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
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
⊢ ∀ (i : ι), ∃ 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)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
z : E
hz : z ∈ closedBall b ε
hgz : g z ∈ closedBall b ε
v : E := f'symm.toFun (y - f z)
⊢ ‖f (z + v) - f z - f' v + f' v - (y - f z)‖ = ‖f (z + v) - f z - f' (z + v - z)‖

Tactic:
simp only [v, ContinuousLinearMap.NonlinearRightInverse.right_inv, add_sub_cancel_left,
          sub_add_cancel]

Goal state after:
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)
⊢ DenseRange ⇑(algebraMap F ((i : ι) → WithAbs (v i)))

Tactic:
have := Fintype.ofFinite ι

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 ι
⊢ DenseRange ⇑(algebraMap F ((i : ι) → WithAbs (v i)))
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
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
⊢ ↑(n + 1) ≤ analyticOrderAt f z₀ ↔ ∀ i < n + 1, iteratedDeriv i f z₀ = 0

Tactic:
have : analyticOrderAt (deriv f) z₀ + 1 = analyticOrderAt f z₀ := by
      simpa [hfz] using hf.analyticOrderAt_deriv_add_one

Goal state after:
case pos
𝕜 : 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
this : analyticOrderAt (deriv f) z₀ + 1 = analyticOrderAt f z₀
⊢ ↑(n + 1) ≤ analyticOrderAt f z₀ ↔ ∀ i < n + 1, iteratedDeriv i f z₀ = 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case refine_2
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _proof_11 }))) x₁).obj 0 =
    ((ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge).obj 1

Tactic:
simp only [← f.tgt_eq, NatTrans.naturality_apply]

Goal state after:
case refine_2
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ ((ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 0 Edge._proof_1 Edge._proof_3).op))
          ((ConcreteCategory.hom (φ.app (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) f.edge)).obj
      0 =
    ((ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge).obj 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
z : E
fz : f z ≠ 0
⊢ f z ^ g z = cexp (log (f z) * g z)

Tactic:
simp only [fz, cpow_def, if_false]

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

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n : ℕ
⊢ ((ordinaryHypergeometricSeries 𝔸 a b c n) fun x ↦ 0) = Pi.single 0 1 n

Tactic:
by
  rw [ordinaryHypergeometricSeries, ofScalars_apply_eq, ordinaryHypergeometricCoefficient]
  cases n <;> 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 δ
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 = fderiv ℝ f z

Tactic:
have op : IsOpen (B ∩ s) := isOpen_ball.inter s_open

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'‖ < ε
op : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s)
⊢ fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: x✝ : ℝ
⊢ -(sin x✝ / cos x✝) = -tan x✝

Tactic:
Real.tan_eq_sin_div_cos

Goal state after:
x✝ : ℝ
⊢ -(sin x✝ / cos x✝) = -(sin x✝ / cos x✝)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
f' g' : StrongDual ℂ E
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
h0 : f x ∈ slitPlane
⊢ HasFDerivWithinAt (fun x ↦ f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') s x

Tactic:
convert!
    (@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp_hasFDerivWithinAt x (hf.prodMk hg)

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

Goal state before:
pp: f : ℂ → ℂ
x : ℂ
hf : DifferentiableAt ℂ f x
c : ℂ
⊢ deriv (fun x ↦ c ^ f x) x = log c * deriv f x * c ^ f x

Tactic:
by
  rw [← derivWithin_univ, derivWithin_const_cpow, derivWithin_univ]
  rwa [differentiableWithinAt_univ]

Goal state after:
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).smeval r = n.factorial • (choose r k * choose (r - ↑k) (n - k))

Tactic:
← Nat.choose_mul_factorial_mul_factorial hkn,

Goal state after:
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).smeval r =
    (n.choose k * k.factorial * (n - k).factorial) • (choose r k * choose (r - ↑k) (n - k))
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
y : ℝ
hne : y ≠ x
⊢ HasDerivAt f (g y) y

Tactic:
· exact f_diff y hne

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  (descPochhammer ℤ k).smeval (r + s) =
    ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
ij : ℕ × ℕ
hij : ij ∈ antidiagonal k
hdx : (descPochhammer ℤ ij.1).smeval r * (X - ↑ij.2).smeval s = (X - ↑ij.2).smeval s * (descPochhammer ℤ ij.1).smeval r
⊢ (r + s - k • 1) * (↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)) =
    ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * ((X - ↑ij.2).smeval s * (descPochhammer ℤ ij.2).smeval s)) +
      ↑(k.choose ij.2) * ((X - ↑ij.1).smeval r * (descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)

Tactic:
← mul_assoc ((descPochhammer ℤ ij.1).smeval r),

Goal state after:
case succ
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  (descPochhammer ℤ k).smeval (r + s) =
    ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
ij : ℕ × ℕ
hij : ij ∈ antidiagonal k
hdx : (descPochhammer ℤ ij.1).smeval r * (X - ↑ij.2).smeval s = (X - ↑ij.2).smeval s * (descPochhammer ℤ ij.1).smeval r
⊢ (r + s - k • 1) * (↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)) =
    ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (X - ↑ij.2).smeval s * (descPochhammer ℤ ij.2).smeval s) +
      ↑(k.choose ij.2) * ((X - ↑ij.1).smeval r * (descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: c : ℂ
⊢ (deriv fun x ↦ ↑x ^ c) =O[atTop] fun x ↦ x ^ (c.re - 1)

Tactic:
obtain rfl | hc := eq_or_ne c 0

Goal state after:
case inl
⊢ (deriv fun x ↦ ↑x ^ 0) =O[atTop] fun x ↦ x ^ (re 0 - 1)

case inr
c : ℂ
hc : c ≠ 0
⊢ (deriv fun x ↦ ↑x ^ c) =O[atTop] fun x ↦ x ^ (c.re - 1)
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
⊢ expGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ (b * ↑n).exp

Tactic:
by
  rw [expGrowthInf, liminf_le_iff']
  refine forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)
  rw [div_le_iff_le_mul (by norm_cast) (natCast_ne_top n), ← log_exp (n * b), mul_comm _ b]
  exact logOrderIso.le_iff_le

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

Goal state before:
pp: α : 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
hf : SuperpolynomialDecay l k f
z : ℤ
⊢ SuperpolynomialDecay l k fun a ↦ k a ^ z * f a

Tactic:
rw [superpolynomialDecay_iff_zpow_tendsto_zero _ hk] at hf ⊢

Goal state after:
α : 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
hf : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ ∀ (z_1 : ℤ), Tendsto (fun a ↦ k a ^ z_1 * (k a ^ z * f a)) l (𝓝 0)