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

Goal state before:
pp: R : Type u_2
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
⊢ (fun x ↦ eval x P) =o[cobounded R] fun x ↦ eval x Q

Tactic:
by
  by_cases hP : P = 0
  · simp [hP]
  · refine isEquivalent_cobounded_leading_monomial.trans_isLittleO <|
      ((IsLittleO.const_mul_right ?_ ?_).const_mul_left _).trans_isEquivalent
        isEquivalent_cobounded_leading_monomial.symm
    · exact leadingCoeff_ne_zero.mpr (ne_zero_of_degree_gt h)
    · exact isLittleO_pow_pow_cobounded_of_lt (natDegree_lt_natDegree hP h)

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

Goal state before:
pp: P Q : ℤ[X]
h : Q.degree < P.degree
o : (fun x ↦ eval x Q) =o[cofinite] fun x ↦ eval x P
nr : ∀ᶠ (x : ℤ) in cofinite, ¬P.IsRoot x
key : ∀ᶠ (x : ℤ) in cofinite, ‖eval x Q‖ < ‖eval x P‖
⊢ {x | |eval x P| ≤ |eval x Q|}.Finite

Tactic:
eventually_cofinite,

Goal state after:
P Q : ℤ[X]
h : Q.degree < P.degree
o : (fun x ↦ eval x Q) =o[cofinite] fun x ↦ eval x P
nr : ∀ᶠ (x : ℤ) in cofinite, ¬P.IsRoot x
key : {x | ¬‖eval x Q‖ < ‖eval x P‖}.Finite
⊢ {x | |eval x P| ≤ |eval x Q|}.Finite
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hna : IsNonarchimedean ⇑v
c : ℝ
hc : 0 ≤ c
⊢ IsNonarchimedean (gaussNorm v c)

Tactic:
intro p q

Goal state after:
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hna : IsNonarchimedean ⇑v
c : ℝ
hc : 0 ≤ c
p q : R[X]
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
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
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
⊢ gaussNorm v c f = 0 ↔ f = 0

Tactic:
by
  refine ⟨?_, fun hf ↦ by simp [hf, vZero]⟩
  contrapose!
  intro hf
  apply ne_of_gt
  obtain ⟨n, hn⟩ := (MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero f).mp hf
  calc
  0 < v (f.coeff n) * ∏ i ∈ n.support, (c i) ^ (n i) := by
    apply mul_pos _ (by exact Finset.prod_pos fun i a ↦ (fun i ↦ pow_pos (hc i) (n i)) i)
    specialize h_eq_zero (f.coeff n)
    grind
  _ ≤ _ := le_gaussNorm v c f hbd n

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

Goal state before:
pp: case cons.refine_1
α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s✝ : Finset ι
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
j : ι
s : Finset ι
hj : j ∉ s
hs✝ : s.Nonempty
IH : ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)
⊢ g (∑ i ∈ s, f i) ≤ g (f j) → g (f j + ∑ i ∈ s, f i) ≤ g (f j)

Tactic:
intro h

Goal state after:
case cons.refine_1
α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s✝ : Finset ι
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
j : ι
s : Finset ι
hj : j ∉ s
hs✝ : s.Nonempty
IH : ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)
h : g (∑ i ∈ s, f i) ≤ g (f j)
⊢ g (f j + ∑ i ∈ s, f i) ≤ g (f j)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: a : ℂ
ha : a ≠ 0
b : ℂ
⊢ (C a * (X + C (a⁻¹ * b))).logMahlerMeasure = log ‖a‖ + log⁺ ‖a⁻¹ * b‖

Tactic:
logMahlerMeasure_C_mul ha (X_add_C_ne_zero (a⁻¹ * b)),

Goal state after:
a : ℂ
ha : a ≠ 0
b : ℂ
⊢ log ‖a‖ + (X + C (a⁻¹ * b)).logMahlerMeasure = log ‖a‖ + log⁺ ‖a⁻¹ * b‖
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case cons.refine_2
α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s✝ : Finset ι
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
j : ι
s : Finset ι
hj : j ∉ s
hs✝ : s.Nonempty
IH : ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)
⊢ g (f j) ≤ g (∑ i ∈ s, f i) → ∃ a ∈ s, g (f j + ∑ i ∈ s, f i) ≤ g (f a)

Tactic:
intro h

Goal state after:
case cons.refine_2
α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s✝ : Finset ι
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
j : ι
s : Finset ι
hj : j ∉ s
hs✝ : s.Nonempty
IH : ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)
h : g (f j) ≤ g (∑ i ∈ s, f i)
⊢ ∃ a ∈ s, g (f j + ∑ i ∈ s, f i) ≤ g (f a)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : multiplicity (↑p) m % 2 = 1
⊢ multiplicity (↑p) m % 2 ≠ 0

Tactic:
Hpv

Goal state after:
m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : multiplicity (↑p) m % 2 = 1
⊢ 1 ≠ 0
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case neg
x : ℝ*
h : ¬∃ r, x.IsSt r
⊢ 0 = stdPart x

Tactic:
simp_rw [isSt_iff] at h

Goal state after:
case neg
x : ℝ*
h : ¬∃ r, 0 ≤ ArchimedeanClass.mk x ∧ stdPart x = r
⊢ 0 = stdPart x
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
⊢ Irrational x⁻¹⁻¹

Tactic:
by rwa [inv_inv]

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

Goal state before:
pp: x y : ℝ*
⊢ x.InfinitePos → ¬y.Infinitesimal → y < 0 → (x * y).InfiniteNeg

Tactic:
by
  rw [← infinitePos_neg, ← neg_pos, neg_mul_eq_mul_neg, ← infinitesimal_neg]
  exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos

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

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

Tactic:
refine lt_of_le_of_lt ?_ (agmSequences_fst_lt_agm_of_pos_of_ne hx hy hn 0)

Goal state after:
x✝ y✝ x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
h : x < y
⊢ x ≤ (x.agmSequences y 0).1
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case e'_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
⊢ ∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ = -2 * (↑n + 1) * ∫ (x : ℝ) in -1..1, u₂ x * v₂' x

Tactic:
← integral_const_mul

Goal state after:
case e'_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
⊢ ∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ = ∫ (x : ℝ) in -1..1, -2 * (↑n + 1) * (u₂ x * v₂' x)
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z ↦ (z.im ^ n) ^ 2) = fun z ↦ z.im ^ (2 * n)

Tactic:
simp only [pow_mul']

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

Goal state before:
pp: case refine_1
p : ℝ
⊢ binEntropy p < log 2 → p ≠ 2⁻¹

Tactic:
rintro h rfl
    simp at h

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

Goal state before:
pp: case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
⊢ ¬DifferentiableAt ℝ (deriv (qaryEntropy q)) p

Tactic:
intro h

Goal state after:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
h : DifferentiableAt ℝ (deriv (qaryEntropy q)) p
⊢ False
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ ‖(1 - x ^ 2) ^ n * cos (x * (π / 2))‖ ≤ 1

Tactic:
rw [norm_eq_abs, abs_mul, abs_pow]

Goal state after:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ |1 - x ^ 2| ^ n * |cos (x * (π / 2))| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ (a • x + b • y)⁻¹ʳ = (a • (conjSqrt x) 1 + b • (conjSqrt x) z)⁻¹ʳ

Tactic:
by
        rw [conjSqrt_conjSqrt_ringInverse _ _ xpos, conjSqrt_one x xpos.nonneg]

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

Goal state before:
pp: case succ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
m : ℕ
⊢ s - 1 ≠ -↑(m + 1)

Tactic:
rw [Ne, sub_eq_iff_eq_add]
      convert! hs m using 2
      push_cast
      ring

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

Goal state before:
pp: case pos
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : 0 < t
⊢ 0 ≤ p.rpowIntegrand₁₂ t x

Tactic:
rw [rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ht']
    refine mul_nonneg hx ?_
    exact rpowIntegrand₀₁_nonneg (by grind) (by grind) hx

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case refine_1
m : ℕ
⊢ ↑(1 / 2) ≠ -↑m

Tactic:
rw [← ofReal_natCast, ← ofReal_neg, ne_eq, ofReal_inj]

Goal state after:
case refine_1
m : ℕ
⊢ ¬1 / 2 = -↑m
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b x < y ↔ x < b ^ y

Tactic:
by
  rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hx]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: 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₀' : 0 < r₂
⊢ -log b r₁⁻¹ ≤ -log b r₂⁻¹

Tactic:
neg_le_neg_iff

Goal state after:
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₀' : 0 < r₂
⊢ log b r₂⁻¹ ≤ log b r₁⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b y < logb b x

Tactic:
rw [← logb_abs b y, ← logb_abs b x]

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 x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hxy : x < y
⊢ log y / log b < log x / log b

Tactic:
div_lt_div_right_of_neg (log_neg b_pos b_lt_one)

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

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hy : 0 < y
⊢ log x / log b < log y / log b ↔ y < x

Tactic:
div_lt_div_right_of_neg (log_neg b_pos b_lt_one)

Goal state after:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hy : 0 < y
⊢ log y < log x ↔ y < x
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: x : ℝ
⊢ -1 ≤ -mulExpNegMulSq 1 (-x)

Tactic:
neg_le_neg_iff

Goal state after:
x : ℝ
⊢ mulExpNegMulSq 1 (-x) ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: 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

Tactic:
rw [← logb_abs b y, ← logb_abs b x]

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.MulExpNegMulSq

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

Tactic:
apply le_trans (dist_triangle (mulExpNegMulSq ε x) 0 (mulExpNegMulSq ε y))

Goal state after:
ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ dist (ε.mulExpNegMulSq x) 0 + dist 0 (ε.mulExpNegMulSq y) ≤ 2 * (√ε)⁻¹
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed → μ.InnerRegularWRT IsCompact IsClosed

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
⊢ μ.InnerRegularWRT IsCompact IsClosed
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
⊢ μ.InnerRegularWRT IsCompact IsClosed → μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
⊢ μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed → μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed → μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
⊢ μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case inr
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
hP'0 : ¬P' = 0
⊢ 0 < const

Tactic:
exact lt_max_of_lt_right
        (toReal_pos ((Measure.measure_univ_ne_zero).mpr hP'0) (by finiteness))

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a b : ℕ
hn : n ≠ 0
⊢ n.nthRoot a < b ↔ a < b ^ n

Tactic:
simp only [← not_le, le_nthRoot_iff hn]

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

Goal state before:
pp: a b c z : ℂ
hc : ∀ (k : ℕ), c ≠ -↑k
⊢ ₂F₁ a b c z / Gamma c = a.regularizedGaussHGFun b c z

Tactic:
regularizedGaussHGFun,

Goal state after:
a b c z : ℂ
hc : ∀ (k : ℕ), c ≠ -↑k
⊢ ₂F₁ a b c z / Gamma c = (a.regularizedGaussHGFunSeries b c).sum z
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : StandardBorelSpace α
inst✝ : Finite α
n : ℕ
n_equiv : α ≃ Fin n
⊢ ∃ n, Nonempty (α ≃ᵐ ↑(range fun x ↦ ↑↑x))

Tactic:
refine ⟨n, ⟨PolishSpace.Equiv.measurableEquiv (n_equiv.trans ?_)⟩⟩

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : StandardBorelSpace α
inst✝ : Finite α
n : ℕ
n_equiv : α ≃ Fin n
⊢ Fin n ≃ ↑(range fun x ↦ ↑↑x)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘'[L - ↑l₀] z = ℘'[L] z + 2 / (z - ↑l₀) ^ 3

Tactic:
rw [← L.derivWeierstrassPExcept_sub l₀, sub_add_cancel]

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

Goal state before:
pp: ⊢ (fun n ↦ ↑n !) ~[atTop] fun n ↦ √(2 * ↑n * π) * (↑n / rexp 1) ^ n

Tactic:
apply Asymptotics.isEquivalent_of_tendsto_one

Goal state after:
⊢ Tendsto ((fun n ↦ ↑n !) / fun n ↦ √(2 * ↑n * π) * (↑n / rexp 1) ^ n) atTop (𝓝 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ P = T ℝ ↑n → sumNodes n c P = sumNodes n c (T ℝ ↑n)

Tactic:
intro h

Goal state after:
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h : P = T ℝ ↑n
⊢ sumNodes n c P = sumNodes n c (T ℝ ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ¬↑((Equiv.prodCongrLeft fun x ↦
              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
            (Prod.map some id p)).2 =
      l₀
hpx : ‖↑p.2 - x‖ ≠ 0
hxz : z ≠ x
⊢ ‖((↑((Equiv.prodCongrLeft fun x ↦
                      { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                        right_inv := ⋯ })
                    (Prod.map some id p)).1 +
              1) *
            (↑((Equiv.prodCongrLeft fun x ↦
                        { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                          right_inv := ⋯ })
                      (Prod.map some id p)).2 -
                x) ^
              (-(↑((Equiv.prodCongrLeft fun x ↦
                          { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                            right_inv := ⋯ })
                        (Prod.map some id p)).1 +
                  2)) -
          Nat.rec
            (↑((Equiv.prodCongrLeft fun x ↦
                      { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                        right_inv := ⋯ })
                    (Prod.map some id p)).2 ^
              (-2))
            (fun n n_ih ↦ 0)
            ((Equiv.prodCongrLeft fun x ↦
                  { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
                (Prod.map some id p)).1) *
        (z - x) ^
          ((Equiv.prodCongrLeft fun x ↦
                { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
              (Prod.map some id p)).1‖ =
    ‖↑p.1 + 2‖ * ‖↑p.2 - x‖ ^ (-3 - ↑p.1) * ‖z - x‖ ^ (p.1 + 1)

Tactic:
by
        norm_num; ring_nf; simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P.leadingCoeff = 2 ^ (n - 1)
hPdeg' : ↑n ≤ P.degree
⊢ P.coeff n = 2 ^ (n - 1)

Tactic:
by
    replace hPdeg' : P.degree = n := eq_of_le_of_ge hPdeg hPdeg'
    rwa [leadingCoeff, natDegree_eq_of_degree_eq_some hPdeg'] at hP

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ sumNodes n (iterateDerivativeC n k x) P = eval x ((⇑derivative)^[k] P)

Tactic:
simp_rw [sumNodes, iterateDerivativeC]
  have h₁ : P.degree < (Finset.range (n + 1)).card := by
    rw [Finset.card_range]; grw [hP]; norm_cast; simp
  convert!
    (Lagrange.eval_iterate_derivative_eq_sum (strictAntiOn_node n).injOn h₁
        (show k < _ by simp [hk]) x).symm
  rw [Finset.mul_sum]
  grind [Nat.range_succ_eq_Iic, Nat.card_Iic]

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

Goal state before:
pp: case pos
L : PeriodPair
z : ℂ
hz : z ∈ (↑L.lattice \ {0})ᶜ
hz0 : z = 0
⊢ (L.relation * id ^ 6) 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

pp: case neg
L : PeriodPair
z : ℂ
hz : z ∈ (↑L.lattice \ {0})ᶜ
hz0 : ¬z = 0
⊢ (L.relation * id ^ 6) 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:
· simp [hz0, relation]; norm_num

Goal state after:
case neg
L : PeriodPair
z : ℂ
hz : z ∈ (↑L.lattice \ {0})ᶜ
hz0 : ¬z = 0
⊢ (L.relation * id ^ 6) 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
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ Odd 3

Tactic:
by decide

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x → ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
intro h

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)
Module: Mathlib.Tactic.NormNum.NatFib

Goal state before:
pp: n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ a * (2 * fib (n + 1) - a) = a'

Tactic:
H.2,

Goal state after:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ a * (2 * b - a) = a'
Module: Mathlib.Tactic.NormNum.NatFib

Goal state before:
pp: n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ fib (n + 1) ^ 2 + a ^ 2 = b'

Tactic:
H.2,

Goal state after:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ b ^ 2 + a ^ 2 = b'
Module: Mathlib.Tactic.NormNum.NatFib

Goal state before:
pp: n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ fib (n' + 1) = b'

Tactic:
rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h2]

Goal state after:
Module: Mathlib.Tactic.NormNum.NatFib

Goal state before:
pp: n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
⊢ fib (n + 1) ^ 2 + a ^ 2 = a'

Tactic:
H.2,

Goal state after:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
⊢ b ^ 2 + a ^ 2 = a'