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
⊢ (∑' (n : ℕ), (expSeries ℚ (tsze R M) n) fun x_1 ↦ x) = inl 0 + 0

Tactic:
inl_zero,

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 ℚ R n) fun x_1 ↦ x.fst
⊢ (∑' (n : ℕ), (expSeries ℚ (tsze R M) n) fun x_1 ↦ x) = 0 + 0
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ ‖x‖₊ = ‖x.fst‖₊ + ‖x.snd‖₊

Tactic:
by
  ext; simp [norm_def]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
f_mul : 1 ≤ c * f 1
hx : 0 < f x
f_nonneg : 0 ≤ f 1
h1 : f 1 = 0
⊢ 0 ≤ c

pp: case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
f_mul : 1 ≤ c * f 1
hx : 0 < f x
f_nonneg : 0 ≤ f 1
h1 : 0 < f 1
⊢ 0 ≤ c

Tactic:
· linarith [show (1 : ℝ) ≤ 0 by simpa [h1] using f_mul]

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
f_mul : 1 ≤ c * f 1
hx : 0 < f x
f_nonneg : 0 ≤ f 1
h1 : 0 < f 1
⊢ 0 ≤ c
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst✝ : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
⊢ liminf (u * v) f ≤ limsup u f * liminf v f

Tactic:
by
  have h := isCoboundedUnder_ge_mul_of_nonneg h₁ h₂ h₃ h₄
  have h' := isBoundedUnder_of_eventually_ge (a := 0)
    <| (h₁.and h₃).mono fun x ⟨u_0, v_0⟩ ↦ mul_nonneg u_0 v_0
  refine le_mul_of_forall_lt₀ fun a a_u b b_v ↦ (liminf_le_iff h h').2 fun c c_ab ↦ ?_
  refine ((frequently_lt_of_liminf_lt h₄ b_v).and_eventually ((eventually_lt_of_limsup_lt a_u).and
    (h₁.and h₃))).mono fun x ⟨x_v, x_u, u_0, v_0⟩ ↦ ?_
  exact (mul_le_mul x_u.le x_v.le v_0 (u_0.trans x_u.le)).trans_lt c_ab

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : 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, IsPowMul ⇑f ∧ (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) ∧ IsNonarchimedean ⇑f

Tactic:
set f := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg

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
⊢ ∃ f, IsPowMul ⇑f ∧ (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) ∧ IsNonarchimedean ⇑f
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 y : R
hlim : Tendsto (fun n ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))
n : ℕ
⊢ f (x * y * c ^ (2 * n)) / f c ^ (2 * n) ≤ f (x * c ^ n) * f (y * c ^ n) / (f c ^ n * f c ^ n)

Tactic:
← pow_add,

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 y : R
hlim : Tendsto (fun n ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))
n : ℕ
⊢ f (x * y * c ^ (2 * n)) / f c ^ (2 * n) ≤ f (x * c ^ n) * f (y * c ^ n) / f c ^ (n + n)
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⟯
this✝ : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : z ∈ K⟮y⟯ ↔ z ∈ ⊥
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : σ z' = z
⊢ False

Tactic:
apply_fun σ.symm at hσ

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
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : z ∈ K⟮y⟯ ↔ z ∈ ⊥
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : σ.symm (σ z') = σ.symm z
⊢ False
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) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
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
h1 : (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
h2 : μ (x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ (μ x ^ (n % ↑m1)) ^ (1 / ↑n)
⊢ L + ε = L + ε / 2 + ε / 2

Tactic:
add_assoc,

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) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
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
h1 : (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
h2 : μ (x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ (μ x ^ (n % ↑m1)) ^ (1 / ↑n)
⊢ L + ε = L + (ε / 2 + ε / 2)
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
⊢ μ (x ^ ↑1) ^ (1 / ↑↑1) ≤ μ x

Tactic:
PNat.one_coe,

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
⊢ μ (x ^ 1) ^ (1 / ↑1) ≤ μ x
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: case neg
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
this : CauchySeq s
⊢ ∃ g, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖

Tactic:
obtain ⟨g : G, hg⟩ := cauchySeq_tendsto_of_complete this

Goal state after:
case neg
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
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
⊢ ∃ g, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
inst✝ : IsUltrametricDist K
x : K
⊢ (invariantExtension K L) ((algebraMap K L) x) = ‖x‖

Tactic:
invariantExtension_extends K L x

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
inst✝ : IsUltrametricDist K
x : K
⊢ ‖x‖ = ‖x‖
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
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
x : L
E : Type v := id ↥K⟮x⟯
this✝ : Field E :=
  id
    (have this := inferInstance;
    this)
this : Module K E :=
  id
    (have this := inferInstance;
    this)
id1 : ↥K⟮x⟯ →ₗ[K] E := LinearMap.id
id2 : E →ₗ[K] ↥K⟮x⟯ := LinearMap.id
hs_norm : RingNorm E :=
  { toFun := fun y ↦ spectralNorm K L ↑(id2 y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n1 : NormedRing E := hs_norm.toNormedRing
N1 : NormedSpace K E :=
  { toSMul := DistribMulAction.toDistribSMul.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯, norm_smul_le := ⋯ }
hf_norm : RingNorm ↥K⟮x⟯ :=
  { toFun := fun y ↦ f ((algebraMap (↥K⟮x⟯) L) y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n2 : NormedRing ↥K⟮x⟯ := hf_norm.toNormedRing
N2 : NormedSpace K ↥K⟮x⟯ :=
  { toSMul := K⟮x⟯.algebra'.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯,
    zero_smul := ⋯, norm_smul_le := ⋯ }
hKx_fin : FiniteDimensional K ↥K⟮x⟯
⊢ ∃ C₁ C₂,
    ∃ (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x_3 : ↥K[x]), f ↑x_3 ≤ C₁ * (spectralAlgNorm K L) ↑x_3 ∧ (spectralAlgNorm K L) ↑x_3 ≤ C₂ * f ↑x_3

Tactic:
have : FiniteDimensional K E := hKx_fin

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
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
x : L
E : Type v := id ↥K⟮x⟯
this✝¹ : Field E :=
  id
    (have this := inferInstance;
    this)
this✝ : Module K E :=
  id
    (have this := inferInstance;
    this)
id1 : ↥K⟮x⟯ →ₗ[K] E := LinearMap.id
id2 : E →ₗ[K] ↥K⟮x⟯ := LinearMap.id
hs_norm : RingNorm E :=
  { toFun := fun y ↦ spectralNorm K L ↑(id2 y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n1 : NormedRing E := hs_norm.toNormedRing
N1 : NormedSpace K E :=
  { toSMul := DistribMulAction.toDistribSMul.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯, norm_smul_le := ⋯ }
hf_norm : RingNorm ↥K⟮x⟯ :=
  { toFun := fun y ↦ f ((algebraMap (↥K⟮x⟯) L) y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n2 : NormedRing ↥K⟮x⟯ := hf_norm.toNormedRing
N2 : NormedSpace K ↥K⟮x⟯ :=
  { toSMul := K⟮x⟯.algebra'.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯,
    zero_smul := ⋯, norm_smul_le := ⋯ }
hKx_fin : FiniteDimensional K ↥K⟮x⟯
this : FiniteDimensional K E
⊢ ∃ C₁ C₂,
    ∃ (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x_3 : ↥K[x]), f ↑x_3 ≤ C₁ * (spectralAlgNorm K L) ↑x_3 ∧ (spectralAlgNorm K L) ↑x_3 ≤ C₂ * f ↑x_3
Module: Mathlib.Analysis.Normed.Group.Tannery

Goal state before:
pp: case refine_2
α : 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
h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable fun x ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ ‖∑' (b : { x // x ∈ (↑T)ᶜ }), f n ↑b - ∑' (b : { x // x ∈ (↑T)ᶜ }), g ↑b‖ < ε / 3 + ε / 3

Tactic:
refine (norm_sub_le _ _).trans_lt (add_lt_add ?_ ?_)

Goal state after:
case refine_2.refine_1
α : 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
h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable fun x ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ ‖∑' (b : { x // x ∈ (↑T)ᶜ }), f n ↑b‖ < ε / 3

case refine_2.refine_2
α : 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
h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable fun x ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ ‖∑' (b : { x // x ∈ (↑T)ᶜ }), g ↑b‖ < ε / 3
Module: Mathlib.Analysis.Normed.Order.Hom.Ultra

Goal state before:
pp: case e'_3
F : Type u_1
α : Type u_2
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroup α
inst✝ : AddGroupSeminormClass F α ℝ
inst : Dist α
f : F
hna : IsNonarchimedean ⇑f
hd : inst = (toSeminormedAddGroup f).toDist
x y z : α
⊢ -x + z = -x + y + (-y + z)

Tactic:
add_assoc,

Goal state after:
case e'_3
F : Type u_1
α : Type u_2
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroup α
inst✝ : AddGroupSeminormClass F α ℝ
inst : Dist α
f : F
hna : IsNonarchimedean ⇑f
hd : inst = (toSeminormedAddGroup f).toDist
x y z : α
⊢ -x + z = -x + (y + (-y + z))
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: case neg
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this : ∀ (x : V →L[𝕜] V), adjoint ↑y ∘SL ↑y ∘SL adjoint x ∘SL ↑y.symm = adjoint x ∘SL adjoint ↑y
⊢ ∃ U, f = U.conjStarAlgEquiv

Tactic:
replace this (x : V →L[𝕜] V) : Commute x (adjoint y.toContinuousLinearMap ∘L y) := by
    simp_rw [commute_iff_eq, mul_def, ← comp_assoc, ← (adjoint_adjoint x ▸ this _), comp_assoc]
    simp

Goal state after:
case neg
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this : ∀ (x : V →L[𝕜] V), Commute x (adjoint ↑y ∘SL ↑y)
⊢ ∃ U, f = U.conjStarAlgEquiv
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
⊢ ∀ x ∈ Icc a b, f x ≤ gronwallBound δ K ε (x - a)

Tactic:
have H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a) := by
    intro x hx ε' (hε' : ε < ε')
    apply image_le_of_liminf_slope_right_lt_deriv_boundary hf hf'
    · rwa [sub_self, gronwallBound_x0]
    · exact fun x => hasDerivAt_gronwallBound_shift δ K ε' x a
    · grind
    · exact hx

Goal state after:
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a)
⊢ ∀ x ∈ Icc a b, f x ≤ gronwallBound δ K ε (x - a)
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha✝ : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
⊢ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 =
    (p.cauchyBound - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1

Tactic:
by
          congr 2
          have : ‖a‖₊ - 1 ≠ 0 := fun nh ↦ (ha.trans_le (tsub_eq_zero_iff_le.mp nh)).false
          field

Goal state after:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atBot] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

Tactic:
refine
    (P.isEquivalent_atBot_lead.symm.div Q.isEquivalent_atBot_lead.symm).symm.trans
      (EventuallyEq.isEquivalent ((eventually_lt_atBot 0).mono fun x hx => ?_))

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
x : 𝕜
hx : x < 0
⊢ ((fun x ↦ P.leadingCoeff * x ^ P.natDegree) / fun x ↦ Q.leadingCoeff * x ^ Q.natDegree) x =
    (fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)) x
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
inst✝ : NonnegHomClass F R ℝ
p : R[X]
h : p.support.Nonempty
hc : 0 ≤ c
⊢ 0 ≤ p.support.sup' h fun i ↦ v (p.coeff i) * c ^ i

Tactic:
simp only [Finset.le_sup'_iff, mem_support_iff]

Goal state after:
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
inst✝ : NonnegHomClass F R ℝ
p : R[X]
h : p.support.Nonempty
hc : 0 ≤ c
⊢ ∃ b, p.coeff b ≠ 0 ∧ 0 ≤ v (p.coeff b) * c ^ b
Module: Mathlib.Analysis.Polynomial.Norm

Goal state before:
pp: case neg
A : Type u_1
inst✝ : SeminormedRing A
n : ℕ
a : A
ha : ¬a = 0
⊢ ((monomial n) a).supNorm = ‖a‖

Tactic:
· simp [supNorm, gaussNorm, support_monomial n ha]

Goal state after:
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case pos
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∃ y, P.IsRoot y ∧ y ≤ x
⊢ 0 ≤ ↑↑(↑P.natDegree).negOnePow * eval x P

Tactic:
obtain ⟨y, hroot, hle⟩ := hroots'
    rw [eq_of_ge_of_le hle (hroots y hroot), hroot, mul_zero]

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
this : p.mahlerMeasure = rexp (log ‖p.leadingCoeff‖) * rexp (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
exp_log <| norm_pos_iff.mpr <| leadingCoeff_ne_zero.mpr hp

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
this : p.mahlerMeasure = ‖p.leadingCoeff‖ * rexp (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg.inl
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hlt : p.natDegree < n
⊢ ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mahlerMeasure

pp: case neg.inr
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
⊢ ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mahlerMeasure

Tactic:
· simp [coeff_eq_zero_of_natDegree_lt hlt, Nat.choose_eq_zero_of_lt hlt]

Goal state after:
case neg.inr
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
⊢ ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mahlerMeasure
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ (n * 3 + 2) = 2 ^ (n + 2 + 2 * n)

Tactic:
add_assoc,

Goal state after:
case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ (n * 3 + 2) = 2 ^ (n + (2 + 2 * n))
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ (2 + (n * 2 + n)) = 2 ^ (2 + 2 * n + n)

Tactic:
add_assoc,

Goal state after:
case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ (2 + (n * 2 + n)) = 2 ^ (2 + (2 * n + n))