mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ meromorphicTrailingCoeffAt f x = g x

Tactic:
have h₁f : MeromorphicAt f x := by
    rw [MeromorphicAt.meromorphicAt_congr h]
    fun_prop
  by_cases h₃ : meromorphicOrderAt f x = ⊤
  · simp only [h₃, WithTop.untop₀_top, zpow_zero, one_smul,
      MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top] at ⊢ h
    apply EventuallyEq.eq_of_nhds (f := 0)
    rw [← ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop) (by fun_prop)]
    apply (h.symm.trans (meromorphicOrderAt_eq_top_iff.1 h₃)).symm
  · unfold meromorphicTrailingCoeffAt
    simp only [h₁f, reduceDIte, h₃, ne_eq]
    obtain ⟨h'₁, h'₂, h'₃⟩ := ((meromorphicOrderAt_ne_top_iff h₁f).1 h₃).choose_spec
    apply Filter.EventuallyEq.eq_of_nhds
    rw [← h'₁.continuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE h₁g.continuousAt]
    filter_upwards [h, h'₃, self_mem_nhdsWithin] with y h₁y h₂y h₃y
    rw [← sub_eq_zero]
    rwa [h₂y, ← sub_eq_zero, ← smul_sub, smul_eq_zero_iff_right] at h₁y
    simp_all [zpow_ne_zero, sub_ne_zero]

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 : 𝕜 → E
x : 𝕜
h : 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
y : 𝕜
h₁y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₂y : y ∈ {x}ᶜ
⊢ g y = ((y - x) ^ (meromorphicOrderAt f x).untop₀)⁻¹ • (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y

Tactic:
← smul_assoc,

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

Goal state before:
pp: case mpr.left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
u : 𝕜
hu : ¬(MeromorphicOn.divisor f U) u = 0
⊢ u ∈ U

Tactic:
exact (MeromorphicOn.divisor f U).supportWithinDomain hu

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

Tactic:
lift meromorphicOrderAt f x to ℤ using h₂ with n hn

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
n : ℤ
hn : ↑n = meromorphicOrderAt f x
⊢ ↑n = meromorphicOrderAt (-f) x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: w z : ℂ
hzw : z - w ≠ 0
hw : w ∈ ball 0 ‖z‖
hz : z ∈ sphere 0 ‖z‖
hR : 0 < ‖z‖
⊢ ‖(starRingEnd ℂ) z * z - (starRingEnd ℂ) w * z‖ = ‖↑‖z‖ * (z - w)‖

Tactic:
← sub_mul,

Goal state after:
w z : ℂ
hzw : z - w ≠ 0
hw : w ∈ ball 0 ‖z‖
hz : z ∈ sphere 0 ‖z‖
hR : 0 < ‖z‖
⊢ ‖((starRingEnd ℂ) z - (starRingEnd ℂ) w) * z‖ = ‖↑‖z‖ * (z - w)‖
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∈ ball 0 R
⊢ (divisor (canonicalFactor R w) (ball 0 R)) z = (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z

pp: case neg
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∉ ball 0 R
⊢ (divisor (canonicalFactor R w) (ball 0 R)) z = (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z

Tactic:
· rw [MeromorphicOn.divisor_apply
      (fun z hz ↦ meromorphic_canonicalFactor R w z) hz]
    obtain (rfl | h₂z) := eq_or_ne z w
    · rw [meromorphicOrderAt_canonicalFactor hz]
      simp_all [Function.locallyFinsuppWithin.restrict_apply]
    · have : meromorphicOrderAt (canonicalFactor R w) z = 0 := by
        rw [(meromorphicNFOn_canonicalFactor hw (Set.mem_univ z)).meromorphicOrderAt_eq_zero_iff]
        exact canonicalFactor_ne_zero hw (ball_subset_closedBall hz) h₂z
      simp [this, h₂z, Function.locallyFinsuppWithin.restrict_apply, hz]

Goal state after:
case neg
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∉ ball 0 R
⊢ (divisor (canonicalFactor R w) (ball 0 R)) z = (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
a : 𝕜
h₂a : (divisor f U) a = 0 a
h₃a : MeromorphicNFAt (φ⁻¹ • f) a
h₄a : a ∈ U
⊢ f a = (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u) a • (φ a)⁻¹ • f a

Tactic:
← smul_assoc,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
a : 𝕜
h₂a : (divisor f U) a = 0 a
h₃a : MeromorphicNFAt (φ⁻¹ • f) a
h₄a : a ∈ U
⊢ f a = ((∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u) a • (φ a)⁻¹) • f a
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 : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
z : ℂ
hz : z ∈ closedBall 0 R
⊢ meromorphicOrderAt (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) z + meromorphicOrderAt f z ≠ ⊤

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 : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
z : ℂ
hz : z ∈ closedBall 0 R
⊢ MeromorphicAt (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) z

Tactic:
· simpa [h₂f ⟨z, hz⟩] using canonicalDecomposition_aux₃ hR

Goal state after:
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 : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
z : ℂ
hz : z ∈ closedBall 0 R
⊢ MeromorphicAt (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) z
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inr
𝕜 : 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
h✝ : meromorphicOrderAt f₁ x ≠ meromorphicOrderAt f₂ x
h : meromorphicOrderAt f₂ x < meromorphicOrderAt f₁ x
⊢ meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)

Tactic:
· simpa [h.le] using meromorphicOrderAt_add_eq_right_of_lt hf₁ h

Goal state after:
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 : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
a : ℂ
ha : a ∈ (-divisor f (ball 0 R)).supportᶜ
h₂a : a ∈ closedBall 0 R
⊢ f a =
    (∏ x ∈ η₀.toFinset, canonicalFactor R x a ^ (-(divisor f (ball 0 R)) x)) •
      (∏ x ∈ η₀.toFinset, canonicalFactor R x a ^ (divisor f (ball 0 R)) x) • f a

Tactic:
← smul_assoc,

Goal state after:
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 : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
a : ℂ
ha : a ∈ (-divisor f (ball 0 R)).supportᶜ
h₂a : a ∈ closedBall 0 R
⊢ f a =
    ((∏ x ∈ η₀.toFinset, canonicalFactor R x a ^ (-(divisor f (ball 0 R)) x)) •
        ∏ x ∈ η₀.toFinset, canonicalFactor R x a ^ (divisor f (ball 0 R)) x) •
      f a
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
η₁ : AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x
η₀ : f =ᶠ[𝓝[≠] x] (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g
this : meromorphicOrderAt (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x = 0
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x

Tactic:
divisor_apply (D.meromorphicOn.mono_set sphere_subset_closedBall) (by aesop),

Goal state after:
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
η₁ : AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x
η₀ : f =ᶠ[𝓝[≠] x] (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g
this : meromorphicOrderAt (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x = 0
⊢ (divisor g (closedBall 0 R)) x = (meromorphicOrderAt f x).untop₀
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
inst✝¹ : CompleteSpace 𝕜
f : 𝕜 → 𝕜
inst✝ : CharZero 𝕜
hf : MeromorphicAt f x
h₁ : meromorphicOrderAt f x ≠ 0
h₂ : meromorphicOrderAt f x ≠ ⊤
⊢ meromorphicOrderAt (logDeriv f) x = -1

Tactic:
lift meromorphicOrderAt f x to ℤ using h₂ with n hn

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
⊢ meromorphicOrderAt (logDeriv f) x = -1
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
x : ℝ
⊢ 0 ≤ sSupNormIm f x

Tactic:
apply Real.sSup_nonneg

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
x : ℝ
⊢ ∀ x_1 ∈ norm ∘ f '' re ⁻¹' {x}, 0 ≤ x_1
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ re ⁻¹' {0, 1}
⊢ ‖F f ε z‖ ≤ 1

Tactic:
simp only [F, norm_smul, norm_invInterpStrip f z hε]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ re ⁻¹' {0, 1}
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1
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
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
x : X
e : ↑(p ⁻¹' {x})
γ : FundamentalGroup X x
h : (hp.fundamentalGroupToMulOpposite e) γ = 1
⊢ ↑(⋯.monodromy γ e) = ↑e

Tactic:
rw [← hp.unop_fundamentalGroupToMulOpposite_smul, h]; apply one_smul

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

Goal state before:
pp: case e_f
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
m : Fin (Module.finrank ℝ E)
⊢ w m ⊗ₜ[ℝ] w m = (if m = m then 1 else 0) • w m ⊗ₜ[ℝ] w m

Tactic:
simp only [↓reduceIte, one_smul]

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

Goal state before:
pp: l u : ℝ
hul : l < u
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
⊢ ↑l + z * (↑u - ↑l) ∈ verticalClosedStrip l u

Tactic:
by
  simp only [verticalClosedStrip, mem_preimage, add_re, ofReal_re, mul_re, sub_re, sub_im,
    ofReal_im, sub_self, mul_zero, sub_zero, mem_Icc] at hz ⊢
  constructor <;> nlinarith [hz.1, hz.2, hul]

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init m 0 = m 0
hmtail : tail m (last n) = m (last n.succ)
⊢ ∂_{m 0} (∂^{init (tail m)} (∂_{tail m (last n)} f)) = ∂^{init m} (∂_{m (last (n + 1))} f)

Tactic:
hmtail,

Goal state after:
V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init m 0 = m 0
hmtail : tail m (last n) = m (last n.succ)
⊢ ∂_{m 0} (∂^{init (tail m)} (∂_{m (last n.succ)} f)) = ∂^{init m} (∂_{m (last (n + 1))} f)
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
n : ℕ
y : V
f : E
⊢ ∂^{fun x ↦ y} f = ∂_{y}^[n] f

Tactic:
by
  induction n with
  | zero => rfl
  | succ n IH =>
    rw [iteratedLineDerivOp_succ_left, Function.iterate_succ_apply']
    congr

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
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
⊢ ∃ R, |z.re| < R ∧ ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C

Tactic:
by
    refine ((eventually_gt_atTop _).and ?_).exists
    rcases hO.exists_pos with ⟨A, hA₀, hA⟩
    simp only [isBigOWith_iff, eventually_inf_principal, eventually_comap, mem_Ioo,
      mem_preimage, (· ∘ ·), Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] at hA
    suffices
        Tendsto (fun R => expR (δ * expR (d * R) + B * expR (c * R) + Real.log A)) atTop (𝓝 0) by
      filter_upwards [this.eventually (ge_mem_nhds hC₀), hA] with R hR Hle w hre him
      calc
        ‖g ε w • f w‖ ≤ expR (δ * expR (d * R) + B * expR (c * R) + Real.log A) := ?_
        _ ≤ C := hR
      rw [norm_smul, Real.exp_add, ← hre, Real.exp_add, Real.exp_log hA₀, mul_assoc, mul_comm _ A]
      gcongr
      exacts [hδ <| Ioo_subset_Icc_self him, Hle _ hre him]
    refine Real.tendsto_exp_atBot.comp ?_
    suffices H : Tendsto (fun R => δ + B * (expR ((d - c) * R))⁻¹) atTop (𝓝 (δ + B * 0)) by
      rw [mul_zero, add_zero] at H
      refine Tendsto.atBot_add ?_ tendsto_const_nhds
      simpa only [id, (· ∘ ·), add_mul, mul_assoc, ← div_eq_inv_mul, ← Real.exp_sub, ← sub_mul,
        sub_sub_cancel]
        using H.neg_mul_atTop δ₀ <| Real.tendsto_exp_atTop.comp <| tendsto_id.const_mul_atTop hd₀
    refine tendsto_const_nhds.add (tendsto_const_nhds.mul ?_)
    exact tendsto_inv_atTop_zero.comp <| Real.tendsto_exp_atTop.comp <|
      tendsto_id.const_mul_atTop (sub_pos.2 hcd)

Goal state after:
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₇
hI₂ : I₂ = I₈ + I₆
⊢ I₇ - I₅ + I₈ - I₄ = 0

Tactic:
have wzInBall : w.re + z.im * I ∈ ball c r :=
      mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)

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₇
hI₂ : I₂ = I₈ + I₆
wzInBall : ↑w.re + ↑z.im * I ∈ ball c r
⊢ I₇ - I₅ + I₈ - I₄ = 0
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₇
hI₂ : I₂ = I₈ + I₆
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f

Tactic:
have hI₀ : I₇ - I₅ + I₈ - I₄ = 0 := by
    have wzInBall : w.re + z.im * I ∈ ball c r :=
      mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)
    have wcInBall : w.re + c.im * I ∈ ball c r := re_add_im_mul_mem_ball w_mem
    have hU : Rectangle (z.re + c.im * I) (w.re + z.im * I) ⊆ ball c r :=
      (convex_ball c r).rectangle_subset (re_add_im_mul_mem_ball hz) wzInBall
        (by simpa using hz) (by simpa using wcInBall)
    simpa [← add_eq_zero_iff_eq_neg, wedgeIntegral_add_wedgeIntegral_eq] using
      hf (z.re + c.im * I) (w.re + z.im * I) hU

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₇
hI₂ : I₂ = I₈ + I₆
hI₀ : I₇ - I₅ + I₈ - I₄ = 0
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f
Module: Mathlib.Analysis.Complex.MeanValue

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
⊢ circleAverage (fun z ↦ ((z - c) * (z - w)⁻¹) • f z) c |R| = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, |R|), (z - w)⁻¹ • f z

Tactic:
by
    simp only [circleAverage_eq_circleIntegral hR.ne', mul_inv_rev, inv_I, neg_mul, neg_smul,
      neg_inj, ne_eq, mul_eq_zero, I_ne_zero, inv_eq_zero, ofReal_eq_zero, pi_ne_zero,
      OfNat.ofNat_ne_zero, or_self, not_false_eq_true, smul_right_inj]
    apply circleIntegral.integral_congr hR.le
    intro z hz
    match_scalars
    have : z - c ≠ 0 := by grind [ne_of_mem_sphere]
    grind

Goal state after: