mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3

Tactic:
calc _ ≤ ‖∑' (k : (Tᶜ : Set β)), bound k‖ := Real.le_norm_self _
         _ = ‖S - ∑ b ∈ T, bound b‖           := congrArg _ ?_
         _ < ε / 3                            := by rwa [dist_eq_norm, norm_sub_rev] at hT

Goal state after:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
⊢ ∑' (k : ↑(↑T)ᶜ), bound ↑k = S - ∑ b ∈ T, bound b
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
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
x✝ : L
k : K
x : L
⊢ (MulRingNorm.mulRingNormEquivAbsoluteValue.invFun f).toMulRingSeminorm ((algebraMap K L) k * x) =
    ‖k‖ * (MulRingNorm.mulRingNormEquivAbsoluteValue.invFun f).toMulRingSeminorm x

Tactic:
map_mul

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
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
x✝ : L
k : K
x : L
⊢ (MulRingNorm.mulRingNormEquivAbsoluteValue.invFun f).toMulRingSeminorm ((algebraMap K L) k) *
      (MulRingNorm.mulRingNormEquivAbsoluteValue.invFun f).toMulRingSeminorm x =
    ‖k‖ * (MulRingNorm.mulRingNormEquivAbsoluteValue.invFun f).toMulRingSeminorm x
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
x : ⨂[𝕜] (i : ι), E i
f : ContinuousMultilinearMap 𝕜 E F
⊢ ‖((↑lift).flip x ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear) f‖ ≤ ‖x‖ * ‖f‖

Tactic:
simpa [mul_comm] using norm_eval_le_projectiveSeminorm f x

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

Goal state before:
pp: case inr.inl
ι : 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)
r : ℝ≥0∞
inst✝² : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝¹ : Fact (1 ≤ ∞)
f : ↥(lp F ∞)
inst✝ : Fact (1 ≤ r)
e : ↥(lp E r)
hp : 1 ≤ r.toReal
hpqr : r.HolderTriple ∞ r
s : Finset ι
⊢ ∑ i ∈ s, ‖↑(((holderₗ r B hBK) e) f) i‖ ^ r.toReal ≤ (↑K * ‖f‖) ^ r.toReal * ‖e‖ ^ r.toReal

Tactic:
refine Memℓp.holder_top_right_bound B hBK
        (by positivity) (by positivity) ?_ (norm_apply_le_norm (by simp) _) s

Goal state after:
case inr.inl
ι : 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)
r : ℝ≥0∞
inst✝² : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝¹ : Fact (1 ≤ ∞)
f : ↥(lp F ∞)
inst✝ : Fact (1 ≤ r)
e : ↥(lp E r)
hp : 1 ≤ r.toReal
hpqr : r.HolderTriple ∞ r
s : Finset ι
⊢ ∀ (s : Finset ι), ∑ i ∈ s, ‖↑e i‖ ^ r.toReal ≤ ‖e‖ ^ r.toReal
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
inst✝¹ : T2Space E
inst✝ : T2Space F
u : E →L[𝕜] F
v : F →L[𝕜] E
hvu : (LinearMap.id.eqLocus (↑v ∘ₗ ↑u)).CoFG
huv : (LinearMap.id.eqLocus (↑u ∘ₗ ↑v)).CoFG
E₁ : Submodule 𝕜 E := (↑(ContinuousLinearMap.id 𝕜 E)).eqLocus ↑(v ∘SL u)
F₁ : Submodule 𝕜 F := (↑(ContinuousLinearMap.id 𝕜 F)).eqLocus ↑(u ∘SL v)
⊢ ∃ E₁ F₁,
    IsClosed[inst✝³] ↑E₁ ∧
      IsClosed[inst✝²] ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible

Tactic:
have u_mapsto : MapsTo u E₁ F₁ := fun x hx ↦ congr(u $hx)

Goal state after:
𝕜 : 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
inst✝¹ : T2Space E
inst✝ : T2Space F
u : E →L[𝕜] F
v : F →L[𝕜] E
hvu : (LinearMap.id.eqLocus (↑v ∘ₗ ↑u)).CoFG
huv : (LinearMap.id.eqLocus (↑u ∘ₗ ↑v)).CoFG
E₁ : Submodule 𝕜 E := (↑(ContinuousLinearMap.id 𝕜 E)).eqLocus ↑(v ∘SL u)
F₁ : Submodule 𝕜 F := (↑(ContinuousLinearMap.id 𝕜 F)).eqLocus ↑(u ∘SL v)
u_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
⊢ ∃ E₁ F₁,
    IsClosed[inst✝³] ↑E₁ ∧
      IsClosed[inst✝²] ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : NormedCommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (thickening ε s)

Tactic:
← ball_mul_one

Goal state after:
α : Type u_1
inst✝² : NormedCommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (ball 1 ε * s)
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : NormedCommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (thickening ε s)

Tactic:
← ball_mul_one

Goal state after:
α : Type u_1
inst✝² : NormedCommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (ball 1 ε * s)
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
⊢ ∑ i ∈ Ico n₀ k, c k * (b i * ∏ i ∈ Ico (i + 1) k, c i) + b k =
    ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) (k + 1), c i + b k * ∏ i ∈ Ico (k + 1) (k + 1), c i

Tactic:
Ico_self,

Goal state after:
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
⊢ ∑ i ∈ Ico n₀ k, c k * (b i * ∏ i ∈ Ico (i + 1) k, c i) + b k =
    ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) (k + 1), c i + b k * ∏ i ∈ ∅, c i
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
h : ∀ (t : ↑(Icc tmin tmax)), α.toFun t = β.toFun t
⊢ α = β

Tactic:
cases α; cases β; simp only [mk.injEq]; ext t; exact h t

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
⊢ EqOn f g (Icc a b)

Tactic:
suffices EqOn (f ∘ Neg.neg) (g ∘ Neg.neg) (Icc (-b) (-a)) by
    rw [eqOn_comp_right_iff] at this
    convert this
    simp

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
⊢ EqOn (f ∘ Neg.neg) (g ∘ Neg.neg) (Icc (-b) (-a))
Module: Mathlib.Analysis.Polynomial.Fourier

Goal state before:
pp: n : ℕ
⊢ toAddCircle (X ^ n) = fourier ↑n

Tactic:
ext θ; simp [toAddCircle, AddCircle.toCircle_nsmul]

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

Goal state before:
pp: n : ℕ
c : ℂ
⊢ toAddCircle ((monomial n) c) = c • fourier ↑n

Tactic:
ext θ; simp [toAddCircle, AddCircle.toCircle_nsmul]

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

Goal state before:
pp: case monomial.inl
p : ℂ[X]
n : ℤ
m : ℕ
a : ℂ
hn : n < 0
⊢ fourierCoeff (⇑(toAddCircle ((monomial m) a))) n = if 0 ≤ n then ((monomial m) a).coeff n.natAbs else 0

Tactic:
simp_all [not_le_of_gt, coeff_monomial, toAddCircle_monomial_eq_smul_fourier,
      fourierCoeff.const_smul, fourierCoeff_fourier, Pi.single_apply]
    grind

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

Goal state before:
pp: case monomial.inr
p : ℂ[X]
m : ℕ
a : ℂ
k : ℕ
⊢ fourierCoeff ⇑(toAddCircle ((monomial m) a)) ↑k = if 0 ≤ ↑k then ((monomial m) a).coeff (↑k).natAbs else 0

Tactic:
simp_all [not_le_of_gt, coeff_monomial, toAddCircle_monomial_eq_smul_fourier,
      fourierCoeff.const_smul, fourierCoeff_fourier, Pi.single_apply]
    grind

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.degree = Q.degree
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))

Tactic:
refine (isEquivalent_atTop_div P Q).symm.tendsto_nhds ?_
  rw [show (P.natDegree : ℤ) = Q.natDegree by simp [hdeg, natDegree]]
  simp

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
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' : ℝ := ⋯
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) β
⊢ Filter.Tendsto
    (fun x ↦ (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ∑ i ∈ Finset.range x, ↑C ^ i)
    Filter.atTop (𝓝 L')

Tactic:
apply Filter.Tendsto.const_mul

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' : ℝ := ⋯
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) β
⊢ Filter.Tendsto (fun x ↦ ∑ i ∈ Finset.range x, ↑C ^ i) Filter.atTop (𝓝 ↑(1 - C)⁻¹)
Module: Mathlib.Analysis.Polynomial.Norm

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedRing A
p : A[X]
⊢ 0 ≤ p.supNorm

Tactic:
apply gaussNorm_nonneg
  norm_num

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

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedRing A
p : A[X]
i : ℕ
⊢ ‖p.coeff i‖ ≤ p.supNorm

Tactic:
simpa using! le_gaussNorm (SeminormedRing.toRingSeminorm A) p (by norm_num : (0 : ℝ) ≤ 1) i

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

Goal state before:
pp: case inr
R : Type u_1
F : Type u_2
inst✝⁴ : Semiring R
inst✝³ : FunLike F R ℝ
v : F
c : ℝ
inst✝² : ZeroHomClass F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
h_supp_p : p.support.Nonempty
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q

Tactic:
have h_supp_q : q.support.Nonempty := support_nonempty.mpr <| right_ne_zero_of_mul hpq

Goal state after:
case inr
R : Type u_1
F : Type u_2
inst✝⁴ : Semiring R
inst✝³ : FunLike F R ℝ
v : F
c : ℝ
inst✝² : ZeroHomClass F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝ : v (p.coeff i) ≠ 0
this : v (q.coeff j) ≠ 0
⊢ gaussNorm v c p * gaussNorm v c q = v ((p * q).coeff (i + j)) * c ^ (i + j)

Tactic:
rw [hi_p, hj_q, coeff_mul, Nat.sum_antidiagonal_eq_sum_range_succ_mk,
    IsNonarchimedean.apply_sum_eq_of_lt hna (k := i) (by simp) (by simp)]

Goal state after:
c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝ : v (p.coeff i) ≠ 0
this : v (q.coeff j) ≠ 0
⊢ v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j) =
    v (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) * c ^ (i + j)

c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝ : v (p.coeff i) ≠ 0
this : v (q.coeff j) ≠ 0
⊢ ∀ j_1 ∈ range (i + j).succ,
    j_1 ≠ i →
      v (p.coeff (j_1, i + j - j_1).1 * q.coeff (j_1, i + j - j_1).2) <
        v (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2)
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case refine_1
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)
⊢ (v ((coeff t) (f * g)) * t.prod fun x1 x2 ↦ c x1 ^ x2) ≤ gaussNorm v c f * gaussNorm v c g

Tactic:
have hk' : k.1 + k.2 = t := by
      simpa [Finset.mem_antidiagonal] using hk (Finset.nonempty_def.mpr ⟨(t, 0), by simp⟩)

Goal state after:
case refine_1
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
⊢ (v ((coeff t) (f * g)) * t.prod fun x1 x2 ↦ c x1 ^ x2) ≤ gaussNorm v c f * gaussNorm v c g
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
h : Even P.natDegree
hlc' : 0 ≤ (P.comp (-X)).leadingCoeff
⊢ 0 < eval x P

Tactic:
have := zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg hroots' 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 ≤ (P.comp (-X)).leadingCoeff
this : 0 < eval (-x) (P.comp (-X))
⊢ 0 < eval x P
Module: Mathlib.Analysis.Polynomial.Order

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

Tactic:
mul_zero

Goal state after:
case pos
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : 0 ≤ P.leadingCoeff
y : ℝ
hroot : P.IsRoot y
hle : y ≤ x
⊢ 0 ≤ 0
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: z : ℂ
this : rexp (log (X - C z).mahlerMeasure) = rexp (log (max 1 ‖z‖))
⊢ (X - C z).mahlerMeasure = max 1 ‖z‖

Tactic:
exp_log (mahlerMeasure_pos_of_ne_zero <| X_sub_C_ne_zero z),

Goal state after:
z : ℂ
this : (X - C z).mahlerMeasure = rexp (log (max 1 ‖z‖))
⊢ (X - C z).mahlerMeasure = max 1 ‖z‖
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
digits : ℕ → Fin b
⊢ Summable (ofDigitsTerm digits)

Tactic:
refine Summable.of_nonneg_of_le (fun _ ↦ ofDigitsTerm_nonneg) (fun _ ↦ ofDigitsTerm_le) ?_

Goal state after:
b : ℕ
digits : ℕ → Fin b
⊢ Summable fun x ↦ (↑b - 1) * (↑b ^ (x + 1))⁻¹
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
⊢ x - (↑b)⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i

Tactic:
have := NeZero.pos b
  have := ofDigits_digits_sum_eq (b := b) hx n
  have h_le := Nat.lt_floor_add_one (b ^ n * x)
  rw [← this] at h_le
  rw [← mul_le_mul_iff_right₀ (show 0 < (b : ℝ) ^ n by positivity),
    mul_sub, inv_pow, mul_inv_cancel₀ (by positivity)]
  linarith

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

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

Tactic:
rw [hasSum_iff_tendsto_nat_of_summable_norm (by exact summable_ofDigitsTerm.abs)]

Goal state after:
x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ Filter.Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i) Filter.atTop (nhds x)
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r : ℝ
⊢ ↑r < ω

Tactic:
apply ofSeq_lt_ofSeq.2 <| Filter.Eventually.filter_mono Nat.hyperfilter_le_atTop _
  obtain ⟨n, hn⟩ := exists_nat_gt r
  rw [eventually_atTop]
  exact ⟨n, fun m hm ↦ hn.trans_le (mod_cast hm)⟩

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

Goal state before:
pp: case refine_1
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2
s : ℝ
hs : s < r
⊢ ↑s ≤ ofSeq f

pp: case refine_2
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2
s : ℝ
hs : s > r
⊢ ofSeq f ≤ ↑s

pp: case refine_3
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ (ofSeq fun n ↦ (s, t).1) < ofSeq f

pp: case refine_4
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ ofSeq f < ofSeq fun n ↦ (s, t).2

Tactic:
· obtain ⟨t, ht⟩ := exists_gt r
    exact (H ⟨s, t⟩ ⟨hs, ht⟩).1.le

Goal state after:
case refine_2
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2
s : ℝ
hs : s > r
⊢ ofSeq f ≤ ↑s

case refine_3
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ (ofSeq fun n ↦ (s, t).1) < ofSeq f

case refine_4
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ ofSeq f < ofSeq fun n ↦ (s, t).2
Module: Mathlib.Data.Rat.Sqrt

Goal state before:
pp: q : ℚ
⊢ mkRat (Int.sqrt (q.num * q.num)) (q.den * q.den).sqrt = |q|

Tactic:
Int.sqrt_eq,

Goal state after:
q : ℚ
⊢ mkRat (↑q.num.natAbs) (q.den * q.den).sqrt = |q|
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
⊢ ∑ n ∈ p.support, ‖(map v p).coeff n‖ = ∑ n ∈ p.support, ‖p.coeff n‖

Tactic:
exact Finset.sum_congr rfl fun x _ ↦ by
    simp [hv.norm_map_of_map_zero (map_zero _)]

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

Goal state before:
pp: case inl
x : ℝ
hx : Irrational x
p_nonzero : C 0 * X + C 0 ≠ 0
x_is_root : (aeval x) (C 0 * X + C 0) = 0
this : ↑0 * x = -↑0
⊢ False

Tactic:
simp at p_nonzero

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

Goal state before:
pp: case inr
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hp : 0 < x
⊢ x.Infinite

Tactic:
exact Or.inl (infinitePos_iff_infinitesimal_inv_pos.mpr ⟨hi, inv_pos.mpr hp⟩)

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

Goal state before:
pp: case succ
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1)) *
      ((2 * ↑n + 2) * (2 * ↑n + 2) / ((2 * ↑n + 1) * (2 * ↑n + 3))) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 / (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1))

Tactic:
_root_.div_mul_div_comm

Goal state after:
case succ
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * ↑n ! ^ 4 * ((2 * ↑n + 2) * (2 * ↑n + 2)) /
      (↑(2 * n)! ^ 2 * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3))) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 / (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1))