mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case h
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, {i | x ∈ u i}.Finite
hU : s ⊆ ⋃ i, u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s p)
v : ι → PartialRefinement u s p
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v j ≤ v i
j : ι
hj : x ∈ (v i).toFun j
⊢ x ∈ (find c ne j).toFun j

Tactic:
have hj' : x ∈ u j := (v i).subset _ hj

Goal state after:
case h
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, {i | x ∈ u i}.Finite
hU : s ⊆ ⋃ i, u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s p)
v : ι → PartialRefinement u s p
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v j ≤ v i
j : ι
hj : x ∈ (v i).toFun j
hj' : x ∈ u j
⊢ x ∈ (find c ne j).toFun j
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
t : Set X
t_in : t ∈ 𝓝 x₀
ht : {i | ((fun i ↦ support ⇑(ρ i)) i ∩ t).Nonempty}.Finite
i : ι
hi : i ∈ {i | x₀ ∈ tsupport ⇑(ρ i)}
⊢ i ∈ {i | ((fun i ↦ support ⇑(ρ i)) i ∩ t).Nonempty}

Tactic:
simp only [inter_comm]

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
t : Set X
t_in : t ∈ 𝓝 x₀
ht : {i | ((fun i ↦ support ⇑(ρ i)) i ∩ t).Nonempty}.Finite
i : ι
hi : i ∈ {i | x₀ ∈ tsupport ⇑(ρ i)}
⊢ i ∈ {i | (t ∩ support ⇑(ρ i)).Nonempty}
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst✝¹] s →
      IsClosed[inst✝¹] t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsClosed[inst✝¹] s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen[inst✝¹] (V i)
hVU : ∀ (i : ι), closure[inst✝¹] (V i) ⊆ U i
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen[inst✝¹] (W i)
hWV : ∀ (i : ι), closure[inst✝¹] (W i) ⊆ V i
⊢ ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U

Tactic:
choose f hfp hf0 hf1 hf01 using fun i =>
    h01 _ _ (isClosed_compl_iff.2 <| hVo i) isClosed_closure
      (disjoint_right.2 fun x hx => Classical.not_not.2 (hWV i hx))

Goal state after:
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst✝¹] s →
      IsClosed[inst✝¹] t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsClosed[inst✝¹] s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen[inst✝¹] (V i)
hVU : ∀ (i : ι), closure[inst✝¹] (V i) ⊆ U i
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen[inst✝¹] (W i)
hWV : ∀ (i : ι), closure[inst✝¹] (W i) ⊆ V i
f : ι → C(X, ℝ)
hfp : ∀ (i : ι), p ⇑(f i)
hf0 : ∀ (i : ι), EqOn (⇑(f i)) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (⇑(f i)) 1 (closure[inst✝¹] (W i))
hf01 : ∀ (i : ι) (x : X), (f i) x ∈ Icc 0 1
⊢ ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
this : FiniteDimensional 𝕜 E
hE : Subsingleton E
⊢ ProperSpace F

pp: case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
this : FiniteDimensional 𝕜 E
hE : Nontrivial E
⊢ ProperSpace F

Tactic:
· have : Subsingleton F := Function.Surjective.subsingleton h
      infer_instance

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
this : FiniteDimensional 𝕜 E
hE : Nontrivial E
⊢ ProperSpace F
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤) g
g_comp : HasCompactSupport g
A : ∀ i ∈ s, Integrable (fun x ↦ g x • (a i • fun x ↦ lineDeriv ℝ f x (v i)) x) μ
S2 : ∫ (x : E), (∑ i ∈ s, a i * (fderiv ℝ g x) (v i)) * f x ∂μ = ∑ i ∈ s, a i * ∫ (x : E), (fderiv ℝ g x) (v i) * f x ∂μ
D : ℝ≥0
g_lip : LipschitzWith D g
⊢ ∫ (x : E), -((∑ x_1 ∈ s, a x_1 * (fderiv ℝ g x) (v x_1)) * f x) ∂μ =
    ∑ x ∈ s, a x * ∫ (x_1 : E), -((fderiv ℝ g x_1) (v x) * f x_1) ∂μ

Tactic:
simp only [integral_neg, mul_neg, Finset.sum_neg_distrib, neg_inj]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤) g
g_comp : HasCompactSupport g
A : ∀ i ∈ s, Integrable (fun x ↦ g x • (a i • fun x ↦ lineDeriv ℝ f x (v i)) x) μ
S2 : ∫ (x : E), (∑ i ∈ s, a i * (fderiv ℝ g x) (v i)) * f x ∂μ = ∑ i ∈ s, a i * ∫ (x : E), (fderiv ℝ g x) (v i) * f x ∂μ
D : ℝ≥0
g_lip : LipschitzWith D g
⊢ ∫ (a_1 : E), (∑ x ∈ s, a x * (fderiv ℝ g a_1) (v x)) * f a_1 ∂μ =
    ∑ x ∈ s, a x * ∫ (a : E), (fderiv ℝ g a) (v x) * f a ∂μ
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case inl
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b : ℝ
f : ℝ → F
a : ℝ
hf : AbsolutelyContinuousOnInterval f a a
hab₀ : a ≤ a
⊢ BoundedVariationOn f (Icc a a)

pp: case inr
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab₀ : a ≤ b
hab : a < b
⊢ BoundedVariationOn f (Icc a b)

Tactic:
· simp [BoundedVariationOn]

Goal state after:
case inr
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab₀ : a ≤ b
hab : a < b
⊢ BoundedVariationOn f (Icc a b)
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)

Tactic:
by
  rcases eq_or_lt_of_le hab with (rfl | h)
  · refine ⟨0, fun x hx => ?_⟩
    have : x = a := by simpa [← le_antisymm_iff] using hx
    simp [← this]
  -- We estimate by the supremum of the norm of the iterated derivative
  let g : ℝ → ℝ := fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
  use SupSet.sSup (g '' Icc a b) / (n !)
  intro x hx
  rw [div_mul_eq_mul_div₀]
  refine taylor_mean_remainder_bound hab hf hx fun y => ?_
  exact (hf.continuousOn_iteratedDerivWithin rfl.le <| uniqueDiffOn_Icc h).norm.le_sSup_image_Icc

Goal state after:
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: M : ℝ
hM : 1 < M
⊢ Filter.map ofReal (𝓝[<] 1) ≤ 𝓝[stolzSet M] 1

Tactic:
rw [← tendsto_id']

Goal state after:
M : ℝ
hM : 1 < M
⊢ Tendsto id (Filter.map ofReal (𝓝[<] 1)) (𝓝[stolzSet M] 1)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x ↦ √x * log x) x = (2 + log x) / (2 * √x)

Tactic:
rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x ↦ √x * log x) x = 0
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case inl
x✝ : ℝ
hx✝ : x✝ ≤ 0
x : ℝ
hx : x ∈ Iic 0
⊢ (2 + log x) / (2 * √x) = 0

Tactic:
rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]

Goal state after:
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
⊢ ‖f w‖ = ‖f z‖

Tactic:
by
  set e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
  have he : ∀ x, ‖e x‖ = ‖x‖ := UniformSpace.Completion.norm_coe
  replace hz : IsMaxOn (norm ∘ e ∘ f) (closedBall z (dist w z)) z := by
    simpa only [IsMaxOn, Function.comp_def, he] using hz
  simpa only [he, Function.comp_def]
    using norm_max_aux₁ (e.differentiable.comp_diffContOnCl hd) hz

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

Goal state before:
pp: x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y * I = (2 * ↑l + 1) * ↑π / 2
⊢ tan (x + y * I) = (tan x + tanh y * I) / (1 - tan x * tanh y * I)

Tactic:
tan_add h,

Goal state after:
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y * I = (2 * ↑l + 1) * ↑π / 2
⊢ (tan x + tan (y * I)) / (1 - tan x * tan (y * I)) = (tan x + tanh y * I) / (1 - tan x * tanh y * I)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : 0 < x
f : ℝ → ℝ := fun t ↦ sin t - (t - t ^ 3 / 6)
hderiv : ∀ (t : ℝ), deriv f t = cos t - 1 + t ^ 2 / 2
hmono : StrictMonoOn f (Ici 0)
⊢ x - x ^ 3 / 6 < sin x

Tactic:
have h0 : f 0 < f x := hmono (by simp) hx.le hx

Goal state after:
x : ℝ
hx : 0 < x
f : ℝ → ℝ := fun t ↦ sin t - (t - t ^ 3 / 6)
hderiv : ∀ (t : ℝ), deriv f t = cos t - 1 + t ^ 2 / 2
hmono : StrictMonoOn f (Ici 0)
h0 : f 0 < f x
⊢ x - x ^ 3 / 6 < sin x
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle (- -x) (-y) = π - angle x y

Tactic:
neg_neg,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle x (-y) = π - angle x y
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
⊢ arccos (⟪x, 0⟫ / (‖x‖ * ‖0‖)) = π / 2

Tactic:
rw [inner_zero_right, zero_div, Real.arccos_zero]

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ slope f x y ≤ f'

Tactic:
by
  apply ge_of_tendsto <| (hasDerivWithinAt_iff_tendsto_slope' self_notMem_Iio).mp hf'
  simp_rw [eventually_nhdsWithin_iff, slope_comm f x y, slope_def_field]
  filter_upwards [eventually_gt_nhds hxy] with t ht (ht' : t < y)
  refine hfc.secant_mono hy hx (?_ : t ∈ S) hxy.ne ht'.ne ht.le
  exact hfc.1.ordConnected.out hx hy ⟨ht.le, ht'.le⟩

Goal state after:
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝔻
⊢ ‖↑z‖ ^ 2 < 1

Tactic:
rw [sq_lt_one_iff_abs_lt_one, abs_norm]
  exact z.norm_lt_one

Goal state after:
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)

Tactic:
have hR₁ : 0 < R₁ := nonempty_ball.mp ⟨_, hz⟩
  have hR₂ : 0 ≤ R₂ := nonempty_closedBall.mp ⟨_, h_maps hz⟩
  rcases eq_or_ne (f z) (f c) with heq | hfne
  · trans 0 <;> [simp [heq]; positivity]
  have hne : z ≠ c := ne_of_apply_ne _ hfne
  -- Let `g : F → ℂ` be a continuous linear function such that `‖g‖ = 1`
  -- and `‖g (f z - f c)‖ = ‖f z - f c‖`.
  rcases exists_dual_vector ℂ _ (norm_sub_eq_zero_iff.not.mpr hfne) with ⟨g, hg, hgf⟩
  -- Consider `h : ℂ → ℂ` given by `h w = g (f (c + w * (z - c)))`.
  set h : ℂ → ℂ := g ∘ f ∘ lineMap c z
  -- This map is differentiable on the ball with center at the origin and radius `R₁ / dist z c`
  -- and it sends this ball to the closed ball with center `h 0 = f c` and radius R₂`.
  have hmaps_line : MapsTo (lineMap c z) (ball (0 : ℂ) (R₁ / dist z c)) (ball c R₁) := by
    intro w hw
    simpa [lt_div_iff₀, hne, dist_comm c] using hw
  have hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂) := by
    refine MapsTo.comp ?_ (h_maps.comp hmaps_line)
    simpa [hg, h] using g.lipschitz.mapsTo_closedBall (f c) R₂
  have hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c)) :=
    g.differentiable.comp_differentiableOn <| hd.comp (lineMap c z).differentiableOn hmaps_line
  -- This map also satisfies `h(w) - h(0) = o(w ^ n)`, thus we can apply the auxiliary lemma above.
  have hn : (h · - h 0) =o[𝓝 0] (fun w ↦ (w - 0) ^ n) := by
    simp only [h, ← map_sub, Function.comp_apply, sub_zero]
    refine (g.isBigO_comp _ _).trans_isLittleO ?_
    rw [← lineMap_apply_zero (k := ℂ) c z] at hn
    refine hn.comp_tendsto ?_ |>.trans_isBigO ?_
    · exact Continuous.tendsto (by fun_prop) 0
    · simpa [Function.comp_def, ← dist_eq_norm_sub, mul_pow, mul_comm]
        using (Asymptotics.isBigO_refl (· ^ n) (𝓝 (0 : ℂ))).norm_left.const_mul_left _
  have hmem : 1 ∈ ball (0 : ℂ) (R₁ / dist z c) := by
    simpa [lt_div_iff₀, hne]
  rw [map_sub] at hgf
  simpa [hgf, h, dist_eq_norm_sub] using schwarz_aux hdiff hmaps hn hmem

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

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
h : MeromorphicNFOn (g • f) U
z : 𝕜
hz : z ∈ U
⊢ MeromorphicNFAt f z

Tactic:
rw [← meromorphicNFAt_smul_iff_right_of_analyticAt (h₁g z hz) (h₂g z hz)]
    exact h hz

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
h₃ : n = 0
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n

Tactic:
simp only [h₃, zpow_zero]

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
h₃ : n = 0
⊢ meromorphicTrailingCoeffAt 1 x = 1
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case refine_1.top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
nneg : 0 ≤ meromorphicOrderAt f x
h₀ : meromorphicOrderAt f x = ⊤
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ f =ᶠ[𝓝[≠] x] g

Tactic:
exact ⟨0, analyticAt_const, meromorphicOrderAt_eq_top_iff.mp h₀⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝² : NontriviallyNormedField 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
z₀ : 𝕜
n : ℕ
inst✝ : Decidable (↑n = 0)
⊢ meromorphicOrderAt (OfNat.ofNat n) z₀ = if ↑n = 0 then ⊤ else 0

Tactic:
convert! meromorphicOrderAt_const z₀ (n : 𝕜')

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝² : NontriviallyNormedField 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
z₀ : 𝕜
n : ℕ
inst✝ : Decidable (↑n = 0)
x✝ : 𝕜
⊢ OfNat.ofNat n x✝ = ↑n
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: f : ℂ →ₗᵢ[ℝ] ℂ
h₃ : ∀ (z : ℂ), z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
z : ℂ
⊢ (f z).re = z.re

Tactic:
by
  simpa [Complex.ext_iff, add_re, add_im, conj_re, conj_im, ← two_mul,
    show (2 : ℝ) ≠ 0 by simp] using (h₃ z).symm

Goal state after:
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)

Tactic:
have minor₁ : ‖map 1‖ ≠ 0 := by
    simpa only [ContinuousLinearMap.ext_ring_iff, Ne, norm_eq_zero] using! nonzero
  refine ⟨‖map 1‖, minor₁, ⟨‖map 1‖⁻¹ • ((map : ℂ →ₗ[ℂ] E) : ℂ →ₗ[ℝ] E), ?_⟩, ?_⟩
  · intro x
    simp only [LinearMap.smul_apply]
    have : x = x • (1 : ℂ) := by rw [smul_eq_mul, mul_one]
    nth_rw 1 [this]
    rw [LinearMap.coe_restrictScalars]
    simp only [map.coe_coe, map.map_smul, norm_smul, norm_inv, norm_norm]
    field
  · ext1
    simp [minor₁]

Goal state after:
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: f : ℂ → ℂ
z : ℂ
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = fderiv ℝ f z ∘SL ↑conjCLE) ∧
      fderiv ℝ f z ≠ 0 ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0

Tactic:
apply and_congr_left

Goal state after:
f : ℂ → ℂ
z : ℂ
⊢ fderiv ℝ f z ≠ 0 →
    (((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = fderiv ℝ f z ∘SL ↑conjCLE) ↔
      DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z))
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
⊢ ∃ h, ECanonicalDecomp f h R

Tactic:
obtain ⟨g, D⟩ := h₁f.exists_canonicalDecomp h₂f

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
g : ℂ → E
D : CanonicalDecomp f g R
⊢ ∃ h, ECanonicalDecomp f h R
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : {x}ᶜ = U \ {x} ∪ Uᶜ
⊢ ∀ᶠ (y : 𝕜) in 𝓝[Uᶜ] x, AnalyticAt 𝕜 f y ∨ y ∉ U

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy using Or.inr hy

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = ↑r
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] (fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ meromorphicOrderAt ((fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g) x =
    ↑r * ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x)

Tactic:
meromorphicOrderAt_smul ?_ (AnalyticAt.meromorphicAt ?_),

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = ↑r
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] (fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ meromorphicOrderAt ((fun x_1 ↦ g x_1 - g x) ^ r) x + meromorphicOrderAt (F ∘ g) x =
    ↑r * ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x)

𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = ↑r
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] (fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ MeromorphicAt ((fun x_1 ↦ g x_1 - g x) ^ r) x

𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = ↑r
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] (fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ AnalyticAt 𝕜 (F ∘ g) x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
⊢ ((∏ i ∈ t₂, meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
        ∏ i ∈ t₁, meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) •
      ((∏ n ∈ t₂, meromorphicTrailingCoeffAt (canonicalFactor R n ^ (-(divisor f B₀R) n)) w) *
          ∏ n ∈ t₁, meromorphicTrailingCoeffAt ((fun x ↦ x - n) ^ (divisor f S₀R) n) w) •
        h w =
    h w

Tactic:
by
      rw [smul_smul, mul_mul_mul_comm, ← Finset.prod_mul_distrib, ← Finset.prod_mul_distrib,
        Finset.prod_eq_one ?η₁, Finset.prod_eq_one ?η₂, mul_one, one_smul]
      case η₁ =>
        intro x hx
        rw [MeromorphicAt.meromorphicTrailingCoeffAt_zpow (by fun_prop), ← zpow_add₀,
          add_neg_cancel, zpow_zero]
        apply MeromorphicAt.meromorphicTrailingCoeffAt_ne_zero (by fun_prop)
          (meromorphicOrderAt_canonicalFactor_ne_top x hR)
      case η₂ =>
        intro x hx
        rw [MeromorphicAt.meromorphicTrailingCoeffAt_zpow (by fun_prop), ← zpow_add₀,
          locallyFinsuppWithin.coe_neg, Pi.neg_apply, neg_add_cancel, zpow_zero]
        rw [meromorphicTrailingCoeffAt_id_sub_const]
        grind

Goal state after: