mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝⁶ : Category.{v', u'} V
inst✝⁵ : MonoidalCategory V
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : EnrichedOrdinaryCategory V C
W : Type u''
inst✝² : Category.{v'', u''} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ((eHomEquiv V).trans (e (X✝ ⟶[V] Z✝))) (f ≫ g) =
    (λ_ (𝟙_ W)).inv ≫
      (((eHomEquiv V).trans (e (X✝ ⟶[V] Y✝))) f ⊗ₘ ((eHomEquiv V).trans (e (Y✝ ⟶[V] Z✝))) g) ≫ eComp W X✝ Y✝ Z✝

Tactic:
dsimp +instances [instEnrichedCategoryTransportEnrichment]
    rw [h, h, h, ← tensorHom_comp_tensorHom_assoc, eComp_eq, tensorHom_def_assoc,
      whiskerRight_id_assoc, unitors_inv_equal, Iso.inv_hom_id_assoc,
      Functor.LaxMonoidal.μ_natural_assoc, Functor.LaxMonoidal.right_unitality_inv_assoc,
      eHomEquiv_comp, ← F.map_comp, ← F.map_comp, unitors_inv_equal]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (inclusion n).op.HasRightKanExtension F
inst✝ : X.IsCoskeletal n
⊢ IsIso ((coskAdj n).unit.app X)

Tactic:
← isCoskeletal_iff_isIso

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (inclusion n).op.HasRightKanExtension F
inst✝ : X.IsCoskeletal n
⊢ X.IsCoskeletal n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case hᵥ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ (X.spine n
          (sx.spineToSimplex
            { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
              arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
              arrow_src := ⋯, arrow_tgt := ⋯ })).vertex
      ((Hom.toOrderHom f) k) =
    (X.spine i ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk f.op))) x)).vertex k

Tactic:
spine_spineToSimplex_apply,

Goal state after:
case hᵥ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
        arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
        arrow_src := ⋯, arrow_tgt := ⋯ }
      ((Hom.toOrderHom f) k) =
    (X.spine i ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk f.op))) x)).vertex k
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
this : x ∈ Set.univ
⊢ ∃ y, x = ↑y ∨ x = ↑(P.p y)

Tactic:
rw [← P.union, Set.mem_union] at this

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
this : x ∈ P.I ∨ x ∈ P.II
⊢ ∃ y, x = ↑y ∨ x = ↑(P.p y)
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
inst✝¹ : P.IsProper
inst✝ : P.IsInner
⊢ ∀ (x : ↑(P.ofIso e hA).II) {d : ℕ} (hd : (↑x).dim = d), ⋯.index hd ≠ 0

Tactic:
rintro ⟨b, hb⟩ d hd
    obtain ⟨a, rfl⟩ := (N.orderIsoOfIso e hA).symm.surjective b
    simp only [ofIso_II, Set.mem_preimage, OrderIso.apply_symm_apply] at hb
    simpa only [P.ofIso_index e hA ⟨a, hb⟩ hd] using IsInner.ne_zero ⟨a, hb⟩ hd

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: case left
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
⊢ Function.Injective h.functor.mapArrow.obj

Tactic:
rintro ⟨x, y, f⟩ ⟨x', y', g⟩ hfg
      obtain rfl : x = x' := by simpa using! congr_arg Arrow.leftFunc.obj hfg
      obtain rfl : y = y' := by simpa using! congr_arg Arrow.rightFunc.obj hfg
      obtain rfl : f = g := by simpa [Arrow.mk_eq_mk_iff] using! hfg
      rfl

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : LocallySmall.{w, v, u} C
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : EssentiallySmall.{w, v', u'} J
F : J ⥤ C
inst✝³ : F.IsDense
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : ∀ (j : J), IsCardinalPresentable (F.obj j) κ
inst✝ : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
X : C
ip : F.DenseAt X
⊢ ∃ J_1 x, ∃ (_ : IsCardinalFiltered J_1 κ), (⊤.map F).colimitsOfShape J_1 X

Tactic:
let e := equivSmallModel.{w} (CostructuredArrow F X)

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : LocallySmall.{w, v, u} C
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : EssentiallySmall.{w, v', u'} J
F : J ⥤ C
inst✝³ : F.IsDense
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : ∀ (j : J), IsCardinalPresentable (F.obj j) κ
inst✝ : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
X : C
ip : F.DenseAt X
e : CostructuredArrow F X ≌ SmallModel.{w, v', max u' v} (CostructuredArrow F X) :=
  equivSmallModel (CostructuredArrow F X)
⊢ ∃ J_1 x, ∃ (_ : IsCardinalFiltered J_1 κ), (⊤.map F).colimitsOfShape J_1 X
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
P : ObjectProperty C
inst✝⁴ : ObjectProperty.EssentiallySmall.{w, v, u} P
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : P.ι.IsDense
inst✝¹ : LocallySmall.{w, v, u} C
hP : P ≤ isCardinalPresentable C κ
inst✝ : ∀ (X : C), IsCardinalFiltered (CostructuredArrow P.ι X) κ
⊢ P.IsCardinalFilteredGenerator κ

Tactic:
rw [← ObjectProperty.IsCardinalFilteredGenerator.isoClosure_iff]
  have (X : P.FullSubcategory) : IsCardinalPresentable (P.ι.obj X) κ := hP _ X.property
  simpa using IsCardinalFilteredGenerator.of_isDense P.ι κ

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

Goal state before:
pp: case refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
h : min x hd ≤ i
⊢ k.castSucc < (x.cast hd).simplex.1 i

Tactic:
· rw [Fin.castSucc_lt_iff_succ_le, ← simplex_fst_min x hd]
    exact stdSimplex.monotone_apply _ h

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
hx : IsType₂ x
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
⊢ (objEquiv
        ((ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) (min x hd).castSucc))
          (objEquiv.symm { toFun := φ x hd, monotone' := ⋯ })))
      i =
    (objEquiv (x.cast hd).simplex) i

Tactic:
rw [objEquiv_δ_apply, Equiv.apply_symm_apply, OrderHom.coe_mk, φ_succAbove]

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 Y : SSet
f : X ⟶ Y
R : C
n : ℕ
x : X _⦋n⦌
⊢ X.ιChainComplex x ≫ (chainComplexMap f R).f n = Y.ιChainComplex ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x)

Tactic:
dsimp [chainComplexMap, chainComplexFunctor, ιChainComplex, Sigma.map',
    chainComplex, chainComplexFunctor]
  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 Y Z : SSet
f : X ⟶ Y
g : Y ⟶ Z
R : C
inst✝ : CategoryWithHomology C
n : ℕ
⊢ SSet.homologyMap (f ≫ g) R n = SSet.homologyMap f R n ≫ SSet.homologyMap g R n

Tactic:
simp [SSet.homologyMap, HomologicalComplex.homologyMap_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case hₗ
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₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝ f₂✝
f₁ f₁' : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ sq₁₂.inl ≫
      (𝟭 C₃).map
          (⋯.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
            ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inl ≫ (Arrow.mk sq₁₂.ι).hom ≫ (𝟭 C₃).map ((F.map (Arrow.Hom.right sq)).app f₂.right)

Tactic:
simp [← NatTrans.comp_app, ← Functor.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case hᵣ
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₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝ f₂✝
f₁ f₁' : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ sq₁₂.inr ≫
      (𝟭 C₃).map
          (⋯.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
            ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inr ≫ (Arrow.mk sq₁₂.ι).hom ≫ (𝟭 C₃).map ((F.map (Arrow.Hom.right sq)).app f₂.right)

Tactic:
simp [← NatTrans.comp_app, ← Functor.map_comp]

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Nonempty (Unique (ZerothHomotopy ↑X))

Tactic:
rw [unique_iff_subsingleton_and_nonempty]

Goal state after:
X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Subsingleton (ZerothHomotopy ↑X) ∧ Nonempty (ZerothHomotopy ↑X)
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this✝ : (i : ι) → Fintype ↑(f i)
u : Finset α := (f i).toFinset
this : s ⊆ u
⊢ s.card ≤ u.card

Tactic:
exact Finset.card_le_card this

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: F : Type u_1
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
⊢ IsPathConnected (↑E)ᶜ

Tactic:
rcases E.exists_isCompl with ⟨E', hE'⟩

Goal state after:
F : Type u_1
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
E' : Submodule ℝ F
hE' : IsCompl E E'
⊢ IsPathConnected (↑E)ᶜ
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: case inr
𝕜 : 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
⊢ y ∈ f '' closedBall b ε

Tactic:
have Jcf' : (1 : ℝ) - c * f'symm.nnnorm ≠ 0 := by apply ne_of_gt; linarith

Goal state after:
case inr
𝕜 : 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
⊢ y ∈ f '' closedBall b ε
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
⊢ v.IsEquiv w ↔ IsHomeomorph ⇑(WithAbs.congr v w (RingEquiv.refl F))

Tactic:
by
  rw [isHomeomorph_iff_isEmbedding_surjective]
  refine ⟨fun h ↦ ⟨h.isEmbedding_equivWithAbs, RingEquiv.surjective _⟩, fun ⟨hi, _⟩ ↦ ?_⟩
  refine isEquiv_iff_lt_one_iff.2 fun x ↦ ?_
  conv_lhs => rw [← WithAbs.ofAbs_toAbs v x]
  conv_rhs => rw [← WithAbs.ofAbs_toAbs w x]
  rw [← WithAbs.norm_eq_apply_ofAbs, ← WithAbs.norm_eq_apply_ofAbs,
    ← tendsto_pow_atTop_nhds_zero_iff_norm_lt_one, ← tendsto_pow_atTop_nhds_zero_iff_norm_lt_one]
  exact ⟨fun h ↦ by simpa [Function.comp_def] using (hi.continuous.tendsto 0).comp h, fun h ↦ by
    simpa [Function.comp_def] using (hi.continuous_iff (f := (WithAbs.congr v w (.refl F)).symm)).2
      continuous_id |>.tendsto 0 |>.comp h ⟩

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

Goal state before:
pp: C D : Type u
inst✝¹ : Category.{u, u} C
inst✝ : Category.{u, u} D
⊢ IsIso (prodComparison hoFunctor (nerve C) (nerve D))

Tactic:
have : IsIso (nerveFunctor.map (prodComparison hoFunctor (nerve C) (nerve D))) := by
    have : IsIso (prodComparison (hoFunctor ⋙ nerveFunctor) (nerve C) (nerve D)) :=
      IsIso.of_isIso_fac_left
        (prodComparison_comp nerveFunctor (hoFunctor ⋙ nerveFunctor)
          (A := Cat.of C) (B := Cat.of D)).symm
    exact IsIso.of_isIso_fac_right (prodComparison_comp hoFunctor nerveFunctor).symm
  exact isIso_of_fully_faithful nerveFunctor _

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : ↑r = analyticOrderAt f (g z₀)
s : ℕ
hs : ↑s = analyticOrderAt (fun x ↦ g x - g z₀) z₀
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z

Tactic:
rw [Eq.comm, hf.analyticOrderAt_eq_natCast] at hr

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : ∃ g_1, AnalyticAt 𝕜 g_1 (g z₀) ∧ g_1 (g z₀) ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • g_1 z
s : ℕ
hs : ↑s = analyticOrderAt (fun x ↦ g x - g z₀) z₀
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
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'‖ < ε
op : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s)
⊢ DifferentiableAt ℝ f z

Tactic:
exact (diff z z_in).differentiableAt (IsOpen.mem_nhds op z_in)

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

Goal state before:
pp: case pos
𝕜 : 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 : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin φ s x = fun i ↦ derivWithin (fun x ↦ φ x i) s x

Tactic:
rw [derivWithin, fderivWithin_pi h hsx]
    simp [derivWithin]

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
g : 𝕜 → 𝕜
x : 𝕜
f : 𝕜 → E
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hfg : MeromorphicAt (g • f) x
⊢ MeromorphicAt f x

Tactic:
refine (hg.inv hg').meromorphicAt.smul hfg |>.congr ?_

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → 𝕜
x : 𝕜
f : 𝕜 → E
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hfg : MeromorphicAt (g • f) x
⊢ g⁻¹ • g • f =ᶠ[𝓝[≠] x] f
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 : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt 𝕜' (fun z ↦ (z - g x) ^ r • f z) (g x)
⊢ MeromorphicAt (f ∘ g) x

Tactic:
by_cases hg' : analyticOrderAt (g · - g x) x = ⊤

Goal state after:
case pos
𝕜 : 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 : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt 𝕜' (fun z ↦ (z - g x) ^ r • f z) (g x)
hg' : analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
⊢ MeromorphicAt (f ∘ g) x

case neg
𝕜 : 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 : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt 𝕜' (fun z ↦ (z - g x) ^ r • f z) (g x)
hg' : ¬analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
⊢ MeromorphicAt (f ∘ g) x
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:
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.Analytic.Binomial

Goal state before:
pp: a : ℂ
this : binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
⊢ HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ a) (binomialSeries ℂ a) 0 1

Tactic:
convert! AnalyticOn.hasFPowerSeriesOnSubball _ _ _
    · norm_num
    · -- TODO: use `fun_prop` for this subgoal
      apply AnalyticOn.cpow (analyticOn_const.add analyticOn_id) analyticOn_const
      intro z hz
      apply Complex.mem_slitPlane_of_norm_lt_one
      rw [← ENNReal.ofReal_one, Metric.eball_ofReal] at hz
      simpa using hz
    · rw [← this]
      exact binomialSeries_radius_ge_one

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)
⊢ (r + s - k • 1) *
      ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s) =
    ∑ x ∈ antidiagonal k,
      (↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ (x.2 + 1)).smeval s) +
        ↑(k.choose x.2) * ((descPochhammer ℤ (x.1 + 1)).smeval r * (descPochhammer ℤ x.2).smeval s))

Tactic:
mul_sum

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)
⊢ ∑ i ∈ antidiagonal k,
      (r + s - k • 1) * (↑(k.choose i.1) * ((descPochhammer ℤ i.1).smeval r * (descPochhammer ℤ i.2).smeval s)) =
    ∑ x ∈ antidiagonal k,
      (↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ (x.2 + 1)).smeval s) +
        ↑(k.choose x.2) * ((descPochhammer ℤ (x.1 + 1)).smeval r * (descPochhammer ℤ x.2).smeval s))
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    (k.choose x.1 * x.1.factorial * (k - x.1).factorial) • (choose r x.1 * choose s x.2)

Tactic:
tsub_eq_of_eq_add_rev (List.Nat.mem_antidiagonal.mp hx).symm,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    (k.choose x.1 * x.1.factorial * x.2.factorial) • (choose r x.1 * choose s x.2)
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 : MvPolynomial σ A
⊢ AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) p) z

Tactic:
apply p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦ ?_ -- `refine` doesn't work
  · simp_rw [aeval_C]; apply analyticAt_const
  · simp_rw [map_add]; exact hp.add hq
  · simp_rw [map_mul, aeval_X]; exact hp.mul (hf i)

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

Goal state before:
pp: a : ℝ
ha : 0 < a
x : ℝ
⊢ HasStrictDerivAt (fun x ↦ a ^ x) (a ^ x * log a) x

Tactic:
simpa using (hasStrictDerivAt_const _ _).rpow (hasStrictDerivAt_id x) ha

Goal state after: