mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: C D : Cat
F G : ↑C ⥤ ↑D
hyp : forget.map F.toCatHom = forget.map G.toCatHom
⊢ F = G

Tactic:
cases F

Goal state after:
case mk
C D : Cat
G : ↑C ⥤ ↑D
obj✝ : ↑C → ↑D
map✝ : {X Y : ↑C} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : ↑C), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
hyp : forget.map { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.toCatHom = forget.map G.toCatHom
⊢ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } = G
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V W : ReflQuiv
F G : ↑V ⥤rq ↑W
hyp : forgetToQuiv.map F = forgetToQuiv.map G
⊢ F = G

Tactic:
cases F

Goal state after:
case mk
V W : ReflQuiv
G : ↑V ⥤rq ↑W
toPrefunctor✝ : ↑V ⥤q ↑W
map_id✝ : ∀ (X : ↑V), toPrefunctor✝.map (𝟙rq X) = 𝟙rq (toPrefunctor✝.obj X)
hyp : forgetToQuiv.map { toPrefunctor := toPrefunctor✝, map_id := map_id✝ } = forgetToQuiv.map G
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝ } = G
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ homMk (Edge.id x) = 𝟙 (mk x)

Tactic:
by
  rw [homMk, ← OneTruncation₂.reflQuiver_id, Cat.FreeRefl.homMk_id,
    CategoryTheory.Functor.map_id]
  rfl

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

Goal state before:
pp: case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
⊢ (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x

Tactic:
let α := strArrowMk₂ (mkOfLeComp (n := n) ⟨i, by omega⟩ ⟨i + k, by omega⟩
          ⟨j, by omega⟩ (by simp) (by simp only [Fin.mk_le_mk]; omega))

Goal state after:
case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
⊢ (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_σ.comp_of.succ.inr
x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
j' : Fin (n + 1)
j'' : Fin (n + 2)
h' : δ i ≫ σ j = σ j' ≫ δ j''
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m

Tactic:
obtain ⟨_, _, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' f hf
          exact ⟨_, _, m₁ ≫ δ j'', P_σ.comp_mem _ _ he he₁, P_δ.comp_mem _ _ hm₁ (P_δ.δ _),
            by simp [← reassoc_of% h₁, h']⟩

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

Goal state before:
pp: m✝ : ℕ
L✝ : List ℕ
x y : SimplexCategoryGenRel
f : x ⟶ y
hf : P_σ f
L : List ℕ
m b : ℕ
h₁ : mk m = y
h₂ : x = mk (m + b)
h : L.length = b
⊢ y.1 + L.length = x.1

Tactic:
rw [h, h₁.symm, h₂]

Goal state after:
m✝ : ℕ
L✝ : List ℕ
x y : SimplexCategoryGenRel
f : x ⟶ y
hf : P_σ f
L : List ℕ
m b : ℕ
h₁ : mk m = y
h₂ : x = mk (m + b)
h : L.length = b
⊢ (mk m).1 + b = (mk (m + b)).1
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
j i : Fin (n + 2)
h✝ : i.castSucc ≤ j.castSucc
h : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ (j.succAbove k).castSucc < i.castSucc ↔ k.castSucc < i

Tactic:
grind [Fin.succAbove]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
k : Fin (⦋n⦌.len + 1)
⊢ (j.succAbove k).castSucc < i.succ ↔ k.castSucc < i

Tactic:
grind [Fin.succAbove]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
⊢ f ≫ 𝟙 Y✝ = f

Tactic:
ext; simpa using fun h ↦ h ▸ f.right

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x : ↑P.II
d : ℕ
hd : (↑x).dim = d
inst✝ : P.IsProper
⊢ ⋯.index hd = ⋯.index hd

Tactic:
by
  rw [← (P.isUniquelyCodimOneFace x).index_of_iso e.symm hd]
  congr
  rw [P.ofIso_p e hA x]
  rfl

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsProper
x : ↑h.pairing.II
⊢ (↑x).IsUniquelyCodimOneFace (↑(h.pairing.p x)).toS

Tactic:
obtain ⟨s, rfl⟩ := h.equivII.surjective x
    simpa using h.isUniquelyCodimOneFace s

Goal state after:
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hP : P.IsStrongGenerator
X : C
A : Subobject X
hA : A ≠ ⊤
⊢ ∃ G, ∃ (_ : P G), ∃ f, ¬A.Factors f

Tactic:
by
  by_contra!
  exact hA (hP.subobject_eq_top this)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
Q : ObjectProperty C
inst✝ : Q.IsClosedUnderIsomorphisms
hQ : ∀ (J : Type w) [inst : SmallCategory J], HasCardinalLT (Arrow J) κ → Q.IsClosedUnderColimitsOfShape J
h : P ≤ Q
⊢ P.colimitsCardinalClosure κ ≤ Q

Tactic:
have (i : SmallCategoryCardinalLT κ) := hQ _ i.hasCardinalLT

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
Q : ObjectProperty C
inst✝ : Q.IsClosedUnderIsomorphisms
hQ : ∀ (J : Type w) [inst : SmallCategory J], HasCardinalLT (Arrow J) κ → Q.IsClosedUnderColimitsOfShape J
h : P ≤ Q
this : ∀ (i : SmallCategoryCardinalLT κ), Q.IsClosedUnderColimitsOfShape (SmallCategoryCardinalLT.categoryFamily κ i)
⊢ P.colimitsCardinalClosure κ ≤ Q
Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable

Goal state before:
pp: case inst
X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ ∀ (k : WalkingParallelPair),
    IsCardinalPresentable ((parallelPair (q ≫ pullback.fst p p) (q ≫ pullback.snd p p)).obj k) Cardinal.aleph0

Tactic:
rintro (_ | _) <;> dsimp <;> infer_instance

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsRegular
hP : IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
f : ℕ → ↑P.op.II
hf : ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ P.AncestralRel ((fun n ↦ ⟨N.opEquiv ↑(f n), ⋯⟩) (n + 1)) ((fun n ↦ ⟨N.opEquiv ↑(f n), ⋯⟩) n)

Tactic:
simpa [← P.op_ancestralRel_iff] using hf n

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

Goal state before:
pp: X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : InnerFibration p
sq₁₃ : internalHom.PullbackObjObj i p
⊢ innerFibrations sq₁₃.π

Tactic:
intro _ _ _ ⟨k, h0, hn⟩

Goal state after:
X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : InnerFibration p
sq₁₃ : internalHom.PullbackObjObj i p
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
n✝ : ℕ
k : Fin (n✝ + 3)
h0 : 0 < k
hn : k < Fin.last (n✝ + 2)
⊢ HasLiftingProperty Λ[n✝ + 2, k].ι sq₁₃.π
Module: Mathlib.AlgebraicTopology.SingularHomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
F : TopCat ⥤ C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ Sigma.ι (fun x ↦ ((evaluation TopCat C).obj (SimplexCategory.toTop.{w} ^⦋n⦌)).obj F) i ≫
      ((singularChainComplexFunctorAdjunction C n).counit.app F).app X =
    F.map (toTopSimplex.inv.app ⦋n⦌ ≫ toTop.map (SSet.yonedaEquiv.symm i) ≫ sSetTopAdj.counit.app X)

pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
F : TopCat ⥤ C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ F.map (toTopSimplex.inv.app ⦋n⦌ ≫ toTop.map (SSet.yonedaEquiv.symm i) ≫ sSetTopAdj.counit.app X) = F.map i.down

Tactic:
· dsimp [singularChainComplexFunctorAdjunction, Adjunction.ofNatIsoRight,
      Adjunction.equivHomsetRightOfNatIso, Adjunction.homEquiv,
      Adjunction.comp, singularChainComplexFunctor, SSet.chainComplexFunctor,
      SSet.chainComplexFunctorAdjunction]
    simp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
F : TopCat ⥤ C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ F.map (toTopSimplex.inv.app ⦋n⦌ ≫ toTop.map (SSet.yonedaEquiv.symm i) ≫ sSetTopAdj.counit.app X) = F.map i.down
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n ↦ x + c ^ n) atTop (𝓝 x)
⊢ ∃ y ∈ U ∩ Set.univ, y ≠ x

Tactic:
have B : ∀ᶠ n in atTop, x + c ^ n ∈ U := tendsto_def.1 A U hU

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n ↦ x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
⊢ ∃ y ∈ U ∩ Set.univ, y ≠ x
Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 := FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial
hr : r ≤ p.radius
g : 𝕜 → 𝕜 := fun t ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall g p x p.radius
hg' :
  IsPreconnected (Metric.eball x r) →
    ∀ {z₀ : 𝕜}, z₀ ∈ Metric.eball x r → f =ᶠ[nhds z₀] g → Set.EqOn f g (Metric.eball x r)
hf : AnalyticAt 𝕜 f x
⊢ f =ᶠ[nhds x] g

Tactic:
apply AnalyticAt.hasFPowerSeriesAt at hf

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 := FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial
hr : r ≤ p.radius
g : 𝕜 → 𝕜 := fun t ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall g p x p.radius
hg' :
  IsPreconnected (Metric.eball x r) →
    ∀ {z₀ : 𝕜}, z₀ ∈ Metric.eball x r → f =ᶠ[nhds z₀] g → Set.EqOn f g (Metric.eball x r)
hf : HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial) x
⊢ f =ᶠ[nhds x] g
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₀ : 𝕜
⊢ analyticOrderAt f z₀ = 0 ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0

Tactic:
by
  by_cases hf : AnalyticAt 𝕜 f z₀
  · rw [← ENat.natCast_zero, hf.analyticOrderAt_eq_natCast]
    constructor
    · intro ⟨g, _, _, hg⟩
      simpa [hf, hg.self_of_nhds]
    · exact fun hz ↦ ⟨f, hf, hz.resolve_left <| not_not_intro hf, by simp⟩
  · simp [hf]

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

Goal state before:
pp: case neg
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
hgt : 1 < (v u) (a w)⁻¹
this : Tendsto (fun n ↦ ‖WithAbs.toAbs (v u) (1 / (1 + (a w)⁻¹ ^ n))‖) atTop (𝓝 0)
⊢ Tendsto
    (fun i ↦
      (WithAbs.equiv (v u)).symm (1 / (1 + (a w)⁻¹ ^ i)) * (WithAbs.equiv (v u)).symm ((WithAbs.equiv (v w)) (z w)))
    atTop (𝓝 0)

Tactic:
simpa using (tendsto_zero_iff_norm_tendsto_zero.2 this).mul_const
        ((WithAbs.equiv (v u)).symm _)

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

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

Tactic:
Function.iterate_succ'

Goal state after:
case succ
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
inst✝ : CharZero 𝕜
n' : ℕ
hk : ∀ {n : ℕ}, ↑n = analyticOrderAt f z₀ → n ≠ 0 → n' ≤ n → analyticOrderAt (deriv^[n'] f) z₀ = ↑(n - n')
n : ℕ
Hn : ↑n = analyticOrderAt f z₀
Hpos : n ≠ 0
Hk : n' + 1 ≤ n
⊢ analyticOrderAt ((deriv ∘ deriv^[n']) f) z₀ = ↑(n - (n' + 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
⊢ f z ≠ 0 → f z ^ g z = cexp (log (f z) * g z)

Tactic:
fz

Goal state after:
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)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
n : ℤ
⊢ MeromorphicAt (f ^ n) x

Tactic:
cases n with
  | ofNat m => simpa only [Int.ofNat_eq_natCast, zpow_natCast] using hf.pow m
  | negSucc m => simpa only [zpow_negSucc, inv_iff] using hf.pow (m + 1)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z₀ : 𝕜
h₁ : AnalyticAt 𝕜 g z₀
h₂ : z₀ ∈ {x}ᶜ
⊢ z₀ - x ≠ 0 ∨ 0 ≤ n

Tactic:
by simp_all [sub_ne_zero_of_ne h₂]

Goal state after:
Module: Mathlib.RingTheory.Binomial

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

Tactic:
exact multichoose_zero_right 1

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case ofNat
k n : ℕ
⊢ ↑(k.factorial * (n + k - 1).choose k) = (ascPochhammer ℕ k).smeval ↑n

Tactic:
rw [← Nat.descFactorial_eq_factorial_mul_choose, smeval_at_natCast, ← eval_eq_smeval n,
        ascPochhammer_nat_eq_descFactorial]

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:
rw [derivWithin_zero_of_not_uniqueDiffWithinAt h,
      derivWithin_zero_of_not_uniqueDiffWithinAt h, mul_zero, zero_mul]

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

Goal state before:
pp: case inl.convert_4.convert_6
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ↑x ∈ slitPlane

Tactic:
· simp [hx]

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

Goal state before:
pp: case inr.convert_6
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
⊢ ↑(-x) ∈ slitPlane

Tactic:
· simp [hx]

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

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

Tactic:
rw [rpow_sub_one hp.ne', ← rpow_def_of_pos hp, smul_add, smul_smul, mul_div_left_comm,
    div_eq_mul_inv, smul_smul, smul_smul, mul_assoc, add_comm]

Goal state after:
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
inst✝² : NormedCommRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt 𝕜 (fun x ↦ f x i) z
p✝ p : MvPolynomial σ A
i : σ
hp : AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) p) z
⊢ AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) (p * X i)) z

Tactic:
simp_rw [map_mul, aeval_X]

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
inst✝² : NormedCommRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt 𝕜 (fun x ↦ f x i) z
p✝ p : MvPolynomial σ A
i : σ
hp : AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) p) z
⊢ AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) p * f x i) z
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: ⊢ linearGrowthInf ⊥ ≤ linearGrowthSup ⊥

Tactic:
exact linearGrowthInf_le_linearGrowthSup

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

Goal state before:
pp: ⊢ linearGrowthInf ⊤ ≤ linearGrowthSup ⊤

Tactic:
exact linearGrowthInf_le_linearGrowthSup

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✝² : CommSemiring β
inst✝¹ : ContinuousAdd β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
p : β[X]
n : ℕ
c : β
⊢ SuperpolynomialDecay l k fun x ↦ eval (k x) ((monomial n) c) * f x

Tactic:
by
    simpa [mul_assoc] using! (hf.param_pow_mul n).const_mul c

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

Goal state before:
pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
⊢ linearGrowthInf u ≤ linearGrowthInf v

Tactic:
apply (linearGrowthInf_eventually_monotone h).trans
  rcases eq_bot_or_bot_lt b with rfl | b_bot
  · simp only [add_bot, ← Pi.bot_def, linearGrowthInf_bot, bot_le]
  · apply (linearGrowthInf_add_le' _ _).trans_eq <;> rw [linearGrowthSup_const b_bot.ne' hb]
    · exact add_zero (linearGrowthInf v)
    · exact Or.inr EReal.zero_ne_top
    · exact Or.inr EReal.zero_ne_bot

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
⊢ ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b

Tactic:
by_contra! hcon

Goal state after:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
⊢ False
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂ν, x ∈ spanningSets μ n → μ.rnDeriv ν x < ∞

Tactic:
← ae_restrict_iff' (measurableSet_spanningSets _ _)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂ν.restrict (spanningSets μ n), μ.rnDeriv ν x < ∞