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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
⊢ Tendsto (fun x ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))

Tactic:
Metric.tendsto_nhds

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
⊢ ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑' (k : β), f x k) (∑' (k : β), g k) < ε
Module: Mathlib.Analysis.Normed.Group.Tannery

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : Tendsto (fun s ↦ ∑ b ∈ s, bound b) (SummationFilter.unconditional β).filter (𝓝 S)
⊢ ∃ T, dist (∑ b ∈ T, bound b) S < ε / 3

Tactic:
Metric.tendsto_nhds

Goal state after:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : ∀ ε > 0, ∀ᶠ (x : Finset β) in (SummationFilter.unconditional β).filter, dist (∑ b ∈ x, bound b) S < ε
⊢ ∃ T, dist (∑ b ∈ T, bound b) S < ε / 3
Module: Mathlib.Analysis.Normed.Group.Tannery

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3
h2 : Tendsto (fun x ↦ ∑ k ∈ T, f x k) 𝓕 (𝓝 (T.sum g))
⊢ ∀ᶠ (x : α) in 𝓕, dist (∑' (k : β), f x k) (∑' (k : β), g k) < ε

Tactic:
Metric.tendsto_nhds

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
⊢ ∀ᶠ (x : α) in 𝓕, dist (∑' (k : β), f x k) (∑' (k : β), g k) < ε
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 : ℝ
hr : (spectralMulAlgNorm K E) ((algebraMap L E) x) = r
s : ℝ
hs : s ∈ Multiset.map (⇑(spectralMulAlgNorm K E)) ((mapAlg K E) (minpoly K x)).roots
a : E
ha : a ∈ ((mapAlg K E) (minpoly K x)).roots
has : (spectralMulAlgNorm K E) a = s
⊢ (spectralMulAlgNorm K E) ((algebraMap L E) x) = (spectralMulAlgNorm K E) a

Tactic:
spectralMulAlgNorm_eq_of_mem_roots K L x ha

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 : ℝ
hr : (spectralMulAlgNorm K E) ((algebraMap L E) x) = r
s : ℝ
hs : s ∈ Multiset.map (⇑(spectralMulAlgNorm K E)) ((mapAlg K E) (minpoly K x)).roots
a : E
ha : a ∈ ((mapAlg K E) (minpoly K x)).roots
has : (spectralMulAlgNorm K E) a = s
⊢ (spectralMulAlgNorm K E) ((algebraMap L E) x) = (spectralMulAlgNorm K E) ((algebraMap L E) x)
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ᶜ * ↑Pᶜ) * ↑R = ↑P + ↑Q * ↑R * ↑Pᶜ

Tactic:
Pᶜ.prop.proj.eq,

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 }
⊢ ↑P + ↑Q * ↑Pᶜ * ↑R = ↑P + ↑Q * ↑R * ↑Pᶜ
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
m : (i : ι) → E i
⊢ FreeAddMonoid.of (1, m) ∈ (⨂ₜ[𝕜] (i : ι), m i).lifts

Tactic:
simp [mem_lifts_iff]

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✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this : ∀ (x : V →L[𝕜] V), adjoint ↑y ∘SL ↑y ∘SL adjoint x ∘SL ↑y.symm = adjoint x ∘SL adjoint ↑y
x : V →L[𝕜] V
⊢ (x ∘SL adjoint ↑y) ∘SL ↑y = (adjoint ↑y ∘SL ↑y) ∘SL x

Tactic:
← (adjoint_adjoint x ▸ this _),

Goal state after:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this : ∀ (x : V →L[𝕜] V), adjoint ↑y ∘SL ↑y ∘SL adjoint x ∘SL ↑y.symm = adjoint x ∘SL adjoint ↑y
x : V →L[𝕜] V
⊢ (adjoint ↑y ∘SL ↑y ∘SL x ∘SL ↑y.symm) ∘SL ↑y = (adjoint ↑y ∘SL ↑y) ∘SL x
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ∞
hxy : edist x y ≠ ∞
⊢ efixedPoint' f hsc hsf hfs x hxs hx = efixedPoint' f htc htf hft y hyt hy

Tactic:
refine (hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h')
    <;> try apply efixedPoint_isFixedPt'
  change Metric.edistLtTopSetoid _ _
  trans x
  · apply Setoid.symm'
    apply edist_efixedPoint_lt_top'
  trans y
  · exact lt_top_iff_ne_top.2 hxy
  · apply edist_efixedPoint_lt_top'

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

Goal state before:
pp: case refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace 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
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
L' : ℝ≥0
h :
  ∀ (x y : E) (hx : x ∈ closedBall x₀ ↑r) (hy : y ∈ closedBall x₀ ↑r) (α β : FunSpace t₀ x₀ r L),
    IsFixedPt (FunSpace.next hf hx) α → IsFixedPt (FunSpace.next hf hy) β → dist α β ≤ ↑L' * dist x y
t : ℝ
ht : t ∈ Icc tmin tmax
x : E
hx : x ∈ closedBall x₀ ↑r
y : E
hy : y ∈ closedBall x₀ ↑r
⊢ dist ((if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0) t)
      ((if hx : y ∈ closedBall x₀ ↑r then (α y hx).compProj else 0) t) ≤
    ↑L' * dist x y

Tactic:
rw [dif_pos hx, dif_pos hy, FunSpace.compProj_apply, FunSpace.compProj_apply,
      ← FunSpace.toContinuousMap_apply_eq_apply, ← FunSpace.toContinuousMap_apply_eq_apply]

Goal state after:
case refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace 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
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
L' : ℝ≥0
h :
  ∀ (x y : E) (hx : x ∈ closedBall x₀ ↑r) (hy : y ∈ closedBall x₀ ↑r) (α β : FunSpace t₀ x₀ r L),
    IsFixedPt (FunSpace.next hf hx) α → IsFixedPt (FunSpace.next hf hy) β → dist α β ≤ ↑L' * dist x y
t : ℝ
ht : t ∈ Icc tmin tmax
x : E
hx : x ∈ closedBall x₀ ↑r
y : E
hy : y ∈ closedBall x₀ ↑r
⊢ dist ((FunSpace.toContinuousMap (α x hx)) (projIcc tmin tmax ⋯ t))
      ((FunSpace.toContinuousMap (α y hy)) (projIcc tmin tmax ⋯ t)) ≤
    ↑L' * dist x y
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case succ
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)
⊢ ‖(next hf hx ((next hf hx)^[n] α)).toFun t - (next hf hx ((next hf hx)^[n] β)).toFun t‖ ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
next_apply,

Goal state after:
case succ
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)
⊢ ‖picard f (↑t₀) x ((next hf hx)^[n] α).compProj ↑t - (next hf hx ((next hf hx)^[n] β)).toFun t‖ ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case succ
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)
⊢ ‖picard f (↑t₀) x ((next hf hx)^[n] α).compProj ↑t - (next hf hx ((next hf hx)^[n] β)).toFun t‖ ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
next_apply,

Goal state after:
case succ
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)
⊢ ‖picard f (↑t₀) x ((next hf hx)^[n] α).compProj ↑t - picard f (↑t₀) x ((next hf hx)^[n] β).compProj ↑t‖ ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x ↦ eval x P / eval x Q) atBot (𝓝 0)
⊢ P.degree < Q.degree

Tactic:
rw [← P.degree_comp_neg_X, ← Q.degree_comp_neg_X]

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x ↦ eval x P / eval x Q) atBot (𝓝 0)
⊢ (P.comp (-X)).degree < (Q.comp (-X)).degree
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ t : ℝ
hf : ContinuousOn (uncurry f) (uIcc t₀ t ×ˢ u)
hα : ∀ t' ∈ uIcc t₀ t, HasDerivWithinAt α (f t' (α t')) (uIcc t₀ t) t'
hmap : MapsTo α (uIcc t₀ t) u
⊢ picard f t₀ (α t₀) α t = α t

Tactic:
rw [← add_sub_cancel (α t₀) (α t), picard_apply,
    integral_eq_sub_of_hasDeriv_right (HasDerivWithinAt.continuousOn hα) _
      (continuousOn_comp hf (HasDerivWithinAt.continuousOn hα) hmap |>.intervalIntegrable)]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ t : ℝ
hf : ContinuousOn (uncurry f) (uIcc t₀ t ×ˢ u)
hα : ∀ t' ∈ uIcc t₀ t, HasDerivWithinAt α (f t' (α t')) (uIcc t₀ t) t'
hmap : MapsTo α (uIcc t₀ t) u
⊢ ∀ x ∈ Ioo (min t₀ t) (max t₀ t), HasDerivWithinAt α (f x (α x)) (Ioi x) x
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: P Q : ℤ[X]
mQ : Q.Monic
h : {a | eval a Q ∣ eval a P}.Infinite
⊢ Q ∣ P

Tactic:
have eqR := modByMonic_add_div P Q
  have degR := degree_modByMonic_lt P mQ
  rw [← modByMonic_eq_zero_iff_dvd mQ]
  set R := P %ₘ Q
  apply eq_zero_of_infinite_isRoot
  refine (h.sdiff (finite_abs_eval_le_of_degree_lt degR)).mono fun x mx ↦ ?_
  simp only [Set.mem_sdiff, Set.mem_ofPred_eq, not_le] at mx
  rw [← eqR, eval_add, eval_mul, Int.dvd_add_self_mul, ← abs_dvd] at mx
  exact Int.eq_zero_of_abs_lt_dvd mx.1 mx.2

Goal state after:
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)
h : g (∑ i ∈ s, f i) ≤ g (f j)
⊢ g (f j + ∑ i ∈ s, f i) ≤ g (f j)

Tactic:
exact (na _ _).trans (max_eq_left h).le

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

Goal state before:
pp: p : ℂ[X]
⊢ ‖p.leadingCoeff‖ ≤ p.mahlerMeasure

Tactic:
rw [← mul_one ‖_‖, mahlerMeasure_eq_leadingCoeff_mul_prod_roots]

Goal state after:
p : ℂ[X]
⊢ ‖p.leadingCoeff‖ * 1 ≤ ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:

Tactic:
π / 2 ^ (n + 2) - sin (π / 2 ^ (n + 2)) < (π / 2 ^ (n + 2)) ^ 3 / 6 :=
        sub_lt_comm.1 <| sin_gt_sub_cube (by positivity)
      _ ≤ (4 / 2 ^ (n + 2)) ^ 3 / 4 := by gcongr; exacts [pi_le_four, by norm_num]
      _ = 1 / (2 ^ n) ^ 3 / 4 := by simp [add_comm n, pow_add, div_mul_eq_div_div]; norm_num

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

Goal state before:
pp: x : ℝ*
hni : ¬x.Infinite
⊢ x.IsSt (sSup {y | ↑y < x})

Tactic:
rw [infinite_iff, not_lt] at hni
  rw [isSt_iff]
  exact ⟨hni, stdPart_eq_sSup coeRingHom x⟩

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

Goal state before:
pp: x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : 0 < r₁ ∧ ¬(-↑r₁ < y ∧ y < ↑r₁)
⊢ 0 < r₁ ∧ ↑r₁ ≤ y

Tactic:
← abs_lt,

Goal state after:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : 0 < r₁ ∧ ¬|y| < ↑r₁
⊢ 0 < r₁ ∧ ↑r₁ ≤ y
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ (π / 2)⁻¹ * W k = (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)

Tactic:
integral_sin_pow_even,

Goal state after:
k : ℕ
⊢ (π / 2)⁻¹ * W k = (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) / (π * ∏ i ∈ range k, (2 * ↑i + 1) / (2 * ↑i + 2))
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ cosh (arcosh x) = x

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

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

Goal state before:
pp: this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i ↦ (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 (π / 2))

Tactic:
rw [this]

Goal state after:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i ↦ (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 ((1 - 0) * (π / 2)))
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ -(π / 2) < (1 + z).arg ∧ (1 + z).arg < π / 2

Tactic:
← abs_lt,

Goal state after:
z : ℂ
hz : ‖z‖ < 1
⊢ |(1 + z).arg| < π / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ (x.agmSequences y 0).2 ≤ y

Tactic:
agmSequences_zero

Goal state after:
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ (sqrt (x * y), (x + y) / 2).2 ≤ y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ x ≤ (x.agmSequences y 0).1

Tactic:
agmSequences_zero

Goal state after:
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ x ≤ (sqrt (x * y), (x + y) / 2).1
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: ⊢ StrictMonoOn (fun x ↦ (1 + x) / (1 - x)) (Ioo (-1) 1)

Tactic:
intro x hx y hy h
  field_simp [show 0 < 1 - x by grind, show 0 < 1 - y by grind]
  grind

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

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
h : x < y
⊢ x ≤ (x.agmSequences y 0).1

Tactic:
agmSequences_zero

Goal state after:
x✝ y✝ x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
h : x < y
⊢ x ≤ (sqrt (x * y), (x + y) / 2).1
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
hn : x ≠ y
h : x < y
⊢ (x.agmSequences y 0).2 ≤ y

Tactic:
agmSequences_zero

Goal state after:
x✝ y✝ x y : ℝ≥0
hn : x ≠ y
h : x < y
⊢ (sqrt (x * y), (x + y) / 2).2 ≤ y
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
this : (fun p ↦ log (↑q - 1) + log (1 - p) - log p) = fun p ↦ log (↑q - 1) + (log (1 - p) - log p)
⊢ Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot

Tactic:
rw [this]

Goal state after:
q : ℕ
this : (fun p ↦ log (↑q - 1) + log (1 - p) - log p) = fun p ↦ log (↑q - 1) + (log (1 - p) - log p)
⊢ Tendsto (fun p ↦ log (↑q - 1) + (log (1 - p) - log p)) (𝓝[<] 1) atBot
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
this : (fun p ↦ log (↑q - 1) + log (1 - p) - log p) = fun p ↦ log (↑q - 1) + (log (1 - p) - log p)
⊢ Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop

Tactic:
rw [this]

Goal state after:
q : ℕ
this : (fun p ↦ log (↑q - 1) + log (1 - p) - log p) = fun p ↦ log (↑q - 1) + (log (1 - p) - log p)
⊢ Tendsto (fun p ↦ log (↑q - 1) + (log (1 - p) - log p)) (𝓝[>] 0) atTop
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt

Goal state before:
pp: case pos
A : Type u_1
inst✝¹⁰ : PartialOrder A
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : Algebra ℝ A
inst✝⁴ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : SeparatelyContinuousMul A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
c a : A
hc : IsStrictlyPositive c
ha : IsUnit a
⊢ ((conjSqrt c) a)⁻¹ʳ = (conjSqrt c⁻¹ʳ) a⁻¹ʳ

Tactic:
grind [conjSqrt_apply]

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

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
⊢ StrictMonoOn (qaryEntropy q) (Icc 0 (1 - 1 / ↑q))

Tactic:
intro p1 hp1 p2 hp2 p1le2
  apply strictMonoOn_of_deriv_pos (convex_Icc 0 (1 - 1 / (q : ℝ))) _ _ hp1 hp2 p1le2
  · exact qaryEntropy_continuous.continuousOn
  · intro p hp
    have : 2 ≤ (q : ℝ) := Nat.ofNat_le_cast.mpr qLe2
    have zero_le_qinv : 0 < (q : ℝ)⁻¹ := by positivity
    have : 0 < 1 - p := by
      simp only [sub_pos]
      have p_lt_1_minus_qinv : p < 1 - (q : ℝ)⁻¹ := by
        simp_all only [inv_pos, interior_Icc, mem_Ioo, one_div]
      linarith
    simp only [one_div, interior_Icc, mem_Ioo] at hp
    rw [deriv_qaryEntropy (by linarith)]
    · simp only [sub_pos, gt_iff_lt]
      rw [← log_mul (by linarith) (by linarith)]
      apply Real.strictMonoOn_log (mem_Ioi.mpr hp.1)
      · simp_all only [mem_Ioi, mul_pos_iff_of_pos_left, show 0 < (q : ℝ) - 1 by linarith]
      · have qpos : 0 < (q : ℝ) := by positivity
        have : q * p < q - 1 := by
          convert! mul_lt_mul_of_pos_left hp.2 qpos using 1
          simp only [mul_sub, mul_one, isUnit_iff_ne_zero, ne_eq, ne_of_gt qpos, not_false_eq_true,
            IsUnit.mul_inv_cancel]
        linarith
    exact (ne_of_gt (lt_add_neg_iff_lt.mp this : p < 1)).symm

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

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

Tactic:
rcases eq_or_ne b 0 with rfl | hb
  · rcases k.eq_zero_or_pos with rfl | hk
    · exact ⟨p.coeff 0, by simp⟩
    exact ⟨0, by simp [hk.ne']⟩
  refine ⟨∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i), ?_⟩
  conv => lhs; rw [← sum_monomial_eq p]
  rw [eval₂_sum, sum, Finset.sum_mul, Int.cast_sum]
  simp only [eval₂_monomial, eq_intCast, div_pow, Int.cast_mul, Int.cast_pow]
  refine Finset.sum_congr rfl (fun i hi => ?_)
  have ik := (le_natDegree_of_mem_supp i hi).trans hp
  rw [mul_assoc, div_mul_comm, ← Int.cast_pow, ← Int.cast_pow, ← Int.cast_pow,
    ← pow_sub_mul_pow b ik, ← Int.cast_div_charZero, Int.mul_ediv_cancel _ (pow_ne_zero _ hb),
    ← mul_assoc, mul_right_comm, ← Int.cast_pow]
  exact dvd_mul_left _ _

Goal state after: