mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: ⊢ ∃ x ∈ Ioo 1 2, IsMinOn Γ (Ioi 0) x

Tactic:
have ⟨x, hx, hmin⟩ := isCompact_Icc.exists_isMinOn (nonempty_Icc.mpr one_le_two) <|
    differentiableOn_Gamma_Ioi.continuousOn.mono <| by grind
  have ⟨h1, h2, h3half⟩ : Γ (3 / 2) < Γ 1 ∧ Γ (3 / 2) < Γ 2 ∧ Γ x ≤ Γ (3 / 2) := by
    simpa [Gamma_three_div_two_lt_one] using hmin <| by norm_num
  refine ⟨x, by grind, fun y _ ↦ ?_⟩
  obtain hy | hy | hy : y ∈ Ioc 0 1 ∨ y ∈ Icc 1 2 ∨ y ∈ Ici 2 := by grind
  · exact h3half.trans h1.le |>.trans <| Gamma_strictAntiOn_Ioc.antitoneOn hy (by simp) hy.right
  · exact hmin hy
  · exact h3half.trans h2.le |>.trans <| Gamma_strictMonoOn_Ici.monotoneOn (by simp) hy hy

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

Goal state before:
pp: ⊢ doublingGamma 1 = 1

Tactic:
by
  simp_rw [doublingGamma, Gamma_one_half_eq, add_halves (1 : ℝ), sub_self, Gamma_one, mul_one,
    rpow_zero, mul_one, div_self (sqrt_ne_zero'.mpr pi_pos)]

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
⊢ ∀ (x : ℝ), x = x / ↑n * ↑n

Tactic:
intro x

Goal state after:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ x = x / ↑n * ↑n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
x : ℝ
| ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)

Tactic:
2,

Goal state after:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
x : ℝ
| ↑x ^ (s - 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: 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))
⊢ ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))

Tactic:
intro x

Goal state after:
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))
x : ℝ
⊢ x ∈ Ioi 0 → Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: 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))
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun n ↦ (1 - x / ↑n) ^ n) = fun n ↦ (1 + -x / ↑n) ^ n

Tactic:
ext1 n

Goal state after:
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))
x : ℝ
hx : x ∈ Ioi 0
n : ℕ
⊢ (1 - x / ↑n) ^ n = (1 + -x / ↑n) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e'_3
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)))
⊢ (fun n ↦ ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) = fun n ↦ ∫ (a : ℝ) in Ioi 0, f n a

Tactic:
ext1 n

Goal state after:
case e'_3
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 : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1) = ∫ (a : ℝ) in Ioi 0, f n a
Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap

Goal state before:
pp: case right
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : SeminormedAddCommGroup V
inst✝⁵ : SeminormedAddCommGroup W
inst✝⁴ : SeminormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖(f.comp g).contLinear‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Tactic:
· calc
      ‖(f.comp g).contLinear‖ ≤ ‖f.contLinear‖ * ‖g.contLinear‖ :=
        (g.comp_contLinear f).symm ▸ f.contLinear.opNorm_comp_le _
      _ ≤ ‖f‖ * ‖g‖ := by grw [f.norm_contLinear_le, g.norm_contLinear_le]
      _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by rw [le_add_iff_nonneg_right]; apply norm_nonneg

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

Goal state before:
pp: z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ (fun n ↦ ↑n / (↑n + 1 - z)) = fun n ↦ ↑n / (↑n + (1 - z))

Tactic:
ext1 n

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

Goal state before:
pp: z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ (fun n ↦ (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ↑π) = fun n ↦
    ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)

Tactic:
ext1 n

Goal state after:
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
n : ℕ
⊢ (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ↑π =
    ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℝ
⊢ Complex.ofReal ∘ s.GammaSeq = (↑s).GammaSeq

Tactic:
ext1 n

Goal state after:
s : ℝ
n : ℕ
⊢ (Complex.ofReal ∘ s.GammaSeq) n = (↑s).GammaSeq n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
h1 : AnalyticOnNhd ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ (↑(Real.Gamma (2 * t)))⁻¹ * 2 ^ (↑(2 * t) - 1) * (↑√π)⁻¹ = (↑(Real.Gamma (2 * t)))⁻¹ * 2 ^ (↑(2 * t) - 1) / ↑√π

Tactic:
← div_eq_mul_inv

Goal state after:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ (↑(Real.Gamma (2 * t)))⁻¹ * 2 ^ (↑(2 * t) - 1) / ↑√π = (↑(Real.Gamma (2 * t)))⁻¹ * 2 ^ (↑(2 * t) - 1) / ↑√π
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁶ : Field 𝕜
inst✝¹⁵ : CharZero 𝕜
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Algebra 𝕜 R
inst✝¹¹ : Module 𝕜 M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : IsTopologicalRing R
inst✝² : IsTopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
⊢ (↑(n + 1).factorial)⁻¹ • (x ^ (n + 1)).snd = ((↑n.factorial)⁻¹ • x.fst ^ n) • x.snd

Tactic:
snd_pow_of_smul_comm _ _ hx,

Goal state after:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁶ : Field 𝕜
inst✝¹⁵ : CharZero 𝕜
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Algebra 𝕜 R
inst✝¹¹ : Module 𝕜 M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : IsTopologicalRing R
inst✝² : IsTopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
⊢ (↑(n + 1).factorial)⁻¹ • (n + 1) • x.fst ^ (n + 1).pred • x.snd = ((↑n.factorial)⁻¹ • x.fst ^ n) • x.snd
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : ProperSpace 𝕜
inst✝² : SeminormedRing F
inst✝¹ : NormedAlgebra 𝕜 F
inst✝ : NormOneClass F
x : F
⊢ ∃ z, IsMinOn (fun x_1 ↦ ‖x - (algebraMap 𝕜 F) x_1‖) univ z

Tactic:
have : Tendsto (‖x - algebraMap 𝕜 F ·‖) (cobounded 𝕜) atTop := by
    exact tendsto_norm_cobounded_atTop |>.comp <| tendsto_const_sub_cobounded x |>.comp <| by simp

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : ProperSpace 𝕜
inst✝² : SeminormedRing F
inst✝¹ : NormedAlgebra 𝕜 F
inst✝ : NormOneClass F
x : F
this : Tendsto (fun x_1 ↦ ‖x - (algebraMap 𝕜 F) x_1‖) (cobounded 𝕜) atTop
⊢ ∃ z, IsMinOn (fun x_1 ↦ ‖x - (algebraMap 𝕜 F) x_1‖) univ z
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case inl
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) Set.univ z
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hM : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 = M
⊢ ∃ z, ‖x - (algebraMap ℂ F) z‖ = 0

Tactic:
exact ⟨z, hM₀.symm⟩

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

Goal state before:
pp: case inl
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℝ F) x_1‖) univ u
hc₀ : x = (algebraMap ℝ F) u
⊢ ∃ z, IsMinOn (fun x_1 ↦ ‖φ x x_1‖) univ z

Tactic:
exact ⟨(u, 0), fun _ ↦ by simp [φ, hc₀, sq, Algebra.smul_def]⟩

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

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

Tactic:
refine ciSup_le (fun _ ↦ ?_)

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
x✝ : R
⊢ f x✝ / f x✝ ≤ 1
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: case h.h
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), B.norm (x * y) ≤ B.norm (B c.1 * B c.2) * B.norm x * B.norm y

Tactic:
intro x

Goal state after:
case h.h
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 : L
⊢ ∀ (y : L), B.norm (x * y) ≤ B.norm (B c.1 * B c.2) * B.norm x * B.norm y
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
⊢ 0 ∈ lowerBounds (Set.range fun n ↦ μ (x ^ ↑n) ^ (1 / ↑↑n))

Tactic:
rintro y ⟨n, rfl⟩
  positivity

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
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (smoothingSeminormSeq μ x n) (smoothingFun μ x) < ε

Tactic:
intro ε hε

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
⊢ ∃ N, ∀ n ≥ N, dist (smoothingSeminormSeq μ x n) (smoothingFun μ x) < ε
Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension

Goal state before:
pp: K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
σ : L ≃ₐ[K] L
⊢ IsPowMul ⇑(algNormOfAlgEquiv σ)

Tactic:
intro x

Goal state after:
K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
σ : L ≃ₐ[K] L
x : L
⊢ ∀ {n : ℕ}, 1 ≤ n → (algNormOfAlgEquiv σ) (x ^ n) = (algNormOfAlgEquiv σ) x ^ n
Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension

Goal state before:
pp: K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
σ : L ≃ₐ[K] L
⊢ IsNonarchimedean ⇑(algNormOfAlgEquiv σ)

Tactic:
intro x

Goal state after:
K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
σ : L ≃ₐ[K] L
x : L
⊢ ∀ (b : L), (algNormOfAlgEquiv σ) (x + b) ≤ max ((algNormOfAlgEquiv σ) x) ((algNormOfAlgEquiv σ) b)
Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension

Goal state before:
pp: K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
⊢ IsPowMul ⇑(invariantExtension K L)

Tactic:
intro x

Goal state after:
K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
x : L
⊢ ∀ {n : ℕ}, 1 ≤ n → (invariantExtension K L) (x ^ n) = (invariantExtension K L) x ^ n
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y ↦ f (x * y) / f y)
h0 : ¬f x = 0
heq : f 1 = 1
⊢ f x = f (x * 1) / f 1

Tactic:
rw [heq, mul_one, div_one]

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
inst✝ : IsDomain S
x y : S
h : IsIntegral K x
⊢ IsConjRoot K x y ↔ y ∈ (minpoly K x).aroots S

Tactic:
Polynomial.mem_aroots,

Goal state after:
K : Type u_2
S : Type u_4
inst✝³ : CommRing S
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : IsDomain S
x y : S
h : IsIntegral K x
⊢ IsConjRoot K x y ↔ minpoly K x ≠ 0 ∧ (Polynomial.aeval y) (minpoly K x) = 0
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
⊢ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))

Tactic:
← rpow_one (L + ε / 2)

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
⊢ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) ^ 1 * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
Module: Mathlib.Analysis.Normed.Group.CocompactMap

Goal state before:
pp: 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‖

Tactic:
intro x

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: 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

Tactic:
intro x

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‖
x : E
⊢ x ∈ (closedBall 0 r)ᶜ → x ∈ f ⁻¹' s
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 : ℕ → ℝ := 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
⊢ C * ‖v n‖ ≤ C * b n

Tactic:
by gcongr; exact (hv _ <| Nat.succ_le_iff.mp hn).le

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
hμ_lim : ∀ (U : Set ℝ), 1 ∈ U → IsOpen U → ∃ N, ∀ (n : ℕ), N ≤ n → μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n))) ∈ U
⊢ ∀ (ε : ℝ), 0 < ε → c ≤ 1 + ε

Tactic:
intro ε hε

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
hμ_lim : ∀ (U : Set ℝ), 1 ∈ U → IsOpen U → ∃ N, ∀ (n : ℕ), N ≤ n → μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n))) ∈ U
ε : ℝ
hε : 0 < ε
⊢ c ≤ 1 + ε
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 ⇑μ
⊢ IsNonarchimedean (smoothingFun μ)

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x : R
⊢ ∀ (b : R), smoothingFun μ (x + b) ≤ max (smoothingFun μ x) (smoothingFun μ b)
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 : ℕ → ℕ := ⋯
nu : ℕ → ℕ := ⋯
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 : ℝ := ⋯
hb : b = 1 - a
hb_lim : Tendsto ((fun n ↦ ↑(nu n) / ↑n) ∘ ψ) atTop (𝓝 b)
b_in : b ∈ Set.Icc 0 1
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx : limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
hy : limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ y ^ b
hxy :
  limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
⊢ ∀ ε > 0, smoothingFun μ (x + y) - ε ≤ max (smoothingFun μ x) (smoothingFun μ y)

Tactic:
intro ε hε

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
hb_lim : Tendsto ((fun n ↦ ↑(nu n) / ↑n) ∘ ψ) atTop (𝓝 b)
b_in : b ∈ Set.Icc 0 1
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx : limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
hy : limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ y ^ b
hxy :
  limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
⊢ 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
σ : Gal(L/K)
hσ : σ x = y
⊢ f y ≤ ⨆ σ, f (σ x)

Tactic:
← hσ

Goal state after:
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
σ : Gal(L/K)
hσ : σ x = y
⊢ f (σ x) ≤ ⨆ σ, f (σ x)
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
σ : Gal(L/K)
hσ : σ x = y
⊢ f (σ x) ≤ ⨆ σ, f (σ x)

Tactic:
apply Finite.le_ciSup _ σ

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
h_alg : Algebra.IsAlgebraic K L
⊢ IsPowMul (spectralNorm K L)

Tactic:
intro x

Goal state after:
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
x : L
⊢ ∀ {n : ℕ}, 1 ≤ n → spectralNorm K L (x ^ n) = spectralNorm K L x ^ n