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

Goal state before:
pp: case inr
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
hy1' : π / 2 ≤ y
⊢ cos y < 1 / √(y ^ 2 + 1)

Tactic:
refine lt_of_le_of_lt ?_ (one_div_pos.mpr <| sqrt_pos_of_pos hy3)
    exact cos_nonpos_of_pi_div_two_le_of_le hy1' (by linarith [pi_pos])

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

Goal state before:
pp: case refine_2.refine_1
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z✝ : ℝ
hzs : z✝ ∈ S
hzx : z✝ < x
z : ℝ
hxz : x < z
hzb : z < b
⊢ {y | y ∈ S ∧ x < y}.Nonempty

Tactic:
exact ⟨z, habs ⟨hxab.1.trans hxz, hzb⟩, hxz⟩

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

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

Tactic:
norm_cast

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

Goal state before:
pp: case h
M : ℝ
z w : ℂ
x✝¹ : M ≠ 0
x✝ : 2 * ↑M - z ≠ 0
h : w = z / (2 * ↑M - z)
⊢ ↑M ≠ 0

Tactic:
norm_cast

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

Goal state before:
pp: f : ℂ → ℂ
c z : ℂ
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₁
this✝ :
  ∀ {R₁ : ℝ},
    DifferentiableOn ℂ f (ball c R₁) →
      MapsTo f (ball c R₁) (closedBall (f c) R₂) →
        z ∈ ball c R₁ →
          0 < R₁ →
            DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂) →
              ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
this : ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
⊢ Tendsto (fun c_1 ↦ R₂ * (‖z - c‖ / c_1) ^ (n + 1)) (𝓝[<] R₁) (𝓝 (R₂ * (‖z - c‖ / R₁) ^ (n + 1)))

Tactic:
refine ContinuousAt.continuousWithinAt ?_

Goal state after:
f : ℂ → ℂ
c z : ℂ
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₁
this✝ :
  ∀ {R₁ : ℝ},
    DifferentiableOn ℂ f (ball c R₁) →
      MapsTo f (ball c R₁) (closedBall (f c) R₂) →
        z ∈ ball c R₁ →
          0 < R₁ →
            DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂) →
              ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
this : ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
⊢ ContinuousAt (fun c_1 ↦ R₂ * (‖z - c‖ / c_1) ^ (n + 1)) R₁
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
p : 𝕜[X]
x : 𝕜
hx : x ∈ ((fun x ↦ eval x p) '' {k | eval k (derivative p) = 0})ᶜ
ne : p ≠ C x
⊢ ((fun x ↦ eval x p) ⁻¹' {x}).Finite

Tactic:
· simpa only [preimage_eval_singleton ne] using rootSet_finite ..

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ IsCoveringMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)

Tactic:
convert! (isCoveringMap_zpow n hn).comp_homeomorph (.setCongr _) using 1
    ext; simpa using! (this _).not

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Action

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜' E
r : ℝ
c : ↑(closedBall 0 1)
x : ↑(ball 0 r)
⊢ ‖↑c • ↑x‖ < r

Tactic:
simpa only [norm_smul, one_mul] using
          mul_lt_mul' (mem_closedBall_zero_iff.1 c.2) (mem_ball_zero_iff.1 x.2) (norm_nonneg _)
            one_pos

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ ∃ t, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ U ⊆ t ∧ ∀ x ∈ t, f =ᶠ[𝓝[≠] x] g

Tactic:
use {x | f =ᶠ[𝓝[≠] x] g}

Goal state after:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | f =ᶠ[𝓝[≠] x] g} ∧
    U ⊆ {x | f =ᶠ[𝓝[≠] x] g} ∧ ∀ x ∈ {x | f =ᶠ[𝓝[≠] x] g}, f =ᶠ[𝓝[≠] x] g
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h₂f : AnalyticAt 𝕜 f x
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
rw [h₂f.meromorphicOrderAt_eq]
    simp

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

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
⊢ meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
simp only [hf, not_false_eq_true, meromorphicOrderAt_of_not_meromorphicAt, WithTop.zero_ne_top,
      false_iff]
    contrapose hf
    exact (MeromorphicAt.const 0 x).congr (EventuallyEq.symm 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
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
h₁f : MeromorphicOn f U
z : 𝕜
hz : z ∉ U
⊢ E

Tactic:
exact f z

Goal state after:
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
hf₂ : MeromorphicAt f₂ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : f₁ =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f₁ x).untop₀ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : f₂ =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f₂ x).untop₀ • g₂ z
this : f₁ • f₂ =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt (f₁ • f₂) x).untop₀ • (g₁ • g₂) z
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = g₁ x • g₂ x

Tactic:
(h₁g₁.smul h₁g₂).meromorphicTrailingCoeffAt_of_eq_nhdsNE this

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
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : f₁ =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f₁ x).untop₀ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : f₂ =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f₂ x).untop₀ • g₂ z
this : f₁ • f₂ =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt (f₁ • f₂) x).untop₀ • (g₁ • g₂) z
⊢ (g₁ • g₂) x = g₁ x • g₂ x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
⊢ meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹

Tactic:
rw [← mul_eq_one_iff_eq_inv₀ (h₁.meromorphicTrailingCoeffAt_ne_zero h₂),
      ← h₁.inv.meromorphicTrailingCoeffAt_mul h₁, meromorphicTrailingCoeffAt_congr_nhdsNE this,
      analyticAt_const.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n := 0)]

Goal state after:
case neg.h₂g
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
⊢ 1 ≠ 0

case neg.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
⊢ 1 =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ 0 • 1
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inr.inl
𝕜 : 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
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x = 0
⊢ False

Tactic:
obtain ⟨c, c_ne, h'c⟩ := tendsto_ne_zero_of_meromorphicOrderAt_eq_zero hf ho

Goal state after:
case inr.inl
𝕜 : 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
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x = 0
c : E
c_ne : c ≠ 0
h'c : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ False
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case coe.coe
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁶ : NormedRing R
inst✝⁵ : NoZeroDivisors R
inst✝⁴ : Module R E
inst✝³ : IsBoundedSMul R E
inst✝² : Module.IsTorsionFree R E
x : 𝕜
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : IsScalarTower 𝕜 R E
f : 𝕜 → R
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : meromorphicOrderAt f x = ↑m
n : ℤ
h₂g : meromorphicOrderAt g x = ↑n
F : 𝕜 → R
h₁F : AnalyticAt 𝕜 F x
h₂F : F x ≠ 0
h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z
G : 𝕜 → E
h₁G : AnalyticAt 𝕜 G x
h₂G : G x ≠ 0
h₃G : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = (z - x) ^ n • G z
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z

Tactic:
use F • G, h₁F.smul h₁G, by simp [h₂F, h₂G]

Goal state after:
case right
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁶ : NormedRing R
inst✝⁵ : NoZeroDivisors R
inst✝⁴ : Module R E
inst✝³ : IsBoundedSMul R E
inst✝² : Module.IsTorsionFree R E
x : 𝕜
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : IsScalarTower 𝕜 R E
f : 𝕜 → R
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : meromorphicOrderAt f x = ↑m
n : ℤ
h₂g : meromorphicOrderAt g x = ↑n
F : 𝕜 → R
h₁F : AnalyticAt 𝕜 F x
h₂F : F x ≠ 0
h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z
G : 𝕜 → E
h₁G : AnalyticAt 𝕜 G x
h₂G : G x ≠ 0
h₃G : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = (z - x) ^ n • G z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • (F • G) z
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
a✝ : ℤ
⊢ ↑n * ↑a✝ + ↑a✝ = (↑n + 1) * ↑a✝

Tactic:
norm_cast

Goal state after:
case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
a✝ : ℤ
⊢ ↑n * a✝ + a✝ = ↑(n + 1) * a✝
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
n : ℤ
⊢ meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x

Tactic:
by
  -- Trivial case: n = 0
  by_cases hn : n = 0
  · simp only [hn, zpow_zero, WithTop.coe_zero, zero_mul]
    rw [← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]
    · exact ⟨1, analyticAt_const, by simp⟩
    · apply MeromorphicAt.const
  -- Trivial case: f locally zero
  by_cases h : meromorphicOrderAt f x = ⊤
  · simp only [h, ne_eq, WithTop.coe_eq_zero, hn, not_false_eq_true, WithTop.mul_top]
    rw [meromorphicOrderAt_eq_top_iff] at *
    filter_upwards [h]
    intro y hy
    simp [hy, zero_zpow n hn]
  -- General case
  obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff hf).1 h
  rw [← WithTop.coe_untop₀_of_ne_top h, ← WithTop.coe_mul,
    meromorphicOrderAt_eq_int_iff (hf.zpow n)]
  use g ^ n, h₁g.zpow h₂g
  constructor
  · simp_all [zpow_eq_zero_iff hn]
  · filter_upwards [h₃g]
    intro y hy
    rw [Pi.pow_apply, hy, Algebra.smul_def, Algebra.smul_def, mul_zpow, ← map_zpow₀]
    congr 1
    rw [mul_comm, zpow_mul]

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

Goal state before:
pp: case neg
𝕜 : 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 : MeromorphicAt f₁ x → MeromorphicAt f₂ x → min ↑n₁ ↑n₂ ≤ meromorphicOrderAt (f₁ + 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
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 : ℤ := min n₁ n₂
g : 𝕜 → E := (fun z ↦ (z - x) ^ (n₁ - n)) • g₁ + (fun z ↦ (z - x) ^ (n₂ - n)) • g₂
h₁g : AnalyticAt 𝕜 g x
this : f₁ + f₂ =ᶠ[𝓝[≠] x] (fun x_1 ↦ x_1 - x) ^ n • g
t₀ : MeromorphicAt ((fun x_1 ↦ x_1 - x) ^ n) x
t₁ : meromorphicOrderAt ((fun x_1 ↦ x_1 - x) ^ n) x = ↑n
⊢ min ↑n₁ ↑n₂ ≤ ↑n + meromorphicOrderAt g x

Tactic:
exact le_add_of_nonneg_right h₁g.meromorphicOrderAt_nonneg

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

Goal state before:
pp: case refine_1
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = I
⊢ ∀ (i : Fin 2), f.toLinearEquiv (basisOneI i) = (LinearIsometryEquiv.refl ℝ ℂ).toLinearEquiv (basisOneI i)

Tactic:
intro i

Goal state after:
case refine_1
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = I
i : Fin 2
⊢ f.toLinearEquiv (basisOneI i) = (LinearIsometryEquiv.refl ℝ ℂ).toLinearEquiv (basisOneI i)
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: case refine_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = -I
⊢ ∀ (i : Fin 2), f.toLinearEquiv (basisOneI i) = conjLIE.toLinearEquiv (basisOneI i)

Tactic:
intro i

Goal state after:
case refine_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = -I
i : Fin 2
⊢ f.toLinearEquiv (basisOneI i) = conjLIE.toLinearEquiv (basisOneI i)
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case inr
c : ℝ
a : Circle
⊢ (∃ map, restrictScalars ℝ map = c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap) ∨
    ∃ map,
      restrictScalars ℝ map = (c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap) ∘SL ↑conjCLE

Tactic:
refine Or.inr ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, ?_⟩

Goal state after:
case inr
c : ℝ
a : Circle
⊢ restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ) =
    (c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap) ∘SL ↑conjCLE
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ ↑1 = ?m.49

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑2 = ?m.59

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑3 = ?m.69

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑4 = ?m.79

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑5 = ?m.89

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑6 = ?m.99

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑7 = ?m.109

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑8 = ?m.119

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑9 = ?m.129

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑10 = ?m.139

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑11 = ?m.149

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑12 = ?m.159

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑13 = ?m.169

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑14 = ?m.180

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑14 = ?m.179

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑15 = ?m.189

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑16 = ?m.199

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑17 = ?m.209

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑18 = ?m.219

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑19 = ?m.229

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑20 = ?m.239

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑21 = ?m.249

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ ↑22 = ?m.260

Tactic:
norm_cast

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ₀ γ₁ : C(↑I, X)
h : γ₀.HomotopicRel γ₁ {0, 1}
e : E
h₀ : γ₀ 0 = p e
h₁ : γ₁ 0 = p e
⊢ (cov.liftPath γ₀ e h₀) 1 = (cov.liftPath γ₁ e h₁) 1

Tactic:
have := (cov.homotopicRel_liftPath h e h₀ h₁).some

Goal state after:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ₀ γ₁ : C(↑I, X)
h : γ₀.HomotopicRel γ₁ {0, 1}
e : E
h₀ : γ₀ 0 = p e
h₁ : γ₁ 0 = p e
this : (cov.liftPath γ₀ e h₀).HomotopyRel (cov.liftPath γ₁ e h₁) {0, 1}
⊢ (cov.liftPath γ₀ e h₀) 1 = (cov.liftPath γ₁ e h₁) 1
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
X✝ Y✝ Z✝ : FundamentalGroupoid X
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ↾cov.monodromy (x✝¹ ≫ x✝) = ↾cov.monodromy x✝¹ ≫ ↾cov.monodromy x✝

Tactic:
ext : 3

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
X✝ Y✝ Z✝ : FundamentalGroupoid X
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ↑(p ⁻¹' {X✝.as})
⊢ (ConcreteCategory.hom (↾cov.monodromy (x✝² ≫ x✝¹))).toFun x✝ =
    (ConcreteCategory.hom (↾cov.monodromy x✝² ≫ ↾cov.monodromy x✝¹)).toFun 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
cov : IsCoveringMap p
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
⊢ (f.comp pγ.toContinuousMap) 0 = p e₀

Tactic:
simp [he]

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
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
⊢ (f.comp pγ'.toContinuousMap) 0 = p e₀

Tactic:
simp [he]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
inst✝¹ : CompleteSpace 𝕜
f : 𝕜 → 𝕜
inst✝ : CharZero 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ↑n = meromorphicOrderAt f x
meromorphicOrderAt_logDeriv_eq_neg_one :
  ∀ [CharZero 𝕜], MeromorphicAt f x → ↑n ≠ 0 → ↑n ≠ ⊤ → meromorphicOrderAt (logDeriv f) x = -1
h₁ : ↑n ≠ 0
⊢ ↑(n - 1) - ↑n = -1

Tactic:
norm_cast

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
inst✝¹ : CompleteSpace 𝕜
f : 𝕜 → 𝕜
inst✝ : CharZero 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ↑n = meromorphicOrderAt f x
meromorphicOrderAt_logDeriv_eq_neg_one :
  ∀ [CharZero 𝕜], MeromorphicAt f x → ↑n ≠ 0 → ↑n ≠ ⊤ → meromorphicOrderAt (logDeriv f) x = -1
h₁ : ↑n ≠ 0
⊢ ↑(n - 1 - n) = -1
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case h.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ((z - ↑l) / (↑u - ↑l)).re = 0

Tactic:
norm_cast

Goal state after:
case h.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ((z - ↑l) / ↑(u - l)).re = 0
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ↑u - ↑l ≠ 0

Tactic:
norm_cast

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ¬u - l = 0
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case h.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ ((z - ↑l) / (↑u - ↑l)).re = 1

Tactic:
norm_cast

Goal state after:
case h.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ ((z - ↑l) / ↑(u - l)).re = 1
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ ↑u - ↑l ≠ 0

Tactic:
norm_cast

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ ¬u - l = 0