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

Goal state before:
pp: V : Truncated 2
x y : V.HomotopyCategory
f : x ⟶ y
x✝ : ⊤ f
⊢ (morphismPropertyHomMk V).multiplicativeClosure f

Tactic:
obtain ⟨f, rfl⟩ := (quotientFunctor _).map_surjective f

Goal state after:
V : Truncated 2
x y : V.HomotopyCategory
f : x.as ⟶ y.as
x✝ : ⊤ ((quotientFunctor V).map f)
⊢ (morphismPropertyHomMk V).multiplicativeClosure ((quotientFunctor V).map f)
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
e : X ≅ Y
⊢ r.degHom e.hom = r.deg Y

Tactic:
refine le_antisymm ?_ ?_
    · simpa using r.degHom_comp_le_right e.hom (𝟙 Y)
    · simpa using r.degHom_comp_le_right e.inv e.hom

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

Goal state before:
pp: case of.σ
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
⊢ ∃ L m_1 b,
    ∃ (h₁ : mk m_1 = mk m) (h₂ : mk (m + 1) = mk (m_1 + b)) (h : L.length = b), IsAdmissible m_1 L ∧ σ k = standardσ L ⋯

Tactic:
use [k.val], m, 1, rfl, rfl, rfl, IsAdmissible.singleton k.is_le

Goal state after:
case right
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
⊢ σ k = standardσ [↑k] ⋯
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.inl.right
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
j : Fin (n + 1)
hj : j < x
⊢ i.succAbove j < x.castSucc

Tactic:
Fin.succAbove_of_castSucc_lt _ _ (lt_of_lt_of_le (by simpa) hx),

Goal state after:
case pos.inl.right
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
j : Fin (n + 1)
hj : j < x
⊢ j.castSucc < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
⊢ ∃! i, (ConcreteCategory.hom (SimplicialObject.δ X.op i)) (opObjEquiv.symm y) = opObjEquiv.symm x

Tactic:
refine ⟨(hxy.index rfl).rev, by simpa using hxy.δ_index rfl, fun i hi ↦ ?_⟩

Goal state after:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
i : Fin (d + 2)
hi : (fun i ↦ (ConcreteCategory.hom (SimplicialObject.δ X.op i)) (opObjEquiv.symm y) = opObjEquiv.symm x) i
⊢ i = (hxy.index ⋯).rev
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
g : h.pairing.RankFunction α
x✝ y✝ : h.ι
hxy : h.AncestralRel x✝ y✝
⊢ g.rank (h.equivII x✝) < g.rank (h.equivII y✝)

Tactic:
ancestralRel_iff

Goal state after:
X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
g : h.pairing.RankFunction α
x✝ y✝ : h.ι
hxy : h.pairing.AncestralRel (h.equivII x✝) (h.equivII y✝)
⊢ g.rank (h.equivII x✝) < g.rank (h.equivII y✝)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
g : h.pairing.WeakRankFunction α
x✝ y✝ : h.ι
hxy : h.AncestralRel x✝ y✝
⊢ h.dim x✝ = h.dim y✝ → g.rank (h.equivII x✝) < g.rank (h.equivII y✝)

Tactic:
ancestralRel_iff

Goal state after:
X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
g : h.pairing.WeakRankFunction α
x✝ y✝ : h.ι
hxy : h.pairing.AncestralRel (h.equivII x✝) (h.equivII y✝)
⊢ h.dim x✝ = h.dim y✝ → g.rank (h.equivII x✝) < g.rank (h.equivII y✝)
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
⊢ ⨆ j, Subcomplex.range (c.ι.app j) = ⊤

Tactic:
by
  ext n x
  simp only [Subfunctor.iSup_obj, Subfunctor.range_obj, Set.mem_iUnion, Set.mem_range,
    Subfunctor.top_obj, Set.top_eq_univ, Set.mem_univ, iff_true]
  exact Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves ((evaluation _ _).obj n) hc) x

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
⊢ (f.filtration j).preimage c.map = c.horn

Tactic:
by
  apply le_antisymm
  · simpa only [subcomplex_le_horn_iff, ← Subcomplex.image_le_iff,
      Cell.image_face_index_compl] using c.subcomplex_not_le_filtration
  · rw [← Subcomplex.image_le_iff, N.subcomplex_le_iff]
    intro s hs
    cases s using N.cases A with
    | mem s hs' => exact hs'.trans (by simp)
    | notMem s =>
      obtain ⟨t, ht⟩ := P.exists_or s
      rw [← c.rank_s]
      refine le_trans ?_ (f.subcomplex_le_filtration ⟨t, rfl⟩ (f.lt ?_))
      · obtain rfl | rfl := ht
        · exact P.le t
        · simp
      · replace hs : t.val.subcomplex ≤ c.horn.image c.map := by
          obtain rfl | rfl := ht
          · exact hs
          · refine le_trans ?_ hs
            rw [← S.le_def]
            exact (P.isUniquelyCodimOneFace t).le
        refine ⟨?_, ?_⟩
        · rintro rfl
          exact c.subcomplex_not_le_image_horn hs
        · rw [Subcomplex.N.lt_iff, SSet.N.lt_iff]
          exact lt_of_le_of_lt hs (c.image_horn_lt_subcomplex)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: A B X Y : SSet
i : A ⟶ B
hi : innerHornInclusions i
f : X ⟶ Y
hf : RelativeCellComplex (fun x ↦ innerHornInclusions.homFamily) f
⊢ Limits.PreservesColimit hf.F (coyoneda.obj (Opposite.op A))

Tactic:
have : IsFinitelyPresentable.{u} A := by
      simp only [innerHornInclusions_eq_iSup, iSup_iff] at hi
      obtain ⟨n, ⟨i⟩⟩ := hi
      infer_instance
    infer_instance

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

Tactic:
α

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: m : ℕ
k : Fin (m + 1)
n : ℕ
t : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
ht : IsType₂ t
s : Type₁ k n
hst : s.δ = t
d : ℕ
hd : t.dim = d
⊢ ht.type₁ hd = s

Tactic:
subst hst hd
  rw [Type₁.ext_iff, Subcomplex.N.ext_iff, N.ext_iff]
  rw [← s.x.toS.cast_eq_self s.hd, S.ext_iff']
  refine ⟨rfl, objEquiv.injective ?_⟩
  ext i : 2
  change φ s.δ rfl i = _
  by_cases! hi : i = s.index.castSucc
  · subst hi
    conv_lhs => rw [← s.isIndex.min_δ]
    dsimp
    rw [φ_castSucc]
    ext : 1
    · simp [← s.isIndex.simplex_fst_castSucc]
      rfl
    · change (s.x.cast s.hd).simplex.2
        (s.index.castSucc.succAbove (min s.δ rfl)) = _
      rw [s.isIndex.min_δ, Fin.succAbove_castSucc_self]
      exact s.isIndex.simplex_snd_succ -- defeq abuse
  · rw [← s.isIndex.min_δ] at hi
    rw [φ_of_ne _ rfl _ hi]
    change objEquiv (s.x.cast s.hd).simplex
      (s.index.castSucc.succAbove ((min s.δ rfl).predAbove i)) = _
    congr 1
    rw [← s.isIndex.min_δ]
    exact Fin.succAbove_predAbove hi

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

Goal state before:
pp: case fst
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
⊢ ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  ((ConcreteCategory.hom (δ Δ[n] (Fin.last (n + 1))))
                    (stdSimplex.objEquiv.symm (SimplexCategory.σ (Fin.last n))))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] (Fin.last (n + 1)))) (stdSimplex.objMk₁ (Fin.last n).castSucc.succ)).1 =
    ((ConcreteCategory.hom (ι₀.app (op ⦋n⦌))) x).1

pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
k : Fin (n + 1)
⊢ ↑(((ConcreteCategory.hom
                (X.map
                  (stdSimplex.objEquiv
                      ((ConcreteCategory.hom (δ Δ[n] (Fin.last (n + 1))))
                        (stdSimplex.objEquiv.symm (SimplexCategory.σ (Fin.last n))))).op))
              x,
            (ConcreteCategory.hom (δ Δ[1] (Fin.last (n + 1)))) (stdSimplex.objMk₁ (Fin.last n).castSucc.succ)).2
        k) =
    ↑(((ConcreteCategory.hom (ι₀.app (op ⦋n⦌))) x).2 k)

Tactic:
· simp [dsimp% SimplexCategory.δ_comp_σ_succ (i := Fin.last n)]

Goal state after:
case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
k : Fin (n + 1)
⊢ ↑(((ConcreteCategory.hom
                (X.map
                  (stdSimplex.objEquiv
                      ((ConcreteCategory.hom (δ Δ[n] (Fin.last (n + 1))))
                        (stdSimplex.objEquiv.symm (SimplexCategory.σ (Fin.last n))))).op))
              x,
            (ConcreteCategory.hom (δ Δ[1] (Fin.last (n + 1)))) (stdSimplex.objMk₁ (Fin.last n).castSucc.succ)).2
        k) =
    ↑(((ConcreteCategory.hom (ι₀.app (op ⦋n⦌))) x).2 k)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Splitting

Goal state before:
pp: case refine_1
X : SSet
x✝ : SimplexCategoryᵒᵖ
n : ℕ
x :
  (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
        (Opposite.op ⦋n⦌)).cofanTypes.pt
⊢ ∃ i y,
    (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
              (Opposite.op ⦋n⦌)).cofanTypes.inj
        i y =
      x

Tactic:
obtain ⟨m, f, _, y, rfl⟩ := X.exists_nonDegenerate x
      exact ⟨.mk f, y, rfl⟩

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

Goal state before:
pp: case fst
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
x : X _⦋n⦌
⊢ ((ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n + 1 + 1⦌)))
          ((ConcreteCategory.hom (σ Δ[n] i.castSucc)) (stdSimplex.objEquiv.symm (SimplexCategory.σ j))),
        (ConcreteCategory.hom (σ Δ[1] i.castSucc)) (stdSimplex.objMk₁ j.castSucc.succ)).1 =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (σ X i)) x)).app (op ⦋n + 1 + 1⦌)))
          (stdSimplex.objEquiv.symm (SimplexCategory.σ j.succ)),
        stdSimplex.objMk₁ j.castSucc.succ.succ).1

Tactic:
simp [SimplexCategory.σ_comp_σ hij, SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}]

Goal state after:
case fst
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (X.map (SimplexCategory.σ j.succ).op))
      ((ConcreteCategory.hom (X.map (SimplexCategory.σ i).op)) x) =
    (ConcreteCategory.hom (X.map (SimplexCategory.σ j.succ).op)) ((ConcreteCategory.hom (σ X i)) x)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Field R
inst✝⁴ : Semifield S
inst✝³ : LinearOrder S
v w : AbsoluteValue R S
inst✝² : IsStrictOrderedRing S
inst✝¹ : Archimedean S
inst✝ : ExistsAddOfLE S
hv✝ : v.IsNontrivial
h : ∀ (x : R), v x < 1 → w x < 1
a : R
ha₀ : a ≠ 0
hw : w a < 1
x₀ : R
hx₀ : x₀ ≠ 0 ∧ v x₀ < 1
n : ℕ
hv : 1 ≤ v a
⊢ v x₀ < v a ^ n

Tactic:
exact lt_of_lt_of_le hx₀.2 <| one_le_pow₀ hv

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

Goal state before:
pp: case coe
𝕜 : 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 a✝ : ℕ
⊢ ↑a✝ = ↑m ↔ ↑m ≤ ↑a✝ ∧ ¬↑m + 1 ≤ ↑a✝

Tactic:
| coe _ =>

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 δ
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
⊢ u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ∧
    v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
simpa [closure_prod_eq] using closure_mono this uv_in

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:
← mul_assoc,

Goal state after:
n : ℕ
⊢ (-1 + -↑n) * (-1) ^ n * ↑n.factorial = (-1) ^ (n + 1) * ↑(n + 1).factorial
Module: Mathlib.RingTheory.Binomial

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

Tactic:
← mul_assoc,

Goal state after:
n : ℕ
⊢ (-1) ^ n * -1 * (↑n + 1) * ↑n.factorial = (-1) ^ (n + 1) * ↑(n + 1).factorial
Module: Mathlib.RingTheory.Binomial

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

Tactic:
← mul_assoc,

Goal state after:
n : ℕ
⊢ (-1) ^ n * -1 * (↑n + 1) * ↑n.factorial = (-1) ^ n * -1 * ↑n.succ * ↑n.factorial
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✝ : ℕ
| a ≠ ↑k✝

Tactic:
ne_comm

Goal state after:
𝕂 : Type v
inst✝² : RCLike 𝕂
𝔸 : Type u
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ ↑k
k✝ : ℕ
| ↑k✝ ≠ a
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_12
p : ℝ × ℝ
hp : p.1 < 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedCommRing.toCommRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ (NormedAlgebra.toNormedSpace ℝ).toModule
⊢ (p.2 * (p.1 ^ p.2 / p.1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    (rexp (log p.1 * p.2) * (-sin (p.2 * π) * π) + cos (p.2 * π) * (rexp (log p.1 * p.2) * log p.1)) •
        ContinuousLinearMap.snd ℝ ℝ ℝ +
      (cos (p.2 * π) * (rexp (log p.1 * p.2) * (p.2 * p.1⁻¹))) • ContinuousLinearMap.fst ℝ ℝ ℝ

Tactic:
← mul_assoc,

Goal state after:
case e'_12
p : ℝ × ℝ
hp : p.1 < 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedCommRing.toCommRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ (NormedAlgebra.toNormedSpace ℝ).toModule
⊢ (p.2 * (p.1 ^ p.2 / p.1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    (rexp (log p.1 * p.2) * -sin (p.2 * π) * π + cos (p.2 * π) * rexp (log p.1 * p.2) * log p.1) •
        ContinuousLinearMap.snd ℝ ℝ ℝ +
      (cos (p.2 * π) * rexp (log p.1 * p.2) * p.2 * p.1⁻¹) • ContinuousLinearMap.fst ℝ ℝ ℝ
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
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : p n = 0
⊢ iteratedFDerivWithin 𝕜 n f s x = 0

Tactic:
by
  have : iteratedFDerivWithin 𝕜 n f s x = p.iteratedFDerivSeries n 0 (fun _ ↦ 0) :=
    ((h.iteratedFDerivWithin h' n hu hx).coeff_zero _).symm
  rw [this, p.iteratedFDerivSeries_eq_zero (p.congr_zero (Nat.zero_add n).symm hn), zero_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
s : Set E
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p✝ : A[X]
p : ℕ
i : A
hp : AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) (C i * X ^ p)) s z
x✝ : E
⊢ (aeval (f x✝)) (C i) * ((aeval (f x✝)) (X ^ p) * (aeval (f x✝)) X) =
    (aeval (f x✝)) (C i) * (aeval (f x✝)) (X ^ p) * f x✝

Tactic:
← mul_assoc,

Goal state after:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
s : Set E
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p✝ : A[X]
p : ℕ
i : A
hp : AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) (C i * X ^ p)) s z
x✝ : E
⊢ (aeval (f x✝)) (C i) * (aeval (f x✝)) (X ^ p) * (aeval (f x✝)) X =
    (aeval (f x✝)) (C i) * (aeval (f x✝)) (X ^ p) * f x✝
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
n : ℕ
f : E [×n]→L[𝕜] F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i ↦ ContinuousLinearMap.id 𝕜 E
⊢ (iteratedFDeriv 𝕜 n (fun x ↦ f fun x_1 ↦ x) x) v = ∑ i, f fun i_1 ↦ v (((Equiv.inv (Perm (Fin n))) i) i_1)

Tactic:
change iteratedFDeriv 𝕜 n (f ∘ g) x v = _

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
n : ℕ
f : E [×n]→L[𝕜] F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i ↦ ContinuousLinearMap.id 𝕜 E
⊢ (iteratedFDeriv 𝕜 n (⇑f ∘ ⇑g) x) v = ∑ i, f fun i_1 ↦ v (((Equiv.inv (Perm (Fin n))) i) i_1)
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: a : ℝ
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℝ fun n ↦ Ring.choose (a + ↑n - 1) n) 0 1

Tactic:
by
  have := (Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero a).restrictScalars (𝕜 := ℝ)
  rw [← Complex.ofRealCLM.map_zero] at this
  convert (Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap).congr ?_
  · ext n
    simp only [ContinuousLinearMap.compFormalMultilinearSeries_apply,
      ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply,
      FormalMultilinearSeries.compContinuousLinearMap_apply]
    simp
    norm_cast
  · simp
  · intro x hx
    have : |x| < 1 := by simpa [enorm_eq_nnnorm] using! hx
    have : 0 ≤ 1 - x := by grind
    simp [-Complex.inv_re, ← Complex.ofReal_one, ← Complex.ofReal_sub, ← Complex.ofReal_cpow this]

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
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
h' : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
⊢ (iteratedFDeriv 𝕜 n f x) v = ∑ σ, (p n) fun i ↦ v (σ i)

Tactic:
simp only [← iteratedFDerivWithin_univ, ← hasFPowerSeriesWithinOnBall_univ] at h ⊢

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
x : E
r : ℝ≥0∞
h' : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
h : HasFPowerSeriesWithinOnBall f p univ x r
⊢ (iteratedFDerivWithin 𝕜 n f univ x) v = ∑ σ, (p n) fun i ↦ v (σ i)
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
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
n : ℕ
v : Fin n → E
⊢ (iteratedFDeriv 𝕜 n f x) v = ∑ σ, (p n) fun i ↦ v (σ i)

Tactic:
simp only [← iteratedFDerivWithin_univ, ← hasFPowerSeriesWithinOnBall_univ] at h ⊢

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
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
n : ℕ
v : Fin n → E
h : HasFPowerSeriesWithinOnBall f p univ x r
⊢ (iteratedFDerivWithin 𝕜 n f univ x) v = ∑ σ, (p n) fun i ↦ v (σ i)
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case coe
y : ℝ
⊢ ∃ a, a.log = ↑y

Tactic:
| coe y =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : EReal
n : ℕ
⊢ (↑n * x).exp = x.exp ^ n

Tactic:
by
  simp_rw [← log_eq_iff, log_pow, log_exp]

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
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun a ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a ↦ |k a ^ (z + 1) * f a|) l, (fun x1 x2 ↦ x1 ≤ x2) x m
h1 : Tendsto (fun x ↦ 0) l (𝓝 0)
h2 : Tendsto (fun a ↦ |(k a)⁻¹| * m) l (𝓝 0)
x : α
hk0 : k x ≠ 0
hx : (fun x1 x2 ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| = |(k x)⁻¹ * (k x ^ (z + 1) * f x)|

Tactic:
← mul_assoc,

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
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun a ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a ↦ |k a ^ (z + 1) * f a|) l, (fun x1 x2 ↦ x1 ≤ x2) x m
h1 : Tendsto (fun x ↦ 0) l (𝓝 0)
h2 : Tendsto (fun a ↦ |(k a)⁻¹| * m) l (𝓝 0)
x : α
hk0 : k x ≠ 0
hx : (fun x1 x2 ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| = |(k x)⁻¹ * k x ^ (z + 1) * f x|