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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ x - x ^ 3 / 6 ≤ sin x

Tactic:
obtain rfl | hx := hx.eq_or_lt

Goal state after:
case inl
hx : 0 ≤ 0
⊢ 0 - 0 ^ 3 / 6 ≤ sin 0

case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x - x ^ 3 / 6 ≤ sin x
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'
⊢ y' ∈ Iic (slope f x y)

Tactic:
simp_rw [mem_Iic, ← hz']

Goal state after:
𝕜 : 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
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
hxs' : ∃ l u, x ∈ Ioo l u ∧ Ioo l u ⊆ S
⊢ HasDerivWithinAt f (sInf (slope f x '' {y | y ∈ S ∧ x < y})) (Ioi x) x

Tactic:
obtain ⟨a, b, hxab, habs⟩ := hxs'

Goal state after:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ HasDerivWithinAt f (sInf (slope f x '' {y | y ∈ S ∧ x < y})) (Ioi x) x
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
hxs' : ∃ l u, x ∈ Ioo l u ∧ Ioo l u ⊆ S
⊢ HasDerivWithinAt f (sSup (slope f x '' {y | y ∈ S ∧ y < x})) (Iio x) x

Tactic:
obtain ⟨a, b, hxab, habs⟩ := hxs'

Goal state after:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ HasDerivWithinAt f (sSup (slope f x '' {y | y ∈ S ∧ y < x})) (Iio x) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h : 1 < x
⊢ 2 * arctan x = arctan (2 * x / (1 - x ^ 2)) + π

Tactic:
rw [two_mul, arctan_add_eq_add_pi (by nlinarith) (by linarith)]; congr 2; ring

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

Goal state before:
pp: case inr.refine_1
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
hxs' : ∃ l u, x ∈ Ioo l u ∧ Ioo l u ⊆ S
⊢ (slope f x '' {y | y ∈ S ∧ y < x}).Nonempty

Tactic:
obtain ⟨a, b, hxab, habs⟩ := hxs'

Goal state after:
case inr.refine_1
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ (slope f x '' {y | y ∈ S ∧ y < x}).Nonempty
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ inner ℝ x y / (‖x‖ * ‖y‖) = Real.cos |(x / y).arg|

Tactic:
rw [Real.cos_abs, Complex.cos_arg (div_ne_zero hx hy)]

Goal state after:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ inner ℝ x y / (‖x‖ * ‖y‖) = (x / y).re / ‖x / y‖
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: a : ℂ
ha : a ≠ 0
x y : ℂ
⊢ angle (a * x) (a * y) = angle x y

Tactic:
obtain rfl | hx := eq_or_ne x 0 <;> obtain rfl | hy := eq_or_ne y 0

Goal state after:
case inl.inl
a : ℂ
ha : a ≠ 0
⊢ angle (a * 0) (a * 0) = angle 0 0

case inl.inr
a : ℂ
ha : a ≠ 0
y : ℂ
hy : y ≠ 0
⊢ angle (a * 0) (a * y) = angle 0 y

case inr.inl
a : ℂ
ha : a ≠ 0
x : ℂ
hx : x ≠ 0
⊢ angle (a * x) (a * 0) = angle x 0

case inr.inr
a : ℂ
ha : a ≠ 0
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ angle (a * x) (a * y) = angle x y
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
hxs' : ∃ l u, x ∈ Ioo l u ∧ Ioo l u ⊆ S
⊢ derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x

Tactic:
obtain ⟨a, b, hxab, habs⟩ := hxs'

Goal state after:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ ‖cos ↑θ - 1 + sin ↑θ * I‖ ∈ Icc (2 / π * |toIocMod Real.two_pi_pos (-π) θ|) |toIocMod Real.two_pi_pos (-π) θ|

Tactic:
(toIocMod_eq_self _).2

Goal state after:
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ ‖cos ↑θ - 1 + sin ↑θ * I‖ ∈ Icc (2 / π * |θ|) |θ|

x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ θ ∈ Ioc (-π) (-π + 2 * π)
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
⊢ IsCoveringMap fun x ↦ ⟨↑x ^ n, ⋯⟩

Tactic:
obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg

Goal state after:
case inl
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑↑n ≠ 0
⊢ IsCoveringMap fun x ↦ ⟨↑x ^ ↑n, ⋯⟩

case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
⊢ IsCoveringMap fun x ↦ ⟨↑x ^ (-↑n), ⋯⟩
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
⊢ IsQuotientCoveringMap (fun x ↦ x ^ n) ↥(zpowGroupHom n).ker

Tactic:
obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg

Goal state after:
case inl
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ ↑n
⊢ IsQuotientCoveringMap (fun x ↦ x ^ ↑n) ↥(zpowGroupHom ↑n).ker

case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
⊢ IsQuotientCoveringMap (fun x ↦ x ^ (-↑n)) ↥(zpowGroupHom (-↑n)).ker
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝔻
⊢ ‖↑z‖ ≠ ‖-1‖

Tactic:
simpa [norm_neg] using z.norm_ne_one

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

Goal state before:
pp: z : 𝕔𝔻
⊢ ‖↑z‖ ^ 2 ≤ 1

Tactic:
rw [sq_le_one_iff_abs_le_one, abs_norm]
  exact z.norm_le_one

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

Goal state before:
pp: case refine_2.refine_6
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
⊢ (p ∘ fun ta ↦ if ta.1 ≤ t n then g' ta else if f ta ∈ (q e).target then ↑(q e).symm (f ta) else g ta) ta = f ta

Tactic:
rw [Function.comp_apply]

Goal state after:
case refine_2.refine_6
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
⊢ p (if ta.1 ≤ t n then g' ta else if f ta ∈ (q e).target then ↑(q e).symm (f ta) else g ta) = f ta
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 : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)

Tactic:
cases h'o : meromorphicOrderAt f x with
  | top =>
    apply tendsto_const_nhds.congr'
    filter_upwards [meromorphicOrderAt_eq_top_iff.1 h'o] with y hy using hy.symm
  | coe n =>
    rcases (meromorphicOrderAt_eq_int_iff hf).1 h'o with ⟨g, g_an, gx, hg⟩
    lift n to ℕ using by simpa [h'o] using ho.le
    have : (0 : E) = (x - x) ^ n • g x := by
      have : 0 < n := by simpa [h'o] using ho
      simp [zero_pow_eq_zero.2 this.ne']
    rw [this]
    have : ContinuousAt (fun z ↦ (z - x) ^ n • g z) x := by fun_prop
    apply this.continuousWithinAt.tendsto.congr'
    filter_upwards [hg] with y hy using by simp [hy]

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

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
h : HasFiniteSupport d
x : 𝕜
⊢ (Function.mulSupport fun u ↦ (x - u) ^ d u) ⊆ ↑(Finite.toFinset h)

pp: case h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
h : HasFiniteSupport d
x : 𝕜
⊢ (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset h)

Tactic:
· intro u
    contrapose
    simp_all

Goal state after:
case h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
h : HasFiniteSupport d
x : 𝕜
⊢ (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset h)
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 : 𝕜
hz : z ∈ Finite.toFinset h₁
⊢ ¬(x - z) ^ d z = 0

Tactic:
by_cases h₂ : x = z

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₁
h₂ : x = z
⊢ ¬(x - z) ^ d z = 0

case neg
𝕜 : 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₁
h₂ : ¬x = z
⊢ ¬(x - z) ^ d z = 0
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
x✝ : WithTop ℤ
h₁f₁ : meromorphicOrderAt f₁ x = x✝
⊢ meromorphicOrderAt f₂ x = x✝

Tactic:
cases h₁f₁ : meromorphicOrderAt f₁ x with

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

Goal state before:
pp: case top
𝕜 : 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
ho : meromorphicOrderAt f x = ⊤
this : AnalyticAt 𝕜 (fun x ↦ 0) x
⊢ (fun x ↦ 0) =ᶠ[𝓝 x] f

Tactic:
← ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE continuousAt_const h'

Goal state after:
case top
𝕜 : 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
ho : meromorphicOrderAt f x = ⊤
this : AnalyticAt 𝕜 (fun x ↦ 0) x
⊢ (fun x ↦ 0) =ᶠ[𝓝[≠] x] f
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
⊢ meromorphicOrderAt (canonicalFactor R w) z ≠ ⊤

Tactic:
apply (meromorphic_canonicalFactor R w).exists_meromorphicOrderAt_ne_top_iff_forall.1
  use 0
  by_cases hw : w = 0
  · simp_all [meromorphicOrderAt_canonicalFactor (mem_ball_self hR)]
  suffices meromorphicOrderAt (canonicalFactor R w) 0 = 0 by simp_all
  rw [MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff]
  · simp_all [canonicalFactor, ne_of_gt hR]
  · apply AnalyticAt.meromorphicNFAt
    apply analyticOnNhd_canonicalFactor
    grind

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

Goal state before:
pp: case empty
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
ι : Type u_5
f : ι → 𝕜 → 𝕜'
hf : ∀ i ∈ ∅, MeromorphicAt (f i) x
⊢ meromorphicOrderAt 1 x = ↑0

Tactic:
meromorphicOrderAt_eq_int_iff

Goal state after:
case empty
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
ι : Type u_5
f : ι → 𝕜 → 𝕜'
hf : ∀ i ∈ ∅, MeromorphicAt (f i) x
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = (z - x) ^ 0 • g z

case empty
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
ι : Type u_5
f : ι → 𝕜 → 𝕜'
hf : ∀ i ∈ ∅, MeromorphicAt (f i) x
⊢ MeromorphicAt 1 x
Module: Mathlib.Analysis.Meromorphic.Order

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

Tactic:
rw [Finset.prod_empty, Finset.sum_empty, ← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]

Goal state after:
case empty
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
ι : Type u_5
f : ι → 𝕜 → 𝕜'
hf : ∀ i ∈ ∅, MeromorphicAt (f i) x
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = (z - x) ^ 0 • g z

case empty
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
ι : Type u_5
f : ι → 𝕜 → 𝕜'
hf : ∀ i ∈ ∅, MeromorphicAt (f i) x
⊢ MeromorphicAt 1 x
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
⊢ ∃ g,
    AnalyticOnNhd 𝕜 g U ∧
      (∀ (u : ↑U), g ↑u ≠ 0) ∧ f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u) • g

Tactic:
let φ := ∏ᶠ u, (· - u) ^ (divisor f U u)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
⊢ meromorphicOrderAt 1 x = ↑0

Tactic:
meromorphicOrderAt_eq_int_iff

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = (z - x) ^ 0 • g z

𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
⊢ MeromorphicAt 1 x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ meromorphicOrderAt 1 x = ↑0

Tactic:
meromorphicOrderAt_eq_int_iff

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = (z - x) ^ 0 • g z

case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ MeromorphicAt 1 x
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
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
ex : ∀ (γ : C(↑I, A)), γ 0 = a₀ → ∃ Γ, Γ 0 = e₀ ∧ p ∘ ⇑Γ = ⇑(f.comp γ)
uniq :
  ∀ (γ γ' : C(↑I, A)) (Γ Γ' : C(↑I, E)),
    γ 0 = a₀ →
      γ' 0 = a₀ → Γ 0 = e₀ → Γ' 0 = e₀ → p ∘ ⇑Γ = ⇑(f.comp γ) → p ∘ ⇑Γ' = ⇑(f.comp γ') → γ 1 = γ' 1 → Γ 1 = Γ' 1
⊢ ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f

Tactic:
choose Γ Γ_0 Γ_lifts using ex

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
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
uniq :
  ∀ (γ γ' : C(↑I, A)) (Γ Γ' : C(↑I, E)),
    γ 0 = a₀ →
      γ' 0 = a₀ → Γ 0 = e₀ → Γ' 0 = e₀ → p ∘ ⇑Γ = ⇑(f.comp γ) → p ∘ ⇑Γ' = ⇑(f.comp γ') → γ 1 = γ' 1 → Γ 1 = Γ' 1
Γ : (γ : C(↑I, A)) → γ 0 = a₀ → C(↑I, E)
Γ_0 : ∀ (γ : C(↑I, A)) (a : γ 0 = a₀), (Γ γ a) 0 = e₀
Γ_lifts : ∀ (γ : C(↑I, A)) (a : γ 0 = a₀), p ∘ ⇑(Γ γ a) = ⇑(f.comp γ)
⊢ ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
hn : ¬IsEmpty n
⊢ toGL g ∈ Subgroup.center (GL n R) ↔ g ∈ Subgroup.center (SpecialLinearGroup n R)

Tactic:
else

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
hn : ¬IsEmpty n
⊢ toGL g ∈ Subgroup.center (GL n R) ↔ g ∈ Subgroup.center (SpecialLinearGroup n R)
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
⊢ (li.toLinearIsometryEquiv ⋯).toLinearIsometry = li

Tactic:
ext1; rfl

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

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 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
⊢ (∃ u, meromorphicOrderAt f ↑u ≠ ⊤) → ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤

Tactic:
intro h₂f
    have := isPreconnected_iff_preconnectedSpace.1 hU.isPreconnected
    rcases isClopen_iff.1 hf.isClopen_setOfPred_meromorphicOrderAt_eq_top with h | h
    · intro u
      have : u ∉ (∅ : Set U) := by exact fun a => a
      rw [← h] at this
      tauto
    · obtain ⟨u, hU⟩ := h₂f
      have : u ∈ univ := by trivial
      rw [← h] at this
      tauto

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

Goal state before:
pp: case succ.refine_4
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
this : Nonempty ↑(p ⁻¹' {x})
q : Bundle.Trivialization (↑(p ⁻¹' {x})) p := ⋯.toTrivialization
s : ↑I
hs : s ∈ Set.Icc 0 (t (n + 1))
⊢ (p ∘ fun s ↦ if s ≤ t n then Γ s else q.invFun (γ s, (↑q (Γ (t n))).2)) s = γ s

Tactic:
rw [Function.comp_apply]

Goal state after:
case succ.refine_4
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
this : Nonempty ↑(p ⁻¹' {x})
q : Bundle.Trivialization (↑(p ⁻¹' {x})) p := ⋯.toTrivialization
s : ↑I
hs : s ∈ Set.Icc 0 (t (n + 1))
⊢ p (if s ≤ t n then Γ s else q.invFun (γ s, (↑q (Γ (t n))).2)) = γ s
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 : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
⊢ ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, AnalyticAt 𝕜 f y

Tactic:
by
  /- At neighboring points in `U`, the function `f` is both meromorphic (by meromorphicity on `U`)
  and continuous (thanks to the formula for a meromorphic function around the point `x`), so it is
  analytic. -/
  have : ∀ᶠ y in 𝓝[U \ {x}] x, ContinuousAt f y := by
    have : U \ {x} ⊆ {x}ᶜ := by simp
    exact nhdsWithin_mono _ this (h x hx).eventually_continuousAt
  filter_upwards [this, self_mem_nhdsWithin] with y hy h'y
  exact (h y h'y.1).analyticAt hy

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ B, f =O[l] fun z ↦ expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ B, g =O[l] fun z ↦ expR (B * expR (c * |u z|))
c₁✝ c₂✝ B₁✝ B₂✝ : ℝ
hc : c₁✝ ≤ c₂✝
hB₀ : 0 ≤ B₂✝
hB : B₁✝ ≤ B₂✝
z : ℂ
⊢ ‖expR (B₁✝ * expR (c₁✝ * |u z|))‖ ≤ ‖expR (B₂✝ * expR (c₂✝ * |u z|))‖

Tactic:
simp only [Real.norm_eq_abs, Real.abs_exp]; gcongr

Goal state after: