mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
h : u ∈ support d
⊢ u ∈ Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u

Tactic:
· simp_all only [mem_mulSupport, ne_eq, ne_iff]
    use u
    simp_all [zero_zpow_eq_one₀]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (f σ) x
⊢ meromorphicTrailingCoeffAt (∏ n ∈ s, f n) x = ∏ n ∈ s, meromorphicTrailingCoeffAt (f n) x

Tactic:
induction s using Finset.induction with

Goal state after:
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
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
ho : 0 < meromorphicOrderAt f x
⊢ False

Tactic:
· apply c_ne
    exact tendsto_nhds_unique hc (tendsto_zero_of_meromorphicOrderAt_pos ho)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
⊢ meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹

Tactic:
by
  by_cases h₁ : MeromorphicAt f x
  · by_cases h₂ : meromorphicOrderAt f x = ⊤
    · simp_all [meromorphicOrderAt_inv (f := f) (x := x)]
    have : f⁻¹ * f =ᶠ[𝓝[≠] x] 1 := by
      filter_upwards [(meromorphicOrderAt_ne_top_iff_eventually_ne_zero h₁).1 h₂]
      simp_all
    rw [← mul_eq_one_iff_eq_inv₀ (h₁.meromorphicTrailingCoeffAt_ne_zero h₂),
      ← h₁.inv.meromorphicTrailingCoeffAt_mul h₁, meromorphicTrailingCoeffAt_congr_nhdsNE this,
      analyticAt_const.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n := 0)]
    · simp
    · simp only [zpow_zero, smul_eq_mul, mul_one]
      exact eventuallyEq_nhdsWithin_of_eqOn fun _ ↦ congrFun rfl
  · simp_all

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
h : ¬meromorphicOrderAt f (g x) = ⊤
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
F : 𝕜 → E
h₁F : AnalyticAt 𝕜 F (g x)
h₂F : F (g x) ≠ 0
h₃F : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ (meromorphicOrderAt f (g x)).untop₀ • F z
h₁ : meromorphicTrailingCoeffAt (f ∘ g) x = meromorphicTrailingCoeffAt ((fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g) x
⊢ meromorphicTrailingCoeffAt ((fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g) x =
    meromorphicTrailingCoeffAt (fun x_1 ↦ g x_1 - g x) x ^ r • meromorphicTrailingCoeffAt f (g x)

Tactic:
MeromorphicAt.meromorphicTrailingCoeffAt_smul (by fun_prop) (by fun_prop),

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
h : ¬meromorphicOrderAt f (g x) = ⊤
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
F : 𝕜 → E
h₁F : AnalyticAt 𝕜 F (g x)
h₂F : F (g x) ≠ 0
h₃F : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ (meromorphicOrderAt f (g x)).untop₀ • F z
h₁ : meromorphicTrailingCoeffAt (f ∘ g) x = meromorphicTrailingCoeffAt ((fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g) x
⊢ meromorphicTrailingCoeffAt ((fun x_1 ↦ g x_1 - g x) ^ r) x • meromorphicTrailingCoeffAt (F ∘ g) x =
    meromorphicTrailingCoeffAt (fun x_1 ↦ g x_1 - g x) x ^ r • meromorphicTrailingCoeffAt f (g x)
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
w x : ℂ
hx : x ∈ {w}ᶜ
⊢ AnalyticAt ℂ (canonicalFactor R w) x

Tactic:
rw [canonicalFactor_def]

Goal state after:
R : ℝ
w x : ℂ
hx : x ∈ {w}ᶜ
⊢ AnalyticAt ℂ (fun z ↦ (↑R ^ 2 - (starRingEnd ℂ) w * z) / (↑R * (z - w))) x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ meromorphicOrderAt (fun z ↦ (↑R ^ 2 - (starRingEnd ℂ) w * z) / (↑R * (z - w))) w = -1

Tactic:
rw [fun_meromorphicOrderAt_div (by fun_prop) (by fun_prop),
    fun_meromorphicOrderAt_mul (by fun_prop) (by fun_prop)]

Goal state after:
R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ meromorphicOrderAt (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w -
      (meromorphicOrderAt (fun z ↦ ↑R) w + meromorphicOrderAt (fun z ↦ z - w) w) =
    -1
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
ι : Type u_5
s : Finset ι
f : ι → 𝕜 → 𝕜'
hf : ∀ i ∈ s, MeromorphicAt (f i) x
⊢ meromorphicOrderAt (∏ i ∈ s, f i) x = ∑ i ∈ s, meromorphicOrderAt (f i) x

Tactic:
induction s using Finset.induction with

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
a : ℤ
ha : ↑a = meromorphicOrderAt f x
g : 𝕜 → 𝕜'
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = (x_1 - x) ^ a • g x_1
a✝ : 𝕜
⊢ (a✝ ∈ {x}ᶜ → f a✝ = (a✝ - x) ^ a • g a✝) → a✝ ∈ {x}ᶜ → f⁻¹ a✝ = (a✝ - x) ^ (-a) • g⁻¹ a✝

Tactic:
h₁a

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
a : ℤ
ha : ↑a = meromorphicOrderAt f x
g : 𝕜 → 𝕜'
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = (x_1 - x) ^ a • g x_1
a✝ : 𝕜
h₁a : a✝ ∈ {x}ᶜ → f a✝ = (a✝ - x) ^ a • g a✝
⊢ a✝ ∈ {x}ᶜ → f⁻¹ a✝ = (a✝ - x) ^ (-a) • g⁻¹ a✝
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : 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
h₂f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
h₂f₁,

Goal state after:
case pos
𝕜 : 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
h₂f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ min ⊤ (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ < R
this : x ∉ sphere 0 R
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x

Tactic:
have := (D.meromorphicNFOn (mem_closedBall_zero_iff.mpr h.le)).meromorphicOrderAt_eq_zero_iff.2
      (D.ne_zero x (by aesop))

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ < R
this✝ : x ∉ sphere 0 R
this : meromorphicOrderAt g x = 0
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x
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
g : ℂ → E
D : CanonicalDecomp f g R
h₄g : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt g ↑u ≠ ⊤
h : ℂ → E
h₁h : AnalyticOnNhd ℂ h (closedBall 0 R)
h₂h : ∀ (u : ↑(closedBall 0 R)), h ↑u ≠ 0
h₃h : g =ᶠ[codiscreteWithin (closedBall 0 R)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor g (closedBall 0 R)) u) • h
a : ℂ
⊢ f a = ((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g) a →
    g a = ((∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor g (closedBall 0 R)) u) • h) a →
      f a =
        (((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) *
              ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor f (sphere 0 R)) v) •
            h)
          a

Tactic:
h₁a

Goal state after:
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₄g : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt g ↑u ≠ ⊤
h : ℂ → E
h₁h : AnalyticOnNhd ℂ h (closedBall 0 R)
h₂h : ∀ (u : ↑(closedBall 0 R)), h ↑u ≠ 0
h₃h : g =ᶠ[codiscreteWithin (closedBall 0 R)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor g (closedBall 0 R)) u) • h
a : ℂ
h₁a : f a = ((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g) a
⊢ g a = ((∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor g (closedBall 0 R)) u) • h) a →
    f a =
      (((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) *
            ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor f (sphere 0 R)) v) •
          h)
        a
Module: Mathlib.Analysis.Meromorphic.Order

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 𝕜
hf : MeromorphicOn f U
z : ↑U
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y = 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : w = z
⊢ ∃ t, (∀ y ∈ t, ¬y = ↑w → f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑w ∈ t

Tactic:
rw [h₁w]

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y = 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : w = z
⊢ ∃ t, (∀ y ∈ t, ¬y = ↑z → f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑z ∈ t
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 | AnalyticAt 𝕜 f x} ∈ codiscreteWithin U

Tactic:
mem_codiscreteWithin

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ {x | AnalyticAt 𝕜 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
U : Set 𝕜
hf : MeromorphicOn f U
⊢ Subtype.val '' {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤} ∈ codiscreteWithin U

Tactic:
mem_codiscreteWithin

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ Subtype.val '' {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑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 : 𝕜
⊢ (∀ᶠ (x : 𝕜) in 𝓝[{x}ᶜ] a, f x = 0) →
    a ∈ (U \ Subtype.val '' {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤})ᶜ

Tactic:
h₁a

Goal state after:
𝕜 : 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
⊢ a ∈ (U \ Subtype.val '' {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑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 : 𝕜
⊢ AnalyticAt 𝕜 f a ∨ a ∈ Uᶜ →
    f a ≠ 0 → a ∈ (U \ Subtype.val '' {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤})ᶜ

Tactic:
h₁a

Goal state after:
𝕜 : 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 : AnalyticAt 𝕜 f a ∨ a ∈ Uᶜ
⊢ f a ≠ 0 → a ∈ (U \ Subtype.val '' {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤})ᶜ
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
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : ¬MeromorphicAt f (g x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)

Tactic:
rw [meromorphicOrderAt_of_not_meromorphicAt hf, meromorphicOrderAt_of_not_meromorphicAt]

Goal state after:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : ¬MeromorphicAt f (g x)
⊢ ¬MeromorphicAt (f ∘ g) x
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 : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hf : ¬MeromorphicAt f x
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x

Tactic:
rw [meromorphicOrderAt_of_not_meromorphicAt hf, meromorphicOrderAt_of_not_meromorphicAt]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hf : ¬MeromorphicAt f x
⊢ ¬MeromorphicAt (g • f) x
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hB : ‖f z‖ ≤ B
hset : z ∈ verticalClosedStrip 0 1
hM1_one : 1 ≤ ε + sSupNormIm f 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ max 1 ((ε + sSupNormIm f 1) ^ (-1))

Tactic:
apply le_trans _ (le_max_left _ _)
      simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 1),
        neg_re, Real.rpow_le_one_of_one_le_of_nonpos
        hM1_one (Right.neg_nonpos_iff.mpr hset.1)]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicAt f x
a : E
⊢ ContDiffAt ℝ 2 f a → (∀ᶠ (x : E) in 𝓝 a, Δ f x = 0 x) → HarmonicAt f a

Tactic:
h₁a

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicAt f x
a : E
h₁a : ContDiffAt ℝ 2 f a
⊢ (∀ᶠ (x : E) in 𝓝 a, Δ f x = 0 x) → HarmonicAt f a
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
r₁ : ℝ := r - dist z c
r₁_pos : 0 < r₁
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
zRe_mem_s : z.re ∈ s
⊢ (fun x ↦ (∫ (t : ℝ) in z.re..x, f (↑t + ↑z.im * I)) - (x - z.re) • f z) =o[𝓝 z.re] fun x ↦ x - z.re

Tactic:
have f_contOn : ContinuousOn (fun (x : ℝ) ↦ f (x + z.im * I)) s :=
    f_cont.comp ((continuous_add_const _).comp continuous_ofReal).continuousOn <|
      fun _ ↦ mem_ball_re_aux

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
r₁ : ℝ := r - dist z c
r₁_pos : 0 < r₁
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
zRe_mem_s : z.re ∈ s
f_contOn : ContinuousOn (fun x ↦ f (↑x + ↑z.im * I)) s
⊢ (fun x ↦ (∫ (t : ℝ) in z.re..x, f (↑t + ↑z.im * I)) - (x - z.re) • f z) =o[𝓝 z.re] fun x ↦ x - z.re
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
s : Set E
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ ∑ i, (iteratedFDerivWithin ℝ 2 (-f) s x) ![(stdOrthonormalBasis ℝ E) i, (stdOrthonormalBasis ℝ E) i] =
    -∑ i, (iteratedFDerivWithin ℝ 2 f s x) ![(stdOrthonormalBasis ℝ E) i, (stdOrthonormalBasis ℝ E) i]

Tactic:
rw [iteratedFDerivWithin_neg_apply hs hx]

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
s : Set E
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ ∑ i, (-iteratedFDerivWithin ℝ 2 f s x) ![(stdOrthonormalBasis ℝ E) i, (stdOrthonormalBasis ℝ E) i] =
    -∑ i, (iteratedFDerivWithin ℝ 2 f s x) ![(stdOrthonormalBasis ℝ E) i, (stdOrthonormalBasis ℝ E) i]
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
f : E → F
x : E
s : Set E
v : 𝕜
hf : ContDiffWithinAt ℝ 2 f s x
hs : UniqueDiffOn ℝ s
a : E
⊢ ContDiffWithinAt ℝ 2 f s a → a ∈ s → (Δ[s] v • f) a = (v • Δ[s] f) a

Tactic:
h₁a

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
f : E → F
x : E
s : Set E
v : 𝕜
hf : ContDiffWithinAt ℝ 2 f s x
hs : UniqueDiffOn ℝ s
a : E
h₁a : ContDiffWithinAt ℝ 2 f s a
⊢ a ∈ s → (Δ[s] v • f) a = (v • Δ[s] f) a
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
s : Set E
l : F →L[ℝ] G
h : ContDiffWithinAt ℝ 2 f s x
hs : UniqueDiffOn ℝ s
a : E
⊢ ContDiffWithinAt ℝ 2 f s a → a ∈ s → (Δ[s] ⇑l ∘ f) a = (⇑l ∘ Δ[s] f) a

Tactic:
h₁a

Goal state after:
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
s : Set E
l : F →L[ℝ] G
h : ContDiffWithinAt ℝ 2 f s x
hs : UniqueDiffOn ℝ s
a : E
h₁a : ContDiffWithinAt ℝ 2 f s a
⊢ a ∈ s → (Δ[s] ⇑l ∘ f) a = (⇑l ∘ Δ[s] f) a
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
hR : ¬R = 0
x : ℂ
hx : x ∈ {z | ‖z - c‖ ∈ Set.Ioc 0 |R|}
⊢ x ∈ closedBall c |R|

Tactic:
mem_closedBall_iff_norm

Goal state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
hR : ¬R = 0
x : ℂ
hx : x ∈ {z | ‖z - c‖ ∈ Set.Ioc 0 |R|}
⊢ ‖x - c‖ ≤ |R|
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun x ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ (f ∘ fun x ↦ x * I) =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)

Tactic:
simpa only [Function.comp_def, norm_mul, norm_I, mul_one]
      using hO.comp_tendsto ((tendsto_mul_right_cobounded I_ne_zero).inf H.tendsto)

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

Goal state before:
pp: x y : ℝ
z : ℍ
⊢ x +ᵥ z = y +ᵥ z ↔ x = y

Tactic:
by
  simp [UpperHalfPlane.ext_iff]

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

Goal state before:
pp: φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ ((↑R * cexp (↑θ * I) + ↑r * cexp (↑φ * I)) / (↑R * cexp (↑θ * I) - ↑r * cexp (↑φ * I))).re ≤ (R + r) / (R - r)

Tactic:
div_eq_mul_inv

Goal state after:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ ((↑R * cexp (↑θ * I) + ↑r * cexp (↑φ * I)) * (↑R * cexp (↑θ * I) - ↑r * cexp (↑φ * I))⁻¹).re ≤ (R + r) / (R - r)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: case inl
x : ℝ
hx : x < 0
⊢ sin x / x * -x ≤ 1

pp: case inl
x : ℝ
hx : x < 0
⊢ 0 < -x

Tactic:
div_eq_mul_inv

Goal state after:
case inl
x : ℝ
hx : x < 0
⊢ sin x * x⁻¹ * -x ≤ 1

case inl
x : ℝ
hx : x < 0
⊢ 0 < -x
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: x : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
hx₂ : x ≠ -1
⊢ DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) x

Tactic:
by
  fun_prop (disch := grind [log_ne_zero])

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
⊢ log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)

Tactic:
induction s using Finset.induction with

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hint
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ IntervalIntegrable (fun y ↦ ↑y ^ r) MeasureTheory.volume 0 c

Tactic:
· exact intervalIntegrable_cpow' h

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)

Tactic:
simpa only [← Int.natCast_succ, zpow_natCast] using! integral_zpow (Or.inl n.cast_nonneg)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hderiv
b : ℝ
ht : 0 < b
⊢ ∀ x ∈ Set.Ioo 0 b, HasDerivAt (fun x ↦ x * log x - x) (log x) x

Tactic:
intro s ⟨hs, _ ⟩

Goal state after:
case hderiv
b : ℝ
ht : 0 < b
s : ℝ
hs : 0 < s
right✝ : s < b
⊢ HasDerivAt (fun x ↦ x * log x - x) (log s) s
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ 4 * 1 - 4 * cos (x / 2) ^ 2 = 4 * sin (x / 2) ^ 2

Tactic:
← sin_sq_add_cos_sq (x / 2)

Goal state after:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ 4 * (sin (x / 2) ^ 2 + cos (x / 2) ^ 2) - 4 * cos (x / 2) ^ 2 = 4 * sin (x / 2) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ 4 - 4 * cos (x / 2) ^ 2 = 4 * sin (x / 2) ^ 2

Tactic:
by
      nth_rw 1 [← mul_one 4, ← sin_sq_add_cos_sq (x / 2)]
      ring

Goal state after: