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 : ι
c : f.Cell j
⊢ f.mapN (Cell.type₂ f c) = { dim := (↑c.s).dim, simplex := (↑c.s).simplex }

Tactic:
dsimp [mapN]
  rw [S.ext_iff, c.ι_b_app_apply, Cell.mapToSucc]
  exact c.map_app_objEquiv_symm_δ_index

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
Y : SSet
w✝¹ : Y.Finite
w✝ : IsFinitelyPresentable Y
p : Y ⟶ X
h✝ : Epi p
⊢ IsFinitelyPresentable X

Tactic:
obtain ⟨Z, _, _, q, _⟩ := exists_epi_from_isCardinalPresentable (pullback p p)

Goal state after:
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
⊢ IsFinitelyPresentable X
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: case mp
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
h : ∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty (Arrow.LiftStruct φ)
⊢ ∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty (Arrow.LiftStruct φ)

Tactic:
β

Goal state after:
case mp
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
h : ∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty (Arrow.LiftStruct φ)
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
⊢ Nonempty (Arrow.LiftStruct β)
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₃
⊢ HasLiftingProperty sq₁₂.ι f₃ ↔ HasLiftingProperty f₂ sq₁₃.π

Tactic:
by
  simp only [Arrow.hasLiftingProperty_iff]
  constructor
  · intro h β
    obtain ⟨α, rfl⟩ := (adj₂.arrowHomEquiv sq₁₂ sq₁₃).surjective β
    exact ⟨adj₂.liftStructEquiv sq₁₂ sq₁₃ α (h α).some⟩
  · intro h α
    exact ⟨(adj₂.liftStructEquiv sq₁₂ sq₁₃ α).symm (h _).some⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ (tensorRight X₃.left).map
        (pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      ((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left ≫
        (α_ X₁.right X₂.right X₃.left).hom ≫
          X₁.right ◁
              pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
            pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
              (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom) =
    (tensorRight X₃.left).map
        (pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      ((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom ≫
        Arrow.Hom.left (whiskerRightIso X₁ X₂).hom ≫
          pushout.desc
            (X₁.right ◁
                pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
              pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
            (pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
              (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
            ⋯

Tactic:
by simp [← whisker_exchange_assoc, Limits.pushout.associator_naturality_left_condition,
            ← comp_whiskerRight_assoc]

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

Goal state before:
pp: case inl.inr.refine_3
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
h₁ : (x.cast hd).simplex.1 i.castSucc = k.castSucc
h₂ : (x.cast hd).simplex.2 i.castSucc = (x.cast hd).simplex.2 (min x hd)
⊢ (x.cast hd).simplex.1 i.castSucc = k.castSucc ∧
    (x.cast hd).simplex.1 i.succ = k.succ ∧ (x.cast hd).simplex.2 i.succ = (x.cast hd).simplex.2 i.castSucc

Tactic:
refine ⟨h₁, ?_, by aesop⟩

Goal state after:
case inl.inr.refine_3
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
h₁ : (x.cast hd).simplex.1 i.castSucc = k.castSucc
h₂ : (x.cast hd).simplex.2 i.castSucc = (x.cast hd).simplex.2 (min x hd)
⊢ (x.cast hd).simplex.1 i.succ = k.succ
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 + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
i : Fin (d + 2)
hu' :
  { dim := u.dim, simplex := u.simplex } =
    { dim := d, simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex }
⊢ i = l.castSucc ∨ i = l.succ

Tactic:
by
  obtain rfl : u.dim = d := congr_arg S.dim hu'
  rw [S.ext_iff] at hu'
  obtain hi | rfl | hi := lt_trichotomy i l.castSucc
  · obtain ⟨l, rfl⟩ := Fin.eq_succ_of_ne_zero (i := l) (by grind)
    refine (hu _ rfl l.succ ?_).elim
    simp [isIndex_succ, S.cast_simplex_rfl, hu', stdSimplex.δ_apply,
      Fin.succAbove_of_lt_succ i l.castSucc hi,
      Fin.succAbove_of_lt_succ i l.succ (by grind), dsimp% hl.simplex_fst_succ,
      dsimp% hl.simplex_snd_succ, dsimp% hl.simplex_fst_castSucc]
  · exact Or.inl rfl
  · obtain rfl | hi := (Fin.castSucc_lt_iff_succ_le.1 hi).eq_or_lt
    · exact Or.inr rfl
    · obtain ⟨l, rfl⟩ := Fin.eq_castSucc_of_ne_last (x := l) (by grind)
      refine (hu _ rfl l.succ ?_).elim
      simp [isIndex_succ, hu', stdSimplex.δ_apply,
        Fin.succAbove_of_castSucc_lt i l.castSucc (by grind),
        Fin.succAbove_of_castSucc_lt i l.succ (by grind),
        dsimp% hl.simplex_fst_castSucc, dsimp% hl.simplex_snd_succ,
        dsimp% hl.simplex_fst_succ]

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

Goal state before:
pp: case pos
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : j ≤ i.castSucc
⊢ ↑((stdSimplex.objEquiv.symm (SimplexCategory.σ i)) j) + ↑0 = ↑j

Tactic:
Fin.coe_ofNat_eq_mod,

Goal state after:
case pos
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : j ≤ i.castSucc
⊢ ↑((stdSimplex.objEquiv.symm (SimplexCategory.σ i)) j) + 0 % 2 = ↑j
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
A : ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
B : ∀ (n : ℕ), #↑(c ^ n • s) = #↑s
⊢ #↑s = #E

Tactic:
apply (Cardinal.mk_of_countable_eventually_mem A B).symm

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOn 𝕜 f (Metric.eball x r)
⊢ r ≤ (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial).radius →
    HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial) x r

Tactic:
rw [Metric.isOpen_eball.analyticOn_iff_analyticOnNhd] at h

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
⊢ r ≤ (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial).radius →
    HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial) x r
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
j : ι
hj : j ≠ i
⊢ Tendsto (fun n ↦ (v j) (c n)) atTop (𝓝 0)

Tactic:
have : 1 < v j a⁻¹ := map_inv₀ (v j) _ ▸
      (one_lt_inv₀ <| (v j).pos fun h ↦ by linarith [map_zero (v _) ▸ h ▸ ha]).2 (haj j hj)

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
j : ι
hj : j ≠ i
this : 1 < (v j) a⁻¹
⊢ Tendsto (fun n ↦ (v j) (c n)) atTop (𝓝 0)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case refine_2.inl
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc : card ι = 2
j : ι
hj : (fun y ↦ y ≠ i) j ∧ ∀ (y : ι), (fun y ↦ y ≠ i) y → y = j
⊢ ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1

Tactic:
let ⟨a, ha⟩ := (v i).exists_one_lt_lt_one_of_not_isEquiv (h i) (h j) (hv hj.1.symm)

Goal state after:
case refine_2.inl
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc : card ι = 2
j : ι
hj : (fun y ↦ y ≠ i) j ∧ ∀ (y : ι), (fun y ↦ y ≠ i) y → y = j
a : R
ha : 1 < (v i) a ∧ (v j) a < 1
⊢ ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun y ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
hy : y ∈ {0}ᶜ
⊢ f y ∈ sphere x r

Tactic:
have : ‖y‖ ≠ 0 := by simpa using hy

Goal state after:
case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun y ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
hy : y ∈ {0}ᶜ
this : ‖y‖ ≠ 0
⊢ f y ∈ sphere x r
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: 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)
⊢ DenseRange ⇑(algebraMap F ((i : ι) → WithAbs (v i)))

Tactic:
by
  classical
  have := Fintype.ofFinite ι
  refine Metric.denseRange_iff.mpr fun z r hr ↦ ?_
  choose a hx using exists_one_lt_lt_one_pi_of_not_isEquiv h hv
  let y := fun n : ℕ ↦ ∑ i, (1 / (1 + (a i)⁻¹ ^ n)) * WithAbs.equiv (v i) (z i)
  have htend : atTop.Tendsto (fun n i ↦ (WithAbs.equiv (v i)).symm (y n)) (𝓝 z) := by
    refine tendsto_pi_nhds.mpr fun u ↦ ?_
    simp_rw [← Fintype.sum_pi_single u z, y, map_sum, map_mul]
    refine tendsto_finsetSum _ fun w _ ↦ ?_
    by_cases hw : u = w
    · rw [← hw, Pi.single_eq_same]
      have hlt : (v u) (a u)⁻¹ < 1 := by
        simpa [← inv_pow, inv_lt_one_iff₀] using Or.inr (hx u).1
      simpa using (WithAbs.tendsto_one_div_one_add_pow_nhds_one hlt).mul_const (z u)
    · rw [Pi.single_eq_of_ne (M := fun i ↦ WithAbs (v i)) hw (z w)]
      have hgt : 1 < (v u) (a w)⁻¹ := by
        rw [map_inv₀]
        refine one_lt_inv_iff₀.mpr ⟨(v u).pos_iff.mpr fun ha ↦ ?_, (hx w).2 u hw⟩
        linarith [map_zero (v w) ▸ ha ▸ (hx w).1]
      have := (v u).tendsto_div_one_add_pow_nhds_zero hgt
      simp_rw [← WithAbs.norm_toAbs_eq] at this
      simpa using (tendsto_zero_iff_norm_tendsto_zero.2 this).mul_const
        ((WithAbs.equiv (v u)).symm _)
  let ⟨N, hN⟩ := Metric.tendsto_atTop.1 htend r hr
  exact ⟨y N, dist_comm z (algebraMap F _ (y N)) ▸ hN N le_rfl⟩

Goal state after:
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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
y : 𝕜
hy : y ∈ U
⊢ (y - x) ^ (s + 1) • deriv F y + deriv (fun u ↦ (u - x) ^ (s + 1)) y • F y =
    (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y

Tactic:
simp [mul_smul, add_smul, Nat.cast_smul_eq_nsmul]

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
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
hts : t ⊆ s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
⊢ f '' s ∈ 𝓝 (f x)

Tactic:
grw [← hts]

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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
hts : t ⊆ s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
⊢ f '' t ∈ 𝓝 (f x)
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
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
⊢ AntilipschitzWith (‖↑f'.symm‖₊⁻¹ - c)⁻¹ (s.domRestrict f)

Tactic:
rcases hc with hE | hc
  · exact AntilipschitzWith.of_subsingleton
  convert! (f'.antilipschitz.domRestrict s).add_lipschitzWith hf.lipschitz_sub hc
  simp [domRestrict]

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

Goal state before:
pp: case refine_2
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
zero : ∃ k < n, ↑k = -a ∨ ↑k = -b ∨ ↑k = -c
⊢ ordinaryHypergeometricSeries 𝔸 a b c n = 0

Tactic:
obtain ⟨_, h, hn⟩ := zero

Goal state after:
case refine_2
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n w✝ : ℕ
h : w✝ < n
hn : ↑w✝ = -a ∨ ↑w✝ = -b ∨ ↑w✝ = -c
⊢ ordinaryHypergeometricSeries 𝔸 a b c n = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: x✝ : ℂ
⊢ logDeriv cos x✝ = (-tan) x✝

Tactic:
rw [logDeriv, Complex.deriv_cos', Pi.div_apply, Pi.neg_apply, Complex.tan, neg_div]

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

Goal state before:
pp: x✝ : ℝ
⊢ logDeriv cos x✝ = (-tan) x✝

Tactic:
rw [logDeriv, Real.deriv_cos', Pi.div_apply, Pi.neg_apply, neg_div, Real.tan_eq_sin_div_cos]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
⊢ multichoose 0 (k + 1) = 0

Tactic:
← nsmul_right_inj (Nat.factorial_ne_zero (k + 1)),

Goal state after:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
⊢ (k + 1).factorial • multichoose 0 (k + 1) = (k + 1).factorial • 0
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ (r + (1 + ↑k • 1)) * (ascPochhammer ℕ k).smeval (r + 1) =
    k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)

Tactic:
add_mul,

Goal state after:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ r * (ascPochhammer ℕ k).smeval (r + 1) + (1 + ↑k • 1) * (ascPochhammer ℕ k).smeval (r + 1) =
    k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case negSucc
k n : ℕ
⊢ (↑k.factorial *
      match -[n+1] with
      | ofNat n => ↑((n + k - 1).choose k)
      | -[n+1] => ↑(↑k).negOnePow * ↑((n + 1).choose k)) =
    (ascPochhammer ℕ k).smeval -[n+1]

Tactic:
| negSucc n =>

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 : ℕ
⊢ (ascPochhammer ℕ n).smeval (-r - ↑n + 1) = (↑n).negOnePow • (descPochhammer ℤ n).smeval (r + ↑n - 1)

Tactic:
show (-r - n + 1) = -(r + n - 1) by abel,

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (ascPochhammer ℕ n).smeval (-(r + ↑n - 1)) = (↑n).negOnePow • (descPochhammer ℤ n).smeval (r + ↑n - 1)
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 : ℕ
hkn : k ≤ n
⊢ n.choose k • (descPochhammer ℤ (k + (n - k))).smeval r =
    n.choose k • ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k))

Tactic:
← descPochhammer_mul,

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • (descPochhammer ℤ k * (descPochhammer ℤ (n - k)).comp (X - ↑k)).smeval r =
    n.choose k • ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k))
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
y : ℝ
f_diff : ∀ (y_1 : ℝ), y_1 ≠ y → HasDerivAt f (g y_1) y_1
hf : ContinuousAt f y
hg : ContinuousAt g y
⊢ HasDerivAt f (g y) y

pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
y : ℝ
hne : y ≠ x
⊢ HasDerivAt f (g y) y

Tactic:
· exact hasDerivAt_of_hasDerivAt_of_ne f_diff hf hg

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
y : ℝ
hne : y ≠ x
⊢ HasDerivAt f (g y) y
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inl
y : ℝ≥0∞
⊢ (∞ * y).log = ∞.log + y.log

Tactic:
rw [log_top]
    rcases ENNReal.trichotomy y with (rfl | rfl | y_real)
    · rw [mul_zero, log_zero, EReal.add_bot]
    · simp
    · rw [log_pos_real' y_real, ENNReal.top_mul', EReal.top_add_coe, log_eq_top_iff]
      simp only [ite_eq_right_iff, zero_ne_top, imp_false]
      exact (ENNReal.toReal_pos_iff.1 y_real).1.ne'

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
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊥ ∨ 0 ≠ ⊤

Tactic:
exact Or.inr EReal.zero_ne_top

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
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊥ ∨ 0 ≠ ⊤

Tactic:
exact Or.inr EReal.zero_ne_top

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

Goal state before:
pp: v : ℕ → ℕ
h : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
M : ℕ
this : Tendsto (fun n ↦ ↑(v n)) atTop (𝓝 ⊤)
n : ℕ
⊢ ↑↑M < ↑(v n) → M ≤ v n

Tactic:
exact_mod_cast le_of_lt

Goal state after: