mathlib-initiative/mathlib-tactics huggingface dataset:
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 m : ℕ
k : Fin (m + 2)
n : ℕ
hk : k = Fin.last (m + 1)
⊢ (Λ[m + 1, 0].op.unionProd ∂Δ[n].op).preimage ((stdSimplex.opIso ⦋m + 1⦌).inv ⊗ₘ (stdSimplex.opIso ⦋n⦌).inv) =
    Λ[m + 1, Fin.last (m + 1)].unionProd ∂Δ[n]

Tactic:
Subcomplex.preimage_unionProd,

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 2)
n : ℕ
hk : k = Fin.last (m + 1)
⊢ (Λ[m + 1, 0].op.preimage (stdSimplex.opIso ⦋m + 1⦌).inv).unionProd (∂Δ[n].op.preimage (stdSimplex.opIso ⦋n⦌).inv) =
    Λ[m + 1, Fin.last (m + 1)].unionProd ∂Δ[n]
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms

Goal state before:
pp: ⊢ (monomorphisms (SimplexCategoryᵒᵖ ⥤ Type u_1)).IsStableUnderCobaseChange

Tactic:
rw [← functorCategory_monomorphisms]

Goal state after:
⊢ ((monomorphisms (Type u_1)).functorCategory SimplexCategoryᵒᵖ).IsStableUnderCobaseChange
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms

Goal state before:
pp: J : Type u
x✝¹ : Category.{u, u} J
x✝ : IsFiltered J
⊢ (monomorphisms (SimplexCategoryᵒᵖ ⥤ Type u)).IsStableUnderColimitsOfShape J

Tactic:
rw [← functorCategory_monomorphisms]

Goal state after:
J : Type u
x✝¹ : Category.{u, u} J
x✝ : IsFiltered J
⊢ ((monomorphisms (Type u)).functorCategory SimplexCategoryᵒᵖ).IsStableUnderColimitsOfShape J
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: X : TopCat
⊢ ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I

Tactic:
apply CartesianMonoidalCategory.hom_ext <;> simp [← Functor.map_comp]

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

Goal state before:
pp: X : TopCat
⊢ ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I

Tactic:
apply CartesianMonoidalCategory.hom_ext <;> simp [← Functor.map_comp]

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

Goal state before:
pp: case h'f
α : Type u
ι : Type v
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
g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (fun x ↦ ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift.{u, v} ι) := Filter.map ULift.up l
i : ULift.{u, v} ι
⊢ #↑(g i) ≤ lift.{v, u} a

Tactic:
simpa [g] using! h'f i.down

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 : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 := FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial
hr : r ≤ p.radius
g : 𝕜 → 𝕜 := fun t ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall g p x p.radius
hg' :
  IsPreconnected (Metric.eball x r) →
    ∀ {z₀ : 𝕜}, z₀ ∈ Metric.eball x r → f =ᶠ[nhds z₀] g → Set.EqOn f g (Metric.eball x r)
⊢ x ∈ Metric.eball x r

Tactic:
by simp [hr_pos]

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

Goal state before:
pp: case refine_2.inr.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
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a = 1
⊢ ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1

Tactic:
let ⟨c, hc⟩ := exists_one_lt_lt_one_pi_of_eq_one ha.1 ha.2 ha₁ hb.1 (hb.2 ⟨j, .inr rfl⟩
        (by grind))
      refine ⟨c, hc.1, fun k hk ↦ ?_⟩
      rcases eq_or_ne k j with (rfl | h); try exact hc.2.2; exact hc.2.1 ⟨k, h⟩ (by grind)

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
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
x y : E
⊢ f x - f y - f' (x - y) = (f - ⇑f') x - (f - ⇑f') y

Tactic:
by
    simp only [map_sub, Pi.sub_apply]; abel

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
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
⊢ log (v b) / log (w b) = log (v a) / log (w a)

Tactic:
by
  by_contra! h_ne
  wlog! ha : 1 < v a generalizing a b
  · apply this (inv_ne_zero ha₀) (by simpa) hb₀ hb₁ (by simpa)
    simpa using one_lt_inv_iff₀.2 ⟨v.pos ha₀, ha₁.lt_of_le ha⟩
  wlog! hb : 1 < v b generalizing a b
  · apply this ha₀ ha₁ (inv_ne_zero hb₀) (by simpa) (by simpa) ha
    simpa using one_lt_inv_iff₀.2 ⟨v.pos hb₀, hb₁.lt_of_le hb⟩
  wlog! h_lt : (v b).log / (w b).log < (v a).log / (w a).log generalizing a b
  · exact this hb₀ hb₁ ha₀ ha₁ h_ne.symm hb ha <| lt_of_le_of_ne h_lt h_ne.symm
  have hwa := h.one_lt_iff.1 ha
  have hwb := h.one_lt_iff.1 hb
  rw [div_lt_div_iff₀ (log_pos hwb) (log_pos hwa), mul_comm (v a).log,
    ← div_lt_div_iff₀ (log_pos ha) (log_pos hwa)] at h_lt
  let ⟨q, ⟨hq₁, hq₂⟩⟩ := exists_rat_btwn h_lt
  rw [← Rat.num_div_den q, Rat.cast_div, Rat.cast_intCast, Rat.cast_natCast] at hq₁ hq₂
  rw [div_lt_div_iff₀ (log_pos ha) (by simp [q.den_pos]), mul_comm, ← log_pow, ← log_zpow,
    log_lt_log_iff (pow_pos (by linarith) _) (zpow_pos (by linarith) _),
    ← div_lt_one (zpow_pos (by linarith) _), ← map_pow, ← map_zpow₀, ← map_div₀] at hq₁
  rw [div_lt_div_iff₀ (by simp [q.den_pos]) (log_pos hwa), mul_comm (w _).log,
    ← log_pow, ← log_zpow, log_lt_log_iff (zpow_pos (by linarith) _) (pow_pos (by linarith) _),
    ← one_lt_div (zpow_pos (by linarith) _), ← map_pow, ← map_zpow₀, ← map_div₀] at hq₂
  exact not_lt_of_gt (h.lt_one_iff.1 hq₁) hq₂

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
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
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
this : CauchySeq u
x : E
hx : Tendsto u atTop (𝓝 x)
xmem : x ∈ closedBall b ε
⊢ f x = y

Tactic:
have hx' : Tendsto u atTop (𝓝[closedBall b ε] x) := by
    simp only [nhdsWithin, tendsto_inf, hx, true_and, tendsto_principal]
    exact Eventually.of_forall fun n => C n _ (D n).2

Goal state after:
case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
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
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
this : CauchySeq u
x : E
hx : Tendsto u atTop (𝓝 x)
xmem : x ∈ closedBall b ε
hx' : Tendsto u atTop (𝓝[closedBall b ε] x)
⊢ f x = y
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })
y : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_14 })
h₂ :
  ComposableArrows.mk₁ (F.map (homMk (Edge.mk' ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x)))) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 2 _proof_12 _proof_15).op)) y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk (Edge.mk' ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x)))) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 0 _proof_12 _proof_15).op)) y
⊢ ComposableArrows.mk₁ (F.map (homMk (Edge.mk' ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_12 _proof_15).op)) x)))) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 1 _proof_12 _proof_15).op)) y

Tactic:
have h' {a b : X _⦋0⦌2} (e : Edge a b) :
          ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) =
            ComposableArrows.mk₁ (F.map (homMk e)) :=
        ComposableArrows.arrowEquiv.injective
          (congr_arg F.mapArrow.obj (congr_arrowMk_homMk (Edge.mk' e.edge) e rfl))

Goal state after:
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })
y : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_14 })
h₂ :
  ComposableArrows.mk₁ (F.map (homMk (Edge.mk' ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x)))) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 2 _proof_12 _proof_15).op)) y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk (Edge.mk' ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x)))) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 0 _proof_12 _proof_15).op)) y
h' :
  ∀ {a b : X.obj (op { obj := ⦋0⦌, property := ⋯ })} (e : Edge a b),
    ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
⊢ ComposableArrows.mk₁ (F.map (homMk (Edge.mk' ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_12 _proof_15).op)) x)))) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 1 _proof_12 _proof_15).op)) y
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‖₊⁻¹
x : F
hx : x ∈ f '' s
y : F
hy : y ∈ f '' s
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
⊢ ‖↑A.symm x - ↑A.symm y - ↑f'.symm (x - y)‖ ≤ ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖x - y‖

Tactic:
rcases (mem_image _ _ _).1 hx with ⟨x', x's, rfl⟩

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
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
y : F
hy : y ∈ f '' s
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
⊢ ‖↑A.symm (f x') - ↑A.symm y - ↑f'.symm (f x' - y)‖ ≤ ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖f x' - y‖
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‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖x' - ↑A.symm (↑A y') - ↑f'.symm (↑A x' - ↑A y')‖ ≤ ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖↑A x' - ↑A y'‖

Tactic:
A.left_inv y's

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
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖x' - y' - ↑f'.symm (↑A x' - ↑A y')‖ ≤ ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖↑A x' - ↑A y'‖
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
h_eq : (fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
z : 𝕜
hfz : (z - x) ^ m • f z = 0 z
hz : z ∈ {x}ᶜ
⊢ 0 = f⁻¹ z

Tactic:
rw [Pi.inv_apply, (smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)).mp hfz,
      inv_zero]

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

Goal state before:
pp: x✝ : ℝ
⊢ (deriv rexp / rexp) x✝ = 1 x✝

Tactic:
Real.deriv_exp,

Goal state after:
x✝ : ℝ
⊢ (rexp / rexp) x✝ = 1 x✝
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: a : ℂ
H :
  (binomialSeries ℂ (-a)).compContinuousLinearMap (-1) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (a + ↑n - 1) n
⊢ HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ (-a)) (binomialSeries ℂ (-a)) (-0) 1

Tactic:
simpa using one_add_cpow_hasFPowerSeriesOnBall_zero

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

Goal state before:
pp: 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
this :
  HasFPowerSeriesOnBall ((fun x ↦ 1 / (1 - x) ^ (a + 1)) ∘ ⇑(z⁻¹ • 1))
    ((FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)).compContinuousLinearMap (z⁻¹ • 1)) 0
    (1 / ‖z⁻¹ • 1‖ₑ)
⊢ 1 / ‖z⁻¹ • 1‖ₑ = ‖z‖ₑ

Tactic:
simp [enorm_smul, enorm_inv, hz]

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

Goal state before:
pp: case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x ↦ x ^ p
p : ℝ
h : ↑(n + 1) ≤ p
⊢ ContDiff ℝ ↑(n + 1) fun x ↦ x ^ p

Tactic:
| succ n ihn =>

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

Goal state before:
pp: r : ℝ
hr : r ≠ 0
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (r - x) ^ 2)
    (FormalMultilinearSeries.ofScalars ℝ fun n ↦ (r ^ (n + 2))⁻¹ * (↑n + 1)) 0 ‖r‖ₑ

Tactic:
by
  simpa [add_comm 1] using one_div_sub_pow_hasFPowerSeriesOnBall_zero 1 hr

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
f : X ≃ᵢ Y
D : DeloneSet X
⊢ D.packingRadius = (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).packingRadius

Tactic:
simp [mapBilipschitz]

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
f : X ≃ᵢ Y
D : DeloneSet X
⊢ D.coveringRadius = (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).coveringRadius

Tactic:
simp [mapBilipschitz]

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
f : X ≃ᵢ Y
D : DeloneSet Y
⊢ D.packingRadius = (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).packingRadius

Tactic:
simp [mapBilipschitz]

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
f : X ≃ᵢ Y
D : DeloneSet Y
⊢ D.coveringRadius = (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).coveringRadius

Tactic:
simp [mapBilipschitz]

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

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
hv₂ : Tendsto v atTop atTop
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthSup u
⊢ (linearGrowthInf fun x ↦ 0) ≤ b

Tactic:
exact (linearGrowthInf_le_linearGrowthSup_of_frequently_le hu).trans u_b.le

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

Goal state before:
pp: u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ expGrowthSup (u * v) ≤ expGrowthSup u + expGrowthSup v

Tactic:
by
  refine (limsup_add_le h h').trans_eq' (limsup_congr (Eventually.of_forall fun n ↦ ?_))
  rw [Pi.add_apply, Pi.mul_apply, log_mul_add, add_div_of_nonneg_right n.cast_nonneg']

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

Goal state before:
pp: case a
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ u n + v n ≤ 2 * max (u n) (v n)

Tactic:
two_mul

Goal state after:
case a
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ u n + v n ≤ max (u n) (v n) + max (u n) (v n)
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : 1 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
n : ℕ
h : 1 n ≤ u n
⊢ 0 n ≤ (u n).log

Tactic:
rw [Pi.one_apply] at h

Goal state after:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : 1 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
n : ℕ
h : 1 ≤ u n
⊢ 0 n ≤ (u n).log
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case refine_3
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
c : ι
⊢ c ∈ t → ∀ b ∈ insert a' u, (B c ∩ B b).Nonempty → ∃ c_1 ∈ insert a' u, (B c ∩ B c_1).Nonempty ∧ δ c ≤ τ * δ c_1

Tactic:
ct

Goal state after:
case refine_3
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
c : ι
ct : c ∈ t
⊢ ∀ b ∈ insert a' u, (B c ∩ B b).Nonempty → ∃ c_1 ∈ insert a' u, (B c ∩ B c_1).Nonempty ∧ δ c ≤ τ * δ c_1
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
⊢ ∫⁻ (_x : α), ⨍⁻ (a : α), f a ∂μ ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
by
  simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure (μ.restrict s)
hμ0 : μ s = 0
⊢ (((μ.restrict s) univ)⁻¹ • μ.restrict s) univ = 0

Tactic:
by simp [hμ0]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
ht₀ : μ t ≠ 0
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hs₀ : 0 < μ.real s
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)

Tactic:
replace ht₀ : 0 < μ.real t := ENNReal.toReal_pos ht₀ htμ

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hs₀ : 0 < μ.real s
ht₀ : 0 < μ.real t
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)