mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case coe.top
𝕜 : 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
h₂g : meromorphicOrderAt g x = ⊤
⊢ meromorphicOrderAt (f • g) x = ↑m + ⊤

Tactic:
| top =>

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
h : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt (f ^ n) x = ⊤

Tactic:
rw [meromorphicOrderAt_eq_top_iff] at *

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
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = 0
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
h₂f : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f⁻¹ x = ⊤

Tactic:
rw [meromorphicOrderAt_eq_top_iff] at *

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = 0
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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₂ x

Tactic:
rw [meromorphicOrderAt_congr]
  filter_upwards [meromorphicOrderAt_eq_top_iff.1 hf₁] with z hz
  simp_all

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
⊢ min ↑n₁ ↑n₂ ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
have t₁ : meromorphicOrderAt ((· - x) ^ n) x = n :=
    (meromorphicOrderAt_eq_int_iff t₀).2 ⟨1, analyticAt_const, by simp⟩

Goal state after:
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₂ ≤ meromorphicOrderAt (f₁ + f₂) x
Module: Mathlib.Analysis.Complex.Isometry

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

Tactic:
let a : Circle := ⟨f 1, by simp [Submonoid.unitSphere, f.norm_map]⟩
  use a
  have : (f.trans (rotation a).symm) 1 = 1 := by simpa [a] using rotation_apply a⁻¹ (f 1)
  refine (linear_isometry_complex_aux this).imp (fun h₁ => ?_) fun h₂ => ?_
  · simpa using eq_mul_of_inv_mul_eq h₁
  · exact eq_mul_of_inv_mul_eq h₂

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

Tactic:
meromorphicOrderAt_eq_top_iff,

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : ¬w = z
⊢ ¬∀ᶠ (z : 𝕜) in 𝓝[≠] ↑w, f z = 0
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 ℂ ℂ, ?_⟩
    ext1
    simp

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
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}
x✝¹ : Set ↑U
x✝ : ↑U
| meromorphicOrderAt f ↑x✝ = ⊤

Tactic:
meromorphicOrderAt_eq_top_iff,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}
x✝¹ : Set ↑U
x✝ : ↑U
| ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑x✝, f z = 0
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : R < 0
⊢ f =ᶠ[codiscreteWithin (closedBall 0 R)]
    ((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) *
        ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor f (sphere 0 R)) v) •
      fun x ↦ f 0

Tactic:
simp_all only [closedBall_of_neg]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f ∅
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : R < 0
⊢ f =ᶠ[codiscreteWithin ∅]
    ((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) *
        ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor f (sphere 0 R)) v) •
      fun x ↦ f 0
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : meromorphicOrderAt f ↑z = ⊤
⊢ ∃
    x ⊆
      {x |
        ∃ t, (∀ y ∈ t, y ∈ {↑x}ᶜ → f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x

Tactic:
meromorphicOrderAt_eq_top_iff,

Goal state after:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z = 0
⊢ ∃
    x ⊆
      {x |
        ∃ t, (∀ y ∈ t, y ∈ {↑x}ᶜ → f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case pos
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))
h : s ≤ t n
⊢ p (Γ s) = γ s

pp: case neg
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))
h : ¬s ≤ t n
⊢ p (q.invFun (γ s, (↑q (Γ (t n))).2)) = γ s

Tactic:
exacts [eqOn ⟨hs.1, h⟩, q.proj_symm_apply' (t_sub ⟨le_of_not_ge h, hs.2⟩)]

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

Goal state before:
pp: case e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
x : ℂ
⊢ meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ^ (-divisor f (sphere 0 R)) x = (w - x) ^ (-divisor f (sphere 0 R)) x

Tactic:
by_cases h : x = w

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h✝ : ℂ → E
D : ECanonicalDecomp f h✝ R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
x : ℂ
h : x = w
⊢ meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ^ (-divisor f (sphere 0 R)) x = (w - x) ^ (-divisor f (sphere 0 R)) x

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h✝ : ℂ → E
D : ECanonicalDecomp f h✝ R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
x : ℂ
h : ¬x = w
⊢ meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ^ (-divisor f (sphere 0 R)) x = (w - x) ^ (-divisor f (sphere 0 R)) x
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2
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✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : 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
⊢ Γ 1 = Γ' 1

Tactic:
(cov.eq_liftPath_iff' <| by simp [γ_0, he]).mpr ⟨Γ_lifts, Γ_0⟩,

Goal state after:
case refine_2
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✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : 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
⊢ (cov.liftPath (f.comp γ) e₀ ⋯) 1 = Γ' 1
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case inr.inr.inr.refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this : ∀ {C : ℝ}, (∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) → (∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) → 0 < C → ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
⊢ (↑a).re = a

Tactic:
ofReal_re

Goal state after:
case inr.inr.inr.refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this : ∀ {C : ℝ}, (∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) → (∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) → 0 < C → ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
⊢ a = a
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))
hB :
  ∃ c < π / (a + b - (a - b)),
    ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
hab : a - b < a + b
hb : 0 < b
⊢ ‖f z‖ ≤ C

Tactic:
rw [add_sub_sub_cancel, ← two_mul, div_mul_eq_div_div] at hB

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))
hB :
  ∃ c < π / 2 / b,
    ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
hab : a - b < a + b
hb : 0 < b
⊢ ‖f z‖ ≤ C
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case mpr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ (∃ x, x.re = u ∧ f x = e) → ∃ x, x.re = 1 ∧ f (↑l + x * (↑u - ↑l)) = e

Tactic:
· intro h
      obtain ⟨z, hz₁, hz₂⟩ := h
      use ((z - l) / (u - l))
      constructor
      · norm_cast
        grind [Complex.div_re, Complex.normSq_ofReal, sub_re, ofReal_re, ofReal_im, mul_eq_zero]
      · rw [div_mul_comm, div_self (by norm_cast; linarith)]
        simp only [one_mul, add_sub_cancel, hz₂]

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

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ MapsTo (fun z ↦ ↑l + z • (↑u - ↑l)) (verticalStrip 0 1) (verticalStrip l u)

Tactic:
· rw [MapsTo]
    intro z hz
    exact scale_id_mem_verticalStrip_of_mem_verticalStrip hul hz

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

Goal state before:
pp: case hbc.hb₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ⋯
I₂ : E := ⋯
I₃ : E := ⋯
I₄ : E := ⋯
I₅ : E := ⋯
I₆ : E := ⋯
I₇ : E := ⋯
I₈ : E := ⋯
z_ball : ball z (r - dist z c) ⊆ ball c r
w_mem : w ∈ ball c r
integrableHoriz :
  ∀ (a₁ a₂ b : ℝ),
    ↑a₁ + ↑b * I ∈ ball c r → ↑a₂ + ↑b * I ∈ ball c r → IntervalIntegrable (fun x ↦ f (↑x + ↑b * I)) volume a₁ a₂
integrableVert :
  ∀ (a b₁ b₂ : ℝ),
    ↑a + ↑b₁ * I ∈ ball c r → ↑a + ↑b₂ * I ∈ ball c r → IntervalIntegrable (fun y ↦ f (↑a + ↑y * I)) volume b₁ b₂
hI₁ : I₁ = I₃ + I₇
⊢ ↑w.re + ↑w.im * I ∈ ball c r

Tactic:
· simpa using w_mem

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Liouville

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
⊢ ∀ (z w : ℂ), f z = f w

Tactic:
by
  intro z w
  obtain ⟨ℓ, h₁ℓ, h₂ℓ⟩ := exists_dual_vector'' ℝ (f z - f w)
  rw [map_sub, RCLike.ofReal_real_eq_id, id_eq] at h₂ℓ
  have η₁ : Bornology.IsBounded (range (ℓ ∘ f)) := by
    simpa [range_comp] using IsBounded.image ℓ h_bound
  rw [← sub_eq_zero, ← norm_eq_zero, ← h₂ℓ]
  grind [bounded_harmonic_on_complex_plane_is_constant_aux (ℓ ∘ f) (h_harm.comp_CLM ℓ) η₁]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᵐ[μ] Ι a b
⊢ μ s = μ (Ι a b)

Tactic:
rw [measure_congr hs_ev]

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: case h₁f
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ ContinuousOn (circleAverage (re ∘ herglotzRieszKernel c w • f) c) (Set.Ioc ‖w - c‖ R)

pp: case hR
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ ‖w - c‖ < R

pp: case h₂f
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ Set.EqOn (circleAverage (re ∘ herglotzRieszKernel c w • f) c) (fun x ↦ f w) (Set.Ioo ‖w - c‖ R)

Tactic:
· apply ContinuousOn.circleAverage
    · rw [herglotzRieszKernel_fun_def]
      apply (continuousOn_herglotz_riesz hw).smul (hf.2.mono _)
      grind [closure_ball c (pos_of_mem_ball hw).ne', mem_closedBall_iff_norm]
    · grind [norm_nonneg (w - c)]

Goal state after:
case hR
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ ‖w - c‖ < R

case h₂f
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ Set.EqOn (circleAverage (re ∘ herglotzRieszKernel c w • f) c) (fun x ↦ f w) (Set.Ioo ‖w - c‖ R)
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: s t : ℝ
ht : 0 < t
⊢ IntegrableOn (fun x ↦ x ^ s) (Ioo 0 t) volume ↔ -1 < s

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  swap
  · rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le ht.le]
    apply intervalIntegrable_rpow' h (a := 0) (b := t)
  contrapose! h
  intro H
  have I : 0 < min 1 t := lt_min zero_lt_one ht
  have H' : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 (min 1 t)) :=
    H.mono (Set.Ioo_subset_Ioo le_rfl (min_le_right _ _)) le_rfl
  have : IntegrableOn (fun x ↦ x⁻¹) (Ioo 0 (min 1 t)) := by
    apply H'.mono' measurable_inv.aestronglyMeasurable
    filter_upwards [ae_restrict_mem measurableSet_Ioo] with x hx
    simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (le_of_lt hx.1)]
    rwa [← Real.rpow_neg_one x, Real.rpow_le_rpow_left_iff_of_base_lt_one hx.1]
    exact lt_of_lt_of_le hx.2 (min_le_left _ _)
  have : IntervalIntegrable (fun x ↦ x⁻¹) volume 0 (min 1 t) := by
    rwa [intervalIntegrable_iff_integrableOn_Ioo_of_le I.le]
  simp [intervalIntegrable_inv_iff, I.ne] at this

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

Goal state before:
pp: case hf₁
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
h₁ : ∀ z ∈ sphere 0 R, z - w ≠ 0
h₃ : ContinuousOn f (sphere 0 R)
⊢ CircleIntegrable (fun z ↦ (z / (z - w)) • f z) 0 R

Tactic:
apply ContinuousOn.circleIntegrable hR.le

Goal state after:
case hf₁
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ⋯
q : ℝ := ⋯
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
h₁ : ∀ z ∈ sphere 0 R, z - w ≠ 0
h₃ : ContinuousOn f (sphere 0 R)
⊢ ContinuousOn (fun z ↦ (z / (z - w)) • f z) (sphere 0 R)
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: case hf₁
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
h₁ : ∀ z ∈ sphere 0 R, z - w ≠ 0
h₃ : ContinuousOn f (sphere 0 R)
⊢ CircleIntegrable (fun z ↦ (z / (z - w)) • f z) 0 R

Tactic:
apply ContinuousOn.circleIntegrable hR.le
        fun_prop (disch := aesop)

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

Goal state before:
pp: case hf₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
h₁ : ∀ z ∈ sphere 0 R, z - w ≠ 0
h₃ : ContinuousOn f (sphere 0 R)
⊢ CircleIntegrable (fun z ↦ (q • z / (q • z - W)) • f z) 0 R

Tactic:
apply ContinuousOn.circleIntegrable hR.le

Goal state after:
case hf₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ⋯
q : ℝ := ⋯
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
h₁ : ∀ z ∈ sphere 0 R, z - w ≠ 0
h₃ : ContinuousOn f (sphere 0 R)
⊢ ContinuousOn (fun z ↦ (q • z / (q • z - W)) • f z) (sphere 0 R)
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: case hf₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
h₁ : ∀ z ∈ sphere 0 R, z - w ≠ 0
h₃ : ContinuousOn f (sphere 0 R)
⊢ CircleIntegrable (fun z ↦ (q • z / (q • z - W)) • f z) 0 R

Tactic:
apply ContinuousOn.circleIntegrable hR.le
        fun_prop (disch := aesop)

Goal state after: