awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedDivisionRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp : p ≠ 0
f : ↥(lp E p)
⊢ ‖HSMul.hSMul (α := 𝕜) 0 f‖ = norm.{u_1} (E := 𝕜) 0 * ‖f‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedDivisionRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
⊢ ‖c • f‖ = ‖c‖ * ‖f‖

Tactic:
le_antisymm (norm_const_smul_le hp c f) ?_

Premises used: le_antisymm, lp.norm_const_smul_le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedDivisionRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
inr : ‖c‖ * ‖f‖ ≤ ‖c • f‖
⊢ ‖c • f‖ = ‖c‖ * ‖f‖

Tactic:
refine le_antisymm (norm_const_smul_le hp c f) ?_

Premises used: le_antisymm, lp.norm_const_smul_le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedDivisionRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
⊢ ‖c‖ * ‖c⁻¹ • c • f‖ ≤ ‖c‖ * (‖c⁻¹‖ * ‖c • f‖)

Tactic:
have := mul_le_mul_of_nonneg_left (norm_const_smul_le hp c⁻¹ (c • f)) (norm_nonneg c)
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedDivisionRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
this : ‖c‖ * ‖c⁻¹ • c • f‖ ≤ ‖c‖ * (‖c⁻¹‖ * ‖c • f‖)
inr : ∀ (this : ‖c‖ * ‖f‖ ≤ ‖c‖ * (‖c⁻¹‖ * ‖c • f‖)), ‖c‖ * ‖f‖ ≤ ‖c • f‖
inr₁ : ∀ (this : ‖c‖ * ‖f‖ ≤ ‖c‖ * (‖c‖⁻¹ * ‖c • f‖)), ‖c‖ * ‖f‖ ≤ ‖c • f‖
inr₂ inr₃ inr₄ inr₅ : ∀ (this : ‖c‖ * ‖f‖ ≤ ‖c • f‖), ‖c‖ * ‖f‖ ≤ ‖c • f‖
⊢ ‖c‖ * ‖f‖ ≤ ‖c • f‖

Tactic:
rwa [inv_smul_smul₀ hc, norm_inv, mul_inv_cancel_left₀ (norm_ne_zero_iff.mpr hc)] at this

Premises used: Iff.mpr, mul_inv_cancel_left₀, inv_smul_smul₀, norm_inv, norm_ne_zero_iff
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
inl : ∀ (hf : Memℓp (E := E) f 0), Memℓp (E := E) (star f) 0
inr : ∀ (hf : Memℓp (E := E) f ∞), Memℓp (E := E) (star f) ∞
inr₁ : ∀ (hp : 0 < p.toReal), Memℓp (E := E) (star f) p
⊢ Memℓp (E := E) (star f) p

Tactic:
rcases p.trichotomy with (rfl | rfl | hp)

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f 0
inl : Set.Finite.{u_3} (α := α) {i : α | star f i ≠ 0}
⊢ Memℓp (E := E) (star f) 0

Tactic:
apply memℓp_zero

Premises used: memℓp_zero
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f 0
⊢ Set.Finite.{u_3} (α := α) {i : α | star f i ≠ 0}

Tactic:
simp [hf.finite_dsupport]

Premises used: Memℓp.finite_dsupport
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f ∞
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖star f i‖)

Tactic:
simpa using hf.bddAbove

Premises used: Memℓp.bddAbove
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
hp : 0 < p.toReal
inr : Summable (α := ℝ) fun (i : α) ↦ ‖star f i‖ ^ p.toReal
⊢ Memℓp (E := E) (star f) p

Tactic:
apply memℓp_gen

Premises used: memℓp_gen
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
hp : 0 < p.toReal
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖star f i‖ ^ p.toReal

Tactic:
simpa using hf.summable hp

Premises used: Memℓp.summable
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
f : (i : α) → E i
⊢ Memℓp (E := E) (star f) p ↔ Memℓp (E := E) f p

Tactic:
⟨fun h => star_star f ▸ Memℓp.star_mem h, Memℓp.star_mem⟩

Premises used: star_star, Memℓp.star_mem, Eq.rec, Iff.intro
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
f : ↥(lp E p)
⊢ (↑(star f) : (i : α) → E i) = star (↑f : (i : α) → E i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
f : ↥(lp E p)
i : α
⊢ (↑(star f) : (i : α) → E i) i = star ((↑f : (i : α) → E i) i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
x : ↥(lp E p)
⊢ star (star x) = x

Tactic:
simp [star]

Premises used: Star.star
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
hp : Fact (1 ≤ p)
f : ↥(lp E p)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (f : ↥(lp E 0)), ‖star f‖ = ‖f‖
inr : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f : ↥(lp E ∞)), ‖star f‖ = ‖f‖
inr₁ : ∀ (h : 0 < p.toReal), ‖star f‖ = ‖f‖
⊢ ‖star f‖ = ‖f‖

Tactic:
rcases p.trichotomy with (rfl | rfl | h)

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
f : ↥(lp E 0)
inl : False
⊢ ‖star f‖ = ‖f‖

Tactic:
exfalso
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
f : ↥(lp E 0)
⊢ ENNReal.toReal 1 ≤ ENNReal.toReal 0

Tactic:
have := ENNReal.toReal_mono ENNReal.zero_ne_top hp.elim
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
f : ↥(lp E 0)
this : ENNReal.toReal 1 ≤ ENNReal.toReal 0
⊢ False

Tactic:
norm_num at this
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f : ↥(lp E ∞)
⊢ ‖star f‖ = ‖f‖

Tactic:
simp only [lp.norm_eq_ciSup, lp.star_apply, norm_star]

Premises used: norm_star, lp.norm_eq_ciSup, lp.star_apply
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
hp : Fact (1 ≤ p)
f : ↥(lp E p)
h : 0 < p.toReal
⊢ ‖star f‖ = ‖f‖

Tactic:
simp only [lp.norm_eq_tsum_rpow h, lp.star_apply, norm_star]

Premises used: norm_star, lp.norm_eq_tsum_rpow, lp.star_apply
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp (E := B) f ∞
hg : Memℓp (E := B) g ∞
rw : BddAbove (α := ℝ) (Set.range fun (i : I) ↦ ‖(f * g) i‖)
⊢ Memℓp (E := B) (f * g) ∞

Tactic:
rw [memℓp_infty_iff]

Premises used: memℓp_infty_iff
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp (E := B) f ∞
hg : Memℓp (E := B) g ∞
obtain :
  ∀ (Cf : ℝ) (hCf : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖f i‖)) Cf) (Cg : ℝ)
    (hCg : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖g i‖)) Cg),
    BddAbove (α := ℝ) (Set.range fun (i : I) ↦ ‖(f * g) i‖)
⊢ BddAbove (α := ℝ) (Set.range fun (i : I) ↦ ‖(f * g) i‖)

Tactic:
obtain ⟨⟨Cf, hCf⟩, ⟨Cg, hCg⟩⟩ := hf.bddAbove, hg.bddAbove

Premises used: Memℓp.bddAbove
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp (E := B) f ∞
hg : Memℓp (E := B) g ∞
Cf : ℝ
hCf : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖f i‖)) Cf
Cg : ℝ
hCg : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖g i‖)) Cg
⊢ BddAbove (α := ℝ) (Set.range fun (i : I) ↦ ‖(f * g) i‖)

Tactic:
⟨Cf * Cg, ?_⟩

Premises used: HMul.hMul, BddAbove, Set.Nonempty, Exists.intro
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp (E := B) f ∞
hg : Memℓp (E := B) g ∞
Cf : ℝ
hCf : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖f i‖)) Cf
Cg : ℝ
hCg : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖g i‖)) Cg
refine : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖(f * g) i‖)) (Cf * Cg)
⊢ BddAbove (α := ℝ) (Set.range fun (i : I) ↦ ‖(f * g) i‖)

Tactic:
refine ⟨Cf * Cg, ?_⟩
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp (E := B) f ∞
hg : Memℓp (E := B) g ∞
Cf : ℝ
hCf : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖f i‖)) Cf
Cg : ℝ
hCg : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖g i‖)) Cg
i : I
⊢ ‖(f * g) i‖ ≤ ‖f i‖ * ‖g i‖

Tactic:
norm_mul_le (f i) (g i)

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp (E := B) f ∞
hg : Memℓp (E := B) g ∞
Cf : ℝ
hCf : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖f i‖)) Cf
Cg : ℝ
hCg : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖g i‖)) Cg
i : I
⊢ ‖f i‖ * ‖g i‖ ≤ Cf * Cg

Tactic:
mul_le_mul (hCf ⟨i, rfl⟩) (hCg ⟨i, rfl⟩) (norm_nonneg _)
        ((norm_nonneg _).trans (hCf ⟨i, rfl⟩))

Premises used: mul_le_mul, Exists.intro, LE.le.trans, norm_nonneg, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp (E := B) f ∞
hg : Memℓp (E := B) g ∞
Cf : ℝ
hCf : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖f i‖)) Cf
Cg : ℝ
hCg : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : I) ↦ ‖g i‖)) Cg
i : I
⊢ (fun (i : I) ↦ ‖(f * g) i‖) i ≤ Cf * Cg

Tactic:
calc
    ‖(f * g) i‖ ≤ ‖f i‖ * ‖g i‖ := norm_mul_le (f i) (g i)
    _ ≤ Cf * Cg :=
      mul_le_mul (hCf ⟨i, rfl⟩) (hCg ⟨i, rfl⟩) (norm_nonneg _)
        ((norm_nonneg _).trans (hCf ⟨i, rfl⟩))

Premises used: HMul.hMul, mul_le_mul, Exists.intro, LE.le.trans, norm_mul_le, norm_nonneg, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NonUnitalNormedRing (B i)
f g : ↥(lp B ∞)
⊢ (↑(f * g) : (i : I) → B i) = (↑f : (i : I) → B i) * (↑g : (i : I) → B i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NonUnitalNormedRing (B i)
f g : ↥(lp B ∞)
⊢ 0 ≤ ‖f‖ * ‖g‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NonUnitalNormedRing (B i)
𝕜 : Type u_7
inst_2 : NormedRing 𝕜
inst_3 : (i : I) → Module.{u_7, u_6} 𝕜 (B i)
inst_4 : ∀ (i : I), IsBoundedSMul.{u_7, u_6} 𝕜 (B i)
inst_5 : ∀ (i : I), IsScalarTower.{u_7, u_6, u_6} 𝕜 (B i) (B i)
⊢ IsScalarTower 𝕜 ↥(lp B ∞) ↥(lp B ∞)

Tactic:
⟨fun r f g => lp.ext <| smul_assoc (N := ∀ i, B i) (α := ∀ i, B i) r (⇑f) (⇑g)⟩

Premises used: smul_assoc, lp.ext, IsScalarTower.mk, Subtype.val
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NonUnitalNormedRing (B i)
𝕜 : Type u_7
inst_2 : NormedRing 𝕜
inst_3 : (i : I) → Module.{u_7, u_6} 𝕜 (B i)
inst_4 : ∀ (i : I), IsBoundedSMul.{u_7, u_6} 𝕜 (B i)
inst_5 : ∀ (i : I), SMulCommClass.{u_7, u_6, u_6} 𝕜 (B i) (B i)
⊢ SMulCommClass 𝕜 ↥(lp B ∞) ↥(lp B ∞)

Tactic:
⟨fun r f g => lp.ext <| smul_comm (N := ∀ i, B i) (α := ∀ i, B i) r (⇑f) (⇑g)⟩

Premises used: lp.ext, SMulCommClass.smul_comm, SMulCommClass.mk, Subtype.val
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NonUnitalNormedRing (B i)
inst_2 : (i : I) → StarRing (B i)
inst_3 : ∀ (i : I), NormedStarGroup.{u_6} (B i)
inst_4 : ∀ (i : I), CStarRing.{u_6} (B i)
f : ↥(lp B ∞)
rw : ‖f‖ ≤ √‖star f * f‖
⊢ ‖f‖ * ‖f‖ ≤ ‖star f * f‖

Tactic:
rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _)]

Premises used: Real.le_sqrt, sq, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NonUnitalNormedRing (B i)
inst_2 : (i : I) → StarRing (B i)
inst_3 : ∀ (i : I), NormedStarGroup.{u_6} (B i)
inst_4 : ∀ (i : I), CStarRing.{u_6} (B i)
f : ↥(lp B ∞)
⊢ ‖f‖ ≤ √‖star f * f‖

Tactic:
lp.norm_le_of_forall_le ‖star f * f‖.sqrt_nonneg fun i => ?_

Premises used: Norm.norm, HMul.hMul, lp.norm_le_of_forall_le, Real.sqrt_nonneg, Star.star
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NonUnitalNormedRing (B i)
inst_2 : (i : I) → StarRing (B i)
inst_3 : ∀ (i : I), NormedStarGroup.{u_6} (B i)
inst_4 : ∀ (i : I), CStarRing.{u_6} (B i)
f : ↥(lp B ∞)
refine : ∀ (i : I), ‖(↑f : (i : I) → B i) i‖ ≤ √‖star f * f‖
⊢ ‖f‖ ≤ √‖star f * f‖

Tactic:
refine lp.norm_le_of_forall_le ‖star f * f‖.sqrt_nonneg fun i => ?_

Premises used: Norm.norm, HMul.hMul, lp.norm_le_of_forall_le, Real.sqrt_nonneg, Star.star
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NonUnitalNormedRing (B i)
inst_2 : (i : I) → StarRing (B i)
inst_3 : ∀ (i : I), NormedStarGroup.{u_6} (B i)
inst_4 : ∀ (i : I), CStarRing.{u_6} (B i)
f : ↥(lp B ∞)
i : I
rw : ‖star ((↑f : (i : I) → B i) i) * (↑f : (i : I) → B i) i‖ ≤ ‖star f * f‖
⊢ ‖(↑f : (i : I) → B i) i‖ ≤ √‖star f * f‖

Tactic:
rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self]

Premises used: Real.le_sqrt, sq, CStarRing.norm_star_mul_self, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NonUnitalNormedRing (B i)
inst_2 : (i : I) → StarRing (B i)
inst_3 : ∀ (i : I), NormedStarGroup.{u_6} (B i)
inst_4 : ∀ (i : I), CStarRing.{u_6} (B i)
f : ↥(lp B ∞)
i : I
⊢ ‖star ((↑f : (i : I) → B i) i) * (↑f : (i : I) → B i) i‖ ≤ ‖star f * f‖

Tactic:
lp.norm_apply_le_norm ENNReal.top_ne_zero (star f * f) i

Premises used: lp.norm_apply_le_norm, ENNReal.ofNNReal, HMul.hMul, WithTop.some, ENNReal.top_ne_zero, Star.star
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NonUnitalNormedRing (B i)
inst_2 : (i : I) → StarRing (B i)
inst_3 : ∀ (i : I), NormedStarGroup.{u_6} (B i)
inst_4 : ∀ (i : I), CStarRing.{u_6} (B i)
f : ↥(lp B ∞)
i : I
⊢ ‖star ((↑f : (i : I) → B i) i) * (↑f : (i : I) → B i) i‖ ≤ ‖star f * f‖

Tactic:
exact lp.norm_apply_le_norm ENNReal.top_ne_zero (star f * f) i

Premises used: lp.norm_apply_le_norm, HMul.hMul, ENNReal.top_ne_zero, Star.star
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NormedRing (B i)
inst_1 : ∀ (i : I), NormOneClass.{u_6} (B i)
i : I
⊢ LE.le (α := ℝ) ((fun (i : I) ↦ norm.{u_6} (E := B i) (1 i)) i) 1

Tactic:
norm_one.le

Premises used: NormOneClass.norm_one, Eq.le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NormedRing (B i)
inst_1 : ∀ (i : I), NormOneClass.{u_6} (B i)
i : I
⊢ LE.le (α := ℝ) ((fun (i : I) ↦ norm.{u_6} (E := B i) (1 i)) i) 1

Tactic:
exact norm_one.le

Premises used: NormOneClass.norm_one, Eq.le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NormedRing (B i)
inst_1 : ∀ (i : I), NormOneClass.{u_6} (B i)
f : (i : I) → B i
hf : Memℓp (E := B) f ∞
n : ℕ
⊢ Memℓp (E := B) (f ^ n) ∞

Tactic:
(lpInftySubring B).pow_mem hf n

Premises used: Set.Mem, setOf, BddAbove, lpInftySubring, Set.Nonempty, Subring.pow_mem, Memℓp, ite
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NormedRing (B i)
inst_1 : ∀ (i : I), NormOneClass.{u_6} (B i)
n : ℕ
⊢ Memℓp (E := B) (↑n : (i : I) → B i) ∞

Tactic:
natCast_mem (lpInftySubring B) n

Premises used: Set.Mem, setOf, natCast_mem, BddAbove, lpInftySubring, Set.Nonempty, PreLp, Memℓp, ite
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NormedRing (B i)
inst_1 : ∀ (i : I), NormOneClass.{u_6} (B i)
z : ℤ
⊢ Memℓp (E := B) (↑z : (i : I) → B i) ∞

Tactic:
intCast_mem (lpInftySubring B) z

Premises used: intCast_mem, Set.Mem, setOf, BddAbove, lpInftySubring, Set.Nonempty, PreLp, Memℓp, ite
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NormedRing (B i)
inst_1 : ∀ (i : I), NormOneClass.{u_6} (B i)
⊢ Eq (α := (i : I) → B i) (↑1 : (i : I) → B i) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NormedRing (B i)
inst_1 : ∀ (i : I), NormOneClass.{u_6} (B i)
f : ↥(lp B ∞)
n : ℕ
⊢ (↑(f ^ n) : (i : I) → B i) = (↑f : (i : I) → B i) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NormedRing (B i)
inst_1 : ∀ (i : I), NormOneClass.{u_6} (B i)
n : ℕ
⊢ Eq (α := (i : I) → B i) (↑(↑n : ↥(lp B ∞)) : (i : I) → B i) (↑n : (i : I) → B i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
I : Type u_5
B : I → Type u_6
inst : (i : I) → NormedRing (B i)
inst_1 : ∀ (i : I), NormOneClass.{u_6} (B i)
z : ℤ
⊢ Eq (α := (i : I) → B i) (↑(↑z : ↥(lp B ∞)) : (i : I) → B i) (↑z : (i : I) → B i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst_1 : (i : I) → NormedRing (B i)
inst_2 : ∀ (i : I), NormOneClass.{u_6} (B i)
inst_3 : Nonempty I
simp_rw : Eq (α := ℝ) (⨆ (i : I), norm.{u_6} (E := B i) ((↑1 : (i : I) → B i) i)) 1
simp_rw₁ : Eq (α := ℝ) (⨆ (i : I), norm.{u_6} (E := B i) (1 i)) 1
simp_rw₂ : Eq (α := ℝ) (⨆ (i : I), norm.{u_6} (E := B i) 1) 1
simp_rw₃ : Eq (α := ℝ) (⨆ (i : I), 1) 1
⊢ norm (E := ↥(lp B ∞)) 1 = 1

Tactic:
simp_rw [lp.norm_eq_ciSup, infty_coeFn_one, Pi.one_apply, norm_one, ciSup_const]

Premises used: Pi.one_apply, NormOneClass.norm_one, lp.infty_coeFn_one, lp.norm_eq_ciSup, ciSup_const
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
I : Type u_5
B : I → Type u_6
inst : NormedField 𝕜
inst_1 : (i : I) → NormedRing (B i)
inst_2 : (i : I) → NormedAlgebra.{u_1, u_6} 𝕜 (B i)
inst_3 : ∀ (i : I), NormOneClass.{u_6} (B i)
k : 𝕜
rw : Memℓp (E := B) (HSMul.hSMul (β := (i : I) → B i) k 1) ∞
⊢ Memℓp (E := B) ((algebraMap 𝕜 ((i : I) → B i) : (a : 𝕜) → (i : I) → B i) k) ∞

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
I : Type u_5
B : I → Type u_6
inst : NormedField 𝕜
inst_1 : (i : I) → NormedRing (B i)
inst_2 : (i : I) → NormedAlgebra.{u_1, u_6} 𝕜 (B i)
inst_3 : ∀ (i : I), NormOneClass.{u_6} (B i)
k : 𝕜
⊢ Memℓp (E := B) (HSMul.hSMul (β := (i : I) → B i) k 1) ∞

Tactic:
(one_memℓp_infty.const_smul k : Memℓp (k • (1 : ∀ i, B i)) ∞)

Premises used: Memℓp.const_smul, one_memℓp_infty
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
I : Type u_5
B : I → Type u_6
inst : NormedField 𝕜
inst_1 : (i : I) → NormedRing (B i)
inst_2 : (i : I) → NormedAlgebra.{u_1, u_6} 𝕜 (B i)
inst_3 : ∀ (i : I), NormOneClass.{u_6} (B i)
k : 𝕜
⊢ Memℓp (E := B) (HSMul.hSMul (β := (i : I) → B i) k 1) ∞

Tactic:
exact (one_memℓp_infty.const_smul k : Memℓp (k • (1 : ∀ i, B i)) ∞)

Premises used: Memℓp.const_smul, one_memℓp_infty
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p_1 q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
inst_4 : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
⊢ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E p) (Pi.single (M := E) i a)

Tactic:
(memℓp_zero ?_).of_exponent_ge zero_le

Premises used: zero_le, Set.Mem, setOf, Memℓp.of_exponent_ge, memℓp_zero, Memℓp, ite
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p_1 q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
inst_4 : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
refine : Set.Finite.{u_3} (α := α) {i_1 : α | Pi.single (M := E) i a i_1 ≠ 0}
⊢ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E p) (Pi.single (M := E) i a)

Tactic:
refine (memℓp_zero ?_).of_exponent_ge zero_le

Premises used: zero_le, Memℓp.of_exponent_ge, memℓp_zero