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

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) univ z
H : ∀ (z' : ℂ), ‖x - (algebraMap ℂ F) z'‖ ≠ 0
c : ℂ
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hMdef : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
y w : ℂ
hy : ‖x - (algebraMap ℂ F) y‖ = M
n : ℕ
hn : n > 0
⊢ ‖x - (algebraMap ℂ F) w‖ ≤ M * (1 + (‖x - (algebraMap ℂ F) w - (x - (algebraMap ℂ F) y)‖ / M) ^ n)

Tactic:
rw [sub_sub_sub_cancel_left, ← map_sub, norm_algebraMap, norm_sub_rev y w, norm_one, mul_one,
    show M * (1 + (‖w - y‖ / M) ^ n) = (M ^ n + ‖w - y‖ ^ n) / M ^ (n - 1) by
      simp only [field, div_pow, ← pow_succ', Nat.sub_add_cancel hn],
    le_div_iff₀ (by positivity)]

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) univ z
H : ∀ (z' : ℂ), ‖x - (algebraMap ℂ F) z'‖ ≠ 0
c : ℂ
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hMdef : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
y w : ℂ
hy : ‖x - (algebraMap ℂ F) y‖ = M
n : ℕ
hn : n > 0
⊢ ‖x - (algebraMap ℂ F) w‖ * M ^ (n - 1) ≤ M ^ n + ‖w - y‖ ^ n
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
⊢ Simplex.Scalene t ↔
    dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
      dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
        dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)

Tactic:
refine ⟨fun h ↦
    ⟨h.dist_ne (by decide : (0 : Fin 3) ≠ 1) (by decide : (0 : Fin 3) ≠ 2) (by decide) (by decide),
     h.dist_ne (by decide : (0 : Fin 3) ≠ 1) (by decide : (1 : Fin 3) ≠ 2) (by decide) (by decide),
     h.dist_ne (by decide : (0 : Fin 3) ≠ 2) (by decide : (1 : Fin 3) ≠ 2) (by decide) (by decide)⟩,
    fun ⟨h₁, h₂, h₃⟩ ↦ ?_⟩
  intro ⟨⟨x₁, x₂⟩, hx⟩ ⟨⟨y₁, y₂⟩, hy⟩ hxy
  simp only at hx hy hxy
  simp only [Subtype.mk.injEq, Prod.mk.injEq]
  fin_cases x₁ <;> fin_cases x₂ <;> simp +decide only at hx <;>
    fin_cases y₁ <;> fin_cases y₂ <;> simp +decide only at hy <;>
    simp [h₁, h₂, h₃, h₁.symm, h₂.symm, h₃.symm] at hxy ⊢

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: case refine_2
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a ↦ ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z ↦ ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ HasSum (fun k ↦ (expSeries ℝ ℍ (2 * k + 1)) fun x ↦ q) ((s / ‖q‖) • q)

Tactic:
· convert! hs using 1
    ext n : 1
    rw [expSeries_odd_of_imaginary hq]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : IsUnit x
hfx : f x ≠ 0
n : ℕ
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h1 : f 1 ≠ 0
hxn : f (x ^ n) = 0
this : f 1 ≤ 0
⊢ False

Tactic:
exact h1 <| this.antisymm (f_nonneg 1)

Goal state after:
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : AddLeftMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
⊢ liminf u f + liminf v f ≤ liminf (u + v) f

Tactic:
have h := isCoboundedUnder_ge_add h₂ h₄
  have h' := isBoundedUnder_ge_add h₁ h₃
  refine add_le_of_forall_lt fun a a_u b b_v ↦ ?_
  rw [le_liminf_iff h h']
  intro c c_ab
  filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x
  exact c_ab.trans (add_lt_add a_x b_x)

Goal state after:
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
have h := IsCoboundedUnder.of_frequently_ge (a := 0)
    <| (h₁.and_eventually h₃).mono fun x ⟨ux_0, vx_0⟩ ↦ mul_nonneg ux_0 vx_0

Goal state after:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ u x * v x
⊢ limsup u f * liminf v f ≤ limsup (u * v) f
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
have h := IsCoboundedUnder.of_frequently_ge (a := 0)
    <| (h₁.and_eventually h₃).mono fun x ⟨ux_0, vx_0⟩ ↦ mul_nonneg ux_0 vx_0

Goal state after:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ u x * v x
⊢ limsup (u * v) f ≤ limsup u f * limsup v f
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst✝ : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f (u * v)
h' : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) f fun x ↦ u x * v x
a : ℝ
a0 : a ≥ 0
au : a < liminf u f
⊢ ∀ b' ≥ 0, b' < liminf v f → a * b' ≤ liminf (u * v) f

Tactic:
b

Goal state after:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst✝ : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f (u * v)
h' : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) f fun x ↦ u x * v x
a : ℝ
a0 : a ≥ 0
au : a < liminf u f
b : ℝ
⊢ b ≥ 0 → b < liminf v f → a * b ≤ liminf (u * v) f
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: case h.h
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
c : ι × ι
left✝¹ : c ∈ univ
hc : (univ.sup' ⋯ fun i ↦ B.norm (B i.1 * B i.2)) = B.norm (B c.1 * B c.2)
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy_def : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x * y)) i‖) = ‖(B.repr (x * y)) ixy‖
⊢ ‖(∑ i, B.repr ((B.repr x) i • B i * ∑ i, (B.repr y) i • B i)) ixy‖ ≤ B.norm (B c.1 * B c.2) * B.norm x * B.norm y

Tactic:
simp_rw [smul_mul_assoc, map_smul, mul_sum, map_finsetSum, mul_smul_comm, map_smul]

Goal state after:
case h.h
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
c : ι × ι
left✝¹ : c ∈ univ
hc : (univ.sup' ⋯ fun i ↦ B.norm (B i.1 * B i.2)) = B.norm (B c.1 * B c.2)
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy_def : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x * y)) i‖) = ‖(B.repr (x * y)) ixy‖
⊢ ‖(∑ x_1, (B.repr x) x_1 • ∑ x, (B.repr y) x • B.repr (B x_1 * B x)) ixy‖ ≤
    B.norm (B c.1 * B c.2) * B.norm x * B.norm y
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
⊢ seminormFromBounded' f x = f x

Tactic:
simp_rw [seminormFromBounded', hx, ← mul_div_assoc']
  apply le_antisymm
  · refine ciSup_le (fun x ↦ ?_)
    by_cases hx : f x = 0
    · rw [hx, div_zero, mul_zero]; exact f_nonneg _
    · rw [div_self hx, mul_one]
  · by_cases! f_ne_zero : f ≠ 0
    · conv_lhs => rw [← mul_one (f x)]
      rw [← div_self (map_one_ne_zero f_ne_zero f_nonneg f_mul)]
      have h_bdd : BddAbove (Set.range fun y ↦ f x * (f y / f y)) := by
        use f x
        rintro r ⟨y, rfl⟩
        by_cases hy0 : f y = 0
        · simp only [hy0, div_zero, mul_zero]; exact f_nonneg _
        · simp only [div_self hy0, mul_one, le_refl]
      exact le_ciSup h_bdd (1 : R)
    · simp_rw [f_ne_zero, Pi.zero_apply, zero_div, zero_mul, ciSup_const]; rfl

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Completeness

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
u : ℕ → E
hu : Summable fun x ↦ ‖u x‖
⊢ ∃ a, Tendsto (fun n ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)

Tactic:
refine cauchySeq_tendsto_of_complete <| cauchySeq_of_summable_dist ?_

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
u : ℕ → E
hu : Summable fun x ↦ ‖u x‖
⊢ Summable fun n ↦ dist (∑ i ∈ range n, u i) (∑ i ∈ range n.succ, u i)
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
⊢ smoothingFun μ x ≤ μ x

Tactic:
by
  apply (smoothingFun_le μ x 1).trans
  rw [PNat.one_coe, pow_one, cast_one, div_one, rpow_one]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: case hom'
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
⊢ NormedAddGroupHom (cokernelCocone f).pt.carrier s.pt.carrier

pp: case normNoninc
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
⊢ NormedAddGroupHom.NormNoninc ?hom'

Tactic:
· apply NormedAddGroupHom.lift _ s.π.1
    rintro _ ⟨b, rfl⟩
    change (f ≫ s.π) b = 0
    simp

Goal state after:
case normNoninc
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
⊢ (NormedAddGroupHom.lift f.hom'.range (Cofork.π s).hom' ⋯).NormNoninc
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
n : ℕ
hn : 1 ≤ n
⊢ 1 / ↑n ≠ 0

Tactic:
exact one_div_ne_zero (cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn))

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : ↑{0}ᶜ
this : 0 < ‖↑x‖
⊢ ‖↑x‖ / r ∈ Ioi 0

Tactic:
rw [mem_Ioi]; positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set ↑(sphere 0 r)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x // x ∈ sphere 0 r }
hyV : y ∈ V
⊢ U • Subtype.val '' V ∈ 𝓝 ((fun x1 x2 ↦ x1 • x2) x ↑y)

Tactic:
wlog hx₀ : 0 < x generalizing x U

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set ↑(sphere 0 r)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x // x ∈ sphere 0 r }
hyV : y ∈ V
this : ∀ {U : Set ℝ}, IsOpen U → 0 ∉ U → ∀ x ∈ U, 0 < x → U • Subtype.val '' V ∈ 𝓝 ((fun x1 x2 ↦ x1 • x2) x ↑y)
hx₀ : ¬0 < x
⊢ U • Subtype.val '' V ∈ 𝓝 ((fun x1 x2 ↦ x1 • x2) x ↑y)

E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set ↑(sphere 0 r)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x // x ∈ sphere 0 r }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
x : ℝ
hxU : x ∈ U
hx₀ : 0 < x
⊢ U • Subtype.val '' V ∈ 𝓝 ((fun x1 x2 ↦ x1 • x2) x ↑y)
Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Goal state before:
pp: α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
R : Type u_3
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
inst✝¹ : CompleteSpace R
inst✝ : TopologicalSpace α
f : ι → α → R
hK : IsCompact K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
hKe : ¬K = ∅
hCK : CompactSpace ↑K
⊢ K.Nonempty

Tactic:
Set.nonempty_iff_ne_empty

Goal state after:
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
R : Type u_3
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
inst✝¹ : CompleteSpace R
inst✝ : TopologicalSpace α
f : ι → α → R
hK : IsCompact K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
hKe : ¬K = ∅
hCK : CompactSpace ↑K
⊢ K ≠ ∅
Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
R : Type u_3
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
inst✝¹ : CompleteSpace R
inst✝ : TopologicalSpace α
f : ι → α → R
hK : IsCompact K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
hKe : ¬K = ∅
hCK : CompactSpace ↑K
hne : Nonempty ↑K
f' : ι → C(↑K, R) := fun i ↦ { toFun := K.domRestrict (f i), continuous_toFun := ⋯ }
⊢ TendstoUniformly (fun i x ↦ ∏ i ∈ i, (1 + f i ↑x)) ((fun x ↦ ∏' (i : ι), (1 + f i x)) ∘ Subtype.val) atTop

Tactic:
have hf'_bd : ∀ᶠ i in cofinite, ‖f' i‖ ≤ u i := by
      simp only [ContinuousMap.norm_le_of_nonempty]
      filter_upwards [h] with i hi using fun x ↦ hi x x.2

Goal state after:
case neg
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
R : Type u_3
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
inst✝¹ : CompleteSpace R
inst✝ : TopologicalSpace α
f : ι → α → R
hK : IsCompact K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
hKe : ¬K = ∅
hCK : CompactSpace ↑K
hne : Nonempty ↑K
f' : ι → C(↑K, R) := fun i ↦ { toFun := K.domRestrict (f i), continuous_toFun := ⋯ }
hf'_bd : ∀ᶠ (i : ι) in cofinite, ‖f' i‖ ≤ u i
⊢ TendstoUniformly (fun i x ↦ ∏ i ∈ i, (1 + f i ↑x)) ((fun x ↦ ∏' (i : ι), (1 + f i x)) ∘ Subtype.val) atTop
Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
R : Type u_3
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
inst✝¹ : CompleteSpace R
inst✝ : TopologicalSpace α
f : ι → α → R
hK : IsCompact K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
hKe : ¬K = ∅
⊢ TendstoUniformly (fun i x ↦ ∏ i ∈ i, (1 + f i ↑x)) ((fun x ↦ ∏' (i : ι), (1 + f i x)) ∘ Subtype.val) atTop

Tactic:
have hCK : CompactSpace K := isCompact_iff_compactSpace.mp hK
    have hne : Nonempty K := by rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty]
    let f' i : C(K, R) := ⟨_, continuousOn_iff_continuous_domRestrict.mp (hcts i)⟩
    have hf'_bd : ∀ᶠ i in cofinite, ‖f' i‖ ≤ u i := by
      simp only [ContinuousMap.norm_le_of_nonempty]
      filter_upwards [h] with i hi using fun x ↦ hi x x.2
    have hM : Multipliable fun i ↦ 1 + f' i :=
      multipliable_one_add_of_summable (hu.of_norm_bounded_eventually (by simpa using hf'_bd))
    convert! ContinuousMap.tendsto_iff_tendstoUniformly.mp hM.hasProd
    · simp [f']
    · exact funext fun k ↦ ContinuousMap.tprod_apply hM k

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
α : FunSpace t₀ x₀ r L
t : ↑(Icc tmin tmax)
⊢ α.compProj ↑t = α.toFun t

Tactic:
by simp only [compProj_apply, projIcc_val]

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

Goal state before:
pp: case inl
p : ℂ[X]
this :
  ∑' (i : ℤ), ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑↑((ContinuousMap.toLp 2 haarAddCircle ℂ) (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
b : ℤ
hb : b ∉ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support
h : 0 ≤ b
⊢ ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ ^ 2 = 0

Tactic:
lift b to ℕ using h

Goal state after:
case inl
p : ℂ[X]
this :
  ∑' (i : ℤ), ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑↑((ContinuousMap.toLp 2 haarAddCircle ℂ) (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
b : ℕ
hb : ↑b ∉ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support
⊢ ‖if 0 ≤ ↑b then p.coeff (↑b).natAbs else 0‖ ^ 2 = 0
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree < Q.degree
hp : ¬P = 0
⊢ (fun x ↦ eval x P) =o[atTop] fun x ↦ eval x Q

Tactic:
· have hq : Q ≠ 0 := ne_zero_of_degree_ge_degree h.le hp
    have hPQ : ∀ᶠ x in atTop, Q.eval x = 0 → P.eval x = 0 :=
      mem_of_superset (eventually_atTop_not_isRoot Q hq) fun x h h' ↦ absurd h' h
    exact isLittleO_of_tendsto' hPQ (div_tendsto_atTop_zero_of_degree_lt P Q h)

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

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
hP : ¬P = 0
⊢ (fun x ↦ eval x P) =o[cobounded R] fun x ↦ eval x Q

Tactic:
refine isEquivalent_cobounded_leading_monomial.trans_isLittleO <|
      ((IsLittleO.const_mul_right ?_ ?_).const_mul_left _).trans_isEquivalent
        isEquivalent_cobounded_leading_monomial.symm
    · exact leadingCoeff_ne_zero.mpr (ne_zero_of_degree_gt h)
    · exact isLittleO_pow_pow_cobounded_of_lt (natDegree_lt_natDegree hP h)

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RCLike 𝕜
a : C(X, 𝕜)
⊢ ∀ ⦃b : C(X, 𝕜)⦄, a ≤ b → a.rclikeToReal ≤ b.rclikeToReal

Tactic:
b

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RCLike 𝕜
a b : C(X, 𝕜)
⊢ a ≤ b → a.rclikeToReal ≤ b.rclikeToReal
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
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‖
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)

Tactic:
have hcont : Continuous (fun x : ℝ ↦ ‖eval (circleMap 0 1 x) p‖) := by fun_prop

Goal state after:
case neg
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‖
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
this : b ≠ 0
⊢ ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊

Tactic:
induction n with
  | zero => simp [Nat.floor_eq_zero.mpr hx.right]
  | succ n ih =>
    rw [Finset.sum_range_succ, mul_add, pow_succ', mul_assoc, ih, ofDigitsTerm, digits, ← pow_succ',
      mul_left_comm, mul_inv_cancel₀ (by positivity), mul_one, mul_comm x, pow_succ', mul_assoc]
    set y := (b : ℝ) ^ n * x
    norm_cast
    rw [← Nat.cast_mul_floor_div_cancel (a := y) (show b ≠ 0 by lia),
      Fin.val_ofNat, Nat.div_add_mod]

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

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

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

Tactic:
· exact hasSum_ofDigitsTerm_digits x hb hx

Goal state after:
b : ℕ
inst✝ : NeZero b
x : ℝ
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ Summable (ofDigitsTerm (x.digits b))
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
by rwa [Rat.cast_intCast]

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
by rwa [Rat.cast_intCast]

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

Goal state before:
pp: x : ℝ*
⊢ x.InfiniteNeg ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0

Tactic:
by
  rw [← infinitePos_neg, infinitePos_iff_infinitesimal_inv_pos, inv_neg, neg_pos, infinitesimal_neg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
z₁ : 1 + z * I ≠ 0
h₂ : 1 - z * I = 0
⊢ z = -I

Tactic:
rw [sub_eq_zero, ← div_eq_iff I_ne_zero, div_I, one_mul] at h₂

Goal state after:
z : ℂ
h₁ : z ≠ I
z₁ : 1 + z * I ≠ 0
h₂ : -I = z
⊢ z = -I
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

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

Tactic:
cosh_arcosh hx

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

Goal state before:
pp: x y : ℝ≥0
⊢ sqrt (x * y) ≤ (x + y) / 2

Tactic:
rw [sqrt_le_iff_le_sq, div_pow, le_div_iff₀' (by positivity), ← mul_assoc]
  norm_num
  exact four_mul_le_sq_add ..

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

Goal state before:
pp: 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
c a : A
⊢ ∀ ⦃b : A⦄, a ≤ b → (conjSqrt c) a ≤ (conjSqrt c) b

Tactic:
b

Goal state after:
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
c a b : A
⊢ a ≤ b → (conjSqrt c) a ≤ (conjSqrt c) b
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Icc 0 1
a : A
⊢ ∀ ⦃b : A⦄, a ≤ b → (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b

Tactic:
b

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Icc 0 1
a b : A
⊢ a ≤ b → (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ ∀ ⦃b : A⦄, a ≤ b → sqrt a ≤ sqrt b

Tactic:
b

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
⊢ a ≤ b → sqrt a ≤ sqrt b