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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∈ U
⊢ f₁ =ᶠ[𝓝[≠] x] f₂

Tactic:
simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin, disjoint_principal_right] at h₁

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
⊢ f₁ =ᶠ[𝓝[≠] x] f₂
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case right.right
𝕜 : 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
⊢ f ^ n =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ (n * m) • g ^ n

Tactic:
filter_upwards [h₃g] with z 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.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 : MeromorphicAt f x
⊢ MeromorphicNFAt (toMeromorphicNFAt f x) x

Tactic:
by_cases h₂f : meromorphicOrderAt f x = ⊤
    · have : toMeromorphicNFAt f x =ᶠ[𝓝 x] 0 := by
        apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE
        · exact hf.eq_nhdsNE_toMeromorphicNFAt.symm.trans (meromorphicOrderAt_eq_top_iff.1 h₂f)
        · simp [h₂f, toMeromorphicNFAt, hf]
      apply AnalyticAt.meromorphicNFAt
      rw [analyticAt_congr this]
      exact analyticAt_const
    · lift meromorphicOrderAt f x to ℤ using h₂f with n hn
      obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff hf).1 hn.symm
      right
      use n, g, h₁g, h₂g
      apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE (hf.eq_nhdsNE_toMeromorphicNFAt.symm.trans h₃g)
      simp only [toMeromorphicNFAt, hf, ↓reduceDIte, ← hn, WithTop.coe_zero,
        WithTop.coe_eq_zero, ne_eq, Function.update_self, sub_self]
      split_ifs with h₃f
      · obtain ⟨h₁G, _, h₃G⟩ :=
          Classical.choose_spec ((meromorphicOrderAt_eq_int_iff hf).1 (h₃f ▸ hn.symm))
        apply Filter.EventuallyEq.eq_of_nhds
        apply (h₁G.continuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop)).1
        filter_upwards [h₃g, h₃G]
        simp_all
      · simp [h₃f, zero_zpow]

Goal state after:
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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
this : meromorphicOrderAt f x = ↑n
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
⊢ Function.update f x (Classical.choose ⋯ x) x = 0 ^ n • g x

Tactic:
hn

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
this : meromorphicOrderAt f x = ↑n
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
⊢ Function.update f x (Classical.choose ⋯ x) x = 0 ^ 0 • g x
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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
this : meromorphicOrderAt f x = ↑n
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
h₀ : AnalyticAt 𝕜 (Classical.choose ⋯) x
h₁ : Classical.choose ⋯ x ≠ 0
h₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ 0 • Classical.choose ⋯ z
⊢ g =ᶠ[𝓝[≠] x] Classical.choose ⋯

Tactic:
hn

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ 0 • g
this : meromorphicOrderAt f x = ↑n
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
h₀ : AnalyticAt 𝕜 (Classical.choose ⋯) x
h₁ : Classical.choose ⋯ x ≠ 0
h₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ 0 • Classical.choose ⋯ z
⊢ g =ᶠ[𝓝[≠] x] Classical.choose ⋯
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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
this : meromorphicOrderAt f x = ↑n
h₃f : ¬meromorphicOrderAt f x = 0
hn : n = 0
⊢ False

Tactic:
hn

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
this : meromorphicOrderAt f x = ↑0
h₃f : ¬meromorphicOrderAt f x = 0
hn : n = 0
⊢ False
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 : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
⊢ toMeromorphicNFOn f U =ᶠ[𝓝 x] toMeromorphicNFAt f x

Tactic:
simp [(toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds hf hx).trans]

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case neg
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
_ : ¬ta.1 ≤ t n
hv : f ta ∉ (q e).target
⊢ p (g ta) = f ta

Tactic:
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
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
⊢ meromorphicOrderAt (f • g) x = meromorphicOrderAt f x + meromorphicOrderAt g x

Tactic:
cases h₂f : meromorphicOrderAt f x with
  | top =>
    simp only [top_add, meromorphicOrderAt_eq_top_iff] at h₂f ⊢
    filter_upwards [h₂f] with z hz using by simp [hz]
  | coe m =>
    cases h₂g : meromorphicOrderAt g x with
    | top =>
      simp only [add_top, meromorphicOrderAt_eq_top_iff] at h₂g ⊢
      filter_upwards [h₂g] with z hz using by simp [hz]
    | coe n => -- Non-trivial case: both functions do not vanish around z₀
      rw [← WithTop.coe_add, meromorphicOrderAt_eq_int_iff (hf.smul hg)]
      obtain ⟨F, h₁F, h₂F, h₃F⟩ := (meromorphicOrderAt_eq_int_iff hf).1 h₂f
      obtain ⟨G, h₁G, h₂G, h₃G⟩ := (meromorphicOrderAt_eq_int_iff hg).1 h₂g
      use F • G, h₁F.smul h₁G, by simp [h₂F, h₂G]
      filter_upwards [self_mem_nhdsWithin, h₃F, h₃G] with a ha hfa hga
      simp [hfa, hga, smul_comm (F a), zpow_add₀ (sub_ne_zero.mpr ha), mul_smul]

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

Goal state before:
pp: case pos
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
⊢ ∃ g, CanonicalDecomp f g R

pp: case neg
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
⊢ ∃ g, CanonicalDecomp f g R

Tactic:
· use fun _ ↦ f 0
    exact {
      meromorphicOn := h₁f
      meromorphicNFOn := fun z hz ↦ AnalyticAt.meromorphicNFAt analyticAt_const
      ne_zero := by simp [ball_eq_empty.2 hR]
      eventuallyEq := by
        filter_upwards [self_mem_codiscreteWithin (closedBall 0 R)] with a ha
        have : R = 0 := by grind [nonneg_of_mem_closedBall ha]
        aesop
    }

Goal state after:
case neg
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
⊢ ∃ g, CanonicalDecomp f g R
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case neg.refine_3
𝕜 : 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_eq_left_of_lt : MeromorphicAt f₂ x → ↑n₁ < ↑n₂ → meromorphicOrderAt (f₁ + f₂) x = ↑n₁
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
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 : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + (fun x_1 ↦ x_1 - x) ^ (n₂ - n₁) • g₂) z

Tactic:
· filter_upwards [h₃g₁, h₃g₂, self_mem_nhdsWithin]
    simp_all [smul_add, ← smul_assoc, ← zpow_add', sub_ne_zero]

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

Goal state before:
pp: case h
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
⊢ f = rotation a ∨ f = conjLIE.trans (rotation a)

Tactic:
refine (linear_isometry_complex_aux this).imp (fun h₁ => ?_) fun h₂ => ?_

Goal state after:
case h.refine_1
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
h₁ : f.trans (rotation a).symm = LinearIsometryEquiv.refl ℝ ℂ
⊢ f = rotation a

case h.refine_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
h₂ : f.trans (rotation a).symm = conjLIE
⊢ f = conjLIE.trans (rotation a)
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 0 + 1 = ?m.47

Tactic:
norm_num1

Goal state after:
⊢ 1 = ?m.47
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 1 + 1 = ?m.57

Tactic:
norm_num1

Goal state after:
⊢ 2 = ?m.57
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 2 + 1 = ?m.67

Tactic:
norm_num1

Goal state after:
⊢ 3 = ?m.67
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 3 + 1 = ?m.77

Tactic:
norm_num1

Goal state after:
⊢ 4 = ?m.77
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 4 + 1 = ?m.87

Tactic:
norm_num1

Goal state after:
⊢ 5 = ?m.87
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 5 + 1 = ?m.97

Tactic:
norm_num1

Goal state after:
⊢ 6 = ?m.97
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 6 + 1 = ?m.107

Tactic:
norm_num1

Goal state after:
⊢ 7 = ?m.107
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 7 + 1 = ?m.117

Tactic:
norm_num1

Goal state after:
⊢ 8 = ?m.117
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 8 + 1 = ?m.127

Tactic:
norm_num1

Goal state after:
⊢ 9 = ?m.127
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 9 + 1 = ?m.137

Tactic:
norm_num1

Goal state after:
⊢ 10 = ?m.137
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 10 + 1 = ?m.147

Tactic:
norm_num1

Goal state after:
⊢ 11 = ?m.147
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 11 + 1 = ?m.157

Tactic:
norm_num1

Goal state after:
⊢ 12 = ?m.157
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 12 + 1 = ?m.167

Tactic:
norm_num1

Goal state after:
⊢ 13 = ?m.167
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 13 + 1 = ?m.178

Tactic:
norm_num1

Goal state after:
⊢ 14 = ?m.178
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |1 -
        (((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) * 9 -
                        1) *
                      10 -
                    1) *
                  11 -
                1) *
              12 -
            1) *
          13| ≤
    1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 - |1| / 14 * ((14 + 1) / 14)

Tactic:
norm_num1

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

Goal state before:
pp: ⊢ 13 + 1 = ?m.177

Tactic:
norm_num1

Goal state after:
⊢ 14 = ?m.177
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 14 + 1 = ?m.187

Tactic:
norm_num1

Goal state after:
⊢ 15 = ?m.187
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 15 + 1 = ?m.197

Tactic:
norm_num1

Goal state after:
⊢ 16 = ?m.197
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 16 + 1 = ?m.207

Tactic:
norm_num1

Goal state after:
⊢ 17 = ?m.207
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 17 + 1 = ?m.217

Tactic:
norm_num1

Goal state after:
⊢ 18 = ?m.217
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 18 + 1 = ?m.227

Tactic:
norm_num1

Goal state after:
⊢ 19 = ?m.227
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 19 + 1 = ?m.237

Tactic:
norm_num1

Goal state after:
⊢ 20 = ?m.237
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 20 + 1 = ?m.247

Tactic:
norm_num1

Goal state after:
⊢ 21 = ?m.247
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

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

Tactic:
MeromorphicAt.meromorphicTrailingCoeffAt_smul (by fun_prop)
        (D.analyticOnNhd w hw).meromorphicAt,

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

Goal state before:
pp: ⊢ 21 + 1 = ?m.258

Tactic:
norm_num1

Goal state after:
⊢ 22 = ?m.258
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |1 -
        (((((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) *
                                                                  7 -
                                                                1) *
                                                              8 -
                                                            1) *
                                                          9 -
                                                        1) *
                                                      10 -
                                                    1) *
                                                  11 -
                                                1) *
                                              12 -
                                            1) *
                                          13 -
                                        1) *
                                      14 -
                                    1) *
                                  15 -
                                1) *
                              16 -
                            1) *
                          17 -
                        1) *
                      18 -
                    1) *
                  19 -
                1) *
              20 -
            1) *
          21| ≤
    1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 * 18 * 19 * 20 * 21 -
      |1| / 22 * ((22 + 1) / 22)

Tactic:
norm_num1

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

Goal state before:
pp: ⊢ 0.6931471803 < 287209 / 414355 - 1 / 10 ^ 10

Tactic:
norm_num1

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

Goal state before:
pp: ⊢ 1.0986122885 < 109861228867 / 100000000000 - 1 / 10 ^ 10

Tactic:
norm_num1

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
H' : ↑I × A → E
x✝¹ : (∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)) ∧ p ∘ H' = ⇑H ∧ ∀ (a : A), H' (0, a) = f a
H'_cont : ∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)
H'_lifts : p ∘ H' = ⇑H
H'_0 : ∀ (a : A), H' (0, a) = f a
x✝ : ↑I × A
t : ↑I
a : A
⊢ H' (t, a) = (cov.liftHomotopy H f H_0) (t, a)

Tactic:
· apply congr_fun ((cov.eq_liftPath_iff _).mpr ⟨H'_cont a, _, H'_0 a⟩) t
    ext ⟨t, a⟩; exact congr_fun H'_lifts _

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

Goal state before:
pp: ⊢ 1.6094379123 < 160943791243 / 100000000000 - 1 / 10 ^ 10

Tactic:
norm_num1

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst✝ : PreconnectedSpace A
f₀' f₁' : C(A, E)
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
rel : ∀ (t : ↑I), ∀ a ∈ S, (cov.liftHomotopy (↑F) f₀' F_0) (t, a) = f₀' a
a : A
ha : a ∈ S
he : f₀' a = f₁' a
⊢ ∀ (x : A), (cov.liftHomotopy (↑F) f₀' F_0).toFun (1, x) = f₁' x

Tactic:
simp_rw [toFun_eq_coe, ← ContinuousMap.curry_apply]

Goal state after:
E : Type u_1
X : Type u_2
A : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst✝ : PreconnectedSpace A
f₀' f₁' : C(A, E)
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
rel : ∀ (t : ↑I), ∀ a ∈ S, (cov.liftHomotopy (↑F) f₀' F_0) (t, a) = f₀' a
a : A
ha : a ∈ S
he : f₀' a = f₁' a
⊢ ∀ (x : A), ((cov.liftHomotopy (↑F) f₀' F_0).curry 1) x = f₁' x
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
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hf : MeromorphicAt f x
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x

Tactic:
simp [meromorphicOrderAt_smul hg.meromorphicAt hf, hg.meromorphicOrderAt_eq,
      hg.analyticOrderAt_eq_zero.mpr hg']

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
⊢ canonicalCovariantTensor E = ∑ i, v i ⊗ₜ[ℝ] v i

Tactic:
let w := stdOrthonormalBasis ℝ E
  calc ∑ m, w m ⊗ₜ[ℝ] w m
  _ = ∑ m, ∑ n, ⟪w m, w n⟫_ℝ • w m ⊗ₜ[ℝ] w n := by
    congr 1 with m
    rw [Fintype.sum_eq_single m _, orthonormal_iff_ite.1 w.orthonormal]
    · simp only [↓reduceIte, one_smul]
    simp only [orthonormal_iff_ite.1 w.orthonormal, ite_smul, one_smul, zero_smul,
      ite_eq_right_iff]
    tauto
  _ = ∑ m, ∑ n, (∑ i, ⟪w m, v i⟫_ℝ * ⟪v i, w n⟫_ℝ) • w m ⊗ₜ[ℝ] w n := by
    simp_rw [OrthonormalBasis.sum_inner_mul_inner v]
  _ = ∑ m, ∑ n, (∑ i, ⟪w m, v i⟫_ℝ * ⟪w n, v i⟫_ℝ) • w m ⊗ₜ[ℝ] w n := by
    simp only [real_inner_comm (w _)]
  _ = ∑ i, (∑ m, ⟪w m, v i⟫_ℝ • w m) ⊗ₜ[ℝ] ∑ n, ⟪w n, v i⟫_ℝ • w n := by
    simp only [sum_tmul, tmul_sum, smul_tmul_smul, Finset.sum_comm (γ := ι), Finset.sum_smul]
    rw [Finset.sum_comm]
  _ = ∑ i, v i ⊗ₜ[ℝ] v i := by
    simp only [w.sum_repr' (v _)]

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

Goal state before:
pp: case neg.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (HPow.hPow ↑(sSupNormIm f 1)) z

Tactic:
refine DifferentiableAt.const_cpow ?_ ?_

Goal state after:
case neg.refine_2.refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (fun x ↦ x) z

case neg.refine_2.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 1) ≠ 0 ∨ z ≠ 0