mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
⊢ IsLimit (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.mapCone (PullbackCone.mk (f.t j) (f.m j) ⋯))

Tactic:
refine (isLimitMapConePullbackConeEquiv _ _).symm
      (IsPullback.isLimit ?_)
    rw [Types.isPullback_iff]
    dsimp
    refine ⟨congr_app (f.w j) (op ⦋d⦌),
      fun a₁ a₂ h ↦ (mono_iff_injective _).mp
        ((NatTrans.mono_iff_mono_app (f.m j)).mp inferInstance _) h.2, fun y b h ↦ ?_⟩
    obtain ⟨x, b, rfl⟩ := f.ιSigmaStdSimplex_jointly_surjective b
    have hb : b ∈ Λ[_, x.index].obj _ := by
      obtain ⟨y, hy⟩ := y
      simp only [← x.preimage_filtration_map]
      rw [Subtype.ext_iff] at h
      dsimp at h
      subst h
      rwa [x.ι_b_app_apply] at hy
    refine ⟨x.ιSigmaHorn.app _ ⟨b, hb⟩, ?_, ?_⟩
    · simpa only [Subfunctor.toFunctor_obj, Subtype.ext_iff,
        x.ι_b_app_apply, x.ι_t_app_apply] using! h.symm
    · rw [← NatTrans.comp_app_apply]
      simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasLimitsOfShape Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
⊢ IsCardinalPresentable c.pt κ

Tactic:
have (k : Kᵒᵖ) : ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ := by
    dsimp; infer_instance
  exact Functor.isCardinalAccessible_of_isLimit
    (coyoneda.mapCone c.op) (isLimitOfPreserves _ hc.op) κ (by simpa)

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

Goal state before:
pp: case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : c.s = c'.s
⊢ Cell.type₂ f c = Cell.type₂ f c'

Tactic:
congr; aesop

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj s.pt :=
  fun s ↦
    {
      app := fun x ↦
        match x with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
⊢ F.isDenseAt Y

Tactic:
have hφ (s) (j) : (restrictedULiftYoneda F).map j.hom ≫ φ s =
        (restrictedULiftYoneda F).map (s.ι.app j) := by
      ext ⟨X⟩ ⟨x⟩
      let α : .mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x)
      have := s.w α
      dsimp [uliftYoneda, φ, α] at this ⊢
      apply ULift.down_injective
      simpa using this.symm

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj s.pt :=
  fun s ↦
    {
      app := fun x ↦
        match x with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
hφ :
  ∀ (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) (j : CostructuredArrow F Y),
    (restrictedULiftYoneda F).map j.hom ≫ φ s = (restrictedULiftYoneda F).map (s.ι.app j)
⊢ F.isDenseAt Y
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₁₃.π
this : (Arrow.Hom.left β ≫ sq₁₃.π) ≫ sq₁₃.fst = (f₂ ≫ Arrow.Hom.right β) ≫ sq₁₃.fst
⊢ (F.map f₁).app X₂ ≫ adj₂.homEquiv.symm (Arrow.Hom.left β) =
    (F.obj X₁).map f₂ ≫ adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.fst)

Tactic:
simp only [Category.assoc, sq₁₃.π_fst] at this

Goal state after:
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₁₃.π
this : Arrow.Hom.left β ≫ (G.map f₁.op).app X₃ = f₂ ≫ Arrow.Hom.right β ≫ sq₁₃.fst
⊢ (F.map f₁).app X₂ ≫ adj₂.homEquiv.symm (Arrow.Hom.left β) =
    (F.obj X₁).map f₂ ≫ adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.fst)
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

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₂
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 sq₁₂.ι ⟶ Arrow.mk f₃
l : Arrow.LiftStruct ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)
this : (l.l ≫ sq₁₃.π) ≫ sq₁₃.fst = Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α) ≫ sq₁₃.fst
⊢ sq₁₂.inr ≫ sq₁₂.ι ≫ adj₂.homEquiv.symm l.l = sq₁₂.inr ≫ Arrow.Hom.left α

Tactic:
simp only [Category.assoc, sq₁₃.π_fst] at this

Goal state after:
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₂
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 sq₁₂.ι ⟶ Arrow.mk f₃
l : Arrow.LiftStruct ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)
this : l.l ≫ (G.map f₁.op).app X₃ = Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α) ≫ sq₁₃.fst
⊢ sq₁₂.inr ≫ sq₁₂.ι ≫ adj₂.homEquiv.symm l.l = sq₁₂.inr ≫ Arrow.Hom.left α
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
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
⊢ i.castSucc ≤ i.succ

Tactic:
exact Fin.castSucc_le_succ i

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

Goal state before:
pp: X Y Z : SSet
⊢ SimplicialObject.δ X 1 ≫ ↾π₀.mk = SimplicialObject.δ X 0 ≫ ↾π₀.mk

Tactic:
ext s

Goal state after:
X Y Z : SSet
s : X _⦋0 + 1⦌
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 1 ≫ ↾π₀.mk)).toFun s =
    (ConcreteCategory.hom (SimplicialObject.δ X 0 ≫ ↾π₀.mk)).toFun s
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: n : ℕ
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
H :
  ∀ (x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })) (y : Y.obj (op { obj := ⦋2⦌, property := _proof_14 })),
    f₁ ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x) =
        (ConcreteCategory.hom (Y.map (δ₂ 2 _proof_12 _proof_15).op)) y →
      f₁ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_12 _proof_15).op)) y →
        f₁ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_12 _proof_15).op)) y
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })
⊢ (Y.spine 1 f₂._proof_6 (f₁ ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x))).vertex 1 =
    (Y.spine 1 f₂._proof_6 (f₁ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x))).vertex 0

Tactic:
by
        simp only [spine_vertex]
        rw [← δ₂_one_eq_const, ← δ₂_zero_eq_const, ← hδ₁, ← hδ₀]
        simp only [← Functor.map_comp_apply, ← op_comp, δ₂_zero_comp_δ₂_two]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #↑t ≤ a

Tactic:
rcases lt_or_ge a ℵ₀ with ha | ha
  /- case `a` finite. In this case, it suffices to show that any finite subset `s` of `t` has
  cardinality at most `a`. For this, we pick `i` such that `f i` contains all the points in `s`,
  and apply the assumption that the cardinality of `f i` is at most `a`.   -/
  · obtain ⟨n, rfl⟩ : ∃ (n : ℕ), a = n := lt_aleph0.1 ha
    apply mk_le_iff_forall_finset_subset_card_le.2 (fun s hs ↦ ?_)
    have A : ∀ x ∈ s, ∀ᶠ i in l, x ∈ f i := fun x hx ↦ ht x (hs hx)
    have B : ∀ᶠ i in l, ∀ x ∈ s, x ∈ f i := (s.eventually_all).2 A
    rcases B.exists with ⟨i, hi⟩
    have : ∀ i, Fintype (f i) := fun i ↦ (lt_aleph0_iff_fintype.1 ((h'f i).trans_lt ha)).some
    let u : Finset α := (f i).toFinset
    have I1 : s.card ≤ u.card := by
      have : s ⊆ u := fun x hx ↦ by simpa only [u, Set.mem_toFinset] using hi x hx
      exact Finset.card_le_card this
    have I2 : (u.card : Cardinal) ≤ n := by
      convert! h'f i; simp only [u, Set.toFinset_card, mk_fintype]
    exact I1.trans (Nat.cast_le.1 I2)
  -- case `a` infinite:
  · have : t ⊆ ⋃ i, f i := by
      intro x hx
      obtain ⟨i, hi⟩ : ∃ i, x ∈ f i := (ht x hx).exists
      exact mem_iUnion_of_mem i hi
    calc #t ≤ #(⋃ i, f i) := mk_le_mk_of_subset this
      _ ≤ sum (fun i ↦ #(f i)) := mk_iUnion_le_sum_mk
      _ ≤ sum (fun _ ↦ a) := sum_le_sum _ _ h'f
      _ = #ι * a := by simp
      _ ≤ ℵ₀ * a := by grw [mk_le_aleph0]
      _ = a := aleph0_mul_eq ha

Goal state after:
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)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
⊢ ∃ y ∈ U ∩ Set.univ, y ≠ x

Tactic:
rcases B.exists with ⟨n, hn⟩

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
n : ℕ
hn : x + c ^ n ∈ U
⊢ ∃ y ∈ U ∩ Set.univ, y ≠ x
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddGroup E
inst✝³ : MulActionWithZero 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
g : E ≃ₜ E := Homeomorph.addLeft x
t : Set E := ⇑g ⁻¹' s
this : t ∈ 𝓝 0
⊢ #↑s = #E

Tactic:
have A : #t = #E := cardinal_eq_of_mem_nhds_zero 𝕜 this

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddGroup E
inst✝³ : MulActionWithZero 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
g : E ≃ₜ E := Homeomorph.addLeft x
t : Set E := ⇑g ⁻¹' s
this : t ∈ 𝓝 0
A : #↑t = #E
⊢ #↑s = #E
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: case inl
𝕜 : 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
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hE : Subsingleton E
this : Subsingleton F
⊢ Surjective f

Tactic:
exact surjective_to_subsingleton _

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

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
⊢ ordinaryHypergeometricSeries 𝔸 a b c = ordinaryHypergeometricSeries 𝔸 b a c

Tactic:
unfold ordinaryHypergeometricSeries ordinaryHypergeometricCoefficient
  simp [mul_assoc, mul_left_comm]

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
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - z₀) ^ n • f z) z₀
h₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (z - z₀) ^ n • f z = 0
y : 𝕜
h₁y : (y - z₀) ^ n • f y = 0
h₂y : ¬y = z₀
⊢ f y = 0

Tactic:
← sub_eq_zero

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - z₀) ^ n • f z) z₀
h₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (z - z₀) ^ n • f z = 0
y : 𝕜
h₁y : (y - z₀) ^ n • f y = 0
h₂y : ¬y - z₀ = 0
⊢ f y = 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case h.left
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
⊢ Subtype.val ⁻¹' t' ⊆ {u | analyticOrderAt f ↑u = ⊤}ᶜ

Tactic:
intro w

Goal state after:
case h.left
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
⊢ w ∈ Subtype.val ⁻¹' t' → w ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
⊢ (∃ n g, AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z) → MeromorphicAt f x

Tactic:
refine fun ⟨n, g, hg_an, hg_eq⟩ ↦ MeromorphicAt.congr ?_ (EventuallyEq.symm hg_eq)
    exact (((MeromorphicAt.id x).sub (.const _ x)).zpow _).smul hg_an.meromorphicAt

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun x ↦ deriv f x) (𝓝[>] a) (𝓝 e)
⊢ HasDerivWithinAt f e (Ici a) a

Tactic:
obtain ⟨b, ab : a < b, sab : Ioc a b ⊆ s⟩ := mem_nhdsGT_iff_exists_Ioc_subset.1 hs
  let t := Ioo a b
  have ts : t ⊆ s := Subset.trans Ioo_subset_Ioc_self sab
  have t_diff : DifferentiableOn ℝ f t := f_diff.mono ts
  have t_conv : Convex ℝ t := convex_Ioo a b
  have t_open : IsOpen t := isOpen_Ioo
  have t_closure : closure t = Icc a b := closure_Ioo ab.ne
  have t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y := by
    rw [t_closure]
    intro y hy
    by_cases h : y = a
    · rw [h]; exact f_lim.mono ts
    · have : y ∈ s := sab ⟨lt_of_le_of_ne hy.1 (Ne.symm h), hy.2⟩
      exact (f_diff.continuousOn y this).mono ts
  have t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (1 : ℝ →L[ℝ] ℝ) e)) := by
    simp only [toSpanSingleton_deriv.symm]
    exact Tendsto.comp
      (isBoundedBilinearMap_smulRight : IsBoundedBilinearMap ℝ _).continuous_right.continuousAt
      (tendsto_nhdsWithin_mono_left Ioo_subset_Ioi_self f_lim')
  -- now we can apply `hasFDerivWithinAt_closure_of_tendsto_fderiv`
  have : HasDerivWithinAt f e (Icc a b) a := by
    rw [hasDerivWithinAt_iff_hasFDerivWithinAt, ← t_closure]
    exact hasFDerivWithinAt_closure_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'
  exact this.mono_of_mem_nhdsWithin (Icc_mem_nhdsGE ab)

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
⊢ (n + k).choose k • choose (r + ↑k) (n + k) = choose (r + ↑k) k * choose r n

Tactic:
choose_smul_choose (r + k) (Nat.le_add_left k n),

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
⊢ choose (r + ↑k) k * choose (r + ↑k - ↑k) (n + k - k) = choose (r + ↑k) k * choose r n
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case convert_2
a : ℕ
z : ℂ
hz : z ≠ 0
this✝ :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)) ((z⁻¹ • 1) 0) 1
H : 1 / ‖z⁻¹ • 1‖ₑ = ‖z‖ₑ
this :
  HasFPowerSeriesOnBall (fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹)
    ((FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)).compContinuousLinearMap (z⁻¹ • 1)) 0 ‖z‖ₑ
⊢ Set.EqOn ((z ^ (a + 1))⁻¹ • fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹) (fun x ↦ 1 / (z - x) ^ (a + 1))
    (Metric.eball 0 ‖z‖ₑ)

Tactic:
intro w

Goal state after:
case convert_2
a : ℕ
z : ℂ
hz : z ≠ 0
this✝ :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)) ((z⁻¹ • 1) 0) 1
H : 1 / ‖z⁻¹ • 1‖ₑ = ‖z‖ₑ
this :
  HasFPowerSeriesOnBall (fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹)
    ((FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)).compContinuousLinearMap (z⁻¹ • 1)) 0 ‖z‖ₑ
w : ℂ
⊢ w ∈ Metric.eball 0 ‖z‖ₑ →
    ((z ^ (a + 1))⁻¹ • fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹) w = (fun x ↦ 1 / (z - x) ^ (a + 1)) w
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
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v

Tactic:
rcases h.contDiffOn' le_rfl (by simp) with ⟨u, u_open, xu, hu⟩

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
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 ω f (insert x s ∩ u)
⊢ (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: case carrier
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
x✝ : X
⊢ x✝ ∈
      ((fun D ↦
            (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius ⋯
              ⋯ ⋯)
          ((fun D ↦
              (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
            D)).carrier ↔
    x✝ ∈ D.carrier

Tactic:
simp [copy_eq]

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: case packingRadius
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
⊢ ↑((fun D ↦
            (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius ⋯
              ⋯ ⋯)
          ((fun D ↦
              (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
            D)).packingRadius =
    ↑D.packingRadius

Tactic:
simp [copy_eq]

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: case coveringRadius
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
⊢ ↑((fun D ↦
            (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius ⋯
              ⋯ ⋯)
          ((fun D ↦
              (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
            D)).coveringRadius =
    ↑D.coveringRadius

Tactic:
simp [copy_eq]

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: case carrier
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
x✝ : Y
⊢ x✝ ∈
      ((fun D ↦ (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
          ((fun D ↦
              (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius
                ⋯ ⋯ ⋯)
            D)).carrier ↔
    x✝ ∈ D.carrier

Tactic:
simp [copy_eq]

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: case packingRadius
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
⊢ ↑((fun D ↦ (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
          ((fun D ↦
              (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius
                ⋯ ⋯ ⋯)
            D)).packingRadius =
    ↑D.packingRadius

Tactic:
simp [copy_eq]

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: case coveringRadius
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
⊢ ↑((fun D ↦ (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
          ((fun D ↦
              (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius
                ⋯ ⋯ ⋯)
            D)).coveringRadius =
    ↑D.coveringRadius

Tactic:
simp [copy_eq]

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

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

Tactic:
rw [expGrowthInf, le_liminf_iff']

Goal state after:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y ≤ (u a).log / ↑a) ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, (b * ↑n).exp ≤ u n
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ (linearGrowthInf fun x ↦ v x + b) ≤ linearGrowthInf v

Tactic:
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: