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

Goal state before:
pp: case inr
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✝ s : Set V
hs : Convex k s
hs' : IsClosed[inst✝²] s
p : V
hp : p ∈ s
v : V
⊢ v ∈ asymptoticCone k s → StarConvex k v (asymptoticCone k s)

Tactic:
hv

Goal state after:
case inr
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✝ s : Set V
hs : Convex k s
hs' : IsClosed[inst✝²] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
⊢ StarConvex k v (asymptoticCone k s)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π

Tactic:
suffices (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z =>
      (Gamma (2 * z))⁻¹ * (2 : ℂ) ^ (2 * z - 1) / ↑(√π) by
    convert! congr_arg Inv.inv (congr_fun this s) using 1
    · rw [mul_inv, inv_inv, inv_inv]
    · rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]

Goal state after:
s : ℂ
⊢ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
Module: Mathlib.Analysis.Polynomial.Factorization

Goal state before:
pp: case inl
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
⊢ ∃ f₁ f₂, f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
obtain ⟨p₁, p₂, hp₁ | hp₂, h'⟩ := hg₂.eq_isMonicOfDegree_one_or_two_mul

Goal state after:
case inl.inl
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₁ : p₁.IsMonicOfDegree 1
⊢ ∃ f₁ f₂, f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

case inl.inr
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₂ : p₁.IsMonicOfDegree 2
⊢ ∃ f₁ f₂, f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
Module: Mathlib.Analysis.Polynomial.Factorization

Goal state before:
pp: case inl.inr
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₂ : p₁.IsMonicOfDegree 2
⊢ ∃ f₁ f₂, f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
rw [h', mul_left_comm] at h hf

Goal state after:
case inl.inr
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
hf : (p₁ * (g₁ * p₂)).IsMonicOfDegree (2 + n)
h : f = p₁ * (g₁ * p₂)
h' : g₂ = p₁ * p₂
hp₂ : p₁.IsMonicOfDegree 2
⊢ ∃ f₁ f₂, f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential

Goal state before:
pp: m : Type u_1
𝔸 : Type u_5
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : CommRing 𝔸
inst✝³ : TopologicalSpace 𝔸
inst✝² : IsTopologicalRing 𝔸
inst✝¹ : Algebra ℚ 𝔸
inst✝ : T2Space 𝔸
A : Matrix m m 𝔸
⊢ ∑' (n : ℕ), (↑n.factorial)⁻¹ • Aᵀ ^ n = ∑' (x : ℕ), ((↑x.factorial)⁻¹ • A ^ x)ᵀ

Tactic:
transpose_smul,

Goal state after:
m : Type u_1
𝔸 : Type u_5
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : CommRing 𝔸
inst✝³ : TopologicalSpace 𝔸
inst✝² : IsTopologicalRing 𝔸
inst✝¹ : Algebra ℚ 𝔸
inst✝ : T2Space 𝔸
A : Matrix m m 𝔸
⊢ ∑' (n : ℕ), (↑n.factorial)⁻¹ • Aᵀ ^ n = ∑' (x : ℕ), (↑x.factorial)⁻¹ • (A ^ x)ᵀ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

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

Tactic:
by
  convert! Complex.hasSum_sin' z using 1
  simp_rw [mul_pow, pow_succ, pow_mul, Complex.I_sq, ← mul_assoc, mul_div_assoc, div_right_comm,
    div_self Complex.I_ne_zero, mul_comm _ ((-1 : ℂ) ^ _), mul_one_div, mul_div_assoc, mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
⊢ ‖x + 1‖ ≤ a

Tactic:
have ha' : 1 < a := (max_lt_iff.mp ha).left

Goal state after:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
⊢ ‖x + 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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
⊢ f (x * y * z) / f z / seminormFromBounded' f y ≤ seminormFromBounded' f x

Tactic:
apply le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z

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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
⊢ f (x * y * z) / f z / seminormFromBounded' f y ≤ f (x * z) / f z
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 ⋯
hB1 : B ⟨1, h1L⟩ = 1
g : L → ℝ := B.norm
hg0 : g 0 = 0
hg_nonneg : ∀ (x : L), 0 ≤ g x
hg_ext : ∀ (x : K), g ((algebraMap K L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w✝¹ : ℝ
w✝ : 0 < w✝¹
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w✝¹ * B.norm x * B.norm y
hg_mul : ∀ (k : K) (y : L), g ((algebraMap K L) k * y) = g ((algebraMap K L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
hf_na : IsNonarchimedean ⇑f
hf_1 : f 1 ≤ 1
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
F' : RingSeminorm L := smoothingSeminorm f hf_1 hf_na
hF' : F' = smoothingSeminorm f hf_1 hf_na
hF'_ext : ∀ (k : K), F' ((algebraMap K L) k) = ‖k‖
hF'_1 : F' 1 = 1
hF'_0 : F' ≠ 0
k : K
y : L
hk : ∀ (y : L), f ((algebraMap K L) k * y) = f ((algebraMap K L) k) * f y
hfk : ‖k‖ = (smoothingSeminorm f hf_1 hf_na) ((algebraMap K L) k)
⊢ ((smoothingSeminorm f hf_1 hf_na).toRingNorm ⋯).toFun (k • y) =
    (smoothingSeminorm f hf_1 hf_na) ((algebraMap K L) k) * ((smoothingSeminorm f hf_1 hf_na).toRingNorm ⋯).toFun y

Tactic:
← smoothingSeminorm_of_mul f hf_1 hf_na hk y

Goal state after:
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 ⋯
hB1 : B ⟨1, h1L⟩ = 1
g : L → ℝ := B.norm
hg0 : g 0 = 0
hg_nonneg : ∀ (x : L), 0 ≤ g x
hg_ext : ∀ (x : K), g ((algebraMap K L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w✝¹ : ℝ
w✝ : 0 < w✝¹
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w✝¹ * B.norm x * B.norm y
hg_mul : ∀ (k : K) (y : L), g ((algebraMap K L) k * y) = g ((algebraMap K L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
hf_na : IsNonarchimedean ⇑f
hf_1 : f 1 ≤ 1
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
F' : RingSeminorm L := smoothingSeminorm f hf_1 hf_na
hF' : F' = smoothingSeminorm f hf_1 hf_na
hF'_ext : ∀ (k : K), F' ((algebraMap K L) k) = ‖k‖
hF'_1 : F' 1 = 1
hF'_0 : F' ≠ 0
k : K
y : L
hk : ∀ (y : L), f ((algebraMap K L) k * y) = f ((algebraMap K L) k) * f y
hfk : ‖k‖ = (smoothingSeminorm f hf_1 hf_na) ((algebraMap K L) k)
⊢ ((smoothingSeminorm f hf_1 hf_na).toRingNorm ⋯).toFun (k • y) =
    (smoothingSeminorm f hf_1 hf_na) ((algebraMap K L) k * y)
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:
by
    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.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n : ℕ
⊢ spectralValue (X ^ n) = 0

Tactic:
by
  rw [spectralValue]
  unfold spectralValueTerms
  simp_rw [coeff_X_pow n, natDegree_X_pow]
  convert! ciSup_const using 2
  · ext m
    by_cases hmn : m < n
    · rw [if_pos hmn, rpow_eq_zero_iff_of_nonneg (norm_nonneg _), if_neg (_root_.ne_of_lt hmn),
        norm_zero, one_div, ne_eq, inv_eq_zero, ← cast_sub (le_of_lt hmn), cast_eq_zero,
        Nat.sub_eq_zero_iff_le]
      exact ⟨Eq.refl _, not_le_of_gt hmn⟩
    · rw [if_neg hmn]
  · infer_instance

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
n : ℕ
⊢ spectralValueTerms P n ≤ 1

Tactic:
spectralValueTerms

Goal state after:
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
n : ℕ
⊢ (if n < P.natDegree then ‖P.coeff n‖ ^ (1 / (↑P.natDegree - ↑n)) else 0) ≤ 1
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
⊢ (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ > 0

Tactic:
simp only [gt_iff_lt, Finset.lt_min'_iff, Finset.mem_image, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      rintro a' ha'
      simp only [Finset.mem_filter, Set.mem_toFinset, S] at ha'
      rw [norm_pos_iff, sub_ne_zero]
      exact ha'.2.symm

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 : ℝ
⊢ ∀ (x_1 : ℕ), (∀ (b : ℕ), x_1 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ r) → 0 ≤ r

Tactic:
m

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
r : ℝ
m : ℕ
⊢ (∀ (b : ℕ), m ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ r) → 0 ≤ r
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := ⋯
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := ⋯
⊢ ∀ n ≥ ?m.257, ‖u n‖ ≤ ?m.255 * (1 / 2) ^ n

Tactic:
rintro n (hn : n ≥ 1)

Goal state after:
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
n : ℕ
hn : n ≥ 1
⊢ ‖u n‖ ≤ ?m.255 * (1 / 2) ^ 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
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)
⊢ f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))

Tactic:
rcases neg_one_pow_eq_or L (card s - m) with h1 | hn1

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 ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))

case inr
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)
hn1 : (-1) ^ (s.card - m) = -1
⊢ f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: 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)
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y)

Tactic:
set b := 1 - a with hb

Goal state after:
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
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y)
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
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
y : L
h : y ∈ s
⊢ f y ≤ ⨆ σ, f (σ x)

Tactic:
obtain ⟨σ, hσ⟩ : ∃ σ : Gal(L/K), σ x = y := minpoly.exists_algEquiv_of_root'
        (Algebra.IsAlgebraic.isAlgebraic x) (aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C s h hs)
      rw [← hσ]
      apply Finite.le_ciSup _ σ

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
hna : IsNonarchimedean ⇑μ
x y : R
n : ℕ
⊢ smoothingSeminormSeq μ (x * y) n ≤ smoothingSeminormSeq μ x n * smoothingSeminormSeq μ y n

Tactic:
have hn : 0 ≤ 1 / (n : ℝ) := by simp only [one_div, inv_nonneg, cast_nonneg]

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
n : ℕ
hn : 0 ≤ 1 / ↑n
⊢ smoothingSeminormSeq μ (x * y) n ≤ smoothingSeminormSeq μ x n * smoothingSeminormSeq μ y n
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
⊢ ∀ {n : ℕ}, 1 ≤ n → smoothingFun μ (x ^ n) = smoothingFun μ x ^ n

Tactic:
m

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
m : ℕ
⊢ 1 ≤ m → smoothingFun μ (x ^ m) = smoothingFun μ x ^ m
Module: Mathlib.Analysis.Normed.Lp.Finsupp

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoEMetricSpace X
f g h : WithLp (↑p) (ι →₀ X)
this : 0 < p
s : Finset ι := f.ofLp.support ∪ g.ofLp.support ∪ h.ofLp.support
⊢ ((zipWith edist ⋯ f.ofLp h.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹ ≤
    ((zipWith edist ⋯ f.ofLp g.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹ +
      ((zipWith edist ⋯ g.ofLp h.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹

Tactic:
rw [sum_of_support_subset (s := s) _ (by grind [support_zipWith]) _ (by simp [*]),
      sum_of_support_subset (s := s) _ (by grind [support_zipWith]) _ (by simp [*]),
      sum_of_support_subset (s := s) _ (by grind [support_zipWith]) _ (by simp [*])]

Goal state after:
ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoEMetricSpace X
f g h : WithLp (↑p) (ι →₀ X)
this : 0 < p
s : Finset ι := f.ofLp.support ∪ g.ofLp.support ∪ h.ofLp.support
⊢ (∑ x ∈ s, (zipWith edist ⋯ f.ofLp h.ofLp) x ^ ↑p) ^ (↑p)⁻¹ ≤
    (∑ x ∈ s, (zipWith edist ⋯ f.ofLp g.ofLp) x ^ ↑p) ^ (↑p)⁻¹ +
      (∑ x ∈ s, (zipWith edist ⋯ g.ofLp h.ofLp) x ^ ↑p) ^ (↑p)⁻¹
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case neg
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 y : L
hx : ¬x = 0
⊢ (spectralAlgNorm K L) (x * y) = (spectralAlgNorm K L) x * (spectralAlgNorm K L) y

Tactic:
have hx' : spectralAlgNorm K L x ≠ 0 :=
      ne_of_gt (spectralNorm_zero_lt hx (Algebra.IsAlgebraic.isAlgebraic x))
    have hf1 : (spectralAlgNorm K L) 1 ≤ 1 := le_of_eq spectralAlgNorm_one
    set f : AlgebraNorm K L := algNormFromConst hf1 hx with hf
    have hf_pow : IsPowMul f := seminormFromConst_isPowMul hf1 hx' isPowMul_spectralNorm
    rw [← spectralNorm_unique hf_pow, hf]
    exact seminormFromConst_const_mul hf1 hx' isPowMul_spectralNorm _

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
E : Type u_2
F : Type u_4
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommMonoid F
inst✝ : Module R F
f : E →L[R] F
hf : f.IsInvertible
⊢ f.HasRightInverse

Tactic:
obtain ⟨e, rfl⟩ := hf
  exact e.hasRightInverse

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
f : ι → α → ℂ
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
i : ι
hi : ∀ x ∈ K, ‖f i x‖ ≤ u i
hi' : u i ≤ 1 / 2
x : α
hx : x ∈ K
⊢ 3 / 2 * ‖f i x‖ ≤ 3 / 2 * u i

Tactic:
simpa using hi x hx

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : α → Type u_3
F : α → Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
inst✝³ : (i : α) → NormedSpace 𝕜 (E i)
inst✝² : (i : α) → NormedAddCommGroup (F i)
inst✝¹ : (i : α) → NormedSpace 𝕜 (F i)
p✝ q r p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
T : (i : α) → E i →L[𝕜] F i
K : ℝ
hK : 0 ≤ K
hTK : ∀ (i : α), ‖T i‖ ≤ K
key : ∀ (i : α) (x : E i), ‖(T i) x‖ ≤ K * ‖x‖
x : ↥(lp E p)
⊢ ‖{ toFun := fun x ↦ ⟨fun i ↦ (T i) (↑x i), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } x‖ ≤ K * ‖x‖

Tactic:
← norm_toNorm

Goal state after:
α : Type u_1
𝕜 : Type u_2
E : α → Type u_3
F : α → Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
inst✝³ : (i : α) → NormedSpace 𝕜 (E i)
inst✝² : (i : α) → NormedAddCommGroup (F i)
inst✝¹ : (i : α) → NormedSpace 𝕜 (F i)
p✝ q r p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
T : (i : α) → E i →L[𝕜] F i
K : ℝ
hK : 0 ≤ K
hTK : ∀ (i : α), ‖T i‖ ≤ K
key : ∀ (i : α) (x : E i), ‖(T i) x‖ ≤ K * ‖x‖
x : ↥(lp E p)
⊢ ‖toNorm ({ toFun := fun x ↦ ⟨fun i ↦ (T i) (↑x i), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } x)‖ ≤ K * ‖x‖
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : α → Type u_3
F : α → Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
inst✝³ : (i : α) → NormedSpace 𝕜 (E i)
inst✝² : (i : α) → NormedAddCommGroup (F i)
inst✝¹ : (i : α) → NormedSpace 𝕜 (F i)
p✝ q r p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
T : (i : α) → E i →L[𝕜] F i
K : ℝ
hK : 0 ≤ K
hTK : ∀ (i : α), ‖T i‖ ≤ K
key : ∀ (i : α) (x : E i), ‖(T i) x‖ ≤ K * ‖x‖
x : ↥(lp E p)
| K * ‖toNorm x‖

Tactic:
← abs_of_nonneg hK,

Goal state after:
α : Type u_1
𝕜 : Type u_2
E : α → Type u_3
F : α → Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
inst✝³ : (i : α) → NormedSpace 𝕜 (E i)
inst✝² : (i : α) → NormedAddCommGroup (F i)
inst✝¹ : (i : α) → NormedSpace 𝕜 (F i)
p✝ q r p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
T : (i : α) → E i →L[𝕜] F i
K : ℝ
hK : 0 ≤ K
hTK : ∀ (i : α), ‖T i‖ ≤ K
key : ∀ (i : α) (x : E i), ‖(T i) x‖ ≤ K * ‖x‖
x : ↥(lp E p)
| |K| * ‖toNorm x‖
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝² : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : NormedField 𝕜
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : ℝ
x : 𝕜
⊢ ∀ (x_1 : (i : ι) → E i), (x, x_1) ∈ FreeAddMonoid.toList p → ‖x‖ * ∏ x, ‖x_1 x‖ = a → 0 ≤ a

Tactic:
m

Goal state after:
ι : Type u_1
inst✝² : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : NormedField 𝕜
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : ℝ
x : 𝕜
m : (i : ι) → E i
⊢ (x, m) ∈ FreeAddMonoid.toList p → ‖x‖ * ∏ x, ‖m x‖ = a → 0 ≤ a