mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x : R
⊢ (fun y ↦ f (-x * y) / f y) = fun y ↦ f (x * y) / f y

Tactic:
ext y

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x y : R
⊢ f (-x * y) / f y = f (x * y) / f y
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
⊢ x ∈ K⟮y⟯

Tactic:
have zsep : IsSeparable K⟮y⟯ z :=
      Field.isSeparable_sub (IsSeparable.tower_top K⟮y⟯ xsep) (isSeparable_algebraMap y')

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
⊢ x ∈ K⟮y⟯
Module: Mathlib.Analysis.Normed.Field.ProperSpace

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
hC : ∀ (n : ℕ), IsCompact (closedBall 0 (‖c‖ ^ n * r))
hTop : Tendsto (fun n ↦ ‖c‖ ^ n * r) atTop atTop
⊢ ProperSpace 𝕜

Tactic:
exact .of_seq_closedBall hTop (Eventually.of_forall hC)

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
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
n : ℕ
hn : n < p.natDegree
⊢ ‖p.coeff n‖ < f x ^ (p.natDegree - n)

Tactic:
have hexp : (‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ))) ^ (p.natDegree - n) =
          ‖p.coeff n‖ := by
        rw [← rpow_natCast, ← rpow_mul (norm_nonneg _), mul_comm, rpow_mul (norm_nonneg _),
          rpow_natCast, ← cast_sub (le_of_lt hn), one_div,
          pow_rpow_inv_natCast (norm_nonneg _) (_root_.ne_of_gt (tsub_pos_of_lt hn))]

Goal state after:
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
n : ℕ
hn : n < p.natDegree
hexp : (‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n))) ^ (p.natDegree - n) = ‖p.coeff n‖
⊢ ‖p.coeff n‖ < f x ^ (p.natDegree - n)
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
⊢ f x ≤ spectralValue p

Tactic:
by_cases hx0 : f x = 0
  · rw [hx0]; exact spectralValue_nonneg p
  · by_contra h_ge
    have hn_lt (n : ℕ) (hn : n < p.natDegree) : ‖p.coeff n‖ < f x ^ (p.natDegree - n) := by
      have hexp : (‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ))) ^ (p.natDegree - n) =
          ‖p.coeff n‖ := by
        rw [← rpow_natCast, ← rpow_mul (norm_nonneg _), mul_comm, rpow_mul (norm_nonneg _),
          rpow_natCast, ← cast_sub (le_of_lt hn), one_div,
          pow_rpow_inv_natCast (norm_nonneg _) (_root_.ne_of_gt (tsub_pos_of_lt hn))]
      have h_base : ‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ)) < f x := by
        rw [spectralValue, iSup, not_le, Set.Finite.csSup_lt_iff (spectralValueTerms_finite_range p)
          (Set.range_nonempty (spectralValueTerms p))] at h_ge
        have h_rg : ‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ)) ∈
          Set.range (spectralValueTerms p) := by use n; simp only [spectralValueTerms, if_pos hn]
        exact h_ge (‖p.coeff n‖₊ ^ (1 / (p.natDegree - n : ℝ))) h_rg
      rw [← hexp, ← rpow_natCast, ← rpow_natCast]
      gcongr
      exact cast_pos.mpr (tsub_pos_of_lt hn)
    have h_deg : 0 < p.natDegree := natDegree_pos_of_monic_of_aeval_eq_zero hp hx
    have h_lt : f ((Finset.range p.natDegree).sum fun i : ℕ ↦ p.coeff i • x ^ i) <
        f (x ^ p.natDegree) := by
      have hn' (n : ℕ) (hn : n < p.natDegree) : f (p.coeff n • x ^ n) < f (x ^ p.natDegree) := by
        by_cases hn0 : n = 0
        · rw [hn0, pow_zero, map_smul_eq_mul, hf_pm _ (succ_le_iff.mpr h_deg),
            ← Nat.sub_zero p.natDegree, ← hn0]
          exact (mul_le_of_le_one_right (norm_nonneg _) hf_pm.map_one_le_one).trans_lt (hn_lt n hn)
        · have : p.natDegree = p.natDegree - n + n := by rw [Nat.sub_add_cancel (le_of_lt hn)]
          rw [map_smul_eq_mul, hf_pm _ (succ_le_iff.mp (pos_iff_ne_zero.mpr hn0)),
            hf_pm _ (succ_le_iff.mpr h_deg), this, pow_add]
          gcongr
          exact hn_lt n hn
      set g := fun i : ℕ ↦ p.coeff i • x ^ i
      obtain ⟨m, hm_in, hm⟩ : ∃ (m : ℕ) (_ : 0 < p.natDegree → m < p.natDegree),
          f ((Finset.range p.natDegree).sum g) ≤ f (g m) := by
        obtain ⟨m, hm, h⟩ := IsNonarchimedean.finset_image_add (map_zero _) (apply_nonneg _) hf_na g
          (Finset.range p.natDegree)
        rw [Finset.nonempty_range_iff, ← zero_lt_iff, Finset.mem_range] at hm
        exact ⟨m, hm, h⟩
      exact lt_of_le_of_lt hm (hn' m (hm_in h_deg))
    have h0 : f 0 ≠ 0 := by
      have h_eq : f 0 = f (x ^ p.natDegree) := by
        rw [← hx, aeval_eq_sum_range, Finset.sum_range_succ, add_comm, hp.coeff_natDegree,
          one_smul, ← max_eq_left_of_lt h_lt]
        exact IsNonarchimedean.add_eq_max_of_ne hf_na (ne_of_gt h_lt)
      exact h_eq ▸ ne_of_gt (lt_of_le_of_lt (apply_nonneg _ _) h_lt)
    exact h0 (map_zero _)

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

Goal state before:
pp: K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h✝ : 0 < ↑p.natDegree - ↑m
hps : s.card = p.natDegree
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h : f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge : f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, f z ≤ f y
g : L → NNReal := fun x ↦ ⟨f x, ⋯⟩
h_card : p.natDegree - m = (Multiset.map g t).card
hx_le : ∀ x ∈ Multiset.map g t, x ≤ g y
this : (Multiset.map g t).prod ≤ g y ^ (p.natDegree - m)
⊢ (Multiset.map (⇑f) t).prod ≤ f y ^ (p.natDegree - m)

Tactic:
simpa [g, ← NNReal.coe_le_coe, NNReal.coe_pow, NNReal.coe_mk, NNReal.coe_multiset_prod,
          map_map, Function.comp_apply, NNReal.coe_mk] using! this

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
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
⊢ spectralNorm K L x ≤ ⨆ σ, f (σ x)

Tactic:
set p := minpoly K 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
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
⊢ spectralNorm K L x ≤ ⨆ σ, f (σ x)
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y : SemiNormedGrp
f : X ⟶ Y
⊢ cokernel.π f ≫ (explicitCokernelIso f).inv = explicitCokernelπ f

Tactic:
by
  simp [explicitCokernelπ, explicitCokernelIso]

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
⊢ ⋯.leftInverse = ↑f.symm

Tactic:
ext y

Goal state after:
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
y : F
⊢ ⋯.leftInverse y = ↑f.symm y
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x : L
⊢ spectralNorm K L x = ‖(minpoly K x).coeff 0‖ ^ (1 / ↑(minpoly K x).natDegree)

Tactic:
by
  set E := (mapAlg K L (minpoly K x)).SplittingField
  have hspl : Splits (mapAlg K E (minpoly K x)) :=
    IsSplittingField.IsScalarTower.splits (K := L) E (minpoly K x)
  have : Algebra.IsAlgebraic L E :=
    IsSplittingField.IsScalarTower.isAlgebraic E (mapAlg K L (minpoly K x))
  have : Algebra.IsAlgebraic K E := Algebra.IsAlgebraic.trans K L E
  rw [one_div, Real.eq_rpow_inv (spectralNorm_nonneg x) (norm_nonneg ((minpoly K x).coeff 0)),
    Real.rpow_natCast, @spectralNorm.eq_of_tower K _ E,
    ← @spectralNorm_extends K _ L _ _ ((minpoly K x).coeff 0),
    @spectralNorm.eq_of_tower K _ E _ _ L, ← spectralMulAlgNorm_def,
    ← spectralMulAlgNorm_def, Polynomial.coeff_zero_of_isScalarTower,
    hspl.coeff_zero_eq_prod_roots_of_monic _, map_mul, map_pow,
    map_neg_eq_map, map_one, one_pow, one_mul, spectralNorm_pow_natDegree_eq_prod_roots _ _ x]
  · simp [monic_mapAlg_iff, minpoly.monic (Algebra.IsAlgebraic.isAlgebraic x).isIntegral]
  · exact_mod_cast (minpoly.natDegree_pos (Algebra.IsIntegral.isIntegral x)).ne'

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
⊢ ⋯.rightInverse = ↑f.symm

Tactic:
ext y

Goal state after:
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
y : F
⊢ ⋯.rightInverse y = ↑f.symm y
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
A : ℝ
h : Real.exp (∑ i ∈ t, ‖f i‖) = A
IH : ‖∏ i ∈ t, (1 + f i) - 1‖ ≤ A - 1
⊢ (‖f x‖ + 1) * A ≤ Real.exp ‖f x‖ * A

Tactic:
exact mul_le_mul_of_nonneg_right (Real.add_one_le_exp _) (h ▸ Real.exp_nonneg _)

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
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
q : ℝ≥0∞
e : (i : ι) → E i
f : (i : ι) → F i
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (i : ι), ‖e i‖ ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
⊢ ∑ i ∈ s, ‖((B i) (e i)) (f i)‖ ^ q.toReal ≤ (K * C) ^ q.toReal * ∑ i ∈ s, ‖f i‖ ^ q.toReal

Tactic:
s.mul_sum

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
q : ℝ≥0∞
e : (i : ι) → E i
f : (i : ι) → F i
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (i : ι), ‖e i‖ ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
⊢ ∑ i ∈ s, ‖((B i) (e i)) (f i)‖ ^ q.toReal ≤ ∑ i ∈ s, (K * C) ^ q.toReal * ‖f i‖ ^ q.toReal
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr✝ : p.HolderTriple q r
e : (i : ι) → E i
f : (i : ι) → F i
hp : 0 < p.toReal
hq : 0 < q.toReal
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
hpqr : p.toReal.HolderTriple q.toReal r.toReal
hr : 0 < r.toReal
this : ∑ i ∈ s, (‖e i‖ * ‖f i‖) ^ r.toReal ≤ C ^ (r.toReal / p.toReal) * D ^ (r.toReal / q.toReal)
⊢ ∑ i ∈ s, ‖((B i) (e i)) (f i)‖ ^ r.toReal ≤ K ^ r.toReal * ∑ i ∈ s, (‖e i‖ * ‖f i‖) ^ r.toReal

Tactic:
s.mul_sum

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr✝ : p.HolderTriple q r
e : (i : ι) → E i
f : (i : ι) → F i
hp : 0 < p.toReal
hq : 0 < q.toReal
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
hpqr : p.toReal.HolderTriple q.toReal r.toReal
hr : 0 < r.toReal
this : ∑ i ∈ s, (‖e i‖ * ‖f i‖) ^ r.toReal ≤ C ^ (r.toReal / p.toReal) * D ^ (r.toReal / q.toReal)
⊢ ∑ i ∈ s, ‖((B i) (e i)) (f i)‖ ^ r.toReal ≤ ∑ i ∈ s, K ^ r.toReal * (‖e i‖ * ‖f i‖) ^ r.toReal
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 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
a : 𝕜
x : ⨂[𝕜] (i : ι), E i
⊢ ‖a • x‖ ≤ ‖a‖ * ‖x‖

Tactic:
by
  simp only [norm_def, Real.mul_iInf_of_nonneg (norm_nonneg _)]
  refine le_ciInf fun p ↦ ?_
  simpa [projectiveSeminormAux_smul] using
    ciInf_le_of_le (bddBelow_projectiveSemiNormAux _) ⟨_, lifts_smul p.2 a⟩ (le_refl _)

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →L[𝕜] W := (apply' W (RingHom.id 𝕜)) z ∘SL (↑f).toContinuousLinearMap ∘SL (smulRightL 𝕜 V V) v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
A : V →L[𝕜] V
x : V
⊢ T (A x) = (f A) (T x)

Tactic:
simp only [hT, ← mul_apply_eq_comp, ← map_mul]

Goal state after:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →L[𝕜] W := (apply' W (RingHom.id 𝕜)) z ∘SL (↑f).toContinuousLinearMap ∘SL (smulRightL 𝕜 V V) v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
A : V →L[𝕜] V
x : V
⊢ (f (smulRight v (A x))) z = (f (A * smulRight v x)) z
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : 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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he : adjoint ↑e ∘SL ↑e = α • ContinuousLinearMap.id 𝕜 V
he' : ↑e ∘SL adjoint ↑e = α • ContinuousLinearMap.id 𝕜 W
hαa : (starRingEnd 𝕜) α' = α'
⊢ ↑(↑(auxIsometry e hα hα2 he he' hαa)).symm = α'⁻¹ • ↑e.symm

Tactic:
ext y

Goal state after:
𝕜 : 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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he : adjoint ↑e ∘SL ↑e = α • ContinuousLinearMap.id 𝕜 V
he' : ↑e ∘SL adjoint ↑e = α • ContinuousLinearMap.id 𝕜 W
hαa : (starRingEnd 𝕜) α' = α'
y : W
⊢ ↑(↑(auxIsometry e hα hα2 he he' hαa)).symm y = (α'⁻¹ • ↑e.symm) y
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n ↦ (MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) y ≤
      edist ⟨x, hxs⟩ (MapsTo.restrict f s s hsf ⟨x, hxs⟩) * ↑K ^ n / (1 - ↑K)
⊢ ∃ y ∈ s,
    IsFixedPt f y ∧
      Tendsto (fun n ↦ f^[n] x) atTop (𝓝 y) ∧ ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)

Tactic:
refine ⟨y, y.2, Subtype.ext_iff.1 hfy, ?_, fun n ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n ↦ (MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) y ≤
      edist ⟨x, hxs⟩ (MapsTo.restrict f s s hsf ⟨x, hxs⟩) * ↑K ^ n / (1 - ↑K)
⊢ Tendsto (fun n ↦ f^[n] x) atTop (𝓝 ↑y)

case refine_2
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n ↦ (MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) y ≤
      edist ⟨x, hxs⟩ (MapsTo.restrict f s s hsf ⟨x, hxs⟩) * ↑K ^ n / (1 - ↑K)
n : ℕ
⊢ edist (f^[n] x) ↑y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
hy : IsFixedPt f y
⊢ dist x y ≤ dist x (f x) / (1 - ↑K)

Tactic:
by
  simpa only [hy.eq, dist_self, add_zero] using hf.dist_inequality x y

Goal state after:
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → E
K a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
ha : f a = 0
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ K * ‖f x‖
⊢ ∀ x ∈ Icc a b, f x = 0

Tactic:
intro x hx
  apply norm_le_zero_iff.mp
  calc ‖f x‖
    _ ≤ gronwallBound 0 K 0 (x - a) :=
      norm_le_gronwallBound_of_norm_deriv_right_le hf hf' (by simp [ha]) (by simpa using bound) _ hx
    _ = 0 := by rw [gronwallBound_ε0_δ0]

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : FunSpace t₀ x₀ r L
t : ↑(Icc tmin tmax)
⊢ IntervalIntegrable (fun t' ↦ f t' (α.compProj t')) volume ↑t₀ ↑t

Tactic:
by
  apply ContinuousOn.intervalIntegrable
  apply α.continuousOn_comp_compProj hf |>.mono
  exact uIcc_subset_Icc t₀.2 t.2

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

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

Tactic:
simp only [Polynomial.eval_eq_sum_range, sum_range_succ]

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x ↦ ∑ i ∈ range P.natDegree, P.coeff i * x ^ i + P.coeff P.natDegree * x ^ P.natDegree) ~[atTop] fun x ↦
    P.leadingCoeff * x ^ P.natDegree
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n : ℕ
⊢ dist α ((next hf hx)^[m]^[n] α) ≤
    ((∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ∑ i ∈ Finset.range n, ↑C ^ i) *
      dist α (next hf hx α)

Tactic:
by
  nth_rw 1 [← iterate_zero_apply (next hf hx) α]
  rw [Finset.mul_sum, Finset.sum_mul]
  apply dist_le_range_sum_of_dist_le (f := fun i ↦ (next hf hx)^[m]^[i] α)
  intro i hi
  rw [iterate_succ_apply]
  apply le_trans <| hm.dist_iterate_succ_le_geometric α i
  rw [mul_assoc, mul_comm ((C : ℝ) ^ i), ← mul_assoc]
  gcongr
  exact dist_iterate_next_le hf hx α m

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

Goal state before:
pp: P Q : ℤ[X]
mQ : Q.Monic
h : {a | eval a Q ∣ eval a P}.Infinite
R : ℤ[X] := ⋯
eqR : R + Q * (P /ₘ Q) = P
degR : R.degree < Q.degree
⊢ {x | R.IsRoot x}.Infinite

Tactic:
refine (h.sdiff (finite_abs_eval_le_of_degree_lt degR)).mono fun x mx ↦ ?_

Goal state after:
P Q : ℤ[X]
mQ : Q.Monic
h : {a | eval a Q ∣ eval a P}.Infinite
R : ℤ[X] := P %ₘ Q
eqR : R + Q * (P /ₘ Q) = P
degR : R.degree < Q.degree
x : ℤ
mx : x ∈ {a | eval a Q ∣ eval a P} \ {x | |eval x Q| ≤ |eval x R|}
⊢ x ∈ {x | R.IsRoot x}
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f✝ : ℝ → E → E
tmin tmax : ℝ
t₀✝ : ↑(Icc tmin tmax)
x₀✝ x : E
a✝ r✝ L✝ K✝ : ℝ≥0
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
⊢ t₀ ∈ Icc (t₀ - ε) (t₀ + ε)

Tactic:
by simp [le_of_lt hε]

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f✝ : ℝ → E → E
tmin tmax : ℝ
t₀✝ : ↑(Icc tmin tmax)
x₀✝ x : E
a✝ r✝ L✝ K✝ : ℝ≥0
inst✝ : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
ε : ℝ
hε : 0 < ε
a r L K : ℝ≥0
x✝ : 0 < r
t₀ : ℝ
⊢ t₀ ∈ Icc (t₀ - ε) (t₀ + ε)

Tactic:
by simp [le_of_lt hε]

Goal state after: