mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case pos
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h✝ : 0 < ↑p.natDegree - ↑m
hps : s.card = p.natDegree
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h : f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge : f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
hs_ne : s ≠ 0
⊢ (Multiset.map (⇑f) t).prod ≤ (⨆ x, if x ∈ s then f x else 0) ^ (p.natDegree - m)

Tactic:
obtain ⟨y, hyx, hy_max⟩ : ∃ y : L, y ∈ s ∧ ∀ z : L, z ∈ s → f z ≤ f y :=
        exists_max_image f hs_ne

Goal state after:
case pos
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h✝ : 0 < ↑p.natDegree - ↑m
hps : s.card = p.natDegree
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h : f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge : f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, f z ≤ f y
⊢ (Multiset.map (⇑f) t).prod ≤ (⨆ x, if x ∈ s then f x else 0) ^ (p.natDegree - m)
Module: Mathlib.Analysis.Normed.Group.HomCompletion

Goal state before:
pp: G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in : f.completion hatg = 0
ε : ℝ
⊢ 0 < ε → ∃ b ∈ ↑(toCompl.comp (incl f.ker)).range, ‖hatg - b‖ < ε

Tactic:
ε_pos

Goal state after:
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in : f.completion hatg = 0
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ b ∈ ↑(toCompl.comp (incl f.ker)).range, ‖hatg - b‖ < ε
Module: Mathlib.Analysis.Normed.Group.Tannery

Goal state before:
pp: case refine_1
α : 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‖
h_suma✝ : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable fun x ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ ‖∑ x ∈ T, (f n x - g x)‖ < ε / 3

pp: case refine_2
α : 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‖
h_suma✝ : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable fun x ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ ‖∑' (x : ↑(↑T)ᶜ), (f n ↑x - g ↑x)‖ < ε / 3 + ε / 3

Tactic:
· simpa only [dist_eq_norm, Finset.sum_sub_distrib] using hn

Goal state after:
case refine_2
α : 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‖
h_suma✝ : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable fun x ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ ‖∑' (x : ↑(↑T)ᶜ), (f n ↑x - g ↑x)‖ < ε / 3 + ε / 3
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 : { P // IsLprojection X P }
⊢ ↑P = ↑(P ⊓ P)

Tactic:
simpa only [coe_inf, ← sq] using P.prop.proj.eq.symm

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : T2Space E
inst✝ : T2Space F
u : E →L[𝕜] F
v : F →L[𝕜] E
hvu : (LinearMap.id.eqLocus (↑v ∘ₗ ↑u)).CoFG
huv : (LinearMap.id.eqLocus (↑u ∘ₗ ↑v)).CoFG
E₁ : Submodule 𝕜 E := (↑(ContinuousLinearMap.id 𝕜 E)).eqLocus ↑(v ∘SL u)
F₁ : Submodule 𝕜 F := (↑(ContinuousLinearMap.id 𝕜 F)).eqLocus ↑(u ∘SL v)
u_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
v_mapsto : MapsTo ⇑v ↑F₁ ↑E₁
⊢ u.restrict u_mapsto ∘SL v.restrict v_mapsto = ContinuousLinearMap.id 𝕜 ↥F₁

Tactic:
ext ⟨x, hx : x = u (v x)⟩
    simp [coe_restrict_apply u_mapsto, coe_restrict_apply v_mapsto, ← hx]

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₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : FunSpace t₀ x₀ r L
t : ↑(Icc tmin tmax)
⊢ IntervalIntegrable (fun t' ↦ f t' (α.compProj t')) volume ↑t₀ ↑t

Tactic:
apply ContinuousOn.intervalIntegrable

Goal state after:
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
hf : IsPicardLindelof f t₀ x₀ a r L K
α : FunSpace t₀ x₀ r L
t : ↑(Icc tmin tmax)
⊢ ContinuousOn (fun t' ↦ f t' (α.compProj t')) (uIcc ↑t₀ ↑t)
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 : ℕ
⊢ dist ((next hf hx)^[n] α) ((next hf hx)^[n] β) ≤ (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n ! * dist α β

Tactic:
← MetricSpace.isometry_induced FunSpace.toContinuousMap FunSpace.toContinuousMap.injective
    |>.dist_eq,

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 : ℕ
⊢ dist (toContinuousMap ((next hf hx)^[n] α)) (toContinuousMap ((next hf hx)^[n] β)) ≤
    (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n ! * dist α β
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 y : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
hy : y ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
this : Nonempty ↑(Icc tmin tmax)
⊢ dist (next hf hx α) (next hf hy α) = dist x y

Tactic:
← MetricSpace.isometry_induced FunSpace.toContinuousMap FunSpace.toContinuousMap.injective
    |>.dist_eq,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x y : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
hy : y ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
this : Nonempty ↑(Icc tmin tmax)
⊢ dist (toContinuousMap (next hf hx α)) (toContinuousMap (next hf hy α)) = dist x y
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:
by
  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: 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
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
t : ℝ
ht : t ∈ Icc tmin tmax
this : Fact (t ∈ Icc tmin tmax)
⊢ IntervalIntegrable (fun t ↦ f t (α t)) volume t₀ t

Tactic:
apply ContinuousOn.intervalIntegrable

Goal state after:
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
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
t : ℝ
ht : t ∈ Icc tmin tmax
this : Fact (t ∈ Icc tmin tmax)
⊢ ContinuousOn (fun t ↦ f t (α t)) (uIcc t₀ t)
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₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
t : ℝ
ht : t ∈ Icc tmin tmax
this : Fact (t ∈ Icc tmin tmax)
⊢ ContinuousOn (fun t ↦ f t (α t)) (uIcc t₀ t)

Tactic:
apply continuousOn_comp hf hα hmem |>.mono

Goal state after:
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
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
t : ℝ
ht : t ∈ Icc tmin tmax
this : Fact (t ∈ Icc tmin tmax)
⊢ uIcc t₀ t ⊆ Icc tmin tmax
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
this : v (p.coeff i) ≠ 0
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)

Tactic:
have := hvpq.2

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
this : v (q.coeff j) ≠ 0
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
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 : Odd P.natDegree
⊢ 0 < ↑↑(-1) * eval x P

Tactic:
push_cast at hlc' ⊢; rw [neg_one_mul] at hlc' ⊢
      have := eval_lt_zero_of_roots_lt_of_leadingCoeff_nonpos hroots' (nonpos_of_neg_nonneg hlc')
      exact neg_pos.mpr (by simpa using this)

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

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

Tactic:
by_cases! hroots' : ∃ y, P.IsRoot y ∧ y ≤ x
  · obtain ⟨y, hroot, hle⟩ := hroots'
    rw [eq_of_ge_of_le hle (hroots y hroot), hroot, mul_zero]
  · exact (zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg hroots' hlc).le

Goal state after:
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 + 1 / ↑prec)

Tactic:
push_cast

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

Goal state before:
pp: b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
⊢ |(∑ i ∈ Finset.range n, ofDigitsTerm x i + (↑b ^ n)⁻¹ * ofDigits fun i ↦ x (i + n)) -
        (∑ i ∈ Finset.range n, ofDigitsTerm y i + (↑b ^ n)⁻¹ * ofDigits fun i ↦ y (i + n))| ≤
    (↑b ^ n)⁻¹

Tactic:
have : ∑ i ∈ Finset.range n, ofDigitsTerm x i = ∑ i ∈ Finset.range n, ofDigitsTerm y i :=
    Finset.sum_congr rfl fun i hi ↦ by simp [ofDigitsTerm, hxy i (Finset.mem_range.mp hi)]

Goal state after:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
this : ∑ i ∈ Finset.range n, ofDigitsTerm x i = ∑ i ∈ Finset.range n, ofDigitsTerm y i
⊢ |(∑ i ∈ Finset.range n, ofDigitsTerm x i + (↑b ^ n)⁻¹ * ofDigits fun i ↦ x (i + n)) -
        (∑ i ∈ Finset.range n, ofDigitsTerm y i + (↑b ^ n)⁻¹ * ofDigits fun i ↦ y (i + n))| ≤
    (↑b ^ n)⁻¹
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
this : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
⊢ 0 ≤ ↑b ^ n * x

Tactic:
have := hx.left; positivity

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

Goal state before:
pp: c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ (2 * ↑b + ↑a) / ↑b ≤ ↑c ^ 2 / ↑d ^ 2

Tactic:
div_le_div_iff₀ hb' (pow_pos hd' _)

Goal state after:
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ (2 * ↑b + ↑a) * ↑d ^ 2 ≤ ↑c ^ 2 * ↑b
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ ↑↑(Fin.last b) * ((1 - (↑(b + 1))⁻¹)⁻¹ - 1) = 1

Tactic:
push_cast

Goal state after:
b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ ↑b * ((1 - (↑b + 1)⁻¹)⁻¹ - 1) = 1
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: ⊢ π < 3.1416

Tactic:
by
  -- bound[31416*^-4, Iters -> 9, Rounding -> .9, Precision -> 16]
  pi_upper_bound [
    4756/3363, 14965/8099, 21183/10799, 49188/24713, 2-53/22000, 2-71/117869, 2-47/312092,
    2-17/451533, 2-4/424971]

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

Goal state before:
pp: x : ℝ
hx : Irrational x
a b : ℤ
⊢ x ≠ ↑a / ↑b

Tactic:
rintro rfl

Goal state after:
a b : ℤ
hx : Irrational (↑a / ↑b)
⊢ False
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : multiplicity (↑p) (y ^ n) % n ≠ 0
⊢ y ≠ 0

Tactic:
rintro rfl

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : 0 ^ n ≠ 0
hv : multiplicity (↑p) (0 ^ n) % n ≠ 0
⊢ False
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
r : ℝ
hi : ¬x.Infinitesimal
hr : x.IsSt r
⊢ r ≠ 0

Tactic:
rintro rfl

Goal state after:
x : ℝ*
hi : ¬x.Infinitesimal
hr : x.IsSt 0
⊢ False
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: ⊢ ∃ l, Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)

Tactic:
apply Antitone.tendsto_alternating_series_of_tendsto_zero

Goal state after:
case hfa
⊢ Antitone fun i ↦ (2 * ↑i + 1)⁻¹

case hf0
⊢ Tendsto (fun i ↦ (2 * ↑i + 1)⁻¹) atTop (𝓝 0)
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun k ↦ ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))

Tactic:
have m : 𝓝[<] (1 : ℝ) ≤ 𝓝 1 := tendsto_nhdsWithin_of_tendsto_nhds fun _ a ↦ a

Goal state after:
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
⊢ Tendsto (fun k ↦ ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (cexp (-z.arctan * I) - cexp (z.arctan * I)) / (cexp (z.arctan * I) + cexp (-z.arctan * I)) * I = z

Tactic:
← mul_div_mul_right _ _ (exp_ne_zero (arctan z * I)),

Goal state after:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (cexp (-z.arctan * I) - cexp (z.arctan * I)) * cexp (z.arctan * I) /
        ((cexp (z.arctan * I) + cexp (-z.arctan * I)) * cexp (z.arctan * I)) *
      I =
    z
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: case succ.refine_3
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * (↑n ! ^ 0 * ↑n ! * ↑n ! * ↑n ! * ↑n !) * ((2 * ↑n + 2) * (2 * ↑n + 2)) *
      (↑((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!)) ^ 0 * ↑((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!)) *
          ↑((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!)) *
        (2 * ↑(n + 1) + 1)) =
    2 ^ (4 * n) * 2 * 2 * 2 * 2 *
        (↑((n + 1) * n !) ^ 0 * ↑((n + 1) * n !) * ↑((n + 1) * n !) * ↑((n + 1) * n !) * ↑((n + 1) * n !)) *
      (↑(2 * n)! ^ 0 * ↑(2 * n)! * ↑(2 * n)! * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))

Tactic:
push_cast

Goal state after:
case succ.refine_3
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * (↑n ! ^ 0 * ↑n ! * ↑n ! * ↑n ! * ↑n !) * ((2 * ↑n + 2) * (2 * ↑n + 2)) *
      (((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!)) ^ 0 * ((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!)) *
          ((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!)) *
        (2 * (↑n + 1) + 1)) =
    2 ^ (4 * n) * 2 * 2 * 2 * 2 *
        (((↑n + 1) * ↑n !) ^ 0 * ((↑n + 1) * ↑n !) * ((↑n + 1) * ↑n !) * ((↑n + 1) * ↑n !) * ((↑n + 1) * ↑n !)) *
      (↑(2 * n)! ^ 0 * ↑(2 * n)! * ↑(2 * n)! * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n : ℕ
⊢ ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2)) ∘ (fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1]) (x, y) =
    (sqrt
        (((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 *
          ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2),
      (((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 +
          ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2) /
        2)

Tactic:
comp_apply

Goal state after:
x y : ℝ≥0
n : ℕ
⊢ (sqrt
        (((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 *
          ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2),
      (((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 +
          ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2) /
        2) =
    (sqrt
        (((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 *
          ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2),
      (((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 +
          ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2) /
        2)
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

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

Tactic:
rw [max_eq_right h]

Goal state after:
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ x.agm y ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
⊢ 0 < 1 - tanh x

Tactic:
by grind [tanh_lt_one]

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

Goal state before:
pp: case refine_1
p : ℝ
h : DifferentiableAt ℝ binEntropy p
⊢ p ≠ 0

Tactic:
rintro rfl

Goal state after:
case refine_1
h : DifferentiableAt ℝ binEntropy 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case refine_2
p : ℝ
h : DifferentiableAt ℝ binEntropy p
⊢ p ≠ 1

Tactic:
rintro rfl

Goal state after:
case refine_2
h : DifferentiableAt ℝ binEntropy 1
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case refine_2
h : DifferentiableAt ℝ (fun p ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
⊢ False

Tactic:
DifferentiableAt.fun_add_iff_right,

Goal state after:
case refine_2
h : DifferentiableAt ℝ (fun p ↦ (1 - p) * log (1 - p)⁻¹) 1
⊢ False

case refine_2
h : DifferentiableAt ℝ (fun p ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
⊢ DifferentiableAt ℝ (fun p ↦ p * log p⁻¹) 1
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ qaryEntropy 2 = binEntropy

Tactic:
ext; simp [qaryEntropy]

Goal state after: