mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : ¬S.Nonempty
⊢ 1 ≤ ‖a - a'‖

Tactic:
simp only [ne_eq, Finset.not_nonempty_iff_eq_empty, Finset.filter_eq_empty_iff,
      Set.mem_toFinset, not_not, S] at hS
      rw [isConjRoot_iff_mem_minpoly_rootSet ⟨f, fmon, fa0⟩,
          ← minpoly.eq_of_irreducible_of_monic firr fa0 fmon] at conj
      exact (ne (hS conj).symm).elim

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
n : ℕ
hn : 0 ≤ 1 / ↑n
⊢ μ ((x * y) ^ n) ^ (1 / ↑n) ≤ μ (x ^ n) ^ (1 / ↑n) * μ (y ^ n) ^ (1 / ↑n)

Tactic:
rw [← mul_rpow (apply_nonneg μ _) (apply_nonneg μ _), mul_pow]

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
n : ℕ
hn : 0 ≤ 1 / ↑n
⊢ μ (x ^ n * y ^ n) ^ (1 / ↑n) ≤ (μ (x ^ n) * μ (y ^ n)) ^ (1 / ↑n)
Module: Mathlib.Analysis.Normed.Group.Tannery

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
h✝ : Nonempty β
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) ⊥ (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in ⊥, ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ Tendsto (fun x ↦ ∑' (k : β), f x k) ⊥ (𝓝 (∑' (k : β), g k))

pp: case inr.inr
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
⊢ Tendsto (fun x ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))

Tactic:
· simp only [tendsto_bot]

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
⊢ Tendsto (fun x ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
Module: Mathlib.Analysis.Normed.Group.Tannery

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
⊢ ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖

Tactic:
filter_upwards [h_bound] with n h

Goal state after:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
n : α
h : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ Summable fun x ↦ ‖f n x‖
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
f : ι → R
inst✝ : CompleteSpace R
hf : Summable fun i ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
s₂ : Finset ι
hs₂ : ∀ (t : Finset ι), Disjoint t s₂ → ‖∏ i ∈ t, (1 + f i) - 1‖ < ε / (2 * r₁)
s : Finset ι := s₁ ∪ s₂
⊢ ∃ t, (∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ t) ∧ ∀ x ∈ t, ∀ y ∈ t, dist x y < ε

Tactic:
refine ⟨Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2), ⟨s, fun b hb ↦ ?_⟩, ?_⟩

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
f : ι → R
inst✝ : CompleteSpace R
hf : Summable fun i ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
s₂ : Finset ι
hs₂ : ∀ (t : Finset ι), Disjoint t s₂ → ‖∏ i ∈ t, (1 + f i) - 1‖ < ε / (2 * r₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
⊢ ∏ x ∈ b, (1 + f x) ∈ Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)

case refine_2
ι : Type u_1
R : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
f : ι → R
inst✝ : CompleteSpace R
hf : Summable fun i ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
s₂ : Finset ι
hs₂ : ∀ (t : Finset ι), Disjoint t s₂ → ‖∏ i ∈ t, (1 + f i) - 1‖ < ε / (2 * r₁)
s : Finset ι := s₁ ∪ s₂
⊢ ∀ x ∈ Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2), ∀ y ∈ Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2), dist x y < ε
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ (↑P + ↑Pᶜ * ↑Q) * (↑P + ↑Pᶜ * ↑R) * (↑P + ↑Pᶜ * ↑(Q ⊓ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ

Tactic:
(Pᶜ.prop.commute (Q ⊓ R).prop).eq,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ (↑P + ↑Pᶜ * ↑Q) * (↑P + ↑Pᶜ * ↑R) * (↑P + ↑(Q ⊓ R) * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ
Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
R : Type u_3
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
inst✝¹ : CompleteSpace R
inst✝ : TopologicalSpace α
f : ι → α → R
hK : IsCompact K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
hKe : K = ∅
⊢ TendstoUniformly (fun i x ↦ ∏ i ∈ i, (1 + f i ↑x)) ((fun x ↦ ∏' (i : ι), (1 + f i x)) ∘ Subtype.val) atTop

Tactic:
simp [TendstoUniformly, hKe]

Goal state after:
Module: Mathlib.Topology.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : Preorder α
inst✝¹ : IsOrderedMonoid α
inst✝ : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen ↑(lowerClosure s)

Tactic:
by
    rw [← mul_one s, ← mul_lowerClosure]
    exact hs.mul_right

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁶] ↑A
inst✝ : A.CoFG
N : Submodule 𝕜 E := A ⊓ (↑u).ker
π : E →L[𝕜] E ⧸ N := N.mkQL
v : E ⧸ N →L[𝕜] F := N.liftQL u ⋯
π_quot : IsOpenQuotientMap ⇑π
u_eq : u = v ∘SL π
B : Submodule 𝕜 (E ⧸ N) := map N.mkQ A
B_cofg : B.CoFG
v_ker : Disjoint (↑v).ker B
comap_B : comap (↑π) B = A
A_mapsTo_B : MapsTo ⇑π ↑A ↑B
B_closed : IsClosed[QuotientModule.Quotient.topologicalSpace N] ↑B
step4_output :
  IsStrictMap ⇑v ∧ IsClosed[inst✝³] ↑(↑v).range ↔
    IsStrictMap ⇑(v.domRestrict B) ∧ IsClosed[inst✝³] ↑(↑(v.domRestrict B)).range
range_eq : (↑v).range = (↑u).range
range_restr_eq : (↑(v.domRestrict B)).range = (↑(u.domRestrict A)).range
π' : ↥A →L[𝕜] ↥B := π.restrict A_mapsTo_B
π'_quot : IsOpenQuotientMap ⇑π'
u_restr_eq : u.domRestrict A = v.domRestrict B ∘SL π'
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝³] ↑(↑u).range ↔
    IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed[inst✝³] ↑(↑(u.domRestrict A)).range

Tactic:
calc IsStrictMap u ∧ IsClosed (u.range : Set F)
      ↔ IsStrictMap v ∧ IsClosed (v.range : Set F) := by
        rw [← range_eq, u_eq, coe_comp, π_quot.isQuotientMap.isStrictMap_iff]
    _ ↔ IsStrictMap (v.domRestrict B) ∧ IsClosed ((v.domRestrict B).range : Set F) :=
        step4_output
    _ ↔ IsStrictMap (u.domRestrict A) ∧ IsClosed ((u.domRestrict A).range : Set F) := by
        rw [← range_restr_eq, u_restr_eq, coe_comp, π'_quot.isQuotientMap.isStrictMap_iff]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: case neg
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
⊢ ∃ U, ∀ (x : V →L[𝕜] V), f x = (↑U ∘SL x) ∘SL ↑U.symm

Tactic:
eq_comp_toContinuousLinearMap_symm

Goal state after:
case neg
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
⊢ ∃ U, ∀ (x : V →L[𝕜] V), f x ∘SL ↑U = ↑U ∘SL x
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: K : ℝ≥0
⊢ ¬↑(1 - K) = ∞

Tactic:
exact ENNReal.coe_ne_top

Goal state after:
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₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
⊢ ∃ α, α ↑t₀ = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t

Tactic:
obtain ⟨α, hα⟩ := FunSpace.exists_isFixedPt_next hf hx

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₀ 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
hα : IsFixedPt (FunSpace.next hf hx) α
⊢ ∃ α, α ↑t₀ = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ dt : ℝ
⊢ IsIntegralCurveAt (γ ∘ fun x ↦ x - dt) (v ∘ fun x ↦ x - dt) (t₀ + dt) ↔ IsIntegralCurveAt γ v t₀

Tactic:
by
  simpa using! isIntegralCurveAt_comp_add (dt := -dt)

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
⊢ IsIntegralCurve (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) ↔ IsIntegralCurve γ v

Tactic:
by
  refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul _⟩
  convert! hγ.comp_mul a⁻¹
  · ext t
    simp only [comp_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one]
  · ext t
    simp only [comp_apply, Pi.smul_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one,
      smul_smul, one_smul]

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

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

Tactic:
by
  convert! ((P.comp (-X)).abs_tendsto_atTop (by simp [hdeg])).comp tendsto_neg_atBot_atTop using 2
  simp

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

Goal state before:
pp: case neg.refine_2
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
hP : ¬P = 0
⊢ (fun x ↦ x ^ P.natDegree) =o[cobounded R] fun x ↦ x ^ Q.natDegree

Tactic:
· exact isLittleO_pow_pow_cobounded_of_lt (natDegree_lt_natDegree hP h)

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

Goal state before:
pp: c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)

Tactic:
have := hvpq.1

Goal state after:
c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this : v (p.coeff i) ≠ 0
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
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
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
⊢ ∃ α, α ↑t₀ = x ∧ ∀ t ∈ Icc tmin tmax, α t = picard f (↑t₀) x α t

Tactic:
obtain ⟨α, hα⟩ := FunSpace.exists_isFixedPt_next hf hx

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₀ 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
hα : IsFixedPt (FunSpace.next hf hx) α
⊢ ∃ α, α ↑t₀ = x ∧ ∀ t ∈ Icc tmin tmax, α t = picard f (↑t₀) x α 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
hlc' : 0 ≤ ↑↑1 * (P.comp (-X)).leadingCoeff
h : Even P.natDegree
⊢ 0 < ↑↑1 * eval x P

pp: case hn
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
hlc' : 0 ≤ ↑↑1 * (P.comp (-X)).leadingCoeff
h : Even P.natDegree
⊢ Even ↑P.natDegree

pp: case hn
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
hlc' : 0 ≤ ↑↑(↑(P.comp (-X)).natDegree).negOnePow * (P.comp (-X)).leadingCoeff
h : Even P.natDegree
⊢ Even ↑(P.comp (-X)).natDegree

Tactic:
· push_cast at hlc' ⊢; rw [one_mul] at hlc' ⊢
      have := zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg hroots' hlc'
      simpa using this

Goal state after:
case hn
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
hlc' : 0 ≤ ↑↑1 * (P.comp (-X)).leadingCoeff
h : Even P.natDegree
⊢ Even ↑P.natDegree

case hn
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
hlc' : 0 ≤ ↑↑(↑(P.comp (-X)).natDegree).negOnePow * (P.comp (-X)).leadingCoeff
h : Even P.natDegree
⊢ Even ↑(P.comp (-X)).natDegree
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: z : ℂ
this : rexp (log (X - C z).mahlerMeasure) = rexp (log⁺ ‖z‖)
⊢ (X - C z).mahlerMeasure = max 1 ‖z‖

Tactic:
rwa [posLog_eq_log_max_one (norm_nonneg z),
    exp_log (mahlerMeasure_pos_of_ne_zero <| X_sub_C_ne_zero z),
    exp_log (lt_of_lt_of_le zero_lt_one <| le_max_left 1 ‖z‖)] at this

Goal state after:
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
⊢ ↑(x.ratSqrt prec) ≤ √↑x

Tactic:
Real.sqrt_sq

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

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)
⊢ √↑x < ↑(x.ratSqrt prec) + 1 / ↑prec

Tactic:
Real.sqrt_sq

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)
⊢ √↑x < ↑(x.ratSqrt prec) + 1 / ↑prec

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 + 1 / ↑prec)
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: n : ℕ
⊢ (π / 2 ^ (n + 2)) ^ 3 / 6 ≤ (4 / 2 ^ (n + 2)) ^ 3 / 4

Tactic:
gcongr; exacts [pi_le_four, by norm_num]

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

Goal state before:
pp: case right
x y : ℝ≥0
h : x ≤ y
⊢ (x + y) / 2 ≤ y

Tactic:
apply div_le_of_le_mul'

Goal state after:
case right
x y : ℝ≥0
h : x ≤ y
⊢ x + y ≤ 2 * y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
| Tendsto (fun x_1 ↦ dist (x.agmSequences y x_1).2 (x.agmSequences y x_1).1) atTop (𝓝 0)

Tactic:
enter [1, n]
    rw [dist_comm]

Goal state after:
x y : ℝ≥0
n : ℕ
| dist (x.agmSequences y n).1 (x.agmSequences y n).2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n : ℕ
⊢ x.agm y = (x.agmSequences y n).1.agm (x.agmSequences y n).2

Tactic:
refine tendsto_nhds_unique ?_ tendsto_agmSequences_snd_agm

Goal state after:
x y : ℝ≥0
n : ℕ
⊢ Tendsto (fun n_1 ↦ ((x.agmSequences y n).1.agmSequences (x.agmSequences y n).2 n_1).2) atTop (𝓝 (x.agm y))
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
⊢ Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop

Tactic:
have : (fun p ↦ log (q - 1) + log (1 - p) - log p)
        = (fun p ↦ log (q - 1) + (log (1 - p) - log p)) := by ext; ring

Goal state after:
q : ℕ
this : (fun p ↦ log (↑q - 1) + log (1 - p) - log p) = fun p ↦ log (↑q - 1) + (log (1 - p) - log p)
⊢ Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
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
c : A
⊢ Monotone ⇑(conjSqrt c)

Tactic:
by
  intro a b hab
  by_cases hc : 0 ≤ c
  · exact IsSelfAdjoint.conjugate_le_conjugate hab (by cfc_tac)
  · simp [conjSqrt_of_not_nonneg hc]

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

Goal state before:
pp: s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / (sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1)
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
hcont' : ContinuousOn (fun x ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
x : ℝ
hx : x ∈ s
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ p * ‖log x‖ ^ 2 ≤ p * sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)

Tactic:
gcongr
          refine le_csSup ?_ (by grind)
          grind [IsCompact.bddAbove, ← IsCompact.image_of_continuousOn]

Goal state after:
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 • y)⁻¹ʳ

Tactic:
conjSqrt_one x xpos.nonneg

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
⊢ (a • x + b • y)⁻¹ʳ = (a • x + b • y)⁻¹ʳ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)

Tactic:
simp only [rpowIntegrand₀₁, hx_zero, add_zero, sub_self, mul_zero]

Goal state after:
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : x = 0
⊢ 0 ≤ t ^ (p - 1)
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ log 7 < 49 / 20 - 1 / 2

Tactic:
log_lt_iff_lt_exp (by positivity)

Goal state after:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 < rexp (49 / 20 - 1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
⊢ ↑π ^ (-s / 2 + -(s + 1) / 2) * (Gamma (2 * (s / 2)) * 2 ^ (1 - 2 * (s / 2)) * ↑√π) =
    2 ^ (1 - s) * (↑π ^ (-1 / 2 - s) * ↑π ^ (1 / 2)) * Gamma s

Tactic:
sqrt_eq_rpow,

Goal state after:
s : ℂ
⊢ ↑π ^ (-s / 2 + -(s + 1) / 2) * (Gamma (2 * (s / 2)) * 2 ^ (1 - 2 * (s / 2)) * ↑(π ^ (1 / 2))) =
    2 ^ (1 - s) * (↑π ^ (-1 / 2 - s) * ↑π ^ (1 / 2)) * Gamma s
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ StrictAnti eulerMascheroniSeq'

Tactic:
refine strictAnti_nat_of_succ_lt (fun n ↦ ?_)

Goal state after:
n : ℕ
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
⊢ ↑π ^ (-s / 2) * ↑π ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) =
    2 ^ (1 - s) * (↑π ^ (-1 / 2 - s) * ↑π ^ (1 / 2)) * Gamma s

Tactic:
by
    rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), Complex.Gamma_mul_Gamma_add_half,
      sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
    ring_nf

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

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ 2 * (2 * ↑π) ^ (-s)
this : HasDerivAt (fun x ↦ (2 * ↑π) ^ (-x)) ((2 * ↑π) ^ (-1) * log (2 * ↑π) * -1) 1
⊢ 2 * ((2 * ↑π) ^ (-1) * log (2 * ↑π) * -1) = -log (2 * ↑π) / ↑π

Tactic:
mul_neg_one,

Goal state after:
f : ℂ → ℂ := fun s ↦ 2 * (2 * ↑π) ^ (-s)
this : HasDerivAt (fun x ↦ (2 * ↑π) ^ (-x)) ((2 * ↑π) ^ (-1) * log (2 * ↑π) * -1) 1
⊢ 2 * -((2 * ↑π) ^ (-1) * log (2 * ↑π)) = -log (2 * ↑π) / ↑π