mathlib-initiative/mathlib-tactics huggingface dataset:
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 : 𝕜
g : 𝕜 → E
hfg : f =ᶠ[𝓝 x] g
⊢ MeromorphicNFAt g x → MeromorphicNFAt f x

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

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

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hgne : g x ≠ 0
⊢ MeromorphicNFAt (f * g⁻¹) x

pp: case inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hfne : f x ≠ 0
⊢ MeromorphicNFAt (f * g⁻¹) x

Tactic:
· have hf := hf.meromorphicNFAt
    have hgAnalytic : AnalyticAt 𝕜 g x := by grind [meromorphicNFAt_iff_analyticAt_or]
    have hgInvAnalytic : AnalyticAt 𝕜 g⁻¹ x := hgAnalytic.inv hgne
    rwa [← meromorphicNFAt_mul_iff_left hgInvAnalytic (inv_ne_zero hgne)] at hf

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hfne : f x ≠ 0
⊢ MeromorphicNFAt (f * g⁻¹) x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n

Tactic:
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff h₁).1 h₂
    rw [h₁g.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE
        (n := (meromorphicOrderAt f x).untop₀) h₂g h₃g,
      (h₁g.zpow h₂g (n := n)).meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE
        (n := (meromorphicOrderAt (f ^ n) x).untop₀)
        (by simp_all [zpow_ne_zero])]
    · simp only [Pi.pow_apply]
    · filter_upwards [h₃g] with a ha
      simp_all [mul_zpow, ← zpow_mul, meromorphicOrderAt_zpow h₁, mul_comm]

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 : 𝕜
hf : AnalyticAt 𝕜 f x
a✝ : ℕ
hn : analyticOrderAt f x = ↑a✝
⊢ meromorphicOrderAt f x = ENat.map Nat.cast ↑a✝

Tactic:
· simp_rw [ENat.map_natCast, meromorphicOrderAt_eq_int_iff hf.meromorphicAt, zpow_natCast]
    rcases hf.analyticOrderAt_eq_natCast.mp hn with ⟨g, h1, h2, h3⟩
    exact ⟨g, h1, h2, h3.filter_mono nhdsWithin_le_nhds⟩

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

Goal state before:
pp: R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
⊢ MeromorphicNFOn (∏ᶠ (u : ℂ), canonicalFactor R u ^ F u) (ball 0 R)

Tactic:
by
  refine meromorphicNFOn_finprod (fun w ↦ ?_) fun z hz a ha b hb ↦ ?_
  · by_cases hw : w ∈ ball 0 R
    · exact fun _ _ ↦ (meromorphicNFOn_canonicalFactor hw).zpow (by trivial)
    · simp only [hw, not_false_eq_true, locallyFinsuppWithin.apply_eq_zero_of_notMem, zpow_zero]
      exact analyticOnNhd_const.meromorphicNFOn
  · have ⟨h₂a, h₂b⟩ : a ∈ ball 0 R ∧ b ∈ ball 0 R := by constructor <;> (by_contra; aesop)
    grind [eq_zero_of_zpow_eq_zero hb, eq_zero_of_zpow_eq_zero ha,
      canonicalFactor_eq_zero_iff h₂b hz, canonicalFactor_eq_zero_iff h₂a hz]

Goal state after:
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
⊢ a ∈ U → f a = ((∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u) • g) a

Tactic:
h₄a

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) • g) 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 ≠ ⊤
⊢ ∃ g, CanonicalDecomp f g R

Tactic:
by_cases hR : R ≤ 0

Goal state after:
case pos
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
⊢ ∃ g, CanonicalDecomp f g R

case neg
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
⊢ ∃ g, CanonicalDecomp f g R
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 g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
t₁ : (support fun u x ↦ ↑(D u) * log ‖x - u‖) = D.support
h₃f : D.support.Finite
z : 𝕜
hz : f z = ((∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g) z
h₂z : D z = 0
h₃z : z ∈ U
this : ∀ x ∈ h₃f.toFinset, ‖z - x‖ ^ D x ≠ 0
⊢ ∑ i ∈ h₃f.toFinset, log (‖z - i‖ ^ D i) + log ‖g z‖ =
    ((∑ i ∈ h₃f.toFinset, fun x ↦ ↑(D i) * log ‖x - i‖) + fun x ↦ log ‖g x‖) z

Tactic:
simp [log_zpow]

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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x ≠ meromorphicOrderAt f₂ x
⊢ meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)

Tactic:
rcases lt_or_lt_iff_ne.mpr h with h | h

Goal state after:
case inl
𝕜 : 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)

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)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
hn : IsEmpty n
⊢ toGL g ∈ Subgroup.center (GL n R) ↔ g ∈ Subgroup.center (SpecialLinearGroup n R)

Tactic:
simp [Subgroup.center_eq_top]

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

Goal state before:
pp: a : Circle
h : rotation a = conjLIE
h1 : ↑a = 1
hI : ↑a = -1
⊢ False

Tactic:
h1,

Goal state after:
a : Circle
h : rotation a = conjLIE
h1 : ↑a = 1
hI : 1 = -1
⊢ False
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
⊢ (meromorphicOrderAt g x).untop₀ = (meromorphicOrderAt f x).untop₀

Tactic:
meromorphicOrderAt_congr η₀,

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
⊢ (meromorphicOrderAt g x).untop₀ =
    (meromorphicOrderAt ((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g) x).untop₀
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 ⋯ ⋯
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 := ⋯ } ≍ γ

Tactic:
rw [eq]; exact γ.cast_heq ..

Goal state after:
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
η₀ : ∀ x ∈ t₁, ‖w - x‖ ^ (-divisor f S₀R) x ≠ 0
x : ℂ
hx : x ∈ t₂
h₁x : x ∈ ball 0 R
⊢ canonicalFactor R x w ≠ 0

Tactic:
refine canonicalFactor_ne_zero h₁x h₁w fun _ ↦ ?_

Goal state after:
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
η₀ : ∀ x ∈ t₁, ‖w - x‖ ^ (-divisor f S₀R) x ≠ 0
x : ℂ
hx : x ∈ t₂
h₁x : x ∈ ball 0 R
x✝ : w = x
⊢ False
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hB : ‖f z‖ ≤ B
hset : z ∈ verticalClosedStrip 0 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ max 1 ((ε + sSupNormIm f 1) ^ (-1))

Tactic:
by_cases hM1_one : 1 ≤ ε + sSupNormIm f 1

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hB : ‖f z‖ ≤ B
hset : z ∈ verticalClosedStrip 0 1
hM1_one : 1 ≤ ε + sSupNormIm f 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ max 1 ((ε + sSupNormIm f 1) ^ (-1))

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hB : ‖f z‖ ≤ B
hset : z ∈ verticalClosedStrip 0 1
hM1_one : ¬1 ≤ ε + sSupNormIm f 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ max 1 ((ε + sSupNormIm f 1) ^ (-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
⊢ MulOpposite.unop ((hp.fundamentalGroupToMulOpposite e) γ) • ↑e = ↑(⋯.monodromy γ e)

Tactic:
by
  simp [fundamentalGroupToMulOpposite, fiberEquivGroup_smul_self]

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)} (∂_{m (last n.succ)} f)) = ∂_{init m 0} (∂^{tail (init m)} (∂_{m (last (n + 1))} f))

Tactic:
hmzero,

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)) = ∂_{m 0} (∂^{tail (init m)} (∂_{m (last (n + 1))} f))
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: R : Type u_4
V : Type u_5
E : Type u_6
inst✝² : LineDeriv V E E
n : ℕ
m : Fin n → V
inst✝¹ : SMul R E
inst✝ : LineDerivSMul R V E E
r : R
x : E
⊢ ∂^{m} (r • x) = r • ∂^{m} x

Tactic:
by
  induction n with
  | zero =>
    simp
  | succ n IH =>
    simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_smul]

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

Goal state before:
pp: case neg
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 : ℝ
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 : ℝ
hzR : |z.re| < R
hR : ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C
hR₀ : 0 < R
hgd : Differentiable ℂ (g ε)
hd : DiffContOnCl ℂ (fun w ↦ g ε w • f w) (Ioo (-R) R ×ℂ Ioo (a - b) (a + b))
w : ℂ
hw : w ∈ Icc (-R) R ×ℂ {a - b, a + b} ∪ {-R, R} ×ℂ Icc (a - b) (a + b)
him : ¬(w.im = a - b ∨ w.im = a + b)
⊢ ‖g ε w • f w‖ ≤ C

Tactic:
· replace hw : w ∈ {-R, R} ×ℂ Icc (a - b) (a + b) := hw.resolve_left fun h ↦ him h.2
      have hw' := eq_endpoints_or_mem_Ioo_of_mem_Icc hw.2; rw [← or_assoc] at hw'
      exact hR _ ((abs_eq hR₀.le).2 hw.1.symm) (hw'.resolve_left him)

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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
e : ℝ
f : ℝ → F
⊢ Δ f e = iteratedDeriv 2 f e

Tactic:
← laplacianWithin_univ,

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
e : ℝ
f : ℝ → F
⊢ (Δ[Set.univ] f) e = iteratedDeriv 2 f e
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
⊢ z.wedgeIntegral w f - (w - z) • f z = I₁ + I • I₂ - (↑(w - z).re + ↑(w - z).im * I) • f z

Tactic:
by congr; rw [re_add_im]

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

Goal state before:
pp: f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
⊢ ∃ F, AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun z ↦ (F z).re) f (ball z R)

Tactic:
by_cases hR : R ≤ 0

Goal state after:
case pos
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : R ≤ 0
⊢ ∃ F, AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun z ↦ (F z).re) f (ball z R)

case neg
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
⊢ ∃ F, AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun z ↦ (F z).re) f (ball z R)
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case inr.refine_1.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ (f ∘ cexp) =O[comap re atBot ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))] fun z ↦ expR (max B 0 * expR (c * |z.re|))

Tactic:
have hc : ContinuousWithinAt f (Ioi 0 ×ℂ Ioi 0) 0 := by
        refine (hd.continuousOn _ ?_).mono subset_closure
        simp [closure_reProdIm, mem_reProdIm]
      refine ((hc.tendsto.comp <| tendsto_exp_comap_re_atBot.inf H.tendsto).isBigO_one ℝ).trans
        (isBigO_of_le _ fun w => ?_)
      rw [norm_one, Real.norm_of_nonneg (Real.exp_pos _).le, Real.one_le_exp_iff]
      positivity

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

Goal state before:
pp: F✝ : Type u_1
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
inst✝ : CompleteSpace F✝
f : ℂ → F✝
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F✝
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + |R|) ⊆ {x | HarmonicAt (⇑g ∘ f) x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + |R|))
h₂F : Set.EqOn (fun z ↦ (F z).re) (⇑g ∘ f) (ball c (e + |R|))
h₃F : DifferentiableOn ℂ F (closure (ball c |R|))
h₄F : Set.EqOn (⇑Complex.reCLM ∘ F) (⇑g ∘ f) (sphere c |R|)
⊢ c ∈ ball c (e + |R|)

Tactic:
simp [mem_ball, dist_self, add_pos_of_pos_of_nonneg h₁e (abs_nonneg R)]

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

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
hR : ¬R = 0
x : ℂ
hx : x ∈ {z | ‖z - c‖ ∈ Set.Ioc 0 |R|}
⊢ x ∈ closure (ball c |R|)

Tactic:
rw [closure_ball _ (by aesop), mem_closedBall_iff_norm]

Goal state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
hR : ¬R = 0
x : ℂ
hx : x ∈ {z | ‖z - c‖ ∈ Set.Ioc 0 |R|}
⊢ ‖x - c‖ ≤ |R|
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
hx' : x = 0
⊢ ↑0 = x

Tactic:
by exact_mod_cast hx'.symm

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

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
hx' : x = 1
⊢ ↑1 = x

Tactic:
by exact_mod_cast hx'.symm

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ HasDerivAt (fun x ↦ x * log x) (log x + 1) x

Tactic:
← deriv_mul_log hx,

Goal state after:
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt (fun x ↦ x * log x) (deriv (fun x ↦ x * log x) x) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ sinc x ≤ |x|⁻¹

Tactic:
sinc_of_ne_zero hx

Goal state after:
x : ℝ
hx : x ≠ 0
⊢ sin x / x ≤ |x|⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case neg.inr.refine_1
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
⊢ AEStronglyMeasurable (fun x ↦ ↑x ^ r) (μ.restrict (Ι a b))

pp: case neg.inr.refine_2
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
⊢ IntervalIntegrable (fun t ↦ ‖↑t ^ r‖) μ a b

Tactic:
· refine (measurable_of_continuousOn_compl_singleton (0 : ℝ) ?_).aestronglyMeasurable
    exact continuousOn_of_forall_continuousAt fun x hx =>
      Complex.continuousAt_ofReal_cpow_const x r (Or.inr hx)

Goal state after:
case neg.inr.refine_2
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
⊢ IntervalIntegrable (fun t ↦ ‖↑t ^ r‖) μ a b
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: x : ℝ
⊢ deriv (fun x ↦ log (log x)) x = x⁻¹ / log x

Tactic:
have := not_continuousAt_log_log_neg_one
  have := not_continuousAt_log_log_zero
  have := not_continuousAt_log_log_one
  obtain (⟨_, _, _⟩ | rfl | rfl | rfl) :
      (x ≠ -1 ∧ x ≠ 0 ∧ x ≠ 1) ∨ x = -1 ∨ x = 0 ∨ x = 1 := by tauto
  · simp_all
  all_goals rw [deriv_zero_of_not_differentiableAt (mt continuousAt ‹_›)]; simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = (↑b ^ (r + 1) - ↑a ^ (r + 1)) / (r + 1)

Tactic:
sub_div

Goal state after:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

Goal state before:
pp: ⊢ ∫ (x : ℝ) in 0..π / 2, log (sin x) = ∫ (x : ℝ) in 0..π / 2, log (sin (2 * x)) - log 2 - log (cos x)

Tactic:
apply intervalIntegral.integral_congr_codiscreteWithin

Goal state after:
⊢ (fun x ↦ log (sin x)) =ᶠ[codiscreteWithin (Ι 0 (π / 2))] fun x ↦ log (sin (2 * x)) - log 2 - log (cos x)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)

Tactic:
have h' : -1 < (r : ℂ).re ∨ (r : ℂ) ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]] := by
    cases h
    · left; rwa [Complex.ofReal_re]
    · right; rwa [← Complex.ofReal_one, ← Complex.ofReal_neg, Ne, Complex.ofReal_inj]
  have :
    (∫ x in a..b, (x : ℂ) ^ (r : ℂ)) = ((b : ℂ) ^ (r + 1 : ℂ) - (a : ℂ) ^ (r + 1 : ℂ)) / (r + 1) :=
    integral_cpow h'
  apply_fun Complex.re at this; convert! this
  · simp_rw [intervalIntegral_eq_integral_uIoc, Complex.real_smul, Complex.re_ofReal_mul, rpow_def,
      ← RCLike.re_eq_complex_re, smul_eq_mul]
    rw [integral_re]
    refine intervalIntegrable_iff.mp ?_
    rcases h' with h' | h'
    · exact intervalIntegrable_cpow' h'
    · exact intervalIntegrable_cpow (Or.inr h'.2)
  · rw [(by push_cast; rfl : (r : ℂ) + 1 = ((r + 1 : ℝ) : ℂ))]
    simp_rw [div_eq_inv_mul, ← Complex.ofReal_inv, Complex.re_ofReal_mul, Complex.sub_re, rpow_def]

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z ↦ cexp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ Tendsto (fun x ↦ cexp (↑ε * ↑x) • f ↑x) atTop (𝓝 0)

Tactic:
← ofReal_mul,

Goal state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z ↦ cexp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ Tendsto (fun x ↦ cexp ↑(ε * x) • f ↑x) atTop (𝓝 0)