mathlib-initiative/mathlib-tactics huggingface dataset:
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₀ : E
a r L K : ℝ≥0
inst✝ : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
⊢ ∃ L',
    ∀ (x y : E) (hx : x ∈ closedBall x₀ ↑r) (hy : y ∈ closedBall x₀ ↑r) (α β : FunSpace t₀ x₀ r L),
      IsFixedPt (next hf hx) α → IsFixedPt (next hf hy) β → dist α β ≤ ↑L' * dist x y

Tactic:
obtain ⟨m, C, h⟩ := exists_contractingWith_iterate_next hf
  let L' := (∑ i ∈ Finset.range m, (K * max (tmax - t₀) (t₀ - tmin)) ^ i / i !) * (1 - C)⁻¹
  have hL' : 0 ≤ L' := by
    have : 0 ≤ max (tmax - t₀) (t₀ - tmin) := le_max_of_le_left <| sub_nonneg_of_le t₀.2.2
    positivity
  refine ⟨.mk L' hL', fun x y hx hy α β hα hβ ↦ ?_⟩
  rw [NNReal.coe_mk]
  apply le_of_tendsto_of_tendsto' (b := Filter.atTop) _ _ <|
    dist_iterate_iterate_next_le_of_lipschitzWith hf hy α (h y hy).2
  · apply Filter.Tendsto.comp (y := 𝓝 β) (tendsto_const_nhds.dist Filter.tendsto_id)
    rw [h y hy |>.fixedPoint_unique (hβ.iterate m)]
    exact h y hy |>.tendsto_iterate_fixedPoint α
  · nth_rw 1 [← hα, dist_next_next]
    apply Filter.Tendsto.mul_const
    apply Filter.Tendsto.const_mul
    convert! hasSum_geometric_of_lt_one C.2 (h y hy).1 |>.tendsto_sum_nat
    simp [NNReal.coe_sub <| le_of_lt (h y hy).1, NNReal.coe_one]

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

Goal state before:
pp: case coe
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
n : ℕ
hf : ContDiffOn ℝ (↑↑n) (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ ContDiffOn ℝ (↑↑n) (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
| coe n =>

Goal state after:
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
p q : R[X]
h✝¹ : p ≠ 0
h✝ : q ≠ 0
hpq : p + q ≠ 0
i : ℕ
a✝ : i ∈ (p + q).support
⊢ v ((p + q).coeff i) * c ^ i ≤ max (v (p.coeff i)) (v (q.coeff i)) * c ^ i

Tactic:
by
    rw [coeff_add]
    gcongr
    exact hna (p.coeff i) (q.coeff i)

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

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedRing A
p : A[X]
⊢ p.supNorm ∈ Set.range fun x ↦ ‖p.coeff x‖

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝ : SeminormedRing A
p : A[X]
⊢ ∃ y, ‖p.coeff y‖ = p.supNorm
Module: Mathlib.Analysis.Polynomial.Norm

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedRing A
p : A[X]
⊢ p.supNorm ∈ upperBounds (Set.range fun x ↦ ‖p.coeff x‖)

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝ : SeminormedRing A
p : A[X]
⊢ ∀ (a : ℕ), ‖p.coeff a‖ ≤ p.supNorm
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
vMul : ∀ (a b : R), v (a * b) ≤ v a * v b
vna : IsNonarchimedean v
vZero : v 0 = 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
t : σ →₀ ℕ
k : (σ →₀ ℕ) × (σ →₀ ℕ)
hk : (Finset.antidiagonal t).Nonempty → k ∈ Finset.antidiagonal t
hsum : v (∑ a ∈ Finset.antidiagonal t, (coeff a.1) f * (coeff a.2) g) ≤ v ((coeff k.1) f * (coeff k.2) g)
⊢ k.1 + k.2 = t

Tactic:
simpa using

Goal state after:
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
vMul : ∀ (a b : R), v (a * b) ≤ v a * v b
vna : IsNonarchimedean v
vZero : v 0 = 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
t : σ →₀ ℕ
k : (σ →₀ ℕ) × (σ →₀ ℕ)
hk : (Finset.antidiagonal t).Nonempty → k ∈ Finset.antidiagonal t
hsum : v (∑ a ∈ Finset.antidiagonal t, (coeff a.1) f * (coeff a.2) g) ≤ v ((coeff k.1) f * (coeff k.2) g)
⊢ k.1 + k.2 = t
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
h : Even P.natDegree
hlc' : 0 ≤ (P.comp (-X)).leadingCoeff
this : 0 < eval (-x) (P.comp (-X))
⊢ 0 < eval x P

Tactic:
simpa using

Goal state after:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
h : Even P.natDegree
hlc' : 0 ≤ (P.comp (-X)).leadingCoeff
this : 0 < eval (-x) (P.comp (-X))
⊢ 0 < eval x P
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
h : Odd P.natDegree
hlc' : 0 ≤ -(P.comp (-X)).leadingCoeff
this : eval (-x) (P.comp (-X)) < 0
⊢ eval x P < 0

Tactic:
simpa using

Goal state after:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
h : Odd P.natDegree
hlc' : 0 ≤ -(P.comp (-X)).leadingCoeff
this : eval (-x) (P.comp (-X)) < 0
⊢ eval x P < 0
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case pos
p q : ℂ[X]
hpq : p * q = 0
⊢ (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure

Tactic:
simpa using

Goal state after:
case pos
p q : ℂ[X]
hpq : p * q = 0
⊢ p = 0 ∨ q = 0
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inr
α : Type u_3
S : Type u_4
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
na : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
H : ∀ {a b : α}, f a ≠ f b → f a > f b → f (a + b) = max (f a) (f b)
hab : ¬f a > f b
⊢ f (a + b) = max (f a) (f b)

Tactic:
simpa using

Goal state after:
case inr
α : Type u_3
S : Type u_4
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
na : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
H : ∀ {a b : α}, f a ≠ f b → f a > f b → f (a + b) = max (f a) (f b)
hab : ¬f a > f b
⊢ f (a + b) = max (f a) (f b)
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inl
α : Type u_3
S : Type u_4
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
na : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
h : f (a + b + -b) ≤ f (a + b)
⊢ max (f a) (f b) ≤ f (a + b)

Tactic:
simpa using

Goal state after:
case inl
α : Type u_3
S : Type u_4
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
na : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
h : f (a + b + -b) ≤ f (a + b)
⊢ f a ≤ f (a + b)
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: α : Type u_3
S : Type u_4
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
na : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
h : f (a + b + -b) ≤ f (-b)
⊢ f (-b) < f (a + b + -b)

Tactic:
simpa using

Goal state after:
α : Type u_3
S : Type u_4
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
na : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
h : f (a + b + -b) ≤ f (-b)
⊢ f (-b) < f a
Module: Mathlib.Analysis.RCLike.ContinuousMap

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RCLike 𝕜
f g : C(X, ℝ)
hfg : realToRCLike 𝕜 f = realToRCLike 𝕜 g
x : X
⊢ f x = g x

Tactic:
simpa using

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RCLike 𝕜
f g : C(X, ℝ)
hfg : realToRCLike 𝕜 f = realToRCLike 𝕜 g
x : X
⊢ f x = g x
Module: Mathlib.Analysis.Rat.NatSqrt.Real

Goal state before:
pp: x prec : ℕ
h : 0 < prec
this✝¹ : x.ratSqrt prec ^ 2 ≤ ↑x
this✝ : ↑(x.ratSqrt prec) ^ 2 ≤ ↑x
this : √(↑(x.ratSqrt prec) ^ 2) ≤ √↑x
⊢ 0 ≤ ↑(x.ratSqrt prec)

Tactic:
simpa using

Goal state after:
x prec : ℕ
h : 0 < prec
this✝¹ : x.ratSqrt prec ^ 2 ≤ ↑x
this✝ : ↑(x.ratSqrt prec) ^ 2 ≤ ↑x
this : √(↑(x.ratSqrt prec) ^ 2) ≤ √↑x
⊢ 0 ≤ x.ratSqrt prec
Module: Mathlib.Analysis.Rat.NatSqrt.Real

Goal state before:
pp: x prec : ℕ
h : 0 < prec
this✝¹ : ↑x < (x.ratSqrt prec + 1 / ↑prec) ^ 2
this✝ : ↑x < ↑((x.ratSqrt prec + 1 / ↑prec) ^ 2)
this : √↑x < √(↑(x.ratSqrt prec + 1 / ↑prec) ^ 2)
⊢ 0 ≤ ↑(x.ratSqrt prec)

Tactic:
simpa using

Goal state after:
x prec : ℕ
h : 0 < prec
this✝¹ : ↑x < (x.ratSqrt prec + 1 / ↑prec) ^ 2
this✝ : ↑x < ↑((x.ratSqrt prec + 1 / ↑prec) ^ 2)
this : √↑x < √(↑(x.ratSqrt prec + 1 / ↑prec) ^ 2)
⊢ 0 ≤ x.ratSqrt prec
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ ⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖ = √((⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) ^ 2)

Tactic:
rw [sqrt_sq]

Goal state after:
p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ 0 ≤ ⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_2
x : ℝ*
r : ℝ
h : x.IsSt r
s : ℝ
hs : s < r
⊢ coeRingHom s ≤ x

Tactic:
simpa using

Goal state after:
case refine_2
x : ℝ*
r : ℝ
h : x.IsSt r
s : ℝ
hs : s < r
⊢ ↑s ≤ x
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_3
x : ℝ*
r : ℝ
h : x.IsSt r
s : ℝ
hs : s > r
⊢ x ≤ coeRingHom s

Tactic:
simpa using

Goal state after:
case refine_3
x : ℝ*
r : ℝ
h : x.IsSt r
s : ℝ
hs : s > r
⊢ x ≤ ↑s
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: ⊢ Irrational √2

Tactic:
simpa using

Goal state after:
⊢ Irrational √2
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
⊢ x ≠ 1

Tactic:
simpa using

Goal state after:
x : ℝ
h : Irrational x
⊢ x ≠ 1
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_1
x : ℝ*
h : x.InfinitePos
⊢ 0 < x ∧ ArchimedeanClass.mk x < 0

pp: case refine_2
x : ℝ*
x✝ : 0 < x ∧ ArchimedeanClass.mk x < 0
r : ℝ
hx : 0 < x
hx' : ArchimedeanClass.mk x < 0
⊢ ↑r < x

Tactic:
· have hx : 0 < x := h 0
    refine ⟨h 0, fun n ↦ ?_⟩
    simpa [abs_of_pos hx] using! h n

Goal state after:
case refine_2
x : ℝ*
x✝ : 0 < x ∧ ArchimedeanClass.mk x < 0
r : ℝ
hx : 0 < x
hx' : ArchimedeanClass.mk x < 0
⊢ ↑r < x
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (x - ↑q)

Tactic:
simpa using

Goal state after:
q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (x + -↑q)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (↑q - x)

Tactic:
simpa using

Goal state after:
q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (↑q + -x)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: q : ℚ
x : ℝ
h : Irrational (x - ↑q)
⊢ Irrational (x + ↑(-q))

Tactic:
simpa using

Goal state after:
q : ℚ
x : ℝ
h : Irrational (x - ↑q)
⊢ Irrational (x + -↑q)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: q : ℚ
x : ℝ
h : Irrational (↑q - x)
⊢ Irrational (↑q + -x)

Tactic:
simpa using

Goal state after:
q : ℚ
x : ℝ
h : Irrational (↑q - x)
⊢ Irrational (↑q + -x)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (x - ↑m)

Tactic:
simpa using

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (x - ↑m)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑m - x)

Tactic:
simpa using

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑m - x)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
⊢ ↑a * x = -↑b

Tactic:
simpa using

Goal state after:
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
⊢ ↑a * x + ↑b = 0
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → dist (sqrt (x * y)) ((x + y) / 2) ≤ dist x y / 2
h : ¬x ≤ y
⊢ dist (sqrt (x * y)) ((x + y) / 2) ≤ dist x y / 2

Tactic:
simpa using

Goal state after:
case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → dist (sqrt (x * y)) ((x + y) / 2) ≤ dist x y / 2
h : ¬x ≤ y
⊢ dist ((x + y) / 2) (sqrt (x * y)) ≤ dist x y / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
h : x ≠ y
n m : ℕ
⊢ (x.agmSequences y n).1 < (x.agmSequences y m).2

Tactic:
suffices ∀ {k}, (agmSequences x y k).1 < (agmSequences x y k).2 by
    obtain h | h := le_total n m
    · exact (agmSequences_fst_monotone h).trans_lt this
    · exact this.trans_le (agmSequences_snd_antitone h)

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

Goal state before:
pp: case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → x.agm y ≤ max x y
h : ¬x ≤ y
⊢ x.agm y ≤ max x y

Tactic:
simpa using

Goal state after:
case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → x.agm y ≤ max x y
h : ¬x ≤ y
⊢ x.agm y ≤ x ∨ x.agm y ≤ y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → min x y ≤ x.agm y
h : ¬x ≤ y
⊢ min x y ≤ x.agm y

Tactic:
simpa using

Goal state after:
case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → min x y ≤ x.agm y
h : ¬x ≤ y
⊢ x ≤ x.agm y ∨ y ≤ x.agm y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
⊢ x.agm y = (sqrt (x * y)).agm ((x + y) / 2)

Tactic:
simpa using

Goal state after:
x y : ℝ≥0
⊢ x.agm y = (sqrt (x * y)).agm ((x + y) / 2)
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
this : ∀ {x y : ℝ≥0}, 0 < x → 0 < y → x ≠ y → x < y → min x y < x.agm y
h : ¬x < y
⊢ min x y < x.agm y

Tactic:
simpa using

Goal state after:
case inr
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
this : ∀ {x y : ℝ≥0}, 0 < x → 0 < y → x ≠ y → x < y → min x y < x.agm y
h : ¬x < y
⊢ x < x.agm y ∨ y < x.agm y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
hn : x ≠ y
this : ∀ {x y : ℝ≥0}, x ≠ y → x < y → x.agm y < max x y
h : ¬x < y
⊢ x.agm y < max x y

Tactic:
simpa using

Goal state after:
case inr
x y : ℝ≥0
hn : x ≠ y
this : ∀ {x y : ℝ≥0}, x ≠ y → x < y → x.agm y < max x y
h : ¬x < y
⊢ x.agm y < x ∨ x.agm y < y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

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

Tactic:
max_eq_right h.le

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun n ↦ (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan

Tactic:
by
  have := ((hasSum_taylorSeries_log (z := z * I) (by simpa)).add
    (hasSum_taylorSeries_neg_log (z := z * I) (by simpa))).mul_left (-I / 2)
  simp_rw [← add_div, ← add_one_mul, hasSum_arctan_aux hz] at this
  replace := (Nat.divModEquiv 2).symm.hasSum_iff.mpr this
  dsimp [Function.comp_def] at this
  simp_rw [← mul_comm 2 _] at this
  refine this.prod_fiberwise fun k => ?_
  dsimp only
  convert! hasSum_fintype (_ : Fin 2 → ℂ) using 1
  rw [Fin.sum_univ_two, Fin.val_zero, Fin.val_one, Odd.neg_one_pow (n := 2 * k + 0 + 1) (by simp),
    neg_add_cancel, zero_mul, zero_div, mul_zero, zero_add,
    show 2 * k + 1 + 1 = 2 * (k + 1) by ring, Even.neg_one_pow (n := 2 * (k + 1)) (by simp),
    ← mul_div_assoc (_ / _), ← mul_assoc, show -I / 2 * (1 + 1) = -I by ring]
  congr 1
  rw [mul_pow, pow_succ' I, pow_mul, I_sq,
    show -I * _ = -(I * I) * (-1) ^ k * z ^ (2 * k + 1) by ring, I_mul_I, neg_neg, one_mul]

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

Goal state before:
pp: case zero
⊢ (fun n ↦ ↑(n.descFactorial 0)) ~[atTop] fun n ↦ ↑n ^ 0

Tactic:
simpa using

Goal state after:
case zero
⊢ (fun n ↦ 1) ~[atTop] fun n ↦ 1
Module: Mathlib.Analysis.SpecialFunctions.Choose

Goal state before:
pp: case succ
k : ℕ
h : (fun n ↦ ↑(n.descFactorial k)) ~[atTop] fun n ↦ ↑n ^ k
hz : ∀ᶠ (x : ℕ) in atTop, ↑x ≠ 0
⊢ Tendsto (fun n ↦ ((fun n ↦ ↑(n - k)) / Nat.cast) (n + k)) atTop (𝓝 1)

Tactic:
simpa using

Goal state after:
case succ
k : ℕ
h : (fun n ↦ ↑(n.descFactorial k)) ~[atTop] fun n ↦ ↑n ^ k
hz : ∀ᶠ (x : ℕ) in atTop, ↑x ≠ 0
⊢ Tendsto (fun n ↦ ↑n / (↑n + ↑k)) atTop (𝓝 1)
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hre : Tendsto re l atTop
him : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun z ↦ |z.im|
⊢ im =O[l] fun z ↦ z.re ^ 0

Tactic:
simpa using

Goal state after:
l : Filter ℂ
hre : Tendsto re l atTop
him : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun z ↦ |z.im|
⊢ im =O[l] fun z ↦ 1
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ 1 - p < 2⁻¹

Tactic:
sub_lt_comm

Goal state after:
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ 1 - 2⁻¹ < p
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

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

Tactic:
simpa using

Goal state after:
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : b < 0
⊢ (fun z ↦ cexp (↑b * z)) =o[l] fun z ↦ z ^ a
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

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

Tactic:
simpa using

Goal state after:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
m n : ℕ
⊢ (fun z ↦ z ^ m * cexp (↑b₁ * z)) =o[l] fun z ↦ z ^ n * cexp (↑b₂ * z)
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

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

Tactic:
simpa using

Goal state after:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
m n : ℤ
⊢ (fun z ↦ z ^ m * cexp (↑b₁ * z)) =o[l] fun z ↦ z ^ n * cexp (↑b₂ * z)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inr.inl
q : ℕ
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ 0 ≤ qaryEntropy q 1

Tactic:
simpa using

Goal state after:
case inr.inl
q : ℕ
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ 0 ≤ log ↑(↑q - 1)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case hf
⊢ Tendsto (fun x ↦ log (1 - x)) (𝓝[<] 1) atBot

Tactic:
have : Tendsto log (𝓝[>] 0) atBot := Real.tendsto_log_nhdsGT_zero

Goal state after:
case hf
this : Tendsto log (𝓝[>] 0) atBot
⊢ Tendsto (fun x ↦ log (1 - x)) (𝓝[<] 1) atBot
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case neg.inl
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
h : DifferentiableAt ℝ (deriv (qaryEntropy q)) p
contAt : ContinuousAt (deriv (qaryEntropy q)) p
h✝ : p = 0
⊢ False

Tactic:
simp_all [not_continuousAt_deriv_qaryEntropy_zero, not_continuousAt_deriv_qaryEntropy_one]

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

Goal state before:
pp: case neg.inr
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
h : DifferentiableAt ℝ (deriv (qaryEntropy q)) p
contAt : ContinuousAt (deriv (qaryEntropy q)) p
h✝ : p = 1
⊢ False

Tactic:
simp_all [not_continuousAt_deriv_qaryEntropy_zero, not_continuousAt_deriv_qaryEntropy_one]

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

Goal state before:
pp: case refine_2
n : ℕ
⊢ ((monomial 2) (-4)).natDegree + (sinPoly n).natDegree ≤ n + 2

Tactic:
simpa using

Goal state after:
case refine_2
n : ℕ
⊢ (sinPoly n).natDegree ≤ n
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: case pos
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ Tendsto (fun i ↦ if a ∈ {b | IsStrictlyPositive b} then cfc (fun x ↦ i⁻¹ * (x ^ i - 1)) a else 0) (𝓝[>] 0)
    (𝓝 (if a ∈ {b | IsStrictlyPositive b} then log a else 0))

Tactic:
simpa using

Goal state after:
case pos
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ Tendsto (fun i ↦ cfc (fun x ↦ i⁻¹ * (x ^ i - 1)) a) (𝓝[>] 0) (𝓝 (log a))
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 | dist (f x) L < δ} ∈ 𝓝[>] 0
⊢ ∀ᶠ (t : ℝ) in 𝓝[{x | (fun t ↦ 0 < t) x}] 0, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - L‖ ≤ δ

Tactic:
mem_nhdsWithin_iff

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 : ∃ ε > 0, ball 0 ε ∩ Ioi 0 ⊆ {x | dist (f x) L < δ}
⊢ ∀ᶠ (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
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
r : ℝ
hr : r ∈ spectrum ℝ z
this : (a • 1 + b • r) ^ ↑(-1) ≤ a • 1 ^ ↑(-1) + b • r ^ ↑(-1)
⊢ (a + b * r) ^ (-1) ≤ a + b * r ^ (-1)

Tactic:
simpa using

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
r : ℝ
hr : r ∈ spectrum ℝ z
this : (a • 1 + b • r) ^ ↑(-1) ≤ a • 1 ^ ↑(-1) + b • r ^ ↑(-1)
⊢ (a + b * r) ^ (-1) ≤ a + b * r ^ (-1)