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

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

Tactic:
coe_inf,

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

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R

Tactic:
by
    have e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * (R : M) * ↑Pᶜ := by
      rw [coe_inf, coe_sup, coe_sup, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, add_mul,
        mul_add, (Pᶜ.prop.commute Q.prop).eq, mul_add, ← mul_assoc, mul_assoc (Q : M),
        (Pᶜ.prop.commute P.prop).eq, mul_compl_self, zero_mul, mul_zero,
        zero_add, add_zero, ← mul_assoc, mul_assoc (Q : M), P.prop.proj.eq, Pᶜ.prop.proj.eq,
        mul_assoc, (Pᶜ.prop.commute R.prop).eq, ← mul_assoc]
    have e₂ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) * ↑(P ⊔ Q ⊓ R) = (P : M) + ↑Q * ↑R * ↑Pᶜ := by
      rw [coe_inf, coe_sup, coe_sup, coe_sup, ← add_sub, ← add_sub, ← add_sub, ← compl_mul, ←
        compl_mul, ← compl_mul, (Pᶜ.prop.commute (Q ⊓ R).prop).eq, coe_inf, mul_assoc,
        distrib_lattice_lemma, (Q.prop.commute R.prop).eq, distrib_lattice_lemma]
    rw [le_def, e₁, coe_inf, e₂]

Goal state after:
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ᶜ) = ↑⊥

Tactic:
coe_inf,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P : { P // IsLprojection X P }
⊢ ↑P * ↑Pᶜ = ↑⊥
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: case inr.inr.inl
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
q r : ℝ≥0∞
e : (i : ι) → E i
f : (i : ι) → F i
hf : Memℓp f q
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
h : Nonempty ι
hK : 0 ≤ K
hpqr : ∞.HolderTriple q r
he : Memℓp e ∞
hpqr' : r⁻¹ = ∞⁻¹ + q⁻¹
⊢ Memℓp (fun i ↦ ((B i) (e i)) (f i)) r

Tactic:
simp_all only [inv_top, zero_add, inv_inj]
    exact he.bilin_of_top_left B hBK hf

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

Goal state before:
pp: f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
⊢ ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a)

Tactic:
intro x hx ε' (hε' : ε < ε')

Goal state after:
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
⊢ f x ≤ gronwallBound δ K ε' (x - a)
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → E
K a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
ha : f a = 0
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ K * ‖f x‖
x : ℝ
hx : x ∈ Icc a b
⊢ f x = 0

Tactic:
apply norm_le_zero_iff.mp

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → E
K a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
ha : f a = 0
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ K * ‖f x‖
x : ℝ
hx : x ∈ Icc a b
⊢ ‖f x‖ ≤ 0
Module: Mathlib.Analysis.ODE.DiscreteGronwall

Goal state before:
pp: case ha
u b c : ℕ → ℝ
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₀ ≤ n
⊢ 0 ≤ u n₀ + ∑ k ∈ Ico n₀ n, b k

Tactic:
try exact add_nonneg hun₀ <| sum_nonneg <| by grind

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

Goal state before:
pp: case hbc
u b c : ℕ → ℝ
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₀ ≤ n
⊢ ∏ i ∈ Ico n₀ n, (1 + c i) ≤ rexp (∑ i ∈ Ico n₀ n, c i)

Tactic:
try exact add_nonneg hun₀ <| sum_nonneg <| by grind

Goal state after:
case hbc
u b c : ℕ → ℝ
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₀ ≤ n
⊢ ∏ i ∈ Ico n₀ n, (1 + c i) ≤ rexp (∑ i ∈ Ico n₀ n, c i)
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 ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (a⁻¹ • s)
⊢ IsIntegralCurveOn γ v s

Tactic:
convert! hγ.comp_mul a⁻¹

Goal state after:
case e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (a⁻¹ • s)
⊢ γ = (γ ∘ fun x ↦ x * a) ∘ fun x ↦ x * a⁻¹

case e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (a⁻¹ • s)
⊢ v = a⁻¹ • (a • v ∘ fun x ↦ x * a) ∘ fun x ↦ x * a⁻¹

case e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (a⁻¹ • s)
⊢ s = {t | t * a⁻¹ ∈ a⁻¹ • s}
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: case e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (a⁻¹ • s)
⊢ v = a⁻¹ • (a • v ∘ fun x ↦ x * a) ∘ fun x ↦ x * a⁻¹

Tactic:
ext t
    simp only [comp_apply, Pi.smul_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one,
      smul_smul, one_smul]

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

Goal state before:
pp: case e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (t₀ / a)
⊢ v = a⁻¹ • (a • v ∘ fun x ↦ x * a) ∘ fun x ↦ x * a⁻¹

Tactic:
ext t
    simp only [comp_apply, Pi.smul_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one,
      smul_smul, one_smul]

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

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

Tactic:
convert! hγ.comp_mul a⁻¹

Goal state after:
case e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurve (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a)
⊢ γ = (γ ∘ fun x ↦ x * a) ∘ fun x ↦ x * a⁻¹

case e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurve (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a)
⊢ v = a⁻¹ • (a • v ∘ fun x ↦ x * a) ∘ fun x ↦ x * a⁻¹
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: case e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurve (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a)
⊢ v = a⁻¹ • (a • v ∘ fun x ↦ x * a) ∘ fun x ↦ x * a⁻¹

Tactic:
ext t
    simp only [comp_apply, Pi.smul_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one,
      smul_smul, one_smul]

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

Goal state before:
pp: 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
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
this : EqOn (f ∘ Neg.neg) (g ∘ Neg.neg) (Icc (-b) (-a))
⊢ EqOn f g (Icc a b)

Tactic:
rw [eqOn_comp_right_iff] at this
    convert this
    simp

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
this : P.natDegree = 0
⊢ Tendsto (fun x ↦ c) atTop (𝓝 c)

Tactic:
exact tendsto_const_nhds

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
⊢ ∃ n C, ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), ContractingWith C (next hf hx)^[n]

Tactic:
obtain ⟨n, hn⟩ := FloorSemiring.tendsto_pow_div_factorial_atTop (K * max (tmax - t₀) (t₀ - tmin))
    |>.eventually (gt_mem_nhds zero_lt_one) |>.exists
  have : (0 : ℝ) ≤ (K * max (tmax - t₀) (t₀ - tmin)) ^ n / n ! := by
    have : 0 ≤ max (tmax - t₀) (t₀ - tmin) := le_max_of_le_left <| sub_nonneg_of_le t₀.2.2
    positivity
  refine ⟨n, ⟨_, this⟩, fun x hx ↦ ?_⟩
  exact ⟨hn, LipschitzWith.of_dist_le_mul fun α β ↦ dist_iterate_next_iterate_next_le hf hx α β n⟩

Goal state after:
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.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊

Tactic:
rw [mul_div_cancel_left₀]

Goal state after:
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
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
⊢ (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ ≤
    (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (p.cauchyBound - 1) * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊

Tactic:
gcongr (∑ x ∈ _, ?_ * _) / _
      rw [cauchyBound, add_tsub_cancel_right]
      field_simp
      apply le_sup (f := (‖p.coeff ·‖₊)) ‹_›

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

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

Tactic:
convert! (isLittleO_atTop_of_degree_lt _ _ h).comp_tendsto tendsto_neg_atBot_atTop using 2

Goal state after:
case e'_7
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : (P.comp (-X)).degree < (Q.comp (-X)).degree
x✝ : 𝕜
⊢ eval x✝ P = ((fun x ↦ eval x (P.comp (-X))) ∘ Neg.neg) x✝

case e'_8
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : (P.comp (-X)).degree < (Q.comp (-X)).degree
x✝ : 𝕜
⊢ eval x✝ Q = ((fun x ↦ eval x (Q.comp (-X))) ∘ Neg.neg) x✝
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmin < tmax
⊢ ContDiffOn ℝ (↑n) α (Icc tmin tmax)

Tactic:
set t₀ := (tmin + tmax) / 2 with h
    have ht₀ : t₀ ∈ Icc tmin tmax := ⟨by linarith, by linarith⟩
    have : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ (α t₀) α t := by
      intro t ht
      have : uIcc t₀ t ⊆ Icc tmin tmax := uIcc_subset_Icc ht₀ ht
      rw [picard_eq_of_hasDerivAt (hf.continuousOn.mono (prod_subset_prod_left this))
        (fun t' ht' ↦ hα t' (this ht') |>.mono this) (hmem.mono_left this)]
    exact contDiffOn_enat_picard_Icc ht₀ hf (HasDerivWithinAt.continuousOn hα) hmem (α t₀) this
      |>.congr this

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 : ℝ
inst✝² : ZeroHomClass F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
i : ℕ
a✝ : i ∈ (p * q).support
j : ℕ
left✝ : j ∈ range (i + 1)
right✝ : v (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) ≤ v (p.coeff j * q.coeff (i - j))
⊢ v (p.coeff j) * c ^ j * (v (q.coeff (i - j)) * c ^ (i - j)) ≤
    (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) * q.support.sup' ⋯ fun i ↦ v (q.coeff i) * c ^ i

Tactic:
have hp_le := p.le_gaussNorm v hc j
      have hq_le := q.le_gaussNorm v hc (i - j)
      have := p.gaussNorm_nonneg v hc
      simp_all only [gaussNorm, ↓reduceDIte]
      gcongr

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

Goal state before:
pp: z : ℂ
⊢ (X + C z).logMahlerMeasure = log⁺ ‖z‖

Tactic:
by
  simp [← sub_neg_eq_add, ← map_neg]

Goal state after:
Module: Mathlib.Data.Rat.NatSqrt.Defs

Goal state before:
pp: x prec : ℕ
h : 0 < prec
⊢ ↑x < (↑(x * prec ^ 2).sqrt / ↑prec + 1 / ↑prec) ^ 2

Tactic:
← mul_lt_mul_iff_of_pos_right (a := (prec ^ 2 : ℚ)) (by positivity)

Goal state after:
x prec : ℕ
h : 0 < prec
⊢ ↑x * ↑prec ^ 2 < (↑(x * prec ^ 2).sqrt / ↑prec + 1 / ↑prec) ^ 2 * ↑prec ^ 2
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

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

Tactic:
by
  simp [← sub_neg_eq_add, ← map_neg]

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

Goal state before:
pp: b : ℕ
digits : ℕ → Fin b
⊢ Summable fun x ↦ (↑b - 1) * (↑b ^ (x + 1))⁻¹

Tactic:
obtain rfl | hb := (Nat.one_le_of_lt (b_pos digits)).eq_or_lt

Goal state after:
case inl
digits : ℕ → Fin 1
⊢ Summable fun x ↦ (↑1 - 1) * (↑1 ^ (x + 1))⁻¹

case inr
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ Summable fun x ↦ (↑b - 1) * (↑b ^ (x + 1))⁻¹
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
digits : ℕ → Fin b
⊢ ofDigits digits ≤ 1

Tactic:
obtain rfl | hb := (Nat.one_le_of_lt (b_pos digits)).eq_or_lt

Goal state after:
case inl
digits : ℕ → Fin 1
⊢ ofDigits digits ≤ 1

case inr
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ ofDigits digits ≤ 1
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ HasSum (ofDigitsTerm (x.digits b)) x

Tactic:
by
  rw [hasSum_iff_tendsto_nat_of_summable_norm (by exact summable_ofDigitsTerm.abs)]
  refine tendsto_of_tendsto_of_tendsto_of_le_of_le ?_ tendsto_const_nhds
    (le_sum_ofDigitsTerm_digits hx) (sum_ofDigitsTerm_digits_le hx)
  convert! tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_abs_lt_one _)
  · simp
  · simp [abs_of_nonneg, inv_lt_one_iff₀, hb]

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

Goal state before:
pp: case hbc
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this : ∀ x ∈ S.toFinset, ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
x : Multiset ℂ
hx : x ∈ S.toFinset
⊢ ∏ b ∈ x.toFinset, ‖b ^ count b x‖ ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots

Tactic:
simp_rw [norm_pow]

Goal state after:
case hbc
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this : ∀ x ∈ S.toFinset, ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
x : Multiset ℂ
hx : x ∈ S.toFinset
⊢ ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
Nat.mul_mod_right

Goal state after:
case inr
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : 0 ≠ 0
this : y ≠ 0
⊢ False
Module: Mathlib.Analysis.Real.Hyperreal

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

Tactic:
Infinitesimal,

Goal state after:
x : ℝ*
⊢ x.IsSt 0 ↔ 0 < ArchimedeanClass.mk x
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
⊢ |x|.Infinite ↔ x.Infinite

Tactic:
by
  cases le_total 0 x <;> simp [*, abs_of_nonneg, abs_of_nonpos, infinite_neg]

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

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ cosh (log (x + √(x ^ 2 - 1))) = x

Tactic:
cosh_eq,

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ (rexp (log (x + √(x ^ 2 - 1))) + rexp (-log (x + √(x ^ 2 - 1)))) / 2 = x
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ sinh (arcosh x) = √(x ^ 2 - 1)

Tactic:
rw [arcosh, sinh_eq, exp_neg, exp_log (by positivity), add_sqrt_self_sq_sub_one_inv hx]
  ring

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

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

Tactic:
by
  rw [agm_eq_ciSup]
  exact le_ciSup bddAbove_range_agmSequences_fst _

Goal state after:
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:
· rw [DifferentiableAt.fun_add_iff_right, differentiableAt_iff_comp_const_sub (b := 1)] at h
    · simp [log_inv, mul_neg, ← neg_mul, ← negMulLog_def, differentiableAt_negMulLog_iff] at h
    · fun_prop (disch := simp)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
⊢ (a • 1 + cfc (fun x ↦ b • x) z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z

Tactic:
← Algebra.algebraMap_eq_smul_one,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
⊢ ((algebraMap ℝ A) a + cfc (fun x ↦ b • x) z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) 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
hcont : ContinuousOn (fun r ↦ r ^ (-1)) (spectrum ℝ z)
⊢ a • 1 + cfc (fun x ↦ b • x ^ (-1)) z = cfc (fun r ↦ a + b * r ^ (-1)) z

Tactic:
← Algebra.algebraMap_eq_smul_one,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
hcont : ContinuousOn (fun r ↦ r ^ (-1)) (spectrum ℝ z)
⊢ (algebraMap ℝ A) a + cfc (fun x ↦ b • x ^ (-1)) z = cfc (fun r ↦ a + b * r ^ (-1)) z
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
x : ℝ
hx : 0 < x
⊢ deriv (fun x ↦ f (x + 1)) x = deriv f x + x⁻¹

Tactic:
← deriv_log,

Goal state after:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
x : ℝ
hx : 0 < x
⊢ deriv (fun x ↦ f (x + 1)) x = deriv f x + deriv log x
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsProbabilityMeasure μ
f : X →ᵇ E
⊢ ‖∫ (x : X), f x ∂μ‖ ≤ ‖f‖

Tactic:
by
  convert! f.norm_integral_le_mul_norm μ
  simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
⊢ Nontrivial E

Tactic:
apply Module.nontrivial_of_finrank_pos (R := ℝ)

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
⊢ 0 < Module.finrank ℝ E
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n : ℕ
hn : n ≠ 0
a b : ℕ
⊢ b ^ n ≤ a ^ n ↔ b ≤ a

Tactic:
exact (Nat.pow_left_strictMono hn).le_iff_le

Goal state after: