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

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
y : L
h_fin : FiniteDimensional K L
hn : Normal K L
inst✝ : IsUltrametricDist K
⊢ ∀ (r : L), (invariantExtension K L) (-r) = (invariantExtension K L) r

Tactic:
;

Goal state after:
R : Type u_1
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
y : L
h_fin : FiniteDimensional K L
hn : Normal K L
inst✝ : IsUltrametricDist K
⊢ ∀ (r : L), (invariantExtension K L) (-r) = (invariantExtension K L) r
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
⊢ spectralNorm K L ((algebraMap K L) x) = ‖x‖

Tactic:
spectralNorm_eq_invariantExtension,

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
⊢ (invariantExtension K L) ((algebraMap K L) x) = ‖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
h_fin : FiniteDimensional K L
hn : Normal K L
inst✝ : IsUltrametricDist K
x : K
⊢ spectralNorm K L ((algebraMap K L) x) = ‖x‖

Tactic:
by
  rw [spectralNorm_eq_invariantExtension, invariantExtension_extends K L x]

Goal state after:
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✝ : PseudoMetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ 0 ≤ (∑ a ∈ (zipWith dist ⋯ f.ofLp g.ofLp).support, dist (f.ofLp a) (g.ofLp a) ^ ↑p) ^ (↑p)⁻¹

Tactic:
;

Goal state after:
ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoMetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ 0 ≤ (∑ a ∈ (zipWith dist ⋯ f.ofLp g.ofLp).support, dist (f.ofLp a) (g.ofLp a) ^ ↑p) ^ (↑p)⁻¹
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✝ : MetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ 0 ≤ (∑ a ∈ (zipWith dist ⋯ f.ofLp g.ofLp).support, dist (f.ofLp a) (g.ofLp a) ^ ↑p) ^ (↑p)⁻¹

Tactic:
;

Goal state after:
ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : MetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ 0 ≤ (∑ a ∈ (zipWith dist ⋯ f.ofLp g.ofLp).support, dist (f.ofLp a) (g.ofLp a) ^ ↑p) ^ (↑p)⁻¹
Module: Mathlib.Analysis.Normed.Lp.LpEquiv

Goal state before:
pp: case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : ↥(lp E ∞)
⊢ ⨆ i, ‖(Equiv.lpPiLp f).ofLp i‖ = ⨆ i, ‖↑f i‖

Tactic:
;

Goal state after:
case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : ↥(lp E ∞)
⊢ ⨆ i, ‖(Equiv.lpPiLp f).ofLp i‖ = ⨆ i, ‖↑f i‖
Module: Mathlib.Analysis.Normed.Lp.LpEquiv

Goal state before:
pp: case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : ↥(lp E p)
h : 0 < p.toReal
⊢ (∑ i, ‖(Equiv.lpPiLp f).ofLp i‖ ^ p.toReal) ^ (1 / p.toReal) = (∑ b, ‖↑f b‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
;

Goal state after:
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : ↥(lp E p)
h : 0 < p.toReal
⊢ (∑ i, ‖(Equiv.lpPiLp f).ofLp i‖ ^ p.toReal) ^ (1 / p.toReal) = (∑ b, ‖↑f b‖ ^ p.toReal) ^ (1 / p.toReal)
Module: Mathlib.Analysis.Normed.Lp.LpEquiv

Goal state before:
pp: α : Type u_1
E : Type u_2
R : Type u_3
A : Type u_4
𝕜 : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : DiscreteTopology α
inst✝⁶ : NormedRing A
inst✝⁵ : NormOneClass A
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NonUnitalNormedRing R
f : ↥(lp (fun x ↦ E) ∞)
⊢ ⨆ x,
      ‖({ toFun := AddEquiv.lpBCF.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := AddEquiv.lpBCF.invFun, left_inv := ⋯,
              right_inv := ⋯ }
            f)
          x‖ =
    ⨆ i, ‖↑f i‖

Tactic:
;

Goal state after:
α : Type u_1
E : Type u_2
R : Type u_3
A : Type u_4
𝕜 : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : DiscreteTopology α
inst✝⁶ : NormedRing A
inst✝⁵ : NormOneClass A
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NonUnitalNormedRing R
f : ↥(lp (fun x ↦ E) ∞)
⊢ ⨆ x,
      ‖({ toFun := AddEquiv.lpBCF.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := AddEquiv.lpBCF.invFun, left_inv := ⋯,
              right_inv := ⋯ }
            f)
          x‖ =
    ⨆ i, ‖↑f i‖
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
K : Type u
inst✝³ : NontriviallyNormedField K
L : Type v
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
h1 : (spectralAlgNorm K L).toRingSeminorm 1 ≤ 1
x : L
hx : x ≠ 0
hx' : (spectralAlgNorm K L) x ≠ 0
k : K
y : L
h_mul :
  ∀ (y : L), spectralNorm K L ((algebraMap K L) k * y) = spectralNorm K L ((algebraMap K L) k) * spectralNorm K L y
⊢ spectralNorm K L ((algebraMap K L) k) = (spectralAlgNorm K L).toRingSeminorm ((algebraMap K L) k)

Tactic:
;

Goal state after:
R : Type u_1
K : Type u
inst✝³ : NontriviallyNormedField K
L : Type v
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
h1 : (spectralAlgNorm K L).toRingSeminorm 1 ≤ 1
x : L
hx : x ≠ 0
hx' : (spectralAlgNorm K L) x ≠ 0
k : K
y : L
h_mul :
  ∀ (y : L), spectralNorm K L ((algebraMap K L) k * y) = spectralNorm K L ((algebraMap K L) k) * spectralNorm K L y
⊢ spectralNorm K L ((algebraMap K L) k) = (spectralAlgNorm K L).toRingSeminorm ((algebraMap K L) k)
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
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✝ : SeminormedAddCommGroup L := seminormedAddCommGroup K L
r : K
x : L
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
by
      change spectralAlgNorm K L (r • x) ≤ ‖r‖ * spectralAlgNorm K L x
      exact le_of_eq (map_smul_eq_mul _ _ _)

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

Goal state before:
pp: R : Type u_1
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
h_fin : FiniteDimensional K L
⊢ CompleteSpace L

Tactic:
by
  let := (normedAddCommGroup K L)
  let := (normedSpace K L)
  exact FiniteDimensional.complete K L

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
hu : IsUltrametricDist K
inst✝⁶ : CompleteSpace K
x : L
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Algebra L E
inst✝² : IsScalarTower K L E
inst✝¹ : IsSplittingField L E ((mapAlg K L) (minpoly K x))
inst✝ : Algebra.IsAlgebraic K E
⊢ ((mapAlg K E) (minpoly K x)).Splits

Tactic:
exact IsSplittingField.IsScalarTower.splits (K := L) E (minpoly K x)

Goal state after:
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 : ↑{0}ᶜ
this : 0 < ‖↑x‖
⊢ 0 < ‖↑x‖ / r

Tactic:
;

Goal state after:
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}ᶜ
this : 0 < ‖↑x‖
⊢ 0 < ‖↑x‖ / r
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‖
⊢ ↑((fun x ↦ ⟨↑x.2 • ↑x.1, ⋯⟩)
        ((fun x ↦
            have this := ⋯;
            (⟨r • ‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖ / r, ⋯⟩))
          ⟨x, hx⟩)) =
    ↑⟨x, hx⟩

Tactic:
;

Goal state after:
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‖
⊢ ↑((fun x ↦ ⟨↑x.2 • ↑x.1, ⋯⟩)
        ((fun x ↦
            have this := ⋯;
            (⟨r • ‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖ / r, ⋯⟩))
          ⟨x, hx⟩)) =
    ↑⟨x, hx⟩
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‖
⊢ (‖x‖ / r * (r * ‖x‖⁻¹)) • x = x

Tactic:
;

Goal state after:
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‖
⊢ (‖x‖ / r * (r * ‖x‖⁻¹)) • x = x
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:
;

Goal state after:
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
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:
;

Goal state after:
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
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)
hf'' : (↑f).range.ClosedComplemented
⊢ (↑f).ker = ⊥

Tactic:
;

Goal state after:
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)
hf'' : (↑f).range.ClosedComplemented
⊢ (↑f).ker = ⊥
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
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceProd] fun x ↦ (⟨r • ‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖ / r, ⋯⟩)

Tactic:
fun_prop (disch := simp)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ ‖inclusionInDoubleDual 𝕜 E‖ ≤ 1

Tactic:
rw [inclusionInDoubleDual_norm_eq]
  exact ContinuousLinearMap.norm_id_le

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
hf : Summable fun i ↦ ‖f i‖
i : ι
| ‖1 + f i‖

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
hf : Summable fun i ↦ ‖f i‖
i : ι
| ‖1 + f i‖
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
hf : Summable fun i ↦ ‖f i‖
| Multipliable fun i ↦ ‖1 + f i‖

Tactic:
enter [1, i]; rw [← sub_add_cancel ‖1 + f i‖ 1, add_comm]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
hf : Summable fun i ↦ ‖f i‖
i : ι
| 1 + (‖1 + f i‖ - 1)
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set ↑(sphere 0 r)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x // x ∈ sphere 0 r }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x // x ∈ Ioi 0 }
hxU : ↑x ∈ U
this : Subtype.val ∘ ⇑(homeomorphSphereProd E r hr₀).symm '' V ×ˢ Ioi 0 ↓∩ U ∈ 𝓝 (↑(y, x).2 • ↑(y, x).1)
⊢ ∀ a ∈ Subtype.val ∘ ⇑(homeomorphSphereProd E r hr₀).symm '' V ×ˢ Ioi 0 ↓∩ U, a ∈ U • Subtype.val '' V

Tactic:
rintro _ ⟨⟨a, b⟩, ⟨ha, hb⟩, rfl⟩

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set ↑(sphere 0 r)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x // x ∈ sphere 0 r }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x // x ∈ Ioi 0 }
hxU : ↑x ∈ U
this : Subtype.val ∘ ⇑(homeomorphSphereProd E r hr₀).symm '' V ×ˢ Ioi 0 ↓∩ U ∈ 𝓝 (↑(y, x).2 • ↑(y, x).1)
a : ↑(sphere 0 r)
b : ↑(Ioi 0)
ha : (a, b).1 ∈ V
hb : (a, b).2 ∈ Ioi 0 ↓∩ U
⊢ (Subtype.val ∘ ⇑(homeomorphSphereProd E r hr₀).symm) (a, b) ∈ U • Subtype.val '' V
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:
;

Goal state after:
α : 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✝
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:
;

Goal state after:
α : 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✝
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: case h₁
ι : 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∞
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
e : (i : ι) → E i
f : (i : ι) → F i
he : Memℓp e ∞
hf : Memℓp f q
h : Nonempty ι
C : ℝ
hC : ∀ (a : ι), ‖e a‖ ≤ C
i : ι
hK_nonneg : 0 ≤ K
⊢ ‖B i‖ ≤ K

pp: case h₂
ι : 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∞
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
e : (i : ι) → E i
f : (i : ι) → F i
he : Memℓp e ∞
hf : Memℓp f q
h : Nonempty ι
C : ℝ
hC : ∀ (a : ι), ‖e a‖ ≤ C
i : ι
hK_nonneg : 0 ≤ K
⊢ ‖e i‖ ≤ C

Tactic:
;

Goal state after:
case h₁
ι : 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∞
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
e : (i : ι) → E i
f : (i : ι) → F i
he : Memℓp e ∞
hf : Memℓp f q
h : Nonempty ι
C : ℝ
hC : ∀ (a : ι), ‖e a‖ ≤ C
i : ι
hK_nonneg : 0 ≤ K
⊢ ‖B i‖ ≤ K

case h₂
ι : 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∞
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
e : (i : ι) → E i
f : (i : ι) → F i
he : Memℓp e ∞
hf : Memℓp f q
h : Nonempty ι
C : ℝ
hC : ∀ (a : ι), ‖e a‖ ≤ C
i : ι
hK_nonneg : 0 ≤ K
⊢ ‖e i‖ ≤ C
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:
;

Goal state after:
ι : 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✝
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:
;

Goal state after:
ι : 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✝
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:
;

Goal state after:
ι : 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✝
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:
;

Goal state after:
ι : 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✝