mathlib-initiative/mathlib-tactics huggingface dataset:
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 κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : IsCardinalPresentable X κ
⊢ P.colimitsCardinalClosure κ X

Tactic:
rw [← (P.colimitsCardinalClosure κ).retractClosure_eq_self]

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
X : C
hX : IsCardinalPresentable X κ
⊢ (P.colimitsCardinalClosure κ).retractClosure X
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : Z ⊗ W ⟶ X
⊢ f ▷ Z ▷ W ≫ (α_ B Z W).hom ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g) =
    (α_ A Z W).hom ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g)

Tactic:
by
  rw [associator_naturality_left_assoc, ← whisker_exchange_assoc, pushout.condition,
    ← MonoidalCategory.whiskerLeft_comp_assoc]

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

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (m + 2)
hi : i ≠ k.castSucc
⊢ i ∈ Set.range ⇑(x.cast hd).simplex.1

Tactic:
subst hd
  have := x.notMem
  simp [Subcomplex.mem_unionProd_iff, mem_horn_iff_notMem_range] at this
  tauto

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: 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₁₃.π
⊢ ⋯.desc (adj₂.homEquiv.symm (Arrow.Hom.left β)) (adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.fst)) ⋯ ≫
      (Arrow.mk f₃).hom =
    (Arrow.mk sq₁₂.ι).hom ≫ adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.snd)

Tactic:
apply sq₁₂.isPushout.hom_ext
        · have := Arrow.w β =≫ sq₁₃.snd
          dsimp at this
          simp only [Category.assoc, sq₁₃.π_snd] at this
          simp [← adj₂.homEquiv_symm_naturality_two,
            ← adj₂.homEquiv_symm_naturality_three, this]
        · simp [← adj₂.homEquiv_symm_naturality_one,
            ← adj₂.homEquiv_symm_naturality_three, sq₁₃.isPullback.w]

Goal state after:
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:
by induction x <;> induction y; exacts [𝟙 X, e.hom, e.inv, 𝟙 Y]

Goal state after:
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 z : WalkingIso
x✝¹ : x ⟶ y
x✝ : y ⟶ z
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ z) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y z))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) z x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) z x)
      x (x✝¹ ≫ x✝) =
    WalkingIso.rec (motive := fun {x} ↦ (x ⟶ y) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y y))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) y x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) y x)
        x x✝¹ ≫
      WalkingIso.rec (motive := fun {x} ↦ (x ⟶ z) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y z))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) z x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) z x)
        y x✝

Tactic:
induction x <;> induction y <;> induction z <;> simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n + 1⦌
⊢ X.ιChainComplex x ≫ (X.chainComplex R).d (n + 1) n =
    ∑ i, (-1) ^ ↑i • X.ιChainComplex ((ConcreteCategory.hom (SimplicialObject.δ X i)) x)

Tactic:
simp [ιChainComplex, chainComplex, chainComplexFunctor, Preadditive.comp_sum]

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

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
this : St = Finset.image it.succ.succAbove Sδ ∪ {it.succ}
⊢ (Finset.image it.succ.succAbove Sδ ∪ {it.succ}).card = Sδ.card + 1

Tactic:
Finset.card_union_of_disjoint (by simp),

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
this : St = Finset.image it.succ.succAbove Sδ ∪ {it.succ}
⊢ (Finset.image it.succ.succAbove Sδ).card + {it.succ}.card = Sδ.card + 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ stdSimplex.δ 1 ≫
      (sSetTopAdj.homEquiv Δ[1] TopCat.I)
        (TopCat.isoOfHomeo (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 0)

Tactic:
rw [← Adjunction.homEquiv_naturality_left, sSetTopAdj_homEquiv_stdSimplex_zero]

Goal state after:
⊢ SSet.const
      (TopCat.toSSetObj₀Equiv.symm
        ((ConcreteCategory.hom
            (toTop.map (stdSimplex.δ 1) ≫
              (TopCat.isoOfHomeo
                  (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom))
          default)) =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 0)
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ stdSimplex.δ 0 ≫
      (sSetTopAdj.homEquiv Δ[1] TopCat.I)
        (TopCat.isoOfHomeo (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 1)

Tactic:
rw [← Adjunction.homEquiv_naturality_left, sSetTopAdj_homEquiv_stdSimplex_zero]

Goal state after:
⊢ SSet.const
      (TopCat.toSSetObj₀Equiv.symm
        ((ConcreteCategory.hom
            (toTop.map (stdSimplex.δ 0) ≫
              (TopCat.isoOfHomeo
                  (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom))
          default)) =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 1)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case pos
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
hlt : (v u) (a u)⁻¹ < 1
⊢ Tendsto
    (fun i ↦
      (WithAbs.equiv (v u)).symm (1 / (1 + (a u)⁻¹ ^ i)) * (WithAbs.equiv (v u)).symm ((WithAbs.equiv (v u)) (z u)))
    atTop (𝓝 (z u))

Tactic:
simpa using (WithAbs.tendsto_one_div_one_add_pow_nhds_one hlt).mul_const (z u)

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
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
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
n : ℕ
⊢ ↑f'symm.nnnorm * dist (f (u n)) y ≤ ↑f'symm.nnnorm * ((↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y)

Tactic:
by
        gcongr
        exact (D n).1

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

Goal state before:
pp: case convert_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
this : AnalyticAt 𝕜 (fun z ↦ ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0) 0
i : ℕ
hi : i < n
⊢ iteratedDeriv i f 0 -
      ∑ x ∈ Finset.range n, (↑(if i = x then x.factorial else 0) / ↑x.factorial) • iteratedDeriv x f 0 =
    0

Tactic:
simp [ite_div, Finset.sum_ite_eq_of_mem _ _ _ (Finset.mem_range.mpr hi)]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Prod

Goal state before:
pp: case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x ↦ φ x i) s x
hsx : ¬AccPt x (𝓟 s)
⊢ derivWithin φ s x = fun i ↦ derivWithin (fun x ↦ φ x i) s x

Tactic:
simp [derivWithin, fderivWithin_zero_of_not_accPt hsx, Pi.zero_def]

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
x : 𝕜
f : 𝕜 → E
h : MeromorphicAt f x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt f y

Tactic:
obtain ⟨n, h⟩ := h

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt f y
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
x : 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
h : MeromorphicAt f x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y

Tactic:
obtain ⟨n, h⟩ := h

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
x : 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
⊢ MeromorphicAt (f ∘ g) x

Tactic:
by
  obtain ⟨r, hr⟩ := hf
  by_cases hg' : analyticOrderAt (g · - g x) x = ⊤
  · -- trivial case: `g` is locally constant near `x`
    refine .congr (.const (f (g x)) x) ?_
    filter_upwards [nhdsWithin_le_nhds <| analyticOrderAt_eq_top.mp hg'] with z hz
    grind
  · -- interesting case: `g z - g x` looks like `(z - x) ^ n` times a non-vanishing function
    obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.mp hg'
    obtain ⟨h, han, hne, heq⟩ := (hg.fun_sub analyticAt_const).analyticOrderAt_eq_natCast.mp hn.symm
    set j := fun z ↦ (z - g x) ^ r • f z
    have : AnalyticAt 𝕜 (fun i ↦ (h i)⁻¹ ^ r • j (g i)) x :=
      ((han.inv hne).pow r).smul (hr.restrictScalars.comp hg)
    refine ⟨n * r, this.congr ?_⟩
    filter_upwards [heq, han.continuousAt.tendsto.eventually_ne hne] with z hz hzne
    simp only [j, inv_pow, Function.comp_apply, inv_smul_eq_iff₀ (pow_ne_zero r hzne)]
    rw [hz, smul_comm, ← smul_assoc, pow_mul, smul_pow]

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:
rw [← derivWithin_univ, derivWithin_const_cpow, derivWithin_univ]

Goal state after:
case hf
f : ℂ → ℂ
x : ℂ
hf : DifferentiableAt ℂ f x
c : ℂ
⊢ DifferentiableWithinAt ℂ f Set.univ x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inr
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
⊢ HasDerivAt (fun y ↦ ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x

Tactic:
have : ∀ᶠ y : ℝ in 𝓝 x,
        (y : ℂ) ^ (r + 1) / (r + 1) = (-y : ℂ) ^ (r + 1) * exp (π * I * (r + 1)) / (r + 1) := by
      refine Filter.eventually_of_mem (Iio_mem_nhds hx) fun y hy => ?_
      rw [ofReal_cpow_of_nonpos (le_of_lt hy)]

Goal state after:
case inr
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)
⊢ HasDerivAt (fun y ↦ ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inr
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
⊢ HasDerivAt (fun y ↦ ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x

Tactic:
· -- harder case : `x < 0`
    have : ∀ᶠ y : ℝ in 𝓝 x,
        (y : ℂ) ^ (r + 1) / (r + 1) = (-y : ℂ) ^ (r + 1) * exp (π * I * (r + 1)) / (r + 1) := by
      refine Filter.eventually_of_mem (Iio_mem_nhds hx) fun y hy => ?_
      rw [ofReal_cpow_of_nonpos (le_of_lt hy)]
    refine HasDerivAt.congr_of_eventuallyEq ?_ this
    rw [ofReal_cpow_of_nonpos (le_of_lt hx)]
    suffices HasDerivAt (fun y : ℝ => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)))
        ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x by
      convert! this.div_const (r + 1) using 1
      conv_rhs => rw [mul_assoc, mul_comm, mul_div_cancel_right₀ _ hr]
    rw [mul_add ((π : ℂ) * _), mul_one, exp_add, exp_pi_mul_I, mul_comm (_ : ℂ) (-1 : ℂ),
      neg_one_mul]
    simp_rw [mul_neg, ← neg_mul, ← ofReal_neg]
    suffices HasDerivAt (fun y : ℝ => (↑(-y) : ℂ) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x by
      convert! this.neg.mul_const _ using 1; ring
    suffices HasDerivAt (fun y : ℝ => (y : ℂ) ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x) by
      convert! @HasDerivAt.scomp ℝ _ ℂ _ _ x ℝ _ _ _ _ _ _ _ _ this (hasDerivAt_neg x) using 1
      rw [real_smul, ofReal_neg 1, ofReal_one]; ring
    suffices HasDerivAt (fun y : ℂ => y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x) by
      exact this.comp_ofReal
    conv in ↑_ ^ _ => rw [(by ring : r = r + 1 - 1)]
    convert! HasDerivAt.cpow_const ?_ ?_ using 1
    · rw [add_sub_cancel_right, add_sub_cancel_right]; exact (mul_one _).symm
    · exact hasDerivAt_id ((-x : ℝ) : ℂ)
    · simp [hx]

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

Goal state before:
pp: f : ℝ → ℝ
f' x p : ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun y ↦ f y ^ p) (f' * p * f x ^ (p - 1)) x

Tactic:
by
  rw [← hasDerivWithinAt_univ] at *
  exact hf.rpow_const hx

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

Goal state before:
pp: r : ℝ
hr : r ≠ 0
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (r - x)) (FormalMultilinearSeries.ofScalars ℝ fun n ↦ (r ^ (n + 1))⁻¹) 0 ‖r‖ₑ

Tactic:
simpa using one_div_sub_pow_hasFPowerSeriesOnBall_zero (a := 0) hr

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

Goal state before:
pp: case top
y : EReal
⊢ (⊤ + y).exp = ⊤.exp * y.exp

Tactic:
induction y
    · simp
    · simp only [EReal.top_add_coe, exp_top, exp_coe]
      rw [ENNReal.top_mul]
      simp [Real.exp_pos]
    · simp

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
⊢ ∀ (s : Set X) (f : X → Set (Set X)),
    (∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}) →
      (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε) →
        ∃ t, (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p ↦ p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0

Tactic:
intro s

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
⊢ ∀ (f : X → Set (Set X)),
    (∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}) →
      (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε) →
        ∃ t, (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p ↦ p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case neg.inr.refine_1
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, ↑(v n) ≤ a' * ↑n
u_b : ∃ᶠ (x : ℕ) in atTop, (u x ≤ b * ↑x ∧ 0 < x) ∧ ∃ m, a⁻¹ * ↑x ≤ ↑m ∧ ↑m ≤ a'⁻¹ * ↑x
M M' : ℕ
aM_M' : ↑M * a ≤ ↑M'
n : ℕ
n_M' : M' ≤ n
un_bn : u n ≤ b * ↑n
right✝ : 0 < n
k : ℕ
an_k : a⁻¹ * ↑n ≤ ↑k
k_an' : ↑k ≤ a'⁻¹ * ↑n
⊢ M ≤ k

Tactic:
← le_div_iff_mul_le a_0 a_top,

Goal state after:
case neg.inr.refine_1
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, ↑(v n) ≤ a' * ↑n
u_b : ∃ᶠ (x : ℕ) in atTop, (u x ≤ b * ↑x ∧ 0 < x) ∧ ∃ m, a⁻¹ * ↑x ≤ ↑m ∧ ↑m ≤ a'⁻¹ * ↑x
M M' : ℕ
aM_M' : ↑M ≤ ↑M' / a
n : ℕ
n_M' : M' ≤ n
un_bn : u n ≤ b * ↑n
right✝ : 0 < n
k : ℕ
an_k : a⁻¹ * ↑n ≤ ↑k
k_an' : ↑k ≤ a'⁻¹ * ↑n
⊢ M ≤ k
Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
μt : μ t ≤ 0
⊢ ∀ᵐ (x : α) ∂μ, x ∉ t

Tactic:
have : μ t = 0 := le_antisymm μt bot_le

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
μt : μ t ≤ 0
this : μ t = 0
⊢ ∀ᵐ (x : α) ∂μ, x ∉ t