mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: case neg
R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : ¬Summable fun n ↦ (expSeries ℚ R n) fun x_1 ↦ x.fst
⊢ ¬Summable fun n ↦ (expSeries ℚ (tsze R M) n) fun x_1 ↦ x

Tactic:
simp_rw [← fst_expSeries] at h

Goal state after:
case neg
R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : ¬Summable fun n ↦ ((expSeries ℚ (tsze R M) n) fun x_1 ↦ x).fst
⊢ ¬Summable fun n ↦ (expSeries ℚ (tsze R M) n) fun x_1 ↦ x
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝⁴ : NormedRing F
inst✝³ : NormOneClass F
inst✝² : NormMulClass F
inst✝¹ : NormedAlgebra ℂ F
inst✝ : Nontrivial F
⊢ Function.Bijective ⇑(ofId ℂ F)

Tactic:
refine ⟨FaithfulSMul.algebraMap_injective ℂ F, fun x ↦ ?_⟩

Goal state after:
F : Type u_1
inst✝⁴ : NormedRing F
inst✝³ : NormOneClass F
inst✝² : NormMulClass F
inst✝¹ : NormedAlgebra ℂ F
inst✝ : Nontrivial F
x : F
⊢ ∃ a, (ofId ℂ F) a = x
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝⁴ : NormedRing F
inst✝³ : NormOneClass F
inst✝² : NormMulClass F
inst✝¹ : NormedAlgebra ℂ F
inst✝ : Nontrivial F
x : F
z : ℂ
hz : ‖x - (algebraMap ℂ F) z‖ = 0
⊢ (ofId ℂ F) z = x

Tactic:
rwa [norm_eq_zero, sub_eq_zero, eq_comm, ← ofId_apply] at hz

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

Goal state before:
pp: case zero
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z : ℝ × ℝ), M ≤ ‖φ x z‖
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * 0)
⊢ M ^ 0 ≤ ‖(aeval x) p‖

Tactic:
simp_all

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case refine_2.inr.inr.inr.inr.inl
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
i₁ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₁₂ : i₁ ≠ i
h₁₃ : i₁ ≠ j
h₂₃ : i ≠ j
h₁ : dist (t.points i₁) (t.points i) = dist (t.points i₁) (t.points j)
h₂ : dist (t.points i₁) (t.points i) = dist (t.points i) (t.points j)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i)

Tactic:
h₂,

Goal state after:
case refine_2.inr.inr.inr.inr.inl
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
i₁ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₁₂ : i₁ ≠ i
h₁₃ : i₁ ≠ j
h₂₃ : i ≠ j
h₁ : dist (t.points i₁) (t.points i) = dist (t.points i₁) (t.points j)
h₂ : dist (t.points i₁) (t.points i) = dist (t.points i) (t.points j)
⊢ dist (t.points i) (t.points j) = dist (t.points i) (t.points j)
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case refine_2.inr.inr.inr.inr.inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
i₁ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₁₃ : i₁ ≠ i
h₁₂ : i₁ ≠ j
h₂₃ : j ≠ i
h₁ : dist (t.points i₁) (t.points j) = dist (t.points i₁) (t.points i)
h₂ : dist (t.points i₁) (t.points j) = dist (t.points j) (t.points i)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points j)

Tactic:
h₂,

Goal state after:
case refine_2.inr.inr.inr.inr.inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
i₁ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₁₃ : i₁ ≠ i
h₁₂ : i₁ ≠ j
h₂₃ : j ≠ i
h₁ : dist (t.points i₁) (t.points j) = dist (t.points i₁) (t.points i)
h₂ : dist (t.points i₁) (t.points j) = dist (t.points j) (t.points i)
⊢ dist (t.points i) (t.points j) = dist (t.points j) (t.points i)
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
HH : M * (1 + (‖φ x u - φ x w‖ / M) ^ n) = (M ^ n + ‖φ x u - φ x w‖ ^ n) / M ^ (n - 1)
⊢ ‖φ x u‖ ≤ M * (1 + (‖φ x u - φ x w‖ / M) ^ n)

Tactic:
rw [HH, le_div_iff₀ (by positivity)]

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ ∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m)

Tactic:
rcases max_cases 1 (‖x‖ ^ m) with (⟨hm, hx⟩ | ⟨hm, hx⟩) <;> rw [hm] <;>
  -- which we show by comparing the terms in the sum one by one
  gcongr with i hi

Goal state after:
case h
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ ‖x‖ ^ i ≤ 1

case ha
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ 1 ≤ ‖x‖

case hmn
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ i ≤ m
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
this : Tendsto (fun y ↦ ‖y.1‖ * c) (cobounded ℝ ×ˢ ⊤) atTop
y : ℝ × ℝ
hy : y ∈ {0}ᶜ ×ˢ Set.univ
⊢ ‖y.1 • x - (y.1 * (y.1⁻¹ * y.2)) • 1‖ = ‖y.1 • x - y.2 • 1‖

Tactic:
simp_all

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
n : ℕ
hn : 1 ≤ n
⊢ μ (x ^ n) = 0

Tactic:
apply le_antisymm _ (apply_nonneg μ _)

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
n : ℕ
hn : 1 ≤ n
⊢ μ (x ^ n) ≤ 0
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_4
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
k : K
y : L
⊢ B.norm ((algebraMap K L) k * y) = B.norm ((algebraMap K L) k) * B.norm y

Tactic:
norm_extends hBi,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
k : K
y : L
⊢ B.norm ((algebraMap K L) k * y) = ‖k‖ * B.norm y
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf : f 0 = 0
n : ℕ
⊢ 0 = 0 n

Tactic:
Pi.zero_apply

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf : f 0 = 0
n : ℕ
⊢ 0 = 0
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ Tendsto (fun n ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))

Tactic:
apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).comp
      (tendsto_atTop_atTop_of_monotone add_left_mono _)

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ ∀ (b : ℕ), ∃ a, b ≤ a + 1
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✝ : Algebra.IsAlgebraic 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'‖
C : Type u_1 := AlgebraicClosure K
this✝ : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst✝ : Algebra L C := iL.toAlgebra
⊢ x ∈ K⟮y⟯

Tactic:
let : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C

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✝ : Algebra.IsAlgebraic 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'‖
C : Type u_1 := AlgebraicClosure K
this✝¹ : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this✝ : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst✝ : Algebra L C := iL.toAlgebra
this : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
⊢ x ∈ K⟮y⟯
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case neg
R : Type u_1
inst✝ : SeminormedRing R
p : R[X]
n : ℕ
h : ¬n < p.natDegree
⊢ 0 ≤ 0

Tactic:
· exact le_refl _

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
n : ℕ
h✝ : n = 0
⊢ ‖r‖ ≤ ‖r‖

pp: case neg
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
n : ℕ
h✝ : ¬n = 0
⊢ 0 ≤ ‖r‖

Tactic:
· exact le_refl _

Goal state after:
case neg
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
n : ℕ
h✝ : ¬n = 0
⊢ 0 ≤ ‖r‖
Module: Mathlib.Analysis.Normed.Group.CocompactMap

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

Tactic:
specialize h (Metric.closedBall 0 ε)ᶜ (mem_cocompact_of_closedBall_compl_subset 0 ⟨ε, rfl.subset⟩)

Goal state after:
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, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
Module: Mathlib.Analysis.Normed.Group.CocompactMap

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

Tactic:
simp_all

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : n = 0
⊢ ↑(mu μ hn n) / ↑n ≤ 1

Tactic:
rw [hn0, cast_zero, div_zero]; exact zero_le_one

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
⊢ BddAbove (Set.range fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : 1 < μ x
⊢ BddAbove (Set.range fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Tactic:
· use 1
    simp only [mem_upperBounds, Set.mem_range, forall_exists_index]
    rintro _ n rfl
    apply le_trans (rpow_le_rpow (apply_nonneg _ _) (map_pow_le_pow' hμ1 _ _) (hψ n))
    rw [← rpow_natCast, ← rpow_mul (apply_nonneg _ _), mul_one_div]
    exact rpow_le_one (apply_nonneg _ _) hx (div_nonneg (cast_nonneg _) (cast_nonneg _))

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : 1 < μ x
⊢ BddAbove (Set.range fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))
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
x : L
hx : x ∈ s
hx0 : (aeval x) p = 0
⊢ f x ≤ spectralValue p

Tactic:
exact norm_root_le_spectralValue hf_pm hf_na
        (monic_of_monic_mapAlg (hp ▸ monic_multisetProd_X_sub_C s)) hx0

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
E : Type u_4
inst✝³ : Field E
inst✝² : Algebra K E
inst✝¹ : Algebra E L
inst✝ : IsScalarTower K E L
x : E
⊢ spectralNorm K E x = spectralNorm K L ((algebraMap E L) x)

Tactic:
have hx : minpoly K (algebraMap E L x) = minpoly K x :=
    minpoly.algebraMap_eq (algebraMap E L).injective x
  simp only [spectralNorm, hx]

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

Tactic:
have hf_pow : IsPowMul f := (Classical.choose_spec
    (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hna)).1

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 ⋯
hf_pow : IsPowMul ⇑f
⊢ 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
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 L ((algebraMap (↥K⟮y⟯) L) (k • g)) =
    ↑‖k‖₊ *
      spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
        ((algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g)

Tactic:
← spectralNorm.eq_of_normalClosure (k • g) rfl,

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⟯)))
      ((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)
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 : WithLp (↑p) (ι →₀ X)
⊢ ((zipWith edist ⋯ f.ofLp f.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹ = 0

Tactic:
by
    have : 0 < p := zero_lt_one.trans_le Fact.out
    simp [sum, *]

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 : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : μ x = 0
⊢ μ (x ^ n) = 0

Tactic:
apply le_antisymm _ (apply_nonneg μ _)

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : μ x = 0
⊢ μ (x ^ n) ≤ 0
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝¹² : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E'
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module R E'
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace F'
inst✝¹ : AddCommMonoid F'
inst✝ : Module R F'
f : E →L[R] F
g : E' →L[R] F'
hf : f.HasLeftInverse
hg : g.HasLeftInverse
⊢ (f.prodMap g).HasLeftInverse

Tactic:
by
  obtain ⟨finv, hfinv⟩ := hf
  obtain ⟨ginv, hginv⟩ := hg
  use finv.prodMap ginv
  simp [hfinv, hginv]

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

Goal state before:
pp: R : Type u_1
inst✝¹² : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E'
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module R E'
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace F'
inst✝¹ : AddCommMonoid F'
inst✝ : Module R F'
f : E →L[R] F
g : E' →L[R] F'
hf : f.HasRightInverse
hg : g.HasRightInverse
⊢ (f.prodMap g).HasRightInverse

Tactic:
by
  obtain ⟨finv, hfinv⟩ := hf
  obtain ⟨ginv, hginv⟩ := hg
  use finv.prodMap ginv
  simp [hfinv, hginv]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁶] ↑A
inst✝ : A.CoFG
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝³] ↑(↑u).range ↔
    IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed[inst✝³] ↑(↑(u.domRestrict A)).range

Tactic:
set N : Submodule 𝕜 E := A ⊓ u.ker

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁶] ↑A
inst✝ : A.CoFG
N : Submodule 𝕜 E := A ⊓ (↑u).ker
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝³] ↑(↑u).range ↔
    IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed[inst✝³] ↑(↑(u.domRestrict A)).range
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case pos
δ ε x : ℝ
⊢ HasDerivAt (gronwallBound δ 0 ε) (0 * gronwallBound δ 0 ε x + ε) x

Tactic:
simp only [gronwallBound_K0, zero_mul, zero_add]

Goal state after:
case pos
δ ε x : ℝ
⊢ HasDerivAt (fun x ↦ δ + ε * x) ε x
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
inst✝ : CompleteSpace E
⊢ IsComplete (range fun α ↦ toContinuousMap α)

Tactic:
apply IsClosed.isComplete

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
inst✝ : CompleteSpace E
⊢ IsClosed (range fun α ↦ toContinuousMap α)
Module: Mathlib.Analysis.PSeriesComplex

Goal state before:
pp: p : ℂ
⊢ (Summable fun n ↦ 1 / ↑n ^ p) ↔ 1 < p.re

Tactic:
← Real.summable_one_div_nat_rpow,

Goal state after:
p : ℂ
⊢ (Summable fun n ↦ 1 / ↑n ^ p) ↔ Summable fun n ↦ 1 / ↑n ^ p.re
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : P = 0
⊢ (fun x ↦ eval x P) =O[atTop] fun x ↦ eval x Q

pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : ¬P = 0
⊢ (fun x ↦ eval x P) =O[atTop] fun x ↦ eval x Q

Tactic:
· simpa [hp] using isBigO_zero Q.eval atTop

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : ¬P = 0
⊢ (fun x ↦ eval x P) =O[atTop] fun x ↦ eval x Q
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
t : ℝ
ht : t ∈ Icc tmin tmax
this : Fact (t ∈ Icc tmin tmax)
⊢ HasDerivWithinAt (fun x ↦ ∫ (τ : ℝ) in t₀..x, f τ (α τ)) (f t (α t)) (Icc tmin tmax) t

Tactic:
apply intervalIntegral.integral_hasDerivWithinAt_right _ -- need `CompleteSpace E` and `Icc`
    (continuousOn_comp hf hα hmem |>.stronglyMeasurableAtFilter_nhdsWithin measurableSet_Icc t)
    (continuousOn_comp hf hα hmem _ ht)

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
t : ℝ
ht : t ∈ Icc tmin tmax
this : Fact (t ∈ Icc tmin tmax)
⊢ IntervalIntegrable (fun t ↦ f t (α t)) volume t₀ t
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case neg
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝ : ZeroHomClass F R ℝ
h_supp : ¬p.support.Nonempty
⊢ ∃ i, gaussNorm v c p = v (p.coeff i) * c ^ i

Tactic:
simp_all

Goal state after: