mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: z w : ℂ
⊢ cos z = w ↔ cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1 = 0

Tactic:
← sub_eq_zero

Goal state after:
z w : ℂ
⊢ cos z - w = 0 ↔ cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1 = 0
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: f : ℕ → ℝ
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
⊢ Tendsto (fun x ↦ ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)

Tactic:
by
  have m : (𝓝 l).map ofReal ≤ 𝓝 ↑l := ofRealCLM.continuous.tendsto l
  replace h := (tendsto_map.comp h).mono_right m
  rw [Function.comp_def] at h
  push_cast at h
  replace h := Complex.tendsto_tsum_powerSeries_nhdsWithin_lt h
  rw [tendsto_map'_iff] at h
  rw [Metric.tendsto_nhdsWithin_nhds] at h ⊢
  convert! h
  simp_rw [Function.comp_apply, dist_eq_norm]
  norm_cast

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

Goal state before:
pp: x : ℂ
hx : cos x = 0
A : sin x ≠ 0
B : Tendsto cos (𝓝[≠] x) (𝓝[≠] 0)
⊢ Tendsto (fun x ↦ ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop

Tactic:
exact continuous_sin.continuousWithinAt.norm.pos_mul_atTop (norm_pos_iff.2 A)
    (tendsto_norm_nhdsNE_zero.comp B).inv_tendsto_nhdsGT_zero

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

Goal state before:
pp: case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(y ^ 2 + 1)
h : 0 < x
⊢ cos x < 1 / √(x ^ 2 + 1)

pp: case inr
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(y ^ 2 + 1)
h✝ : x < 0
⊢ cos x < 1 / √(x ^ 2 + 1)

Tactic:
· exact this h hx2

Goal state after:
case inr
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(y ^ 2 + 1)
h✝ : x < 0
⊢ cos x < 1 / √(x ^ 2 + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : arctan (-x) + arctan (-y) = arctan ((-x + -y) / (1 - -x * -y)) + π
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Tactic:
show _ / _ = -((x + y) / (1 - x * y)) by ring,

Goal state after:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : arctan (-x) + arctan (-y) = arctan (-((x + y) / (1 - x * y))) + π
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

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

Tactic:
have hy4 : 0 < cos y := cos_pos_of_mem_Ioo ⟨by linarith, hy2'⟩

Goal state after:
case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ cos y < 1 / √(y ^ 2 + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ 2 * arctan 3⁻¹ + arctan 7⁻¹ = π / 4

Tactic:
rw [two_mul_arctan, arctan_add]

Goal state after:
⊢ arctan ((2 * 3⁻¹ / (1 - 3⁻¹ ^ 2) + 7⁻¹) / (1 - 2 * 3⁻¹ / (1 - 3⁻¹ ^ 2) * 7⁻¹)) = π / 4

⊢ 2 * 3⁻¹ / (1 - 3⁻¹ ^ 2) * 7⁻¹ < 1

case h₁
⊢ -1 < 3⁻¹

case h₂
⊢ 3⁻¹ < 1
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
⊢ MonotoneOn (derivWithin f S) S

Tactic:
intro x hx y hy hxy

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
⊢ derivWithin f S x ≤ derivWithin f S y
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
⊢ MonotoneOn (deriv f) S

Tactic:
intro x hx y hy hxy

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
⊢ deriv f x ≤ deriv f y
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
⊢ StrictMonoOn (derivWithin f S) S

Tactic:
intro x hx y hy hxy

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ derivWithin f S x < derivWithin f S y
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
⊢ StrictMonoOn (deriv f) S

Tactic:
intro x hx y hy hxy

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ deriv f x < deriv f y
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
⊢ AntitoneOn (derivWithin f S) S

Tactic:
intro x hx y hy hxy

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
⊢ derivWithin f S y ≤ derivWithin f S x
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : StrictConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
⊢ StrictAntiOn (derivWithin f S) S

Tactic:
intro x hx y hy hxy

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ derivWithin f S y < derivWithin f S x
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inr
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)

Tactic:
set g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)

Goal state after:
case inr
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case refine_1
⊢ IsQuotientMap fun z ↦ ⟨cexp z, ⋯⟩

Tactic:
refine IsOpenMap.isQuotientMap ?_ (by fun_prop) fun z ↦ ⟨_, Subtype.ext (exp_log z.2)⟩

Goal state after:
case refine_1
⊢ IsOpenMap fun z ↦ ⟨cexp z, ⋯⟩
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case ho
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := ⋯
g' : ℂ → ℂ := ⋯
⊢ (fun z ↦ g z - g c) =o[𝓝[≠] c] fun z ↦ (z - c)⁻¹

Tactic:
refine Asymptotics.isBigO_refl (fun w ↦ ((w - c) ^ (n + 1))⁻¹) _ |>.mul_isLittleO hn
        |>.mono (nhdsWithin_le_nhds (s := {c}ᶜ)) |>.congr' ?_ ?_
      · simp [g]
      · refine eventually_mem_nhdsWithin.mono fun w hw ↦ ?_
        rw [mem_compl_singleton_iff, ← sub_ne_zero] at hw
        simp [pow_succ, field]

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

Goal state before:
pp: case inr.refine_1
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
⊢ ∀ z ∈ sphere c R₁, ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)

Tactic:
intro w

Goal state after:
case inr.refine_1
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
w : ℂ
⊢ w ∈ sphere c R₁ → ‖g' w‖ ≤ R₂ / R₁ ^ (n + 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
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)
⊢ MapsTo (⇑(lineMap c z)) (ball 0 (R₁ / dist z c)) (ball c R₁)

Tactic:
intro w

Goal state after:
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)
w : ℂ
⊢ w ∈ ball 0 (R₁ / dist z c) → (lineMap c z) w ∈ ball c R₁
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
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))
hn : (fun x ↦ h x - h 0) =o[𝓝 0] fun w ↦ (w - 0) ^ n
⊢ 1 ∈ ball 0 (R₁ / dist z c)

Tactic:
simpa [lt_div_iff₀, hne]

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
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 ∈ 𝓝 a,
    ∃ g',
      ContinuousOn g' (Set.univ ×ˢ N) ∧
        p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ (t : ↑I), g' (t, a) = g (t, a)

Tactic:
suffices ∀ n, ∃ N, a ∈ N ∧ IsOpen N ∧ ∃ g' : I × A → E, ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
      p ∘ g' = f ∧ (∀ a, g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a) by
    obtain ⟨N, haN, N_open, hN⟩ := this n_max
    simp_rw [h_max _ le_rfl] at hN
    refine ⟨N, N_open.mem_nhds haN, ?_⟩; convert! hN
    · rw [eq_comm, Set.eq_univ_iff_forall]; exact fun t ↦ ⟨bot_le, le_top⟩
    · rw [imp_iff_right]; exact le_top

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
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 : ℕ),
    ∃ 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)
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
⊢ divisor f⁻¹ U = -divisor f U

Tactic:
ext z
  by_cases h : MeromorphicOn f U ∧ z ∈ U
  · simp [divisor_apply, h, meromorphicOrderAt_inv]
  · simp [divisor_def, h]

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 : 𝕜
hf : AnalyticAt 𝕜 f x
⊢ MeromorphicNFAt f x

Tactic:
by
  simp [meromorphicNFAt_iff_analyticAt_or, hf]

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

Goal state before:
pp: case right.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g_f
⊢ g • f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g • g_f

Tactic:
filter_upwards [h₃g_f]
      intro y hy
      simp only [Pi.smul_apply', hy, Pi.pow_apply]
      rw [smul_comm]

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

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

Tactic:
by
  by_cases h : ¬ MeromorphicOn f (U + {c})
  · have := meromorphicOn_comp_add_const_iff_meromorphicOn.not.2 h
    simp_all
  rw [not_not] at h
  have := meromorphicOn_comp_add_const_iff_meromorphicOn.2 h
  by_cases h₁ : ¬ x ∈ (U + {c})
  · rw [Function.locallyFinsuppWithin.apply_eq_zero_of_notMem,
      Function.locallyFinsuppWithin.apply_eq_zero_of_notMem]
    <;> simp_all [← sub_eq_add_neg]
  rw [divisor_apply, divisor_apply]
  <;> simp_all [← sub_eq_add_neg, meromorphicOrderAt_comp_add_const_eq_meromorphicOrderAt]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ : AnalyticAt 𝕜 ⋯.choose x
h'₂ : ⋯.choose x ≠ 0
h'₃ : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose z
y : 𝕜
h₁y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₂y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose y
h₃y : y ∈ {x}ᶜ
⊢ ⋯.choose y = g y

Tactic:
← sub_eq_zero

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ : AnalyticAt 𝕜 ⋯.choose x
h'₂ : ⋯.choose x ≠ 0
h'₃ : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose z
y : 𝕜
h₁y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₂y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose y
h₃y : y ∈ {x}ᶜ
⊢ ⋯.choose y - g y = 0
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case pos.inr
𝕜 : 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
⊢ (if h : True then Function.update f x (if h_1 : meromorphicOrderAt f x = 0 then Classical.choose ⋯ x else 0) else 0)
      x =
    ((fun x_1 ↦ x_1 - x) ^ n • g) x

Tactic:
by_cases h₃f : meromorphicOrderAt f x = 0

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
⊢ (if h : True then Function.update f x (if h_1 : meromorphicOrderAt f x = 0 then Classical.choose ⋯ x else 0) else 0)
      x =
    ((fun x_1 ↦ x_1 - x) ^ n • g) x

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
⊢ (if h : True then Function.update f x (if h_1 : meromorphicOrderAt f x = 0 then Classical.choose ⋯ x else 0) else 0)
      x =
    ((fun x_1 ↦ x_1 - x) ^ n • g) x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
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
⊢ (fun z ↦ ‖(z - x) ^ m • g z‖) =ᶠ[𝓝[≠] x] fun x ↦ ‖f x‖

Tactic:
filter_upwards [hg] with z hz using by simp [hz]

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
⊢ c = 0

Tactic:
exact tendsto_nhds_unique hc (tendsto_zero_of_meromorphicOrderAt_pos ho)

Goal state after:
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
⊢ ∃ g,
    AnalyticOnNhd 𝕜 g U ∧
      (∀ (u : ↑U), g ↑u ≠ 0) ∧ f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u) • g

Tactic:
have hφ : MeromorphicOn φ U := (meromorphicNFOn (divisor f U) U).meromorphicOn

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,
    AnalyticOnNhd 𝕜 g U ∧
      (∀ (u : ↑U), g ↑u ≠ 0) ∧ f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u) • g
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
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
cont_A : ∀ (a : A), Continuous[_, inst✝²] fun x ↦ g (x, a)
⊢ ∀ (x : ↑I × A), ContinuousAt g x

Tactic:
intro ⟨t, a⟩

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
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
cont_A : ∀ (a : A), Continuous[_, inst✝²] fun x ↦ g (x, a)
t : ↑I
a : A
⊢ ContinuousAt g (t, a)
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: f : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ ∃ a, f = rotation a ∨ f = conjLIE.trans (rotation a)

Tactic:
let a : Circle := ⟨f 1, by simp [Submonoid.unitSphere, f.norm_map]⟩

Goal state after:
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
⊢ ∃ a, f = rotation a ∨ f = conjLIE.trans (rotation a)
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case h.left
𝕜 : 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
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
⊢ Subtype.val ⁻¹' t' ⊆ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ

Tactic:
intro w

Goal state after:
case h.left
𝕜 : 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
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
⊢ w ∈ Subtype.val ⁻¹' t' → w ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖map 1‖ ≠ 0
⊢ ∀ (x : ℂ), ‖(‖map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖

Tactic:
intro x
    simp only [LinearMap.smul_apply]
    have : x = x • (1 : ℂ) := by rw [smul_eq_mul, mul_one]
    nth_rw 1 [this]
    rw [LinearMap.coe_restrictScalars]
    simp only [map.coe_coe, map.map_smul, norm_smul, norm_inv, norm_norm]
    field

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

Goal state before:
pp: case right
𝕜 : 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
hz : meromorphicOrderAt f ↑z = ⊤
⊢ ∃
    x ⊆
      {x |
        ∃ t, (∀ y ∈ t, y ∈ {↑x}ᶜ → f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x

Tactic:
rw [meromorphicOrderAt_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at hz

Goal state after:
case right
𝕜 : 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
hz : ∃ t, (∀ y ∈ t, y ∈ {↑z}ᶜ → f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑z ∈ t
⊢ ∃
    x ⊆
      {x |
        ∃ t, (∀ y ∈ t, y ∈ {↑x}ᶜ → f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case h
𝕜 : 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'
⊢ Subtype.val ⁻¹' t' ⊆
    {x | ∃ t, (∀ y ∈ t, ¬y = ↑x → f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t}

Tactic:
intro w

Goal state after:
case h
𝕜 : 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
⊢ w ∈ Subtype.val ⁻¹' t' →
    w ∈ {x | ∃ t, (∀ y ∈ t, ¬y = ↑x → f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t}