mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
v : A →+* ℂ
hv : Isometry ⇑v
n : ℕ
p : A[X]
hv_norm : ‖p.coeff n‖ = ‖v (p.coeff n)‖
hcoeff : ‖v (p.coeff n)‖ = ‖(map v p).coeff n‖
⊢ ↑((map v p).natDegree.choose n) * (map v p).mahlerMeasure ≤ ↑(p.natDegree.choose n) * p.mapMahlerMeasure v

Tactic:
natDegree_map_eq_of_injective hv.injective,

Goal state after:
A : Type u_2
inst✝ : NormedRing A
v : A →+* ℂ
hv : Isometry ⇑v
n : ℕ
p : A[X]
hv_norm : ‖p.coeff n‖ = ‖v (p.coeff n)‖
hcoeff : ‖v (p.coeff n)‖ = ‖(map v p).coeff n‖
⊢ ↑(p.natDegree.choose n) * (map v p).mahlerMeasure ≤ ↑(p.natDegree.choose n) * p.mapMahlerMeasure v
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
r : ℝ
hxr : x.IsSt r
f : ℝ → ℝ
hf : ContinuousAt f r
⊢ IsSt (Germ.map f x) (f r)

Tactic:
rcases ofSeq_surjective x with ⟨g, rfl⟩

Goal state after:
r : ℝ
f : ℝ → ℝ
hf : ContinuousAt f r
g : ℕ → ℝ
hxr : (ofSeq g).IsSt r
⊢ IsSt (Germ.map f (ofSeq g)) (f r)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

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

Tactic:
have z₂ : 1 - z * I ≠ 0 := by
    contrapose h₂
    rw [sub_eq_zero, ← div_eq_iff I_ne_zero, div_I, one_mul] at h₂
    exact h₂.symm

Goal state after:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ (π / 2)⁻¹ * W k = (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)

Tactic:
by
  rw [integral_sin_pow_even, integral_sin_pow_odd, mul_div_mul_comm, ← prod_div_distrib, inv_div]
  simp_rw [div_div_div_comm, div_div_eq_mul_div, mul_div_assoc]
  rfl

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

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ 1 ≤ x + √(x ^ 2 - 1)

Tactic:
calc
    1 ≤ x + 0 := by simpa
    _ ≤ x + √(x ^ 2 - 1) := by gcongr; positivity

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

Goal state before:
pp: x : ℝ
hx : x ∈ Ioi 1
⊢ HasStrictDerivAt arcosh (sinh (arcosh x))⁻¹ x

Tactic:
refine coshOpenPartialHomeomorph.hasStrictDerivAt_symm hx ?_ (hasStrictDerivAt_cosh _)

Goal state after:
x : ℝ
hx : x ∈ Ioi 1
⊢ sinh (arcosh x) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ |↑((x + y) / 2 - sqrt (x * y))| ≤ dist x y / 2

Tactic:
abs_eq

Goal state after:
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑((x + y) / 2 - sqrt (x * y)) ≤ dist x y / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑(y - x) / 2 = |↑(y - x)| / 2

Tactic:
abs_eq

Goal state after:
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑(y - x) / 2 = ↑(y - x) / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inl
x y : ℝ≥0
h✝ : x ≠ y
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 < (x.agmSequences y k).2
h : n ≤ m
⊢ (x.agmSequences y n).1 < (x.agmSequences y m).2

pp: case inr
x y : ℝ≥0
h✝ : x ≠ y
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 < (x.agmSequences y k).2
h : m ≤ n
⊢ (x.agmSequences y n).1 < (x.agmSequences y m).2

Tactic:
· exact (agmSequences_fst_monotone h).trans_lt this

Goal state after:
case inr
x y : ℝ≥0
h✝ : x ≠ y
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 < (x.agmSequences y k).2
h : m ≤ n
⊢ (x.agmSequences y n).1 < (x.agmSequences y m).2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case h
x y : ℝ≥0
⊢ ∀ (y_1 : ℝ≥0), (∃ y_2, (x.agmSequences y y_2).1 = y_1) → y_1 ≤ (x.agmSequences y 0).2

Tactic:
forall_exists_index,

Goal state after:
case h
x y : ℝ≥0
⊢ ∀ (y_1 : ℝ≥0) (x_1 : ℕ), (x.agmSequences y x_1).1 = y_1 → y_1 ≤ (x.agmSequences y 0).2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
hn : x ≠ y
h : x < y
⊢ x.agm y < max x y

Tactic:
rw [max_eq_right h.le]

Goal state after:
x✝ y✝ x y : ℝ≥0
hn : x ≠ y
h : x < y
⊢ x.agm y < y
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

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

Tactic:
by
  obtain rfl | hp₀ := hp₀.eq_or_lt
  · simp
  obtain rfl | hp₁ := hp₁.eq_or_lt
  · simp
  exact (binEntropy_pos hp₀ hp₁).le

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

Goal state before:
pp: case neg
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : -p * log p ≤ 0
⊢ -p * log p < (1 - p) * log (1 - p)

Tactic:
nlinarith [(log_pos (by linarith) : 0 < log (1 - p))]

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

Goal state before:
pp: l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
⊢ (fun z ↦ z ^ a₂ * cexp (↑b₁ * z) * cexp (↑(b₂ - b₁) * z)) =ᶠ[l] fun z ↦ z ^ a₂ * cexp (↑b₂ * z)

Tactic:
by
      simp only [ofReal_sub, sub_mul, mul_assoc, ← exp_add, add_sub_cancel]
      norm_cast

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

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
⊢ p2 ∈ Icc 0 (1 - 1 / ↑q) → p1 < p2 → qaryEntropy q p1 < qaryEntropy q p2

Tactic:
hp2

Goal state after:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
⊢ p1 < p2 → qaryEntropy q p1 < qaryEntropy q p2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
⊢ p2 ∈ Icc (1 - 1 / ↑q) 1 → p1 < p2 → qaryEntropy q p2 < qaryEntropy q p1

Tactic:
hp2

Goal state after:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
⊢ p1 < p2 → qaryEntropy q p2 < qaryEntropy q p1
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
δ : ℝ
hδ : δ > 0
C : ℝ := |log (b / a)|
hC_def : C = |log (b / a)|
δ' : ℝ := δ / (C + 1)
⊢ ∀ᶠ (x : ℝ) in F, dist (∫ (x : ℝ) in a * x..b * x, x⁻¹ • f x) (log (b / a) • V) < δ

Tactic:
filter_upwards [hpos, huni δ' (by positivity)] with t ht_pos hbound

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
δ : ℝ
hδ : δ > 0
C : ℝ := |log (b / a)|
hC_def : C = |log (b / a)|
δ' : ℝ := δ / (C + 1)
t : ℝ
ht_pos : 0 < t
hbound : ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ'
⊢ dist (∫ (x : ℝ) in a * t..b * t, x⁻¹ • f x) (log (b / a) • V) < δ
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)
n : ℕ
⊢ f (↑n + 2) - f (↑n + 1) = log (↑n + 1)

Tactic:
show n + 2 = (n + 1) + (1 : ℝ) by ring,

Goal state after:
n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)
n : ℕ
⊢ f (↑n + 1 + 1) - f (↑n + 1) = log (↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
⊢ rexp ((a * ↑x ^ 2).re + (b * ↑x).re) = rexp (a.re * x ^ 2 + b.re * x)

Tactic:
← ofReal_pow,

Goal state after:
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
⊢ rexp ((a * ↑(x ^ 2)).re + (b * ↑x).re) = rexp (a.re * x ^ 2 + b.re * x)
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ ↑b ^ (Nat.clog b ⌈r⁻¹⌉₊ - 1) < r⁻¹

Tactic:
← Nat.cast_pow

Goal state after:
case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ ↑(b ^ (Nat.clog b ⌈r⁻¹⌉₊ - 1)) < r⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
hx : 0 < x
⊢ log (x ^ y) / log b = y * logb b x

Tactic:
log_rpow hx,

Goal state after:
b x y : ℝ
hx : 0 < x
⊢ y * log x / log b = y * logb b x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ StrictAntiOn (logb b) (Iio 0)

Tactic:
rintro x (hx : x < 0) y (hy : y < 0) hxy

Goal state after:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b y < logb b x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ StrictMonoOn (logb b) (Iio 0)

Tactic:
rintro x (hx : x < 0) y (hy : y < 0) hxy

Goal state after:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b x < logb b y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case neg.inr
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
h✝ : b = 1
⊢ ⌊logb (↑b) r⌋ = Int.log b r

Tactic:
· simp_all only [Nat.cast_one, logb_one_left, Int.floor_zero, Int.log_one_left]

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

Goal state before:
pp: case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ logb (↑b) r ≤ ↑(Int.clog b r)

Tactic:
logb_le_iff_le_rpow hb1' hr,

Goal state after:
case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ r ≤ ↑b ^ ↑(Int.clog b r)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: c : ℝ
⊢ (fun x ↦ log (c * x)) =O[atTop] log

Tactic:
obtain rfl | hc := eq_or_ne c 0

Goal state after:
case inl
⊢ (fun x ↦ log (0 * x)) =O[atTop] log

case inr
c : ℝ
hc : c ≠ 0
⊢ (fun x ↦ log (c * x)) =O[atTop] log
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖l ^ 2 - (s - l) ^ 2‖ / (‖s - l‖ ^ 2 * ‖l‖ ^ 2) ≤ ‖l ^ 2 - (s - l) ^ 2‖ / ((‖l‖ / 2) ^ 2 * ‖l‖ ^ 2)

Tactic:
gcongr
      rw [norm_sub_rev]
      exact .trans (by linarith) (norm_sub_norm_le l s)

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : ↑(sphere 0 1)
this : Nontrivial E
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ μ.toSphere (ball x ε)

Tactic:
wlog hε₂ : ε ≤ 2 generalizing ε

Goal state after:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : ↑(sphere 0 1)
this✝ : Nontrivial E
this : ∀ {ε : ℝ}, 0 < ε → ε ≤ 2 → ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ μ.toSphere (ball x ε)
hε₂ : ¬ε ≤ 2
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ μ.toSphere (ball x ε)

E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ μ.toSphere (ball x ε)
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
n : ℕ
j : ℂ
ha : j ∈ a
hj : j = -↑n
⊢ (regularizedHGFunSeries a b).radius = ⊤

Tactic:
apply FormalMultilinearSeries.radius_eq_top_of_eventually_eq_zero
  apply eventually_atTop.mpr
  use n + 1
  grind

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

Goal state before:
pp: case pos
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∃ j ∈ a, ∃ k, j = -↑k
⊢ (regularizedHGFunSeries a b).radius = ⊤

Tactic:
obtain ⟨j, hj, k, ha⟩ := ha
    apply radius_regularizedHGFunSeries_eq_top_of_finite hj ha

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : StandardBorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
⊢ Nonempty (α ≃ᵐ ↑(range Nat.cast))

Tactic:
have : PolishSpace (range ((↑) : ℕ → ℝ)) :=
    Nat.isClosedEmbedding_coe_real.isClosedMap.isClosed_range.polishSpace
  refine ⟨PolishSpace.Equiv.measurableEquiv ?_⟩
  refine (nonempty_equiv_of_countable.some : α ≃ ℕ).trans ?_
  exact Equiv.ofInjective ((↑) : ℕ → ℝ) Nat.cast_injective

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

Goal state before:
pp: case refine_1
⊢ range sigmoid ⊆ Ioo 0 1

Tactic:
rintro - ⟨x, rfl⟩

Goal state after:
case refine_1
x : ℝ
⊢ x.sigmoid ∈ Ioo 0 1
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: x : ℝ
⊢ ↑(sigmoid (-x)) = ↑(σ (sigmoid x))

Tactic:
exact Real.sigmoid_neg x

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

Goal state before:
pp: case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ deriv ℘[L] x = ℘'[L] x

Tactic:
rw [deriv_zero_of_not_differentiableAt, L.derivWeierstrassP_coe ⟨x, hx⟩]
    exact fun H ↦ L.not_continuousAt_weierstrassP x hx H.continuousAt

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r q : ℚ
hq : cos (↑r * π) = ↑q
⊢ cos (↑(Int.fract r) * π) = ↑((-1) ^ ⌊r⌋ * q)

Tactic:
Int.fract

Goal state after:
r q : ℚ
hq : cos (↑r * π) = ↑q
⊢ cos (↑(r - ↑⌊r⌋) * π) = ↑((-1) ^ ⌊r⌋ * q)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
this : Meromorphic fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃
z w : ℂ
hw : w ∈ {z}ᶜ
hw' : w ∈ (↑L.lattice \ {z})ᶜ
⊢ ℘'[L] w ^ 2 - 4 * ℘[L] w ^ 3 + L.g₂ * ℘[L] w + L.g₃ =
    if w ∈ L.lattice then 0 else ℘'[L] w ^ 2 - 4 * ℘[L] w ^ 3 + L.g₂ * ℘[L] w + L.g₃

Tactic:
if_neg (by simp_all)

Goal state after:
L : PeriodPair
this : Meromorphic fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃
z w : ℂ
hw : w ∈ {z}ᶜ
hw' : w ∈ (↑L.lattice \ {z})ᶜ
⊢ ℘'[L] w ^ 2 - 4 * ℘[L] w ^ 3 + L.g₂ * ℘[L] w + L.g₃ = ℘'[L] w ^ 2 - 4 * ℘[L] w ^ 3 + L.g₂ * ℘[L] w + L.g₃
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ L.relation * id ^ 6 =ᶠ[𝓝 0] fun z ↦
    (℘'[L - 0] z * z ^ 3 - 2) ^ 2 - 4 * (℘[L - 0] z * z ^ 2 + 1) ^ 3 + L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
      L.g₃ * z ^ 6

Tactic:
filter_upwards [L.compl_lattice_sdiff_singleton_mem_nhds _] with z hz
  by_cases hz0 : z = 0
  · simp [hz0, relation]; norm_num
  replace hz : z ∉ L.lattice := by simp_all
  simp only [Pi.mul_apply, Pi.pow_apply, relation, ↓reduceIte, hz,
    ← ZeroMemClass.coe_zero L.lattice, L.derivWeierstrassPExcept_def, L.weierstrassPExcept_def]
  simp
  field

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

Goal state before:
pp: z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
m : Fin 2 → ℤ
⊢ ‖((↑(m 0) + ↑a) * ↑z + ↑(m 1) + ↑b)⁻¹‖ ≤ ?m.98

Tactic:
simpa [Real.rpow_neg_one, add_assoc] using
    summand_bound_of_mem_verticalStrip zero_le_one ![m 0 + a, m 1 + b] z.2 h0

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case negSucc
n : ℕ
⊢ fib (-[n+1] + 2) = fib -[n+1] + fib (-[n+1] + 1)

Tactic:
rw [negSucc_eq, ← Nat.cast_add_one, fib_neg_natCast]

Goal state after:
case negSucc
n : ℕ
⊢ fib (-↑(n + 1) + 2) = (-1) ^ (n + 1 + 1) * ↑(Nat.fib (n + 1)) + fib (-↑(n + 1) + 1)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: m : ℕ
n : ℤ
⊢ fib (↑m + n) + fib (↑m + n + 1) = fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib (↑(m + 1) + n)

Tactic:
rw [fib_natCast_add]

Goal state after:
m : ℕ
n : ℤ
⊢ fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib (↑m + n + 1) =
    fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib (↑(m + 1) + n)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: m : ℕ
n : ℤ
⊢ fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib (↑(m + 1) + n) =
    fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib ↑m * fib n + fib (↑m + 1) * fib (n + 1)

Tactic:
rw [fib_natCast_add]

Goal state after:
m : ℕ
n : ℤ
⊢ fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + (fib (↑(m + 1) - 1) * fib n + fib ↑(m + 1) * fib (n + 1)) =
    fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib ↑m * fib n + fib (↑m + 1) * fib (n + 1)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℤ
m : ℕ
⊢ fib (↑m + n) + fib (↑m + n + 1) = fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib (↑(m + 1) + n)

Tactic:
rw [fib_natCast_add]

Goal state after:
n : ℤ
m : ℕ
⊢ fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib (↑m + n + 1) =
    fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib (↑(m + 1) + n)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℤ
m : ℕ
⊢ fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib (↑(m + 1) + n) =
    fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib ↑m * fib n + fib (↑m + 1) * fib (n + 1)

Tactic:
rw [fib_natCast_add]

Goal state after:
n : ℤ
m : ℕ
⊢ fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + (fib (↑(m + 1) - 1) * fib n + fib ↑(m + 1) * fib (n + 1)) =
    fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib ↑m * fib n + fib (↑m + 1) * fib (n + 1)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℤ
⊢ fib (2 * (n + 1)) = fib (n + 1) * (2 * fib n + fib (n + 1))

Tactic:
fib_two_mul

Goal state after:
n : ℤ
⊢ fib (n + 1) * (2 * fib (n + 1 + 1) - fib (n + 1)) = fib (n + 1) * (2 * fib n + fib (n + 1))
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: this : fibRec.IsSolution ((fun n ↦ (√5)⁻¹ * φ ^ n) - fun n ↦ (√5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / √5 = ((fun n ↦ (√5)⁻¹ * φ ^ n) - fun n ↦ (√5)⁻¹ * ψ ^ n) x✝

Tactic:
Pi.sub_apply

Goal state after:
this : fibRec.IsSolution ((fun n ↦ (√5)⁻¹ * φ ^ n) - fun n ↦ (√5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / √5 = (√5)⁻¹ * φ ^ x✝ - (√5)⁻¹ * ψ ^ x✝
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: case hv
⊢ fibRec.IsSolution fun n ↦ (φ ^ n - ψ ^ n) / √5

Tactic:
suffices LinearRecurrence.IsSolution fibRec
        ((fun n ↦ (√5)⁻¹ * φ ^ n) - (fun n ↦ (√5)⁻¹ * ψ ^ n)) by
      convert! this
      rw [Pi.sub_apply]
      ring

Goal state after:
case hv
⊢ fibRec.IsSolution ((fun n ↦ (√5)⁻¹ * φ ^ n) - fun n ↦ (√5)⁻¹ * ψ ^ n)
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
⊢ ↑(Nat.fib (n + 1)) - φ * ↑(Nat.fib n) = ψ ^ n

Tactic:
repeat rw [coe_fib_eq]
  rw [mul_div, div_sub_div_same, mul_sub, ← pow_succ']
  ring_nf
  have nz : √5 ≠ 0 := by norm_num
  rw [← (mul_inv_cancel₀ nz).symm, one_mul]

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
⊢ ∫ (a : ℝ) in Ioi 0, a ^ (↑k + 1 - 1) * rexp (-(c * a)) ≠ 0

Tactic:
rw [key]

Goal state after:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
⊢ (1 / c) ^ (↑k + 1) * Gamma (↑k + 1) ≠ 0
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case hab
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := ⋯
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
⊢ u n ≤ u (c N)

Tactic:
exact hmono ncN.le

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case c0
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ 0 ≤ g ↑i

Tactic:
grw [gpos]; apply hg <;> grind

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case c0
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ 0 ≤ g (x - 1)

Tactic:
grw [gpos]; apply hg <;> grind

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ ∫ (x : ℝ) in ↑a..↑b, f x * g (x - 1) ≤ ∑ i ∈ Finset.Ico a b, f ↑i * g ↑i

Tactic:
by
  apply integral_le_sum_Ico_of_le (f := fun x ↦ f x * g x) hab
  · intro i hi x hx
    simp only [Nat.cast_add, Nat.cast_one, mem_Ico, ← Nat.add_one_le_iff] at hx hi
    rify at hi
    gcongr
    · grw [gpos]; apply hg <;> grind
    · grw [fpos]; apply hf <;> grind
    · apply hf <;> grind
    · apply hg <;> grind
  · apply Integrable.mono_measure _ (volume.restrict_mono_set Ico_subset_Icc_self)
    apply (hf.integrableOn_isCompact isCompact_Icc).mul_of_top_left
    apply MonotoneOn.memLp_isCompact isCompact_Icc
    intro _ _ _ _ _
    apply hg <;> grind

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case base
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ ∃ a, CofilteredClosureSmall.abstractCofilteredClosureRealization f a = { obj := f x, property := ⋯ }.obj

Tactic:
refine ⟨⟨0, ?_⟩,?_⟩
    · simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      exact ULift.up x
    · simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization,
        CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      rfl

Goal state after: