mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.TangentCone.Seq

Goal state before:
pp: case mp.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
c : ℕ → 𝕜
d : ℕ → E
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hd₀' : ∀ᶠ (n : ℕ) in atTop, d n ≠ 0
hd₀ : Tendsto (fun x ↦ ‖d x‖) atTop (𝓝 0)
hcd : Tendsto (fun x ↦ ‖c x‖ / ‖d x‖⁻¹) atTop (𝓝 ‖y‖)
⊢ Tendsto (fun x ↦ ‖c x‖) atTop atTop

Tactic:
refine .num ?_ (by simpa) hcd

Goal state after:
case mp.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
c : ℕ → 𝕜
d : ℕ → E
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hd₀' : ∀ᶠ (n : ℕ) in atTop, d n ≠ 0
hd₀ : Tendsto (fun x ↦ ‖d x‖) atTop (𝓝 0)
hcd : Tendsto (fun x ↦ ‖c x‖ / ‖d x‖⁻¹) atTop (𝓝 ‖y‖)
⊢ Tendsto (fun x ↦ ‖d x‖⁻¹) atTop atTop
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, x_1 ∈ {x}ᶜ → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ}, 0 < α → ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
⊢ 0 < (b - x) / 2

Tactic:
by simp [hx.left.right]

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun n ↦ (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
this :
  Tendsto
    (fun x ↦
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, (∑ k ∈ range x, f k - ∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
n : ℕ
| fun x ↦ (l - s n) * z ^ x + (∑ k ∈ range n, f k - ∑ k ∈ range (x + 1), f k) * z ^ x

Tactic:
i

Goal state after:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun n ↦ (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
this :
  Tendsto
    (fun x ↦
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, (∑ k ∈ range x, f k - ∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
n i : ℕ
| (l - s n) * z ^ i + (∑ k ∈ range n, f k - ∑ k ∈ range (i + 1), f k) * z ^ i
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
⊢ ‖x‖ / (‖x‖ + ‖y‖) + ‖y‖ / (‖x‖ + ‖y‖) = 1

Tactic:
rw [← add_div, div_self hxy.ne']

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

Goal state before:
pp: θ : ℂ
⊢ cexp (θ * I) = -cexp (-θ * I) ↔ cexp (2 * θ * I) = -1

Tactic:
neg_eq_neg_one_mul,

Goal state after:
θ : ℂ
⊢ cexp (θ * I) = -1 * cexp (-θ * I) ↔ cexp (2 * θ * I) = -1
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
x : E
hx : x ∈ U
H₁ : ‖f x‖ = ‖f c‖
H₂ : ‖f x + f c‖ = ‖f c + f c‖
⊢ ‖f x + Function.const E (f c) x‖ = ‖f x‖ + ‖Function.const E (f c) x‖

Tactic:
simp only [H₂, SameRay.rfl.norm_add, H₁, Function.const]

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

Goal state before:
pp: x : ℝ
⊢ 0 ≤ arctan x ↔ 0 ≤ x

Tactic:
simpa only [arctan_zero] using arctan_le_arctan_iff (x := 0)

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

Goal state before:
pp: x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -(π / 2) < (2 * ↑k + 1) * π / 2
ub : arctan x < π / 2
⊢ False

Tactic:
neg_eq_neg_one_mul,

Goal state after:
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 * (π / 2) < (2 * ↑k + 1) * π / 2
ub : arctan x < π / 2
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
⊢ 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(y ^ 2 + 1)

Tactic:
hy1

Goal state after:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
⊢ y ≤ 3 * π / 2 → cos y < 1 / √(y ^ 2 + 1)
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
this : ‖x / y - 1‖ ∈ Icc (2 / π * angle x (1 * y)) (angle x (1 * y))
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Tactic:
div_sub_one,

Goal state after:
case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
this : ‖(x - y) / y‖ ∈ Icc (2 / π * angle x (1 * y)) (angle x (1 * y))
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
this : ‖x / y - 1‖ ∈ Icc (2 / π * angle x (1 * y)) (angle x (1 * y))
⊢ y ≠ 0
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ angle x y ≤ π / 2 * ‖x - y‖

Tactic:
← div_le_iff₀' <| by positivity,

Goal state after:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ angle x y / (π / 2) ≤ ‖x - y‖
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
⊢ IsQuotientCoveringMap (fun x ↦ x ^ n) ↥(rootsOfUnity n 𝕜)

Tactic:
have : IsQuotientMap fun x : 𝕜ˣ ↦ x ^ n := by
    let e := unitsHomeomorphNeZero (G₀ := 𝕜)
    convert! (e.symm.isQuotientMap.comp this).comp (e.trans (.ofEqSubtypes _)).isQuotientMap
    · exact (e.left_inv _).symm
    · ext; simp [NeZero.ne]

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝¹ : NeZero n
this✝ : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
this : IsQuotientMap fun x ↦ x ^ n
⊢ IsQuotientCoveringMap (fun x ↦ x ^ n) ↥(rootsOfUnity n 𝕜)
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
R : ℝ
f : E → F
z : E
hd : DifferentiableOn ℂ f (ball 0 R)
h_maps : MapsTo f (ball 0 R) (closedBall 0 R)
h₀ : f 0 = 0
hz : ‖z‖ < R
⊢ ‖f z‖ ≤ ‖z‖

Tactic:
simpa [h₀] using dist_le_dist_of_mapsTo_ball hd (by rwa [h₀]) (mem_ball_zero_iff.mpr hz)

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ (divisor (f ∘ fun x ↦ x + c) U) (x - c) = (divisor f (U + {c})) x

Tactic:
divisor_apply,

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ (meromorphicOrderAt (f ∘ fun x ↦ x + c) (x - c)).untop₀ = (divisor f (U + {c})) x

case neg.hf
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ MeromorphicOn (f ∘ fun x ↦ x + c) U

case neg.hz
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ x - c ∈ U
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton
⊢ MeromorphicNFAt (∏ i ∈ s, f i) x

Tactic:
have h₃f {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}) :
      AnalyticAt 𝕜 (f τ) x := by
    rw [← (h₁f τ h₁τ).meromorphicOrderAt_nonneg_iff_analyticAt]
    apply ((h₁f τ h₁τ).meromorphicOrderAt_eq_zero_iff.2 _).symm.le
    grind
  by_cases h₄f : {σ ∈ s | f σ x = 0} = ∅
  · exact (Finset.analyticAt_prod _ (fun σ hσ ↦ h₃f hσ (by aesop))).meromorphicNFAt
  rw [Finset.filter_eq_empty_iff] at h₄f
  push Not at h₄f
  obtain ⟨τ, h₁τ, h₂τ⟩ := h₄f
  have {μ : ι} (hμ : μ ∈ s.erase τ) : f μ x ≠ 0 := by
    by_contra
    have : τ = μ := h₂f (by aesop) (by aesop)
    aesop
  rw [← Finset.mul_prod_erase _ _ h₁τ, meromorphicNFAt_mul_iff_left]
  · apply h₁f τ h₁τ
  · apply Finset.analyticAt_prod _ (fun μ hμ ↦ h₃f (Finset.mem_of_mem_erase hμ) (by aesop))
  · rw [Finset.prod_apply, Finset.prod_ne_zero_iff]
    aesop

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
h : ¬analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
m : ℕ
hm : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
⊢ analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose ⋯ • f z) x = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
simp only [← hm, ENat.natCast_ne_top, false_iff]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
h : ¬analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
m : ℕ
hm : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
⊢ ¬∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
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 : 𝕜
n : ℤ
hf : MeromorphicAt f x
⊢ meromorphicOrderAt f x = ↑n ↔ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
by
  simp only [meromorphicOrderAt, hf, ↓reduceDIte]
  by_cases h : analyticOrderAt (fun z ↦ (z - x) ^ hf.choose • f z) x = ⊤
  · rw [h, ENat.map_top, ← WithTop.coe_natCast, top_sub,
      eq_false_intro WithTop.top_ne_coe, false_iff]
    rw [analyticOrderAt_eq_top] at h
    refine fun ⟨g, hg_an, hg_ne, hg_eq⟩ ↦ hg_ne ?_
    apply EventuallyEq.eq_of_nhds
    rw [EventuallyEq, ← AnalyticAt.frequently_eq_iff_eventually_eq hg_an analyticAt_const]
    apply Eventually.frequently
    rw [eventually_nhdsWithin_iff] at hg_eq ⊢
    filter_upwards [h, hg_eq] with z hfz hfz_eq hz
    rwa [hfz_eq hz, ← mul_smul, smul_eq_zero_iff_right] at hfz
    exact mul_ne_zero (pow_ne_zero _ (sub_ne_zero.mpr hz)) (zpow_ne_zero _ (sub_ne_zero.mpr hz))
  · obtain ⟨m, h⟩ := ENat.ne_top_iff_exists.mp h
    rw [← h, ENat.map_natCast, ← WithTop.coe_natCast, ← coe_sub, WithTop.coe_inj]
    obtain ⟨g, hg_an, hg_ne, hg_eq⟩ := hf.choose_spec.analyticOrderAt_eq_natCast.mp h.symm
    replace hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ (↑m - ↑hf.choose : ℤ) • g z := by
      rw [eventually_nhdsWithin_iff]
      filter_upwards [hg_eq] with z hg_eq hz
      rwa [← smul_right_inj <| zpow_ne_zero _ (sub_ne_zero.mpr hz), ← mul_smul,
        ← zpow_add₀ (sub_ne_zero.mpr hz), ← add_sub_assoc, add_sub_cancel_left, zpow_natCast,
        zpow_natCast]
    exact ⟨fun h ↦ ⟨g, hg_an, hg_ne, h ▸ hg_eq⟩,
      AnalyticAt.unique_eventuallyEq_zpow_smul_nonzero ⟨g, hg_an, hg_ne, hg_eq⟩⟩

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

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x < 0
c : E
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ False

Tactic:
apply not_tendsto_atTop_of_tendsto_nhds hc.norm

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x < 0
c : E
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ Tendsto (fun x ↦ ‖f x‖) (𝓝[≠] x) atTop
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho✝ : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
ho : meromorphicOrderAt f x < 0
⊢ False

Tactic:
apply not_tendsto_atTop_of_tendsto_nhds hc.norm

Goal state after:
case inr.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho✝ : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
ho : meromorphicOrderAt f x < 0
⊢ Tendsto (fun x ↦ ‖f x‖) (𝓝[≠] x) atTop
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho✝ : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x < 0
⊢ False

Tactic:
apply not_tendsto_atTop_of_tendsto_nhds hc.norm

Goal state after:
case inr.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho✝ : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x < 0
⊢ Tendsto (fun x ↦ ‖f x‖) (𝓝[≠] x) atTop
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 : 𝕜
f : 𝕜 → E
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x

Tactic:
by
  by_cases h₁ : ¬MeromorphicAt f x
  · aesop
  rw [not_not] at h₁
  by_cases h₂ : meromorphicOrderAt f x = ⊤
  · rw [h₂, eq_comm]
    simp_all [meromorphicOrderAt_eq_top_iff]
  lift meromorphicOrderAt f x to ℤ using h₂ with n hn
  rw [eq_comm, meromorphicOrderAt_eq_int_iff (by fun_prop)] at *
  obtain ⟨g, hg⟩ := hn
  use -g
  simp_all

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

Goal state before:
pp: R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
⊢ MeromorphicNFOn (∏ᶠ (u : ℂ), canonicalFactor R u ^ F u) (ball 0 R)

Tactic:
refine meromorphicNFOn_finprod (fun w ↦ ?_) fun z hz a ha b hb ↦ ?_
  · by_cases hw : w ∈ ball 0 R
    · exact fun _ _ ↦ (meromorphicNFOn_canonicalFactor hw).zpow (by trivial)
    · simp only [hw, not_false_eq_true, locallyFinsuppWithin.apply_eq_zero_of_notMem, zpow_zero]
      exact analyticOnNhd_const.meromorphicNFOn
  · have ⟨h₂a, h₂b⟩ : a ∈ ball 0 R ∧ b ∈ ball 0 R := by constructor <;> (by_contra; aesop)
    grind [eq_zero_of_zpow_eq_zero hb, eq_zero_of_zpow_eq_zero ha,
      canonicalFactor_eq_zero_iff h₂b hz, canonicalFactor_eq_zero_iff h₂a hz]

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
u : 𝕜
hx : D u = 0
⊢ (fun x ↦ ↑(D u) * log ‖x - u‖) = 0

Tactic:
· simp_all [Pi.zero_def]

Goal state after:
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 : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∀ u ∈ ball 0 R, g u ≠ 0

Tactic:
by
      intro z hz
      rw [← MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff (h₂g (ball_subset_closedBall hz))]
      have : divisor g (ball 0 R) z = 0 := by simp [h₃g]
      rw [divisor_apply (fun x hx ↦ (h₂g (ball_subset_closedBall hx)).meromorphicAt) hz] at this
      simpa [h₄g (ball_subset_closedBall hz)] using this

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
i : n
⊢ (∃ x, (GeneralLinearGroup.scalar n) x = toGL g) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (diagonal fun x ↦ r) = ↑g

Tactic:
refine ⟨fun ⟨r, hr⟩ ↦ ⟨r, by simpa [Units.ext_iff] using congr(GeneralLinearGroup.det $hr),
    by simpa [Units.ext_iff] using hr⟩, fun ⟨r, hr1, hr⟩ ↦ ⟨⟨r, g⁻¹.1 i i, ?_, ?_⟩,
      by simp [Units.ext_iff, hr]⟩⟩

Goal state after:
case refine_1
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (diagonal fun x ↦ r) = ↑g
r : R
hr1 : r ^ Fintype.card n = 1
hr : (diagonal fun x ↦ r) = ↑g
⊢ r * ↑g⁻¹ i i = 1

case refine_2
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (diagonal fun x ↦ r) = ↑g
r : R
hr1 : r ^ Fintype.card n = 1
hr : (diagonal fun x ↦ r) = ↑g
⊢ ↑g⁻¹ i i * r = 1
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: a : Circle
⊢ rotation a ≠ conjLIE

Tactic:
by
  intro h
  have h1 : rotation a 1 = conj 1 := LinearIsometryEquiv.congr_fun h 1
  have hI : rotation a I = conj I := LinearIsometryEquiv.congr_fun h I
  rw [rotation_apply, map_one, mul_one] at h1
  rw [rotation_apply, conj_I, ← neg_one_mul, mul_left_inj' I_ne_zero, h1, eq_neg_self_iff] at hI
  exact one_ne_zero hI

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

Goal state before:
pp: f : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ f 1 ∈ Submonoid.unitSphere ℂ

Tactic:
simp [Submonoid.unitSphere, f.norm_map]

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
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : {x}ᶜ = U \ {x} ∪ Uᶜ
⊢ ∀ᶠ (y : 𝕜) in 𝓝[U \ {x} ∪ Uᶜ] x, AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ

Tactic:
nhdsWithin_union

Goal state after:
𝕜 : 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}] x ⊔ 𝓝[Uᶜ] x, AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ
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
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
a : 𝕜
h₁a : ∀ᶠ (x : 𝕜) in 𝓝[{x}ᶜ] a, f x = 0
this : ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0
⊢ a ∈ (U \ Subtype.val '' {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤})ᶜ

Tactic:
simp +contextual [meromorphicOrderAt_eq_top_iff, this]

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

Goal state before:
pp: this : |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
⊢ |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10

Tactic:
by
    norm_num1 at *
    assumption

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

Goal state before:
pp: this : |log 3 - 109861228867 / 100000000000| ≤ (2 / 3) ^ 71 / 3⁻¹ + (1 / 10 ^ 10 - (2 / 3) ^ 71 / 3⁻¹)
⊢ |log 3 - 109861228867 / 100000000000| ≤ 1 / 10 ^ 10

Tactic:
by
    norm_num1 at *
    assumption

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

Goal state before:
pp: ⊢ |log 3 - 109861228867 / 100000000000| ≤ 1 / 10 ^ 10

Tactic:
by
  suffices |log 3 - 109861228867 / 100000000000| ≤
      (2 / 3) ^ 71 / 3⁻¹ + (1 / 10 ^ 10 - (2 / 3) ^ 71 / 3⁻¹) by
    norm_num1 at *
    assumption
  have t : |2 / 3| = (2 : ℝ) / 3 := by norm_num
  have z := abs_log_sub_add_sum_range_le (x := 2 / 3) (by norm_num) 70
  rw [t, show (1 - (2 : ℝ) / 3) = (1 / 3 : ℝ) by norm_num, one_div (3 : ℝ), log_inv,
    ← sub_eq_add_neg, _root_.abs_sub_comm] at z
  apply le_trans (_root_.abs_sub_le _ _ _) (add_le_add z _)
  norm_num [sum_range_succ]

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

Goal state before:
pp: this : |log 5 - 160943791243 / 100000000000| ≤ (4 / 5) ^ 131 / 5⁻¹ + (1 / 10 ^ 10 - (4 / 5) ^ 131 / 5⁻¹)
⊢ |log 5 - 160943791243 / 100000000000| ≤ 1 / 10 ^ 10

Tactic:
by
    norm_num1 at *
    assumption

Goal state after:
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
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
⊢ h w =
    ((∏ᶠ (i : ℂ), canonicalFactor R i w ^ (divisor f (ball 0 R)) i) *
        ∏ᶠ (i : ℂ), (w - i) ^ (-divisor f (sphere 0 R)) i) •
      meromorphicTrailingCoeffAt f w

Tactic:
rw [D.eq_smul_meromorphicTrailingCoeffAt h₁w hR]
  congr! 4 with x x
  · by_cases h₃x : (divisor f (ball 0 R)) x = 0
    · simp [h₃x]
    have h₁x : x ∈ ball 0 R := (divisor f (ball 0 R)).supportWithinDomain h₃x
    have h₂x : w ≠ x := by
      rintro rfl
      exact h₃x (by simp [(D.meromorphicOn.mono_set ball_subset_closedBall).divisor_apply h₁x, h₂w])
    rw [AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero
      (Complex.analyticOnNhd_canonicalFactor R x w h₂x)
      (Complex.canonicalFactor_ne_zero h₁x h₁w h₂x)]
  · by_cases h : x = w
    · simp_all [meromorphicTrailingCoeffAt_id_sub_const, divisor_def]
    grind [meromorphicTrailingCoeffAt_id_sub_const]

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
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
hn : ↑n ≠ 0
hmero : MeromorphicAt f x
g : 𝕜 → E
hga : AnalyticAt 𝕜 g x
hg0 : g x ≠ 0
hg : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z
z : 𝕜
hgz : AnalyticAt 𝕜 g z
hmem : z ∈ {x}ᶜ
hz : deriv f z = deriv (fun z ↦ (z - x) ^ n • g z) z
hzx : z - x ≠ 0
⊢ deriv f z = (z - x) ^ (n - 1) • (↑n • g z + (z - x) • deriv g z)

Tactic:
calc
    deriv f z = deriv (fun z ↦ (z - x) ^ n • g z) z :=
      hz
    _ = (z - x) ^ n • deriv g z + deriv ((· ^ n) ∘ (· - x)) z • g z :=
      deriv_fun_smul (by fun_prop (disch := grind)) hgz.differentiableAt
    _ = (z - x) ^ n • deriv g z + (n * (z - x) ^ (n - 1)) • g z := by
      rw [deriv_comp _ (by fun_prop (disch := grind)) (by fun_prop)]
      simp [deriv_zpow]
    _ = (z - x) ^ (n - 1) • ((n : 𝕜) • g z + (z - x) • deriv g z) := by
      simp [smul_smul, ← zpow_add_one₀ hzx, add_comm, mul_comm]

Goal state after: