mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.ODE.DiscreteGronwall

Goal state before:
pp: case hf
u b c : ℕ → ℝ
n₀ n₁ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n ∈ Ico n₀ n₁
this : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k
⊢ ∀ i ∈ Ico n₀ n₁, i ∉ Ico n₀ n → 0 ≤ b i

pp: case hb
u b c : ℕ → ℝ
n₀ n₁ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n ∈ Ico n₀ n₁
this : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k
⊢ n ≤ n₁

pp: case hf
u b c : ℕ → ℝ
n₀ n₁ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n ∈ Ico n₀ n₁
this : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k
⊢ ∀ i ∈ Ico n₀ n₁, i ∉ Ico n₀ n → 0 ≤ c i

pp: case hb
u b c : ℕ → ℝ
n₀ n₁ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n ∈ Ico n₀ n₁
this : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k
⊢ n ≤ n₁

Tactic:
<;>

Goal state after:
case hf
u b c : ℕ → ℝ
n₀ n₁ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n ∈ Ico n₀ n₁
this : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k
⊢ ∀ i ∈ Ico n₀ n₁, i ∉ Ico n₀ n → 0 ≤ b i

case hb
u b c : ℕ → ℝ
n₀ n₁ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n ∈ Ico n₀ n₁
this : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k
⊢ n ≤ n₁

case hf
u b c : ℕ → ℝ
n₀ n₁ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n ∈ Ico n₀ n₁
this : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k
⊢ ∀ i ∈ Ico n₀ n₁, i ∉ Ico n₀ n → 0 ≤ c i

case hb
u b c : ℕ → ℝ
n₀ n₁ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n ∈ Ico n₀ n₁
this : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k
⊢ n ≤ n₁
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: case left
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
t : ℝ
ht : -b ≤ t ∧ t < -a
⊢ a < -t

pp: case right
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
t : ℝ
ht : -b ≤ t ∧ t < -a
⊢ -t ≤ b

Tactic:
<;>

Goal state after:
case left
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
t : ℝ
ht : -b ≤ t ∧ t < -a
⊢ a < -t

case right
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
t : ℝ
ht : -b ≤ t ∧ t < -a
⊢ -t ≤ b
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: case inl
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 : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
h : t' < t₀
hss : Icc t' t₀ ⊆ Ioo a b
⊢ f t' = g t'

Tactic:
exact ODE_solution_unique_of_mem_Icc_left
      (fun t'' ht'' ↦ hv t'' ((Ioc_subset_Icc_self.trans hss) ht''))
      (HasDerivAt.continuousOn fun _ ht'' ↦ (hf _ <| hss ht'').1)
      (fun _ ht'' ↦ (hf _ <| hss <| Ioc_subset_Icc_self ht'').1.hasDerivWithinAt)
      (fun _ ht'' ↦ (hf _ <| hss <| Ioc_subset_Icc_self ht'').2)
      (HasDerivAt.continuousOn fun _ ht'' ↦ (hg _ <| hss ht'').1)
      (fun _ ht'' ↦ (hg _ <| hss <| Ioc_subset_Icc_self ht'').1.hasDerivWithinAt)
      (fun _ ht'' ↦ (hg _ <| hss <| Ioc_subset_Icc_self ht'').2) heq
      ⟨le_rfl, le_of_lt h⟩

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 𝕜
⊢ (IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ |eval x P|) ↔ P.degree ≤ 0

Tactic:
refine ⟨fun h => ?_, fun h => ⟨|P.coeff 0|, eventually_map.mpr (Eventually.of_forall
    (forall_imp (fun _ => le_of_eq) fun x => congr_arg abs <| _root_.trans (congr_arg (eval x)
    (eq_C_of_degree_le_zero h)) eval_C))⟩⟩
  contrapose! h
  exact not_isBoundedUnder_of_tendsto_atTop (abs_tendsto_atTop P h)

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

Goal state before:
pp: p : ℂ[X]
⊢ ∑ i ∈ p.support, ‖p.coeff i‖ ^ 2 = Real.circleAverage (fun θ ↦ ‖eval θ p‖ ^ 2) 0 1

Tactic:
have := tsum_sq_fourierCoeff (T := 2 * π) (p.toAddCircle.toLp 2 haarAddCircle ℂ)

Goal state after:
p : ℂ[X]
this :
  ∑' (i : ℤ), ‖fourierCoeff (↑↑((ContinuousMap.toLp 2 haarAddCircle ℂ) (toAddCircle p))) i‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑↑((ContinuousMap.toLp 2 haarAddCircle ℂ) (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
⊢ ∑ i ∈ p.support, ‖p.coeff i‖ ^ 2 = Real.circleAverage (fun θ ↦ ‖eval θ p‖ ^ 2) 0 1
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 : ℝ
inst✝ : ZeroHomClass F R ℝ
r : R
hr : r = 0
⊢ gaussNorm v c (C r) = v r

pp: case neg
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
inst✝ : ZeroHomClass F R ℝ
r : R
hr : ¬r = 0
⊢ gaussNorm v c (C r) = v r

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
inst✝ : ZeroHomClass F R ℝ
r : R
hr : r = 0
⊢ gaussNorm v c (C r) = v r

case neg
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
inst✝ : ZeroHomClass F R ℝ
r : R
hr : ¬r = 0
⊢ gaussNorm v c (C r) = v r
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: P Q : ℤ[X]
mQ : Q.Monic
h : {a | eval a Q ∣ eval a P}.Infinite
eqR : P %ₘ Q + Q * (P /ₘ Q) = P
degR : (P %ₘ Q).degree < Q.degree
⊢ Q ∣ P

Tactic:
← modByMonic_eq_zero_iff_dvd mQ

Goal state after:
P Q : ℤ[X]
mQ : Q.Monic
h : {a | eval a Q ∣ eval a P}.Infinite
eqR : P %ₘ Q + Q * (P /ₘ Q) = P
degR : (P %ₘ Q).degree < Q.degree
⊢ P %ₘ Q = 0
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 : ℝ
inst✝ : ZeroHomClass F R ℝ
n : ℕ
r : R
hr : r = 0
⊢ gaussNorm v c ((monomial n) r) = v r * c ^ n

pp: case neg
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
inst✝ : ZeroHomClass F R ℝ
n : ℕ
r : R
hr : ¬r = 0
⊢ gaussNorm v c ((monomial n) r) = v r * c ^ n

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
inst✝ : ZeroHomClass F R ℝ
n : ℕ
r : R
hr : r = 0
⊢ gaussNorm v c ((monomial n) r) = v r * c ^ n

case neg
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
inst✝ : ZeroHomClass F R ℝ
n : ℕ
r : R
hr : ¬r = 0
⊢ gaussNorm v c ((monomial n) r) = v r * c ^ n
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case pos.succ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
n : ℕ
hn : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u) → ContDiffOn ℝ (↑n) (picard f t₀ x₀ α) (Icc tmin tmax)
hf : ContDiffOn ℝ (↑n + 1) (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ DifferentiableOn ℝ (picard f t₀ x₀ α) (Icc tmin tmax) ∧
    (↑n = ⊤ → AnalyticOn ℝ (picard f t₀ x₀ α) (Icc tmin tmax)) ∧
      ContDiffOn ℝ (↑n) (derivWithin (picard f t₀ x₀ α) (Icc tmin tmax)) (Icc tmin tmax)

Tactic:
refine ⟨fun t ht ↦ HasDerivWithinAt.differentiableWithinAt (this t ht), by simp, ?_⟩

Goal state after:
case pos.succ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
n : ℕ
hn : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u) → ContDiffOn ℝ (↑n) (picard f t₀ x₀ α) (Icc tmin tmax)
hf : ContDiffOn ℝ (↑n + 1) (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ ContDiffOn ℝ (↑n) (derivWithin (picard f t₀ x₀ α) (Icc tmin tmax)) (Icc tmin tmax)
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✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : p.support.Nonempty
⊢ 0 ≤ 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✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p.support.Nonempty
⊢ 0 ≤ gaussNorm v c p

Tactic:
<;>

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✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : p.support.Nonempty
⊢ 0 ≤ gaussNorm v c p

case neg
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p.support.Nonempty
⊢ 0 ≤ gaussNorm v c p
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case a
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.coeff i) * c ^ i ≤ gaussNorm v c p

pp: case a
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 (q.coeff i) * c ^ i ≤ gaussNorm v c q

Tactic:
<;>

Goal state after:
case a
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.coeff i) * c ^ i ≤ gaussNorm v c p

case a
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 (q.coeff i) * c ^ i ≤ gaussNorm v c q
Module: Mathlib.Analysis.Polynomial.Norm

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

Tactic:
by simpa [eq_comm] using exists_eq_supNorm p

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

Goal state before:
pp: case hcd
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
⊢ ↑t₀ ≤ ↑t₀'

pp: case hab
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
⊢ ↑t₀' ≤ ↑t₀

Tactic:
<;>

Goal state after:
case hcd
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
⊢ ↑t₀ ≤ ↑t₀'

case hab
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
⊢ ↑t₀' ≤ ↑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
⊢ 0 ≤ ↑↑(↑(P.comp (-X)).natDegree).negOnePow * (P.comp (-X)).leadingCoeff

Tactic:
rw [show (P.comp (-X)).leadingCoeff = P.leadingCoeff * Int.negOnePow P.natDegree by simp; ring,
      show (P.comp (-X)).natDegree = P.natDegree by simp [natDegree_comp], mul_comm, mul_assoc]

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

Goal state before:
pp: case pos
p : ℂ[X]
h✝ : p ≠ 0
⊢ p.logMahlerMeasure = log (rexp p.logMahlerMeasure)

pp: case neg
p : ℂ[X]
h✝ : ¬p ≠ 0
⊢ p.logMahlerMeasure = log 0

Tactic:
<;>

Goal state after:
case pos
p : ℂ[X]
h✝ : p ≠ 0
⊢ p.logMahlerMeasure = log (rexp p.logMahlerMeasure)

case neg
p : ℂ[X]
h✝ : ¬p ≠ 0
⊢ p.logMahlerMeasure = log 0
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case pos
p : ℂ[X]
hp : p = 0
⊢ 0 ≤ p.mahlerMeasure

pp: case neg
p : ℂ[X]
hp : ¬p = 0
⊢ 0 ≤ p.mahlerMeasure

Tactic:
<;>

Goal state after:
case pos
p : ℂ[X]
hp : p = 0
⊢ 0 ≤ p.mahlerMeasure

case neg
p : ℂ[X]
hp : ¬p = 0
⊢ 0 ≤ p.mahlerMeasure
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
hp : p ≠ 0
⊢ 0 < p.mahlerMeasure

Tactic:
grind [exp_pos, mahlerMeasure_def_of_ne_zero]

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

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

Tactic:
hroot,

Goal state after:
case pos
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : 0 ≤ P.leadingCoeff
y : ℝ
hroot : P.IsRoot y
hle : y ≤ x
⊢ 0 ≤ ↑↑(↑P.natDegree).negOnePow * 0
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case cons.refine_1
α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s✝ : Finset ι
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
j : ι
s : Finset ι
hj : j ∉ s
hs✝ : s.Nonempty
IH : ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)
⊢ g (∑ i ∈ s, f i) ≤ g (f j) → g (f j + ∑ i ∈ s, f i) ≤ g (f j)

pp: case cons.refine_2
α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s✝ : Finset ι
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
j : ι
s : Finset ι
hj : j ∉ s
hs✝ : s.Nonempty
IH : ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)
⊢ g (f j) ≤ g (∑ i ∈ s, f i) → ∃ a ∈ s, g (f j + ∑ i ∈ s, f i) ≤ g (f a)

Tactic:
<;>

Goal state after:
case cons.refine_1
α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s✝ : Finset ι
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
j : ι
s : Finset ι
hj : j ∉ s
hs✝ : s.Nonempty
IH : ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)
⊢ g (∑ i ∈ s, f i) ≤ g (f j) → g (f j + ∑ i ∈ s, f i) ≤ g (f j)

case cons.refine_2
α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s✝ : Finset ι
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
j : ι
s : Finset ι
hj : j ∉ s
hs✝ : s.Nonempty
IH : ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)
⊢ g (f j) ≤ g (∑ i ∈ s, f i) → ∃ a ∈ s, g (f j + ∑ i ∈ s, f i) ≤ g (f a)
Module: Mathlib.Analysis.Rat.NatSqrt.Real

Goal state before:
pp: x prec : ℕ
h : 0 < prec
⊢ ↑(x.ratSqrt prec) ≤ √↑x

Tactic:
have := ratSqrt_sq_le (x := x) h
  have : (x.ratSqrt prec ^ 2 : ℝ) ≤ ↑x := by norm_cast
  have := Real.sqrt_monotone this
  rwa [Real.sqrt_sq] at this
  simpa only [Rat.cast_nonneg] using ratSqrt_nonneg _ _

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

Goal state before:
pp: p : ℂ[X]
⊢ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2) ≤ √(↑p.natDegree + 1) * p.supNorm

Tactic:
by
    rw [show √(↑(p.natDegree) + 1) * p.supNorm = √((p.natDegree + 1) * p.supNorm ^ 2) by
      rw [Real.sqrt_mul (by positivity), Real.sqrt_sq p.supNorm_nonneg]]
    gcongr
    refine (p.support.sum_le_card_nsmul _ (p.supNorm ^ 2) fun i _ ↦ ?_).trans ?_
    · gcongr; exact p.le_supNorm _
    · simp only [nsmul_eq_mul]
      gcongr
      exact mod_cast p.card_supp_le_succ_natDegree

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

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

Tactic:
_root_.norm_natCast

Goal state after:
case neg.inr
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
⊢ ∑ x ∈ (powersetCard (p.natDegree - n) p.roots).toFinset,
      ↑(count x (powersetCard (p.natDegree - n) p.roots)) * ‖x.prod‖ ≤
    ↑(p.natDegree.choose n) * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod
Module: Mathlib.Data.Rat.Sqrt

Goal state before:
pp: z : ℤ
⊢ sqrt ↑z = ↑(Int.sqrt z)

Tactic:
by
  simp only [sqrt, num_intCast, den_intCast, Nat.sqrt_one, mkRat_one]

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

Goal state before:
pp: case inr
q : ℚ
hq : q < 0
⊢ False ↔ ¬IsSquare q ∧ 0 ≤ q

Tactic:
false_iff,

Goal state after:
case inr
q : ℚ
hq : q < 0
⊢ ¬(¬IsSquare q ∧ 0 ≤ q)
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case inl
x : ℝ*
h✝ : 0 ≤ x
⊢ |x|.Infinite ↔ x.Infinite

pp: case inr
x : ℝ*
h✝ : x ≤ 0
⊢ |x|.Infinite ↔ x.Infinite

Tactic:
<;>

Goal state after:
case inl
x : ℝ*
h✝ : 0 ≤ x
⊢ |x|.Infinite ↔ x.Infinite

case inr
x : ℝ*
h✝ : x ≤ 0
⊢ |x|.Infinite ↔ x.Infinite
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: case succ.refine_1
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 2

pp: case succ.refine_2
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 1

pp: case succ.refine_3
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 2

pp: case succ.refine_4
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 3

Tactic:
<;>

Goal state after:
case succ.refine_1
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 2

case succ.refine_2
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 1

case succ.refine_3
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 2

case succ.refine_4
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 3
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: case left
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ -1 < y

pp: case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ y < 1

Tactic:
<;>

Goal state after:
case left
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ -1 < y

case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ y < 1
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:

Tactic:
1 ≤ x + 0 := by simpa
    _ ≤ x + √(x ^ 2 - 1) := by gcongr; positivity

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

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 1
this : 0 < √((1 + x) / (1 - x))
⊢ sinh (artanh x) = x / (√(1 + x) * √(1 - x))

pp: case hx
x : ℝ
hx : x ∈ Ioo (-1) 1
this : 0 < √((1 + x) / (1 - x))
⊢ 0 ≤ 1 + x

Tactic:
<;>

Goal state after:
x : ℝ
hx : x ∈ Ioo (-1) 1
this : 0 < √((1 + x) / (1 - x))
⊢ sinh (artanh x) = x / (√(1 + x) * √(1 - x))

case hx
x : ℝ
hx : x ∈ Ioo (-1) 1
this : 0 < √((1 + x) / (1 - x))
⊢ 0 ≤ 1 + x
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 1
this : 0 < √((1 + x) / (1 - x))
⊢ cosh (artanh x) = 1 ^ 2 / (√(1 + x) * √(1 - x))

pp: case hx
x : ℝ
hx : x ∈ Ioo (-1) 1
this : 0 < √((1 + x) / (1 - x))
⊢ 0 ≤ 1 + x

Tactic:
<;>

Goal state after:
x : ℝ
hx : x ∈ Ioo (-1) 1
this : 0 < √((1 + x) / (1 - x))
⊢ cosh (artanh x) = 1 ^ 2 / (√(1 + x) * √(1 - x))

case hx
x : ℝ
hx : x ∈ Ioo (-1) 1
this : 0 < √((1 + x) / (1 - x))
⊢ 0 ≤ 1 + x
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case zero
k x y : ℝ≥0
⊢ ((k * x).agmSequences (k * y) 0).2 = k * (x.agmSequences y 0).2

Tactic:
simp [← mul_div_assoc, mul_add]

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

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

Tactic:
rw [← binEntropy_one_sub]; ring_nf

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

Goal state before:
pp: p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this✝ : 0 < 1 - p
this : 0 < log p⁻¹
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹

Tactic:
have : 0 < log (1 - p)⁻¹ := log_pos <| (one_lt_inv₀ ‹_›).2 (sub_lt_self _ hp₀)

Goal state after:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this✝¹ : 0 < 1 - p
this✝ : 0 < log p⁻¹
this : 0 < log (1 - p)⁻¹
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inl
⊢ binEntropy 0 = 0

pp: case inr
⊢ binEntropy 1 = 0

Tactic:
<;>

Goal state after:
case inl
⊢ binEntropy 0 = 0

case inr
⊢ binEntropy 1 = 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
⊢ 1 - p ≠ 0

pp: p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
⊢ p ≠ 0

Tactic:
<;>

Goal state after:
p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
⊢ 1 - p ≠ 0

p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
⊢ p ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

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

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

Tactic:
<;>

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

case refine_2
p : ℝ
h : DifferentiableAt ℝ binEntropy p
⊢ p ≠ 1