mathlib-initiative/mathlib-tactics huggingface dataset:
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
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
⊢ ∑ k ∈ range n, ‖u (k + 1)‖ + ‖u 0‖ ≤ ∑ k ∈ range n, C * ‖v (k + 1)‖ + ‖u 0‖

Tactic:
gcongr

Goal state after:
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
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)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
k : ℕ
a✝ : k ∈ range n
⊢ ‖u (k + 1)‖ ≤ C * ‖v (k + 1)‖
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
m : ℕ
hm : 1 ≤ m
h0 : ↑(ψ m) ≠ 0
⊢ (↑(ψ m) - ↑(mu (ψ m))) / ↑(ψ m) = ↑(nu (ψ m)) / ↑(ψ m)

Tactic:
cast_sub (hmu_le _)

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
m : ℕ
hm : 1 ≤ m
h0 : ↑(ψ m) ≠ 0
⊢ (↑(ψ m) - ↑(mu (ψ m))) / ↑(ψ m) = (↑(ψ m) - ↑(mu (ψ m))) / ↑(ψ m)
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
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
⊢ C * ‖h‖ + ∑ k ∈ range (n + 1), C * b k ≤ C * ‖h‖ + ε * ‖h‖

Tactic:
gcongr

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
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in : f.completion hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑g‖ < δ
g' : G
hgg' : f g' = f g
hfg : ‖g'‖ ≤ C' * ‖f g‖
mem_ker : g - g' ∈ f.ker
⊢ ‖f‖ * ‖hatg - ↑g‖ ≤ ‖f‖ * δ

Tactic:
gcongr

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
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in : f.completion hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑g‖ < δ
g' : G
hgg' : f g' = f g
hfg : ‖g'‖ ≤ C' * ‖f g‖
mem_ker : g - g' ∈ f.ker
this : ‖f g‖ ≤ ‖f‖ * δ
⊢ δ + C' * ‖f g‖ ≤ δ + C' * (‖f‖ * δ)

Tactic:
gcongr

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
⊢ spectralNorm K L 1 = 1

Tactic:
have h1 : (1 : L) = algebraMap K L 1 := by rw [map_one]

Goal state after:
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h1 : 1 = (algebraMap K L) 1
⊢ spectralNorm K L 1 = 1
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
n : ℕ
hn : 0 ≤ 1 / ↑n
⊢ μ (x ^ n * y ^ n) ^ (1 / ↑n) ≤ (μ (x ^ n) * μ (y ^ n)) ^ (1 / ↑n)

Tactic:
gcongr

Goal state after:
case h₁
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
n : ℕ
hn : 0 ≤ 1 / ↑n
⊢ μ (x ^ n * y ^ n) ≤ μ (x ^ n) * μ (y ^ n)
Module: Mathlib.Analysis.Normed.Lp.Finsupp

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoEMetricSpace X
f g h : WithLp (↑p) (ι →₀ X)
this : 0 < p
s : Finset ι := f.ofLp.support ∪ g.ofLp.support ∪ h.ofLp.support
⊢ (∑ x ∈ s, edist (f.ofLp x) (h.ofLp x) ^ ↑p) ^ (1 / ↑p) ≤
    (∑ i ∈ s, (edist (f.ofLp i) (g.ofLp i) + edist (g.ofLp i) (h.ofLp i)) ^ ↑p) ^ (1 / ↑p)

Tactic:
gcongr

Goal state after:
case h₁
ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoEMetricSpace X
f g h : WithLp (↑p) (ι →₀ X)
this : 0 < p
s : Finset ι := ⋯
x : ι
a✝ : x ∈ s
⊢ edist (f.ofLp x) (h.ofLp x) ≤ edist (f.ofLp x) (g.ofLp x) + edist (g.ofLp x) (h.ofLp 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 ∈ sphere 0 r
d : ℝ
hd✝ : d ∈ Ioi 0
hd : 0 < d
⊢ (fun x ↦
        have this := ⋯;
        (⟨r • ‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖ / r, ⋯⟩))
      ((fun x ↦ ⟨↑x.2 • ↑x.1, ⋯⟩) (⟨x, hx⟩, ⟨d, hd✝⟩)) =
    (⟨x, hx⟩, ⟨d, hd✝⟩)

Tactic:
mem_sphere_zero_iff_norm

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 ∈ sphere 0 r
hx : ‖x‖ = r
d : ℝ
hd✝ : d ∈ Ioi 0
hd : 0 < d
⊢ (fun x ↦
        have this := ⋯;
        (⟨r • ‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖ / r, ⋯⟩))
      ((fun x ↦ ⟨↑x.2 • ↑x.1, ⋯⟩) (⟨x, hx✝⟩, ⟨d, hd✝⟩)) =
    (⟨x, hx✝⟩, ⟨d, hd✝⟩)
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

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

Tactic:
use finv.prodMap ginv

Goal state after:
case h
R : Type u_1
inst✝¹² : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E'
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module R E'
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace F'
inst✝¹ : AddCommMonoid F'
inst✝ : Module R F'
f : E →L[R] F
g : E' →L[R] F'
finv : F →L[R] E
hfinv : LeftInverse ⇑finv ⇑f
ginv : F' →L[R] E'
hginv : LeftInverse ⇑ginv ⇑g
⊢ LeftInverse ⇑(finv.prodMap ginv) ⇑(f.prodMap g)
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

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

Tactic:
use finv.prodMap ginv

Goal state after:
case h
R : Type u_1
inst✝¹² : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E'
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module R E'
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace F'
inst✝¹ : AddCommMonoid F'
inst✝ : Module R F'
f : E →L[R] F
g : E' →L[R] F'
finv : F →L[R] E
hfinv : RightInverse ⇑finv ⇑f
ginv : F' →L[R] E'
hginv : RightInverse ⇑ginv ⇑g
⊢ RightInverse ⇑(finv.prodMap ginv) ⇑(f.prodMap g)
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 : ↥(lp E p)
⊢ ‖toNorm ({ toFun := fun x ↦ ⟨fun i ↦ (T i) (↑x i), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } x)‖ ≤ K * ‖x‖

Tactic:
conv_rhs => rw [← norm_toNorm, ← abs_of_nonneg hK, ← Real.norm_eq_abs, ← norm_smul]

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 : ↥(lp E p)
⊢ ‖toNorm ({ toFun := fun x ↦ ⟨fun i ↦ (T i) (↑x i), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } x)‖ ≤ ‖K • toNorm 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
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‖ * ‖e i‖ * ‖f i‖ ≤ K * C * ‖f i‖

Tactic:
gcongr

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.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)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
e : (i : ι) → E i
f : (i : ι) → F i
he : Memℓp e 0
⊢ Memℓp (fun i ↦ ((B i) (e i)) (f i)) 0

Tactic:
rw [memℓp_zero_iff] at he ⊢
  exact he.subset fun i hi h ↦ hi <| by simp [h]

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 : ι
hi : i ∈ s
⊢ ‖((B i) (e i)) (f i)‖ ^ q.toReal ≤ (K * C * ‖f i‖) ^ q.toReal

Tactic:
gcongr

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∞
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 : ι
hi : i ∈ s
⊢ ‖((B i) (e i)) (f i)‖ ≤ K * C * ‖f i‖
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)
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 : ι
hi : i ∈ s
⊢ ‖((B i) (e i)) (f i)‖ ^ r.toReal ≤ (K * ‖e i‖ * ‖f i‖) ^ r.toReal

Tactic:
gcongr

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)
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 : ι
hi : i ∈ s
⊢ ‖((B i) (e i)) (f i)‖ ≤ K * ‖e i‖ * ‖f i‖
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)
⊢ K ^ r.toReal * ∑ i ∈ s, (‖e i‖ * ‖f i‖) ^ r.toReal ≤
    K ^ r.toReal * (C ^ (r.toReal / p.toReal) * D ^ (r.toReal / q.toReal))

Tactic:
gcongr

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)
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x : ⨂[𝕜] (i : ι), E i
m : (i : ι) → E i
⊢ ∏ i, ‖(f i) (m i)‖ ≤ ∏ x, ‖f x‖ * ‖m x‖

Tactic:
gcongr

Goal state after:
case h1
ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x : ⨂[𝕜] (i : ι), E i
m : (i : ι) → E i
i : ι
a✝ : i ∈ Finset.univ
⊢ ‖(f i) (m i)‖ ≤ ‖f i‖ * ‖m i‖
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
⊢ (∑ i ∈ s, ‖e i‖ ^ p.toReal) ^ (r.toReal / p.toReal) * (∑ i ∈ s, ‖f i‖ ^ q.toReal) ^ (r.toReal / q.toReal) ≤
    C ^ (r.toReal / p.toReal) * D ^ (r.toReal / q.toReal)

Tactic:
gcongr

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)
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
⊢ ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C

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)
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
⊢ ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
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
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
G : Type (max (max uE u𝕜) uι) := (⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker
G' : Submodule 𝕜 F := (lift f.toMultilinearMap).range
e : ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) ≃ₗ[𝕜] ↥(lift f.toMultilinearMap).range :=
  (lift f.toMultilinearMap).quotKerEquivRange
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) :=
  lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)
hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i, ‖x i‖
f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) := f'₀.mkContinuous ‖f‖ hf'₀
hnorm : ‖f'‖ ≤ ‖f‖
heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x
h : ‖(lift f.toMultilinearMap) x‖ ≤ ‖f'‖ * injectiveSeminorm x
⊢ ‖f'‖ * injectiveSeminorm x ≤ ‖f‖ * injectiveSeminorm x

Tactic:
gcongr

Goal state after: