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

Goal state before:
pp: K : Type u
inst✝⁹ : NontriviallyNormedField K
L : Type v
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
hu : IsUltrametricDist K
inst✝⁶ : CompleteSpace K
x : L
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Algebra L E
inst✝² : IsScalarTower K L E
inst✝¹ : IsSplittingField L E ((mapAlg K L) (minpoly K x))
inst✝ : Algebra.IsAlgebraic K E
h_deg : (minpoly K x).natDegree = ((mapAlg K E) (minpoly K x)).roots.card
r : ℝ
⊢ Multiset.count r (Multiset.replicate (minpoly K x).natDegree ((spectralMulAlgNorm K E) ((algebraMap L E) x))) =
    Multiset.count r (Multiset.map (⇑(spectralMulAlgNorm K E)) ((mapAlg K E) (minpoly K x)).roots)

Tactic:
rw [Multiset.count_replicate]

Goal state after:
K : Type u
inst✝⁹ : NontriviallyNormedField K
L : Type v
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
hu : IsUltrametricDist K
inst✝⁶ : CompleteSpace K
x : L
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Algebra L E
inst✝² : IsScalarTower K L E
inst✝¹ : IsSplittingField L E ((mapAlg K L) (minpoly K x))
inst✝ : Algebra.IsAlgebraic K E
h_deg : (minpoly K x).natDegree = ((mapAlg K E) (minpoly K x)).roots.card
r : ℝ
⊢ (if (spectralMulAlgNorm K E) ((algebraMap L E) x) = r then (minpoly K x).natDegree else 0) =
    Multiset.count r (Multiset.map (⇑(spectralMulAlgNorm K E)) ((mapAlg K E) (minpoly K x)).roots)
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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖)

Tactic:
by
            rw [sub_mul, h₃.proj.eq, one_mul, sub_self, zero_smul, zero_sub, norm_neg]

Goal state after:
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₁)
⊢ ∃ t ∈ Filter.map (fun s ↦ ∏ b ∈ s, (fun i ↦ 1 + f i) b) (unconditional ι).filter, ∀ x ∈ t, ∀ y ∈ t, dist x y < ε

Tactic:
simp only [unconditional, Filter.mem_map, mem_atTop_sets, Set.mem_preimage]

Goal state after:
ι : 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₁)
⊢ ∃ t, (∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ t) ∧ ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: δ K x : ℝ
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)

Tactic:
by_cases hK : K = 0
  · simp only [gronwallBound_K0, hK, zero_mul, exp_zero, add_zero, mul_one]
  · simp only [gronwallBound_of_K_ne_0 hK, zero_div, zero_mul, add_zero]

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
hγ : IsIntegralCurve γ v
dt : ℝ
⊢ IsIntegralCurve (γ ∘ fun x ↦ x + dt) (v ∘ fun x ↦ x + dt)

Tactic:
rw [← isIntegralCurveOn_univ] at *

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
hγ : IsIntegralCurveOn γ v univ
dt : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun x ↦ x + dt) (v ∘ fun x ↦ x + dt) univ
Module: Mathlib.Analysis.ODE.Transform

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

Tactic:
rw [← isIntegralCurveOn_univ] at *

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
hγ : IsIntegralCurveOn γ v univ
a : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) univ
Module: Mathlib.Analysis.ODE.PicardLindelof

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

Tactic:
rw [intervalIntegral.norm_intervalIntegral_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 : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ ‖∫ (x_1 : ℝ) in uIoc ↑t₀ ↑t,
        f x_1 (((next hf hx)^[n] α).compProj x_1) - f x_1 (((next hf hx)^[n] β).compProj x_1) ∂volume‖ ≤
    ∫ (τ : ℝ) in uIoc ↑t₀ ↑t, ↑K ^ (n + 1) * |τ - ↑t₀| ^ n / ↑n ! * dist α β
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : Q = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atTop] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atTop] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

Tactic:
· simp [hQ, IsEquivalent.refl]

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atTop] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : Q = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atBot] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atBot] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

Tactic:
· simp [hQ, IsEquivalent.refl]

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atBot] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)
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‖₊
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x

Tactic:
calc ‖a‖₊ ^ p.natDegree
    _ = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ := by
      rw [mul_div_cancel_left₀]
      simpa
    _ ≤ ‖∑ x ∈ range p.natDegree, p.coeff x * a ^ x‖₊ / ‖p.leadingCoeff‖₊ := by gcongr
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊ := by
      gcongr
      apply nnnorm_sum_le
    _ = (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ := by simp
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (cauchyBound p - 1) * ‖a‖₊ ^ x) /
        ‖p.leadingCoeff‖₊ := by
      gcongr (∑ x ∈ _, ?_ * _) / _
      rw [cauchyBound, add_tsub_cancel_right]
      field_simp
      apply le_sup (f := (‖p.coeff ·‖₊)) ‹_›
    _ = (cauchyBound p - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x := by
      simp only [← mul_sum]
      field

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree < Q.degree
hp : P = 0
⊢ (fun x ↦ eval x P) =o[atTop] fun x ↦ eval x Q

pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree < Q.degree
hp : ¬P = 0
⊢ (fun x ↦ eval x P) =o[atTop] fun x ↦ eval x Q

Tactic:
· simp [hp]

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree < Q.degree
hp : ¬P = 0
⊢ (fun x ↦ eval x P) =o[atTop] fun x ↦ eval x Q
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
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), ContractingWith C (next hf hx)^[m]
L' : ℝ := ⋯
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ ↑r
hy : y ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ Filter.Tendsto (fun x ↦ dist α ((next hf hy)^[m]^[x] α)) Filter.atTop (𝓝 (dist α β))

Tactic:
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 α

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
c : ℝ
p : R[X]
inst✝ : ZeroHomClass F R ℝ
⊢ ∃ i, gaussNorm v c p = v (p.coeff i) * c ^ i

Tactic:
by_cases h_supp : p.support.Nonempty

Goal state after:
case pos
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝ : ZeroHomClass F R ℝ
h_supp : p.support.Nonempty
⊢ ∃ i, gaussNorm v c p = v (p.coeff i) * c ^ i

case neg
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝ : ZeroHomClass F R ℝ
h_supp : ¬p.support.Nonempty
⊢ ∃ i, gaussNorm v c p = v (p.coeff i) * c ^ i
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case pos
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : p = 0
⊢ PowerSeries.gaussNorm (⇑v) c ↑p = gaussNorm v c p

pp: case neg
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
⊢ PowerSeries.gaussNorm (⇑v) c ↑p = gaussNorm v c p

Tactic:
· simp [hp]

Goal state after:
case neg
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
⊢ PowerSeries.gaussNorm (⇑v) c ↑p = gaussNorm v c p
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
vZero : v 0 = 0
⊢ gaussNorm v c 0 = 0

Tactic:
by simp [gaussNorm, vZero]

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

Goal state before:
pp: case inr.a
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
this : (fun i ↦ v (p.coeff i) * 0 ^ i) = fun i ↦ if i = 0 then v (p.coeff 0) else 0
hcoeff0 : p.coeff 0 ≠ 0
⊢ gaussNorm v 0 p ≤ v (p.coeff 0)

pp: case a
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
this : (fun i ↦ v (p.coeff i) * 0 ^ i) = fun i ↦ if i = 0 then v (p.coeff 0) else 0
hcoeff0 : p.coeff 0 ≠ 0
⊢ v (p.coeff 0) ≤ gaussNorm v 0 p

Tactic:
· aesop (add norm (by simp [gaussNorm, Finset.sup'_le_iff]))

Goal state after:
case a
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
this : (fun i ↦ v (p.coeff i) * 0 ^ i) = fun i ↦ if i = 0 then v (p.coeff 0) else 0
hcoeff0 : p.coeff 0 ≠ 0
⊢ v (p.coeff 0) ≤ gaussNorm v 0 p
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case inl
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]
hp : p = 0
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)

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

Tactic:
· simp [hp]

Goal state after:
case 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
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
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
i : ℕ
a✝ : i ∈ (p + q).support
⊢ v ((p + q).coeff i) * c ^ i ≤
    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)

Tactic:
calc
  v ((p + q).coeff i) * c ^ i
    ≤ max (v (p.coeff i)) (v (q.coeff i)) * c ^ i := by
    rw [coeff_add]
    gcongr
    exact hna (p.coeff i) (q.coeff i)
  _ = max (v (p.coeff i) * c ^ i) (v (q.coeff i) * c ^ i) := by
    rw [max_mul_of_nonneg _ _ (pow_nonneg hc _)]
  _ ≤ max (gaussNorm v c p) (gaussNorm v c q) := by
    apply max_le_max <;>
    exact le_gaussNorm v _ hc i

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E → E
tmin tmax tmin' tmax' : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
t₀' : ↑(Icc tmin' tmax')
ht₀ : ↑t₀ = ↑t₀'
htmin : tmin ≤ tmin'
htmax : tmax' ≤ tmax
⊢ ↑L * max (tmax' - ↑t₀') (↑t₀' - tmin') ≤ ↑L * max (tmax - ↑t₀) (↑t₀ - tmin)

Tactic:
gcongr <;> linarith

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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
⊢ ∃ ε, ∃ (hε : 0 < ε), ∃ a r L K, ∃ (_ : 0 < r), ∀ (t₀ : ℝ), IsPicardLindelof (fun x ↦ f) ⟨t₀, ⋯⟩ x₀ a r L K

Tactic:
obtain ⟨K, s, hs, hl⟩ := hf.exists_lipschitzOnWith

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
⊢ ∃ ε, ∃ (hε : 0 < ε), ∃ a r L K, ∃ (_ : 0 < r), ∀ (t₀ : ℝ), IsPicardLindelof (fun x ↦ f) ⟨t₀, ⋯⟩ x₀ a r L K
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
⊢ p.logMahlerMeasure = log p.mahlerMeasure

Tactic:
rw [mahlerMeasure]

Goal state after:
p : ℂ[X]
⊢ p.logMahlerMeasure = log (if p ≠ 0 then rexp p.logMahlerMeasure else 0)
Module: Mathlib.Data.Rat.NatSqrt.Defs

Goal state before:
pp: x prec : ℕ
⊢ 0 ≤ x.ratSqrt prec

Tactic:
unfold ratSqrt
  positivity

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

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

Tactic:
have := logMahlerMeasure_X_sub_C z
  rw [logMahlerMeasure_eq_log_MahlerMeasure] at this
  apply_fun exp at this
  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.Polynomial.MahlerMeasure

Goal state before:
pp: case pos
p : ℂ[X]
hp : p = 0
⊢ p.logMahlerMeasure = log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum

pp: case neg
p : ℂ[X]
hp : ¬p = 0
⊢ p.logMahlerMeasure = log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum

Tactic:
· simp [hp]

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
⊢ p.logMahlerMeasure = log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
⊢ p.logMahlerMeasure = log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum

Tactic:
have : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0 := by grind [Multiset.mem_map]

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
this : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0
⊢ p.logMahlerMeasure = log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case pos
p : ℂ[X]
hp : p = 0
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

pp: case neg
p : ℂ[X]
hp : ¬p = 0
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
· simp [hp]

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case pos
p : ℂ[X]
hp : p = 0
⊢ p.mahlerMeasure ≤ p.sum fun x a ↦ ‖a‖

pp: case neg
p : ℂ[X]
hp : ¬p = 0
⊢ p.mahlerMeasure ≤ p.sum fun x a ↦ ‖a‖

Tactic:
· simp [hp]

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
⊢ p.mahlerMeasure ≤ p.sum fun x a ↦ ‖a‖
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case pos
p : ℂ[X]
this✝ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this : NeZero (volume (uIoc 0 (2 * π)))
hp : p = 0
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)

pp: case neg
p : ℂ[X]
this✝ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)

Tactic:
· simp [hp]

Goal state after:
case neg
p : ℂ[X]
this✝ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case pos
n : ℕ
p : ℂ[X]
hp : p = 0
⊢ ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mahlerMeasure

pp: case neg
n : ℕ
p : ℂ[X]
hp : ¬p = 0
⊢ ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mahlerMeasure

Tactic:
· simp [hp]

Goal state after:
case neg
n : ℕ
p : ℂ[X]
hp : ¬p = 0
⊢ ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mahlerMeasure
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : multiplicity (↑p) m % 2 = 1
⊢ multiplicity (↑p) m % 2 ≠ 0

Tactic:
by rw [Hpv]; exact one_ne_zero

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

Goal state before:
pp: x y : ℝ
⊢ x ∈ Set.range Rat.cast ∧ y ∈ Set.range Rat.cast → x + y ∈ Set.range Rat.cast

Tactic:
rintro ⟨⟨rx, rfl⟩, ⟨ry, rfl⟩⟩

Goal state after:
rx ry : ℚ
⊢ ↑rx + ↑ry ∈ Set.range Rat.cast
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
by
  simpa only [sub_eq_add_neg, cast_neg] using h.add_ratCast (-q)

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

Goal state before:
pp: x y : ℝ
⊢ x ∈ Set.range Rat.cast ∧ y ∈ Set.range Rat.cast → x * y ∈ Set.range Rat.cast

Tactic:
rintro ⟨⟨rx, rfl⟩, ⟨ry, rfl⟩⟩

Goal state after:
rx ry : ℚ
⊢ ↑rx * ↑ry ∈ Set.range Rat.cast
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
⊢ x.InfiniteNeg ↔ x < 0 ∧ ArchimedeanClass.mk x < 0

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨hx, hx'⟩ r ↦ ?_⟩
  · have hx : x < 0 := h 0
    refine ⟨h 0, fun n ↦ ?_⟩
    simpa [abs_of_neg hx, lt_neg] using! h (-n)
  · exact lt_of_mk_lt_mk_of_nonpos (hx'.trans_le <| mk_map_nonneg_of_archimedean coeRingHom _) hx.le

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

Goal state before:
pp: x y : ℝ*
⊢ x.InfiniteNeg → ¬y.InfinitePos → (x + y).InfiniteNeg

Tactic:
← infinitePos_neg,

Goal state after:
x y : ℝ*
⊢ (-x).InfinitePos → ¬y.InfinitePos → (x + y).InfiniteNeg
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
⊢ (-x).InfinitePos → ¬y.InfinitePos → (x + y).InfiniteNeg

Tactic:
← infinitePos_neg,

Goal state after:
x y : ℝ*
⊢ (-x).InfinitePos → ¬y.InfinitePos → (-(x + y)).InfinitePos
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
⊢ x.InfiniteNeg ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0

Tactic:
← infinitePos_neg,

Goal state after:
x : ℝ*
⊢ (-x).InfinitePos ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
⊢ x.InfiniteNeg → ¬y.Infinitesimal → y < 0 → (x * y).InfinitePos

Tactic:
← infinitePos_neg,

Goal state after:
x y : ℝ*
⊢ (-x).InfinitePos → ¬y.Infinitesimal → y < 0 → (x * y).InfinitePos
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
⊢ x.InfinitePos → ¬y.Infinitesimal → y < 0 → (x * y).InfiniteNeg

Tactic:
← infinitePos_neg,

Goal state after:
x y : ℝ*
⊢ x.InfinitePos → ¬y.Infinitesimal → y < 0 → (-(x * y)).InfinitePos
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
⊢ x.InfiniteNeg → ¬y.Infinitesimal → 0 < y → (x * y).InfiniteNeg

Tactic:
← infinitePos_neg,

Goal state after:
x y : ℝ*
⊢ (-x).InfinitePos → ¬y.Infinitesimal → 0 < y → (x * y).InfiniteNeg
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
⊢ (-x).InfinitePos → ¬y.Infinitesimal → 0 < y → (x * y).InfiniteNeg

Tactic:
← infinitePos_neg,

Goal state after:
x y : ℝ*
⊢ (-x).InfinitePos → ¬y.Infinitesimal → 0 < y → (-(x * y)).InfinitePos
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

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

Tactic:
specialize this h.symm (h.gt_or_lt.resolve_left hl)
    rwa [mul_comm, add_comm]

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

Goal state before:
pp: case inl
x y : ℝ≥0
h : x ≤ y
⊢ (min x y).agmSequences (max x y) = x.agmSequences y

Tactic:
rw [min_eq_left h, max_eq_right h]

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

Goal state before:
pp: case neg
p : ℝ
hp : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ deriv binEntropy p = log (1 - p) - log p

Tactic:
rw [deriv_zero_of_not_differentiableAt (differentiableAt_binEntropy_iff_ne_zero_one.not.2 hp)]
    push +distrib Not at hp
    obtain rfl | rfl := hp <;> simp

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

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - 1 / ↑q))
this : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
⊢ p < 1 - (↑q)⁻¹

Tactic:
simp_all only [inv_pos, interior_Icc, mem_Ioo, one_div]

Goal state after: