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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
⊢ ∃ q ⊆ s, q.Finite ∧ sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ

Tactic:
have : sphere 0 1 ⊆ ⋃ y ∈ s, ball y δ := by
      apply hs.trans (fun z hz ↦ ?_)
      obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, dist z y < δ := Metric.mem_closure_iff.1 hz δ δpos
      exact mem_biUnion ys hy

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
this : sphere 0 1 ⊆ ⋃ y ∈ s, ball y δ
⊢ ∃ q ⊆ s, q.Finite ∧ sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y ↦ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)

Tactic:
use SupSet.sSup (g '' Icc a b) / (n !)

Goal state after:
case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := ⋯
⊢ ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) / ↑n ! * (x - a) ^ (n + 1)
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: case h.h.h.h
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H : √((1 - z).re ^ 2 + z.im ^ 2) < M * (1 - √((1 - (1 - z).re) ^ 2 + z.im ^ 2))
⊢ z ∈ stolzSet M

Tactic:
have h : z.im ^ 2 = (1 - z).im ^ 2 := by
    simp only [sub_im, one_im, zero_sub, neg_sq]

Goal state after:
case h.h.h.h
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H : √((1 - z).re ^ 2 + z.im ^ 2) < M * (1 - √((1 - (1 - z).re) ^ 2 + z.im ^ 2))
h : z.im ^ 2 = (1 - z).im ^ 2
⊢ z ∈ stolzSet M
Module: Mathlib.Analysis.Normed.Module.Ray

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
r : ℝ
hr : 0 ≤ r
hy : r • x ∈ {y | SameRay ℝ x y}
s : ℝ
hs : 0 ≤ s
hz : s • x ∈ {y | SameRay ℝ x y}
h : ‖r‖ = ‖s‖
⊢ r • x = s • x

Tactic:
norm_of_nonneg hr,

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
r : ℝ
hr : 0 ≤ r
hy : r • x ∈ {y | SameRay ℝ x y}
s : ℝ
hs : 0 ≤ s
hz : s • x ∈ {y | SameRay ℝ x y}
h : r = ‖s‖
⊢ r • x = s • x
Module: Mathlib.Analysis.Convex.Uniform

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ‖x + y‖ ≤ 2 - δ'

Tactic:
have hxy' : ε / 3 ≤ ‖x' - y'‖ :=
    calc
      ε / 3 = ε - (ε / 3 + ε / 3) := by ring
      _ ≤ ‖x - y‖ - (‖x' - x‖ + ‖y' - y‖) := by
        gcongr
        · exact (h₂ _ hx hx'.le).trans <| min_le_of_right_le <| min_le_left _ _
        · exact (h₂ _ hy hy'.le).trans <| min_le_of_right_le <| min_le_left _ _
      _ ≤ _ := by
        have : ∀ x' y', x - y = x' - y' + (x - x') + (y' - y) := fun _ _ => by abel
        rw [sub_le_iff_le_add, norm_sub_rev _ x, ← add_assoc, this]
        exact norm_add₃_le

Goal state after:
case inr.inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ ‖x + y‖ ≤ 2 - δ'
Module: Mathlib.Analysis.Convex.Uniform

Goal state before:
pp: E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
⊢ ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ

Tactic:
by
  have hε' : 0 < ε / 3 := div_pos hε zero_lt_three
  obtain ⟨δ, hδ, h⟩ := exists_forall_sphere_dist_add_le_two_sub E hε'
  set δ' := min (1 / 2) (min (ε / 3) <| δ / 3)
  refine ⟨δ', lt_min one_half_pos <| lt_min hε' (div_pos hδ zero_lt_three), fun x hx y hy hxy => ?_⟩
  obtain hx' | hx' := le_or_gt ‖x‖ (1 - δ')
  · rw [← one_add_one_eq_two]
    exact (norm_add_le_of_le hx' hy).trans (sub_add_eq_add_sub _ _ _).le
  obtain hy' | hy' := le_or_gt ‖y‖ (1 - δ')
  · rw [← one_add_one_eq_two]
    exact (norm_add_le_of_le hx hy').trans (add_sub_assoc _ _ _).ge
  have hδ' : 0 < 1 - δ' := sub_pos_of_lt (min_lt_of_left_lt one_half_lt_one)
  have h₁ : ∀ z : E, 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1 := by
    rintro z hz
    rw [norm_smul_of_nonneg (inv_nonneg.2 <| norm_nonneg _), inv_mul_cancel₀ (hδ'.trans hz).ne']
  have h₂ : ∀ z : E, ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ' := by
    rintro z hz hδz
    nth_rw 3 [← one_smul ℝ z]
    rwa [← sub_smul,
      norm_smul_of_nonneg (sub_nonneg_of_le <| (one_le_inv₀ (hδ'.trans_le hδz)).2 hz),
      sub_mul, inv_mul_cancel₀ (hδ'.trans_le hδz).ne', one_mul, sub_le_comm]
  set x' := ‖x‖⁻¹ • x
  set y' := ‖y‖⁻¹ • y
  have hxy' : ε / 3 ≤ ‖x' - y'‖ :=
    calc
      ε / 3 = ε - (ε / 3 + ε / 3) := by ring
      _ ≤ ‖x - y‖ - (‖x' - x‖ + ‖y' - y‖) := by
        gcongr
        · exact (h₂ _ hx hx'.le).trans <| min_le_of_right_le <| min_le_left _ _
        · exact (h₂ _ hy hy'.le).trans <| min_le_of_right_le <| min_le_left _ _
      _ ≤ _ := by
        have : ∀ x' y', x - y = x' - y' + (x - x') + (y' - y) := fun _ _ => by abel
        rw [sub_le_iff_le_add, norm_sub_rev _ x, ← add_assoc, this]
        exact norm_add₃_le
  calc
    ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖ := by
      have : ∀ x' y', x + y = x' + y' + (x - x') + (y - y') := fun _ _ => by abel
      rw [norm_sub_rev, norm_sub_rev y', this]
      exact norm_add₃_le
    _ ≤ 2 - δ + δ' + δ' := by
      gcongr
      exacts [h (h₁ _ hx') (h₁ _ hy') hxy', h₂ _ hx hx'.le, h₂ _ hy hy'.le]
    _ ≤ 2 - δ' := by
      suffices δ' ≤ δ / 3 by linarith
      exact min_le_of_right_le <| min_le_right _ _

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
f : α → β
inst✝ : DecidablePred fun x ↦ f x ≤ 0
s : Finset α
h0 : Even #({x ∈ s | f x ≤ 0})
⊢ ∏ x ∈ s, (if f x ≤ 0 then -1 else 1) * f x = ∏ x ∈ s, f x

Tactic:
Finset.prod_mul_distrib,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
f : α → β
inst✝ : DecidablePred fun x ↦ f x ≤ 0
s : Finset α
h0 : Even #({x ∈ s | f x ≤ 0})
⊢ (∏ x ∈ s, if f x ≤ 0 then -1 else 1) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℂ
⊢ (∃ k, x = 2 * ↑k * ↑π + 0 ∨ x = 2 * ↑k * ↑π - 0) ↔ ∃ k, ↑k * (2 * ↑π) = x

Tactic:
simp [mul_assoc, mul_left_comm, eq_comm]

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
⊢ ∃ b ∈ Ioo w y, deriv f b < (f y - f w) / (y - w)

Tactic:
apply StrictMonoOn.exists_deriv_lt_slope_aux _ hwy _ _
      · refine hf.mono (Icc_subset_Icc hxw.le le_rfl)
      · exact hf'_mono.mono (Ioo_subset_Ioo hxw.le le_rfl)
      · intro z hz
        rw [← hw]
        apply ne_of_gt
        exact hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hz.1, hz.2⟩ hz.1

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

Goal state before:
pp: x : ℂ
⊢ ContinuousAt tan x ↔ cos x ≠ 0

Tactic:
refine ⟨fun hc h₀ => ?_, fun h => (hasDerivAt_tan h).continuousAt⟩

Goal state after:
x : ℂ
hc : ContinuousAt tan x
h₀ : cos x = 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

Goal state before:
pp: x : ℝ
⊢ ContinuousAt tan x ↔ cos x ≠ 0

Tactic:
refine ⟨fun hc h₀ => ?_, fun h => (hasDerivAt_tan h).continuousAt⟩

Goal state after:
x : ℝ
hc : ContinuousAt tan x
h₀ : cos x = 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a : ℝ
h : ∀ (k : ℤ), a ≠ ↑k * (2 * π)
b : ℝ
⊢ ∑ i ∈ range n, cos (a * ↑i + b) = sin (↑n * a / 2) * cos ((↑n - 1) * a / 2 + b) / sin (a / 2)

Tactic:
have h := Complex.sum_cos n (a := a) (by exact_mod_cast h) b

Goal state after:
n : ℕ
a : ℝ
h✝ : ∀ (k : ℤ), a ≠ ↑k * (2 * π)
b : ℝ
h :
  ∑ i ∈ range n, Complex.cos (↑a * ↑i + ↑b) =
    Complex.sin (↑n * ↑a / 2) * Complex.cos ((↑n - 1) * ↑a / 2 + ↑b) / Complex.sin (↑a / 2)
⊢ ∑ i ∈ range n, cos (a * ↑i + b) = sin (↑n * a / 2) * cos ((↑n - 1) * a / 2 + b) / sin (a / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ arcsin x = arcsin (x / √((1 - x ^ 2) * ((1 - x ^ 2 + x ^ 2) / (1 - x ^ 2))))

pp: case hx
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2

pp: x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0

pp: x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2

Tactic:
mul_div_cancel₀

Goal state after:
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ arcsin x = arcsin (x / √(1 - x ^ 2 + x ^ 2))

case hb
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0

case hx
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2

x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0

x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : x < y
hys : y ∈ s
y' : 𝕜
x✝ : y' ∈ slope f x '' {y | y ∈ s ∧ y < x}
z : 𝕜
hz : z ∈ {y | y ∈ s ∧ y < x}
hz' : slope f x z = y'
⊢ slope f x z ≤ slope f x y

Tactic:
refine hfc.slope_mono (interior_subset hxs) ?_ ?_ (hz.2.trans hyx).le

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : x < y
hys : y ∈ s
y' : 𝕜
x✝ : y' ∈ slope f x '' {y | y ∈ s ∧ y < x}
z : 𝕜
hz : z ∈ {y | y ∈ s ∧ y < x}
hz' : slope f x z = y'
⊢ z ∈ s \ {x}

case refine_2
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : x < y
hys : y ∈ s
y' : 𝕜
x✝ : y' ∈ slope f x '' {y | y ∈ s ∧ y < x}
z : 𝕜
hz : z ∈ {y | y ∈ s ∧ y < x}
hz' : slope f x z = y'
⊢ y ∈ s \ {x}
Module: Mathlib.Analysis.Complex.Arg

Goal state before:
pp: x y : ℂ
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
x y : ℂ
hx : x = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

case neg
x y : ℂ
hx : ¬x = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ arccos (⟪-x, -y⟫ / (‖-x‖ * ‖-y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))

Tactic:
rw [inner_neg_neg, norm_neg, norm_neg]

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

Goal state before:
pp: M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
⊢ ‖2 * ↑M * w / (1 + w)‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)

Tactic:
simp only [norm_div, norm_mul, norm_ofNat, norm_real, Real.norm_eq_abs, abs_of_pos hM]

Goal state after:
M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
⊢ 2 * M * ‖w‖ / ‖1 + w‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : slope f x y < slope f u y
⊢ slope f x y < f'

Tactic:
exact this.trans_le <| hfc.convexOn.slope_le_of_hasDerivWithinAt_Iio hu hy huy hf'

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

Goal state before:
pp: f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := f z / (2 * ↑M - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * ↑M - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * ↑M - f z ≠ 0
⊢ ‖2 * ↑M * w / (1 + w)‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)

Tactic:
simp only [norm_div, norm_mul, norm_ofNat, norm_real, Real.norm_eq_abs, abs_of_pos hM]

Goal state after:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := f z / (2 * ↑M - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * ↑M - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * ↑M - f z ≠ 0
⊢ 2 * M * ‖w‖ / ‖1 + w‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle (NormedSpace.normalize x) y = angle x y

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x = 0
⊢ angle (NormedSpace.normalize x) y = angle x y

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ¬x = 0
⊢ angle (NormedSpace.normalize x) y = angle x y
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope (⇑e ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
w : ℂ
⊢ dslope (⇑e ∘ f) c w = (⇑e ∘ dslope f c) w

Tactic:
rw [e.dslope_comp, Function.comp_apply]

Goal state after:
case H
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope (⇑e ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
w : ℂ
⊢ c = w → DifferentiableAt ℂ f 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 : 𝕜
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = ↑n
hn : n < 0
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

Tactic:
right

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = ↑n
hn : n < 0
⊢ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : ¬meromorphicOrderAt f₁ z = ⊤
h₂ : ¬meromorphicOrderAt f₂ z = ⊤
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀

Tactic:
rw [← WithTop.untop₀_min h₁ h₂]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : ¬meromorphicOrderAt f₁ z = ⊤
h₂ : ¬meromorphicOrderAt f₂ z = ⊤
⊢ (min (meromorphicOrderAt f₁ z) (meromorphicOrderAt f₂ z)).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
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

Goal state after:
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 = ⊤
⊢ ∃ n g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mpr.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x < 0
h₃ : f x = 0
⊢ MeromorphicNFAt f x

Tactic:
right

Goal state after:
case mpr.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x < 0
h₃ : f x = 0
⊢ ∃ n g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case inr
𝕜 : 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
⊢ MeromorphicNFAt (g • f) x

Tactic:
right

Goal state after:
case inr
𝕜 : 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
⊢ ∃ n g_1, AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ g • f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g_1
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case neg.inr
𝕜 : 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
⊢ MeromorphicNFAt (f ^ n) x

Tactic:
right

Goal state after:
case neg.inr
𝕜 : 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
⊢ ∃ n_1 g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f ^ n =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n_1 • g
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
n : ℤ
g : 𝕜 → 𝕜
h₁ : AnalyticAt 𝕜 g x
h₂ : g x ≠ 0
h₃ : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
⊢ MeromorphicNFAt f⁻¹ x

Tactic:
right

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
n : ℤ
g : 𝕜 → 𝕜
h₁ : AnalyticAt 𝕜 g x
h₂ : g x ≠ 0
h₃ : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
⊢ ∃ n g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f⁻¹ =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
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 : meromorphicOrderAt f x ≠ 0
⊢ MeromorphicAt f x

Tactic:
contrapose hf
  simp [hf]

Goal state after:
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 : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ↑n = meromorphicOrderAt f x
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ MeromorphicNFAt (toMeromorphicNFAt f x) x

Tactic:
right

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ↑n = meromorphicOrderAt f x
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ ∃ n g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ toMeromorphicNFAt f x =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
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
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x

Tactic:
lift meromorphicOrderAt f₂ x to ℤ using h₁f₂ with n₂ hn₂

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
h : meromorphicOrderAt f₁ x < ↑n₂
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

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

Tactic:
have : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x := by
      intro τ hτ
      apply h τ (Finset.mem_insert_of_mem hτ)
    rw [Finset.prod_insert hσ, Finset.prod_insert hσ,
      (h σ (Finset.mem_insert_self σ s₁)).meromorphicTrailingCoeffAt_mul
      (MeromorphicAt.prod this), hind this]

Goal state after: