mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Uniform

Goal state before:
pp: case inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx : ‖r⁻¹ • x‖ ≤ 1
y : E
hy : ‖r⁻¹ • y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
this : ε / r ≤ ‖r⁻¹ • x - r⁻¹ • y‖ → ‖r⁻¹ • x + r⁻¹ • y‖ ≤ 2 - δ
⊢ ‖x + y‖ ≤ 2 * r - δ * r

Tactic:
← smul_add,

Goal state after:
case inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx : ‖r⁻¹ • x‖ ≤ 1
y : E
hy : ‖r⁻¹ • y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
this : ε / r ≤ ‖r⁻¹ • x - r⁻¹ • y‖ → ‖r⁻¹ • (x + y)‖ ≤ 2 - δ
⊢ ‖x + y‖ ≤ 2 * r - δ * r
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
he : ∀ (x : F), ‖e x‖ = ‖x‖
⊢ ‖f w‖ = ‖f z‖

Tactic:
replace hz : IsMaxOn (norm ∘ e ∘ f) (closedBall z (dist w z)) z := by
    simpa only [IsMaxOn, Function.comp_def, he] using hz

Goal state after:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
he : ∀ (x : F), ‖e x‖ = ‖x‖
hz : IsMaxOn (norm ∘ ⇑e ∘ f) (closedBall z (dist w z)) z
⊢ ‖f w‖ = ‖f z‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ -arctan 1 = -(π / 4)

Tactic:
arctan_one

Goal state after:
x : ℝ
⊢ -(π / 4) = -(π / 4)
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
⊢ BddAbove (slope f x '' {y | y ∈ s ∧ y < x})

Tactic:
obtain ⟨y, hyx, hys⟩ : ∃ y, x < y ∧ y ∈ s :=
    Eventually.exists_gt (mem_interior_iff_mem_nhds.mp hxs)
  refine bddAbove_iff_subset_Iic.mpr ⟨slope f x y, fun y' ⟨z, hz, hz'⟩ ↦ ?_⟩
  simp_rw [mem_Iic, ← hz']
  refine hfc.slope_mono (interior_subset hxs) ?_ ?_ (hz.2.trans hyx).le
  · simp [hz.2.ne, hz.1]
  · simp [hys, hyx.ne']

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

Goal state before:
pp: case insert
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
a : ι
s : Finset ι
ha : a ∉ s
hs :
  (∀ i ∈ s, MeromorphicOn (f i) U) →
    (∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤) → divisor (∏ i ∈ s, f i) U = ∑ i ∈ s, divisor (f i) U
h₁f : ∀ i ∈ insert a s, MeromorphicOn (f i) U
h₂f : ∀ i ∈ insert a s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
⊢ divisor (∏ i ∈ insert a s, f i) U = ∑ i ∈ insert a s, divisor (f i) U

Tactic:
| insert a s ha hs =>

Goal state after:
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
⊢ f x ≠ 0 → meromorphicOrderAt f x = 0

Tactic:
intro h
    rcases id hf with h₁ | ⟨n, g, h₁g, h₂g, h₃g⟩
    · have := h₁.eq_of_nhds
      tauto
    · have : n = 0 := by
        by_contra hContra
        have := h₃g.eq_of_nhds
        simp only [Pi.smul_apply', Pi.pow_apply, sub_self, zero_zpow n hContra, zero_smul] at this
        tauto
      simp only [this, zpow_zero] at h₃g
      apply (meromorphicOrderAt_eq_int_iff hf.meromorphicAt).2
      use g, h₁g, h₂g
      simp only [zpow_zero]
      exact h₃g.filter_mono nhdsWithin_le_nhds

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

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hfg : f =ᶠ[𝓝 x] g
⊢ MeromorphicNFAt f x → MeromorphicNFAt g x

Tactic:
rintro (h | ⟨n, h, h₁h, h₂h, h₃h⟩)
    · exact .inl (hfg.symm.trans h)
    · exact .inr ⟨n, h, h₁h, h₂h, hfg.symm.trans h₃h⟩

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

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

Tactic:
use -n, g⁻¹, h₁.inv h₂, (by simp_all)

Goal state after:
case right
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
n : ℤ
g : 𝕜 → 𝕜
h₁ : AnalyticAt 𝕜 g x
h₂ : g x ≠ 0
h₃ : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
⊢ f⁻¹ =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ (-n) • g⁻¹
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

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

Tactic:
by_cases h₂ : meromorphicOrderAt f₁ x = ⊤

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

case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
h₁ : MeromorphicAt f₁ x
h₂ : ¬meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
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 : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = 0
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, g x = 0

Tactic:
rw [eventually_nhdsWithin_iff] at hg_eq ⊢

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = 0
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = (x_1 - x) ^ n • g x_1
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → g x_1 = 0
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
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
h : meromorphicOrderAt f x ≠ ⊤
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
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, f x ≠ 0

Tactic:
filter_upwards [h₃g, self_mem_nhdsWithin, eventually_nhdsWithin_of_eventually_nhds
      ((h₁g.continuousAt.ne_iff_eventually_ne continuousAt_const).mp h₂g)]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
h : meromorphicOrderAt f x ≠ ⊤
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
⊢ ∀ (a : 𝕜), f a = (a - x) ^ (meromorphicOrderAt f x).untop₀ • g a → a ∈ {x}ᶜ → g a ≠ 0 → f a ≠ 0
Module: Mathlib.Analysis.Meromorphic.NormalForm

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

Tactic:
refine ⟨fun h y hy ↦ ?_, fun h y hy ↦ ?_⟩
  · rw [add_singleton, mem_image] at hy
    obtain ⟨x, h₁x, h₂x⟩ := hy
    simpa [← h₂x, ← meromorphicNFAt_comp_add_const_iff_meromorphicNFAt] using h h₁x
  · rw [meromorphicNFAt_comp_add_const_iff_meromorphicNFAt]
    aesop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
R : ℝ
⊢ MeromorphicNFOn (f ∘ fun x ↦ x - c) (closedBall c R) ↔ MeromorphicNFOn f (closedBall 0 R)

Tactic:
by
  rw [meromorphicNFOn_comp_sub_const_iff_meromorphicNFOn, closedBall_sub_singleton, sub_self]

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
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
h₁f₁ : ¬↑n₁ = ⊤
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₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
h₁ : n₁ = n₂
g₂ : 𝕜 → E
h₂ : g₁ x + g₂ x ≠ 0
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
τ₀ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + g₂) z
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = g₁ x + g₂ x

Tactic:
simp [AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (by fun_prop)
    (by simp_all) τ₀]

Goal state after:
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
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x

Tactic:
rw [h₂, eq_comm]
    simp_all [meromorphicOrderAt_eq_top_iff]

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

Goal state before:
pp: case insert
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
ι : Type u_5
f : ι → 𝕜 → 𝕜'
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, MeromorphicAt (f i) x) → meromorphicOrderAt (∏ i ∈ s, f i) x = ∑ i ∈ s, meromorphicOrderAt (f i) x
hf : ∀ i ∈ insert a s, MeromorphicAt (f i) x
⊢ meromorphicOrderAt (∏ i ∈ insert a s, f i) x = ∑ i ∈ insert a s, meromorphicOrderAt (f i) x

Tactic:
| insert a s ha hs =>

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
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

Tactic:
let F (a : A) : E := Γ _ (somePath a₀ a).source 1

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 : A → E := fun a ↦ (Γ (somePath a₀ a).toContinuousMap ⋯) 1
⊢ ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f
Module: Mathlib.Analysis.Complex.Conformal

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

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

Goal state after:
case inl
c : ℝ
a : Circle
⊢ restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ) = c • (rotation a).toLinearIsometry.toContinuousLinearMap
Module: Mathlib.Analysis.Complex.PhragmenLindelof

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

Tactic:
filter_upwards [(eventually_cobounded_le_norm 1).filter_mono inf_le_left] with z hz
    simp only [Real.norm_eq_abs, Real.abs_exp]
    gcongr

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
x y : X
γ : Path.Homotopic.Quotient x y
ex : ↑(p ⁻¹' {x})
ey : ↑(p ⁻¹' {y})
Γ : Path.Homotopic.Quotient ↑ex ↑ey
eq : Γ.map { toFun := p, continuous_toFun := ⋯ } = γ.cast ⋯ ⋯
⊢ cov.monodromy γ ex = ey

Tactic:
convert ← cov.monodromy_map Γ

Goal state after:
case e'_1
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y : X
γ : Path.Homotopic.Quotient x y
ex : ↑(p ⁻¹' {x})
ey : ↑(p ⁻¹' {y})
Γ : Path.Homotopic.Quotient ↑ex ↑ey
eq : Γ.map { toFun := p, continuous_toFun := ⋯ } = γ.cast ⋯ ⋯
⊢ { toFun := p, continuous_toFun := ⋯ } ↑ey = y

case e'_2.e'_7
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y : X
γ : Path.Homotopic.Quotient x y
ex : ↑(p ⁻¹' {x})
ey : ↑(p ⁻¹' {y})
Γ : Path.Homotopic.Quotient ↑ex ↑ey
eq : Γ.map { toFun := p, continuous_toFun := ⋯ } = γ.cast ⋯ ⋯
e_1✝ : ↑(p ⁻¹' {{ toFun := p, continuous_toFun := ⋯ } ↑ey}) = ↑(p ⁻¹' {y})
⊢ { toFun := p, continuous_toFun := ⋯ } ↑ex = x

case e'_2.e'_8
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y : X
γ : Path.Homotopic.Quotient x y
ex : ↑(p ⁻¹' {x})
ey : ↑(p ⁻¹' {y})
Γ : Path.Homotopic.Quotient ↑ex ↑ey
eq : Γ.map { toFun := p, continuous_toFun := ⋯ } = γ.cast ⋯ ⋯
e_1✝ : ↑(p ⁻¹' {{ toFun := p, continuous_toFun := ⋯ } ↑ey}) = ↑(p ⁻¹' {y})
⊢ { toFun := p, continuous_toFun := ⋯ } ↑ey = y

case e'_2.e'_9
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y : X
γ : Path.Homotopic.Quotient x y
ex : ↑(p ⁻¹' {x})
ey : ↑(p ⁻¹' {y})
Γ : Path.Homotopic.Quotient ↑ex ↑ey
eq : Γ.map { toFun := p, continuous_toFun := ⋯ } = γ.cast ⋯ ⋯
e_1✝ : ↑(p ⁻¹' {{ toFun := p, continuous_toFun := ⋯ } ↑ey}) = ↑(p ⁻¹' {y})
e_7✝ : { toFun := p, continuous_toFun := ⋯ } ↑ex = x
e_8✝ : { toFun := p, continuous_toFun := ⋯ } ↑ey = y
⊢ Γ.map { toFun := p, continuous_toFun := ⋯ } ≍ γ

case e'_3.e'_2
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y : X
γ : Path.Homotopic.Quotient x y
ex : ↑(p ⁻¹' {x})
ey : ↑(p ⁻¹' {y})
Γ : Path.Homotopic.Quotient ↑ex ↑ey
eq : Γ.map { toFun := p, continuous_toFun := ⋯ } = γ.cast ⋯ ⋯
e_1✝ : ↑(p ⁻¹' {{ toFun := p, continuous_toFun := ⋯ } ↑ey}) = ↑(p ⁻¹' {y})
x✝ : E
⊢ { toFun := p, continuous_toFun := ⋯ } ↑ey = y
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
x c : 𝕜
f : 𝕜 → E
h : ¬¬MeromorphicAt f (x + c)
⊢ meromorphicOrderAt (f ∘ fun x ↦ x + c) x = meromorphicOrderAt f (x + c)

Tactic:
rw [MeromorphicAt.meromorphicOrderAt_comp (by simp_all) (by fun_prop)
    (by simp [eventuallyConst_iff_analyticOrderAt_sub_eq_top])]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : ¬¬MeromorphicAt f (x + c)
⊢ meromorphicOrderAt f (x + c) * ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ x_1 + c - (x + c)) x) =
    meromorphicOrderAt f (x + c)
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: 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
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
⊢ ∑ i ∈ t₂, log (‖canonicalFactor R i w‖ ^ (divisor f B₀R) i) + ∑ i ∈ t₁, log (‖w - i‖ ^ (-divisor f S₀R) i) +
      log ‖meromorphicTrailingCoeffAt f w‖ =
    ∑ i ∈ t₂, ↑((divisor f B₀R) i) * log ‖canonicalFactor R i w‖ + ∑ x ∈ t₁, -(↑((divisor f S₀R) x) * log ‖w - x‖) +
      log ‖meromorphicTrailingCoeffAt f w‖

Tactic:
congr! 3 with i hi i hi <;> simp

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

Goal state before:
pp: case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

pp: case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Tactic:
· eta_expand; simp_rw [interpStrip_eq_of_zero f _ h]; exact diffContOnCl_const

Goal state after:
case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)
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)| ≤ d * b

Tactic:
_root_.abs_mul,

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
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ Tendsto (fun ε ↦ ‖(↑ε + ↑(sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(sSupNormIm f 1)) ^ z‖) (𝓝[>] 0) (𝓝 ‖interpStrip f z‖)

Tactic:
rw [interpStrip_eq_of_mem_verticalStrip _ _ hz]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ Tendsto (fun ε ↦ ‖(↑ε + ↑(sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(sSupNormIm f 1)) ^ z‖) (𝓝[>] 0)
    (𝓝 ‖↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z‖)
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: 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 := ∫ (x : ℝ) in c.re..w.re, f (↑x + ↑c.im * I)
I₂ : E := I • ∫ (y : ℝ) in c.im..w.im, f (↑w.re + ↑y * I)
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f (↑x + ↑c.im * I)
I₄ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑z.re + ↑y * I)
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₆ : E := I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑c.im * I)
I₈ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑w.re + ↑y * I)
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₇
⊢ I₂ = I₈ + I₆

Tactic:
← smul_add,

Goal state after:
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 := ∫ (x : ℝ) in c.re..w.re, f (↑x + ↑c.im * I)
I₂ : E := I • ∫ (y : ℝ) in c.im..w.im, f (↑w.re + ↑y * I)
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f (↑x + ↑c.im * I)
I₄ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑z.re + ↑y * I)
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₆ : E := I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑c.im * I)
I₈ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑w.re + ↑y * I)
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₇
⊢ I₂ = I • ((∫ (y : ℝ) in c.im..z.im, f (↑w.re + ↑y * I)) + ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I))
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: case right
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ Δ (f₁ - f₂) =ᶠ[𝓝 x] 0

Tactic:
filter_upwards [h₁.1.laplacian_sub_nhds h₂.1, h₁.2, h₂.2]
    simp_all

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ Δ[s] f₁ - f₂ =ᶠ[𝓝[s] x] (Δ[s] f₁) - Δ[s] f₂

Tactic:
nth_rw 1 [← s.insert_eq_of_mem hx]
  filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp),
    eventually_mem_nhdsWithin] with y h₁y h₂y h₃y
  rw [s.insert_eq_of_mem hx] at h₃y
  simp [h₁y.laplacianWithin_sub h₂y hs h₃y]

Goal state after: