mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
x : E
hx : x ∈ closedBall x₀ ↑r
t : ℝ
ht : t ∈ Icc tmin tmax
t' : ℝ
⊢ t' ∈ Icc tmin tmax → (α x hx).compProj t' = picard f (↑t₀) x (α x hx).compProj t'

Tactic:
ht'

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
x : E
hx : x ∈ closedBall x₀ ↑r
t : ℝ
ht : t ∈ Icc tmin tmax
t' : ℝ
ht' : t' ∈ Icc tmin tmax
⊢ (α x hx).compProj t' = picard f (↑t₀) x (α x hx).compProj t'
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
t : ↑(Icc tmin tmax)
⊢ dist (((next hf hx)^[0] α).toFun t) (((next hf hx)^[0] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ 0 / ↑0! * dist α β

Tactic:
simpa using!
      ContinuousMap.dist_apply_le_dist (f := toContinuousMap α) (g := toContinuousMap β) _

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
t' : ℝ
⊢ t' ∈ Ioc (min ↑t₀ ↑t) (max ↑t₀ ↑t) →
    ‖f t' (((next hf hx)^[n] α).compProj t') - f t' (((next hf hx)^[n] β).compProj t')‖ ≤
      ↑K ^ (n + 1) * |t' - ↑t₀| ^ n / ↑n ! * dist α β

Tactic:
ht'

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
t' : ℝ
ht' : t' ∈ Ioc (min ↑t₀ ↑t) (max ↑t₀ ↑t)
⊢ ‖f t' (((next hf hx)^[n] α).compProj t') - f t' (((next hf hx)^[n] β).compProj t')‖ ≤
    ↑K ^ (n + 1) * |t' - ↑t₀| ^ n / ↑n ! * dist α β
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
⊢ t' ∈ Ioo a b → f t' = g t'

Tactic:
ht'

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
⊢ f t' = g t'
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0) ↔ P.degree < Q.degree

Tactic:
refine ⟨fun h => ?_, div_tendsto_atTop_zero_of_degree_lt P Q⟩

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)
⊢ P.degree < Q.degree
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atTop atTop

Tactic:
by
  have hQ : Q ≠ 0 := fun h => by
    simp only [h, div_zero, leadingCoeff_zero] at hpos
    exact hpos.false
  rw [← natDegree_lt_natDegree_iff hQ] at hdeg
  refine (isEquivalent_atTop_div P Q).symm.tendsto_atTop ?_
  apply Tendsto.const_mul_atTop hpos
  apply tendsto_zpow_atTop_atTop
  lia

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

Goal state before:
pp: p : ℂ[X]
this :
  ∑ x ∈ p.support, ‖p.coeff x‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
t : AddCircle (2 * π)
ht : ↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t = (toAddCircle p) t
⊢ ‖(toAddCircle p) t‖ ^ 2 = ‖↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t‖ ^ 2

Tactic:
← ht

Goal state after:
p : ℂ[X]
this :
  ∑ x ∈ p.support, ‖p.coeff x‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
t : AddCircle (2 * π)
ht : ↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t = (toAddCircle p) t
⊢ ‖↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t‖ ^ 2 =
    ‖↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t‖ ^ 2
Module: Mathlib.RingTheory.PowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
⊢ gaussNorm v c f = ⨆ i, v ((coeff i) f) * c ^ i

Tactic:
refine Equiv.iSup_congr (Finsupp.uniqueEquiv ()) ?_
  intro x
  simp only [coeff, Finsupp.uniqueEquiv_apply, PUnit.default_eq_unit, Finsupp.prod_pow,
    Finset.univ_unique, Finset.prod_singleton, show (Finsupp.single () (x PUnit.unit)) = x by grind]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
hbd : HasGaussNorm v c f
t : ℕ
⊢ v ((coeff t) f) * c ^ t ≤ gaussNorm v c f

Tactic:
by
  rw [gaussNorm_eq]
  apply le_ciSup hbd

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ t : ℝ
hf : ContinuousOn (uncurry f) (uIcc t₀ t ×ˢ u)
hα : ∀ t' ∈ uIcc t₀ t, HasDerivWithinAt α (f t' (α t')) (uIcc t₀ t) t'
hmap : MapsTo α (uIcc t₀ t) u
t' : ℝ
⊢ t' ∈ Ioo (min t₀ t) (max t₀ t) → HasDerivWithinAt α (f t' (α t')) (Ioi t') t'

Tactic:
ht'

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ t : ℝ
hf : ContinuousOn (uncurry f) (uIcc t₀ t ×ˢ u)
hα : ∀ t' ∈ uIcc t₀ t, HasDerivWithinAt α (f t' (α t')) (uIcc t₀ t) t'
hmap : MapsTo α (uIcc t₀ t) u
t' : ℝ
ht' : t' ∈ Ioo (min t₀ t) (max t₀ t)
⊢ HasDerivWithinAt α (f t' (α t')) (Ioi t') t'
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
⊢ eval x P ≤ 0

Tactic:
suffices 0 ≤ (-P).eval x by apply neg_nonneg.mp; rwa [← eval_neg]
  refine zero_le_eval_of_roots_le_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_
  · rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
  · rwa [leadingCoeff_neg, neg_nonneg]

Goal state after:
Module: Mathlib.Analysis.RCLike.BoundedContinuous

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : PseudoEMetricSpace E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
g : C(E, ℝ)
⊢ (∃ x, (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) x ∈ A ∧ (toContinuousMapₐ ℝ) x = g) →
    ∃ x ∈ A, (toContinuousMapStarₐ 𝕜) x = (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) g

pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : PseudoEMetricSpace E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
g : C(E, ℝ)
⊢ (∃ x ∈ A, (toContinuousMapStarₐ 𝕜) x = (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) g) →
    ∃ x, (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) x ∈ A ∧ (toContinuousMapₐ ℝ) x = g

Tactic:
· intro ⟨x, hxA, hxg⟩
    use (@ofRealAm 𝕜 _).compLeftContinuousBounded ℝ lipschitzWith_ofReal x, hxA
    ext a
    simp only [toContinuousMapStarₐ_apply_apply, AlgHom.compLeftContinuousBounded_apply_apply,
      ofRealAm_coe, AlgHom.compLeftContinuous_apply_apply, algebraMap.coe_inj]
    exact DFunLike.congr_fun hxg a

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : PseudoEMetricSpace E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
g : C(E, ℝ)
⊢ (∃ x ∈ A, (toContinuousMapStarₐ 𝕜) x = (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) g) →
    ∃ x, (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) x ∈ A ∧ (toContinuousMapₐ ℝ) x = g
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

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

Tactic:
calc
    _  = (v (coeff i₀ f) * i₀.prod (c · ^ ·)) * (v (coeff j₀ g) * j₀.prod (c · ^ ·)) := by
          rw [← hi₀, ← hj₀]
    _ = v (coeff i₀ f) * v (coeff j₀ g) * ((i₀ + j₀).prod (c · ^ ·)) := by
          have hprod : (i₀ + j₀).prod (c · ^ ·) = i₀.prod (c · ^ ·) * j₀.prod (c · ^ ·) := by
            simp [Finsupp.prod_add_index', pow_add]
          rw [hprod]; ring
    _ = v (coeff i₀ f * coeff j₀ g) * (i₀ + j₀).prod (c · ^ ·) := by rw [vMulEq]
    _ = v (coeff (i₀ + j₀) (f * g)) * (i₀ + j₀).prod (c · ^ ·) := by
      rw [antidiagonal_dominant v f g i₀ j₀ vna vMulEq vNeg hdom']
    _ ≤ gaussNorm v c (f * g) := le_gaussNorm v c (f * g) hbfg (i₀ + j₀)

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

Goal state before:
pp: n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ ∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z x ≤ ∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z p.roots

Tactic:
gcongr with a
      · exact le_max_left 1 ‖a‖
      · exact hx.1

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

Goal state before:
pp: n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False

Tactic:
have hdivn : (D : ℤ) ^ n ∣ N ^ n := Dvd.intro_left m hxr

Goal state after:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : ↑D ^ n ∣ N ^ n
⊢ False
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))⁻¹
⊢ Irrational x

Tactic:
exact h.of_inv.of_pow _

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

Goal state before:
pp: x : ℝ*
⊢ (-x).st = -x.st

Tactic:
by_cases h : Infinite x
  · rw [h.st_eq, (infinite_neg.2 h).st_eq, neg_zero]
  · exact (isSt_st' (not_infinite_neg h)).unique (isSt_st' h).neg

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

Goal state before:
pp: case h₀
x : ℝ
⊢ ¬Real.arctan x = π / 2

Tactic:
← ne_eq

Goal state after:
case h₀
x : ℝ
⊢ Real.arctan x ≠ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
⊢ log ((1 + z * I) * (1 - z * I)⁻¹) = log ((1 + z * I) / (1 - z * I))

pp: z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
⊢ (1 + z * I).arg + (1 - z * I)⁻¹.arg ∈ Set.Ioc (-π) π

Tactic:
div_eq_mul_inv

Goal state after:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
⊢ log ((1 + z * I) * (1 - z * I)⁻¹) = log ((1 + z * I) * (1 - z * I)⁻¹)

z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
⊢ (1 + z * I).arg + (1 - z * I)⁻¹.arg ∈ Set.Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : p < 0
⊢ -p * log p < (1 - p) * log (1 - p)

Tactic:
by_cases hp' : p < -1

Goal state after:
case pos
p : ℝ
hp : p < 0
hp' : p < -1
⊢ -p * log p < (1 - p) * log (1 - p)

case neg
p : ℝ
hp : p < 0
hp' : ¬p < -1
⊢ -p * log p < (1 - p) * log (1 - p)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case pos
p : ℝ
hp : p < 0
hp' : p < -1
⊢ -p * log p < (1 - p) * log (1 - p)

pp: case neg
p : ℝ
hp : p < 0
hp' : ¬p < -1
⊢ -p * log p < (1 - p) * log (1 - p)

Tactic:
· have : log p < log (1 - p) := by
      rw [← log_neg_eq_log]
      exact log_lt_log (Left.neg_pos_iff.mpr hp) (by linarith)
    nlinarith [log_pos_of_lt_neg_one hp']

Goal state after:
case neg
p : ℝ
hp : p < 0
hp' : ¬p < -1
⊢ -p * log p < (1 - p) * log (1 - p)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt

Goal state before:
pp: A : Type u_1
inst✝¹⁰ : PartialOrder A
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : Algebra ℝ A
inst✝⁴ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : SeparatelyContinuousMul A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
c a : A
hc : IsStrictlyPositive c
⊢ (conjSqrt c) ((conjSqrt c⁻¹ʳ) a) = a

Tactic:
by
  grind [conjSqrt_ringInverse_conjSqrt _ _ hc.ringInverse]

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
⊢ Monotone fun a ↦ a ^ p

Tactic:
by
  let q : ℝ≥0 := ⟨p, hp.1⟩
  change Monotone (fun a : A => a ^ (q : ℝ))
  obtain hq | hq := eq_zero_or_pos q
  · rw [hq]
    intro a b hab
    by_cases ha : 0 ≤ a
    · have hb : 0 ≤ b := ha.trans hab
      simp [CFC.rpow_zero a, CFC.rpow_zero b]
    · have : a ^ (0 : ℝ) = 0 := cfc_apply_of_not_predicate a ha
      simp [this]
  · simp_rw [← CFC.nnrpow_eq_rpow hq]
    exact monotone_nnrpow hp

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

Goal state before:
pp: n : ℕ
⊢ 0 < ↑(harmonic (n + 1)) - log (↑(n + 1) + 1) - (↑(harmonic n) - log (↑n + 1))

Tactic:
sub_sub_sub_comm,

Goal state after:
n : ℕ
⊢ 0 < ↑(harmonic (n + 1)) - ↑(harmonic n) - (log (↑(n + 1) + 1) - log (↑n + 1))
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
⊢ 0 < ↑(harmonic n) - log ↑n - (↑(harmonic (n + 1)) - log ↑(n + 1))

Tactic:
sub_sub_sub_comm,

Goal state after:
case inr
n : ℕ
hn : n > 0
⊢ 0 < ↑(harmonic n) - ↑(harmonic (n + 1)) - (log ↑n - log ↑(n + 1))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

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

Tactic:
rcases eq_or_lt_of_le' hx with hx_zero | _
  case inl =>
    push _ ∈ _ at hp
    simp [hx_zero, Real.zero_rpow (by linarith)]
  case inr =>
    have : ∫ t in Ioi 0, rpowIntegrand₀₁ p t 1 ≠ 0 :=
      ne_of_gt <| integral_rpowIntegrand₀₁_one_pos hp
    rw [integral_rpowIntegrand₀₁_eq_rpow_mul_const hp hx, mul_comm, mul_assoc, mul_inv_cancel₀
      this, mul_one]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ cfcₙ (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p.rpowIntegrand₀₁ t) b

Tactic:
calc
    _ = t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • a) := by
      rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht a ha]
    _ ≤ t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • b) := by
      gcongr
      unfold rpowIntegrand₀₁
      simp only [Real.one_rpow, one_mul, inv_one]
      refine CFC.monotoneOn_one_sub_one_add_inv_real
        (?_ : 0 ≤ t⁻¹ • a) (?_ : 0 ≤ t⁻¹ • b) (by gcongr)
      all_goals positivity
    _ = cfcₙ (rpowIntegrand₀₁ p t) b := by
      rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht b hb]

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

Goal state before:
pp: ε y : ℝ
⊢ HasDerivAt ε.mulExpNegMulSq (rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))) y

Tactic:
nth_rw 1 [← one_mul (exp (-(ε * y * y)))]
  apply HasDerivAt.mul (hasDerivAt_id' y)
  apply HasDerivAt.exp (HasDerivAt.congr_deriv (HasDerivAt.neg
    (HasDerivAt.mul (HasDerivAt.const_mul ε (hasDerivAt_id' y)) (hasDerivAt_id' y))) (by ring))

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

Goal state before:
pp: case inr
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
⊢ Tendsto (fun x ↦ |logb b x|) atTop atTop

Tactic:
exact (this (b := -b) (by simp [hb, neg_eq_iff_eq_neg]) (by linarith +splitNe)).congr (by simp)

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

Goal state before:
pp: b c : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
⊢ c = 0 ∨ Tendsto (Norm.norm ∘ logb b) atTop atTop

Tactic:
or_iff_not_imp_left

Goal state after:
b c : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
⊢ ¬c = 0 → Tendsto (Norm.norm ∘ logb b) atTop atTop
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 →ᵇ ℝ
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Tactic:
rcases eq_or_neBot L with rfl | hL

Goal state after:
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 ∂μ))

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.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 → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Tactic:
rcases eq_or_neBot L with rfl | hL

Goal state after:
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 ∂μ))

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.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : N ≤ n
⊢ 0 ≤ ε * (‖g‖ * ‖g‖)

Tactic:
exact (mul_nonneg (le_of_lt hε) (mul_self_nonneg (norm g)))

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
⊢ ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1)) =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))

Tactic:
apply congr_arg fun z => ENNReal.ofReal p * z

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
⊢ ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1)) =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case h₁
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
⊢ ↑((Equiv.neg ↥L.lattice) l) = l₀ ↔ ↑l = -l₀

pp: case h₃
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
a✝ : ¬↑l = -l₀
⊢ 1 / (-z - ↑((Equiv.neg ↥L.lattice) l)) ^ 2 - 1 / ↑((Equiv.neg ↥L.lattice) l) ^ 2 = 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2

Tactic:
· simp [neg_eq_iff_eq_neg]

Goal state after:
case h₃
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
a✝ : ¬↑l = -l₀
⊢ 1 / (-z - ↑((Equiv.neg ↥L.lattice) l)) ^ 2 - 1 / ↑((Equiv.neg ↥L.lattice) l) ^ 2 = 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e'_5.h₁
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
⊢ -↑l = l₀ ↔ ↑l = -l₀

pp: case e'_5.h₃
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
a✝ : ¬↑l = -l₀
⊢ -2 / (↑l - z) ^ 3 = -2 / -(z - ↑l) ^ 3

Tactic:
· simp [neg_eq_iff_eq_neg]

Goal state after:
case e'_5.h₃
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
a✝ : ¬↑l = -l₀
⊢ -2 / (↑l - z) ^ 3 = -2 / -(z - ↑l) ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ := { carrier := {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
⊢ Submodule.span ℤ {L.ω₁, L.ω₂} ≤ AddSubgroup.toIntSubmodule G

Tactic:
Submodule.span_le

Goal state after:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ := { carrier := {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
⊢ {L.ω₁, L.ω₂} ⊆ ↑(AddSubgroup.toIntSubmodule G)