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

Goal state before:
pp: case inr
ι : 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
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v)
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > limsup v f
c : ℝ
c_ab : c > a * b
x : ι
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
u_0 : 0 ≤ u x
⊢ u x * v x ≤ a * b

Tactic:
· exact mul_le_mul x_a.le x_b.le v_0 (u_0.trans x_a.le)

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
i : ι
hBi : B i = 1
x : K
⊢ B.norm ((algebraMap K L) x) = ‖x‖

Tactic:
simp only [norm, repr_algebraMap hBi, Finsupp.single_apply]
  apply le_antisymm
  · aesop
  · exact le_sup'_of_le _ (mem_univ i) (by simp)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n ↦ ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun t ↦ -(↑(t % m1) / ↑t)) atTop (𝓝 (-0))

Tactic:
exact Tendsto.neg h_exp

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

Goal state before:
pp: case h
F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ (f x) ≤ C * nα x
hlim : Tendsto (fun n ↦ C ^ (1 / ↑n) * nα x) atTop (𝓝 (nα x))
n : ℕ
hn : 1 ≤ n
h : (C ^ (1 / ↑n)) ^ n = C
⊢ nβ (f x) ^ n ≤ (C ^ (1 / ↑n) * nα x) ^ n

Tactic:
mul_pow,

Goal state after:
case h
F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ (f x) ≤ C * nα x
hlim : Tendsto (fun n ↦ C ^ (1 / ↑n) * nα x) atTop (𝓝 (nα x))
n : ℕ
hn : 1 ≤ n
h : (C ^ (1 / ↑n)) ^ n = C
⊢ nβ (f x) ^ n ≤ (C ^ (1 / ↑n)) ^ n * nα x ^ n
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
x : R
h : x = 0
⊢ seminormFromBounded' f x = 0

Tactic:
h

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
x : R
h : x = 0
⊢ seminormFromBounded' f 0 = 0
Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
hf : RingHom.IsBoundedWrt (⇑nα) nβ f
x : α
⊢ nβ (f x) ≤ nα x

Tactic:
obtain ⟨C, hC0, hC⟩ := hf
  have hlim : Tendsto (fun n : ℕ => C ^ (1 / (n : ℝ)) * nα x) atTop (𝓝 (nα x)) := by
    nth_rewrite 2 [← one_mul (nα x)]
    exact ((rpow_zero C ▸ ContinuousAt.tendsto (continuousAt_const_rpow (ne_of_gt hC0))).comp
      (tendsto_const_div_atTop_nhds_zero_nat 1)).mul tendsto_const_nhds
  apply ge_of_tendsto hlim
  simp only [eventually_atTop]
  use 1
  intro n hn
  have h : (C ^ (1 / n : ℝ)) ^ n = C := by
    have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (ne_of_gt hn)
    rw [← rpow_natCast, ← rpow_mul hC0.le, one_div, inv_mul_cancel₀ hn0, rpow_one]
  apply le_of_pow_le_pow_left₀ (ne_of_gt hn) (by positivity)
  · rw [mul_pow, h, ← hβ _ hn, ← map_pow]
    apply le_trans (hC (x ^ n))
    rw [mul_le_mul_iff_right₀ hC0]
    exact map_pow_le_pow _ _ (Nat.one_le_iff_ne_zero.mp hn)

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.IsConjRoot

Goal state before:
pp: K : Type u_2
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Field K
inst✝ : Algebra K S
x y : S
r : K
h : IsConjRoot K x y
⊢ (minpoly K x).comp (X - C r) = (minpoly K y).comp (X - C r)

Tactic:
h

Goal state after:
K : Type u_2
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Field K
inst✝ : Algebra K S
x y : S
r : K
h : IsConjRoot K x y
⊢ (minpoly K y).comp (X - C r) = (minpoly K y).comp (X - C r)
Module: Mathlib.FieldTheory.Minpoly.IsConjRoot

Goal state before:
pp: K : Type u_2
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Field K
inst✝ : Algebra K S
x y : S
h : IsConjRoot K x y
⊢ (-1) ^ (minpoly K x).natDegree * (minpoly K x).comp (-X) = (-1) ^ (minpoly K y).natDegree * (minpoly K y).comp (-X)

Tactic:
h

Goal state after:
K : Type u_2
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Field K
inst✝ : Algebra K S
x y : S
h : IsConjRoot K x y
⊢ (-1) ^ (minpoly K y).natDegree * (minpoly K y).comp (-X) = (-1) ^ (minpoly K y).natDegree * (minpoly K y).comp (-X)
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
this : (⨆ n, if n = 0 then ‖r‖ else 0) = ‖r‖
n : ℕ
hn : n = 0
⊢ ‖r‖ ^ 1⁻¹ = ‖r‖

Tactic:
inv_one,

Goal state after:
case pos
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
this : (⨆ n, if n = 0 then ‖r‖ else 0) = ‖r‖
n : ℕ
hn : n = 0
⊢ ‖r‖ ^ 1 = ‖r‖
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : S.Nonempty
⊢ δ ≤ ‖a - a'‖

Tactic:
simp only [hS, ↓reduceDIte, δ]

Goal state after:
case pos
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : S.Nonempty
⊢ (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ ≤ ‖a - a'‖
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : ¬S.Nonempty
⊢ δ ≤ ‖a - a'‖

Tactic:
simp only [hS, ↓reduceDIte, δ]

Goal state after:
case neg
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : ¬S.Nonempty
⊢ 1 ≤ ‖a - a'‖
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : S.Nonempty
⊢ δ > 0

Tactic:
simp only [hS, ↓reduceDIte, δ]

Goal state after:
case pos
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : S.Nonempty
⊢ (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ > 0
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : ¬S.Nonempty
⊢ δ > 0

Tactic:
simp only [hS, ↓reduceDIte, δ]

Goal state after:
case neg
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : ¬S.Nonempty
⊢ 1 > 0
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
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, f z ≤ f y
⊢ (Multiset.map (⇑f) t).prod ≤ (⨆ x, if x ∈ s then f x else 0) ^ (p.natDegree - m)

Tactic:
have : (map f t).prod ≤ f y ^ (p.natDegree - m) := by
        set g : L → NNReal := fun x ↦ ⟨f x, apply_nonneg f x⟩
        have h_card : p.natDegree - m = card (t.map g) := by rw [card_map, ht_card, ← hps]
        have hx_le : ∀ x : NNReal, x ∈ map g t → x ≤ g y := by
          intro r hr
          obtain ⟨_, hzt, hzr⟩ := mem_map.mp hr
          exact hzr ▸ hy_max _ (hts _ hzt)
        have : (map g t).prod ≤ g y ^ (p.natDegree - m) := h_card ▸ prod_le_pow_card _ _ hx_le
        simpa [g, ← NNReal.coe_le_coe, NNReal.coe_pow, NNReal.coe_mk, NNReal.coe_multiset_prod,
          map_map, Function.comp_apply, NNReal.coe_mk] using! this

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
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, f z ≤ f y
this : (Multiset.map (⇑f) t).prod ≤ f y ^ (p.natDegree - m)
⊢ (Multiset.map (⇑f) t).prod ≤ (⨆ x, if x ∈ s then f x else 0) ^ (p.natDegree - m)
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ e = explicitCokernelDesc w

Tactic:
apply (isColimitCokernelCocone f).uniq (Cofork.ofπ g (by simp [w]))

Goal state after:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ ∀ (j : WalkingParallelPair), (cokernelCocone f).ι.app j ≫ e = (Cofork.ofπ g ⋯).ι.app j
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y : SemiNormedGrp
f : X ⟶ Y
Z : SemiNormedGrp
g : explicitCokernel f ⟶ Z
⊢ ∀ (h : explicitCokernel f ⟶ Z), explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h → g = h

Tactic:
h

Goal state after:
X Y : SemiNormedGrp
f : X ⟶ Y
Z : SemiNormedGrp
g h : explicitCokernel f ⟶ Z
⊢ explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h → g = h
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
hu : IsUltrametricDist K
x : L
hna : IsNonarchimedean fun x ↦ ‖x‖
⊢ spectralNorm K L x = (invariantExtension K L) x

Tactic:
set f := Classical.choose (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hna)
    with hf

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
hu : IsUltrametricDist K
x : L
hna : IsNonarchimedean fun x ↦ ‖x‖
f : AlgebraNorm K L := Classical.choose ⋯
hf : f = Classical.choose ⋯
⊢ spectralNorm K L x = (invariantExtension K L) x
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
inst✝ : IsUltrametricDist K
⊢ IsPowMul (spectralNorm K L)

Tactic:
rw [spectralNorm_eq_invariantExtension K L]
  exact isPowMul_invariantExtension K L

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

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
y : L
h_fin : FiniteDimensional K L
hn : Normal K L
inst✝ : IsUltrametricDist K
⊢ ∀ (x y : L), spectralNorm K L (x * y) ≤ spectralNorm K L x * spectralNorm K L y

Tactic:
simp only [spectralNorm_eq_invariantExtension]
    exact map_mul_le_mul (invariantExtension K L)

Goal state after:
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‖₊
hf_iso : ∀ (σ : Gal(L/K)) (x : L), f x = f (σ x)
x : L
⊢ ⨆ σ, f (σ x) = ⨆ x_1, f x

Tactic:
exact iSup_congr fun σ ↦ by rw [hf_iso σ x]

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

Goal state before:
pp: K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
k : K
y : L
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
hgy : k • y = (algebraMap (↥K⟮y⟯) L) (k • g)
h :
  (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) (k • g) =
    k • (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g
⊢ spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      ((algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) (k • g)) =
    ↑‖k‖₊ *
      spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
        ((algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g)

Tactic:
h

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
k : K
y : L
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
hgy : k • y = (algebraMap (↥K⟮y⟯) L) (k • g)
h :
  (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) (k • g) =
    k • (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g
⊢ spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      (k • (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g) =
    ↑‖k‖₊ *
      spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
        ((algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g)
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
⊢ normedMk x = 0

Tactic:
h

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
⊢ 0 x = 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
inst✝ : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
⊢ IsNonarchimedean (spectralNorm K L)

Tactic:
by
  intro x y
  set E := K⟮x, y⟯
  have h_finiteDimensional_E : FiniteDimensional K E :=
    IntermediateField.finiteDimensional_adjoin_pair (h_alg.isAlgebraic x).isIntegral
       (h_alg.isAlgebraic y).isIntegral
  set gx := IntermediateField.AdjoinPair.gen₁ K x y
  set gy := IntermediateField.AdjoinPair.gen₂ K x y
  have hxy : x + y = (algebraMap K⟮x, y⟯ L) (gx + gy) := rfl
  rw [hxy, ← spectralNorm.eq_of_normalClosure (gx + gy) hxy,
    ← spectralNorm.eq_of_normalClosure gx (IntermediateField.AdjoinPair.algebraMap_gen₁ K x y),
    ← spectralNorm.eq_of_normalClosure gy (IntermediateField.AdjoinPair.algebraMap_gen₂ K x y),
    _root_.map_add]
  apply isNonarchimedean_spectralNorm_of_finiteDimensional_normal

Goal state after:
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‖
n : α
⊢ (∀ (k : β), ‖f n k‖ ≤ bound k) → Summable fun x ↦ ‖f n x‖

Tactic:
h

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‖
n : α
h : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ Summable fun x ↦ ‖f n x‖
Module: Mathlib.Analysis.Normed.Group.Tannery

Goal state before:
pp: case inr.inr
α : 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
⊢ ∀ᶠ (x : α) in 𝓕, dist (∑' (k : β), f x k) (∑' (k : β), g k) < ε

Tactic:
let ⟨S, hS⟩ := h_sum

Goal state after:
case inr.inr
α : 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
⊢ ∀ᶠ (x : α) in 𝓕, dist (∑' (k : β), f x k) (∑' (k : β), g k) < ε
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
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
y : R
hlim : Tendsto (fun n ↦ μ x * smoothingSeminormSeq μ y n) atTop (𝓝 (smoothingFun μ x * smoothingFun μ y))
n : ℕ
hn1 : 1 ≤ n
hn0 : ↑n ≠ 0
⊢ μ ((x * y) ^ n) ^ (1 / ↑n) = μ x * μ (y ^ n) ^ (1 / ↑n)

Tactic:
mul_pow,

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
y : R
hlim : Tendsto (fun n ↦ μ x * smoothingSeminormSeq μ y n) atTop (𝓝 (smoothingFun μ x * smoothingFun μ y))
n : ℕ
hn1 : 1 ≤ n
hn0 : ↑n ≠ 0
⊢ μ (x ^ n * y ^ n) ^ (1 / ↑n) = μ x * μ (y ^ n) ^ (1 / ↑n)