mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G H : D ⥤ C
inst✝ : HasPullbacks C
f : F ⟶ H
g : G ⟶ H
d : D
⊢ (pullbackObjIso f g d).hom ≫ pullback.snd (f.app d) (g.app d) = (pullback.snd f g).app d

Tactic:
simp [pullbackObjIso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G H : D ⥤ C
inst✝ : HasPullbacks C
f : F ⟶ H
g : G ⟶ H
d : D
⊢ (pullbackObjIso f g d).inv ≫ (pullback.fst f g).app d = pullback.fst (f.app d) (g.app d)

Tactic:
simp [pullbackObjIso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G H : D ⥤ C
inst✝ : HasPullbacks C
f : F ⟶ H
g : G ⟶ H
d : D
⊢ (pullbackObjIso f g d).inv ≫ (pullback.snd f g).app d = pullback.snd (f.app d) (g.app d)

Tactic:
simp [pullbackObjIso]

Goal state after:
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
j : ι
c : f.Cell j
d : ℕ
⊢ Function.Injective ⇑(ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋d⦌)))

Tactic:
intro x y h

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
d : ℕ
x y : Δ[c.dim + 1] _⦋d⦌
h :
  (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋d⦌))) x =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋d⦌))) y
⊢ x = y
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a.notMem
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
⊢ s.subcomplex ≤ f.filtration j

Tactic:
rw [← c.rank_s]

Goal state after:
case a.notMem
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
⊢ s.subcomplex ≤ f.filtration (f.rank c.s)
Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C κ)

Tactic:
rw [h.isPresentable_eq_retractClosure]
  infer_instance

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 sq₁₂.ι ⟶ Arrow.mk f₃
l : Arrow.LiftStruct ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)
this : l.l ≫ (G.obj (op Y₁)).map f₃ = adj₂.homEquiv (Arrow.Hom.right α)
⊢ adj₂.homEquiv.symm l.l ≫ f₃ = Arrow.Hom.right α

Tactic:
← adj₂.homEquiv_symm_naturality_three,

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 sq₁₂.ι ⟶ Arrow.mk f₃
l : Arrow.LiftStruct ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)
this : l.l ≫ (G.obj (op Y₁)).map f₃ = adj₂.homEquiv (Arrow.Hom.right α)
⊢ adj₂.homEquiv.symm (l.l ≫ (G.obj (op Y₁)).map f₃) = Arrow.Hom.right α
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: X₁ Y₁ E✝ B✝ : SSet
i : X₁ ⟶ Y₁
p✝ : E✝ ⟶ B✝
inst✝¹ : Mono i
inst✝ : InnerFibration p✝
sq₁₃ : internalHom.PullbackObjObj i p✝
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
n✝ : ℕ
k : Fin (n✝ + 3)
h0 : 0 < k
hn : k < Fin.last (n✝ + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[n✝ + 2, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[n✝ + 2, k].ι
E B : SSet
p : E ⟶ B
hp : innerFibrations p
sq₁₃' : internalHom.PullbackObjObj Λ[n✝ + 2, k].ι p := Functor.PullbackObjObj.ofHasPullback internalHom Λ[n✝ + 2, k].ι p
X Y : SSet
n : ℕ
⊢ HasLiftingProperty ∂Δ[n].ι sq₁₃'.π

Tactic:
rw [← internalHomAdjunction₂.hasLiftingProperty_iff
    (Subcomplex.unionProd.pushoutObjObj.{u} _ _),
    Subcomplex.unionProd.pushoutObjObj_ι]

Goal state after:
X₁ Y₁ E✝ B✝ : SSet
i : X₁ ⟶ Y₁
p✝ : E✝ ⟶ B✝
inst✝¹ : Mono i
inst✝ : InnerFibration p✝
sq₁₃ : internalHom.PullbackObjObj i p✝
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
n✝ : ℕ
k : Fin (n✝ + 3)
h0 : 0 < k
hn : k < Fin.last (n✝ + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[n✝ + 2, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[n✝ + 2, k].ι
E B : SSet
p : E ⟶ B
hp : innerFibrations p
sq₁₃' : internalHom.PullbackObjObj Λ[n✝ + 2, k].ι p := Functor.PullbackObjObj.ofHasPullback internalHom Λ[n✝ + 2, k].ι p
X Y : SSet
n : ℕ
⊢ HasLiftingProperty (Λ[n✝ + 2, k].unionProd ∂Δ[n]).ι p
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct

Goal state before:
pp: X₁ Y₁ E✝ B✝ : SSet
i : X₁ ⟶ Y₁
p✝ : E✝ ⟶ B✝
inst✝¹ : Mono i
inst✝ : Fibration p✝
sq₁₃ : internalHom.PullbackObjObj i p✝
m : ℕ
X✝ Y✝ : SSet
k : Fin (m + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[m + 1, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[m + 1, k].ι
E B : SSet
p : E ⟶ B
hp : fibrations SSet p
sq₁₃' : internalHom.PullbackObjObj Λ[m + 1, k].ι p := Functor.PullbackObjObj.ofHasPullback internalHom Λ[m + 1, k].ι p
X Y : SSet
n : ℕ
⊢ HasLiftingProperty ∂Δ[n].ι sq₁₃'.π

Tactic:
rw [← internalHomAdjunction₂.hasLiftingProperty_iff
    (Subcomplex.unionProd.pushoutObjObj.{u} _ _),
    Subcomplex.unionProd.pushoutObjObj_ι]

Goal state after:
X₁ Y₁ E✝ B✝ : SSet
i : X₁ ⟶ Y₁
p✝ : E✝ ⟶ B✝
inst✝¹ : Mono i
inst✝ : Fibration p✝
sq₁₃ : internalHom.PullbackObjObj i p✝
m : ℕ
X✝ Y✝ : SSet
k : Fin (m + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[m + 1, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[m + 1, k].ι
E B : SSet
p : E ⟶ B
hp : fibrations SSet p
sq₁₃' : internalHom.PullbackObjObj Λ[m + 1, k].ι p := Functor.PullbackObjObj.ofHasPullback internalHom Λ[m + 1, k].ι p
X Y : SSet
n : ℕ
⊢ HasLiftingProperty (Λ[m + 1, k].unionProd ∂Δ[n]).ι p
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 + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
y : Fin (d + 1)
hy : y ∈ finset hl.δ ⋯
⊢ l ≤ y

Tactic:
simp only [mem_finset_iff, Monoidal.tensorObj_obj, S.cast_dim,
      S.cast_simplex_rfl, prod_δ_fst, stdSimplex.δ_apply] at hy

Goal state after:
case refine_2
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
y : Fin (d + 1)
hy : (x.cast hd).simplex.1 (l.castSucc.succAbove y) = k.succ
⊢ l ≤ y
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
⊢ stdSimplex.δ j.castSucc.succ ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv h.map)) = fg.map

Tactic:
by
    simp [stdSimplex.δ_comp_yonedaEquiv_symm, δ_opObjEquiv,
      ← stdSimplex.yonedaEquiv_δ_comp, ← hij, Fin.rev_castSucc, Fin.rev_succ]

Goal state after:
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 : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop
hcⱼ : ∀ (j : ι), j ≠ i → ∀ s ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}, 0 ∈ s → (fun n ↦ (v j) (c n)) ⁻¹' s ∈ atTop
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1

Tactic:
mem_atTop_sets,

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 : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop
hcⱼ :
  ∀ (j : ι),
    j ≠ i →
      ∀ s ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}, 0 ∈ s → ∃ a, ∀ (b : ℕ), a ≤ b → b ∈ (fun n ↦ (v j) (c n)) ⁻¹' s
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case «1»
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 := ⦋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 := ⦋1⦌, property := _proof_12 })
⊢ ((hY.spineEquiv 2 f₂._proof_4)
          (f₂ f₀ f₁ hδ₁ hδ₀ hY ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_15 _proof_12).op)) x))).arrow
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    ((hY.spineEquiv 2 f₂._proof_4) ((ConcreteCategory.hom (Y.map (σ₂ 0 _proof_15 _proof_12).op)) (f₁ x))).arrow
      ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
dsimp
    rw [spineEquiv_f₂_arrow_one]
    simp [StrictSegal.spineEquiv, SimplexCategory.mkOfSucc_one_eq_δ,
      ← Functor.map_comp_apply, ← op_comp]

Goal state after:
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))
hcₙ : Tendsto (fun n ↦ w (c n)) atTop (𝓝 (w b))
hcⱼ : ∀ (j : ι), j ≠ i → ∀ s ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}, 0 ∈ s → (fun n ↦ (v j) (c n)) ⁻¹' s ∈ atTop
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1

Tactic:
mem_atTop_sets,

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))
hcₙ : Tendsto (fun n ↦ w (c n)) atTop (𝓝 (w b))
hcⱼ :
  ∀ (j : ι),
    j ≠ i →
      ∀ s ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}, 0 ∈ s → ∃ a, ∀ (b : ℕ), a ≤ b → b ∈ (fun n ↦ (v j) (c n)) ⁻¹' s
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : CharZero 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
⊢ AnalyticAt 𝕜 (g ∘ f) x ↔ AnalyticAt 𝕜 g (f x)

Tactic:
refine ⟨fun hg ↦ ?_, (AnalyticAt.comp · hf)⟩

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : CharZero 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
⊢ AnalyticAt 𝕜 g (f x)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case pos.inr.inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : w a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : w b ≠ 1
⊢ v b ^ (log (w a) / log (v a)) = w b

Tactic:
rw [← h.symm.log_div_log_eq_log_div_log ha₀ ha₁ hb₀ hb₁, div_eq_inv_mul, rpow_mul (v.nonneg _),
      rpow_inv_log (v.pos hb₀) (h.eq_one_iff.not.2 hb₁), exp_one_rpow, exp_log (w.pos hb₀)]

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : U ∈ 𝓝 0
⊢ ⇑(WithAbs.congr v w (RingEquiv.refl F)) '' U ∈ 𝓝 0

Tactic:
by
  rw [Metric.mem_nhds_iff] at hU ⊢
  obtain ⟨ε, hε, hU⟩ := hU
  obtain ⟨c, hc, hvw⟩ := isEquiv_iff_exists_rpow_eq.1 h
  refine ⟨ε ^ c, rpow_pos_of_pos hε _, fun x hx ↦ ?_⟩
  rw [← RingEquiv.apply_symm_apply (WithAbs.congr v w (.refl F)) x]
  refine Set.mem_image_of_mem _ (hU ?_)
  rw [Metric.mem_ball, dist_zero_right, WithAbs.norm_eq_apply_ofAbs, ← funext_iff.1 hvw,
    rpow_lt_rpow_iff (v.nonneg _) hε.le hc] at hx
  simpa [WithAbs.norm_eq_apply_ofAbs]

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

Goal state before:
pp: case neg.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
f' : 𝕜 → 𝕜
h₁f' : AnalyticAt 𝕜 f' z₀
h₂f' : f' z₀ ≠ 0
h₃f' : f =ᶠ[𝓝 z₀] fun z ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z
g' : 𝕜 → E
h₁g' : AnalyticAt 𝕜 g' z₀
h₂g' : g' z₀ ≠ 0
h₃g' : g =ᶠ[𝓝 z₀] fun z ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z
t : Set 𝕜
h₁t : ∀ y ∈ t, f y = (fun z ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z) y
h₂t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h₃t : z₀ ∈ t
s : Set 𝕜
h₁s : ∀ y ∈ s, g y = (fun z ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z) y
h₂s : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h₃s : z₀ ∈ s
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f • g) z = (z - z₀) ^ (analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀) • (f' • g') z

Tactic:
exact eventually_nhds_iff.2
      ⟨t ∩ s, fun y hy ↦ (by simp [h₁t y hy.1, h₁s y hy.2]; module), h₂t.inter h₂s, h₃t, h₃s⟩

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
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : U ∈ 𝓝 0
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / ↑i.factorial) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
hz : z ∉ U
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      z ^ n • (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0)

Tactic:
smul_inv_smul₀

Goal state after:
case neg
𝕜 : 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 : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : U ∈ 𝓝 0
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / ↑i.factorial) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
hz : z ∉ U
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      (f z - ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0)

case neg.ha
𝕜 : 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 : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : U ∈ 𝓝 0
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / ↑i.factorial) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
hz : z ∉ U
⊢ z ^ n ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case convert_5
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
⊢ Tendsto (fun k ↦ (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))) atTop (𝓝 1)

Tactic:
apply (mul_one (1 : 𝕂)) ▸ Filter.Tendsto.mul <;>
  convert! tendsto_add_mul_div_add_mul_atTop_nhds _ _ (1 : 𝕂) one_ne_zero <;> simp

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = g x_1
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (fun z ↦ z - x) x
z : 𝕜
hz : z ∈ {x}ᶜ → f z = g z
hn : z ≠ x
⊢ (z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z

Tactic:
hz (Set.mem_compl_singleton_iff.mp hn),

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = g x_1
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (fun z ↦ z - x) x
z : 𝕜
hz : z ∈ {x}ᶜ → f z = g z
hn : z ≠ x
⊢ (z - x) • (z - x) ^ m • g z = (z - x) ^ (m + 1) • g z
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 : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin φ s x = fun i ↦ derivWithin (fun x ↦ φ x i) s x

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

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (ascPochhammer ℤ n).smeval r * (X + ↑n).smeval r = (ascPochhammer ℕ n).smeval r * (X + ↑n).smeval r

Tactic:
rw [smeval_ascPochhammer_int_ofNat r n]

Goal state after:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (ascPochhammer ℕ n).smeval r * (X + ↑n).smeval r = (ascPochhammer ℕ n).smeval r * (X + ↑n).smeval r
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 : ℕ
⊢ (descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - ↑n + 1)

Tactic:
descPochhammer_eq_ascPochhammer,

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

Tactic:
choose_one_right',

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
⊢ r ^ 1 = r
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ r * (descPochhammer ℤ k).smeval r + (descPochhammer ℤ k).smeval r =
    (descPochhammer ℤ k).smeval r + (r * (descPochhammer ℤ k).smeval r - ↑k • 1 * (descPochhammer ℤ k).smeval r) +
      k • (descPochhammer ℤ k).smeval r

Tactic:
← add_sub_assoc,

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

Tactic:
by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1))]
  simp only [smul_add, ← descPochhammer_eq_factorial_smul_choose]
  rw [Nat.factorial_succ, mul_smul,
    ← descPochhammer_eq_factorial_smul_choose r, descPochhammer_succ_succ_smeval r k]

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

Goal state before:
pp: case inl
⊢ (deriv fun x ↦ x ^ 0) =O[atTop] fun x ↦ x ^ (0 - 1)

pp: case inr
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x ↦ x ^ p) =O[atTop] fun x ↦ x ^ (p - 1)

Tactic:
case inl =>
    simp [zero_sub, Real.rpow_neg_one, Real.rpow_zero, deriv_const', Asymptotics.isBigO_zero]

Goal state after:
case inr
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x ↦ x ^ p) =O[atTop] fun x ↦ x ^ (p - 1)
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
x : X
⊢ ∃ y ∈ D, dist x y ≤ ↑D.coveringRadius

Tactic:
obtain ⟨y, hy, hdist⟩ := D.isCover_coveringRadius (x := x) (by trivial)
  exact ⟨y, hy, by simpa [edist_dist] using hdist⟩

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

Goal state before:
pp: ⊢ StrictMono exp

Tactic:
intro x y h

Goal state after:
x y : EReal
h : x < y
⊢ x.exp < y.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: ⊢ StrictMono log

Tactic:
intro x y h

Goal state after:
x y : ℝ≥0∞
h : x < y
⊢ x.log < y.log
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inl.inr.inr
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
⊢ (x ^ y).log = ↑y * x.log

Tactic:
simp only [log, rpow_eq_zero_iff, x_ne_zero, false_and, x_ne_top, or_self, ↓reduceIte,
        rpow_eq_top_iff]

Goal state after:
case inl.inr.inr
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
⊢ ↑(Real.log (x ^ y).toReal) = ↑y * ↑(Real.log x.toReal)