mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), z i < y i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), z i + δ < y i
⊢ ball y δ ⊆ s

Tactic:
rintro w hw

Goal state after:
case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), z i < y i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), z i + δ < y i
w : ι → ℝ
hw : w ∈ ball y δ
⊢ w ∈ s
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), y i < z i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), y i + δ < z i
⊢ ball y δ ⊆ s

Tactic:
rintro w hw

Goal state after:
case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), y i < z i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), y i + δ < z i
w : ι → ℝ
hw : w ∈ ball y δ
⊢ w ∈ s
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
⊢ IsClosed ↑(lowerClosure s)

Tactic:
cases nonempty_fintype ι
  refine IsSeqClosed.isClosed fun f x hf hx ↦ ?_
  choose g hg hfg using hf
  have : BoundedGENhdsClass ℝ := by infer_instance
  obtain ⟨a, ha⟩ := hx.bddBelow_range
  obtain ⟨b, hb, φ, hφ, hbf⟩ := tendsto_subseq_of_bounded (hs'.isBounded_inter bddBelow_Ici) fun n ↦
    ⟨hg n, (ha <| mem_range_self _).trans <| hfg _⟩
  exact ⟨b, closure_minimal inter_subset_left hs hb,
    le_of_tendsto_of_tendsto' (hx.comp hφ.tendsto_atTop) hbf fun _ ↦ hfg _⟩

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

Goal state before:
pp: 𝕜 : 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 : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →L[𝕜] W := (apply' W (RingHom.id 𝕜)) z ∘SL (↑f).toContinuousLinearMap ∘SL (smulRightL 𝕜 V V) v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
this : ∀ (A : V →L[𝕜] V) (x : V), T (A x) = (f A) (T x)
d : StrongDual 𝕜 W
hd : d ((f (smulRight v u)) z) = 1
surj : Function.Surjective ⇑T
x y : V
hxy : T x = T y
⊢ x = y

Tactic:
have h_smul : smulRight v x = smulRight v y := by
      apply f.injective <| ContinuousLinearMap.ext fun z ↦ ?_
      obtain ⟨w, rfl⟩ := surj z
      simp [← this, hxy]
    simpa [huv.isUnit.smul_left_cancel] using congr((fun f ↦ f u) $h_smul)

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
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
dt t : ℝ
ht : dt + t ∈ s
⊢ t + dt ∈ s

Tactic:
add_comm

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
dt t : ℝ
ht : t + dt ∈ s
⊢ t + dt ∈ s
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: case h₂
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 : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
⊢ EqOn f g (Icc t₀ b)

Tactic:
have hss : Ico t₀ b ⊆ Ioo a b := Ico_subset_Ioo_left ht.1
    exact ODE_solution_unique_of_mem_Icc_right (fun t ht ↦ hv t (hss ht))
      (hf.mono <| Icc_subset_Icc_left <| le_of_lt ht.1)
      (fun _ ht' ↦ (hf' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hfs _ (hss ht')))
      (hg.mono <| Icc_subset_Icc_left <| le_of_lt ht.1)
      (fun _ ht' ↦ (hg' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hgs _ (hss ht'))) heq

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

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
x : K
hx : x ≠ 0
p : K[X]
⊢ ‖x‖₊ ≠ 0

Tactic:
simpa

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

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

Tactic:
· exact tendsto_abs_atBot_atTop.comp (P.tendsto_atBot_of_leadingCoeff_nonpos hdeg hP)

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 : ℕ
⊢ ∀ {k : ℕ},
    k < n →
      dist ((next hf hx)^[k] α) ((next hf hx)^[k + 1] α) ≤
        (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ k / ↑k ! * dist α (next hf hx α)

Tactic:
intro i hi

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 i : ℕ
hi : i < n
⊢ dist ((next hf hx)^[i] α) ((next hf hx)^[i + 1] α) ≤
    (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i ! * dist α (next hf hx α)
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
⊢ ‖p.leadingCoeff‖₊ ≠ 0

Tactic:
simpa

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

Goal state before:
pp: case ha
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ ‖p.leadingCoeff‖₊ ≠ 0

Tactic:
simpa

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
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n : ℕ
⊢ ∀ {k : ℕ},
    k < n →
      dist ((next hf hx)^[m]^[k] α) ((next hf hx)^[m]^[k + 1] α) ≤
        (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑C ^ k * dist α (next hf hx α)

Tactic:
intro i hi

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
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n i : ℕ
hi : i < n
⊢ dist ((next hf hx)^[m]^[i] α) ((next hf hx)^[m]^[i + 1] α) ≤
    (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑C ^ i * dist α (next hf hx α)
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case inr.inr.inr
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
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)

Tactic:
simp only [gaussNorm, support_nonempty, ne_eq, hpq, not_false_eq_true, ↓reduceDIte,
    Finset.sup'_le_iff]

Goal state after:
case inr.inr.inr
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
⊢ ∀ b ∈ (p + q).support,
    v ((p + q).coeff b) * c ^ b ≤
      max (if h : p.support.Nonempty then p.support.sup' h fun i ↦ v (p.coeff i) * c ^ i else 0)
        (if h : q.support.Nonempty then q.support.sup' h fun i ↦ v (q.coeff i) * c ^ i else 0)
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
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
t : σ →₀ ℕ
⊢ max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) ≤
    max (gaussNorm v c f) (gaussNorm v c g)

Tactic:
simp only [le_sup_iff]

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
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
t : σ →₀ ℕ
⊢ max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) ≤ gaussNorm v c f ∨
    max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) ≤ gaussNorm v c g
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case refine_2
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
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
⊢ 0 ≤ max (gaussNorm v c f) (gaussNorm v c g)

Tactic:
simp only [le_sup_iff]

Goal state after:
case refine_2
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
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
⊢ 0 ≤ gaussNorm v c f ∨ 0 ≤ gaussNorm v c g
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
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

Tactic:
simpa

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

Goal state before:
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 : Odd P.natDegree
⊢ Odd ↑P.natDegree

Tactic:
simpa

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

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

Tactic:
simpa

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

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

Tactic:
simpa

Goal state after:
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)
⊢ (v ((coeff i₀) f * (coeff j₀) g) * (i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2) =
    v ((coeff (i₀ + j₀)) (f * g)) * (i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2

Tactic:
antidiagonal_dominant v f g i₀ j₀ vna vMulEq vNeg hdom'

Goal state after:
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)
⊢ (v ((coeff i₀) f * (coeff j₀) g) * (i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2) =
    v ((coeff i₀) f * (coeff j₀) g) * (i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg.inr
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
⊢ ‖p.leadingCoeff‖ * ‖p.roots.esymm (p.natDegree - n)‖ ≤
    ‖p.leadingCoeff‖ * (↑(p.natDegree.choose n) * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod)

Tactic:
mul_le_mul_iff_right₀ (by simp [leadingCoeff_ne_zero.mpr hp]),

Goal state after:
case neg.inr
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
⊢ ‖p.roots.esymm (p.natDegree - n)‖ ≤ ↑(p.natDegree.choose n) * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod
Module: Mathlib.Analysis.Real.OfDigits

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

Tactic:
← this

Goal state after:
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
this✝ : 0 < b
this : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
h_le : ↑b ^ n * x < ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i + 1
⊢ x - (↑b)⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_1
x : ℝ*
h : 0 ≤ ArchimedeanClass.mk x
y : ℝ
hy : 0 < y
⊢ (fun x1 x2 ↦ x1 - x2) (stdPart x) y < stdPart x

Tactic:
simpa

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

Goal state before:
pp: case refine_2
x : ℝ*
h : 0 ≤ ArchimedeanClass.mk x
y : ℝ
hy : 0 < y
⊢ stdPart x < (fun x1 x2 ↦ x1 + x2) (stdPart x) y

Tactic:
simpa

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

Goal state before:
pp: x : ℝ
h : Irrational (x ^ 0)
⊢ Irrational x

Tactic:
rw [pow_zero] at h
    exact (h ⟨1, cast_one⟩).elim

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

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

Tactic:
simpa

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

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ 1 ≤ x + 0

Tactic:
simpa

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

Goal state before:
pp: case inr
x y : ℝ≥0
h : x ≠ y
this : sqrt (y * x) < (y + x) / 2
hl : ¬y < x
⊢ sqrt (y * x) < (x + y) / 2

Tactic:
add_comm

Goal state after:
case inr
x y : ℝ≥0
h : x ≠ y
this : sqrt (y * x) < (y + x) / 2
hl : ¬y < x
⊢ sqrt (y * x) < (y + x) / 2
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ 1 < x + 0

Tactic:
simpa

Goal state after:
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))^[n + 1 + 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:
iterate_succ',

Goal state after:
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)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ ‖z * I‖ < 1

Tactic:
simpa

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

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

Tactic:
simpa

Goal state after:
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
⊢ ‖z * I‖ < 1

Tactic:
simpa

Goal state after:
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
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
⊢ ‖-(z * I)‖ < 1

Tactic:
simpa

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

Goal state before:
pp: case a
x : ℝ≥0
⊢ x.agm x ≤ x

Tactic:
← max_self x

Goal state after:
case a
x : ℝ≥0
⊢ x.agm x ≤ max x x
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ≤ 0
⊢ artanh x ≤ 0

Tactic:
by_cases -1 < x
  case pos =>
    rw [← artanh_zero, artanh_le_artanh_iff (by grind) (by grind)]
    exact hx
  case neg => grind [artanh_eq_zero_iff]

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

Goal state before:
pp: x : ℝ
hx : ‖x‖ < 1
⊢ ‖↑x‖ < 1

Tactic:
simpa

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

Goal state before:
pp: case succ
k : ℕ
h : (fun n ↦ ↑(n.descFactorial k)) ~[atTop] fun n ↦ ↑n ^ k
⊢ (fun n ↦ ↑(n - k)) ~[atTop] Nat.cast

Tactic:
have hz : ∀ᶠ (x : ℕ) in atTop, (x : ℝ) ≠ 0 :=
      eventually_atTop.mpr ⟨1, fun n hn ↦ ne_of_gt (mod_cast hn)⟩

Goal state after:
case succ
k : ℕ
h : (fun n ↦ ↑(n.descFactorial k)) ~[atTop] fun n ↦ ↑n ^ k
hz : ∀ᶠ (x : ℕ) in atTop, ↑x ≠ 0
⊢ (fun n ↦ ↑(n - k)) ~[atTop] Nat.cast
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ binEntropy (2⁻¹ + p) = binEntropy (2⁻¹ - p)

Tactic:
← binEntropy_one_sub

Goal state after:
p : ℝ
⊢ binEntropy (1 - (2⁻¹ + p)) = binEntropy (2⁻¹ - p)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : 1 < p
⊢ binEntropy p < 0

Tactic:
← binEntropy_one_sub

Goal state after:
p : ℝ
hp : 1 < p
⊢ binEntropy (1 - p) < 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : 1 ≤ p
⊢ binEntropy p ≤ 0

Tactic:
← binEntropy_one_sub

Goal state after:
p : ℝ
hp : 1 ≤ p
⊢ binEntropy (1 - p) ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

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

Tactic:
← binEntropy_one_sub

Goal state after:
case refine_2.inr
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp✝ : ¬p < 2⁻¹
hp : 1 - p < 2⁻¹
⊢ binEntropy (1 - p) < log 2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ ¬binEntropy p < log 2 ↔ p = 2⁻¹

Tactic:
binEntropy_lt_log_two,

Goal state after:
p : ℝ
⊢ ¬p ≠ 2⁻¹ ↔ p = 2⁻¹
Module: Mathlib.Analysis.Real.Pi.Irrational

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

Tactic:
simp [add_comm 2, cosPoly_natDegree_le n]

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

Goal state before:
pp: case inl.inl
p : ℤ[X]
a : ℤ
hp : p.natDegree ≤ 0
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ 0 = ↑z

pp: case inl.inr
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
hk : k > 0
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ k = ↑z

Tactic:
· exact ⟨p.coeff 0, by simp⟩

Goal state after:
case inl.inr
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
hk : k > 0
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ k = ↑z
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
⊢ ((conjSqrt x) (a • 1 + b • z))⁻¹ʳ = (conjSqrt x⁻¹ʳ) ((a • 1 + b • z) ^ (-1))

Tactic:
rw [ringInverse_conjSqrt _ _ xpos, ← inverse_eq_rpow_neg_one]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
hsplit :
  ∀ {ε r : ℝ},
    0 < ε →
      0 < r →
        ∫ (x : ℝ) in ε..r, x⁻¹ • (f (a * x) - f (b * x)) =
          (∫ (x : ℝ) in a * ε..b * ε, u x) - ∫ (x : ℝ) in a * r..b * r, u x
h_ev :
  (fun p ↦ ∫ (x : ℝ) in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x))) =ᶠ[𝓝[>] 0 ×ˢ atTop] fun p ↦
    (∫ (x : ℝ) in a * p.1..b * p.1, u x) - ∫ (x : ℝ) in a * p.2..b * p.2, u x
⊢ Tendsto (fun p ↦ (∫ (x : ℝ) in a * p.1..b * p.1, u x) - ∫ (x : ℝ) in a * p.2..b * p.2, u x) (𝓝[>] 0 ×ˢ atTop)
    (𝓝 (log (b / a) • L - log (b / a) • R))

Tactic:
exact ((tendsto_integral_inv_smul_nhdsWithin hf ha hb hL).comp tendsto_fst).sub
    ((tendsto_integral_inv_smul_atTop hf ha hb hR).comp tendsto_snd)

Goal state after: