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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
h : spectralValue p = 0
n : ℕ
hn : n < p.natDegree
h0 : spectralValueTerms p n = 0
⊢ p.coeff n = 0

Tactic:
rw [spectralValueTerms_of_lt_natDegree _ hn,
    Real.rpow_eq_zero_iff_of_nonneg (norm_nonneg _)] at h0

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
h : spectralValue p = 0
n : ℕ
hn : n < p.natDegree
h0 : ‖p.coeff n‖ = 0 ∧ 1 / (↑p.natDegree - ↑n) ≠ 0
⊢ p.coeff n = 0
Module: Mathlib.Analysis.Normed.Group.CocompactMap

Goal state before:
pp: 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‖
⊢ Tendsto f (cocompact E) (cocompact F)

Tactic:
rw [tendsto_def]
  intro s hs
  rcases closedBall_compl_subset_of_mem_cocompact hs 0 with ⟨ε, hε⟩
  rcases h ε with ⟨r, hr⟩
  apply mem_cocompact_of_closedBall_compl_subset 0
  use r
  intro x hx
  simp only [Set.mem_compl_iff, Metric.mem_closedBall, dist_zero_right, not_le] at hx
  apply hε
  simp [hr x hx]

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

Goal state before:
pp: case neg
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
⊢ (if x ∈ s then f x else 0) ≤ spectralValue p

Tactic:
simp only [if_neg hx, spectralValue_nonneg _]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: case h
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
⊢ f 0 = 0 ∧ ‖0‖ ≤ (C + ε) * ‖0‖

Tactic:
simp

Goal state after:
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
⊢ 0 < 1 / 2

Tactic:
simp

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
⊢ limsup (fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a

Tactic:
have h_eq : (fun n : ℕ =>
        (μ (x ^ s (ψ n)) ^ (1 / (s (ψ n) : ℝ))) ^ ((s (ψ n) : ℝ) / (ψ n : ℝ))) =ᶠ[atTop]
        fun n : ℕ => μ (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ)) := by
      have h : (fun n : ℕ => (1 : ℝ) / (s (ψ n) : ℝ) * (s (ψ n) : ℝ)) =ᶠ[atTop] 1 := by
        apply Filter.EventuallyEq.div_mul_cancel_atTop
        exact (tendsto_natCast_atTop_atTop.comp hψ_mono.tendsto_atTop).num ha_pos hψ_lim
      simp_rw [← rpow_mul (apply_nonneg μ _), mul_div]
      exact EventuallyEq.comp₂ EventuallyEq.rfl HPow.hPow (h.div EventuallyEq.rfl)

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
h_eq :
  (fun n ↦ (μ (x ^ s (ψ n)) ^ (1 / ↑(s (ψ n)))) ^ (↑(s (ψ n)) / ↑(ψ n))) =ᶠ[atTop] fun n ↦
    μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))
⊢ limsup (fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
Module: Mathlib.Analysis.Normed.Group.HomCompletion

Goal state before:
pp: G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
⊢ ∀ (v : G), ‖↑v‖ ≤ 1 * ‖v‖

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.HomCompletion

Goal state before:
pp: G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
x : G
⊢ (f.completion.comp toCompl) x = (toCompl.comp f) x

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: M : SemiNormedGrp
r : M.carrier
⊢ (ConcreteCategory.hom (𝟙 M)) r = r

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: M N O : SemiNormedGrp
f : M ⟶ N
g : N ⟶ O
r : M.carrier
⊢ (ConcreteCategory.hom (f ≫ g)) r = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) r)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: M N : SemiNormedGrp
e : M ≅ N
r : M.carrier
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: M N : SemiNormedGrp
e : M ≅ N
s : N.carrier
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: M : SemiNormedGrp₁
r : M.carrier
⊢ ↑(Hom.hom (𝟙 M)) r = r

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: M N O : SemiNormedGrp₁
f : M ⟶ N
g : N ⟶ O
r : M.carrier
⊢ ↑(Hom.hom (f ≫ g)) r = ↑(Hom.hom g) (↑(Hom.hom f) r)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: M N : SemiNormedGrp₁
e : M ≅ N
r : M.carrier
⊢ ↑(Hom.hom (e.hom ≫ e.inv)) r = r

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: M N : SemiNormedGrp₁
e : M ≅ N
s : N.carrier
⊢ ↑(Hom.hom (e.inv ≫ e.hom)) s = s

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: V W : SemiNormedGrp₁
i : V ≅ W
⊢ Isometry ⇑↑(Hom.hom i.hom)

Tactic:
by
  change Isometry (⟨⟨i.hom, map_zero _⟩, fun _ _ => map_add _ _ _⟩ : V →+ W)
  refine AddMonoidHomClass.isometry_of_norm _ ?_
  intro v
  apply le_antisymm (i.hom.2 v)
  calc
    ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [← comp_apply, Iso.hom_inv_id, id_apply]
    _ ≤ ‖i.hom v‖ := i.inv.2 _

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion

Goal state before:
pp: V : SemiNormedGrp
v : V.carrier
⊢ ‖↑v‖ ≤ 1 * ‖v‖

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: case hom'
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
b : X.carrier
⊢ ↑(Hom.hom (f ≫ Cofork.π s)) b = 0

Tactic:
simp

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
⊢ ‖1‖ = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X✝ Y✝ : SemiNormedGrp₁
f : X✝ ⟶ Y✝
s : CokernelCofork f
x✝ : Y✝.carrier
b : X✝.carrier
⊢ ↑(Hom.hom (f ≫ Cofork.π s)) b = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y : SemiNormedGrp
f : X ⟶ Y
s : CokernelCofork f
b : X.carrier
⊢ (ConcreteCategory.hom (f ≫ Cofork.π s)) b = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y : SemiNormedGrp
f : X ⟶ Y
s : CokernelCofork f
x✝ : Y.carrier
b : X.carrier
⊢ (ConcreteCategory.hom (f ≫ Cofork.π s)) b = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: case e'_3
X Y : SemiNormedGrp
f : X ⟶ Y
e_1✝ : (X ⟶ explicitCokernel f) = ((parallelPair f 0).obj WalkingParallelPair.zero ⟶ (cokernelCocone f).pt)
⊢ 0 = (cokernelCocone f).ι.app WalkingParallelPair.zero

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: case e'_2
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
e_1✝ : ((parallelPair f 0).obj WalkingParallelPair.zero ⟶ (Cofork.ofπ g ⋯).pt) = (X ⟶ Z)
⊢ (cokernelCocone f).ι.app WalkingParallelPair.zero ≫ e = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
⊢ ∀ (v : M), ‖(↑mkAddMonoidHom).toFun v‖ ≤ 1 * ‖v‖

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
m : M
⊢ ‖normedMk m‖ ≤ 1 * ‖m‖

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
this : normedMk x = 0
⊢ mk x = normedMk x

Tactic:
simp

Goal state after:
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
e : K
⊢ e • 0 = 0

Tactic:
simp

Goal state after:
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
e : K
⊢ e • 0 = 0

Tactic:
simp

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

Goal state before:
pp: case neg
K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x y : L
hx : ¬x = 0
hx' : (spectralAlgNorm K L) x ≠ 0
hf1 : (spectralAlgNorm K L) 1 ≤ 1
f : AlgebraNorm K L := algNormFromConst hf1 hx
hf : f = algNormFromConst hf1 hx
hf_pow : IsPowMul ⇑f
⊢ f (x * y) = f x * f y

Tactic:
hf

Goal state after:
case neg
K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x y : L
hx : ¬x = 0
hx' : (spectralAlgNorm K L) x ≠ 0
hf1 : (spectralAlgNorm K L) 1 ≤ 1
f : AlgebraNorm K L := algNormFromConst hf1 hx
hf : f = algNormFromConst hf1 hx
hf_pow : IsPowMul ⇑f
⊢ (algNormFromConst hf1 hx) (x * y) = (algNormFromConst hf1 hx) x * (algNormFromConst hf1 hx) y
Module: Mathlib.Analysis.Normed.Group.Tannery

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

Tactic:
refine ((norm_tsum_le_tsum_norm (h_suma.subtype _)).trans ?_).trans_lt h1

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
⊢ ∑' (i : { x // x ∈ (↑T)ᶜ }), ‖f n ↑i‖ ≤ ∑' (k : ↑(↑T)ᶜ), bound ↑k
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : x ∈ {0}ᶜ
this : 0 < ‖x‖
⊢ 1 • x = x

Tactic:
simp

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
⊢ ↑f.symm ∘SL ↑f = ContinuousLinearMap.id R E

Tactic:
simp

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
y : F
⊢ ⋯.leftInverse y = ⋯.leftInverse (f (f.symm y))

Tactic:
simp

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : Semiring R
F : Type u_4
G : Type u_6
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
x : F
⊢ (fst R F G) ((inl R F G) x) = x

Tactic:
simp

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : Semiring R
F : Type u_4
G : Type u_6
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
x : G
⊢ (snd R F G) ((inr R F G) x) = x

Tactic:
simp

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

Goal state before:
pp: R : Type u_7
E : Type u_8
F : Type u_10
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →L[R] F
hf : f.HasLeftInverse
y : F
⊢ (f ∘SL hf.leftInverse) y ∈ (↑f).range

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: case funProp.discharger
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
⊢ ∀ (x : ↑{0}ᶜ), ‖↑x‖ ≠ 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_7
E : Type u_8
F : Type u_9
inst✝⁶ : NontriviallyNormedField R
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace R E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : CompleteSpace F
f : E →L[R] F
hf : Injective ⇑f
hf' : IsClosed (range ⇑f)
this : (↑f.rangeRestrict).ker = ⊥
p : F →L[R] ↥(↑f).range
hp : ∀ (x : ↥(↑f).range), p ↑x = x
x : E
⊢ f x ∈ (↑f).range

Tactic:
simp

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
⊢ ↑f ∘SL ↑f.symm = ContinuousLinearMap.id R F

Tactic:
simp

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : Semiring R
F : Type u_4
G : Type u_6
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
x : F
⊢ (fst R F G) (((ContinuousLinearMap.id R F).prod 0) x) = x

Tactic:
simp

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : Semiring R
F : Type u_4
G : Type u_6
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
x : G
⊢ (snd R F G) ((ContinuousLinearMap.prod 0 (ContinuousLinearMap.id R G)) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hfs : Summable f
⊢ Summable fun s ↦ ∏ i ∈ s, f i

Tactic:
refine summable_of_sum_le (c := Real.exp (∑' i, f i))
    (fun s ↦ Finset.prod_nonneg fun i _ ↦ hf i) fun T ↦ ?_

Goal state after:
ι : Type u_1
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hfs : Summable f
T : Finset (Finset ι)
⊢ ∑ x ∈ T, ∏ i ∈ x, f i ≤ Real.exp (∑' (i : ι), f i)
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: case empty
ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
⊢ ‖∏ i ∈ ∅, (1 + f i) - 1‖ ≤ Real.exp (∑ i ∈ ∅, ‖f i‖) - 1

Tactic:
simp

Goal state after:
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
hu : Summable fun n ↦ ‖f n‖
this : Summable fun x ↦ ‖1 + f x‖ - 1
⊢ ∀ (b : ι), Real.log (1 + (‖1 + f b‖ - 1)) = Real.log ‖1 + f b‖

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x y : ⨂[𝕜] (i : ι), E i
x✝ : ContinuousMultilinearMap 𝕜 E F
⊢ (((↑lift).flip (x + y) ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear).mkContinuous ‖x + y‖ ⋯) x✝ =
    (((↑lift).flip x ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear).mkContinuous ‖x‖ ⋯ +
        ((↑lift).flip y ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear).mkContinuous ‖y‖ ⋯)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a : 𝕜
x : ⨂[𝕜] (i : ι), E i
x✝ : ContinuousMultilinearMap 𝕜 E F
⊢ (((↑lift).flip (a • x) ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear).mkContinuous ‖a • x‖ ⋯) x✝ =
    ((RingHom.id 𝕜) a • ((↑lift).flip x ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear).mkContinuous ‖x‖ ⋯) x✝

Tactic:
simp

Goal state after:
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✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : ContinuousMultilinearMap 𝕜 E F
x✝ : ⨂[𝕜] (i : ι), E i
⊢ ((lift (f + g).toMultilinearMap).mkContinuous ‖f + g‖ ⋯) x✝ =
    ((lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯ + (lift g.toMultilinearMap).mkContinuous ‖g‖ ⋯) x✝

Tactic:
simp

Goal state after:
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✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a : 𝕜
f : ContinuousMultilinearMap 𝕜 E F
x✝ : ⨂[𝕜] (i : ι), E i
⊢ ((lift (a • f).toMultilinearMap).mkContinuous ‖a • f‖ ⋯) x✝ =
    ((RingHom.id 𝕜) a • (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯) x✝

Tactic:
simp

Goal state after: