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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : ¬(support d).Finite
⊢ MeromorphicNFOn (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) univ

Tactic:
rw [← mulSupport d] at hd

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : ¬(Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u).Finite
⊢ MeromorphicNFOn (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) univ
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]

Goal state after:
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✝
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ a✝ • g z
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this : ∀ y ∈ Finite.toFinset h, ‖(x - y) ^ update d x 0 y‖ ≠ 0
⊢ log (∏ b ∈ Finite.toFinset h, ‖(x - b) ^ update d x 0 b‖) = ∑ᶠ (u : 𝕜), ↑(d u) * log ‖x - u‖

Tactic:
log_prod this

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this : ∀ y ∈ Finite.toFinset h, ‖(x - y) ^ update d x 0 y‖ ≠ 0
⊢ ∑ i ∈ Finite.toFinset h, log ‖(x - i) ^ update d x 0 i‖ = ∑ᶠ (u : 𝕜), ↑(d u) * log ‖x - u‖
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case neg
𝕜 : 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 = ⊤
g : 𝕜 → 𝕜'
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x

Tactic:
← WithTop.coe_untop₀_of_ne_top h,

Goal state after:
case neg
𝕜 : 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 = ⊤
g : 𝕜 → 𝕜'
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ meromorphicOrderAt (f ^ n) x = ↑n * ↑(meromorphicOrderAt f x).untop₀
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ ∀ (a : ↑I), Continuous[_, inst✝¹] fun x ↦ (Γ (x, a).2) (x, a).1

Tactic:
exact fun t ↦ (Γ t).2

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
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : ¬MeromorphicAt f₁ x
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x

Tactic:
have : ¬ (MeromorphicAt (f₁ + f₂) x) := by
      contrapose hf₁
      simpa using hf₁.sub hf₂

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
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : ¬MeromorphicAt f₁ x
this : ¬MeromorphicAt (f₁ + f₂) x
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
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
⊢ log (∏ x ∈ h₃f.toFinset, ‖z - x‖ ^ D x) + log ‖g z‖ =
    ((∑ i ∈ h₃f.toFinset, fun x ↦ ↑(D i) * log ‖x - i‖) + fun x ↦ log ‖g x‖) z

Tactic:
log_prod this

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

Tactic:
by
  by_cases hf₁ : MeromorphicAt f₁ x; swap
  · have : ¬ (MeromorphicAt (f₁ + f₂) x) := by
      contrapose hf₁
      simpa using hf₁.sub hf₂
    simp [this, hf₁]
  -- Trivial case: f₂ vanishes identically around z₀
  by_cases h₁f₂ : meromorphicOrderAt f₂ x = ⊤
  · rw [meromorphicOrderAt_congr]
    filter_upwards [meromorphicOrderAt_eq_top_iff.1 h₁f₂]
    simp
  -- General case
  lift meromorphicOrderAt f₂ x to ℤ using h₁f₂ with n₂ hn₂
  lift meromorphicOrderAt f₁ x to ℤ using h.ne_top with n₁ hn₁
  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (meromorphicOrderAt_eq_int_iff hf₁).1 hn₁.symm
  obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (meromorphicOrderAt_eq_int_iff hf₂).1 hn₂.symm
  rw [meromorphicOrderAt_eq_int_iff (hf₁.add hf₂)]
  refine ⟨g₁ + (· - x) ^ (n₂ - n₁) • g₂, ?_, ?_, ?_⟩
  · apply h₁g₁.add (AnalyticAt.smul _ h₁g₂)
    apply AnalyticAt.zpow_nonneg (by fun_prop)
      (sub_nonneg.2 (le_of_lt (WithTop.coe_lt_coe.1 h)))
  · simpa [zero_zpow _ <| sub_ne_zero.mpr (WithTop.coe_lt_coe.1 h).ne']
  · filter_upwards [h₃g₁, h₃g₂, self_mem_nhdsWithin]
    simp_all [smul_add, ← smul_assoc, ← zpow_add', sub_ne_zero]

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:
· rw [meromorphicOrderAt_eq_top_iff, not_eventually]
          apply Filter.Eventually.frequently
          rw [eventually_nhdsWithin_iff, eventually_nhds_iff]
          use t' \ {z.1}, fun y h₁y h₂y ↦ h₁t' y h₁y.1 h₁y.2, h₂t'.sdiff isClosed_singleton, hw,
            mem_singleton_iff.not.2 (Subtype.coe_ne_coe.mpr h₁w)

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

Goal state before:
pp: ⊢ 0.36787944116 < rexp (-1)

Tactic:
rw [exp_neg, lt_inv_comm₀ _ (exp_pos _)]

Goal state after:
⊢ rexp 1 < 0.36787944116⁻¹

⊢ 0 < 0.36787944116
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
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
H' : ↑I × A → E
x✝¹ : (∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)) ∧ p ∘ H' = ⇑H ∧ ∀ (a : A), H' (0, a) = f a
H'_cont : ∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)
H'_lifts : p ∘ H' = ⇑H
H'_0 : ∀ (a : A), H' (0, a) = f a
x✝ : ↑I × A
t : ↑I
a : A
⊢ H' (t, a) = (cov.liftHomotopy H f H_0) (t, a)

Tactic:
apply congr_fun ((cov.eq_liftPath_iff _).mpr ⟨H'_cont a, _, H'_0 a⟩) t

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
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
H' : ↑I × A → E
x✝¹ : (∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)) ∧ p ∘ H' = ⇑H ∧ ∀ (a : A), H' (0, a) = f a
H'_cont : ∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)
H'_lifts : p ∘ H' = ⇑H
H'_0 : ∀ (a : A), H' (0, a) = f a
x✝ : ↑I × A
t : ↑I
a : A
⊢ (p ∘ fun x ↦ H' (x, a)) = ⇑(H.comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const ↑I (t, a).2)))
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst✝ : PreconnectedSpace A
f₀' f₁' : C(A, E)
he : ∃ a ∈ S, f₀' a = f₁' a
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
t : ↑I
a : A
ha : a ∈ S
⊢ (cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const ↑I (t, a).2))) (f₀' (t, a).2) ⋯) 0 = f₀' a

Tactic:
apply cov.liftPath_zero

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

Goal state before:
pp: case refine_2.mk
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
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
pγγ' : Path a₀ a₀ := pγ.trans pγ'.symm
w✝ : FundamentalGroup E e₀
pΓΓ' : Path { as := e₀ }.as { as := e₀ }.as
eq :
  (Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid { as := e₀ }.as { as := e₀ }.as)) pΓΓ')
          { toFun := p, continuous_toFun := ⋯ }).cast
      ⋯ ⋯ =
    Path.Homotopic.Quotient.mk (pγγ'.map ⋯)
⊢ cov.monodromy (Path.Homotopic.Quotient.mk (pγγ'.map ⋯)) ⟨e₀, he⟩ = id ⟨e₀, he⟩

Tactic:
exact eq ▸ Subtype.ext congr($(cov.monodromy_map <| .mk _))

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
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
e₀ : E
f : C(A, ↑s)
he : p e₀ = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a₀
hs : ∀ (a : A), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a ∈ s
⊢ ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f)

Tactic:
lift e₀ to p ⁻¹' s using by rw [Set.mem_preimage, he]; apply hs

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
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : C(A, ↑s)
hs : ∀ (a : A), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a ∈ s
e₀ : { x // x ∈ p ⁻¹' s }
he : p ↑e₀ = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a₀
⊢ ∃! F, F a₀ = ↑e₀ ∧ p ∘ ⇑F = ⇑({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f)
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
y : ℂ
yRe : y.re ∈ s
yIm : y.im = z.im
⊢ y ∈ ball z r₁

Tactic:
mem_ball,

Goal state after:
c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
y : ℂ
yRe : y.re ∈ s
yIm : y.im = z.im
⊢ dist y z < r₁
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 = l ∧ f x = e) → ∃ x, x.re = 0 ∧ f (↑l + x * (↑u - ↑l)) = e

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

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

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

Tactic:
apply DiffContOnCl.smul_const

Goal state after:
case hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl ℂ (fun x ↦ x) (verticalStrip 0 1)
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: case mp
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
h : HarmonicAt (⇑l ∘ f) x
⊢ HarmonicAt f x

Tactic:
simpa [Function.comp_def] using h.comp_CLM l.symm.toContinuousLinearMap

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

Goal state before:
pp: case neg
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
⊢ ∃ F, AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun z ↦ (F z).re) f (ball z R)

Tactic:
have hg : DifferentiableOn ℂ g (ball z R) :=
    fun x hx ↦ (HarmonicAt.differentiableAt_complex_partial (hf x hx)).differentiableWithinAt

Goal state after:
case neg
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : DifferentiableOn ℂ g (ball z R)
⊢ ∃ F, AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun z ↦ (F z).re) f (ball z R)
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|
⊢ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, |R|), (z - w)⁻¹ • f z = f w

Tactic:
rw [circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw h₁f h₂f]
    match_scalars
    simp [field]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η x : ℝ
⊢ (fun θ ↦ f (circleMap c R θ)) (x + 2 * π) = (fun θ ↦ f (circleMap c R θ)) x

Tactic:
simp [periodic_circleMap c R x]

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

Goal state before:
pp: f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
⊢ AnalyticAt ℝ f x

Tactic:
obtain ⟨ε, h₁ε, h₂ε⟩ := isOpen_iff.1 (isOpen_setOfPred_harmonicAt (f := f)) x hf
  obtain ⟨F, h₁F, h₂F⟩ := InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq
    (fun _ hy ↦ h₂ε hy)
  rw [analyticAt_congr (Filter.eventually_of_mem (ball_mem_nhds x h₁ε) (fun y hy ↦ h₂F.symm hy))]
  exact (reCLM.analyticAt (F x)).comp (h₁F x (mem_ball_self h₁ε)).restrictScalars

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: case pos
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun x ↦ Real.log ‖f x‖) = 2⁻¹ • Real.log ∘ ⇑normSq ∘ f
h₃f : f z ∈ slitPlane
⊢ HarmonicAt (Real.log ∘ ⇑normSq ∘ f) z

Tactic:
exact analyticAt_harmonicAt_log_normSq h₁f h₂f h₃f

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

Goal state before:
pp: a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn (fun x ↦ x ^ r) (Ι 0 c) volume

Tactic:
uIoc_of_le hc

Goal state after:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn (fun x ↦ x ^ r) (Ioc 0 c) volume
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x ↦ x ^ r) volume 0 c

Tactic:
· rw [IntervalIntegrable.iff_comp_neg, neg_zero]
    have m := (this (-c) (by linarith)).smul (cos (r * π))
    rw [intervalIntegrable_iff] at m ⊢
    refine m.congr_fun ?_ measurableSet_Ioc; intro x hx
    rw [uIoc_of_le (by linarith : 0 ≤ -c)] at hx
    simp only [Pi.smul_apply, smul_eq_mul, log_neg_eq_log, mul_comm,
      rpow_def_of_pos hx.1, rpow_def_of_neg (by linarith [hx.1] : -x < 0)]

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

Goal state before:
pp: case hst
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ι 0 c
⊢ (fun x ↦ x ^ r.re) x = (fun t ↦ ‖↑t ^ r‖) x

Tactic:
uIoc_of_le hc

Goal state after:
case hst
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
⊢ (fun x ↦ x ^ r.re) x = (fun t ↦ ‖↑t ^ r‖) x
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ι 0 c
⊢ ContinuousAt (fun x ↦ ↑x ^ r) x

Tactic:
uIoc_of_le hc

Goal state after:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
⊢ ContinuousAt (fun x ↦ ↑x ^ r) x
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
z : ℂ
hz : z ∈ ball (↑x₀) (dist 0 ↑x₀)
⊢ z ∈ {z | 0 < z.re}

Tactic:
mem_ball,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
z : ℂ
hz : dist z ↑x₀ < dist 0 ↑x₀
⊢ z ∈ {z | 0 < z.re}
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: case neg
x : ℝ
h : log x < 0
⊢ max 0 (log x) - max 0 (-log x) = log x

Tactic:
· simp [neg_nonneg.1 (Left.nonneg_neg_iff.2 h.le)]

Goal state after:
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]

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

Goal state before:
pp: a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ι a b, |x - a| ^ n = ∫ (x : ℝ) in a..b, |x - a| ^ n

Tactic:
by
        rw [uIoc_of_le hab, ← integral_of_le hab]

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

Goal state before:
pp: case e'_2.e_f
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
x : ℝ
⊢ ↑x * ↑((1 + x ^ 2) ^ t) = ↑x * (1 + ↑x ^ 2) ^ ↑t

Tactic:
this x t

Goal state after:
case e'_2.e_f
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
x : ℝ
⊢ ↑x * (1 + ↑x ^ 2) ^ ↑t = ↑x * (1 + ↑x ^ 2) ^ ↑t
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case neg
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
⊢ log⁺ (R⁻¹ * ‖c - a‖) = 0

Tactic:
posLog_eq_zero_iff,

Goal state after:
case neg
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
⊢ |R⁻¹ * ‖c - a‖| ≤ 1
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
z : E
hz : z ∈ sphere 0 1
t : ℂ
ht : t ∈ ball 0 r
⊢ AnalyticAt ℂ (ray z) t

Tactic:
· exact analyticAt_const.add
        ((ContinuousLinearMap.smulRight (ContinuousLinearMap.id ℂ ℂ) z).analyticAt t)

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * ↑π * I / ↑h)) z
diff_ne : q * (2 * ↑π * I / ↑h) ≠ 0
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Tactic:
let L := (qdiff.localInverse (𝕢 h) _ z) diff_ne

Goal state after:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * ↑π * I / ↑h)) z
diff_ne : q * (2 * ↑π * I / ↑h) ≠ 0
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * ↑π * I / ↑h)) z qdiff diff_ne
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_bd : I∞.BoundedAtFilter f
q : ℂ
hq : q ∈ {0}ᶜ
⊢ (f ∘ invQParam h) q = cuspFunction h f q

Tactic:
cuspFunction_eq_of_nonzero _ _ hq,

Goal state after:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_bd : I∞.BoundedAtFilter f
q : ℂ
hq : q ∈ {0}ᶜ
⊢ (f ∘ invQParam h) q = f (invQParam h q)
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: p : ℂ[X]
h : ¬∃ x, C x = p
x : ℂ
eq : ∀ (z : ℂ), eval z p = x
⊢ ∀ (r : ℂ), eval r (C x) = eval r p

Tactic:
by simpa [eq_comm (a := x)]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (Metric.eball c r)
z : ℂ
hz : z ∈ Metric.eball c r
⊢ HasSum (fun n ↦ (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Tactic:
obtain ⟨r', hzr', hr'⟩ := exists_between (Metric.mem_eball'.mp hz)
  lift r' to NNReal using ne_top_of_lt hr'
  rw [← Metric.mem_eball', Metric.eball_coe] at hzr'
  refine hasSum_taylorSeries_on_ball ?_ hzr'
  rw [← Metric.eball_coe]
  exact hf.mono <| Metric.eball_subset_eball hr'.le

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

Goal state before:
pp: case hf
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
z : ℂ
hz : z ∈ U
⊢ HasStrictDerivAt ?f (2 * f z) (f z)

Tactic:
simpa using hasStrictDerivAt_pow 2 (f z)

Goal state after: