mathlib-initiative/mathlib-tactics huggingface dataset:
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
i : n
x✝ : ∃ x, (GeneralLinearGroup.scalar n) x = toGL g
r : Rˣ
hr : (GeneralLinearGroup.scalar n) r = toGL g
⊢ (diagonal fun x ↦ ↑r) = ↑g

Tactic:
simpa [Units.ext_iff] using hr

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

Goal state before:
pp: a : Circle
⊢ ((LinearMap.toMatrix basisOneI basisOneI) ↑(rotation a).toLinearEquiv).det = 1

Tactic:
toMatrix_rotation,

Goal state after:
a : Circle
⊢ (↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯)).det = 1
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
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
a : ℂ
ha : a ∉ ball 0 R
⊢ AnalyticAt ℂ (canonicalFactor R a ^ (-(divisor f (ball 0 R)) a)) x

Tactic:
simp_all only [mem_ball, dist_zero_right, not_lt,
          locallyFinsuppWithin.apply_eq_zero_of_notMem, neg_zero, zpow_zero]

Goal state after:
case neg
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
a : ℂ
ha : R ≤ ‖a‖
⊢ AnalyticAt ℂ 1 x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case h.right
𝕜 : 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'
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t') ∧ z ∈ Subtype.val ⁻¹' t'

Tactic:
exact ⟨isOpen_induced h₂t', h₃t'⟩

Goal state after:
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 = (meromorphicOrderAt f x).untop₀

Tactic:
divisor_apply D.meromorphicNFOn.meromorphicOn (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
⊢ (meromorphicOrderAt g x).untop₀ = (meromorphicOrderAt f x).untop₀
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 = ⊤}
| ∃ t ⊆ {u | meromorphicOrderAt f ↑u = ⊤}, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t

Tactic:
conv =>

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.Topology.Homotopy.Lifting

Goal state before:
pp: case pos
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y z : X
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
x✝ : ↑I
h✝ : ↑x✝ ≤ 1 / 2
⊢ p ({ toContinuousMap := cov.liftPath (↑γ) e ⋯, source' := ⋯, target' := ⋯ } ⟨2 * ↑x✝, ⋯⟩) = γ ⟨2 * ↑x✝, ⋯⟩

Tactic:
exact congr_fun (cov.liftPath_lifts γ e (γ.source.trans hpe)) _

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
⊢ {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤} ∈ codiscrete ↑U

Tactic:
rw [mem_codiscrete_subtype_iff_mem_codiscreteWithin, mem_codiscreteWithin]
  intro x hx
  rw [Filter.disjoint_principal_right]
  rcases (hf x hx).eventually_eq_zero_or_eventually_ne_zero with h₁f | h₁f
  · filter_upwards [eventually_eventually_nhdsWithin.2 h₁f] with a h₁a
    suffices ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0 by
      simp +contextual [meromorphicOrderAt_eq_top_iff, this]
    obtain rfl | hax := eq_or_ne a x
    · exact h₁a
    rw [eventually_nhdsWithin_iff, eventually_nhds_iff] at h₁a ⊢
    obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₁a
    use t \ {x}, fun y h₁y _ ↦ h₁t y h₁y.1 h₁y.2
    exact ⟨h₂t.sdiff isClosed_singleton, Set.mem_sdiff_of_mem h₃t hax⟩
  · filter_upwards [hf.eventually_analyticAt_or_mem_compl hx, h₁f] with a h₁a h'₁a
    simp only [mem_compl_iff, Set.mem_sdiff, mem_image, mem_ofPred_eq, Subtype.exists,
      exists_and_right, exists_eq_right, not_exists, not_or, not_and, not_forall, Decidable.not_not]
    rcases h₁a with h' | h'
    · simp +contextual [h'.meromorphicOrderAt_eq, h'.analyticOrderAt_eq_zero.2, h'₁a]
    · exact fun ha ↦ (h' ha).elim

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 ∈ t₂, ‖canonicalFactor R x w‖ ^ (divisor f B₀R) x ≠ 0
⊢ log (∏ x ∈ t₂, ‖canonicalFactor R x w‖ ^ (divisor f B₀R) x) + log (∏ x ∈ t₁, ‖w - x‖ ^ (-divisor f S₀R) x) +
      log ‖meromorphicTrailingCoeffAt f w‖ =
    ∑ i ∈ t₂, log (‖canonicalFactor R i w‖ ^ (divisor f B₀R) i) + ∑ i ∈ t₁, log (‖w - i‖ ^ (-divisor f S₀R) i) +
      log ‖meromorphicTrailingCoeffAt f w‖

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 ∈ t₂, ‖canonicalFactor R x w‖ ^ (divisor f B₀R) x ≠ 0
⊢ ‖meromorphicTrailingCoeffAt f w‖ ≠ 0

Tactic:
Real.log_prod η₁,

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 ∈ t₂, ‖canonicalFactor R x w‖ ^ (divisor f B₀R) x ≠ 0
⊢ ∑ i ∈ t₂, log (‖canonicalFactor R i w‖ ^ (divisor f B₀R) i) + log (∏ x ∈ t₁, ‖w - x‖ ^ (-divisor f S₀R) x) +
      log ‖meromorphicTrailingCoeffAt f w‖ =
    ∑ i ∈ t₂, log (‖canonicalFactor R i w‖ ^ (divisor f B₀R) i) + ∑ i ∈ t₁, log (‖w - i‖ ^ (-divisor f S₀R) i) +
      log ‖meromorphicTrailingCoeffAt f w‖

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 ∈ t₂, ‖canonicalFactor R x w‖ ^ (divisor f B₀R) x ≠ 0
⊢ ‖meromorphicTrailingCoeffAt f w‖ ≠ 0
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 < π / 2 / 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:
have hπb : 0 < π / 2 / b := div_pos Real.pi_div_two_pos hb

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 < π / 2 / 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
hπb : 0 < π / 2 / b
⊢ ‖f z‖ ≤ C
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case pos.inl
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h0 : sSupNormIm f 0 = 0
⊢ ¬z = 1

Tactic:
simp only [Complex.ext_iff, one_re, ne_of_lt hz.2, false_and, not_false_eq_true]

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
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
⊢ (fun x ↦ (∫ (t : ℝ) in z.re..x, f (↑t + ↑z.im * I)) - (x - z.re) • f z) =o[𝓝 z.re] fun x ↦ x - z.re

Tactic:
let r₁ := r - dist z c

Goal state after:
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
r₁ : ℝ := r - dist z c
⊢ (fun x ↦ (∫ (t : ℝ) in z.re..x, f (↑t + ↑z.im * I)) - (x - z.re) • f z) =o[𝓝 z.re] fun x ↦ x - z.re
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ (a - b)⁻¹ • ∫ (x : ℝ) in Ioc b a, f x = (-(b - a))⁻¹ • ∫ (x : ℝ) in Ioc b a, f x ∂volume

Tactic:
neg_sub

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ (a - b)⁻¹ • ∫ (x : ℝ) in Ioc b a, f x = (a - b)⁻¹ • ∫ (x : ℝ) in Ioc b a, f x ∂volume
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
| (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) = a

Tactic:
conv =>

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
θ : ℝ
| a
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: case neg
x : ℝ
hx : ¬x = 0
⊢ ContinuousAt (dslope sin 0) x

Tactic:
rw [continuousAt_dslope_of_ne hx]

Goal state after:
case neg
x : ℝ
hx : ¬x = 0
⊢ ContinuousAt sin x
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
⊢ Real.circleAverage (fun z ↦ (z / (z - w)) • f z) 0 R - Real.circleAverage (fun z ↦ (q • z / (q • z - W)) • f z) 0 R =
    f w

Tactic:
← abs_of_pos hR

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 |R|)
hw : w ∈ ball 0 |R|
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
⊢ Real.circleAverage (fun z ↦ (z / (z - w)) • f z) 0 R - Real.circleAverage (fun z ↦ (q • z / (q • z - W)) • f z) 0 R =
    f w
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hderiv.refine_2
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
⊢ r ≠ -1

Tactic:
contrapose hr; rw [hr]; ring

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

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

Tactic:
conv =>

Goal state after:
x : ℝ
| log (sin (π - x))
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

Goal state before:
pp: ⊢ sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ

Tactic:
apply analyticOnNhd_sin.preimage_zero_mem_codiscrete (x := π / 2)

Goal state after:
⊢ sin (π / 2) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
| HasDerivAt (fun y ↦ Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x

Tactic:
conv =>

Goal state after:
case f
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
| fun y ↦ Complex.exp (c * ↑y) / c

case f'
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
| Complex.exp (c * ↑x)

case x
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
| x
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hderiv
b : ℝ
ht : 0 < b
s : ℝ
⊢ s ∈ Set.Ioo 0 b → HasDerivAt (fun x ↦ x * log x - x) (log s) s

Tactic:
⟨hs, _ ⟩

Goal state after:
case hderiv
b : ℝ
ht : 0 < b
s : ℝ
hs : 0 < s
right✝ : s < b
⊢ HasDerivAt (fun x ↦ x * log x - x) (log s) s
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: b : ℝ
h : b < 0
| ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
conv =>

Goal state after:
b : ℝ
h : b < 0
t : ℝ
| log (-t)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case inl
a : ℂ
h : 1 < ‖a‖
⊢ circleAverage (fun x ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖

Tactic:
rw [circleAverage_log_norm_sub_const₂ h]

Goal state after:
case inl
a : ℂ
h : 1 < ‖a‖
⊢ log ‖a‖ = log⁺ ‖a‖
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z ↦ ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
h5 : ‖f z₀ - v‖ < ε / 2
z : ℂ
hz1 : z ∈ ball z₀ r
hz2 : IsLocalMin (fun z ↦ ‖f z - v‖) z
h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z ↦ f z - v) y
key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v
h7 : ∃ᶠ (w : ℂ) in 𝓝[≠] z, f w = f z
h8 : IsPreconnected (ball z₀ r)
h9 : EqOn f (fun x ↦ f z) (ball z₀ r)
⊢ False

Tactic:
have h10 : f z = f z₀ := (h9 (mem_ball_self hr)).symm

Goal state after:
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z ↦ ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
h5 : ‖f z₀ - v‖ < ε / 2
z : ℂ
hz1 : z ∈ ball z₀ r
hz2 : IsLocalMin (fun z ↦ ‖f z - v‖) z
h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z ↦ f z - v) y
key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v
h7 : ∃ᶠ (w : ℂ) in 𝓝[≠] z, f w = f z
h8 : IsPreconnected (ball z₀ r)
h9 : EqOn f (fun x ↦ f z) (ball z₀ r)
h10 : f z = f z₀
⊢ False
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
| circleAverage (fun z ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖) 0 R = log ‖w - ρ‖

Tactic:
conv =>

Goal state after:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
z : ℂ
| herglotzRieszKernel 0 (w - c) z
Module: Mathlib.Order.Interval.Set.IsoIoo

Goal state before:
pp: case refine_2.refine_1
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ ∀ (x : k), -x / (1 + |(-x)|) = -(x / (1 + |x|))

Tactic:
intro x
      simp only [abs_neg, neg_div]

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: a : ℂ
⊢ a.sqrt = ↑√((‖a‖ + a.re) / 2) + (if 0 ≤ a.im then 1 else -1) * ↑√((‖a‖ - a.re) / 2) * I

Tactic:
rw [← cpow_inv_two_re, sqrt]

Goal state after:
a : ℂ
⊢ a ^ 2⁻¹ = ↑(a ^ 2⁻¹).re + (if 0 ≤ a.im then 1 else -1) * ↑√((‖a‖ - a.re) / 2) * I
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖

Tactic:
h₁f.meromorphicOn.circleAverage_log_norm hR,

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) +
        ↑((divisor f (closedBall c |R|)) c) * Real.log R +
      Real.log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) +
        ↑((divisor f (closedBall c |R|)) c) * Real.log R +
      Real.log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖

Tactic:
h₁f.divisor_apply (by simp),

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) +
        ↑(ENat.map Nat.cast (analyticOrderAt f c)).untop₀ * Real.log R +
      Real.log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
htrace : (↑g).trace = 0
hc : ↑g 1 0 = 0
⊢ g • z = z ↔ z.re = ↑g 0 1 / (2 * ↑g 1 1)

Tactic:
Matrix.trace_fin_two,

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
htrace : ↑g 0 0 + ↑g 1 1 = 0
hc : ↑g 1 0 = 0
⊢ g • z = z ↔ z.re = ↑g 0 1 / (2 * ↑g 1 1)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ g • z = z ↔ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) ^ 2 = -(↑g).det / ↑g 1 0 ^ 2

Tactic:
Matrix.trace_fin_two,

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : ↑g 0 0 + ↑g 1 1 = 0
hc : ↑g 1 0 ≠ 0
⊢ g • z = z ↔ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) ^ 2 = -(↑g).det / ↑g 1 0 ^ 2
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ num (g * h) u / denom (g * h) u = num g (num h u / denom h u) / denom g (num h u / denom h u)

Tactic:
rw [div_eq_div_iff (denom_ne_zero_of_im _ hu) (denom_ne_zero_of_im _ hu'),
    denom, mul_div, div_add' _ _ _ (denom_ne_zero_of_im _ hu), mul_div]

Goal state after:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ num (g * h) u * (↑(↑g 1 0) * num h u + ↑(↑g 1 1) * denom h u) / denom h u =
    num g (num h u / denom h u) * denom (g * h) u
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: τ : ℍ
⊢ ↑(J • τ) = ↑(↑ofComplex (-(starRingEnd ℂ) ↑τ))

Tactic:
coe_J_smul,

Goal state after:
τ : ℍ
⊢ -(starRingEnd ℂ) ↑τ = ↑(↑ofComplex (-(starRingEnd ℂ) ↑τ))
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
ih :
  ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
    (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det
⊢ (f (M k k)).det * (f ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det).det -
      (f (M k k)).det *
        ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
            (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    0

Tactic:
ih,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
ih :
  ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
    (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det
⊢ (f (M k k)).det *
        ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
            (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det -
      (f (M k k)).det *
        ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
            (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ HasStrictDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ

Tactic:
suffices HasStrictDerivAt (num g / denom g) (g.val.det / denom g τ ^ 2) τ by
    refine this.congr_of_eventuallyEq ?_
    rw [← isOpenEmbedding_coe.map_nhds_eq, eventuallyEq_map]
    simp [Function.comp_def, coe_smul_of_det_pos hg]

Goal state after:
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ HasStrictDerivAt (num g / denom g) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ -x + √(1 + (-x) ^ 2) = (rexp (arsinh x))⁻¹

Tactic:
exp_arsinh

Goal state after:
x : ℝ
⊢ -x + √(1 + (-x) ^ 2) = (x + √(1 + x ^ 2))⁻¹
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
⊢ dist d c * dist b d ≤ dist d b * dist c d + dist b c * dist d d

Tactic:
rw [dist_self, mul_zero, add_zero, dist_comm d, dist_comm d, mul_comm]

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

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ dist z w = r ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) = sinh (r / 2)

Tactic:
by
  rw [← div_left_inj' (two_ne_zero' ℝ), ← sinh_inj, sinh_half_dist]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case succ
n : ℕ
ih : iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh
⊢ deriv (iteratedDeriv (n + 1) sinh) = iteratedDeriv (n + 1) cosh

Tactic:
ih,

Goal state after:
case succ
n : ℕ
ih : iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh
⊢ deriv (iteratedDeriv n cosh) = iteratedDeriv (n + 1) cosh