mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case hb
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ 0 < p * (1 - p)

Tactic:
· simp_all only [mul_pos_iff_of_pos_left, sub_pos]

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

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

Tactic:
simp [hk.ne']

Goal state after:
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
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
hint_V : IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b
hint_inv : IntervalIntegrable (fun x ↦ x⁻¹ * δ) volume a b
⊢ ‖∫ (x : ℝ) in a..b, x⁻¹ • (f x - V)‖ ≤ |∫ (x : ℝ) in a..b, x⁻¹ * δ|

Tactic:
by
        apply norm_integral_le_abs_of_norm_le
        · exact (ae_restrict_mem measurableSet_uIoc).mono fun x hx ↦ by
            have hx_pos : 0 < x :=
              lt_of_lt_of_le (lt_min ha hb) (uIoc_subset_uIcc hx).1
            rw [norm_smul, Real.norm_eq_abs, abs_of_pos (inv_pos.2 hx_pos)]
            exact mul_le_mul_of_nonneg_left (h x hx) (inv_nonneg.2 hx_pos.le)
        · exact hint_inv

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
hδ : δ > 0
hev : ∀ᶠ (x : ℝ) in 𝓝[>] 0, dist (f x) L < δ
⊢ ∀ᶠ (t : ℝ) in 𝓝[{x | (fun t ↦ 0 < t) x}] 0, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - L‖ ≤ δ

Tactic:
Filter.Eventually,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
hδ : δ > 0
hev : {x | dist (f x) L < δ} ∈ 𝓝[>] 0
⊢ ∀ᶠ (t : ℝ) in 𝓝[{x | (fun t ↦ 0 < t) x}] 0, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - L‖ ≤ δ
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
⊢ ∀ x ∈ spectrum ℝ z, id x ≠ 0 ∨ 0 ≤ -1

Tactic:
#adaptation_note /-- Before nightly-2026-06-04, this was just `grind. -/

Goal state after:
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
⊢ ∀ x ∈ spectrum ℝ z, id x ≠ 0 ∨ 0 ≤ -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
⊢ ∀ x ∈ spectrum ℝ z, x ≠ 0 ∨ 0 ≤ -1

Tactic:
#adaptation_note /-- Before nightly-2026-06-04, this was just `grind. -/

Goal state after:
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
⊢ ∀ x ∈ spectrum ℝ z, x ≠ 0 ∨ 0 ≤ -1
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
h_lim :
  ∀ᶠ (x : ℝ) in 𝓝[>] 0,
    ∀ᶠ (y : ℝ) in atTop, dist (intervalIntegral g (x, y).1 (x, y).2 volume) (log (b / a) • (L - R)) < ε / 2
hε : ε > 0
⊢ ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε

Tactic:
Filter.Eventually,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
h_lim :
  {x | ∀ᶠ (y : ℝ) in atTop, dist (intervalIntegral g (x, y).1 (x, y).2 volume) (log (b / a) • (L - R)) < ε / 2} ∈ 𝓝[>] 0
hε : ε > 0
⊢ ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: ⊢ Differentiable ℂ fun s ↦ (2 * (2 * ↑π) ^ (-s))⁻¹ * (Gamma s)⁻¹

Tactic:
refine (Differentiable.inv ?_ (by simp)).mul differentiable_one_div_Gamma

Goal state after:
⊢ Differentiable ℂ fun s ↦ 2 * (2 * ↑π) ^ (-s)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

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

Tactic:
div_eq_iff_mul_eq (by positivity),

Goal state after:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : (-γ + ↑(harmonic n)) * ↑n ! = deriv Gamma (↑n + 1)
⊢ deriv Gamma (↑n + 1) = ↑n ! * (-γ + ↑(harmonic n))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t x ∂μ
a : A
ha : 0 ≤ a
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₀₁ x 0 = 0
⊢ IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₀₁ t) a) (Ioi 0) μ

Tactic:
exact integrableOn_cfcₙ measurableSet_Ioi _ bound a hf hmapzero hbound hbound_finite_integral

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₁₂ x 0 = 0
⊢ IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₁₂ t) a) (Ioi 0) μ

Tactic:
exact integrableOn_cfcₙ measurableSet_Ioi _ bound a hf hmapzero hbound hbound_finite_integral

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₁₂ x 0 = 0
r : ℝ
hr : r ∈ quasispectrum ℝ a
⊢ ↑(r.toNNReal.nnrpow p) = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t r ∂μ

Tactic:
have hr' : 0 ≤ r := by grind

Goal state after:
A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₁₂ x 0 = 0
r : ℝ
hr : r ∈ quasispectrum ℝ a
hr' : 0 ≤ r
⊢ ↑(r.toNNReal.nnrpow p) = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t r ∂μ
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: n : ℕ
⊢ ↑n.log2 ≤ logb 2 ↑n

Tactic:
by
  calc (Nat.log2 n : ℝ) = Nat.log 2 n := mod_cast Nat.log2_eq_log_two
  _ ≤ Real.logb 2 n := natLog_le_logb _ _

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

Goal state before:
pp: L : PeriodPair
s : Set ℂ
hs : s ⊆ ↑L.lattice
⊢ IsClosed s

Tactic:
by
  convert!
    L.isClosed_lattice.isClosedMap_subtype_val _ (isClosed_discrete (α := L.lattice) ((↑) ⁻¹' s))
  convert! Set.image_preimage_eq_inter_range.symm using 1
  simpa

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

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

Tactic:
rw [← sub_nonneg] at h ⊢

Goal state after:
n a b : ℕ
hb : b ≠ 0
h : 0 ≤ (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
⊢ 0 ≤ ↑a ^ (n + 1) + ↑n * ↑b * ↑b ^ n - (↑n + 1) * ↑a * ↑b ^ n
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: case pos
n : ℕ
ε : ℝ
h : n ≠ 0 ∧ 0 < ε
⊢ 0 < ↑n * (min ε.toNNReal 2 / 4) ^ n

pp: case neg
n : ℕ
ε : ℝ
h : ¬(n ≠ 0 ∧ 0 < ε)
⊢ 0 < 1

Tactic:
· cases h
    positivity

Goal state after:
case neg
n : ℕ
ε : ℝ
h : ¬(n ≠ 0 ∧ 0 < ε)
⊢ 0 < 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n : ℕ
hn : n ≠ 0
a : ℕ
x✝ : 1 ≠ 0
⊢ a < (nthRoot 1 a + 1) ^ 1

Tactic:
| =>

Goal state after:
n : ℕ
hn : n ≠ 0
a : ℕ
x✝ : 1 ≠ 0
⊢ a < (nthRoot 1 a + 1) ^ 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n✝ : ℕ
hn✝ : n✝ ≠ 0
a n : ℕ
hn : n + 2 ≠ 0
⊢ a < ((n + 2).nthRoot a + 1) ^ (n + 2)

Tactic:
| =>

Goal state after:
n✝ : ℕ
hn✝ : n✝ ≠ 0
a n : ℕ
hn : n + 2 ≠ 0
⊢ a < ((n + 2).nthRoot a + 1) ^ (n + 2)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e'_6
L : PeriodPair
⊢ ℘[L] = ℘[L - L.ω₁ / 2]

Tactic:
rw [L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]

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

Goal state before:
pp: case neg.hd
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖l‖ ^ 3

Tactic:
· exact Real.rpow_pos_of_pos (by simpa) _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

Tactic:
by_cases hα : Countable α
  · cases finite_or_infinite α
    · obtain ⟨n, h_nonempty_equiv⟩ := exists_nat_measurableEquiv_range_coe_fin_of_finite α
      refine ⟨_, ?_, h_nonempty_equiv⟩
      exact (Set.finite_range ((↑) : Fin n → ℝ)).measurableSet
    · refine ⟨_, ?_, measurableEquiv_range_coe_nat_of_infinite_of_countable α⟩
      exact Nat.isClosedEmbedding_coe_real.isClosed_range.measurableSet
  · refine
      ⟨univ, MeasurableSet.univ,
        ⟨(PolishSpace.measurableEquivOfNotCountable hα ?_ : α ≃ᵐ (univ : Set ℝ))⟩⟩
    rw [countable_coe_iff]
    exact Cardinal.not_countable_real

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

Goal state before:
pp: case e'_9
x : ℝ
⊢ x.sigmoid * (1 - x.sigmoid) = -(rexp (-x) * -1) / (1 + rexp (-x)) ^ 2

Tactic:
← sigmoid_neg,

Goal state after:
case e'_9
x : ℝ
⊢ x.sigmoid * (-x).sigmoid = -(rexp (-x) * -1) / (1 + rexp (-x)) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ ℘[L] (z - ↑l) = ℘[L] z

Tactic:
by
  rw [← L.weierstrassP_add_coe _ l, sub_add_cancel]

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

Goal state before:
pp: L : PeriodPair
⊢ HasSumLocallyUniformly (fun l z ↦ -2 / (z - ↑l) ^ 3) ℘'[L]

Tactic:
convert! L.hasSumLocallyUniformly_derivWeierstrassPExcept (L.ω₁ / 2) using 3 with l z

Goal state after:
case e'_5
L : PeriodPair
l : ↥L.lattice
z : ℂ
⊢ -2 / (z - ↑l) ^ 3 = if ↑l = L.ω₁ / 2 then 0 else -2 / (z - ↑l) ^ 3

case e'_6
L : PeriodPair
⊢ ℘'[L] = ℘'[L - L.ω₁ / 2]
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inr.hderiv
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
x : ℝ
hx : x ∈ Ioo a b
⊢ Icc a b ∈ 𝓝 x

Tactic:
exact Icc_mem_nhds hx.1 hx.2

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

Goal state before:
pp: n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
this :
  (∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I)) * (Complex.exp (↑k / (2 * ↑n) * ↑π * I))⁻¹ *
      (Complex.exp (↑k / ↑n * ↑π * I) - 1) =
    (-1) ^ k - 1
hf : ∀ {s a b t : ℂ}, s * a⁻¹ * b = t → a ≠ 0 → b ≠ 0 → s = a / b * t
⊢ Complex.exp (↑k / ↑n * ↑π * I) - 1 ≠ 0

Tactic:
grind [exp_sub_one_ne_zero]

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ (cexp (-(↑q * ↑π) * I))

Tactic:
by
  simpa using isIntegral_exp_rat_mul_pi_mul_I (-q)

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

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
z : ℂ := Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz : z = Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz₂ : Complex.exp (↑k / ↑n * ↑π * I) = z ^ 2
⊢ z ^ 2 - 1 ≠ 0 ∧ 1 - z ^ 2 ≠ 0

Tactic:
grind [exp_sub_one_ne_zero]

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

Goal state before:
pp: k n : ℕ
hn : n ≠ 0
⊢ cos (↑↑n * (↑k * π / ↑n)) = (-1) ^ ↑k

Tactic:
convert! Real.cos_int_mul_pi k using 2

Goal state after:
k n : ℕ
hn : n ≠ 0
⊢ ↑↑n * (↑k * π / ↑n) = ↑↑k * π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((↑k + 1) * π / (↑n + 1)) = x
⊢ eval x (U ℝ ↑n) = 0

Tactic:
suffices (U ℝ n).eval x * sin ((k + 1) * π / (n + 1)) = 0 by
      refine (mul_eq_zero_iff_right (ne_of_gt (sin_pos_of_pos_of_lt_pi (by positivity) ?_))).mp this
      field_simp
      norm_cast
      grind

Goal state after:
case refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((↑k + 1) * π / (↑n + 1)) = x
⊢ eval x (U ℝ ↑n) * sin ((↑k + 1) * π / (↑n + 1)) = 0
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case max.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
⊢ FilteredClosureSmall.abstractFilteredClosureRealization f
      ⟨(Max.max n m).succ, ⋯.mpr (FilteredClosureSmall.InductiveStep.max ⋯ ⋯ x y)⟩ =
    {
        obj :=
          max (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
            (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩),
        property := ⋯ }.obj

Tactic:
simp only [FilteredClosureSmall.abstractFilteredClosureRealization]

Goal state after:
case max.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
⊢ (FilteredClosureSmall.bundledAbstractFilteredClosure f (Max.max n m).succ).snd
      (⋯.mpr (FilteredClosureSmall.InductiveStep.max ⋯ ⋯ x y)) =
    max ((FilteredClosureSmall.bundledAbstractFilteredClosure f n).snd x)
      ((FilteredClosureSmall.bundledAbstractFilteredClosure f m).snd y)
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case coeq.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
g g' :
  FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩ ⟶
    FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩
⊢ FilteredClosureSmall.abstractFilteredClosureRealization f
      ⟨(Max.max n m).succ, ⋯.mpr (FilteredClosureSmall.InductiveStep.coeq ⋯ ⋯ x y g g')⟩ =
    { obj := coeq g g', property := ⋯ }.obj

Tactic:
simp only [FilteredClosureSmall.abstractFilteredClosureRealization]

Goal state after:
case coeq.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
g g' :
  FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩ ⟶
    FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩
⊢ (FilteredClosureSmall.bundledAbstractFilteredClosure f (Max.max n m).succ).snd
      (⋯.mpr (FilteredClosureSmall.InductiveStep.coeq ⋯ ⋯ x y g g')) =
    coeq g g'
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
I : Type v₁
inst✝¹ : Category.{v₂, v₁} I
F : I ⥤ C
inst✝ : HasColimit F
i : I
⊢ 𝟙 (limit (F.op ⋙ coyoneda)) ≫ limit.π (F.op ⋙ coyoneda) (op i) = limit.π (F.op ⋙ coyoneda) (op i)

Tactic:
Category.id_comp

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
I : Type v₁
inst✝¹ : Category.{v₂, v₁} I
F : I ⥤ C
inst✝ : HasColimit F
i : I
⊢ limit.π (F.op ⋙ coyoneda) (op i) = limit.π (F.op ⋙ coyoneda) (op i)
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ 𝟙 (limit (F.op ⋙ yoneda.obj A)) ≫ limit.π (F.op ⋙ yoneda.obj A) (op i) = limit.π (F.op ⋙ yoneda.obj A) (op i)

Tactic:
Category.id_comp

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ limit.π (F.op ⋙ yoneda.obj A) (op i) = limit.π (F.op ⋙ yoneda.obj A) (op i)
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
I : Type v₁
inst✝¹ : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝ : HasColimit F
i : I
⊢ 𝟙 (limit (F.rightOp ⋙ coyoneda)) ≫ limit.π (F.rightOp ⋙ coyoneda) i = limit.π (F.rightOp ⋙ coyoneda) i

Tactic:
Category.id_comp

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
I : Type v₁
inst✝¹ : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝ : HasColimit F
i : I
⊢ limit.π (F.rightOp ⋙ coyoneda) i = limit.π (F.rightOp ⋙ coyoneda) i
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ 𝟙 (limit (F.rightOp ⋙ yoneda.obj A)) ≫ limit.π (F.rightOp ⋙ yoneda.obj A) i = limit.π (F.rightOp ⋙ yoneda.obj A) i

Tactic:
Category.id_comp

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ limit.π (F.rightOp ⋙ yoneda.obj A) i = limit.π (F.rightOp ⋙ yoneda.obj A) i