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
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
p : P
t₁ : Set k
ht₁ : t₁ ∈ atTop
t₂ : Set V
ht₂ : ∃ t ∈ 𝓝 v, ∀ x ∈ t, t₂ ∈ 𝓝 x
hs : t₁ • t₂ ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
⊢ s ∈ (map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)).bind 𝓝

Tactic:
obtain ⟨t₃, ht₃, ht₂⟩ := ht₂

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
p : P
t₁ : Set k
ht₁ : t₁ ∈ atTop
t₂ : Set V
hs : t₁ • t₂ ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
t₃ : Set V
ht₃ : t₃ ∈ 𝓝 v
ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x
⊢ s ∈ (map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)).bind 𝓝
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
⊢ asymptoticCone k s = closure[inst✝⁵] s

Tactic:
by
  ext v
  rw [mem_closure_iff_frequently, ← map_snd_prod (atTop (α := k)) (𝓝 v), frequently_map,
    mem_asymptoticCone_iff, asymptoticNhds_eq_smul, ← map₂_smul, ← map_prod_eq_map₂, frequently_map]
  apply frequently_congr
  filter_upwards [tendsto_fst.eventually (eventually_gt_atTop 0)] with ⟨c, u⟩ hc
  refine ⟨fun hu => ?_, hs c hc u⟩
  specialize hs c⁻¹ (inv_pos_of_pos hc) (c • u) hu
  rwa [inv_smul_smul₀ hc.ne'] at hs

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

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst✝²] s
hc : 0 ≤ c
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ p ∈ s
t : k
u : V
ht : c ≤ t
h : t • u +ᵥ p ∈ s
⊢ c • u +ᵥ p ∈ segment k p (t • u +ᵥ p)

Tactic:
mem_segment_iff_sameRay,

Goal state after:
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst✝²] s
hc : 0 ≤ c
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ p ∈ s
t : k
u : V
ht : c ≤ t
h : t • u +ᵥ p ∈ s
⊢ SameRay k ((c • u +ᵥ p) - p) ((t • u +ᵥ p) - (c • u +ᵥ p))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case inr
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ ↑n
⊢ ‖↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)‖ ≤ rexp (-x) * x ^ (s.re - 1)

Tactic:
norm_mul,

Goal state after:
case inr
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ ↑n
⊢ ‖↑((1 - x / ↑n) ^ n)‖ * ‖↑x ^ (s - 1)‖ ≤ rexp (-x) * x ^ (s.re - 1)
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun u ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
⊢ c • v +ᵥ p ∈ [-(c • u) +ᵥ c • v +ᵥ p -[k] t • u +ᵥ c • v +ᵥ p]

Tactic:
mem_segment_iff_sameRay,

Goal state after:
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun u ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
⊢ SameRay k ((c • v +ᵥ p) - (-(c • u) +ᵥ c • v +ᵥ p)) ((t • u +ᵥ c • v +ᵥ p) - (c • v +ᵥ p))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
⊢ ↑n * ↑n ! ^ 2 /
      ((↑(∏ i ∈ Finset.range n, (i + 1) ^ 2) * ∏ x ∈ Finset.range n, (1 - z ^ 2 / (↑x + 1) ^ 2)) * (z * (↑n + 1 - z))) =
    ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))

Tactic:
Finset.prod_pow,

Goal state after:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
⊢ ↑n * ↑n ! ^ 2 /
      ((↑((∏ x ∈ Finset.range n, (x + 1)) ^ 2) * ∏ x ∈ Finset.range n, (1 - z ^ 2 / (↑x + 1) ^ 2)) *
        (z * (↑n + 1 - z))) =
    ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
⊢ ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))

Tactic:
one_mul

Goal state after:
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
⊢ ↑π / sin (↑π * z) = ↑π / sin (↑π * z)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case neg
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
this : sin (↑π * s) ≠ 0
A : ↑π / sin (↑π * s) ≠ 0
⊢ Gamma s ≠ 0

Tactic:
rw [← Complex.Gamma_mul_Gamma_one_sub s, mul_ne_zero_iff] at A

Goal state after:
case neg
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
this : sin (↑π * s) ≠ 0
A : Gamma s ≠ 0 ∧ Gamma (1 - s) ≠ 0
⊢ Gamma s ≠ 0
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case refine_2
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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : s.Regular
σ : Equiv.Perm (Fin (n + 1))
⊢ ∃ x, (s.reindex e).points ∘ ⇑σ = ⇑x ∘ (s.reindex e).points

Tactic:
rcases h ((e.trans σ).trans e.symm) with ⟨x, hx⟩
    refine ⟨x, ?_⟩
    ext i
    simpa using congrFun hx (e.symm i)

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
hr0 : ∀ (i : Fin 3), r i ≠ 0
p' : P
hp' : ∀ (i : Fin 3), p' ∈ line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
⊢ ∏ x, r x ≠ 0

Tactic:
exact Finset.prod_ne_zero_iff.2 fun _ _ ↦ hr0 _

Goal state after:
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: α : Type u_1
L : SummationFilter α
f : α → ℝ
⊢ Summable (fun a ↦ ↑(f a)) L ↔ Summable f L

Tactic:
by
  simpa only using!
    Summable.map_iff_of_leftInverse (algebraMap ℝ ℍ) (show ℍ →ₗ[ℝ] ℝ from
      QuaternionAlgebra.reₗ _ _ _)
      (continuous_algebraMap _ _) continuous_re re_coe

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

Goal state before:
pp: case succ
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z : ℝ × ℝ), M ≤ ‖φ x z‖
n : ℕ
ih : ∀ {p : ℝ[X]}, p.IsMonicOfDegree (2 * n) → M ^ n ≤ ‖(aeval x) p‖
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * n + 2)
f₁ f₂ : ℝ[X]
hf₁ : f₁.IsMonicOfDegree 2
hf₂ : f₂.IsMonicOfDegree (2 * n)
H : p = f₁ * f₂
a b : ℝ
hab : f₁ = X ^ 2 - C a * X + C b
⊢ M ^ (n + 1) ≤ ‖(aeval x) f₁ * (aeval x) f₂‖

Tactic:
norm_mul,

Goal state after:
case succ
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z : ℝ × ℝ), M ≤ ‖φ x z‖
n : ℕ
ih : ∀ {p : ℝ[X]}, p.IsMonicOfDegree (2 * n) → M ^ n ≤ ‖(aeval x) p‖
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * n + 2)
f₁ f₂ : ℝ[X]
hf₁ : f₁.IsMonicOfDegree 2
hf₂ : f₂.IsMonicOfDegree (2 * n)
H : p = f₁ * f₂
a b : ℝ
hab : f₁ = X ^ 2 - C a * X + C b
⊢ M ^ (n + 1) ≤ ‖(aeval x) f₁‖ * ‖(aeval x) f₂‖
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel : ‖(aeval x) (q u) * (aeval x) p‖ = ‖(aeval x) (q w ^ n - (q w - q u) ^ n)‖
⊢ ‖φ x u‖ * ‖(aeval x) p‖ ≤ M ^ n + ‖φ x u - φ x w‖ ^ n

Tactic:
norm_mul,

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel : ‖(aeval x) (q u)‖ * ‖(aeval x) p‖ = ‖(aeval x) (q w ^ n - (q w - q u) ^ n)‖
⊢ ‖φ x u‖ * ‖(aeval x) p‖ ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: case mk
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f f' : AlgebraNorm R S
toRingNorm✝ : RingNorm S
smul'✝ : ∀ (a : R) (x : S), toRingNorm✝.toFun (a • x) = ‖a‖ * toRingNorm✝.toFun x
h : ⇑{ toRingNorm := toRingNorm✝, smul' := smul'✝ }.toRingSeminorm = ⇑f'.toRingSeminorm
⊢ { toRingNorm := toRingNorm✝, smul' := smul'✝ } = f'

Tactic:
cases f'

Goal state after:
case mk.mk
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
toRingNorm✝¹ : RingNorm S
smul'✝¹ : ∀ (a : R) (x : S), toRingNorm✝¹.toFun (a • x) = ‖a‖ * toRingNorm✝¹.toFun x
toRingNorm✝ : RingNorm S
smul'✝ : ∀ (a : R) (x : S), toRingNorm✝.toFun (a • x) = ‖a‖ * toRingNorm✝.toFun x
h :
  ⇑{ toRingNorm := toRingNorm✝¹, smul' := smul'✝¹ }.toRingSeminorm =
    ⇑{ toRingNorm := toRingNorm✝, smul' := smul'✝ }.toRingSeminorm
⊢ { toRingNorm := toRingNorm✝¹, smul' := smul'✝¹ } = { toRingNorm := toRingNorm✝, smul' := smul'✝ }
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ ⨆ y, f (1 * y) / f y = 1

Tactic:
one_mul

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ ⨆ y, f y / f y = 1
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
f_ne_zero : f = 0
⊢ ⨆ y, f (1 * y) / f y ≤ 1

Tactic:
one_mul

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
f_ne_zero : f = 0
⊢ ⨆ y, f y / f y ≤ 1
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
F : Filter ι
inst✝³ : AddCommSemigroup R
inst✝² : Sub R
inst✝¹ : ContinuousSub R
inst✝ : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f
⊢ limsup (fun i ↦ f i - c) F = limsup f F - c

Tactic:
by
  rcases F.eq_or_neBot with rfl | _
  · have {a : R} : sInf Set.univ ≤ a := by
      apply csInf_le _ (Set.mem_univ a)
      simp only [IsCoboundedUnder, IsCobounded, map_bot, eventually_bot, true_implies] at cobdd
      rcases cobdd with ⟨x, hx⟩
      refine ⟨x, mem_lowerBounds.2 fun y ↦ ?_⟩
      simp only [Set.mem_univ, hx y, implies_true]
    simp only [limsup, limsSup, map_bot, eventually_bot, Set.ofPred_true]
    exact this.antisymm (tsub_le_iff_right.2 this)
  · apply (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x - c) _ _).symm
    · exact fun _ _ h ↦ tsub_le_tsub_right h c
    · exact (continuous_sub_right c).continuousAt

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✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean Norm.norm
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x + y)) i‖) = ‖(B.repr (x + y)) ixy‖
⊢ B.norm (x + y) ≤ max (B.norm x) (B.norm y)

Tactic:
have hxy : ‖B.repr (x + y) ixy‖ ≤ max ‖B.repr x ixy‖ ‖B.repr y ixy‖ := by
    rw [map_add, Finsupp.coe_add, Pi.add_apply]; exact hna _ _

Goal state after:
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
hna : IsNonarchimedean Norm.norm
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x + y)) i‖) = ‖(B.repr (x + y)) ixy‖
hxy : ‖(B.repr (x + y)) ixy‖ ≤ max ‖(B.repr x) ixy‖ ‖(B.repr y) ixy‖
⊢ B.norm (x + y) ≤ max (B.norm x) (B.norm y)
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: 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‖
| B.norm (x * y)

Tactic:
simp only [Basis.norm]

Goal state after:
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‖
| univ.sup' ⋯ fun i ↦ ‖(B.repr (x * y)) i‖
Module: Mathlib.Analysis.Normed.Group.CocompactMap

Goal state before:
pp: E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : 𝓕
inst✝² : ProperSpace F
inst✝¹ : FunLike 𝓕 E F
inst✝ : CocompactMapClass 𝓕 E F
ε : ℝ
h : ⇑f ⁻¹' (closedBall 0 ε)ᶜ ∈ cocompact E
r : ℝ
hr : (closedBall 0 r)ᶜ ⊆ ⇑f ⁻¹' (closedBall 0 ε)ᶜ
⊢ ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖

Tactic:
use r

Goal state after:
case h
E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : 𝓕
inst✝² : ProperSpace F
inst✝¹ : FunLike 𝓕 E F
inst✝ : CocompactMapClass 𝓕 E F
ε : ℝ
h : ⇑f ⁻¹' (closedBall 0 ε)ᶜ ∈ cocompact E
r : ℝ
hr : (closedBall 0 r)ᶜ ⊆ ⇑f ⁻¹' (closedBall 0 ε)ᶜ
⊢ ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
Module: Mathlib.Analysis.Normed.Group.CocompactMap

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
ε : ℝ
hε : (closedBall 0 ε)ᶜ ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
⊢ ∃ r, (closedBall 0 r)ᶜ ⊆ f ⁻¹' s

Tactic:
use r

Goal state after:
case h
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
ε : ℝ
hε : (closedBall 0 ε)ᶜ ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
⊢ (closedBall 0 r)ᶜ ⊆ f ⁻¹' s
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case inl
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h : 0 < ↑p.natDegree - ↑m
hps : s.card = p.natDegree
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h1 : (-1) ^ (s.card - m) = 1
⊢ f (1 * s.esymm (s.card - m)) = f (s.esymm (s.card - m))

Tactic:
one_mul

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

Goal state before:
pp: case pos
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h✝ : 0 < ↑p.natDegree - ↑m
hps : s.card = p.natDegree
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h : f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge : f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
⊢ f t.prod ≤ (⨆ x, if x ∈ s then f x else 0) ^ (p.natDegree - m)

Tactic:
have h_pr : f t.prod ≤ (t.map f).prod := le_prod_of_submultiplicative_of_nonneg f
        (apply_nonneg _) (le_of_eq hf1) (map_mul_le_mul _) t

Goal state after:
case pos
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h✝ : 0 < ↑p.natDegree - ↑m
hps : s.card = p.natDegree
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h : f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge : f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
⊢ f t.prod ≤ (⨆ x, if x ∈ s then f x else 0) ^ (p.natDegree - m)
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
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 (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm : ∀ (b_1 : ℕ), m ≤ b_1 → μ x ^ (↑(s (ψ b_1)) * (1 / ↑(ψ b_1))) ≤ b
⊢ ∀ (b_1 : ℕ), m ≤ b_1 → μ (x ^ s (ψ b_1)) ^ (1 / ↑(ψ b_1)) ≤ b

Tactic:
intro k hkm

Goal state after:
case h
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 (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm : ∀ (b_1 : ℕ), m ≤ b_1 → μ x ^ (↑(s (ψ b_1)) * (1 / ↑(ψ b_1))) ≤ b
k : ℕ
hkm : m ≤ k
⊢ μ (x ^ s (ψ k)) ^ (1 / ↑(ψ k)) ≤ b
Module: Mathlib.Analysis.Normed.Group.HomCompletion

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

Tactic:
NormedAddGroupHom.coe_id,

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

Goal state before:
pp: V W : SemiNormedGrp
f g : V ⟶ W
c : Fork f g
⊢ (NormedAddGroupHom.compHom (Hom.hom f) - NormedAddGroupHom.compHom (Hom.hom g)) (Hom.hom c.ι) = 0

Tactic:
AddMonoidHom.sub_apply,

Goal state after:
V W : SemiNormedGrp
f g : V ⟶ W
c : Fork f g
⊢ (NormedAddGroupHom.compHom (Hom.hom f)) (Hom.hom c.ι) - (NormedAddGroupHom.compHom (Hom.hom g)) (Hom.hom c.ι) = 0
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
x : L
hf1 : f 1 = 1
p : K[X] := minpoly K x
hp_sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
s : Multiset L
hs : Polynomial.map (algebraMap K L) (minpoly K x) = 1 * (Multiset.map (fun x ↦ X - C x) s).prod
h_lc : (algebraMap K L) (minpoly K x).leadingCoeff = 1
⊢ spectralNorm K L x ≤ ⨆ σ, f (σ x)

Tactic:
one_mul

Goal state after:
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
x : L
hf1 : f 1 = 1
p : K[X] := minpoly K x
hp_sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
s : Multiset L
hs : Polynomial.map (algebraMap K L) (minpoly K x) = (Multiset.map (fun x ↦ X - C x) s).prod
h_lc : (algebraMap K L) (minpoly K x).leadingCoeff = 1
⊢ spectralNorm K L x ≤ ⨆ σ, f (σ x)
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
inst✝ : NontrivialTopology M
⊢ ‖normedMk‖ = 1

Tactic:
apply NormedAddGroupHom.opNorm_eq_of_bounds _ zero_le_one
  · simpa only [normedMk_apply, one_mul] using! fun _ ↦ le_rfl
  · intro N _ hle
    obtain ⟨x, _⟩ := exists_norm_ne_zero M
    exact one_le_of_le_mul_right₀ (by positivity) (hle x)

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
n✝ : R
n : ℕ+
hpos : (-1) ^ ↑n = 1
⊢ μ (1 * n✝ ^ ↑n) ^ (1 / ↑↑n) = μ (n✝ ^ ↑n) ^ (1 / ↑↑n)

Tactic:
one_mul

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
n✝ : R
n : ℕ+
hpos : (-1) ^ ↑n = 1
⊢ μ (n✝ ^ ↑n) ^ (1 / ↑↑n) = μ (n✝ ^ ↑n) ^ (1 / ↑↑n)