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

Goal state before:
pp: case succ.inr
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
n : ℕ
h : ∀ {f : ℝ → E}, ContDiffOn ℝ (↑n) f s → (fun x ↦ f x - taylorWithinEval f n s x₀ x) =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ n
f : ℝ → E
hs' : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n + 1) f s
x : ℝ
hx : x ∈ s
⊢ HasDerivWithinAt f (derivWithin f s x) s x

Tactic:
exact (hf.differentiableOn (by simp) _ hx).hasDerivWithinAt

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ray

Goal state before:
pp: case inl
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
h : ‖x‖ = ‖0‖
⊢ SameRay ℝ x 0 ↔ x = 0

Tactic:
rw [norm_zero, norm_eq_zero] at h
    exact iff_of_true (SameRay.zero_right _) h

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ ∫ (x : ℝ) in a..b, f x * deriv g x = ∫ (x : ℝ) in a..b, deriv f x * g x + f x * deriv g x - deriv f x * g x

pp: case hf
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ IntervalIntegrable (fun x ↦ deriv f x * g x + f x * deriv g x) volume a b

pp: case hg
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ IntervalIntegrable (fun x ↦ deriv f x * g x) volume a b

Tactic:
· simp_rw [add_sub_cancel_left]

Goal state after:
case hf
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ IntervalIntegrable (fun x ↦ deriv f x * g x + f x * deriv g x) volume a b

case hg
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ IntervalIntegrable (fun x ↦ deriv f x * g x) volume a b
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case mpr
θ : ℂ
⊢ (∃ k, θ = ↑k * ↑π) → ∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2

Tactic:
rintro ⟨k, rfl⟩

Goal state after:
case mpr
k : ℤ
⊢ ∃ k_1, ↑k * ↑π - ↑π / 2 = (2 * ↑k_1 + 1) * ↑π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case h₁.mp
x y : ℂ
⊢ (∃ k, x = ↑k * ↑π * 2 + y) → ∃ k, y = ↑k * ↑π * 2 + x

Tactic:
rintro ⟨k, rfl⟩

Goal state after:
case h₁.mp
y : ℂ
k : ℤ
⊢ ∃ k_1, y = ↑k_1 * ↑π * 2 + (↑k * ↑π * 2 + y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case h₁.mpr
x y : ℂ
⊢ (∃ k, y = ↑k * ↑π * 2 + x) → ∃ k, x = ↑k * ↑π * 2 + y

Tactic:
rintro ⟨k, rfl⟩

Goal state after:
case h₁.mpr
x : ℂ
k : ℤ
⊢ ∃ k_1, x = ↑k_1 * ↑π * 2 + (↑k * ↑π * 2 + x)
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:
rw [← 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.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ cexp (log w / I * I) ^ 2 - 2 * x * cexp (log w / I * I) + 1 = 0

Tactic:
div_mul_cancel₀ _ I_ne_zero,

Goal state after:
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ cexp (log w) ^ 2 - 2 * x * cexp (log w) + 1 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y ↦ tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ 0 < deriv (fun y' ↦ tan y' - y') y

Tactic:
simp only [deriv_tan_sub_id y this.ne', one_div, gt_iff_lt, sub_pos]

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y ↦ tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ 1 < (cos y ^ 2)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case hx₁
x y : ℝ
h : x * y < 1
⊢ -(π / 2) < arctan x + arctan y

pp: case hx₂
x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y < π / 2

Tactic:
· rw [neg_lt, neg_add, ← arctan_neg, ← arctan_neg]
    rw [← neg_mul_neg] at h
    exact arctan_add_arctan_lt_pi_div_two h

Goal state after:
case hx₂
x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y < π / 2
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
x : ℂ
hx : x ∈ ball 0 R
⊢ (f x).re - (f 0).re ≤ M - (f 0).re

Tactic:
gcongr; exact hf₁ hx

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:
rw [← 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 inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
hg : AnalyticAt 𝕜 g x
hf : f =ᶠ[𝓝 (g x)] 0
⊢ MeromorphicNFAt (f ∘ g) x

pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
hg : AnalyticAt 𝕜 g x
n : ℤ
q : 𝕜 → E
hq_an : AnalyticAt 𝕜 q (g x)
hq_ne : q (g x) ≠ 0
hf : f =ᶠ[𝓝 (g x)] (fun x_1 ↦ x_1 - g x) ^ n • q
⊢ MeromorphicNFAt (f ∘ g) x

Tactic:
· exact Or.inl (hg.continuousAt.tendsto.eventually hf)

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
hg : AnalyticAt 𝕜 g x
n : ℤ
q : 𝕜 → E
hq_an : AnalyticAt 𝕜 q (g x)
hq_ne : q (g x) ≠ 0
hf : f =ᶠ[𝓝 (g x)] (fun x_1 ↦ x_1 - g x) ^ n • q
⊢ MeromorphicNFAt (f ∘ g) x
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
⊢ MeromorphicNFAt (f ∘ fun x ↦ x + c) x ↔ MeromorphicNFAt f (x + c)

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [show f = ((f ∘ fun x ↦ x + c) ∘ fun z ↦ z - c) by aesop]
    rw [show x = (x + c) - c by ring] at h
    exact h.comp_analyticAt (g := fun z ↦ z - c) (by fun_prop)
  · exact h.comp_analyticAt (g := fun z ↦ z + c) (by fun_prop)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ EventuallyConst f (𝓝[≠] x) ↔ ∃ c, meromorphicOrderAt (fun x ↦ f x - c) x = ⊤

Tactic:
simp only [eventuallyConst_iff_exists_eventuallyEq, meromorphicOrderAt_eq_top_iff,
    sub_eq_zero, EventuallyEq]

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

Goal state before:
pp: case pos
𝕜 : 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:
apply meromorphicTrailingCoeffAt_congr_nhdsNE
    filter_upwards [meromorphicOrderAt_eq_top_iff.1 h₁f₂]
    simp

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

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho✝ : 0 ≤ meromorphicOrderAt f x
ho : 0 = meromorphicOrderAt f x
⊢ ∃ c, Tendsto f (𝓝[≠] x) (𝓝 c)

pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho✝ : 0 ≤ meromorphicOrderAt f x
ho : 0 < meromorphicOrderAt f x
⊢ ∃ c, Tendsto f (𝓝[≠] x) (𝓝 c)

Tactic:
· rcases tendsto_ne_zero_of_meromorphicOrderAt_eq_zero hf ho.symm with ⟨c, -, hc⟩
    exact ⟨c, hc⟩

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho✝ : 0 ≤ meromorphicOrderAt f x
ho : 0 < meromorphicOrderAt f x
⊢ ∃ c, Tendsto f (𝓝[≠] x) (𝓝 c)
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this✝ : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset hd)
this : u₀ ∈ Finite.toFinset hd
⊢ ∏ i ∈ Finite.toFinset hd, (fun x ↦ x - i) ^ d i =
    (fun x ↦ x - u₀) ^ d u₀ * ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ update d u₀ 0 u

Tactic:
rw [← Finset.mul_prod_erase hd.toFinset _ this]

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this✝ : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset hd)
this : u₀ ∈ Finite.toFinset hd
⊢ (fun x ↦ x - u₀) ^ d u₀ * ∏ x ∈ (Finite.toFinset hd).erase u₀, (fun x_1 ↦ x_1 - x) ^ d x =
    (fun x ↦ x - u₀) ^ d u₀ * ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ update d u₀ 0 u
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
w : ℂ
⊢ Meromorphic (canonicalFactor R w)

Tactic:
intro x
  unfold canonicalFactor
  fun_prop

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

Goal state before:
pp: case coe
𝕜 : 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
n : ℤ
ho : meromorphicOrderAt f x = ↑n
⊢ AnalyticAt 𝕜 f x

Tactic:
rcases (meromorphicOrderAt_eq_int_iff h).1 ho with ⟨g, g_an, gx, hg⟩
    have : 0 ≤ meromorphicOrderAt f x := by
      apply (tendsto_nhds_iff_meromorphicOrderAt_nonneg h).1
      exact ⟨f x, h'.continuousWithinAt.tendsto⟩
    lift n to ℕ using by simpa [ho] using this
    have A : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ n • g z = f z := by
      apply (ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop) h').1
      filter_upwards [hg] with z hz using by simpa using hz.symm
    exact AnalyticAt.congr (by fun_prop) A

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
z₀ : 𝕜
e : E
inst✝ : Decidable (e = 0)
he : ¬e = 0
⊢ meromorphicOrderAt (fun x ↦ e) z₀ = 0

Tactic:
· exact (meromorphicOrderAt_eq_int_iff (.const e z₀)).2 ⟨fun _ ↦ e, by fun_prop, by simpa⟩

Goal state after:
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 (f ^ n) x = ↑n * meromorphicOrderAt f x

Tactic:
simp only [hn, zpow_zero, WithTop.coe_zero, zero_mul]

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
⊢ meromorphicOrderAt 1 x = 0
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
⊢ (f z).re = z.re

Tactic:
apply LinearIsometry.re_apply_eq_re_of_add_conj_eq

Goal state after:
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
⊢ ∀ (z : ℂ), z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
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)
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
⊢ ∃ Γ, p ∘ ⇑Γ = ⇑γ ∧ Γ 0 = e

Tactic:
suffices ∀ n, ∃ Γ : I → E, ContinuousOn Γ (Set.Icc 0 (t n)) ∧
      (Set.Icc 0 (t n)).EqOn (p ∘ Γ) γ ∧ Γ 0 = e by
    obtain ⟨Γ, cont, eqOn, Γ_0⟩ := this n_max
    rw [h_max _ le_rfl] at cont eqOn
    exact ⟨⟨Γ, continuousOn_univ.mp
      (by convert! cont; rw [eq_comm, Set.eq_univ_iff_forall]; exact fun t ↦ ⟨bot_le, le_top⟩)⟩,
      funext fun _ ↦ eqOn ⟨bot_le, le_top⟩, Γ_0⟩

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)
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 : ℕ), ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t n)) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n)) ∧ Γ 0 = e
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
⊢ ℓ (↑a.re • ↑b.re) + ℓ (↑(a.im * b.re) • I) + (ℓ (↑a.re • ↑b.im • I) + ℓ (↑(-a.im * b.im) • 1)) =
    ↑a.re • ℓ ↑b.re + (↑a.im • I) • ℓ ↑b.re + (↑a.re • ℓ (↑b.im • I) + (↑a.im • I) • ℓ (↑b.im • I))

Tactic:
rw [Complex.coe_smul, ℓ.map_smul]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
⊢ a.re • ℓ ↑b.re + ℓ (↑(a.im * b.re) • I) + (ℓ (↑a.re • ↑b.im • I) + ℓ (↑(-a.im * b.im) • 1)) =
    ↑a.re • ℓ ↑b.re + (↑a.im • I) • ℓ ↑b.re + (↑a.re • ℓ (↑b.im • I) + (↑a.im • I) • ℓ (↑b.im • I))
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
⊢ a.re • ℓ ↑b.re + ℓ (↑(a.im * b.re) • I) + (ℓ (↑a.re • ↑b.im • I) + ℓ (↑(-a.im * b.im) • 1)) =
    ↑a.re • ℓ ↑b.re + (↑a.im • I) • ℓ ↑b.re + (↑a.re • ℓ (↑b.im • I) + (↑a.im • I) • ℓ (↑b.im • I))

Tactic:
rw [Complex.coe_smul, ℓ.map_smul]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
⊢ a.re • ℓ ↑b.re + (a.im * b.re) • ℓ I + (ℓ (↑a.re • ↑b.im • I) + ℓ (↑(-a.im * b.im) • 1)) =
    ↑a.re • ℓ ↑b.re + (↑a.im • I) • ℓ ↑b.re + (↑a.re • ℓ (↑b.im • I) + (↑a.im • I) • ℓ (↑b.im • I))
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
⊢ a.re • ℓ ↑b.re + (a.im * b.re) • ℓ I + (ℓ (↑a.re • ↑b.im • I) + ℓ (↑(-a.im * b.im) • 1)) =
    ↑a.re • ℓ ↑b.re + (↑a.im • I) • ℓ ↑b.re + (↑a.re • ℓ (↑b.im • I) + (↑a.im • I) • ℓ (↑b.im • I))

Tactic:
rw [Complex.coe_smul, ℓ.map_smul]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
⊢ a.re • ℓ ↑b.re + (a.im * b.re) • ℓ I + (a.re • ℓ (↑b.im • I) + ℓ (↑(-a.im * b.im) • 1)) =
    ↑a.re • ℓ ↑b.re + (↑a.im • I) • ℓ ↑b.re + (↑a.re • ℓ (↑b.im • I) + (↑a.im • I) • ℓ (↑b.im • I))
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
⊢ a.re • ℓ ↑b.re + (a.im * b.re) • ℓ I + (a.re • ℓ (↑b.im • I) + ℓ (↑(-a.im * b.im) • 1)) =
    ↑a.re • ℓ ↑b.re + (↑a.im • I) • ℓ ↑b.re + (↑a.re • ℓ (↑b.im • I) + (↑a.im • I) • ℓ (↑b.im • I))

Tactic:
rw [Complex.coe_smul, ℓ.map_smul]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
⊢ a.re • ℓ ↑b.re + (a.im * b.re) • ℓ I + (a.re • b.im • ℓ I + ℓ (↑(-a.im * b.im) • 1)) =
    ↑a.re • ℓ ↑b.re + (↑a.im • I) • ℓ ↑b.re + (↑a.re • b.im • ℓ I + (↑a.im • I) • b.im • ℓ I)
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
⊢ a.re • ℓ ↑b.re + (a.im * b.re) • ℓ I + (a.re • b.im • ℓ I + ℓ (↑(-a.im * b.im) • 1)) =
    ↑a.re • ℓ ↑b.re + (↑a.im • I) • ℓ ↑b.re + (↑a.re • b.im • ℓ I + (↑a.im • I) • b.im • ℓ I)

Tactic:
rw [Complex.coe_smul, ℓ.map_smul]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
⊢ a.re • ℓ ↑b.re + (a.im * b.re) • ℓ I + (a.re • b.im • ℓ I + (-a.im * b.im) • ℓ 1) =
    ↑a.re • ℓ ↑b.re + (↑a.im • I) • ℓ ↑b.re + (↑a.re • b.im • ℓ I + (↑a.im • I) • b.im • ℓ I)
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
⊢ a.re • ℓ ↑b.re + (a.im * b.re) • ℓ I + (a.re • b.im • ℓ I + (-a.im * b.im) • ℓ 1) =
    ↑a.re • ℓ ↑b.re + (↑a.im • I) • ℓ ↑b.re + (↑a.re • b.im • ℓ I + (↑a.im • I) • b.im • ℓ I)

Tactic:
rw [Complex.coe_smul, ℓ.map_smul]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
⊢ a.re • ℓ ↑b.re + (a.im * b.re) • ℓ I + (a.re • b.im • ℓ I + (-a.im * b.im) • ℓ 1) =
    a.re • ℓ ↑b.re + (↑a.im • I) • ℓ ↑b.re + (↑a.re • b.im • ℓ I + (↑a.im • I) • b.im • ℓ I)
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
γ✝ : C(↑I, X)
e✝ : E
γ_0 : γ✝ 0 = p e✝
x y z : X
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
Γ : C(↑I, E) := cov.liftPath (↑γ) e ⋯
⊢ ↑γ' 0 = p (Γ 1)

Tactic:
simpa using congr($(cov.liftPath_lifts γ ..) 1).symm

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

Goal state before:
pp: case neg
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y z : X
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
x✝ : ↑I
h✝ : ¬↑x✝ ≤ 1 / 2
⊢ ↑γ' 0 = p ((cov.liftPath (↑γ) e ⋯) 1)

Tactic:
simpa using congr($(cov.liftPath_lifts γ ..) 1).symm

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
w : ℂ
hw : |w.im - a| ≤ b
⊢ |d * (w.im - (↑a).re)| ≤ d * b

Tactic:
ofReal_re,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
w : ℂ
hw : |w.im - a| ≤ b
⊢ |d * (w.im - a)| ≤ d * b
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ ≤ (ε + sSupNormIm f 0) ^ (1 - z.re) * (ε + sSupNormIm f 1) ^ z.re

Tactic:
rw [← mul_inv_le_iff₀', ← one_mul (((ε + sSupNormIm f 1) ^ z.re)), ← mul_inv_le_iff₀,
    ← Real.rpow_neg_one, ← Real.rpow_neg_one]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ * ((ε + sSupNormIm f 0) ^ (1 - z.re)) ^ (-1) * ((ε + sSupNormIm f 1) ^ z.re) ^ (-1) ≤ 1

E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < (ε + sSupNormIm f 1) ^ z.re

E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < (ε + sSupNormIm f 0) ^ (1 - z.re)