mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
u : E →L[𝕜] F
A : Submodule 𝕜 F
inst✝ : FiniteDimensional 𝕜 ↥A
A_compl : A.ClosedComplemented
S : Submodule 𝕜 F
A_compl_S : IsTopCompl A S
Φ : (F ⧸ A) ≃L[𝕜] ↥S := A.quotientEquivOfIsTopCompl S A_compl_S
i : ↥S →L[𝕜] F := S.subtypeL
i_clemb : IsClosedEmbedding ⇑i
p : F →L[𝕜] F := S.projectionL A ⋯
p_def : p = S.projectionL A ⋯
eq : ⇑i ∘ ⇑Φ ∘ ⇑A.mkQ = ⇑p
this : ↑u ≈ ↑(p ∘SL u)
⊢ IsStrictMap (⇑p ∘ ⇑u) ∧ IsClosed[inst✝⁴] (range (⇑p ∘ ⇑u)) ↔
    IsStrictMap (⇑i ∘ ⇑Φ ∘ ⇑A.mkQ ∘ ⇑u) ∧ IsClosed[inst✝⁴] (range (⇑i ∘ ⇑Φ ∘ ⇑A.mkQ ∘ ⇑u))

Tactic:
by
          simp_rw [← eq, Function.comp_assoc]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
inst✝ : Semiring R
vNonneg : ∀ (a : R), v a ≥ 0
h : HasGaussNorm v c f
⊢ 0 ≤ v (constantCoeff f)

Tactic:
simp [vNonneg]

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E → E
tmin tmax tmin' tmax' : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
t₀' : ↑(Icc tmin' tmax')
ht₀ : ↑t₀ = ↑t₀'
htmin : tmin ≤ tmin'
htmax : tmax' ≤ tmax
⊢ IsPicardLindelof f t₀' x₀ a r L K

Tactic:
apply hf.shrink t₀' htmin htmax le_rfl
  calc L * max (tmax' - t₀') (t₀' - tmin')
    _ ≤ L * max (tmax - t₀) (t₀ - tmin) := by gcongr <;> linarith
    _ ≤ a - r := hf.mul_max_le

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
h : p.degree = 1
⊢ p.logMahlerMeasure = log ‖p.coeff 1‖ + log⁺ ‖(p.coeff 1)⁻¹ * p.coeff 0‖

Tactic:
eq_X_add_C_of_degree_le_one (le_of_eq h)

Goal state after:
p : ℂ[X]
h : p.degree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).logMahlerMeasure =
    log ‖(C (p.coeff 1) * X + C (p.coeff 0)).coeff 1‖ +
      log⁺ ‖((C (p.coeff 1) * X + C (p.coeff 0)).coeff 1)⁻¹ * (C (p.coeff 1) * X + C (p.coeff 0)).coeff 0‖
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
h : p.degree = 1
⊢ p.mahlerMeasure = max ‖p.coeff 1‖ ‖p.coeff 0‖

Tactic:
eq_X_add_C_of_degree_le_one (le_of_eq h)

Goal state after:
p : ℂ[X]
h : p.degree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).mahlerMeasure =
    max ‖(C (p.coeff 1) * X + C (p.coeff 0)).coeff 1‖ ‖(C (p.coeff 1) * X + C (p.coeff 0)).coeff 0‖
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vna : IsNonarchimedean v
vNeg : ∀ (a : R), v a = v (-a)
hbfg : HasGaussNorm v c (f * g)
i₀ j₀ : σ →₀ ℕ
hi₀ : (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c f
hj₀ : (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c g
hdom' :
  ∀ p ∈ Finset.antidiagonal (i₀ + j₀),
    p ≠ (i₀, j₀) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i₀) f) * v ((coeff j₀) g)
⊢ (v ((coeff i₀) f) * v ((coeff j₀) g) * (i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2) =
    v ((coeff i₀) f * (coeff j₀) g) * (i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2

Tactic:
rw [vMulEq]

Goal state after:
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
this✝ : 0 < b
this : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
h_le : ↑b ^ n * x < ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i + 1
⊢ ↑b ^ n * (x - (↑b)⁻¹ ^ n) ≤ ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i

Tactic:
mul_sub,

Goal state after:
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
this✝ : 0 < b
this : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
h_le : ↑b ^ n * x < ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i + 1
⊢ ↑b ^ n * x - ↑b ^ n * (↑b)⁻¹ ^ n ≤ ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: ⊢ π < 4

Tactic:
pi_upper_bound [4 / 3]

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
r : ℝ
hx : Germ.Tendsto x (𝓝 r)
⊢ 0 ≤ ArchimedeanClass.mk x

Tactic:
rw [tendsto_iff_forall] at hx
  obtain ⟨s, hs⟩ := exists_lt r
  obtain ⟨t, ht⟩ := exists_gt r
  exact mk_nonneg_of_le_of_le_of_archimedean coeRingHom (hx.1 s hs) (hx.2 t ht)

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x / ↑q)

Tactic:
div_eq_mul_inv,

Goal state after:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * (↑q)⁻¹)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: q : ℚ
x : ℝ
⊢ Irrational (x / ↑q) ↔ q ≠ 0 ∧ Irrational x

Tactic:
div_eq_mul_inv,

Goal state after:
q : ℚ
x : ℝ
⊢ Irrational (x * (↑q)⁻¹) ↔ q ≠ 0 ∧ Irrational x
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: f : ℕ → ℝ
hf : Tendsto f atTop atBot
⊢ (ofSeq f).InfiniteNeg

Tactic:
by
  replace hf := hf.mono_left Nat.hyperfilter_le_atTop
  rw [infiniteNeg_iff]
  exact ⟨lt_of_tendsto_atBot 0 hf, archimedeanClassMk_neg_of_tendsto_atBot hf⟩

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
have hu₁_eval_one : u₁ 1 = 0 := by simp only [u₁, f]; simp

Goal state after:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 + z * I) / (1 - z * I) ≠ 0

Tactic:
· exact div_ne_zero z₁ z₂

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case inl
z : ℂ
h₂ : z.re ≤ π / 2
k : ℤ
h₁ : -1 < ↑(2 * k + 1)
nr : z.re = ↑(2 * k + 1) * π / 2
⊢ z.re = π / 2

Tactic:
rw [nr, ← one_mul (π / 2), mul_div_assoc, mul_le_mul_iff_of_pos_right (by positivity)] at h₂

Goal state after:
case inl
z : ℂ
k : ℤ
h₂ : ↑(2 * k + 1) ≤ 1
h₁ : -1 < ↑(2 * k + 1)
nr : z.re = ↑(2 * k + 1) * π / 2
⊢ z.re = π / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
⊢ Tendsto (fun n ↦ (x.agmSequences y n).1) atTop (𝓝 (x.agm y))

Tactic:
by
  rw [agm_eq_ciSup]
  exact tendsto_atTop_ciSup agmSequences_fst_monotone bddAbove_range_agmSequences_fst

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: y : ℝ≥0
n : ℕ
⊢ (agmSequences 0 y n).1 = 0

Tactic:
induction n with
  | zero => simp [agmSequences]
  | succ n ih =>
    rw [agmSequences_succ', ih, zero_mul, sqrt_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
plq : p < q
⊢ (p + q) / 2 < q / 2 + q / 2

Tactic:
rw [add_div]

Goal state after:
x y : ℝ≥0
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
plq : p < q
⊢ p / 2 + q / 2 < q / 2 + q / 2
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case convert_2.convert_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ -2 * (↑n + 1) * (u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) - ∫ (x : ℝ) in -1..1, u₂' x * v₂ x) =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
mul_sub,

Goal state after:
case convert_2.convert_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ -2 * (↑n + 1) * (u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1)) - -2 * (↑n + 1) * ∫ (x : ℝ) in -1..1, u₂' x * v₂ x =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < binEntropy p

Tactic:
by
  unfold binEntropy
  have : 0 < 1 - p := sub_pos.2 hp₁
  have : 0 < log p⁻¹ := log_pos <| (one_lt_inv₀ hp₀).2 hp₁
  have : 0 < log (1 - p)⁻¹ := log_pos <| (one_lt_inv₀ ‹_›).2 (sub_lt_self _ hp₀)
  positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Choose

Goal state before:
pp: k : ℕ
⊢ (fun n ↦ ↑n ^ k / ↑k !) =Θ[atTop] fun n ↦ ↑n ^ k

Tactic:
div_eq_mul_inv,

Goal state after:
k : ℕ
⊢ (fun n ↦ ↑n ^ k * (↑k !)⁻¹) =Θ[atTop] fun n ↦ ↑n ^ k
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ (fun x ↦ ‖Real.log ‖x‖‖) z ≤ (fun z ↦ Real.log √2 + Real.log (max z.re |z.im|)) z

Tactic:
simp only [Real.norm_of_nonneg (Real.log_nonneg hz')]

Goal state after:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ Real.log ‖z‖ ≤ Real.log √2 + Real.log (max z.re |z.im|)
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case inl
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ k = ↑z

Tactic:
rcases k.eq_zero_or_pos with rfl | hk
    · exact ⟨p.coeff 0, by simp⟩
    exact ⟨0, by simp [hk.ne']⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
hp : p ≠ 1
ht : 0 < t
x : ℝ
⊢ t ^ p * (t⁻¹ - (t + x)⁻¹) = t ^ (p - 1) - t ^ p * (t + x)⁻¹

Tactic:
mul_sub,

Goal state after:
p t : ℝ
hp : p ≠ 1
ht : 0 < t
x : ℝ
⊢ t ^ p * t⁻¹ - t ^ p * (t + x)⁻¹ = t ^ (p - 1) - t ^ p * (t + x)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
ht : 0 < t
x : ℝ
hx : x ∈ Ici 0
⊢ t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹) = (fun x ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) x

Tactic:
simp [mul_comm, smul_eq_mul, rpowIntegrand₀₁]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
t : ℝ
ht : 1 < t
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 2) * x

Tactic:
exact rpowIntegrand₀₁_le_rpow_sub_two_mul_self hp (by positivity) hx

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ 2 * (2 * ↑π) ^ (-s) * Gamma s / (cos (↑π * s / 2))⁻¹ = 2 * (2 * ↑π) ^ (-s) * Gamma s * cos (↑π * s / 2)

Tactic:
div_eq_mul_inv,

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ 2 * (2 * ↑π) ^ (-s) * Gamma s * (cos (↑π * s / 2))⁻¹⁻¹ = 2 * (2 * ↑π) ^ (-s) * Gamma s * cos (↑π * s / 2)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (log ∘ Gamma) (↑n + 1) = -γ + ↑(harmonic n)
⊢ deriv Gamma (↑n + 1) = ↑n ! * (-γ + ↑(harmonic n))

Tactic:
rwa [Function.comp_def, deriv.log (differentiableAt_Gamma (fun m ↦ by linarith))
      (by positivity), Gamma_nat_eq_factorial, div_eq_iff_mul_eq (by positivity),
      mul_comm, Eq.comm] at this

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ 0 ≤ (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹

Tactic:
rw [inv_nonneg]; exact le_of_lt <| integral_rpowIntegrand₀₁_one_pos hp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * cos (↑π * (s - 1) / 2) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * (s - 1) / 2 / ↑π * sin (↑π * s / 2) * ((s - 1).Gammaℝ * (s - 1) / 2 / ↑π)⁻¹

Tactic:
mul_sub,

Goal state after:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * cos ((↑π * s - ↑π * 1) / 2) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * (s - 1) / 2 / ↑π * sin (↑π * s / 2) * ((s - 1).Gammaℝ * (s - 1) / 2 / ↑π)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
⊢ 0 < (↑π / a).re

Tactic:
div_eq_mul_inv,

Goal state after:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
⊢ 0 < (↑π * a⁻¹).re
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
Ff_bd : 𝓕 f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
⊢ ∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2)

Tactic:
convert! Real.tsum_eq_tsum_fourier_of_rpow_decay (by fun_prop) one_lt_two f_bd Ff_bd 0 using 1

Goal state after:
case e'_2
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
Ff_bd : 𝓕 f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
⊢ ∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) = ∑' (n : ℤ), f (0 + ↑n)

case e'_3
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
Ff_bd : 𝓕 f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
⊢ 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2) = ∑' (n : ℤ), 𝓕 f ↑n * (fourier n) ↑0
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ ↑(Nat.log b ⌊↑(b ^ n)⌋₊) = ↑n

Tactic:
Nat.floor_natCast,

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ ↑(Nat.log b (b ^ n)) = ↑n
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |ε.mulExpNegMulSq x| ≤ (√ε)⁻¹

Tactic:
mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one hε x,

Goal state after:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |(√ε)⁻¹ * mulExpNegMulSq 1 (√ε * x)| ≤ (√ε)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case neg
b : ℝ
h : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
⊢ logb b =O[⊤] log

Tactic:
· simpa [logb, div_eq_mul_inv, mul_comm]
      using! (Asymptotics.isBigO_refl log ⊤).const_mul_left (log b)⁻¹

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
L : PeriodPair
⊢ IsZLattice ℝ L.lattice

Tactic:
simp_rw [L.lattice_eq_span_range_basis]
  infer_instance

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℤ × ℤ
⊢ ↑(L.latticeEquivProd.symm x) = ↑x.1 * L.ω₁ + ↑x.2 * L.ω₂

Tactic:
simp [latticeEquivProd, Finsupp.linearCombination]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
h : Tendsto (fun n ↦ (↑n)⁻¹) atTop (𝓝 0)
this :
  Tendsto
    ((fun n ↦ (Multiset.map (fun x ↦ x / ↑n + 1) a).prod) / fun x ↦
      (Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) b).prod * (1 + (↑x)⁻¹))
    atTop (𝓝 1)
⊢ Tendsto
    (fun n ↦ (Multiset.map (fun x ↦ x / ↑n + 1) a).prod / ((Multiset.map (fun x ↦ x / ↑n + 1) b).prod * (1 + (↑n)⁻¹)))
    atTop (𝓝 1)

Tactic:
apply this.congr

Goal state after:
a b : Multiset ℂ
h : Tendsto (fun n ↦ (↑n)⁻¹) atTop (𝓝 0)
this :
  Tendsto
    ((fun n ↦ (Multiset.map (fun x ↦ x / ↑n + 1) a).prod) / fun x ↦
      (Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) b).prod * (1 + (↑x)⁻¹))
    atTop (𝓝 1)
⊢ ∀ (x : ℕ),
    ((fun n ↦ (Multiset.map (fun x ↦ x / ↑n + 1) a).prod) / fun x ↦
          (Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) b).prod * (1 + (↑x)⁻¹))
        x =
      (Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) a).prod / ((Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) b).prod * (1 + (↑x)⁻¹))
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ ↑n ^ (↑a.card - ↑b.card - 1)) atTop (𝓝 0)

Tactic:
apply this.congr

Goal state after:
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 0)
⊢ ∀ (x : ℕ), (1 / ↑x) ^ (b.card + 1 - a.card) = ↑x ^ (↑a.card - ↑b.card - 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
this : ¬2 * ↑n ∣ ↑i
⊢ ∫ (a : ℝ), eval a (T ℝ ↑i) ∂measureT = sumZeroes n (T ℝ ↑i)

Tactic:
rw [integral_eval_T_real_measureT_of_ne_zero (by grind), sumZeroes_T_of_not_dvd this]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: x : Fin 2 → ℤ
⊢ ‖x‖ = ↑(max (x 0).natAbs (x 1).natAbs)

Tactic:
rw [← coe_nnnorm, ← NNReal.coe_natCast, NNReal.coe_inj, Nat.cast_max]
  refine eq_of_forall_ge_iff fun c ↦ ?_
  simp only [pi_nnnorm_le_iff, Fin.forall_fin_two, max_le_iff, NNReal.natCast_natAbs]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case zero
L : PeriodPair
l : ℂ
⊢ (if 0 = 0 then ℘[L - l] l else (↑0 + 1) * L.sumInvPow l (0 + 2)) =
    (if 0 = 0 then ℘[L - l] l else ↑(0 + 1)! * L.sumInvPow l (0 + 2)) / ↑0!

Tactic:
simp [Nat.factorial_succ]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case succ
L : PeriodPair
l : ℂ
n✝ : ℕ
⊢ (if n✝ + 1 = 0 then ℘[L - l] l else (↑(n✝ + 1) + 1) * L.sumInvPow l (n✝ + 1 + 2)) =
    (if n✝ + 1 = 0 then ℘[L - l] l else ↑(n✝ + 1 + 1)! * L.sumInvPow l (n✝ + 1 + 2)) / ↑(n✝ + 1)!

Tactic:
simp [Nat.factorial_succ]

Goal state after:
case succ
L : PeriodPair
l : ℂ
n✝ : ℕ
⊢ (↑n✝ + 1 + 1) * L.sumInvPow l (n✝ + 1 + 2) =
    (↑n✝ + 1 + 1) * ((↑n✝ + 1) * ↑n✝!) * L.sumInvPow l (n✝ + 1 + 2) / ((↑n✝ + 1) * ↑n✝!)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case hbc.inl
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
H1 : 1 ≤ (↑(x 0) / ‖x‖) ^ 2
⊢ r z ≤ ‖↑(x 0) / ↑↑(max (x 0).natAbs (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑(max (x 0).natAbs (x 1).natAbs)‖

pp: case hbc.inr
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
H2 : 1 ≤ (↑(x 1) / ‖x‖) ^ 2
⊢ r z ≤ ‖↑(x 0) / ↑↑(max (x 0).natAbs (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑(max (x 0).natAbs (x 1).natAbs)‖

Tactic:
· simpa only [norm_eq_max_natAbs, ofReal_div, ofReal_intCast] using auxbound1 z (x 1 / ‖x‖) H1

Goal state after:
case hbc.inr
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
H2 : 1 ≤ (↑(x 1) / ‖x‖) ^ 2
⊢ r z ≤ ‖↑(x 0) / ↑↑(max (x 0).natAbs (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑(max (x 0).natAbs (x 1).natAbs)‖
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
this : AnalyticAt ℂ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) x
⊢ AnalyticAt ℂ L.relation x

Tactic:
apply this.congr

Goal state after:
case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
this : AnalyticAt ℂ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) x
⊢ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) =ᶠ[𝓝 x] L.relation
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: m : ℕ
n : ℤ
h : ↑m ∣ n
⊢ fib ↑((↑m).gcd n) = fib ↑m

Tactic:
(gcd_eq_left_iff_dvd (by simp)).mpr

Goal state after:
m : ℕ
n : ℤ
h : ↑m ∣ n
⊢ fib ↑m = fib ↑m

m : ℕ
n : ℤ
h : ↑m ∣ n
⊢ ↑m ∣ n
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ 1 - φ = ψ

Tactic:
by
  linarith [goldenRatio_add_goldenConj]

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ 1 - ψ = φ

Tactic:
by
  linarith [goldenRatio_add_goldenConj]

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1) - φ * (φ ^ n - ψ ^ n)) / √5 = ψ ^ n

Tactic:
mul_sub,

Goal state after:
n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1) - (φ * φ ^ n - φ * ψ ^ n)) / √5 = ψ ^ n