mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case h₂.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₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝ : Arrow C₃
⊢ Arrow.Hom.right
        ({
                app := fun X₂ ↦
                  Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                    (pullback.lift
                      (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                      (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj X₂).right))) ⋯)
                    ⋯,
                naturality := ⋯ }.app
            ((G.leibnizPullback.obj (op X₁)).obj x✝) ≫
          (G.leibnizPullback.obj (op X₁)).map
            ({
                  app := fun X₃ ↦
                    Arrow.homMk
                      (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj X₃).left))
                        (adj₂.homEquiv.symm
                          (pullback.fst ((G.obj (op (unop (op X₁)).left)).map X₃.hom)
                            ((G.map (unop (op X₁)).hom.op).app X₃.right)))
                        ⋯)
                      (adj₂.homEquiv.symm
                        (pullback.snd ((G.obj (op (unop (op X₁)).left)).map X₃.hom)
                          ((G.map (unop (op X₁)).hom.op).app X₃.right)))
                      ⋯,
                  naturality := ⋯ }.app
              x✝)) ≫
      pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝.hom) ((G.map (unop (op X₁)).hom.op).app x✝.right) =
    Arrow.Hom.right (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝)) ≫
      pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝.hom) ((G.map (unop (op X₁)).hom.op).app x✝.right)

Tactic:
simp [← homEquiv_naturality_three]

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₂
adj₂ : F ⊣₂ G
X₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝ : Arrow C₃
⊢ Arrow.Hom.right
        ({
                app := fun X₂ ↦
                  Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                    (pullback.lift
                      (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                      (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj X₂).right))) ⋯)
                    ⋯,
                naturality := ⋯ }.app
            ((G.leibnizPullback.obj (op X₁)).obj x✝) ≫
          (G.leibnizPullback.obj (op X₁)).map
            ({
                  app := fun X₃ ↦
                    Arrow.homMk
                      (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj X₃).left))
                        (adj₂.homEquiv.symm
                          (pullback.fst ((G.obj (op (unop (op X₁)).left)).map X₃.hom)
                            ((G.map (unop (op X₁)).hom.op).app X₃.right)))
                        ⋯)
                      (adj₂.homEquiv.symm
                        (pullback.snd ((G.obj (op (unop (op X₁)).left)).map X₃.hom)
                          ((G.map (unop (op X₁)).hom.op).app X₃.right)))
                      ⋯,
                  naturality := ⋯ }.app
              x✝)) ≫
      pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝.hom) ((G.map (unop (op X₁)).hom.op).app x✝.right) =
    Arrow.Hom.right (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝)) ≫
      pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝.hom) ((G.map (unop (op X₁)).hom.op).app x✝.right)

Tactic:
simp [← homEquiv_naturality_three]

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

Goal state before:
pp: X : TopCat
s : toSSet.obj X _⦋1⦌
⊢ (CategoryTheory.ConcreteCategory.hom (toSSetObj₁Equiv s)) 0 =
    toSSetObj₀Equiv ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (toSSet.obj X) 1)) s)

Tactic:
simp [toSSetObj₀Equiv, toSSetObj₁Equiv, -ContinuousMap.coe_mk,
    Subsingleton.elim (default : stdSimplex ℝ (Fin 1)) (stdSimplex.vertex 0)]

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

Goal state before:
pp: X : TopCat
s : toSSet.obj X _⦋1⦌
⊢ (CategoryTheory.ConcreteCategory.hom (toSSetObj₁Equiv s)) 1 =
    toSSetObj₀Equiv ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (toSSet.obj X) 0)) s)

Tactic:
simp [toSSetObj₀Equiv, toSSetObj₁Equiv, -ContinuousMap.coe_mk,
    Subsingleton.elim (default : stdSimplex ℝ (Fin 1)) (stdSimplex.vertex 0)]

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
⊢ ∀ ⦃y : E⦄, y ∈ sᶜ → JoinedIn sᶜ a y

Tactic:
intro b

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
⊢ b ∈ sᶜ → JoinedIn sᶜ a b
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
B : {t | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t : ℝ
z : E := c + t • y
ht : [c + x -[ℝ] c + t • y] ∩ s = ∅ ∧ [c - x -[ℝ] c + t • y] ∩ s = ∅
⊢ [a -[ℝ] z] ∩ s = ∅

Tactic:
convert! ht.2

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
B : {t | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t : ℝ
z : E := c + t • y
ht : [c + x -[ℝ] c + t • y] ∩ s = ∅ ∧ [c - x -[ℝ] c + t • y] ∩ s = ∅
⊢ a = c - x
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
this :
  ∀ {a : F},
    a ≠ 0 →
      v a ≠ 1 →
        ∀ {b : F},
          b ≠ 0 →
            v b ≠ 1 →
              log (v b) / log (w b) ≠ log (v a) / log (w a) →
                1 < v a → 1 < v b → log (v b) / log (w b) < log (v a) / log (w a) → False
h_lt : log (v a) / log (w a) ≤ log (v b) / log (w b)
⊢ False

pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
h_lt : log (v b) / log (w b) < log (v a) / log (w a)
⊢ False

Tactic:
· exact this hb₀ hb₁ ha₀ ha₁ h_ne.symm hb ha <| lt_of_le_of_ne h_lt h_ne.symm

Goal state after:
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
h_lt : log (v b) / log (w b) < log (v a) / log (w a)
⊢ False
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: case hbc
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := ⋯
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := ⋯
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
n : ℕ
w : E
hw : dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ 1 - (↑c * ↑f'symm.nnnorm) ^ n ≤ 1

Tactic:
sub_le_self_iff

Goal state after:
case hbc
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
n : ℕ
w : E
hw : dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ 0 ≤ (↑c * ↑f'symm.nnnorm) ^ n
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case refine_2
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : U ∈ Filter.map (⇑(↑(WithAbs.congr v w (RingEquiv.refl F))).symm) (𝓝 0)
s : Set (WithAbs w)
hs : s ∈ 𝓝 0
hss : ⇑↑(WithAbs.congr v w (RingEquiv.refl F)).symm '' s ⊆ U
⊢ U ∈ 𝓝 0

Tactic:
WithAbs.congr_symm

Goal state after:
case refine_2
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : U ∈ Filter.map (⇑(↑(WithAbs.congr v w (RingEquiv.refl F))).symm) (𝓝 0)
s : Set (WithAbs w)
hs : s ∈ 𝓝 0
hss : ⇑↑(WithAbs.congr w v (RingEquiv.refl F).symm) '' s ⊆ U
⊢ U ∈ 𝓝 0
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)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : ¬u = w
⊢ 1 < (v u) (a w)⁻¹

Tactic:
rw [map_inv₀]

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : ¬u = w
⊢ 1 < ((v u) (a w))⁻¹
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)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
htend : Tendsto (fun n i ↦ (WithAbs.equiv (v i)).symm (y n)) atTop (𝓝 z)
N : ℕ
hN : ∀ n ≥ N, dist (fun i ↦ (WithAbs.equiv (v i)).symm (y n)) z < r
⊢ ∃ y, dist z ((algebraMap F ((i : ι) → WithAbs (v i))) y) < r

Tactic:
exact ⟨y N, dist_comm z (algebraMap F _ (y N)) ▸ hN N le_rfl⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: x✝ : ℝ
hx : 0 < x✝
x : ℝ
⊢ Real.log x = (log ↑x).re

Tactic:
exact (Complex.log_ofReal_re x).symm

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

Goal state before:
pp: 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 ^ n = 0
⊢ z ∈ U

Tactic:
exact (pow_eq_zero_iff'.mp hz).1 ▸ mem_of_mem_nhds hU0

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
⊢ (fderivWithin 𝕜 φ s x) 1 = fun i ↦ derivWithin (fun x ↦ φ x i) s x

Tactic:
fderivWithin_pi h hsx

Goal state after:
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
⊢ (ContinuousLinearMap.pi fun i ↦ fderivWithin 𝕜 (fun x ↦ φ x i) s x) 1 = fun i ↦ derivWithin (fun x ↦ φ x i) s x
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
⊢ (descPochhammer ℤ (k + 1)).smeval ↑n = ↑(n.descFactorial (k + 1))

Tactic:
rw [descPochhammer_succ_right, Nat.descFactorial_succ, smeval_mul, ih, mul_comm, Nat.cast_mul,
      smeval_sub, smeval_X, smeval_natCast, npow_one, npow_zero, nsmul_one]
    by_cases! h : n < k
    · simp only [Nat.descFactorial_eq_zero_iff_lt.mpr h, Nat.cast_zero, zero_mul]
    · rw [Nat.cast_sub h]

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicAt (f ∘ fun x ↦ x + c) x
⊢ MeromorphicAt ((f ∘ fun x ↦ x + c) ∘ fun z ↦ z - c) (x + c)

Tactic:
show x = (x + c) - c by ring

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicAt (f ∘ fun x ↦ x + c) (x + c - c)
⊢ MeromorphicAt ((f ∘ fun x ↦ x + c) ∘ fun z ↦ z - c) (x + c)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicOn (f ∘ fun x ↦ x + c) U
y : 𝕜
hy : y ∈ U + {c}
⊢ MeromorphicAt f y

Tactic:
add_singleton,

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicOn (f ∘ fun x ↦ x + c) U
y : 𝕜
hy : y ∈ (fun x ↦ x + c) '' U
⊢ MeromorphicAt f y
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: 𝕂 : Type v
inst✝² : RCLike 𝕂
𝔸 : Type u
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ ↑k
⊢ (binomialSeries 𝔸 a).radius = 1

Tactic:
by
  simp only [binomialSeries_eq_ordinaryHypergeometricSeries (b := (1 : 𝕂)) (by norm_cast; simp),
    FormalMultilinearSeries.radius_compNeg]
  conv at ha => ext; rw [ne_comm]
  exact ordinaryHypergeometricSeries_radius_eq_one _ _ _ _ (by norm_cast; grind)

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

Goal state before:
pp: 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
⊢ HasDerivAt f (g x) x

Tactic:
have A : HasDerivWithinAt f (g x) (Ici x) x := by
    have diff : DifferentiableOn ℝ f (Ioi x) := fun y hy =>
      (f_diff y (ne_of_gt hy)).differentiableAt.differentiableWithinAt
    -- next line is the nontrivial bit of this proof, appealing to differentiability
    -- extension results.
    apply
      hasDerivWithinAt_Ici_of_tendsto_deriv diff hf.continuousWithinAt
        self_mem_nhdsWithin
    have : Tendsto g (𝓝[>] x) (𝓝 (g x)) := tendsto_inf_left hg
    apply this.congr' _
    apply mem_of_superset self_mem_nhdsWithin fun y hy => _
    intro y hy
    exact (f_diff y (ne_of_gt hy)).deriv.symm

Goal state after:
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
A : HasDerivWithinAt f (g x) (Ici x) x
⊢ HasDerivAt f (g x) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inr
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y ↦ ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)

Tactic:
suffices HasDerivAt (fun y : ℂ => y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x) by
      exact this.comp_ofReal

Goal state after:
case inr
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y ↦ y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x)
Module: Mathlib.Analysis.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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z ↦ (p n) fun x_1 ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := fun k ↦ if h : n = k then h ▸ p n else 0
m : ℕ
⊢ n + 1 ≤ m → q m = 0

Tactic:
hm

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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z ↦ (p n) fun x_1 ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := fun k ↦ if h : n = k then h ▸ p n else 0
m : ℕ
hm : n + 1 ≤ m
⊢ q m = 0
Module: Mathlib.Topology.MetricSpace.MetricSeparated

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
s : Set X
ε : ℝ≥0∞
⊢ IsSeparated ε s ↔ SetRel.IsSeparated {(x, y) | edist x y ≤ ε} s

Tactic:
simp [IsSeparated, SetRel.IsSeparated]

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

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

Tactic:
exact (isTheta_deriv_rpow_const_atTop hp).1

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

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
x y : X
hx : x ∈ D
hy : y ∈ D
hne : x ≠ y
⊢ ↑D.packingRadius < dist x y

Tactic:
by
  have hsep : ENNReal.ofReal D.packingRadius < ENNReal.ofReal (dist x y) := by
    simpa [edist_dist] using D.isSeparated_packingRadius hx hy hne
  exact (ENNReal.ofReal_lt_ofReal_iff (h := dist_pos.mpr hne)).1 hsep

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Z : Type u_3
inst✝ : MetricSpace Z
D : DeloneSet X
f : X ≃ Y
g : Y ≃ Z
K₁f K₂f K₁g K₂g : ℝ≥0
hf₁_pos : 0 < K₁f
hf₂_pos : 0 < K₂f
hg₁_pos : 0 < K₁g
hg₂_pos : 0 < K₂g
hf_anti : AntilipschitzWith K₁f ⇑f
hf_lip : LipschitzWith K₂f ⇑f
hg_anti : AntilipschitzWith K₁g ⇑g
hg_lip : LipschitzWith K₂g ⇑g
⊢ mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip (mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D) =
    mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D

Tactic:
by
  ext
  · simp only [mapBilipschitz_carrier, Equiv.trans_apply, Set.mem_image]
    exact exists_exists_and_eq_and
  · simp only [mapBilipschitz_packingRadius, NNReal.coe_div, div_div]
  · simp only [mapBilipschitz_coveringRadius, NNReal.coe_mul, mul_assoc]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → EReal
⊢ linearGrowthSup (⨆ x ∈ Set.univ, u x) = ⨆ i, linearGrowthSup (u i)

Tactic:
linearGrowthSup_biSup u Set.finite_univ,

Goal state after:
ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → EReal
⊢ ⨆ x ∈ Set.univ, linearGrowthSup (u x) = ⨆ i, linearGrowthSup (u i)
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
⊢ (v.enlarge δ δpos).filterAt = v.filterAt

Tactic:
ext1 x
  suffices {t | MeasurableSet t → (interior t).Nonempty → ¬t ⊆ closedBall x δ →
      t ∈ v.setsAt x} ∈ (𝓝 x).smallSets by
    simpa [VitaliFamily.filterAt, VitaliFamily.enlarge, ← sup_principal, inf_sup_left,
      mem_inf_principal]
  filter_upwards [eventually_smallSets_subset.mpr (closedBall_mem_nhds _ δpos)]
  simp +contextual

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

Goal state before:
pp: u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
⊢ expGrowthInf u ≤ expGrowthInf v

Tactic:
apply (expGrowthInf_eventually_monotone h).trans
  rcases eq_zero_or_pos b with rfl | b_pos
  · simp only [zero_mul, ← Pi.zero_def, expGrowthInf_zero, bot_le]
  · apply (expGrowthInf_mul_le _ _).trans_eq <;> rw [expGrowthSup_const b_pos.ne' hb]
    · exact zero_add (expGrowthInf v)
    · exact .inl zero_ne_bot
    · exact .inl zero_ne_top

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
⊢ μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0

Tactic:
let s := {x | g x + ε ≤ f x ∧ g x ≤ N} ∩ spanningSets μ p

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p
⊢ μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0