mathlib-initiative/mathlib-tactics huggingface dataset:
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
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ 0 • g
this : meromorphicOrderAt f x = ↑n
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
h₀ : AnalyticAt 𝕜 (Classical.choose ⋯) x
h₁ : Classical.choose ⋯ x ≠ 0
h₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ 0 • Classical.choose ⋯ z
⊢ g =ᶠ[𝓝[≠] x] Classical.choose ⋯

Tactic:
simp only [zpow_zero, one_smul, ne_eq] at h₃g h₂

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
this : meromorphicOrderAt f x = ↑n
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
h₀ : AnalyticAt 𝕜 (Classical.choose ⋯) x
h₁ : Classical.choose ⋯ x ≠ 0
h₃g : f =ᶠ[𝓝 x] g
h₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = Classical.choose ⋯ z
⊢ g =ᶠ[𝓝[≠] x] Classical.choose ⋯
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
n : ℤ
h'o : meromorphicOrderAt f x = ↑n
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ 0 ≤ n

Tactic:
simpa [h'o] using ho.le

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
this : 0 ≤ meromorphicOrderAt f x
n : ℕ
ho : meromorphicOrderAt f x = ↑↑n
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ ↑n • g z
z : 𝕜
hz : f z = (z - x) ^ ↑n • g z
⊢ (z - x) ^ n • g z = f z

Tactic:
by simpa using hz.symm

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 =
    (∏ i ∈ η₀.toFinset,
        canonicalFactor R i a ^ (-(divisor f (ball 0 R)) i) • canonicalFactor R i a ^ (divisor f (ball 0 R)) i) •
      f a

Tactic:
Finset.prod_eq_one,

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 = 1 • f a

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
⊢ ∀ x ∈ η₀.toFinset,
    canonicalFactor R x a ^ (-(divisor f (ball 0 R)) x) • canonicalFactor R x a ^ (divisor f (ball 0 R)) x = 1
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: case h.refine_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
h₂ : f.trans (rotation a).symm = conjLIE
⊢ f = conjLIE.trans (rotation a)

Tactic:
exact eq_mul_of_inv_mul_eq h₂

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}
x✝¹ : Set ↑U
x✝ : ↑U
| meromorphicOrderAt f ↑x✝ = ⊤

Tactic:
rw [meromorphicOrderAt_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}
x✝¹ : Set ↑U
x✝ : ↑U
| ∃ t, (∀ y ∈ t, y ∈ {↑x✝}ᶜ → f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x✝ ∈ t
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case η₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
⊢ Preperfect (closedBall 0 R)

Tactic:
case η₁ =>
        rw [← closure_ball _ hR.ne']
        exact isOpen_ball.perfect_closure.2

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

Goal state before:
pp: ⊢ ↑3 ≤ rexp 1 + 1 / 2

Tactic:
grw [← exp_one_gt_d9]

Goal state after:
⊢ ↑3 ≤ 2.7182818283 + 1 / 2
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
e₀ e₁ : E
γ₀ γ₁ : Path e₀ e₁
⊢ (γ₀.map ⋯).Homotopic (γ₁.map ⋯) → γ₀.Homotopic γ₁

Tactic:
exact (cov.homotopicRel_iff_comp ⟨0, .inl rfl, γ₀.source.trans γ₁.source.symm⟩).mpr

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
x : ℂ
h₃x : (divisor f (ball 0 R)) x = 0
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ (divisor f (ball 0 R)) x =
    canonicalFactor R x w ^ (divisor f (ball 0 R)) x

Tactic:
simp [h₃x]

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
cov : IsCoveringMap p
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
⊢ ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f

Tactic:
refine cov.isLocalHomeomorph.existsUnique_continuousMap_lifts f a₀ e₀ he (fun γ γ_0 ↦ ?_)
    fun γ γ' Γ Γ' γ_0 γ'_0 Γ_0 Γ'_0 Γ_lifts Γ'_lifts γγ'1 ↦ ?_
  · simpa [and_comm] using cov.exists_path_lifts (f.comp γ) e₀ (by simp [γ_0, he])
  let pγ : Path a₀ (γ 1) := ⟨γ, γ_0, rfl⟩
  let pγ' : Path a₀ (γ 1) := ⟨γ', γ'_0, γγ'1.symm⟩
  convert!
    cov.liftPath_apply_one_eq_of_homotopicRel
      (ContinuousMap.HomotopicRel.comp_continuousMap (SimplyConnectedSpace.paths_homotopic pγ pγ')
        f)
      e₀ (by simp [he]) (by simp [he]) <;>
    rw [eq_liftPath_iff']
  exacts [⟨Γ_lifts, Γ_0⟩, ⟨Γ'_lifts, Γ'_0⟩]

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

Tactic:
add_sub_sub_cancel,

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

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz0 : z.re = 0
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1

Tactic:
simp only [hz0, zero_sub, Real.rpow_neg_one, neg_zero, Real.rpow_zero, mul_one,
      inv_mul_le_iff₀ (sSupNormIm_eps_pos f hε 0)]

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz0 : z.re = 0
⊢ ‖f z‖ ≤ ε + sSupNormIm f 0
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
        I • fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) I) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) I) x)
      I =
    I •
      (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
          I • fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) I) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) I) x)
        1

Tactic:
simp only [ContinuousLinearMap.fderiv, sub_apply, ContinuousLinearMap.comp_apply, ofRealCLM_apply,
    smul_apply, smul_eq_mul]

Goal state after:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ ↑((fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x) I) - I * ↑((fderiv ℝ (fun x ↦ (fderiv ℝ f x) I) x) I) =
    I * (↑((fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x) 1) - I * ↑((fderiv ℝ (fun x ↦ (fderiv ℝ f x) I) x) 1))
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
⊢ a ≠ b

Tactic:
intro hab

Goal state after:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
hab : a = b
⊢ False
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun x ↦ c) (Ioo r R)
⊢ Ioc r R ∈ 𝓝[<] R

Tactic:
mem_nhdsLT_iff_exists_Ioo_subset

Goal state after:
f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun x ↦ c) (Ioo r R)
⊢ ∃ l ∈ Iio R, Ioo l R ⊆ Ioc r R
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:

Tactic:
Real.log ∘ normSq ∘ g
    _ =ᶠ[𝓝 z] reCLM ∘ ofRealCLM ∘ Real.log ∘ normSq ∘ g := by aesop
    _ =ᶠ[𝓝 z] reCLM ∘ log ∘ ((conjCLE ∘ g) * g) := by
      filter_upwards with x
      simp only [Function.comp_apply, ofRealCLM_apply, Pi.mul_apply, conjCLE_apply]
      rw [ofReal_log, normSq_eq_conj_mul_self]
      exact normSq_nonneg (g x)
    _ =ᶠ[𝓝 z] reCLM ∘ (log ∘ conjCLE ∘ g + log ∘ g) := by
      filter_upwards [t₀] with x hx
      simp only [Function.comp_apply, Pi.mul_apply, conjCLE_apply, Pi.add_apply]
      congr
      rw [Complex.log_mul_eq_add_log_iff _ hx.2, Complex.arg_conj]
      · simp [Complex.slitPlane_arg_ne_pi hx.1, Real.pi_pos, Real.pi_nonneg]
      · simpa [ne_eq, map_eq_zero] using hx.2
    _ =ᶠ[𝓝 z] ⇑reCLM ∘ (⇑conjCLE ∘ log ∘ g + log ∘ g) := by
      apply Filter.eventuallyEq_iff_exists_mem.2
      use g ⁻¹' (Complex.slitPlane ∩ {0}ᶜ), t₀
      intro x hx
      simp only [Function.comp_apply, Pi.add_apply, conjCLE_apply]
      congr 1
      rw [← Complex.log_conj]
      simp [Complex.slitPlane_arg_ne_pi hx.1]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 0 < deriv^[2] (fun x ↦ x * log x) x

Tactic:
deriv2_mul_log

Goal state after:
x : ℝ
hx : 0 < x
⊢ 0 < x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: case mp
x : ℝ
h : DifferentiableAt ℝ (fun x ↦ -x * log x) x
⊢ x ≠ 0

Tactic:
eq0

Goal state after:
case mp
x : ℝ
h : DifferentiableAt ℝ (fun x ↦ -x * log x) x
eq0 : x = 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case e'_9
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioo 0 c
⊢ x ^ r = (r + 1) * x ^ (r + 1 - 1) / (r + 1)

Tactic:
simp [(by linarith : r + 1 ≠ 0)]

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
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'
hfc : ContinuousOn (fun x ↦ f ↑x) (Ici 0)
x₀ : ℝ
hx₀ : 0 ≤ x₀
hne : f ↑x₀ ≠ 0
⊢ ‖0‖ < ‖f ↑x₀‖

Tactic:
rwa [norm_zero, norm_pos_iff]

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

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

Tactic:
rw [← IntervalIntegrable.intervalIntegrable_norm_iff]

Goal state after:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun t ↦ ‖↑t ^ r‖) volume 0 c

a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ AEStronglyMeasurable (fun x ↦ ↑x ^ r) (volume.restrict (Ι 0 c))
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case inr
a b : ℝ
r : ℂ
h : -1 < r.re
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)).const_mul (Complex.exp (π * Complex.I * r))
    rw [intervalIntegrable_iff, uIoc_of_le (by linarith : 0 ≤ -c)] at m ⊢
    refine m.congr_fun (fun x hx => ?_) measurableSet_Ioc
    #adaptation_note /-- 2026-05-17(kmill) added `dsimp only` because a slightly different
    instantiation order leads to a term with a beta redex.
    https://github.com/leanprover/lean4/pull/13762
    This will be removed once app elaboration itself does beta reduction. -/
    dsimp only
    have : -x ≤ 0 := by linarith [hx.1]
    rw [Complex.ofReal_cpow_of_nonpos this, mul_comm]
    simp

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

Goal state before:
pp: a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun x ↦ c * ↑x) c x

Tactic:
simpa only [mul_one] using! ((hasDerivAt_id (x : ℂ)).const_mul _).comp_ofReal

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * ↑π * I / ↑h)) z
diff_ne : q * (2 * ↑π * I / ↑h) ≠ 0
hol_z :
  DifferentiableAt ℂ f
    (HasStrictFDerivAt.localInverse (𝕢 h)
      ((ContinuousLinearEquiv.unitsEquivAut ℂ) (Units.mk0 (q * (2 * ↑π * I / ↑h)) diff_ne)) z ⋯ (𝕢 h z))
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * ↑π * I / ↑h)) z qdiff diff_ne
diff_L : DifferentiableAt ℂ L q
hL : 𝕢 h ∘ L =ᶠ[𝓝 q] id
hF : f ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id
this : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Tactic:
exact (hol_z.comp q diff_L).congr_of_eventuallyEq hF.symm

Goal state after:
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
⊢ MonotoneOn f (s ∪ t)

Tactic:
by
  have A : ∀ x, x ∈ s ∪ t → x ≤ c → x ∈ s := by
    intro x hx hxc
    cases hx
    · assumption
    rcases eq_or_lt_of_le hxc with (rfl | h'x)
    · exact hs.1
    exact (lt_irrefl _ (h'x.trans_le (ht.2 (by assumption)))).elim
  have B : ∀ x, x ∈ s ∪ t → c ≤ x → x ∈ t := by
    intro x hx hxc
    match hx with
    | Or.inr hx => exact hx
    | Or.inl hx =>
      rcases eq_or_lt_of_le hxc with (rfl | h'x)
      · exact ht.1
      exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim
  intro x hx y hy hxy
  rcases lt_or_ge x c with (hxc | hcx)
  · have xs : x ∈ s := A _ hx hxc.le
    rcases lt_or_ge y c with (hyc | hcy)
    · exact h₁ xs (A _ hy hyc.le) hxy
    · exact (h₁ xs hs.1 hxc.le).trans (h₂ ht.1 (B _ hy hcy) hcy)
  · have xt : x ∈ t := B _ hx hcx
    have yt : y ∈ t := B _ hy (hcx.trans hxy)
    exact h₂ xt yt hxy

Goal state after:
Module: Mathlib.Order.Interval.Set.IsoIoo

Goal state before:
pp: case refine_1
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
x : k
⊢ |x / (1 + |x|)| < 1

Tactic:
have H : 0 < 1 + |x| := (abs_nonneg x).trans_lt (lt_one_add _)

Goal state after:
case refine_1
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
x : k
H : 0 < 1 + |x|
⊢ |x / (1 + |x|)| < 1
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : I = 0
⊢ (map ℂ 𝕜)
      (↑√((‖(map 𝕜 ℂ) a‖ + ((map 𝕜 ℂ) a).re) / 2) +
        (if 0 ≤ ((map 𝕜 ℂ) a).im then 1 else -1) * ↑√((‖(map 𝕜 ℂ) a‖ - ((map 𝕜 ℂ) a).re) / 2) * Complex.I) =
    ↑√((‖a‖ + re a) / 2) + (if 0 ≤ im a then 1 else -1) * ↑√((‖a‖ - re a) / 2) * I

pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : im I = 1
⊢ (map ℂ 𝕜)
      (↑√((‖(map 𝕜 ℂ) a‖ + ((map 𝕜 ℂ) a).re) / 2) +
        (if 0 ≤ ((map 𝕜 ℂ) a).im then 1 else -1) * ↑√((‖(map 𝕜 ℂ) a‖ - ((map 𝕜 ℂ) a).re) / 2) * Complex.I) =
    ↑√((‖a‖ + re a) / 2) + (if 0 ≤ im a then 1 else -1) * ↑√((‖a‖ - re a) / 2) * I

Tactic:
· rw [← re_add_im a]
    simp [h, im_eq_zero]

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : im I = 1
⊢ (map ℂ 𝕜)
      (↑√((‖(map 𝕜 ℂ) a‖ + ((map 𝕜 ℂ) a).re) / 2) +
        (if 0 ≤ ((map 𝕜 ℂ) a).im then 1 else -1) * ↑√((‖(map 𝕜 ℂ) a‖ - ((map 𝕜 ℂ) a).re) / 2) * Complex.I) =
    ↑√((‖a‖ + re a) / 2) + (if 0 ≤ im a then 1 else -1) * ↑√((‖a‖ - re a) / 2) * I
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ sqrt (-a) = I * sqrt a

Tactic:
rw [sqrt_eq_ite, dif_pos h, RingEquiv.symm_apply_eq, map_neg,
    Complex.sqrt_neg_of_nonneg (by simpa)]

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ Complex.I * ((complexRingEquiv h) a).sqrt = (complexRingEquiv h) (I * sqrt a)
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : im I = 1
⊢ ((complexRingEquiv h) (-I)).sqrt =
    (complexRingEquiv h) ↑√2⁻¹ * (complexRingEquiv h) (1 + I) * (complexRingEquiv h) (-I)

Tactic:
simp [h, mul_assoc, add_comm, Complex.sqrt_neg_I, neg_mul, mul_add, add_mul, mul_sub,
      mul_comm Complex.I, ← sub_eq_add_neg]

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
h : (↑(↑N * -n) +ᵥ z).re = ↑(-↑N * ⌊z.re / ↑N⌋) + z.re
⊢ |z.re + ↑(-↑N * ⌊z.re / ↑N⌋)| ≤ ↑N

Tactic:
simp only [neg_mul, Int.cast_neg, Int.cast_mul, Int.cast_natCast]

Goal state after:
case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
h : (↑(↑N * -n) +ᵥ z).re = ↑(-↑N * ⌊z.re / ↑N⌋) + z.re
⊢ |z.re + -(↑N * ↑⌊z.re / ↑N⌋)| ≤ ↑N
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: case pos
w : ℂ
hw : 0 < w.im
⊢ ↑ofComplex w = { coe := w, coe_im_pos := hw }

Tactic:
exact ofComplex_apply ⟨w, hw⟩

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case zero
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : IsEmpty m
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
simp_rw [Matrix.det_isEmpty, map_one, det_one]

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l✝ + 1
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
have ⟨k⟩ := Fintype.card_pos_iff.mp (Nat.lt_of_sub_eq_succ l)

Goal state after:
case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l✝ + 1
k : m
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det