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

Goal state before:
pp: case pos
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
⊢ ∃ g, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖

Tactic:
hyp_h

Goal state after:
case pos
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
⊢ ∃ g, f g = 0 ∧ ‖g‖ ≤ (C + ε) * ‖0‖
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✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h : 0 < ↑p.natDegree - ↑m
⊢ s.card = p.natDegree

Tactic:
← natDegree_map (algebraMap K L),

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h : 0 < ↑p.natDegree - ↑m
⊢ s.card = (Polynomial.map (algebraMap K L) p).natDegree
Module: Mathlib.Analysis.Normed.Group.HomCompletion

Goal state before:
pp: G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in : f.completion hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑g‖ < δ
g' : G
hgg' : f g' = f g
hfg : ‖g'‖ ≤ C' * ‖f g‖
⊢ g - g' ∈ f.ker

Tactic:
f.mem_ker,

Goal state after:
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in : f.completion hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑g‖ < δ
g' : G
hgg' : f g' = f g
hfg : ‖g'‖ ≤ C' * ‖f g‖
⊢ f (g - g') = 0
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun n ↦ ↑(nu n) / ↑n) ∘ ψ) atTop (𝓝 b)
b_in : b ∈ Set.Icc 0 1
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx : limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
hy : limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ y ^ b
hxy :
  limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
h : smoothingFun μ x ≤ smoothingFun μ y
⊢ smoothingFun μ x ^ a * smoothingFun μ y ^ b ≤ smoothingFun μ y

Tactic:
apply le_trans (mul_le_mul_of_nonneg_right
        (rpow_le_rpow (smoothingFun_nonneg μ hμ1 _) h a_in.1)
        (rpow_nonneg (smoothingFun_nonneg μ hμ1 _) _))

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := ⋯
nu : ℕ → ℕ := ⋯
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := ⋯
hb : b = 1 - a
hb_lim : Tendsto ((fun n ↦ ↑(nu n) / ↑n) ∘ ψ) atTop (𝓝 b)
b_in : b ∈ Set.Icc 0 1
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx : limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
hy : limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ y ^ b
hxy :
  limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
h : smoothingFun μ x ≤ smoothingFun μ y
⊢ smoothingFun μ y ^ a * smoothingFun μ y ^ b ≤ smoothingFun μ y
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 : 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) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable fun x ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ ε = ε / 3 + (ε / 3 + ε / 3)

Tactic:
ring

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

Goal state before:
pp: case neg
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
⊢ 0 = Multiset.count r (Multiset.map (⇑(spectralMulAlgNorm K E)) ((mapAlg K E) (minpoly K x)).roots)

Tactic:
rw [Multiset.count_eq_zero_of_notMem]

Goal state after:
case neg
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
⊢ r ∉ Multiset.map (⇑(spectralMulAlgNorm K E)) ((mapAlg K E) (minpoly K x)).roots
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: 𝕜 : Type u_7
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_8
F : Type u_9
inst✝¹² : TopologicalSpace E
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : T2Space F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 F
hf : Injective ⇑f
⊢ f.HasLeftInverse

Tactic:
obtain ⟨g, hg⟩ :=
    f.toLinearMap.exists_leftInverse_of_injective (f.ker_eq_bot_of_injective hf)
  exact ⟨⟨g, LinearMap.continuous_of_finiteDimensional _⟩, fun x ↦ congr($hg x)⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
F : Type u_4
G : Type u_6
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
⊢ (snd R F G).HasRightInverse

Tactic:
by
  use ContinuousLinearMap.prod 0 (.id R G)
  intro x
  simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
IH : ‖∏ i ∈ t, (1 + f i) - 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1
⊢ (1 + f x) * ∏ i ∈ t, (1 + f i) - 1 = ∏ i ∈ t, (1 + f i) - 1 + f x * ∏ x ∈ t, (1 + f x)

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Goal state before:
pp: α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (fun i x ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove ((fun x ↦ (∑' (i : ι), log (f i x)).re) '' s)
⊢ HasProdUniformlyOn f (fun x ↦ ∏' (i : ι), f i x) s

Tactic:
by
  simp only [hasProdUniformlyOn_iff_tendstoUniformlyOn]
  obtain ⟨r, hr⟩ := hf.exists
  suffices H : TendstoUniformlyOn (fun s x ↦ ∏ i ∈ s, f i x) (cexp ∘ r) atTop s by
    refine H.congr_right (hr.tsum_eqOn.comp_left.symm.trans ?_)
    exact fun x hx ↦ (cexp_tsum_eq_tprod (hfn x hx) (hf.summable hx))
  refine (hr.tendstoUniformlyOn.comp_cexp ?_).congr ?_
  · simpa +contextual [← hr.tsum_eqOn _] using hg
  · filter_upwards with s i hi using by simp [exp_sum, fun y ↦ exp_log (hfn i hi y)]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ injectiveSeminorm ≤ projectiveSeminorm

Tactic:
rw [injectiveSeminorm]

Goal state after:
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ sSup
      {p |
        ∃ G x x_1,
          p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)} ≤
    projectiveSeminorm
Module: Mathlib.Topology.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : IsUpperSet s
⊢ IsUpperSet (interior s)

Tactic:
by
  rw [← isLowerSet_compl, ← closure_compl]
  exact h.compl.closure

Goal state after:
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case refine_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + 3 / 4 * δ = δ

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case refine_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + 3 / 4 * δ = δ

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
j : ℕ
hj : j ∈ Ico n₀ k
⊢ c k * (b j * ∏ i ∈ Ico (j + 1) k, c i) = b j * ((∏ k ∈ Ico (j + 1) k, c k) * c k)

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
heq :
  c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k =
    ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i
⊢ c k * (u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i) + b k =
    u n₀ * ((∏ x ∈ Ico n₀ k, c x) * c k) + (c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k)

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
⊢ edist x (efixedPoint' f hsc hsf hf x hxs hx) ≤ edist x (f x) / (1 - ↑K)

Tactic:
by
  convert! hf.apriori_edist_iterate_efixedPoint_le' hsc hsf hxs hx 0
  rw [pow_zero, mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
heq :
  c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k =
    ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i
⊢ c k * (u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i) + b k =
    u n₀ * ∏ i ∈ Ico n₀ (k + 1), c i + ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i

Tactic:
by
          rw [← heq, ← prod_Ico_mul_eq_prod_Ico_add_one hk]; ring

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 𝕜
⊢ (fun x ↦ eval x P) ~[atTop] fun x ↦ P.leadingCoeff * x ^ P.natDegree

Tactic:
by
  by_cases h : P = 0
  · simp [h, IsEquivalent.refl]
  · simp only [Polynomial.eval_eq_sum_range, sum_range_succ]
    exact
      IsLittleO.add_isEquivalent
        (IsLittleO.fun_sum fun i hi =>
          IsLittleO.const_mul_left
            ((IsLittleO.const_mul_right fun hz => h <| leadingCoeff_eq_zero.mp hz) <|
              isLittleO_pow_pow_atTop_of_lt (mem_range.mp hi))
            _)
        IsEquivalent.refl

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
n : ℕ
⊢ 0 ≤ (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n ! * dist α β

Tactic:
have : 0 ≤ max (tmax - t₀) (t₀ - tmin) := le_max_of_le_left <| sub_nonneg_of_le t₀.2.2
    positivity

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 : ℕ
hn : (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n ! < 1
this : 0 ≤ (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n !
⊢ ∃ n C, ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), ContractingWith C (next hf hx)^[n]

Tactic:
refine ⟨n, ⟨_, this⟩, fun x hx ↦ ?_⟩

Goal state after:
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 : ℕ
hn : (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n ! < 1
this : 0 ≤ (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n !
x : E
hx : x ∈ closedBall x₀ ↑r
⊢ ContractingWith ⟨(↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n !, this⟩ (next hf hx)^[n]
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
inst✝ : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), ContractingWith C (next hf hx)^[m]
L' : ℝ := (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑(1 - C)⁻¹
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ ↑r
hy : y ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ dist α β ≤ ↑(NNReal.mk L' hL') * dist x y

Tactic:
NNReal.coe_mk

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
inst✝ : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), ContractingWith C (next hf hx)^[m]
L' : ℝ := (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑(1 - C)⁻¹
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ ↑r
hy : y ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ dist α β ≤ L' * dist x y
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
P : R[X]
h : ¬P = 0
⊢ (fun x ↦ eval x P) ~[cobounded R] fun x ↦ P.leadingCoeff * x ^ P.natDegree

Tactic:
· simp only [eval_eq_sum_range, sum_range_succ]
    exact (IsLittleO.fun_sum fun i hi ↦
      ((isLittleO_pow_pow_cobounded_of_lt (mem_range.mp hi)).const_mul_right
        (leadingCoeff_ne_zero.mpr h)).const_mul_left _).add_isEquivalent .refl

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

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

Tactic:
← eqR,

Goal state after:
P Q : ℤ[X]
mQ : Q.Monic
h : {a | eval a Q ∣ eval a P}.Infinite
R : ℤ[X] := P %ₘ Q
eqR : R + Q * (P /ₘ Q) = P
degR : R.degree < Q.degree
x : ℤ
mx : eval x Q ∣ eval x (R + Q * (P /ₘ Q)) ∧ |eval x R| < |eval x Q|
⊢ x ∈ {x | R.IsRoot x}
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f ⟨t₀, ⋯⟩ x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < ↑a' - ↑r'
ε' : ℝ := min ε ((↑a' - ↑r') / (↑L + 1))
hε'pos : 0 < ε'
hε'_le : ε' ≤ ε
⊢ ↑L * ((↑a' - ↑r') / (↑L + 1)) = ↑L / (↑L + 1) * (↑a' - ↑r')

Tactic:
ring

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

Goal state before:

Tactic:
(L : ℝ) * ε'
    _ ≤ L * ((a' - r') / (L + 1)) := by gcongr; exact min_le_right _ _
    _ = L / (L + 1) * (a' - r') := by ring
    _ ≤ 1 * (a' - r') := by gcongr; rw [div_le_one (by positivity : (0 : ℝ) < L + 1)]; linarith
    _ = a' - r' := one_mul _

Goal state after:
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
⊢ (-1) ^ P.natDegree * P.leadingCoeff = P.leadingCoeff * (-1) ^ P.natDegree

Tactic:
ring

Goal state after:
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 ≤ ↑↑1 * (P.comp (-X)).leadingCoeff
h : Even P.natDegree
⊢ 0 < ↑↑1 * eval x P

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

Tactic:
push_cast 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
h : Odd P.natDegree
hlc' : 0 ≤ -1 * (P.comp (-X)).leadingCoeff
⊢ 0 < -1 * eval x P
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
vMul : ∀ (a b : R), v (a * b) ≤ v a * v b
vna : IsNonarchimedean v
vZero : v 0 = 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
t : σ →₀ ℕ
k : (σ →₀ ℕ) × (σ →₀ ℕ)
hk : (Finset.antidiagonal t).Nonempty → k ∈ Finset.antidiagonal t
hsum : v (∑ a ∈ Finset.antidiagonal t, (coeff a.1) f * (coeff a.2) g) ≤ v ((coeff k.1) f * (coeff k.2) g)
hk' : k.1 + k.2 = t
hprod : (t.prod fun x1 x2 ↦ c x1 ^ x2) = (k.1.prod fun x1 x2 ↦ c x1 ^ x2) * k.2.prod fun x1 x2 ↦ c x1 ^ x2
⊢ v ((coeff k.1) f) * v ((coeff k.2) g) * ((k.1.prod fun x1 x2 ↦ c x1 ^ x2) * k.2.prod fun x1 x2 ↦ c x1 ^ x2) =
    (v ((coeff k.1) f) * k.1.prod fun x1 x2 ↦ c x1 ^ x2) * (v ((coeff k.2) g) * k.2.prod fun x1 x2 ↦ c x1 ^ x2)

Tactic:
ring

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

Goal state before:
pp: case neg
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ rexp (π⁻¹ * 2⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log (‖eval (circleMap 0 1 θ) p‖ * ‖eval (circleMap 0 1 θ) q‖)) =
    rexp (π⁻¹ * 2⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) *
      rexp (π⁻¹ * 2⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) q‖)

Tactic:
← exp_add,

Goal state after:
case neg
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ rexp (π⁻¹ * 2⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log (‖eval (circleMap 0 1 θ) p‖ * ‖eval (circleMap 0 1 θ) q‖)) =
    rexp
      ((π⁻¹ * 2⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) +
        π⁻¹ * 2⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) q‖)
Module: Mathlib.Analysis.RCLike.ContinuousMap

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RCLike 𝕜
f g : C(X, ℝ)
hfg : realToRCLike 𝕜 f = realToRCLike 𝕜 g
⊢ f = g

Tactic:
ext x; simpa using congr($hfg x)

Goal state after:
Module: Mathlib.Analysis.RCLike.ContinuousMap

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RCLike 𝕜
f : C(X, 𝕜)
hf : IsSelfAdjoint f
a✝ : X
⊢ (realToRCLike 𝕜 f.rclikeToReal) a✝ = f a✝

Tactic:
simp only [realToRCLike_apply, rclikeToReal_apply, ← RCLike.conj_eq_iff_re]

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RCLike 𝕜
f : C(X, 𝕜)
hf : IsSelfAdjoint f
a✝ : X
⊢ (starRingEnd 𝕜) (f a✝) = f a✝
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vna : IsNonarchimedean v
vNeg : ∀ (a : R), v a = v (-a)
hbfg : HasGaussNorm v c (f * g)
i₀ j₀ : σ →₀ ℕ
hi₀ : (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c f
hj₀ : (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c g
hdom' :
  ∀ p ∈ Finset.antidiagonal (i₀ + j₀),
    p ≠ (i₀, j₀) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i₀) f) * v ((coeff j₀) g)
hprod : ((i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2) = (i₀.prod fun x1 x2 ↦ c x1 ^ x2) * j₀.prod fun x1 x2 ↦ c x1 ^ x2
⊢ (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) * (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) =
    v ((coeff i₀) f) * v ((coeff j₀) g) * ((i₀.prod fun x1 x2 ↦ c x1 ^ x2) * j₀.prod fun x1 x2 ↦ c x1 ^ x2)

Tactic:
ring

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:
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]]

Goal state after:
p : ℂ[X]
⊢ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2) ≤ √((↑p.natDegree + 1) * p.supNorm ^ 2)
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case e_a.e_f
b : ℕ
a : ℕ → Fin b
n i : ℕ
⊢ ↑↑(a (i + n)) * (↑b ^ (i + n + 1))⁻¹ = (↑b ^ n)⁻¹ * (↑↑(a (i + n)) * (↑b ^ (i + 1))⁻¹)

Tactic:
ring

Goal state after: