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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this✝² : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this✝¹ : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst✝ : Algebra L C := iL.toAlgebra
this✝ : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := of_completeSpace_of_normal K C
norm_iL : ∀ (x : L), ‖iL x‖ = ‖x‖
⊢ x ∈ K⟮y⟯

Tactic:
suffices this : iL x ∈ K⟮iL y⟯ by
      simpa [← Set.image_singleton, ← IntermediateField.adjoin_map] using! this

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this✝² : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this✝¹ : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst✝ : Algebra L C := iL.toAlgebra
this✝ : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := of_completeSpace_of_normal K C
norm_iL : ∀ (x : L), ‖iL x‖ = ‖x‖
⊢ iL x ∈ K⟮iL y⟯
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
this : ‖v 0‖ ≤ ‖h‖ + b 0
⊢ C * (‖h‖ + b 0) = C * b 0 + C * ‖h‖

Tactic:
rw [add_comm, mul_add]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
δpos : δ > 0
hε : (δ / max ‖a‖ 1) ^ f.natDegree / (↑f.natDegree + 1) > 0
g : K[X]
gmon : g.Monic
gdeg : f.natDegree = g.natDegree
gcoeff : ∀ (n : ℕ), ‖(map (algebraMap K L) g).coeff n - f.coeff n‖ < (δ / max ‖a‖ 1) ^ f.natDegree / (↑f.natDegree + 1)
b : f.SplittingField
hab✝ :
  ‖a - b‖ < ((↑f.natDegree + 1) * ((δ / max ‖a‖ 1) ^ f.natDegree / (↑f.natDegree + 1))) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1
hab : ‖a - b‖ < δ
bbot : b ∈ ⊥
hb : ¬g = 0 ∧ (aeval b) (map (algebraMap K L) g) = 0
abot : a ∈ ⊥
aCp : L
haCp : (algebraMap L f.SplittingField) aCp = a
⊢ (algebraMap L F) (eval aCp f) = (algebraMap L F) 0

Tactic:
← Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval,

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
δpos : δ > 0
hε : (δ / max ‖a‖ 1) ^ f.natDegree / (↑f.natDegree + 1) > 0
g : K[X]
gmon : g.Monic
gdeg : f.natDegree = g.natDegree
gcoeff : ∀ (n : ℕ), ‖(map (algebraMap K L) g).coeff n - f.coeff n‖ < (δ / max ‖a‖ 1) ^ f.natDegree / (↑f.natDegree + 1)
b : f.SplittingField
hab✝ :
  ‖a - b‖ < ((↑f.natDegree + 1) * ((δ / max ‖a‖ 1) ^ f.natDegree / (↑f.natDegree + 1))) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1
hab : ‖a - b‖ < δ
bbot : b ∈ ⊥
hb : ¬g = 0 ∧ (aeval b) (map (algebraMap K L) g) = 0
abot : a ∈ ⊥
aCp : L
haCp : (algebraMap L f.SplittingField) aCp = a
⊢ (aeval ((algebraMap L F) aCp)) f = (algebraMap L F) 0
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : (Hom.hom g).NormNoninc
⊢ (Hom.hom (explicitCokernelDesc cond)).NormNoninc

Tactic:
refine NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.2 ?_

Goal state after:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : (Hom.hom g).NormNoninc
⊢ ‖Hom.hom (explicitCokernelDesc cond)‖ ≤ 1
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
y : L
hy✝ : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
hy : -y = (algebraMap (↥K⟮y⟯) L) (-g)
⊢ spectralNorm K L (-y) = spectralNorm K L y

Tactic:
rw [← spectralNorm.eq_of_normalClosure g (IntermediateField.AdjoinSimple.algebraMap_gen K y), hy,
    ← spectralNorm.eq_of_normalClosure (-g) hy, map_neg,
    ← spectralAlgNorm_of_finiteDimensional_normal_def]

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
y : L
hy✝ : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
hy : -y = (algebraMap (↥K⟮y⟯) L) (-g)
⊢ (spectralAlgNorm_of_finiteDimensional_normal K ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      (-(algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g) =
    spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      ((algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g)
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
x y : L
hx : IsAlgebraic K x
hy : IsAlgebraic K y
⊢ spectralNorm K L (x * y) ≤ spectralNorm K L x * spectralNorm K L y

Tactic:
by
  set E := K⟮x, y⟯
  have h_finiteDimensional_E : FiniteDimensional K E :=
    IntermediateField.finiteDimensional_adjoin_pair hx.isIntegral hy.isIntegral
  set gx := IntermediateField.AdjoinPair.gen₁ K x y
  set gy := IntermediateField.AdjoinPair.gen₂ K x y
  have hxy : x * y = (algebraMap K⟮x, y⟯ L) (gx * gy) := rfl
  rw [hxy, ← spectralNorm.eq_of_normalClosure (gx * gy) hxy,
    ← spectralNorm.eq_of_normalClosure gx (IntermediateField.AdjoinPair.algebraMap_gen₁ K x y),
    ← spectralNorm.eq_of_normalClosure gy (IntermediateField.AdjoinPair.algebraMap_gen₂ K x y),
    map_mul, ← spectralAlgNorm_of_finiteDimensional_normal_def]
  exact map_mul_le_mul _ _ _

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : ↑m ≠ 0
⊢ μ ((x ^ m) ^ n) ^ (1 / ↑m * (1 / ↑n) * ↑m) = μ ((x ^ m) ^ n) ^ (1 / ↑n)

Tactic:
mul_comm (1 / (m : ℝ)),

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : ↑m ≠ 0
⊢ μ ((x ^ m) ^ n) ^ (1 / ↑n * (1 / ↑m) * ↑m) = μ ((x ^ m) ^ n) ^ (1 / ↑n)
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
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x : L
E : Type v := ((mapAlg K L) (minpoly K x)).SplittingField
hspl : ((mapAlg K E) (minpoly K x)).Splits
this✝ : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ spectralNorm K L x ^ ↑(minpoly K x).natDegree = ‖(minpoly K x).coeff 0‖

pp: K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x : L
E : Type v := ((mapAlg K L) (minpoly K x)).SplittingField
hspl : ((mapAlg K E) (minpoly K x)).Splits
this✝ : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ ↑(minpoly K x).natDegree ≠ 0

Tactic:
Real.rpow_natCast,

Goal state after:
K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x : L
E : Type v := ((mapAlg K L) (minpoly K x)).SplittingField
hspl : ((mapAlg K E) (minpoly K x)).Splits
this✝ : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ spectralNorm K L x ^ (minpoly K x).natDegree = ‖(minpoly K x).coeff 0‖

K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x : L
E : Type v := ((mapAlg K L) (minpoly K x)).SplittingField
hspl : ((mapAlg K E) (minpoly K x)).Splits
this✝ : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ ↑(minpoly K x).natDegree ≠ 0
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
inst✝ : NormMulClass R
hf : ∀ (i : ι), 1 + f i ≠ 0
hu : Summable fun x ↦ ‖f x‖
⊢ Multipliable fun i ↦ 1 + f i

Tactic:
exact multipliable_one_add_of_summable hu

Goal state after:
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✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F
⊢ (liftIsometry 𝕜 E F).symm l = l.compContinuousMultilinearMap (tprodL 𝕜)

Tactic:
by
  rfl

Goal state after:
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✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x : ⨂[𝕜] (i : ι), E i
⊢ (mapL f) x = (map fun i ↦ ↑(f i)) x

Tactic:
by
  rfl

Goal state after:
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✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_5
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
c : 𝕜
u : E i →L[𝕜] E' i
⊢ mapL (update f i (c • u)) = c • mapL (update f i u)

Tactic:
ext
  simp [mapL_add_smul_aux, PiTensorProduct.map_update_smul]

Goal state after:
Module: Mathlib.Analysis.Normed.Order.Hom.Ultra

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroup α
inst✝ : AddGroupSeminormClass F α ℝ
inst : Dist α
f : F
hna : IsNonarchimedean ⇑f
hd : inst = (toSeminormedAddGroup f).toDist
x y z : α
⊢ dist x z ≤ max (dist x y) (dist y z)

Tactic:
by
    simp +instances only [hd, dist_eq_norm_neg_add,
      AddGroupSeminormClass.toSeminormedAddGroup_norm_eq]
    convert! hna (-x + y) (-y + z) using 2
    rw [add_assoc, ← add_assoc y, add_neg_cancel, zero_add]

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

Goal state before:
pp: 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
⊢ u n ≤ (u n₀ + ∑ k ∈ Ico n₀ n₁, b k) * rexp (∑ i ∈ Ico n₀ n₁, c i)

Tactic:
exact (discrete_gronwall hun₀ hu hc hb (mem_Ico.mp hn).1).trans (by gcongr <;> grind)

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 ((FunSpace.toContinuousMap (α x hx)) (projIcc tmin tmax ⋯ t)) ((α y hy).toFun (projIcc tmin tmax ⋯ t)) ≤
    ↑L' * dist x y

Tactic:
← 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: 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 : ℕ
⊢ dist α ((next hf hx)^[n] α) ≤
    (∑ i ∈ Finset.range n, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * dist α (next hf hx α)

Tactic:
by
  nth_rw 1 [← iterate_zero_apply (next hf hx) α]
  rw [Finset.sum_mul]
  apply dist_le_range_sum_of_dist_le (f := fun i ↦ (next hf hx)^[i] α)
  intro i hi
  rw [iterate_succ_apply]
  exact dist_iterate_next_iterate_next_le hf hx _ _ i

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n : ℕ
⊢ dist ((next hf hx)^[0] α) ((next hf hx)^[m]^[n] α) ≤
    ∑ i ∈ Finset.range n,
      (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑C ^ i * dist α (next hf hx α)

Tactic:
apply dist_le_range_sum_of_dist_le (f := fun i ↦ (next hf hx)^[m]^[i] α)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n : ℕ
⊢ ∀ {k : ℕ},
    k < n →
      dist ((next hf hx)^[m]^[k] α) ((next hf hx)^[m]^[k + 1] α) ≤
        (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑C ^ k * dist α (next hf hx α)
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case hbc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n i : ℕ
hi : i < n
⊢ dist α ((next hf hx)^[m] α) ≤
    (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * dist α (next hf hx α)

Tactic:
exact dist_iterate_next_le hf hx α m

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

Goal state before:
pp: case neg.inl
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
h : tmax < tmin
x✝ : ℝ
ht : x✝ ∈ Icc tmin tmax
⊢ ContDiffWithinAt ℝ (↑n) α (Icc tmin tmax) x✝

Tactic:
Icc_eq_empty (not_le.mpr h)

Goal state after:
case neg.inl
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
h : tmax < tmin
x✝ : ℝ
ht : x✝ ∈ ∅
⊢ ContDiffWithinAt ℝ (↑n) α (Icc tmin tmax) x✝
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
inst✝ : Semiring R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
⊢ gaussNorm v c f ≠ 0

Tactic:
apply ne_of_gt

Goal state after:
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
inst✝ : Semiring R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
⊢ 0 < gaussNorm v c f
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
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
hα : IsFixedPt (FunSpace.next hf hx) α
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ picard f (↑t₀) x α.compProj ↑(projIcc tmin tmax ⋯ t) = picard f (↑t₀) x α.compProj t

Tactic:
projIcc_of_mem _ ht

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace 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
hα : IsFixedPt (FunSpace.next hf hx) α
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ picard f (↑t₀) x α.compProj ↑⟨t, ht⟩ = picard f (↑t₀) x α.compProj 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
hlc' : 0 ≤ ↑↑(↑(P.comp (-X)).natDegree).negOnePow * (P.comp (-X)).leadingCoeff
h : Odd P.natDegree
⊢ 0 < ↑↑(↑P.natDegree).negOnePow * eval x P

Tactic:
rw [Int.negOnePow_odd] at hlc' ⊢

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
hlc' : 0 ≤ ↑↑(-1) * (P.comp (-X)).leadingCoeff
h : Odd P.natDegree
⊢ 0 < ↑↑(-1) * eval x P

case hn
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
hlc' : 0 ≤ ↑↑(-1) * (P.comp (-X)).leadingCoeff
h : Odd P.natDegree
⊢ Odd ↑P.natDegree

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

Goal state before:
pp: p : ℂ[X]
hp : p ≠ 0
⊢ p.mahlerMeasure = rexp ((2 * π)⁻¹ * ∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖)

Tactic:
simp [mahlerMeasure, hp, logMahlerMeasure_def, circleAverage_def]

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

Goal state before:
pp: p : ℂ[X]
⊢ p = 0 → p.mahlerMeasure = 0

Tactic:
simp_all [mahlerMeasure_zero]

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

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

Tactic:
by apply neg_nonneg.mp; simpa

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

Goal state before:
pp: case refine_2
p : ℂ[X]
this✝ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
⊢ InjOn (circleMap 0 1) {a | a ∈ uIoc 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0}

Tactic:
grw [ofPred_and, inter_subset_left]

Goal state after:
case refine_2
p : ℂ[X]
this✝ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
⊢ InjOn (circleMap 0 1) {a | a ∈ uIoc 0 (2 * π)}
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
this✝ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
⊢ |0 - 2 * π| ≤ 2 * π

Tactic:
simp [abs_of_pos pi_pos]

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

Goal state before:
pp: p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ √(⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖ ^ 2) = √(circleAverage (fun θ ↦ ‖eval θ p‖ ^ 2) 0 1)

Tactic:
simp [circleAverage_eq_intervalAverage]

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

Goal state before:
pp: case neg
x : ℝ*
h : ¬∃ r, x.IsSt r
⊢ 0 = stdPart x

Tactic:
isSt_iff

Goal state after:
case neg
x : ℝ*
h : ¬∃ r, 0 ≤ ArchimedeanClass.mk x ∧ stdPart x = r
⊢ 0 = stdPart x
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
m : ℤ
h : Irrational (↑m + x)
⊢ Irrational x

Tactic:
rw [← cast_intCast] at h
  exact h.of_ratCast_add m

Goal state after: