mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
⊢ AbsolutelyContinuousOnInterval (fun x ↦ α • f x) a b

Tactic:
apply squeeze_zero (fun t ↦ ?_) (fun t ↦ ?_) (by simpa using hf.const_mul ‖α‖)

Goal state after:
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ 0 ≤ ∑ i ∈ Finset.range t.1, dist ((fun x ↦ α • f x) (t.2 i).1) ((fun x ↦ α • f x) (t.2 i).2)

F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range t.1, dist ((fun x ↦ α • f x) (t.2 i).1) ((fun x ↦ α • f x) (t.2 i).2) ≤
    ‖α‖ * ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: case h.h.h.h
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))
⊢ {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M

Tactic:
rintro z ⟨hzl, hzr⟩

Goal state after:
case h.h.h.h
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))
z : ℂ
hzl : z ∈ {z | 1 - ε < z.re}
hzr : z ∈ stolzCone s
⊢ z ∈ stolzSet M
Module: Mathlib.Analysis.Normed.Module.Ray

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
H : ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|

Tactic:
SameRay.sameRay_comm

Goal state after:
case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H : ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
Module: Mathlib.Analysis.Convex.Uniform

Goal state before:
pp: case inl
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : ‖x‖ ≤ 1 - δ'
⊢ ‖x + y‖ ≤ 1 + 1 - δ'

Tactic:
exact (norm_add_le_of_le hx' hy).trans (sub_add_eq_add_sub _ _ _).le

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

Goal state before:
pp: case refine_1
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : ℕ × (ℕ → ℝ × ℝ) → Set ℝ := fun E ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this✝ :
  Tendsto (fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this :
  Tendsto (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
⊢ ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    0 ≤
      ∑ i ∈ Finset.range t.1,
        dist ((fun x ↦ ∫ (v : ℝ) in c..x, f v) (t.2 i).1) ((fun x ↦ ∫ (v : ℝ) in c..x, f v) (t.2 i).2)

Tactic:
filter_upwards with (n, I)

Goal state after:
case refine_1
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : ℕ × (ℕ → ℝ × ℝ) → Set ℝ := fun E ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this✝ :
  Tendsto (fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this :
  Tendsto (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
n : ℕ
I : ℕ → ℝ × ℝ
⊢ 0 ≤ ∑ i ∈ Finset.range (n, I).1, dist (∫ (v : ℝ) in c..((n, I).2 i).1, f v) (∫ (v : ℝ) in c..((n, I).2 i).2, f v)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : ℕ × (ℕ → ℝ × ℝ) → Set ℝ := fun E ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this✝¹ :
  Tendsto (fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this✝ :
  Tendsto (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
hnI2 : (↑(Finset.range (n, I).1)).PairwiseDisjoint fun i ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
⊢ ∀ i ∈ Finset.range (n, I).1, MeasurableSet (uIoc ((n, I).2 i).1 ((n, I).2 i).2)

Tactic:
simp +contextual [uIoc]

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

Goal state before:
pp: θ : ℂ
⊢ sin θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ ↑k * ↑π

Tactic:
by
  contrapose!; exact sin_eq_zero_iff

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

Goal state before:
pp: x : ℝ
hx : x ≤ 0
⊢ x ≤ sin x

Tactic:
by simpa using sin_le <| neg_nonneg.2 hx

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

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ (π / 2)⁻¹ * x < sin x

Tactic:
simpa [-inv_div, mul_inv_cancel_left₀ pi_div_two_pos.ne'] using @lt_sin_mul ((π / 2)⁻¹ * x)
    (mul_pos (inv_pos.2 pi_div_two_pos) hx) (by rwa [← div_eq_inv_mul, div_lt_one pi_div_two_pos])

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

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
⊢ ConcaveOn ℝ D f

Tactic:
by
  have : (interior D).EqOn (deriv f) f' := deriv_eqOn isOpen_interior hf'
  refine concaveOn_of_deriv2_nonpos hD hf (fun x hx ↦ (hf' _ hx).differentiableWithinAt) ?_ ?_
  · rw [differentiableOn_congr this]
    exact fun x hx ↦ (hf'' _ hx).differentiableWithinAt
  · rintro x hx
    convert hf''₀ _ hx
    dsimp
    rw [deriv_eqOn isOpen_interior (fun y hy ↦ ?_) hx]
    exact (hf'' _ hy).congr this <| by rw [this hy]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

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

Tactic:
rw [angle_comm, angle_self_neg_of_nonzero hx]

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

Goal state before:
pp: M : ℝ
z : ℂ
x✝¹ : 0 < M
x✝ : z.re ≤ M
⊢ ‖z‖ ≤ ‖2 * ↑M - z‖

Tactic:
rw [← sq_le_sq₀ (by positivity) (by positivity)]
  suffices z.re * z.re ≤ (2 * M - z.re) * (2 * M - z.re) by simpa [Complex.sq_norm, normSq_apply]
  nlinarith

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

Goal state before:
pp: f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := f z / (2 * ↑M - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * ↑M - f z)‖ ≤ ‖z‖ / R
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)

Tactic:
have h_denom : 2 * M - f z ≠ 0 := sub_ne_zero_of_ne (fun h => by simpa [← h, hM] using hf₁ hz)

Goal state after:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := f z / (2 * ↑M - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * ↑M - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * ↑M - f z ≠ 0
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: f : ℂ → ℂ
c z : ℂ
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₁
hR₁ : 0 < R₁
this✝ :
  ∀ {R₁ : ℝ},
    DifferentiableOn ℂ f (ball c R₁) →
      MapsTo f (ball c R₁) (closedBall (f c) R₂) →
        z ∈ ball c R₁ →
          0 < R₁ →
            DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂) →
              ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
this : ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
⊢ ContinuousAt (fun c_1 ↦ R₂ * (‖z - c‖ / c_1) ^ (n + 1)) R₁

Tactic:
fun_prop (disch := positivity)

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → 𝔻
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ+
f : X → 𝔻
hfc : ContinuousOn (fun i ↦ ↑(f i)) U
hf : ∀ (x : X), (fun i ↦ ↑(f i)) x ^ ↑n = (UnitDisc.coe ∘ g) x
⊢ ∃ f, ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x

Tactic:
refine ⟨f, isEmbedding_coe.continuousOn_iff.mpr hfc, fun x ↦ ?_⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → 𝔻
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ+
f : X → 𝔻
hfc : ContinuousOn (fun i ↦ ↑(f i)) U
hf : ∀ (x : X), (fun i ↦ ↑(f i)) x ^ ↑n = (UnitDisc.coe ∘ g) x
x : X
⊢ f x ^ n = g x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x e : 𝕜
⊢ meromorphicTrailingCoeffAt (fun x ↦ e) x = e

Tactic:
by_cases he : e = 0

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x e : 𝕜
he : e = 0
⊢ meromorphicTrailingCoeffAt (fun x ↦ e) x = e

case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x e : 𝕜
he : ¬e = 0
⊢ meromorphicTrailingCoeffAt (fun x ↦ e) x = e
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case e_a.e_a
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
hg : AnalyticAt 𝕜 g x
n : ℤ
q : 𝕜 → E
hq_an : AnalyticAt 𝕜 q (g x)
m : ℕ
p : 𝕜 → 𝕜
hq_ne : ¬q (g x) = 0
hf : f =ᶠ[𝓝 (g x)] (fun x_1 ↦ x_1 - g x) ^ n • q
hm : ↑m = analyticOrderAt (fun x_1 ↦ g x_1 - g x) x
h₁p : AnalyticAt 𝕜 p x
h₂p : ¬p x = 0
h₃p : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ m * p z
a : 𝕜
h₁a : g a - g x = (a - x) ^ m * p a
h₂a : f (g a) = (((a - x) ^ m) ^ n * p a ^ n) • q (g a)
⊢ ((a - x) ^ m) ^ n = (a - x) ^ (↑m * n)

Tactic:
zpow_mul,

Goal state after:
case e_a.e_a
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
hg : AnalyticAt 𝕜 g x
n : ℤ
q : 𝕜 → E
hq_an : AnalyticAt 𝕜 q (g x)
m : ℕ
p : 𝕜 → 𝕜
hq_ne : ¬q (g x) = 0
hf : f =ᶠ[𝓝 (g x)] (fun x_1 ↦ x_1 - g x) ^ n • q
hm : ↑m = analyticOrderAt (fun x_1 ↦ g x_1 - g x) x
h₁p : AnalyticAt 𝕜 p x
h₂p : ¬p x = 0
h₃p : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ m * p z
a : 𝕜
h₁a : g a - g x = (a - x) ^ m * p a
h₂a : f (g a) = (((a - x) ^ m) ^ n * p a ^ n) • q (g a)
⊢ ((a - x) ^ m) ^ n = ((a - x) ^ ↑m) ^ n
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
h : n₁ < n₂
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
z : 𝕜
h₁z : f₁ z = (z - x) ^ n₁ • g₁ z
h₂z : f₂ z = (z - x) ^ n₂ • g₂ z
h₃z : z ∈ {x}ᶜ
⊢ (z - x) ^ n₂ • g₂ z = ((z - x) ^ n₁ * (z - x) ^ (n₂ - n₁)) • g₂ z

Tactic:
rw [← zpow_add₀, add_sub_cancel]

Goal state after:
case ha
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
h : n₁ < n₂
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
z : 𝕜
h₁z : f₁ z = (z - x) ^ n₁ • g₁ z
h₂z : f₂ z = (z - x) ^ n₂ • g₂ z
h₃z : z ∈ {x}ᶜ
⊢ z - x ≠ 0
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
x : 𝕜
hx : x ∈ U
⊢ toMeromorphicNFOn f U x = f x

Tactic:
simp only [toMeromorphicNFOn, h.meromorphicOn, ↓reduceDIte, hx]

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
x : 𝕜
hx : x ∈ U
⊢ toMeromorphicNFAt f x x = f x
Module: Mathlib.Analysis.Meromorphic.Order

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

Tactic:
refine ⟨fun nneg ↦ ?_, fun ⟨g, hg₁, hg₂⟩ ↦ ?_⟩

Goal state after:
case refine_1
𝕜 : 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
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ f =ᶠ[𝓝[≠] x] g

case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ f =ᶠ[𝓝[≠] x] g
g : 𝕜 → E
hg₁ : AnalyticAt 𝕜 g x
hg₂ : f =ᶠ[𝓝[≠] x] g
⊢ 0 ≤ meromorphicOrderAt f x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x c : 𝕜
h : ¬¬MeromorphicAt f (x + c)
⊢ ¬EventuallyConst (fun x ↦ x + c) (𝓝 x)

Tactic:
by simp [eventuallyConst_iff_analyticOrderAt_sub_eq_top]

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

Goal state before:
pp: case inr
R : ℝ
w x : ℂ
hx : x ∈ {w}ᶜ
h : R ≠ 0
this : x - w ≠ 0
⊢ AnalyticAt ℂ (fun z ↦ (↑R ^ 2 - (starRingEnd ℂ) w * z) / (↑R * (z - w))) x

Tactic:
fun_prop (disch := positivity)

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

Goal state before:
pp: w z : ℂ
hzw : z - w ≠ 0
hw : w ∈ ball 0 ‖z‖
hz : z ∈ sphere 0 ‖z‖
hR : 0 < ‖z‖
⊢ ‖↑(normSq z) - (starRingEnd ℂ) w * z‖ = ‖↑‖z‖ * (z - w)‖

Tactic:
normSq_eq_conj_mul_self,

Goal state after:
w z : ℂ
hzw : z - w ≠ 0
hw : w ∈ ball 0 ‖z‖
hz : z ∈ sphere 0 ‖z‖
hR : 0 < ‖z‖
⊢ ‖(starRingEnd ℂ) z * z - (starRingEnd ℂ) w * z‖ = ‖↑‖z‖ * (z - w)‖
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case coe.coe
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁶ : NormedRing R
inst✝⁵ : NoZeroDivisors R
inst✝⁴ : Module R E
inst✝³ : IsBoundedSMul R E
inst✝² : Module.IsTorsionFree R E
x : 𝕜
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : IsScalarTower 𝕜 R E
f : 𝕜 → R
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : meromorphicOrderAt f x = ↑m
n : ℤ
h₂g : meromorphicOrderAt g x = ↑n
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z

Tactic:
obtain ⟨F, h₁F, h₂F, h₃F⟩ := (meromorphicOrderAt_eq_int_iff hf).1 h₂f

Goal state after:
case coe.coe
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁶ : NormedRing R
inst✝⁵ : NoZeroDivisors R
inst✝⁴ : Module R E
inst✝³ : IsBoundedSMul R E
inst✝² : Module.IsTorsionFree R E
x : 𝕜
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : IsScalarTower 𝕜 R E
f : 𝕜 → R
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : meromorphicOrderAt f x = ↑m
n : ℤ
h₂g : meromorphicOrderAt g x = ↑n
F : 𝕜 → R
h₁F : AnalyticAt 𝕜 F x
h₂F : F x ≠ 0
h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz✝ : ¬z ∉ U
hz : z ∈ F.support
⊢ ((F z * if z ∈ U then (single z 1) z else 0) + ∑ x ∈ h.toFinset.erase z, F x * if z ∈ U then (single x 1) z else 0) =
    F z

Tactic:
Finset.sum_eq_zero (by aesop)

Goal state after:
case pos
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz✝ : ¬z ∉ U
hz : z ∈ F.support
⊢ (F z * if z ∈ U then (single z 1) z else 0) + 0 = F z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: 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 : R ≤ 0
a : ℂ
ha : a ∈ closedBall 0 R
⊢ R = 0

Tactic:
grind [nonneg_of_mem_closedBall ha]

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

Goal state before:
pp: case hf
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
meromorphicOrderAt_add : MeromorphicAt f₁ x → MeromorphicAt f₂ x → min ↑n₁ ↑n₂ ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := ⋯
g : 𝕜 → E := ⋯
⊢ AnalyticAt 𝕜 ((fun z ↦ (z - x) ^ (n₁ - n)) • g₁) x

pp: case hg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
meromorphicOrderAt_add : MeromorphicAt f₁ x → MeromorphicAt f₂ x → min ↑n₁ ↑n₂ ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := ⋯
g : 𝕜 → E := ⋯
⊢ AnalyticAt 𝕜 ((fun z ↦ (z - x) ^ (n₂ - n)) • g₂) x

Tactic:
· apply (AnalyticAt.zpow_nonneg (by fun_prop) (sub_nonneg.2 (min_le_left n₁ n₂))).smul h₁g₁

Goal state after:
case hg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
meromorphicOrderAt_add : MeromorphicAt f₁ x → MeromorphicAt f₂ x → min ↑n₁ ↑n₂ ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := ⋯
g : 𝕜 → E := ⋯
⊢ AnalyticAt 𝕜 ((fun z ↦ (z - x) ^ (n₂ - n)) • g₂) x
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : GL n R
⊢ ↑g ∈ Set.range ⇑(Matrix.scalar n) → g ∈ Subgroup.center (GL n R)

Tactic:
· refine fun ⟨a, ha⟩ ↦ Subgroup.mem_center_iff.mpr fun h ↦ ?_
    simp [-scalar_apply, Units.ext_iff, ← ha, Matrix.scalar_comm a (Commute.all _)]

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

Goal state before:
pp: case mpr.inr
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g ∘SL ↑conjCLE
⊢ IsConformalMap g

Tactic:
· have minor₁ : g = map.restrictScalars ℝ ∘L ↑conjCLE := by
        ext1
        simp only [hmap, ContinuousLinearEquiv.coe_coe, comp_apply, conjCLE_apply,
          starRingEnd_self_apply]
      rw [minor₁] at h₂ ⊢
      refine isConformalMap_complex_linear_conj ?_
      contrapose h₂ with w
      simp only [w, restrictScalars_zero, zero_comp]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : ¬¬MeromorphicAt f (x + c)
⊢ ¬EventuallyConst (fun x ↦ x + c) (𝓝 x)

Tactic:
by simp [eventuallyConst_iff_analyticOrderAt_sub_eq_top]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
inst✝¹ : CompleteSpace 𝕜
f : 𝕜 → 𝕜
inst✝ : CharZero 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ↑n = meromorphicOrderAt f x
meromorphicOrderAt_logDeriv_eq_neg_one :
  ∀ [CharZero 𝕜], MeromorphicAt f x → ↑n ≠ 0 → ↑n ≠ ⊤ → meromorphicOrderAt (logDeriv f) x = -1
h₁ : ↑n ≠ 0
⊢ meromorphicOrderAt (logDeriv f) x = -1

Tactic:
logDeriv,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
inst✝¹ : CompleteSpace 𝕜
f : 𝕜 → 𝕜
inst✝ : CharZero 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ↑n = meromorphicOrderAt f x
meromorphicOrderAt_logDeriv_eq_neg_one :
  ∀ [CharZero 𝕜], MeromorphicAt f x → ↑n ≠ 0 → ↑n ≠ ⊤ → meromorphicOrderAt (logDeriv f) x = -1
h₁ : ↑n ≠ 0
⊢ meromorphicOrderAt (deriv f / f) x = -1
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case h.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ((z - ↑l) / ↑(u - l)).re = 0

Tactic:
Complex.div_re,

Goal state after:
case h.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ (z - ↑l).re * (↑(u - l)).re / normSq ↑(u - l) + (z - ↑l).im * (↑(u - l)).im / normSq ↑(u - l) = 0