mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : a = 0
⊢ limsup (fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a

pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
⊢ limsup (fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a

Tactic:
· rw [ha] at hψ_lim
    calc limsup (fun n : ℕ => μ (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ))) atTop ≤
          limsup (fun n : ℕ => μ x ^ ((s (ψ n) : ℝ) * (1 / (ψ n : ℝ)))) atTop := by
          apply csInf_le_csInf _ (μ_nonempty μ hs_le ψ)
          · intro b hb
            simp only [eventually_map, eventually_atTop, Set.mem_ofPred_eq] at hb ⊢
            obtain ⟨m, hm⟩ := hb
            use m
            intro k hkm
            apply le_trans _ (hm k hkm)
            rw [rpow_mul (apply_nonneg μ x), rpow_natCast]
            gcongr
            exact map_pow_le_pow' hμ1 x _
          · use 0
            simp only [mem_lowerBounds, eventually_map, eventually_atTop,
              Set.mem_ofPred_eq, forall_exists_index]
            exact fun _ m hm ↦ le_trans (by positivity) (hm m (le_refl _))
      _ ≤ 1 := (μ_limsup_le_one μ hs_le hψ_lim)
      _ = smoothingFun μ x ^ a := by rw [ha, rpow_zero]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
⊢ limsup (fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
Module: Mathlib.Analysis.Normed.Group.HomCompletion

Goal state before:
pp: G : Type u_1
inst✝ : SeminormedAddCommGroup G
x : Completion G
⊢ (id G).completion x = (id (Completion G)) x

Tactic:
rw [NormedAddGroupHom.completion_def, NormedAddGroupHom.coe_id, Completion.map_id]

Goal state after:
G : Type u_1
inst✝ : SeminormedAddCommGroup G
x : Completion G
⊢ _root_.id x = (id (Completion G)) x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
v : V.carrier
⊢ ‖v‖ = ‖(ConcreteCategory.hom (i.hom ≫ i.inv)) v‖

Tactic:
Iso.hom_inv_id,

Goal state after:
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
v : V.carrier
⊢ ‖v‖ = ‖(ConcreteCategory.hom (𝟙 V)) v‖
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
⊢ ‖v‖ = ‖↑(Hom.hom (i.hom ≫ i.inv)) v‖

Tactic:
Iso.hom_inv_id,

Goal state after:
V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
⊢ ‖v‖ = ‖↑(Hom.hom (𝟙 V)) v‖
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
k : 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
hgy : k • y = (algebraMap (↥K⟮y⟯) L) (k • g)
⊢ (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) (k • g) =
    k • (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g

Tactic:
rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_assoc]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.Finsupp

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoEMetricSpace X
f g h : WithLp (↑p) (ι →₀ X)
⊢ ((zipWith edist ⋯ f.ofLp h.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹ ≤
    ((zipWith edist ⋯ f.ofLp g.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹ +
      ((zipWith edist ⋯ g.ofLp h.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹

Tactic:
have : 0 < p := zero_lt_one.trans_le Fact.out
    let s := f.ofLp.support ∪ g.ofLp.support ∪ h.ofLp.support
    rw [sum_of_support_subset (s := s) _ (by grind [support_zipWith]) _ (by simp [*]),
      sum_of_support_subset (s := s) _ (by grind [support_zipWith]) _ (by simp [*]),
      sum_of_support_subset (s := s) _ (by grind [support_zipWith]) _ (by simp [*])]
    simp only [zipWith_apply, ← one_div]
    grw [← ENNReal.Lp_add_le _ _ _ (mod_cast Fact.out)]
    gcongr
    exact edist_triangle ..

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 Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ (P * R) • x = (R * P * R) • x

Tactic:
by
      rw [← norm_sub_eq_zero_iff]
      have e1 : ‖R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
        calc
          ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
              (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) := by
            rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub,
              mul_smul]
          _ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
              (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖) := by
            rw [h₃.proj.eq, sub_smul 1 P, one_smul, smul_sub, mul_smul]
          _ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
              (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) := by
            rw [sub_mul, h₃.proj.eq, one_mul, sub_self, zero_smul, zero_sub, norm_neg]
          _ = ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖ := by abel
          _ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ := by
            rw [ge_iff_le]
            have :=
              add_le_add_left (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)
            simpa only [mul_smul, sub_smul, one_smul] using this
      rw [two_smul] at e1
      nlinarith [e1, norm_nonneg ((P * R) • x - (R * P * R) • x)]

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 Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖(P * Q) • x + (x - (P * Q) • x)‖ ≤ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖

Tactic:
by apply norm_add_le

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 Q R : { P // IsLprojection X P }
⊢ ↑P * ↑P + ↑P * (↑(Q ⊓ R) * ↑Pᶜ) + (↑Pᶜ * ↑R * ↑P + ↑Pᶜ * (↑R * ↑(Q ⊓ R) * ↑Pᶜ)) = ↑P + ↑(Q ⊓ R) * ↑Pᶜ

Tactic:
(Pᶜ.prop.commute R.prop).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 * ↑P + ↑P * (↑(Q ⊓ R) * ↑Pᶜ) + (↑R * ↑Pᶜ * ↑P + ↑Pᶜ * (↑R * ↑(Q ⊓ R) * ↑Pᶜ)) = ↑P + ↑(Q ⊓ R) * ↑Pᶜ
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

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

Tactic:
sub_le_sub_iff_right

Goal state after:
case insert
ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
A : ℝ
h : Real.exp (∑ i ∈ t, ‖f i‖) = A
IH : ‖∏ i ∈ t, (1 + f i) - 1‖ ≤ A - 1
⊢ A + ‖f x‖ * ‖∏ x ∈ t, (1 + f x)‖ ≤ Real.exp ‖f x‖ * A
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 * ↑Pᶜ

Tactic:
(Pᶜ.prop.commute R.prop).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 * (↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : 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 : ℝ≥0∞
e : (i : ι) → E i
f : (i : ι) → F i
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (i : ι), ‖e i‖ ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
⊢ ∑ i ∈ s, ‖((B i) (e i)) (f i)‖ ^ q.toReal ≤ (K * C) ^ q.toReal * D

Tactic:
grw [← hDf s, s.mul_sum]

Goal state after:
ι : 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 : ℝ≥0∞
e : (i : ι) → E i
f : (i : ι) → F i
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (i : ι), ‖e i‖ ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
⊢ ∑ i ∈ s, ‖((B i) (e i)) (f i)‖ ^ q.toReal ≤ ∑ i ∈ s, (K * C) ^ q.toReal * ‖f i‖ ^ q.toReal
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)
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
⊢ ‖(lift f.toMultilinearMap) x‖ ≤ ‖f‖ * injectiveSeminorm x

Tactic:
set G := (⨂[𝕜] i, E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)

Goal state after:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
G : Type (max (max uE u𝕜) uι) := (⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker
⊢ ‖(lift f.toMultilinearMap) x‖ ≤ ‖f‖ * injectiveSeminorm x
Module: Mathlib.Topology.Maps.Strict.Group

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
f : G →* H
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace H
⊢ IsStrictMap ⇑f ↔ IsEmbedding ⇑(kerLift f)

Tactic:
simp_rw [isEmbedding_iff_isStrictMap_injective, kerLift_injective, and_true,
    (isQuotientMap_mk _).isStrictMap_iff]

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
f : G →* H
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace H
⊢ IsStrictMap ⇑f ↔ IsStrictMap (⇑(kerLift f) ∘ QuotientGroup.mk)
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
u : E →L[𝕜] F
pkg : u.FredholmPackage
⊢ MapsTo ⇑u ↑pkg.decDom.X₁ ↑pkg.decCodom.X₁

Tactic:
simpa [← FredholmPackage.range_eq, LinearMap.coe_range] using Set.mapsTo_range _ _

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

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
⊢ y ∈ interior s

Tactic:
cases nonempty_fintype ι
  obtain ⟨ε, hε, hxy⟩ := Pi.exists_forall_pos_add_lt h
  obtain ⟨z, hz, hxz⟩ := Metric.mem_closure_iff.1 hx _ hε
  rw [dist_pi_lt_iff hε] at hxz
  have hyz : ∀ i, y i < z i := by
    refine fun i =>
      (lt_sub_iff_add_lt.2 <| hxy _).trans_le (sub_le_comm.1 <| (le_abs_self _).trans ?_)
    rw [← Real.norm_eq_abs, ← dist_eq_norm]
    exact (hxz _).le
  obtain ⟨δ, hδ, hyz⟩ := Pi.exists_forall_pos_add_lt hyz
  refine mem_interior.2 ⟨ball y δ, ?_, isOpen_ball, mem_ball_self hδ⟩
  rintro w hw
  refine hs (fun i => ?_) hz
  simp_rw [ball_pi _ hδ, Real.ball_eq_Ioo] at hw
  exact ((hw _ <| mem_univ _).2.trans <| hyz _).le

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

Goal state before:
pp: α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
⊢ Tendsto (fun n ↦ f^[n] x) atTop (𝓝 (fixedPoint f hf))

Tactic:
convert! tendsto_iterate_efixedPoint hf (edist_ne_top x _)

Goal state after:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
⊢ fixedPoint f hf = efixedPoint f hf x ⋯
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
this : dist (f^[n] x) (f^[n.succ] x) ≤ ↑K * dist x (f x)
⊢ IsFixedPt f x

Tactic:
iterate_succ_apply',

Goal state after:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
this : dist (f^[n] x) (f (f^[n] x)) ≤ ↑K * dist x (f x)
⊢ IsFixedPt f x
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
n : ℕ
t : ↑(Icc tmin tmax)
α β : FunSpace t₀ x₀ r L
h : dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
⊢ ↑K * dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    ↑K * (↑K ^ n * |↑t - ↑t₀| ^ n) / ↑n ! * dist α β

Tactic:
mul_div_assoc,

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
n : ℕ
t : ↑(Icc tmin tmax)
α β : FunSpace t₀ x₀ r L
h : dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
⊢ ↑K * dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    ↑K * (↑K ^ n * |↑t - ↑t₀| ^ n / ↑n !) * 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)
⊢ dist (((next hf hx)^[n + 1] α).toFun t) (((next hf hx)^[n + 1] β).toFun t) ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
iterate_succ_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)
⊢ dist ((next hf hx ((next hf hx)^[n] α)).toFun t) (((next hf hx)^[n + 1] β).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)
⊢ dist ((next hf hx ((next hf hx)^[n] α)).toFun t) (((next hf hx)^[n + 1] β).toFun t) ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
iterate_succ_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)
⊢ dist ((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 α β
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 : ℕ
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)
⊢ |↑K ^ (n + 1)| * |∫ (x : ℝ) in uIoc ↑t₀ ↑t, |x - ↑t₀| ^ n ∂volume| / |↑n !| * |dist α β| ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
integral_pow_abs_sub_uIoc,

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

Tactic:
apply le_trans <| hm.dist_iterate_succ_le_geometric α 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 i : ℕ
hi : i < n
⊢ dist α ((next hf hx)^[m] α) * ↑C ^ i ≤
    (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑C ^ i * dist α (next hf hx α)
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
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
n : ℕ
hf : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
⊢ ContDiffOn ℝ (↑n) (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
induction n with
    | zero =>
      simp only [Nat.cast_zero, contDiffOn_zero] at *
      exact HasDerivWithinAt.continuousOn this
    | succ n hn =>
      simp only [Nat.cast_add, Nat.cast_one] at *
      rw [contDiffOn_succ_iff_derivWithin <| uniqueDiffOn_Icc hlt]
      refine ⟨fun t ht ↦ HasDerivWithinAt.differentiableWithinAt (this t ht), by simp, ?_⟩
      apply contDiffOn_comp hf.of_succ (ContDiffOn.congr (hn hf.of_succ) heqon) hmem |>.congr
      intro t ht
      exact HasDerivWithinAt.derivWithin (this t ht) <| (uniqueDiffOn_Icc hlt).uniqueDiffWithinAt ht

Goal state after:
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 / (↑L + 1) * (↑a' - ↑r') ≤ 1 * (↑a' - ↑r')

Tactic:
by gcongr; rw [div_le_one (by positivity : (0 : ℝ) < L + 1)]; linarith

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inr
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
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
t : σ →₀ ℕ
hv : v ((coeff t) f + (coeff t) g) ≤ max (v ((coeff t) f)) (v ((coeff t) g))
h : max (v ((coeff t) f)) (v ((coeff t) g)) = v ((coeff t) g)
⊢ v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
    max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)

Tactic:
have : max (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i)
          (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) =
          (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) := by
        simp only [sup_eq_right]
        exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)
      simp_rw [this]
      exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RCLike 𝕜
⊢ Monotone rclikeToReal

Tactic:
by
  intro a b; simp_all [le_def, RCLike.le_iff_re_im (K := 𝕜)]

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

Goal state before:
pp: n : ℕ
⊢ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π

Tactic:
have : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π := by
    rw [← lt_div_iff₀, ← sin_pi_over_two_pow_succ]
    focus
      apply sin_lt
      apply div_pos pi_pos
    all_goals apply pow_pos; norm_num

Goal state after:
n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:

Tactic:
∑ x ∈ S.toFinset, count x S * ‖x.prod‖
    _ ≤ ∑ x ∈ S.toFinset, count x S * ((p.roots).map (fun a ↦ max 1 ‖a‖)).prod := by
      gcongr with x hx
      rw [Finset.prod_multiset_map_count, Finset.prod_multiset_count, norm_prod]
      simp_rw [norm_pow]
      exact this x hx
    _ = p.natDegree.choose n * (p.roots.map (fun a ↦ 1 ⊔ ‖a‖)).prod := by
      rw [← Finset.sum_mul]
      congr
      norm_cast
      simp only [mem_powersetCard, mem_toFinset, imp_self, implies_true, sum_count_eq_card,
        card_powersetCard, S, ← Nat.choose_symm hn]
      congr
      exact splits_iff_card_roots.mp <| IsAlgClosed.splits p

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

Goal state before:
pp: x : ℝ*
hx : Germ.Tendsto x atTop
⊢ ArchimedeanClass.mk x < 0

Tactic:
have : 0 < x := lt_of_tendsto_atTop 0 hx
  intro n
  simpa [abs_of_pos this] using! lt_of_tendsto_atTop n hx

Goal state after: