mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
α : Type u_4
l : Filter α
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ (asymptoticNhds k P v).NeBot

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
α : Type u_4
l : Filter α
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
p : P
⊢ (asymptoticNhds k P v).NeBot
Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
p : P
t : V → Set ℝ
ht : ∀ i ∈ Metric.sphere 0 1, t i ∈ atTop
u : V → Set V
hu : ∀ i ∈ Metric.sphere 0 1, u i ∈ 𝓝 i
smul_subset_s : ∀ i ∈ Metric.sphere 0 1, t i • u i ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, x ∈ Metric.sphere 0 1
h₂ : Metric.sphere 0 1 ⊆ ⋃ x ∈ cover, u x
⊢ s ∈ cobounded P

Tactic:
← Metric.comap_dist_left_atTop p

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
p : P
t : V → Set ℝ
ht : ∀ i ∈ Metric.sphere 0 1, t i ∈ atTop
u : V → Set V
hu : ∀ i ∈ Metric.sphere 0 1, u i ∈ 𝓝 i
smul_subset_s : ∀ i ∈ Metric.sphere 0 1, t i • u i ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, x ∈ Metric.sphere 0 1
h₂ : Metric.sphere 0 1 ⊆ ⋃ x ∈ cover, u x
⊢ s ∈ comap (dist p) atTop
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case succ.refine_2.e_a.e_a.e_f
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ / u
j : ℕ
⊢ u + 1 + ↑j = u + (↑j + 1)

Tactic:
abel

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s : ℝ
hs : 0 < s
⊢ 1 - 2 * s = -(2 * s - 1)

Tactic:
abel

Goal state after:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
⊢ asymptoticNhds k P 0 = ⊤

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
p : P
⊢ asymptoticNhds k P 0 = ⊤
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
c : k
hc : 0 < c
⊢ asymptoticNhds k P (c • v) = asymptoticNhds k P v

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
c : k
hc : 0 < c
p : P
⊢ asymptoticNhds k P (c • v) = asymptoticNhds k P v
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ (𝓝 v).bind (asymptoticNhds k P) ≤ asymptoticNhds k P v

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance

Goal state after:
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
p : P
⊢ (𝓝 v).bind (asymptoticNhds k P) ≤ asymptoticNhds k P v
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ s + 1 + ↑n = ↑n + 1 + s

Tactic:
abel

Goal state after:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹² : Field k
inst✝¹¹ : LinearOrder k
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module k V
inst✝⁸ : AddTorsor V P
inst✝⁷ : TopologicalSpace V
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : IsStrictOrderedRing k
inst✝³ : IsTopologicalAddGroup V
inst✝² : ContinuousSMul k V
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalAddTorsor P
v : V
s : Set P
h : s ∈ asymptoticNhds k P v
⊢ s ∈ (asymptoticNhds k P v).bind 𝓝

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹² : Field k
inst✝¹¹ : LinearOrder k
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module k V
inst✝⁸ : AddTorsor V P
inst✝⁷ : TopologicalSpace V
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : IsStrictOrderedRing k
inst✝³ : IsTopologicalAddGroup V
inst✝² : ContinuousSMul k V
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalAddTorsor P
v : V
s : Set P
h : s ∈ asymptoticNhds k P v
p : P
⊢ s ∈ (asymptoticNhds k P v).bind 𝓝
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
⊢ IsClosed[inst✝⁵] (asymptoticCone k s)

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
p : P
⊢ IsClosed[inst✝⁵] (asymptoticCone k s)
Module: Mathlib.Analysis.Normed.Affine.MazurUlam

Goal state before:
pp: E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}
this : Nonempty ↑s
e : PE ≃ᵢ PE
hx : e x = x
right✝ : e y = y
⊢ dist (e x) (e z) + dist x z = dist x z + dist x z

Tactic:
rw [e.dist_eq x z]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : ↑s → Finset ι
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
fsx : ↑s → Finset ι := fun i ↦ insert (↑i) (fs i)
hfsx : ∀ (i : ↑s), ↑i ∈ fsx i
wx : ↑s → ι → k := fun i ↦ (↑(fs i)).indicator (w i)
hwx : ∀ (i : ↑s), ∑ j ∈ fsx i, wx i j = 1
i : ↑s
⊢ p' ∈ line[k, p ↑i, (Finset.affineCombination k (fsx i) p) (wx i)]

Tactic:
convert! hp' i using 4

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : ↑s → Finset ι
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
fsx : ↑s → Finset ι := fun i ↦ insert (↑i) (fs i)
hfsx : ∀ (i : ↑s), ↑i ∈ fsx i
wx : ↑s → ι → k := fun i ↦ (↑(fs i)).indicator (w i)
hwx : ∀ (i : ↑s), ∑ j ∈ fsx i, wx i j = 1
i : ↑s
⊢ (Finset.affineCombination k (fsx i) p) (wx i) = (Finset.affineCombination k (fs i) p) (w i)
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : CommRing k
inst✝³ : NoZeroDivisors k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h✝ : Nontrivial k
w : ↑Set.univ → Fin 3 → k := fun i ↦ Finset.affineCombinationLineMapWeights (↑i + 1) (↑i + 2) (r ↑i)
hw : ∀ (i : ↑Set.univ), ∑ j, w i j = 1
w' : Fin (2 + 1) → k
hw' : ∑ j, w' j = 1
h : ∀ (i : ↑Set.univ), ∃ r, ∀ (j : Fin (2 + 1)), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j
hp' :
  ∀ (i : Fin 3),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
hp'w :
  ∀ (i : ↑Set.univ),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points ↑i, (Finset.affineCombination k Finset.univ t.points) (w i)]
h' :
  ∀ (i : Fin 3), ∃ c, ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k := fun i ↦ ⋯.choose
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
hcr : (∏ i, c i) * ∏ i, r i = (∏ i, c i) * ∏ i, (1 - r i)
i : Fin 3
hi : c i = 0
hw'i1 : w' (i + 1) = 0
⊢ ∏ i, r i = ∏ i, (1 - r i)

Tactic:
have hw'i2 : w' (i + 2) = 0 := by simpa [hi] using (hc2 i).symm

Goal state after:
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : CommRing k
inst✝³ : NoZeroDivisors k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h✝ : Nontrivial k
w : ↑Set.univ → Fin 3 → k := fun i ↦ Finset.affineCombinationLineMapWeights (↑i + 1) (↑i + 2) (r ↑i)
hw : ∀ (i : ↑Set.univ), ∑ j, w i j = 1
w' : Fin (2 + 1) → k
hw' : ∑ j, w' j = 1
h : ∀ (i : ↑Set.univ), ∃ r, ∀ (j : Fin (2 + 1)), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j
hp' :
  ∀ (i : Fin 3),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
hp'w :
  ∀ (i : ↑Set.univ),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points ↑i, (Finset.affineCombination k Finset.univ t.points) (w i)]
h' :
  ∀ (i : Fin 3), ∃ c, ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k := fun i ↦ ⋯.choose
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
hcr : (∏ i, c i) * ∏ i, r i = (∏ i, c i) * ∏ i, (1 - r i)
i : Fin 3
hi : c i = 0
hw'i1 : w' (i + 1) = 0
hw'i2 : w' (i + 2) = 0
⊢ ∏ i, r i = ∏ i, (1 - r i)
Module: Mathlib.Analysis.Normed.Ring.Ultra

Goal state before:
pp: case succ
R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
n : ℕ
hn : ‖↑n‖₊ ≤ 1
⊢ ‖↑(n + 1)‖₊ ≤ 1

Tactic:
| succ n hn =>

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

Goal state before:
pp: case ha
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ 1 ≤ ‖x‖

Tactic:
contrapose! hx

Goal state after:
case ha
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
hx : ‖x‖ < 1
⊢ ‖x‖ ^ m ≤ 1
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case refine_2
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
⊢ Tendsto (fun y ↦ ‖y.1‖) (cobounded ℝ ×ˢ ⊤) atTop

Tactic:
tendsto_norm_atTop_iff_cobounded

Goal state after:
case refine_2
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
⊢ Tendsto Prod.fst (cobounded ℝ ×ˢ ⊤) (cobounded ℝ)
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : ¬x * y = 0
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y

Tactic:
change ite _ _ _ ≤ ite _ _ _ * ite _ _ _

Goal state after:
case neg
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : ¬x * y = 0
⊢ (if x * y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) * if y = 0 then 0 else 1
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f ((algebraMap R S) a) = ‖a‖

Tactic:
Algebra.algebraMap_eq_smul_one

Goal state after:
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ f ((algebraMap R S) a) = ‖a‖

Tactic:
Algebra.algebraMap_eq_smul_one

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ f (a • 1) = ‖a‖
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case neg
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
h1 : ¬f 1 = 0
⊢ f x / f 1 ≤ seminormFromBounded' f x

Tactic:
conv_lhs => rw [← mul_one x]

Goal state after:
case neg
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
h1 : ¬f 1 = 0
⊢ f (x * 1) / f 1 ≤ seminormFromBounded' f x
Module: Mathlib.Analysis.Normed.Field.Approximation

Goal state before:
pp: K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ ∃ b ∈ g.roots, ‖a - b‖ < ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1

Tactic:
by
  -- Let `a` be a root of `f`. To show there exists a root `b` of `g` such that `‖a - b‖` is small,
  -- it suffices to show that `∏ (b ∈ g.roots) ‖a - b‖` is small.
  suffices this : (g.roots.map fun x => ‖a - x‖).prod <
      ((f.natDegree + 1) * ε) * (max ‖a‖ 1) ^ (f.natDegree : ℝ) by
    by_contra! h
    have := Multiset.prod_map_le_prod_map₀ (fun b ↦ ((f.natDegree + 1) * ε) ^ (f.natDegree : ℝ)⁻¹ *
        (‖a‖ ⊔ 1)) (fun b ↦ ‖a - b‖) (by intros; positivity) h
    simp only [Multiset.map_const', hg.natDegree_eq_card_roots.symm ▸ hdeg, Multiset.prod_replicate,
      mul_pow, ← Real.rpow_natCast,
      ← Real.rpow_mul (by positivity : ((f.natDegree + 1) * ε) > 0).le] at this
    rw [inv_mul_cancel₀, Real.rpow_one] at this
    · linarith
    · simp only [ne_eq, Nat.cast_eq_zero, hfm, Monic.natDegree_eq_zero]
      intro h
      simp [h] at ha
  -- `∏ (b ∈ g.roots) ‖a - b‖ = ‖g(a)‖ = ‖(g - f)(a)‖` is small since every
  -- coefficient of `‖g - f‖` is small.
  calc
  _ = (g.roots.map (fun x ↦ NormedField.toMulRingNorm K (a - x))).prod := rfl
  _ = ‖(g.roots.map (fun x ↦ a - x)).prod‖ := by
    rw [g.roots.prod_hom' (NormedField.toMulRingNorm K) (fun x : K ↦ a - x)]
    rfl
  _ = ‖g.eval a‖ := by
    congr
    rw [hg.eval_eq_prod_roots_of_monic hgm]
  _ ≤ ‖g.eval a - f.eval a‖ + ‖f.eval a‖ := by
    convert! norm_add_le (g.eval a - f.eval a) (f.eval a)
    simp
  _ = ‖(∑ i ∈ Finset.range (g.natDegree + 1), C (g.coeff i - f.coeff i) * X ^ i).eval a‖ := by
    rw [← eval_sub]
    simp only [ha, norm_zero, add_zero]
    rw [(g - f).as_sum_range' (g.natDegree + 1)]
    · congr
      simp [← C_mul_X_pow_eq_monomial]
    · simpa [hdeg, Nat.lt_succ_iff] using g.natDegree_sub_le f
  _ ≤ ∑ i ∈ Finset.range (g.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖ := by
    have := norm_sum_le (Finset.range (g.natDegree + 1))
        (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
    simpa [eval_mul, eval_finsetSum] using this
    -- The following tactic does not work here:
    -- simpa [eval_mul, eval_finsetSum] using norm_sum_le (Finset.range (g.natDegree + 1))
    --     (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
  _ < _ := by
    rw [hdeg]
    convert!
      Finset.sum_lt_sum_of_nonempty (g := fun i ↦ ε * (‖a‖ ⊔ 1) ^ ↑f.natDegree)
        (Finset.nonempty_range_add_one) ?_
    · simp [mul_assoc]
    · simp only [Finset.mem_range, norm_mul, norm_pow]
      intro i hi
      apply mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
      · simpa [← map_sub] using hcoeff i
      · refine (pow_le_pow_left₀ (norm_nonneg a) (le_max_left ‖a‖ 1) i).trans ?_
        exact pow_le_pow_right₀ (le_max_right ‖a‖ 1) (Nat.le_of_lt_succ hi)
      all_goals positivity

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

Goal state before:
pp: case neg
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
x : R
hx : ¬f x = 0
⊢ f x✝ * (f x / f x) ≤ f x✝

Tactic:
· rw [div_self hx, mul_one]

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
B : Basis ι K L := Basis.extend h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B
hem : Nonempty ι
h1L : 1 ∈ h1.extend ⋯
⊢ B ⟨1, h1L⟩ = 1

Tactic:
rw [Basis.coe_extend, Subtype.coe_mk]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
m n : ℕ
hmn : m ≤ n
hc_pos : 0 < f c
heq : m = n
⊢ f (x * c ^ m) * f (c ^ (n - m)) / f c ^ n ≤ f (x * c ^ m) / f c ^ m

Tactic:
have hnm : n - m = 0 := by rw [heq, Nat.sub_self n]
    rw [hnm, heq, div_le_div_iff_of_pos_right (pow_pos hc_pos _), pow_zero]
    conv_rhs => rw [← mul_one (f (x * c ^ n))]
    gcongr

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

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

Tactic:
isConjRoot_iff_mem_minpoly_rootSet (xsep.isIntegral.map _),

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

Goal state before:
pp: R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
this : (⨆ n, if n = 0 then ‖r‖ else 0) = ‖r‖
⊢ (⨆ n, if n = 0 then ‖X.coeff n - (C r).coeff n‖ ^ (1 - ↑n)⁻¹ else 0) = ‖r‖

Tactic:
rw [← this]
    apply congr_arg
    ext n
    by_cases hn : n = 0
    · rw [if_pos hn, if_pos hn, hn, cast_zero, sub_zero, coeff_X_zero, coeff_C_zero, zero_sub,
        norm_neg, inv_one, rpow_one]
    · rw [if_neg hn, if_neg hn]

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

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
r : ℝ
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ r
⊢ 0 ≤ r

Tactic:
exact le_trans (rpow_nonneg (apply_nonneg μ _) _) (hm m (le_refl _))

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ BddAbove (Set.range fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Tactic:
by
  have hψ : ∀ n, 0 ≤ 1 / (ψ n : ℝ) := fun _ ↦ by simp only [one_div, inv_nonneg, cast_nonneg]
  by_cases! hx : μ x ≤ 1
  · use 1
    simp only [mem_upperBounds, Set.mem_range, forall_exists_index]
    rintro _ n rfl
    apply le_trans (rpow_le_rpow (apply_nonneg _ _) (map_pow_le_pow' hμ1 _ _) (hψ n))
    rw [← rpow_natCast, ← rpow_mul (apply_nonneg _ _), mul_one_div]
    exact rpow_le_one (apply_nonneg _ _) hx (div_nonneg (cast_nonneg _) (cast_nonneg _))
  · use μ x
    simp only [mem_upperBounds, Set.mem_range, forall_exists_index]
    rintro _ n rfl
    apply le_trans (rpow_le_rpow (apply_nonneg _ _) (map_pow_le_pow' hμ1 _ _) (hψ n))
    rw [← rpow_natCast, ← rpow_mul (apply_nonneg _ _), mul_one_div]
    conv_rhs => rw [← rpow_one (μ x)]
    rw [rpow_le_rpow_left_iff hx]
    exact div_le_one_of_le₀ (cast_le.mpr (hs (ψ n))) (cast_nonneg _)

Goal state after: