mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.ExponentialBounds

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

Tactic:
by
  rw [exp_neg, lt_inv_comm₀ _ (exp_pos _)]
  · refine lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) ?_
    norm_num
  · norm_num

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : ¬MeromorphicAt f (g x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)

Tactic:
· rw [meromorphicOrderAt_of_not_meromorphicAt hf, meromorphicOrderAt_of_not_meromorphicAt]
    rwa [meromorphicAt_comp_iff_of_deriv_ne_zero hg hg']

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
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
hn : ↑n ≠ 0
hf : meromorphicOrderAt f x = ↑n
hmero : MeromorphicAt f x
⊢ meromorphicOrderAt (deriv f) x = ↑(n - 1)

Tactic:
rw [meromorphicOrderAt_eq_int_iff hmero] at hf

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
hn : ↑n ≠ 0
hf : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
hmero : MeromorphicAt f x
⊢ meromorphicOrderAt (deriv f) x = ↑(n - 1)
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
⊢ ∑ 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‖ =
    ∑ i ∈ t₂, ↑((divisor f B₀R) i) * log ‖canonicalFactor R i w‖ - ∑ᶠ (i : ℂ), ↑((divisor f S₀R) i) * log ‖w - i‖ +
      log ‖meromorphicTrailingCoeffAt f w‖

pp: case η₀
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
⊢ (support fun i ↦ ↑((divisor f B₀R) i) * log ‖canonicalFactor R i w‖) ⊆ ↑t₂

Tactic:
finsum_eq_sum_of_support_subset (s := t₁) _ ?η₁

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

case η₁
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
⊢ (support fun i ↦ ↑((divisor f S₀R) i) * log ‖w - i‖) ⊆ ↑t₁

case η₀
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
⊢ (support fun i ↦ ↑((divisor f B₀R) i) * log ‖canonicalFactor R i w‖) ⊆ ↑t₂
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 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : BF ∈ upperBounds (norm ∘ F f ε '' verticalClosedStrip 0 1)
⊢ ∃ B,
    (fun x ↦ invInterpStrip f x ε • f x) =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z ↦
      Real.exp (B * Real.exp (0 * |z.im|))

Tactic:
simp only [comp_apply, mem_upperBounds, mem_image, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂] at hBF

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
⊢ ∃ B,
    (fun x ↦ invInterpStrip f x ε • f x) =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z ↦
      Real.exp (B * Real.exp (0 * |z.im|))
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.re - z.re| < r₁

Tactic:
grind [abs_lt]

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

Goal state before:
pp: case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ interpStrip f z = ↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z

Tactic:
rw [interpStrip_eq_of_zero _ z h]
    rcases h with h0 | h1
    · simp only [h0, ofReal_zero, zero_eq_mul, cpow_eq_zero_iff, ne_eq, true_and, ofReal_eq_zero]
      left
      rw [sub_eq_zero, eq_comm]
      simp only [Complex.ext_iff, one_re, ne_of_lt hz.2, false_and, not_false_eq_true]
    · simp only [h1, ofReal_zero, zero_eq_mul, cpow_eq_zero_iff, ofReal_eq_zero, ne_eq, true_and]
      right
      rw [eq_comm]
      simp only [Complex.ext_iff, zero_re, ne_of_lt hz.1, false_and, not_false_eq_true]

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

Goal state before:
pp: case succ
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} f = ∂^{init m} (∂_{m (last (n + 1))} f)

Tactic:
calc
      _ = ∂_{m 0} (∂^{tail m} f) := iteratedLineDerivOp_succ_left _ _
      _ = ∂_{m 0} (∂^{init <| tail m} (∂_{tail m <| last n} f)) := by
        congr 1
        exact IH _
      _ = _ := by
        rw [hmtail, iteratedLineDerivOp_succ_left, hmzero, tail_init_eq_init_tail]

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

Goal state before:
pp: c : ℂ
R : ℝ
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
⊢ (↑(2 * π))⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) =
    (2 * ↑π * I)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c R θ)

Tactic:
by
    rw [intervalIntegral.integral_smul, mul_inv_rev, smul_smul]
    match_scalars
    field

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

Goal state before:
pp: case neg
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
H : ContinuousOn (circleAverage (⇑g ∘ f) c) (Set.Ioc 0 |R|)
r : ℝ
hr : r ∈ Set.Ioo 0 |R|
⊢ closedBall c r ⊆ ball c |R|

Tactic:
exact closedBall_subset_ball hr.2

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

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun x ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ (f ∘ fun x ↦ x * I) =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)

pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun x ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
⊢ ‖(f ∘ fun x ↦ x * I) (↑x * I)‖ ≤ C

Tactic:
· simpa only [Function.comp_def, norm_mul, norm_I, mul_one]
      using hO.comp_tendsto ((tendsto_mul_right_cobounded I_ne_zero).inf H.tendsto)

Goal state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun x ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
⊢ ‖(f ∘ fun x ↦ x * I) (↑x * I)‖ ≤ C
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: z : ℍ
n : ℤ
hn : n ≠ 0
w✝ : ℤ
hm : ↑w✝ = ↑n / ↑z
this : (↑n / ↑z).im ≠ 0
⊢ False

Tactic:
simpa [← hm]

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

Goal state before:
pp: ⊢ negMulLog 0 = 0

Tactic:
simp [negMulLog]

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

Goal state before:
pp: ⊢ negMulLog 1 = 0

Tactic:
simp [negMulLog]

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
C' : ℝ
hC' : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C'
z : ℂ
hz : 0 ≤ z.re
⊢ ‖f z‖ ≤ max C C'

Tactic:
rcases hexp with ⟨c, hc, B, hO⟩
    rcases le_total z.im 0 with h | h
    · refine quadrant_IV (hd.mono fun _ => And.left) ⟨c, hc, B, ?_⟩
          (fun x hx => (hC' x hx).trans <| le_max_right _ _)
          (fun x _ => (him x).trans (le_max_left _ _)) hz h
      exact hO.mono (inf_le_inf_left _ <| principal_mono.2 fun _ => And.left)
    · refine quadrant_I (hd.mono fun _ => And.left) ⟨c, hc, B, ?_⟩
          (fun x hx => (hC' x hx).trans <| le_max_right _ _)
          (fun x _ => (him x).trans (le_max_left _ _)) hz h
      exact hO.mono (inf_le_inf_left _ <| principal_mono.2 fun _ => And.left)

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

Goal state before:
pp: case neg
x : ℝ
hr : log x < 0
⊢ 2⁻¹ * (log x + |log x|) = log⁺ x

Tactic:
simp [posLog, hr.le, abs_of_nonpos]

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

Goal state before:
pp: ⊢ MonotoneOn log⁺ (Set.Ici 0)

Tactic:
by
  intro x hx y hy hxy
  simp only [posLog, le_sup_iff, sup_le_iff, le_refl, true_and]
  by_cases! h : log x ≤ 0
  · tauto
  · right
    have := log_le_log (lt_trans Real.zero_lt_one ((log_pos_iff hx).1 h)) hxy
    simp only [this, and_true, ge_iff_le]
    linarith

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

Goal state before:
pp: case hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (fun x ↦ 2⁻¹ * log ‖f x‖) volume a b

pp: case hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (fun x ↦ 2⁻¹ * |log ‖f x‖|) volume a b

Tactic:
· apply hf.intervalIntegrable_log_norm.const_mul

Goal state after:
case hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (fun x ↦ 2⁻¹ * |log ‖f x‖|) volume a b
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: case hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (fun x ↦ 2⁻¹ * |log ‖f x‖|) volume a b

Tactic:
apply hf.intervalIntegrable_log_norm.abs.const_mul

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

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
⊢ log ‖1 - 0 * a‖ = 0

pp: a : ℂ
h : ‖a‖ < 1
⊢ InnerProductSpace.HarmonicOnNhd (fun x ↦ log ‖1 - x * a‖) (closedBall 0 |1|)

Tactic:
zero_mul,

Goal state after:
a : ℂ
h : ‖a‖ < 1
⊢ log ‖1 - 0‖ = 0

a : ℂ
h : ‖a‖ < 1
⊢ InnerProductSpace.HarmonicOnNhd (fun x ↦ log ‖1 - x * a‖) (closedBall 0 |1|)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
⊢ log ‖1‖ = 0

pp: a : ℂ
h : ‖a‖ < 1
⊢ InnerProductSpace.HarmonicOnNhd (fun x ↦ log ‖1 - x * a‖) (closedBall 0 |1|)

Tactic:
CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem,

Goal state after:
a : ℂ
h : ‖a‖ < 1
⊢ log 1 = 0

a : ℂ
h : ‖a‖ < 1
⊢ InnerProductSpace.HarmonicOnNhd (fun x ↦ log ‖1 - x * a‖) (closedBall 0 |1|)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
x : ℂ
hx : x ∈ closedBall 0 |1|
this : ‖1‖ < 1
hCon : 1 = x * a
⊢ False

Tactic:
CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem,

Goal state after:
a : ℂ
h : ‖a‖ < 1
x : ℂ
hx : x ∈ closedBall 0 |1|
this : 1 < 1
hCon : 1 = x * a
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: r : ℝ
⊢ (Complex.exp (Complex.I * ↑r) - Complex.exp (Complex.I * -↑r)) / Complex.I = 2 * ↑(sin r)

Tactic:
simp only [mul_comm Complex.I, Complex.exp_mul_I, Complex.cos_neg, Complex.sin_neg,
      add_sub_add_left_eq_sub, Complex.div_I, Complex.ofReal_sin]
    rw [sub_mul, mul_assoc, mul_assoc, two_mul]
    simp

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

Goal state before:
pp: a b c : ℝ
⊢ ∫ (x : ℝ) in a..b, c * (c ^ 2 + x ^ 2)⁻¹ = arctan (b / c) - arctan (a / c)

Tactic:
by
    by_cases hc : c = 0
    · simp [hc]
    · rw [integral_const_mul, integral_inv_sq_add_sq hc]
      field_simp

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

Goal state before:
pp: case inl.refine_1
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 1

Tactic:
lia

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

Goal state before:
pp: case inl.refine_2
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 2

Tactic:
lia

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

Goal state before:
pp: case inr.refine_1
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 2

Tactic:
lia

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

Goal state before:
pp: case inr.refine_2
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 3

Tactic:
lia

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

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
⊢ f c ≤ f z

Tactic:
by
  convert!
    apply_le_of_iteratedDeriv_nonneg (f := fun z ↦ f (-z)) (hf.comp <| differentiable_neg)
      (fun n hn ↦ ?_) (neg_le_neg_iff.mpr hz) using 1
  · simp only [neg_neg]
  · simp only [neg_neg]
  · simpa only [iteratedDeriv_comp_neg, neg_neg, smul_eq_mul] using h n hn

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

Goal state before:
pp: 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
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
a : ℂ
ha : a ∈ U
b : ℂ
hb : b ∈ U
hab : f b = -f a
⊢ a = b

Tactic:
by
      rw [← hf_inv b, hab]
      simp [hf_inv a]

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

Goal state before:
pp: case refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ StrictMono (codRestrict (fun x ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)

pp: case refine_3
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ Function.RightInverse (fun x ↦ ↑x / (1 - |↑x|)) (codRestrict (fun x ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)

Tactic:
· refine (strictMono_of_odd_strictMonoOn_nonneg ?_ ?_).codRestrict _
    · intro x
      simp only [abs_neg, neg_div]
    · rintro x (hx : 0 ≤ x) y (hy : 0 ≤ y) hxy
      simp [abs_of_nonneg, mul_add, mul_comm x y, div_lt_div_iff₀, hx.trans_lt (lt_one_add _),
        hy.trans_lt (lt_one_add _), *]

Goal state after:
case refine_3
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ Function.RightInverse (fun x ↦ ↑x / (1 - |↑x|)) (codRestrict (fun x ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
hR : ∀ (r : Rˣ), ∃ k, k ^ Fintype.card n = r
g : GL n R
r : Rˣ
hr : r ^ Fintype.card n = (GeneralLinearGroup.det g)⁻¹
⊢ r ^ Fintype.card n * GeneralLinearGroup.det g = 1

Tactic:
simpa [mul_eq_one_iff_eq_inv] using hr

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
⊢ Tendsto (fun t ↦ (2 / 3) ^ t * ‖f‖) atTop (𝓝 0)

Tactic:
← zero_mul ‖f‖

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
⊢ Tendsto (fun t ↦ (2 / 3) ^ t * ‖f‖) atTop (𝓝 (0 * ‖f‖))
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n✝ : ℕ
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
n : ℕ
hn : 1 ≤ n
IH : ((Matrix.scalar (Fin 2)) a + m) ^ n = (Matrix.scalar (Fin 2)) (a ^ n) + (↑n * a ^ (n - 1)) • m
⊢ n = n - 1 + 1

Tactic:
lia

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n✝ : ℕ
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
n : ℕ
hn : 1 ≤ n
IH : ((Matrix.scalar (Fin 2)) a + m) ^ n = (Matrix.scalar (Fin 2)) (a ^ n) + (↑n * a ^ (n - 1)) • m
⊢ n - 1 + 1 = n

Tactic:
lia

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

Goal state before:
pp: S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ M k k ^ Fintype.card { a // a = k ↔ True } • det 1 * ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det =
    M k k * ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det

Tactic:
iff_true,

Goal state after:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ M k k ^ Fintype.card { a // a = k } • det 1 * ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det =
    M k k * ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ arsinh (-x) = -arsinh x

Tactic:
← exp_eq_exp,

Goal state after:
x : ℝ
⊢ rexp (arsinh (-x)) = rexp (-arsinh x)
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case 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
⊢ dist b c * dist b d ≤ 0 * dist c d + dist b c * dist b d

Tactic:
zero_mul,

Goal state after:
case 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
⊢ dist b c * dist b d ≤ 0 + dist b c * dist b d
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℂ
⊢ HasStrictDerivAt sinh (cosh x) x

Tactic:
simp only [cosh, div_eq_mul_inv]

Goal state after:
x : ℂ
⊢ HasStrictDerivAt sinh ((cexp x + cexp (-x)) * 2⁻¹) x
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: case trans
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F G x y z : Ultrafilter α
a✝¹ : Relation.EqvGen (fun F G ↦ ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) x y
a✝ : Relation.EqvGen (fun F G ↦ ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) y z
h : Ultrafilter.extend g x = Ultrafilter.extend g y
h' : Ultrafilter.extend g y = Ultrafilter.extend g z
⊢ Ultrafilter.extend g x = Ultrafilter.extend g z

Tactic:
| trans x y z _ _ h h' =>

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
⊢ some ⁻¹' {∞} = ∅

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_3
f : OnePoint X → α
l : Filter α
⊢ Tendsto f (𝓝 ∞) l ↔ Tendsto f (pure ∞) l ∧ Tendsto (f ∘ some) (coclosedCompact X) l

Tactic:
simp [nhds_infty_eq, and_comm]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
a₀ : E
h : ¬a = ⊤
⊢ ℝ → ℝ

Tactic:
· exact circleAverage (log⁺ ‖f · - a.untop₀‖⁻¹) 0

Goal state after: