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
hs : t₁ • t₂ ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
t₃ : Set V
ht₃ : t₃ ∈ 𝓝 v
ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x
c : k
x✝ : c ∈ t₁ ∩ Set.Ioi 0
u : V
hu : u ∈ t₃
hc₁ : c ∈ t₁
hc₂ : c ∈ Set.Ioi 0
⊢ (fun x ↦ x +ᵥ p) ⁻¹' s ∈ 𝓝 (c • u)

Tactic:
filter_upwards [smul_mem_nhds_smul₀ hc₂.ne' (ht₂ u hu)]

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
c : k
x✝ : c ∈ t₁ ∩ Set.Ioi 0
u : V
hu : u ∈ t₃
hc₁ : c ∈ t₁
hc₂ : c ∈ Set.Ioi 0
⊢ ∀ a ∈ c • t₂, a ∈ (fun x ↦ x +ᵥ p) ⁻¹' s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℝ
⊢ ↑(Gamma s * Gamma (1 - s)) = ↑(π / sin (π * s))

Tactic:
Complex.ofReal_div,

Goal state after:
s : ℝ
⊢ ↑(Gamma s * Gamma (1 - s)) = ↑π / ↑(sin (π * s))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

Goal state before:
pp: z : ℂ
⊢ HasSum (fun n ↦ (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)

Tactic:
have := (((expSeries_div_hasSum_exp (-z * Complex.I)).sub
    (expSeries_div_hasSum_exp (z * Complex.I))).mul_right Complex.I).div_const 2

Goal state after:
z : ℂ
this :
  HasSum (fun i ↦ ((-z * I) ^ i / ↑i ! - (z * I) ^ i / ↑i !) * I / 2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
⊢ HasSum (fun n ↦ (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
Module: Mathlib.Analysis.Normed.Ring.Ultra

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
z : ℤ
⊢ ‖↑z‖₊ ≤ 1

Tactic:
cases z <;>
  simpa only [Int.ofNat_eq_natCast, Int.cast_natCast, Int.cast_negSucc, Nat.cast_one, nnnorm_neg]
    using nnnorm_natCast_le_one _ _

Goal state after:
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
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n

Tactic:
have hq (y : ℝ × ℝ) : IsMonicOfDegree (q y) 2 := isMonicOfDegree_sub_add_two ..

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
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
m : ℕ
⊢ p (x ^ s (ψ m)) ^ (1 / ↑(ψ m)) ≤ p x ^ (↑(s (ψ m)) / ↑(ψ m))

Tactic:
← mul_one_div (s (ψ m) : ℝ),

Goal state after:
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
m : ℕ
⊢ p (x ^ s (ψ m)) ^ (1 / ↑(ψ m)) ≤ p x ^ (↑(s (ψ m)) * (1 / ↑(ψ m)))
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ IsBoundedUnder LE.le atTop fun n ↦ p (x ^ s (ψ n)) ^ (1 / ↑(ψ n))

Tactic:
have h_le : ∀ m : ℕ, p (x ^ s (ψ m)) ^ (1 / (ψ m : ℝ)) ≤ p x ^ ((s (ψ m) : ℝ) / (ψ m : ℝ)) := by
    intro m
    rw [← mul_one_div (s (ψ m) : ℝ), rpow_mul (apply_nonneg p x), rpow_natCast]
    grw [map_pow_le_pow' hp x]
  apply isBoundedUnder_of
  cases le_or_gt (p x) 1 with
  | inl hfx =>
    use 1, fun m ↦ le_trans (h_le m) (rpow_le_one (by positivity) hfx (by positivity))
  | inr hfx =>
    use p x
    refine fun m ↦ le_trans (h_le m) <| rpow_le_self_of_one_le hfx.le ?_
    exact div_le_one_of_le₀ (mod_cast hs_le _) (cast_nonneg _)

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

Goal state before:
pp: case hf
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)
h0 : Tendsto (fun t ↦ -(↑(t % m1) / ↑t)) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ (L + ε) ^ (-(↑(x % m1) / ↑x))) atTop (𝓝 1)

Tactic:
← rpow_zero (L + ε)

Goal state after:
case hf
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)
h0 : Tendsto (fun t ↦ -(↑(t % m1) / ↑t)) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ (L + ε) ^ (-(↑(x % m1) / ↑x))) atTop (𝓝 ((L + ε) ^ 0))
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✝ : Normal 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'‖
z : L := x - y
this : FiniteDimensional K ↥K⟮y⟯
⊢ x ∈ K⟮y⟯

Tactic:
have : IsUltrametricDist L := IsUltrametricDist.of_normedAlgebra K

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✝ : Normal 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'‖
z : L := x - y
this✝ : FiniteDimensional K ↥K⟮y⟯
this : IsUltrametricDist L
⊢ x ∈ K⟮y⟯
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) < (L + ε / 2) ^ ↑↑m1
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
hm10 : ↑↑m1 ≠ 0
h_lt : 0 < ↑(n / ↑m1) / ↑n
⊢ μ (x ^ ↑m1) ^ (↑(n / ↑m1) / ↑n) < (L + ε / 2) ^ (↑↑m1 * (↑(n / ↑m1) / ↑n))

Tactic:
rpow_mul (le_of_lt hL0')

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) < (L + ε / 2) ^ ↑↑m1
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
hm10 : ↑↑m1 ≠ 0
h_lt : 0 < ↑(n / ↑m1) / ↑n
⊢ μ (x ^ ↑m1) ^ (↑(n / ↑m1) / ↑n) < ((L + ε / 2) ^ ↑↑m1) ^ (↑(n / ↑m1) / ↑n)
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
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : sSup (Set.range (spectralValueTerms p)) < f x
n : ℕ
hn : n < p.natDegree
hexp : (‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n))) ^ (p.natDegree - n) = ‖p.coeff n‖
⊢ ‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n)) < f x

Tactic:
Set.Finite.csSup_lt_iff (spectralValueTerms_finite_range p)
          (Set.range_nonempty (spectralValueTerms p))

Goal state after:
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ∀ x_1 ∈ Set.range (spectralValueTerms p), x_1 < f x
n : ℕ
hn : n < p.natDegree
hexp : (‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n))) ^ (p.natDegree - n) = ‖p.coeff n‖
⊢ ‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n)) < f 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
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
⊢ s.card = p.natDegree

Tactic:
rw [← natDegree_map (algebraMap K L), ← mapAlg_eq_map, hp,
          natDegree_multiset_prod_X_sub_C_eq_card]

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✝ : 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
g : L → NNReal := fun x ↦ ⟨f x, ⋯⟩
h_card : p.natDegree - m = (Multiset.map g t).card
⊢ ∀ x ∈ Multiset.map g t, x ≤ g y

Tactic:
intro r hr

Goal state after:
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
g : L → NNReal := fun x ↦ ⟨f x, ⋯⟩
h_card : p.natDegree - m = (Multiset.map g t).card
r : NNReal
hr : r ∈ Multiset.map g t
⊢ r ≤ g y
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case h
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)
⊢ f y ∈ upperBounds (Set.range fun x ↦ if x ∈ s then f x else 0)

Tactic:
intro r hr

Goal state after:
case h
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)
r : ℝ
hr : r ∈ Set.range fun x ↦ if x ∈ s then f x else 0
⊢ r ≤ f y
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
m : ℕ
hm : 1 ≤ m
h0 : ↑(ψ m) ≠ 0
⊢ ↑(ψ m) / ↑(ψ m) - ↑(mu (ψ m)) / ↑(ψ m) = ↑(nu (ψ m)) / ↑(ψ m)

Tactic:
← sub_div,

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
m : ℕ
hm : 1 ≤ m
h0 : ↑(ψ m) ≠ 0
⊢ (↑(ψ m) - ↑(mu (ψ m))) / ↑(ψ m) = ↑(nu (ψ m)) / ↑(ψ m)
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
S : ℝ
hS : HasSum bound S
⊢ ∀ᶠ (x : α) in 𝓕, dist (∑' (k : β), f x k) (∑' (k : β), g k) < ε

Tactic:
obtain ⟨T, hT⟩ : ∃ (T : Finset β), dist (∑ b ∈ T, bound b) S < ε / 3 := by
    rw [HasSum, Metric.tendsto_nhds] at hS
    exact Eventually.exists <| hS _ (by positivity)

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
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
⊢ ∀ᶠ (x : α) in 𝓕, dist (∑' (k : β), f x k) (∑' (k : β), g k) < ε
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
x : L
E : Type v := ((mapAlg K L) (minpoly K x)).SplittingField
hspl : ((mapAlg K E) (minpoly K x)).Splits
this✝ : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ spectralNorm K L x ^ (minpoly K x).natDegree = ‖(minpoly K x).coeff 0‖

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
x : L
E : Type v := ((mapAlg K L) (minpoly K x)).SplittingField
hspl : ((mapAlg K E) (minpoly K x)).Splits
this✝ : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ ↑(minpoly K x).natDegree ≠ 0

Tactic:
@spectralNorm.eq_of_tower K _ E,

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
x : L
E : Type v := ((mapAlg K L) (minpoly K x)).SplittingField
hspl : ((mapAlg K E) (minpoly K x)).Splits
this✝ : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ spectralNorm K E ((algebraMap L E) x) ^ (minpoly K x).natDegree = ‖(minpoly K x).coeff 0‖

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
x : L
E : Type v := ((mapAlg K L) (minpoly K x)).SplittingField
hspl : ((mapAlg K E) (minpoly K x)).Splits
this✝ : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ ↑(minpoly K x).natDegree ≠ 0
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
F : Type u_4
G : Type u_6
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
⊢ (inl R F G).HasLeftInverse

Tactic:
by
  use ContinuousLinearMap.fst _ _ _
  intro x
  simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P : { P // IsLprojection X P }
⊢ ↑P * (1 - ↑P) = ↑⊥

Tactic:
coe_bot,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P : { P // IsLprojection X P }
⊢ ↑P * (1 - ↑P) = 0
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
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
G : Type (max (max uE u𝕜) uι) := (⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker
G' : Submodule 𝕜 F := (lift f.toMultilinearMap).range
e : ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) ≃ₗ[𝕜] ↥(lift f.toMultilinearMap).range :=
  (lift f.toMultilinearMap).quotKerEquivRange
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) :=
  lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)
hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i, ‖x i‖
f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) := f'₀.mkContinuous ‖f‖ hf'₀
hnorm : ‖f'‖ ≤ ‖f‖
heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x
⊢ (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) ∈
    {p |
      ∃ G x x_1, p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)}

Tactic:
Set.mem_ofPred

Goal state after:
ι : 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
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
G : Type (max (max uE u𝕜) uι) := (⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker
G' : Submodule 𝕜 F := (lift f.toMultilinearMap).range
e : ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) ≃ₗ[𝕜] ↥(lift f.toMultilinearMap).range :=
  (lift f.toMultilinearMap).quotKerEquivRange
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) :=
  lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)
hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i, ‖x i‖
f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) := f'₀.mkContinuous ‖f‖ hf'₀
hnorm : ‖f'‖ ≤ ‖f‖
heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x
⊢ ∃ G_1 x x_1,
    (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) =
      (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G_1 →L[𝕜] G_1)).comp (toDualContinuousMultilinearMap G_1)
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: case refine_1
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ {p |
      ∃ G x x_1,
        p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)}.Nonempty

Tactic:
existsi 0

Goal state after:
case refine_1
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ 0 ∈
    {p |
      ∃ G x x_1, p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)}