mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
this : HasDerivAt (fun x ↦ ↑π ^ (-x / 2)) (↑π ^ (-1 / 2) * log ↑π * (-1 / 2)) 1
⊢ ↑π ^ (-1 / 2) * (log ↑π * -1 / 2) = -log ↑π / 2 / ↑√π

Tactic:
mul_neg_one,

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
this : HasDerivAt (fun x ↦ ↑π ^ (-x / 2)) (↑π ^ (-1 / 2) * log ↑π * (-1 / 2)) 1
⊢ ↑π ^ (-1 / 2) * (-log ↑π / 2) = -log ↑π / 2 / ↑√π
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : 1 ≤ r₂
⊢ -↑(Nat.clog b ⌈r₁⁻¹⌉₊) ≤ ↑(Nat.log b ⌊r₂⌋₊)

Tactic:
exact (neg_nonpos.mpr (Int.natCast_nonneg _)).trans (Int.natCast_nonneg _)

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

Goal state before:
pp: a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ (logb (a / b) c)⁻¹ = (logb a c)⁻¹ - (logb b c)⁻¹

Tactic:
simp_rw [inv_logb]; exact logb_div h₁ h₂

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

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

Tactic:
by
  rw [logb, log_rpow hx, logb, mul_div_assoc]

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ (∫⁻ (x : X), ↑(f x) ∂μ).toReal = (∫⁻ (a : X), ENNReal.ofReal ↑(f a) ∂μ).toReal

Tactic:
simp only [ENNReal.ofReal_coe_nnreal]

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

Goal state before:
pp: b : ℝ
n : ℕ
⊢ (fun x ↦ logb b x ^ n) =o[atTop] id

Tactic:
by
  rw [Asymptotics.isLittleO_iff_tendsto']
  · simpa using tendsto_pow_logb_div_mul_add_atTop 1 0 n one_ne_zero
  · filter_upwards [eventually_ne_atTop (0 : ℝ)] with x h₁ h₂ using (h₁ h₂).elim

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

Goal state before:
pp: case inl
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ ℝ
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) ⊥ ≤ ∫ (x : X), f x ∂μ
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) ⊥ (𝓝 (∫ (x : X), f x ∂μ))

pp: case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Tactic:
· simp only [tendsto_bot]

Goal state after:
case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < μ A
K' : Set α
hpK' : p K'
hK'_lt : μ K'ᶜ < μ A - r
⊢ ∃ K, p K ∧ K ⊆ A ∧ μ (A \ K) < μ A - r

Tactic:
refine ⟨K' ∩ A, hpq K' A hpK' hA, inter_subset_right, ?_⟩

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < μ A
K' : Set α
hpK' : p K'
hK'_lt : μ K'ᶜ < μ A - r
⊢ μ (A \ (K' ∩ A)) < μ A - r
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ

Tactic:
have key := h _ (f.add_norm_nonneg)

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
key : limsup (fun i ↦ ∫ (x : X), (f + const X ‖f‖) x ∂μs i) L ≤ ∫ (x : X), (f + const X ‖f‖) x ∂μ
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
exact innerRegularWRT_isCompact_closure P

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

Goal state before:
pp: case inl
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ ℝ
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) ⊥
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) ⊥ (𝓝 (∫ (x : X), f x ∂μ))

pp: case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Tactic:
· simp only [tendsto_bot]

Goal state after:
case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
this : P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) fun s ↦ MeasurableSet s ∧ P s ≠ ∞
x✝ : Set α
⊢ MeasurableSet x✝ → P x✝ ≠ ∞

Tactic:
exact fun _ ↦ measure_ne_top P _

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

Goal state before:
pp: case inr.hinf
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L

Tactic:
have key := h _ (f.add_norm_nonneg)

Goal state after:
case inr.hinf
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
key : ∫ (x : X), (f + const X ‖f‖) x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), (f + const X ‖f‖) x ∂μs i) L
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a b : ℕ
hb : b ≠ 0
⊢ (n + 1) * a * b ^ n ≤ a ^ (n + 1) + n * b * b ^ n

Tactic:
#adaptation_note /-- Prior to nightly-2026-04-06, this was
  ```
  have := (Commute.all (b : ℤ) (a - b)).pow_add_mul_le_add_pow_of_sq_nonneg
    (by positivity) (sq_nonneg _) (sq_nonneg _) (by grind) (n + 1)
  grind
  ```
  -/

Goal state after:
n a b : ℕ
hb : b ≠ 0
⊢ (n + 1) * a * b ^ n ≤ a ^ (n + 1) + n * b * b ^ n
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
this : ∀ {ε : ℝ}, 0 < ε → ε ≤ 2 → ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ μ.toSphere (ball x ε)
hε₂ : ¬ε ≤ 2
⊢ 0 < min ε 2

Tactic:
by simp [hε]

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

Goal state before:
pp: case h
a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
n : ℕ
hn : (b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) + 1 ≤ n
h' : regularizedHGFunCoeff a b n = 0
⊢ False

Tactic:
regularizedHGFunCoeff_eq_zero_iff

Goal state after:
case h
a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
n : ℕ
hn : (b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) + 1 ≤ n
h' : (∃ j ∈ a, ∃ k < n, j = -↑k) ∨ ∃ j ∈ b, ∃ m, j + ↑n = -↑m
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: x : ℝ
⊢ HasDerivAt sigmoid (x.sigmoid * (1 - x.sigmoid)) x

Tactic:
by
  convert! (hasDerivAt_neg' x |>.exp.const_add 1 |>.inv <| by positivity) using 1
  rw [← sigmoid_neg, ← sigmoid_mul_rexp_neg x, sigmoid_def]
  field [sq]

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ log ↑(n✝ + 1)! - (log √(2 * ↑(n✝ + 1)) + log ((↑(n✝ + 1) / rexp 1) ^ (n✝ + 1))) =
    log ↑(n✝ + 1)! - 1 / 2 * log (2 * ↑(n✝ + 1)) - ↑(n✝ + 1) * log (↑(n✝ + 1) / rexp 1)

pp: case succ.hx
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) ≠ 0

pp: case succ.hy
n✝ : ℕ
⊢ (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0

pp: case succ.hx
n✝ : ℕ
⊢ ↑(n✝ + 1)! ≠ 0

pp: case succ.hy
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) * (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0

Tactic:
sqrt_eq_rpow,

Goal state after:
case succ
n✝ : ℕ
⊢ log ↑(n✝ + 1)! - (log ((2 * ↑(n✝ + 1)) ^ (1 / 2)) + log ((↑(n✝ + 1) / rexp 1) ^ (n✝ + 1))) =
    log ↑(n✝ + 1)! - 1 / 2 * log (2 * ↑(n✝ + 1)) - ↑(n✝ + 1) * log (↑(n✝ + 1) / rexp 1)

case succ.hx
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) ≠ 0

case succ.hy
n✝ : ℕ
⊢ (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0

case succ.hx
n✝ : ℕ
⊢ ↑(n✝ + 1)! ≠ 0

case succ.hy
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) * (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ deriv ℘[L - L.ω₁ / 2] x = ℘'[L - L.ω₁ / 2] x

Tactic:
L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept (L.ω₁ / 2) (x := x) (by simp [hx])

Goal state after:
case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ ℘'[L - L.ω₁ / 2] x = ℘'[L - L.ω₁ / 2] x
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
⊢ sin θ ∈ {-1, -1 / 2, 0, 1 / 2, 1}

Tactic:
convert! ← niven (θ := θ - π / 2) ?_ ?_ using 1

Goal state after:
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
⊢ cos (θ - π / 2) = sin θ

case convert_1
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
⊢ ∃ r, θ - π / 2 = ↑r * π

case convert_2
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
⊢ ∃ q, cos (θ - π / 2) = ↑q
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case convert_1
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
⊢ ∃ r, θ - π / 2 = ↑r * π

Tactic:
exact hθ.imp' (· - 1 / 2) (by intros; push_cast; linarith)

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
n : ℕ
inst✝ : DecidableEq α
⊢ 0 ∈ box n ↔ n = 0

Tactic:
cases n <;> simp [box_succ_eq_sdiff]

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

Goal state before:
pp: case r_le
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖x + ↑↑r - x‖ < ‖↑l - x‖

Tactic:
intro l hl
      simpa [-Metric.mem_closedBall, mem_closedBall_iff_norm]
        using Set.subset_compl_comm.mp hr ⟨l.2, hl⟩

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

Goal state before:
pp: case a
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ z.re ^ 2 / z.im ^ 2 + 1 ≤
    { coe := { re := A, im := B }, coe_im_pos := h }.re ^ 2 / { coe := { re := A, im := B }, coe_im_pos := h }.im ^ 2 +
      1

Tactic:
add_le_add_iff_right,

Goal state after:
case a
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ z.re ^ 2 / z.im ^ 2 ≤
    { coe := { re := A, im := B }, coe_im_pos := h }.re ^ 2 / { coe := { re := A, im := B }, coe_im_pos := h }.im ^ 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
⊢ r z ≤ ‖↑c * ↑z + ↑d‖

Tactic:
by
  have H1 : √(r1 z) ≤ √((c * z.re + d) ^ 2 + (c * z.im) ^ 2) :=
    (Real.sqrt_le_sqrt_iff (by positivity)).mpr (r1_aux_bound _ _ hd)
  simpa only [r, norm_def, normSq_apply, add_re, re_ofReal_mul, coe_re, ofReal_re, ← pow_two,
    add_im, im_ofReal_mul, coe_im, ofReal_im, add_zero, min_le_iff] using Or.inr H1

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

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

Tactic:
norm_eq_max_natAbs,

Goal state after:
x : Fin 2 → ℤ
hx : ↑(max (x 0).natAbs (x 1).natAbs) ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
⊢ x 0 ≠ 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

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

Tactic:
norm_eq_max_natAbs,

Goal state after:
x : Fin 2 → ℤ
hx : ↑(max (x 0).natAbs (x 1).natAbs) ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
⊢ x 1 ≠ 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z * ‖x‖ ≤ ‖↑(x 0) * ↑z + ↑(x 1)‖

Tactic:
norm_eq_max_natAbs,

Goal state after:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z * ↑(max (x 0).natAbs (x 1).natAbs) ≤ ‖↑(x 0) * ↑z + ↑(x 1)‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
⊢ IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

Tactic:
cases k.even_or_odd
  case inl hk₂ => exact .inr (isLocalMax_T_real hn hk₀ hk₁ hk₂)
  case inr hk₂ => exact .inl (isLocalMin_T_real hn hk₁ hk₂)

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

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Complex.sin (↑π * x) ≠ 0

Tactic:
by
  apply Complex.sin_ne_zero_iff.2
  intro k
  nth_rw 2 [mul_comm]
  exact Injective.ne (mul_right_injective₀ (ofReal_ne_zero.mpr Real.pi_ne_zero)) (by aesop)

Goal state after:
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:
by
        rw [fib_natCast_add]; grind

Goal state after:
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:
by
        rw [fib_natCast_add]; grind

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Fibonacci

Goal state before:
pp: h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
⊢ |ψ / φ| < 1

Tactic:
by
    rw [abs_div, div_lt_one <| by positivity, abs_of_pos goldenRatio_pos, abs_lt]
    ring_nf
    bound

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

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
n : ℕ
| iteratedDerivWithin k (fun t ↦ cotTerm t n) ℍₒ z

Tactic:
rw [eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet k n (by simp [hz])]

Goal state after:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
n : ℕ
| (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑n + 1)) ^ (-1 - ↑k) + (z - (↑n + 1)) ^ (-1 - ↑k))) z
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: 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 : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
n : ℕ
hn : ‖u (c n) / ↑(c n) - l‖ ≤ ε * ‖1‖
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
⊢ u (c n) - ↑(c n) * l ≤ ε * ↑(c n)

Tactic:
have cnpos : 0 < c n := cnpos'

Goal state after:
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 : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
n : ℕ
hn : ‖u (c n) / ↑(c n) - l‖ ≤ ε * ‖1‖
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
e : H →L[ℂ] H
he : IsStarProjection e
S : VonNeumannAlgebra H
⊢ (∀ x ∈ S.commutant, e ∘SL x ∘SL e = x ∘SL e) → ∀ x ∈ S.commutant, e ∘SL x ∘SL e = e ∘SL x

Tactic:
← mul_def

Goal state after:
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
e : H →L[ℂ] H
he : IsStarProjection e
S : VonNeumannAlgebra H
⊢ (∀ x ∈ S.commutant, e * (x * e) = x * e) → ∀ x ∈ S.commutant, e * (x * e) = e * x
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ g ≫ cokernel.π (f ≫ g) = 0

Tactic:
← assoc,

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g) ≫ cokernel.π (f ≫ g) = 0
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case hbc
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))
⊢ ↑(c N) - ↑(c (N - 1)) ≤ ε * ↑(c (N - 1))

Tactic:
· linarith only [IcN]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: 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
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
n : ℕ
hn : ‖u (c n) / ↑(c n) - l‖ ≤ ε * ‖1‖
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
⊢ ↑(c n) * l - u (c n) ≤ ε * ↑(c n)

Tactic:
have cnpos : 0 < c n := cnpos'

Goal state after:
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
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
n : ℕ
hn : ‖u (c n) / ↑(c n) - l‖ ≤ ε * ‖1‖
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ i ∈ range N with j < c ^ i, (1 - c⁻¹)⁻¹ ^ 2 * (1 / (c ^ i) ^ 2) ≤ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2

Tactic:
by
      rw [← mul_sum, ← mul_div_assoc']
      gcongr
      exact sum_div_pow_sq_le_div_sq N hj hc

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
T : Type u₃
inst✝⁴ : Category.{v₃, u₃} T
L : C ⥤ T
R : D ⥤ T
C' : Type u₄
inst✝³ : Category.{v₄, u₄} C'
D' : Type u₅
inst✝² : Category.{v₅, u₅} D'
T' : Type u₆
inst✝¹ : Category.{v₆, u₆} T'
L' : C' ⥤ T'
R' : D' ⥤ T'
F₁ : C ⥤ C'
F₂ : D ⥤ D'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝ : IsIso β
X : Comma L' R'
Y : Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β))
⊢ L'.map Y.left.hom ≫
      ((Comma.map α β).obj { left := Y.left.right, right := Y.right.right, hom := Hom.right Y.hom }).hom =
    X.hom ≫ R'.map Y.right.hom

Tactic:
simpa using congrFun (congrArg CategoryStruct.comp (StructuredArrow.w Y.hom))
        (β.app Y.right.right)

Goal state after: