mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
⊢ angle x y = 0

Tactic:
← inner_eq_mul_norm_iff_angle_eq_zero hx hy

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inr
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₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : g (f z - f c) = ↑‖f z - f c‖
h : ℂ → ℂ := ⇑g ∘ f ∘ ⇑(lineMap c z)
hmaps_line : MapsTo (⇑(lineMap c z)) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)

Tactic:
have hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c)) :=
    g.differentiable.comp_differentiableOn <| hd.comp (lineMap c z).differentiableOn hmaps_line

Goal state after:
case inr
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₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : g (f z - f c) = ↑‖f z - f c‖
h : ℂ → ℂ := ⇑g ∘ f ∘ ⇑(lineMap c z)
hmaps_line : MapsTo (⇑(lineMap c z)) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
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 f U
hf : ∀ (x : X), f x ^ ↑n = (UnitDisc.coe ∘ g) x
⊢ ∃ f, ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x

Tactic:
suffices ∀ x, ‖f x‖ < 1 by
    lift f to X → 𝔻 using this
    refine ⟨f, isEmbedding_coe.continuousOn_iff.mpr hfc, fun x ↦ ?_⟩
    simpa only [← coe_pow, Function.comp_apply, coe_inj] using hf 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 f U
hf : ∀ (x : X), f x ^ ↑n = (UnitDisc.coe ∘ g) x
⊢ ∀ (x : X), ‖f x‖ < 1
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₁ R₂ : ℝ
f : E → F
c : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
this : 0 ≤ R₂
z : E
⊢ z ∈ ball c R₁ → ‖f z - f c‖ ≤ R₂ / R₁ * ‖z - c‖

Tactic:
hz

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
R₁ R₂ : ℝ
f : E → F
c : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
this : 0 ≤ R₂
z : E
hz : z ∈ ball c R₁
⊢ ‖f z - f c‖ ≤ R₂ / R₁ * ‖z - c‖
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
⊢ MeromorphicNFAt f x

Tactic:
· right
        use analyticOrderNatAt f x
        have : analyticOrderAt f x ≠ ⊤ := h₂f
        rw [← ENat.natCast_toNat_eq_self, eq_comm, h.analyticOrderAt_eq_natCast] at this
        obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
        use g, h₁g, h₂g
        simpa

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : ↑n = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or : MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ ↑n < 0 ∧ f x = 0
h₂ : ↑n < 0
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 : 𝕜
⊢ (z ∈ {x}ᶜ → f z = (z - x) ^ n • g z) → f z = ((fun x_1 ↦ x_1 - x) ^ n • g) z

Tactic:
hz

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : ↑n = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or : MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ ↑n < 0 ∧ f x = 0
h₂ : ↑n < 0
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 : 𝕜
hz : z ∈ {x}ᶜ → f z = (z - x) ^ n • g z
⊢ f z = ((fun x_1 ↦ x_1 - x) ^ n • g) z
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
⊢ (divisor (f₁ + f₂) U)⁻ ≤ (divisor f₁ U)⁻ + (divisor f₂ U)⁻

Tactic:
calc (divisor (f₁ + f₂) U)⁻
    _ ≤ max (divisor f₁ U)⁻ (divisor f₂ U)⁻ :=
      negPart_divisor_add_le_max hf₁ hf₂
    _ ≤ (divisor f₁ U)⁻ + (divisor f₂ U)⁻ := by
      by_cases h : (divisor f₁ U)⁻ ≤ (divisor f₂ U)⁻
      <;> simp_all [negPart_nonneg]

Goal state after:
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 (fun a ↦ ∏ i ∈ s, f i a) x

Tactic:
by
  convert! meromorphicNFAt_prod h₁f h₂f
  exact (Finset.prod_apply _ s f).symm

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf : f =ᶠ[𝓝 x] 0
z : 𝕜
⊢ f z = 0 z → (f ^ n) z = 0 z

Tactic:
hz

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf : f =ᶠ[𝓝 x] 0
z : 𝕜
hz : f z = 0 z
⊢ (f ^ n) z = 0 z
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ m • g
z : 𝕜
⊢ f z = ((fun x_1 ↦ x_1 - x) ^ m • g) z → (f ^ n) z = ((fun x_1 ↦ x_1 - x) ^ (n * m) • g ^ n) z

Tactic:
hz

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ m • g
z : 𝕜
hz : f z = ((fun x_1 ↦ x_1 - x) ^ m • g) z
⊢ (f ^ n) z = ((fun x_1 ↦ x_1 - x) ^ (n * m) • g ^ n) z
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
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf✝ • f z = 0
z : 𝕜
hf : (z - x) ^ Exists.choose hf✝ • f z = 0
⊢ ¬z = x → f z = 0

Tactic:
hz

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf✝ : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf✝ • f z = 0
z : 𝕜
hf : (z - x) ^ Exists.choose hf✝ • f z = 0
hz : ¬z = x
⊢ f z = 0
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : DecidableEq 𝕜
x y : 𝕜
h : ¬x = y
⊢ meromorphicTrailingCoeffAt (fun x ↦ x - y) x = if x = y then 1 else x - y

Tactic:
simp_all only [ite_false]

Goal state after:
case neg
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : DecidableEq 𝕜
x y : 𝕜
h : ¬x = y
⊢ meromorphicTrailingCoeffAt (fun x ↦ x - y) x = x - y
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
x : 𝕜
hf : MeromorphicNFAt f x
z : 𝕜
hz : z = x
⊢ toMeromorphicNFAt f x z = f z

Tactic:
hz

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
z : 𝕜
hz : z = x
⊢ toMeromorphicNFAt f x x = f x
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2.refine_3
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
x✝¹ :
  ∃ N,
    a ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a)
N : Set A
haN : a ∈ N
N_open : IsOpen[inst✝] N
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a) = g (t', a)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q e).source
this : Set.Icc (t n) (t (n + 1)) ×ˢ {a} ⊆ ⇑f ⁻¹' (q e).target
u : Set ↑I
v : Set A
v_open : IsOpen[inst✝] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav✝ : {a} ⊆ v
huv : u ×ˢ v ⊆ ⇑f ⁻¹' (q e).target
ta : ↑I × A
x✝ : ta ∈ Set.Icc 0 (t n.succ) ×ˢ (v ∩ (N ∩ (g' ∘ fun y ↦ (t n, y)) ⁻¹' (q e).source)) ∩ frontier {a | a.1 ≤ t n}
left✝¹ : ta.1 ∈ Set.Icc 0 (t n.succ)
hav : ta.2 ∈ v
left✝ : ta.2 ∈ N
ha : ta.2 ∈ (g' ∘ fun y ↦ (t n, y)) ⁻¹' (q e).source
hfr : ta ∈ frontier {a | a.1 ≤ t n}
⊢ g' ta = if f ta ∈ (q e).target then ↑(q e).symm (f ta) else g ta

Tactic:
have ht := Set.mem_ofPred.mp (frontier_le_subset_eq continuous_fst continuous_const hfr)
    have : f ta ∈ (q e).target := huv ⟨hu (by rw [ht]; exact ⟨le_rfl, t_mono n.le_succ⟩), hav⟩
    rw [if_pos this]
    -- here we use that {tₙ} × Nₙ₊₁ is mapped to the domain of `q e`
    apply (q e).injOn (by rwa [← ta.eta, ht]) ((q e).map_target this)
    rw [(q e).right_inv this, ← hpq e]; exact congr($g'_lifts ta)

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 : 𝕜
n : ℤ
hf : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = 0
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = (x_1 - x) ^ n • g x_1
z : 𝕜
hfz : (z - x) ^ Exists.choose hf • f z = 0
hfz_eq : z ∈ {x}ᶜ → f z = (z - x) ^ n • g z
⊢ z ∈ {x}ᶜ → g z = 0

Tactic:
hz

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = 0
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = (x_1 - x) ^ n • g x_1
z : 𝕜
hfz : (z - x) ^ Exists.choose hf • f z = 0
hfz_eq : z ∈ {x}ᶜ → f z = (z - x) ^ n • g z
hz : z ∈ {x}ᶜ
⊢ g 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
h✝ : ¬analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
m : ℕ
h : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq✝ : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = (z - x) ^ m • g z
z : 𝕜
hg_eq : (z - x) ^ Exists.choose hf • f z = (z - x) ^ m • g z
⊢ z ∈ {x}ᶜ → f z = (z - x) ^ (↑m - ↑(Exists.choose hf)) • g z

Tactic:
hz

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h✝ : ¬analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
m : ℕ
h : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq✝ : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = (z - x) ^ m • g z
z : 𝕜
hg_eq : (z - x) ^ Exists.choose hf • f z = (z - x) ^ m • g z
hz : z ∈ {x}ᶜ
⊢ f z = (z - x) ^ (↑m - ↑(Exists.choose hf)) • g z
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
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ - f₂) x = meromorphicTrailingCoeffAt f₁ x

Tactic:
rw [sub_eq_add_neg]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ + -f₂) x = meromorphicTrailingCoeffAt f₁ x
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 : 𝕜
⊢ z ∈ U → MeromorphicNFAt f z

Tactic:
hz

Goal state after:
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
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mpr
𝕜 : 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 f U
z : 𝕜
⊢ z ∈ U → MeromorphicNFAt (g • f) z

Tactic:
hz

Goal state after:
case mpr
𝕜 : 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 f U
z : 𝕜
hz : z ∈ U
⊢ MeromorphicNFAt (g • f) z
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 : 𝕜
ho : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
m : ℤ
hm : ↑m = meromorphicOrderAt f x
m_neg : m < 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • g z
A : Tendsto (fun z ↦ ‖(z - x) ^ m • g z‖) (𝓝[≠] x) atTop
z : 𝕜
⊢ f z = (z - x) ^ m • g z → ‖(z - x) ^ m • g z‖ = ‖f z‖

Tactic:
hz

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
ho : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
m : ℤ
hm : ↑m = meromorphicOrderAt f x
m_neg : m < 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • g z
A : Tendsto (fun z ↦ ‖(z - x) ^ m • g z‖) (𝓝[≠] x) atTop
z : 𝕜
hz : f z = (z - x) ^ m • g z
⊢ ‖(z - x) ^ m • g z‖ = ‖f z‖
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 𝕜
hf : MeromorphicOn f U
z : 𝕜
⊢ z ∈ U → MeromorphicNFAt (toMeromorphicNFOn f U) z

Tactic:
hz

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 : 𝕜
hz : z ∈ U
⊢ MeromorphicNFAt (toMeromorphicNFOn f U) z
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : HasFiniteMulSupport fun u ↦ (fun x ↦ x - u) ^ d u
z : 𝕜
⊢ z ∈ Finite.toFinset h₁ → ((fun x ↦ x - z) ^ d z) x ≠ 0

Tactic:
hz

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : HasFiniteMulSupport fun u ↦ (fun x ↦ x - u) ^ d u
z : 𝕜
hz : z ∈ Finite.toFinset h₁
⊢ ((fun x ↦ x - z) ^ d z) x ≠ 0
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
z : 𝕜
⊢ z ∈ univ → MeromorphicNFAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) z

Tactic:
hz

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
z : 𝕜
hz : z ∈ univ
⊢ MeromorphicNFAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) z
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
⊢ meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) z ≠ ⊤

Tactic:
by_cases hd : d.support.Finite
  · simp [meromorphicOrderAt_eq d hd]
  · rw [← mulSupport] at hd
    simp [finprod_of_infinite_mulSupport hd]

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

Goal state before:
pp: R : ℝ
w : ℂ
h : w ∈ ball 0 R
z : ℂ
⊢ z ∈ univ → MeromorphicNFAt (canonicalFactor R w) z

Tactic:
hz

Goal state after:
R : ℝ
w : ℂ
h : w ∈ ball 0 R
z : ℂ
hz : z ∈ univ
⊢ MeromorphicNFAt (canonicalFactor R w) z
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 : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
this : 0 ≤ meromorphicOrderAt f x
n : ℕ
ho : meromorphicOrderAt f x = ↑↑n
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ ↑n • g z
z : 𝕜
⊢ f z = (z - x) ^ ↑n • g z → (z - x) ^ n • g z = f z

Tactic:
hz

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
this : 0 ≤ meromorphicOrderAt f x
n : ℕ
ho : meromorphicOrderAt f x = ↑↑n
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ ↑n • g z
z : 𝕜
hz : f z = (z - x) ^ ↑n • g z
⊢ (z - x) ^ n • g z = f z
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
⊢ meromorphicOrderAt ((fun x_1 ↦ x_1 - x) ^ n) x = ↑n

Tactic:
by
  rw [meromorphicOrderAt_eq_int_iff (by fun_prop)]
  exact ⟨fun z ↦ 1, by fun_prop, one_ne_zero, by aesop⟩

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
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
h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
z : 𝕜
⊢ f z = 0 → (f • g) z = 0

Tactic:
hz

Goal state after:
𝕜 : 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
h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
z : 𝕜
hz : f z = 0
⊢ (f • g) 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
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
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = 0
z : 𝕜
⊢ g z = 0 → (f • g) z = 0

Tactic:
hz

Goal state after:
𝕜 : 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
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = 0
z : 𝕜
hz : g z = 0
⊢ (f • g) z = 0
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
z : 𝕜
⊢ z ∈ U → meromorphicOrderAt φ⁻¹ z ≠ ⊤

Tactic:
hz

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
z : 𝕜
hz : z ∈ U
⊢ meromorphicOrderAt φ⁻¹ z ≠ ⊤
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
h₂f : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f⁻¹ x = -⊤

Tactic:
← LinearOrderedAddCommGroupWithTop.neg_top,

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
h₂f : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f⁻¹ x = - -⊤