awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f : PiLp ∞ β), ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
inr : ∀ (hp_1 : 1 ≤ p.toReal), ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

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

Premises used: ENNReal.dichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f : PiLp ∞ β
inl : ‖c • f.ofLp‖₊ ≤ ‖c‖₊ * ‖f.ofLp‖₊
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

Tactic:
rw [← nnnorm_ofLp, ← nnnorm_ofLp, ofLp_smul]

Premises used: WithLp.ofLp_smul, PiLp.nnnorm_ofLp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f : PiLp ∞ β
⊢ ‖c • f.ofLp‖₊ ≤ ‖c‖₊ * ‖f.ofLp‖₊

Tactic:
nnnorm_smul_le c (ofLp f)

Premises used: nnnorm_smul_le, WithLp.ofLp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f : PiLp ∞ β
⊢ ‖c • f.ofLp‖₊ ≤ ‖c‖₊ * ‖f.ofLp‖₊

Tactic:
exact nnnorm_smul_le c (ofLp f)

Premises used: nnnorm_smul_le, WithLp.ofLp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
⊢ 0 < p.toReal

Tactic:
have hp0 : 0 < p.toReal := zero_lt_one.trans_le hp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
⊢ p ≠ ∞

Tactic:
have hpt : p ≠ ⊤ := p.toReal_pos_iff_ne_top.mp hp0
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : LE.le (α := ℝ≥0) (∑ i : ι, ‖(c • f).ofLp i‖₊ ^ p.toReal) (∑ i : ι, ‖c‖₊ ^ p.toReal * ‖f.ofLp i‖₊ ^ p.toReal)
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

Tactic:
rw [nnnorm_eq_sum hpt, nnnorm_eq_sum hpt, one_div, NNReal.rpow_inv_le_iff hp0,
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one,
        Finset.mul_sum]

Premises used: Finset.mul_sum, NNReal.rpow_mul, NNReal.rpow_inv_le_iff, LT.lt.ne', one_div, PiLp.nnnorm_eq_sum, NNReal.rpow_one, NNReal.mul_rpow, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : LE.le (α := ℝ≥0) (∑ x : ι, ‖c • f.ofLp x‖₊ ^ p.toReal) (∑ x : ι, (‖c‖₊ * ‖f.ofLp x‖₊) ^ p.toReal)
⊢ LE.le (α := ℝ≥0) (∑ i : ι, ‖(c • f).ofLp i‖₊ ^ p.toReal) (∑ i : ι, ‖c‖₊ ^ p.toReal * ‖f.ofLp i‖₊ ^ p.toReal)

Tactic:
simp_rw [← NNReal.mul_rpow, smul_apply]

Premises used: PiLp.smul_apply, NNReal.mul_rpow
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → ‖c • f.ofLp i‖₊ ≤ ‖c‖₊ * ‖f.ofLp i‖₊
⊢ LE.le (α := ℝ≥0) (∑ x : ι, ‖c • f.ofLp x‖₊ ^ p.toReal) (∑ x : ι, (‖c‖₊ * ‖f.ofLp x‖₊) ^ p.toReal)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ‖c • f.ofLp i‖₊ ≤ ‖c‖₊ * ‖f.ofLp i‖₊

Tactic:
apply nnnorm_smul_le

Premises used: nnnorm_smul_le
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), NormSMulClass.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f : PiLp ∞ β), ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
inr : ∀ (hp_1 : 1 ≤ p.toReal), ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

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

Premises used: ENNReal.dichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), NormSMulClass.{u_1, u_4} 𝕜 (β i)
c : 𝕜
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f : PiLp ∞ β
inl : ‖(c • f).ofLp‖₊ = ‖c‖₊ * ‖f‖₊
inl₁ : ‖(c • f).ofLp‖₊ = ‖c‖₊ * ‖f.ofLp‖₊
inl₂ : ‖c • f.ofLp‖₊ = ‖c‖₊ * ‖f.ofLp‖₊
inl₃ inl₄ : ‖c‖₊ * ‖f.ofLp‖₊ = ‖c‖₊ * ‖f.ofLp‖₊
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

Tactic:
rw [← nnnorm_ofLp, ← nnnorm_ofLp, WithLp.ofLp_smul, nnnorm_smul]

Premises used: WithLp.ofLp_smul, nnnorm_smul, PiLp.nnnorm_ofLp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), NormSMulClass.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
⊢ 0 < p.toReal

Tactic:
have hp0 : 0 < p.toReal := zero_lt_one.trans_le hp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), NormSMulClass.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
⊢ p ≠ ∞

Tactic:
have hpt : p ≠ ⊤ := p.toReal_pos_iff_ne_top.mp hp0
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), NormSMulClass.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : Eq (α := ℝ≥0) (∑ i : ι, ‖(c • f).ofLp i‖₊ ^ p.toReal) (∑ i : ι, ‖c‖₊ ^ p.toReal * ‖f.ofLp i‖₊ ^ p.toReal)
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

Tactic:
rw [nnnorm_eq_sum hpt, nnnorm_eq_sum hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne',
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one,
        Finset.mul_sum]

Premises used: Finset.mul_sum, NNReal.rpow_mul, NNReal.rpow_inv_eq_iff, LT.lt.ne', one_div, PiLp.nnnorm_eq_sum, NNReal.rpow_one, NNReal.mul_rpow, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), NormSMulClass.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : Eq (α := ℝ≥0) (∑ i : ι, ‖(c • f).ofLp i‖₊ ^ p.toReal) (∑ x : ι, (‖c‖₊ * ‖f.ofLp x‖₊) ^ p.toReal)
inr₁ : Eq (α := ℝ≥0) (∑ x : ι, ‖c • f.ofLp x‖₊ ^ p.toReal) (∑ x : ι, (‖c‖₊ * ‖f.ofLp x‖₊) ^ p.toReal)
⊢ Eq (α := ℝ≥0) (∑ i : ι, ‖(c • f).ofLp i‖₊ ^ p.toReal) (∑ i : ι, ‖c‖₊ ^ p.toReal * ‖f.ofLp i‖₊ ^ p.toReal)

Tactic:
simp_rw [← NNReal.mul_rpow, smul_apply, nnnorm_smul]

Premises used: nnnorm_smul, PiLp.smul_apply, NNReal.mul_rpow
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : Semiring 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
inst_3 : (i : ι) → SeminormedAddCommGroup (β i)
inst_4 : (i : ι) → Module.{u_1, u_3} 𝕜 (α i)
inst_5 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
c : 𝕜
ι' : Type u_5
inst_6 : Fintype ι'
E : Type u_6
inst_7 : SeminormedAddCommGroup E
inst_8 : Module 𝕜 E
e : ι ≃ ι'
x' : PiLp.{u_2, u_6} p fun (x : ι) ↦ E
inl :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x' : PiLp.{u_2, u_6} ∞ fun (x : ι) ↦ E),
    Norm.norm (E := PiLp.{u_5, u_6} ∞ fun (x : ι') ↦ E)
        ((WithLp.linearEquiv ∞ 𝕜 (ι → E) ≪≫ₗ
                (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ
                  LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 (ι' → E))) :
              (a : PiLp ∞ fun (x : ι) ↦ E) → PiLp ∞ fun (x : ι') ↦ E)
            x' :
          PiLp.{u_5, u_6} ∞ fun (x : ι') ↦ E) =
      ‖x'‖
inr :
  ∀ (h : 1 ≤ p.toReal),
    Norm.norm (E := PiLp.{u_5, u_6} p fun (x : ι') ↦ E)
        ((WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
                (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ
                  LinearEquiv.symm (WithLp.linearEquiv p 𝕜 (ι' → E))) :
              (a : PiLp p fun (x : ι) ↦ E) → PiLp p fun (x : ι') ↦ E)
            x' :
          PiLp.{u_5, u_6} p fun (x : ι') ↦ E) =
      ‖x'‖
⊢ Norm.norm (E := PiLp.{u_5, u_6} p fun (x : ι') ↦ E)
      ((WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
              (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv p 𝕜 (ι' → E))) :
            (a : PiLp p fun (x : ι) ↦ E) → PiLp p fun (x : ι') ↦ E)
          x' :
        PiLp.{u_5, u_6} p fun (x : ι') ↦ E) =
    ‖x'‖

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

Premises used: ENNReal.dichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fintype ι
inst_1 : Semiring 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
inst_3 : (i : ι) → SeminormedAddCommGroup (β i)
inst_4 : (i : ι) → Module.{u_1, u_3} 𝕜 (α i)
inst_5 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
c : 𝕜
ι' : Type u_5
inst_6 : Fintype ι'
E : Type u_6
inst_7 : SeminormedAddCommGroup E
inst_8 : Module 𝕜 E
e : ι ≃ ι'
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
__LinearEquiv : (PiLp.{u_2, u_6} ∞ fun (x : ι) ↦ E) ≃ₗ[𝕜] PiLp.{u_5, u_6} ∞ fun (x : ι') ↦ E :=
  WithLp.linearEquiv ∞ 𝕜 (ι → E) ≪≫ₗ
    (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 (ι' → E)))
x' : PiLp.{u_2, u_6} ∞ fun (x : ι) ↦ E
inl :
  Eq (α := ℝ)
    (⨆ (i : ι'),
      Norm.norm.{u_6} (E := E)
        (ofLp (p := ∞)
          ((WithLp.linearEquiv ∞ 𝕜 (ι → E) ≪≫ₗ
                (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ
                  LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 (ι' → E))) :
              (a : PiLp ∞ fun (x : ι) ↦ E) → PiLp ∞ fun (x : ι') ↦ E)
            x')
          i))
    (⨆ (i : ι), ‖x'.ofLp i‖)
⊢ Norm.norm (E := PiLp.{u_5, u_6} ∞ fun (x : ι') ↦ E)
      ((WithLp.linearEquiv ∞ 𝕜 (ι → E) ≪≫ₗ
              (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 (ι' → E))) :
            (a : PiLp ∞ fun (x : ι) ↦ E) → PiLp ∞ fun (x : ι') ↦ E)
          x' :
        PiLp.{u_5, u_6} ∞ fun (x : ι') ↦ E) =
    ‖x'‖

Tactic:
simp_rw [norm_eq_ciSup]

Premises used: PiLp.norm_eq_ciSup
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fintype ι
inst_1 : Semiring 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
inst_3 : (i : ι) → SeminormedAddCommGroup (β i)
inst_4 : (i : ι) → Module.{u_1, u_3} 𝕜 (α i)
inst_5 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
c : 𝕜
ι' : Type u_5
inst_6 : Fintype ι'
E : Type u_6
inst_7 : SeminormedAddCommGroup E
inst_8 : Module 𝕜 E
e : ι ≃ ι'
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
__LinearEquiv : (PiLp.{u_2, u_6} ∞ fun (x : ι) ↦ E) ≃ₗ[𝕜] PiLp.{u_5, u_6} ∞ fun (x : ι') ↦ E :=
  WithLp.linearEquiv ∞ 𝕜 (ι → E) ≪≫ₗ
    (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 (ι' → E)))
x' : PiLp.{u_2, u_6} ∞ fun (x : ι) ↦ E
⊢ Eq (α := ℝ)
    (⨆ (i : ι'),
      Norm.norm.{u_6} (E := E)
        (ofLp (p := ∞)
          ((WithLp.linearEquiv ∞ 𝕜 (ι → E) ≪≫ₗ
                (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ
                  LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 (ι' → E))) :
              (a : PiLp ∞ fun (x : ι) ↦ E) → PiLp ∞ fun (x : ι') ↦ E)
            x')
          i))
    (⨆ (i : ι), ‖x'.ofLp i‖)

Tactic:
e.symm.iSup_congr fun _ => rfl

Premises used: Equiv.symm, Equiv.iSup_congr, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fintype ι
inst_1 : Semiring 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
inst_3 : (i : ι) → SeminormedAddCommGroup (β i)
inst_4 : (i : ι) → Module.{u_1, u_3} 𝕜 (α i)
inst_5 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
c : 𝕜
ι' : Type u_5
inst_6 : Fintype ι'
E : Type u_6
inst_7 : SeminormedAddCommGroup E
inst_8 : Module 𝕜 E
e : ι ≃ ι'
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
__LinearEquiv : (PiLp.{u_2, u_6} ∞ fun (x : ι) ↦ E) ≃ₗ[𝕜] PiLp.{u_5, u_6} ∞ fun (x : ι') ↦ E :=
  WithLp.linearEquiv ∞ 𝕜 (ι → E) ≪≫ₗ
    (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 (ι' → E)))
x' : PiLp.{u_2, u_6} ∞ fun (x : ι) ↦ E
⊢ Eq (α := ℝ)
    (⨆ (i : ι'),
      Norm.norm.{u_6} (E := E)
        (ofLp (p := ∞)
          ((WithLp.linearEquiv ∞ 𝕜 (ι → E) ≪≫ₗ
                (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ
                  LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 (ι' → E))) :
              (a : PiLp ∞ fun (x : ι) ↦ E) → PiLp ∞ fun (x : ι') ↦ E)
            x')
          i))
    (⨆ (i : ι), ‖x'.ofLp i‖)

Tactic:
exact e.symm.iSup_congr fun _ => rfl

Premises used: Equiv.symm, Equiv.iSup_congr, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : Semiring 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
inst_3 : (i : ι) → SeminormedAddCommGroup (β i)
inst_4 : (i : ι) → Module.{u_1, u_3} 𝕜 (α i)
inst_5 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
c : 𝕜
ι' : Type u_5
inst_6 : Fintype ι'
E : Type u_6
inst_7 : SeminormedAddCommGroup E
inst_8 : Module 𝕜 E
e : ι ≃ ι'
x' : PiLp.{u_2, u_6} p fun (x : ι) ↦ E
h : 1 ≤ p.toReal
inr :
  HPow.hPow (α := ℝ)
      (∑ i : ι',
        Norm.norm.{u_6} (E := E)
            (ofLp (p := p)
              ((WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
                    (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ
                      LinearEquiv.symm (WithLp.linearEquiv p 𝕜 (ι' → E))) :
                  (a : PiLp p fun (x : ι) ↦ E) → PiLp p fun (x : ι') ↦ E)
                x')
              i) ^
          p.toReal)
      (1 / p.toReal) =
    HPow.hPow (α := ℝ) (∑ i : ι, ‖x'.ofLp i‖ ^ p.toReal) (1 / p.toReal)
⊢ Norm.norm (E := PiLp.{u_5, u_6} p fun (x : ι') ↦ E)
      ((WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
              (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv p 𝕜 (ι' → E))) :
            (a : PiLp p fun (x : ι) ↦ E) → PiLp p fun (x : ι') ↦ E)
          x' :
        PiLp.{u_5, u_6} p fun (x : ι') ↦ E) =
    ‖x'‖

Tactic:
simp only [norm_eq_sum (zero_lt_one.trans_le h)]

Premises used: PiLp.norm_eq_sum, zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : Semiring 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
inst_3 : (i : ι) → SeminormedAddCommGroup (β i)
inst_4 : (i : ι) → Module.{u_1, u_3} 𝕜 (α i)
inst_5 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
c : 𝕜
ι' : Type u_5
inst_6 : Fintype ι'
E : Type u_6
inst_7 : SeminormedAddCommGroup E
inst_8 : Module 𝕜 E
e : ι ≃ ι'
x' : PiLp.{u_2, u_6} p fun (x : ι) ↦ E
h : 1 ≤ p.toReal
inr :
  Eq (α := ℝ)
    (∑ i : ι',
      Norm.norm.{u_6} (E := E)
          (ofLp (p := p)
            ((WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
                  (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ
                    LinearEquiv.symm (WithLp.linearEquiv p 𝕜 (ι' → E))) :
                (a : PiLp p fun (x : ι) ↦ E) → PiLp p fun (x : ι') ↦ E)
              x')
            i) ^
        p.toReal)
    (∑ i : ι, ‖x'.ofLp i‖ ^ p.toReal)
⊢ HPow.hPow (α := ℝ)
      (∑ i : ι',
        Norm.norm.{u_6} (E := E)
            (ofLp (p := p)
              ((WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
                    (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ
                      LinearEquiv.symm (WithLp.linearEquiv p 𝕜 (ι' → E))) :
                  (a : PiLp p fun (x : ι) ↦ E) → PiLp p fun (x : ι') ↦ E)
                x')
              i) ^
          p.toReal)
      (1 / p.toReal) =
    HPow.hPow (α := ℝ) (∑ i : ι, ‖x'.ofLp i‖ ^ p.toReal) (1 / p.toReal)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : Semiring 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
inst_3 : (i : ι) → SeminormedAddCommGroup (β i)
inst_4 : (i : ι) → Module.{u_1, u_3} 𝕜 (α i)
inst_5 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
c : 𝕜
ι' : Type u_5
inst_6 : Fintype ι'
E : Type u_6
inst_7 : SeminormedAddCommGroup E
inst_8 : Module 𝕜 E
e : ι ≃ ι'
x' : PiLp.{u_2, u_6} p fun (x : ι) ↦ E
h : 1 ≤ p.toReal
⊢ Eq (α := ℝ)
    (∑ i : ι',
      Norm.norm.{u_6} (E := E)
          (ofLp (p := p)
            ((WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
                  (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ
                    LinearEquiv.symm (WithLp.linearEquiv p 𝕜 (ι' → E))) :
                (a : PiLp p fun (x : ι) ↦ E) → PiLp p fun (x : ι') ↦ E)
              x')
            i) ^
        p.toReal)
    (∑ i : ι, ‖x'.ofLp i‖ ^ p.toReal)

Tactic:
Fintype.sum_equiv e.symm _ _ fun _ => rfl

Premises used: Equiv.symm, Fintype.sum_equiv, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : Semiring 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
inst_3 : (i : ι) → SeminormedAddCommGroup (β i)
inst_4 : (i : ι) → Module.{u_1, u_3} 𝕜 (α i)
inst_5 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
c : 𝕜
ι' : Type u_5
inst_6 : Fintype ι'
E : Type u_6
inst_7 : SeminormedAddCommGroup E
inst_8 : Module 𝕜 E
e : ι ≃ ι'
x' : PiLp.{u_2, u_6} p fun (x : ι) ↦ E
h : 1 ≤ p.toReal
⊢ Eq (α := ℝ)
    (∑ i : ι',
      Norm.norm.{u_6} (E := E)
          (ofLp (p := p)
            ((WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
                  (LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) ↦ E) e ≪≫ₗ
                    LinearEquiv.symm (WithLp.linearEquiv p 𝕜 (ι' → E))) :
                (a : PiLp p fun (x : ι) ↦ E) → PiLp p fun (x : ι') ↦ E)
              x')
            i) ^
        p.toReal)
    (∑ i : ι, ‖x'.ofLp i‖ ^ p.toReal)

Tactic:
exact Fintype.sum_equiv e.symm _ _ fun _ => rfl

Premises used: Equiv.symm, Fintype.sum_equiv, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : Semiring 𝕜
ι' : Type u_5
inst_2 : Fintype ι'
E : Type u_6
inst_3 : SeminormedAddCommGroup E
inst_4 : Module 𝕜 E
e : ι ≃ ι'
v : PiLp.{u_2, u_6} p fun (x : ι) ↦ E
⊢ Eq (α := (i : ι') → (fun (x : ι') ↦ E) i)
    (ofLp (p := p)
        ((LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e : (a : PiLp p fun (x : ι) ↦ E) → PiLp p fun (x : ι') ↦ E) v) :
      (i : ι') → (fun (x : ι') ↦ E) i)
    ((Equiv.piCongrLeft' (fun (x : ι) ↦ E) e : (a : (a : ι) → E) → (b : ι') → E) v.ofLp : (b : ι') → E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : Semiring 𝕜
ι' : Type u_5
inst_2 : Fintype ι'
E : Type u_6
inst_3 : SeminormedAddCommGroup E
inst_4 : Module 𝕜 E
e : ι ≃ ι'
h :
  ∀ (x : PiLp.{u_5, u_6} p fun (x : ι') ↦ E) (i : ι),
    Eq.{u_6 + 1} (α := E)
      (ofLp (p := p)
        ((LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) :
            (a : PiLp p fun (x : ι') ↦ E) → PiLp p fun (x : ι) ↦ E)
          x)
        i)
      (ofLp (p := p)
        ((LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e.symm : (a : PiLp p fun (x : ι') ↦ E) → PiLp p fun (x : ι) ↦ E) x) i)
⊢ Eq (α := (PiLp.{u_5, u_6} p fun (x : ι') ↦ E) ≃ₗᵢ[𝕜] PiLp.{u_2, u_6} p fun (x : ι) ↦ E)
    (LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e))
    (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e.symm)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : Semiring 𝕜
ι' : Type u_5
inst_2 : Fintype ι'
E : Type u_6
inst_3 : SeminormedAddCommGroup E
inst_4 : Module 𝕜 E
e : ι ≃ ι'
x : PiLp.{u_5, u_6} p fun (x : ι') ↦ E
i : ι
⊢ Eq.{u_6 + 1} (α := E)
    (ofLp (p := p)
      ((LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) :
          (a : PiLp p fun (x : ι') ↦ E) → PiLp p fun (x : ι) ↦ E)
        x)
      i)
    (ofLp (p := p)
      ((LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e.symm : (a : PiLp p fun (x : ι') ↦ E) → PiLp p fun (x : ι) ↦ E) x) i)

Tactic:
simp [LinearIsometryEquiv.piLpCongrLeft, LinearIsometryEquiv.symm]

Premises used: LinearIsometryEquiv.symm, LinearIsometryEquiv.piLpCongrLeft
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : Semiring 𝕜
ι' : Type u_5
inst_2 : Fintype ι'
E : Type u_6
inst_3 : SeminormedAddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq ι
inst_6 : DecidableEq ι'
e : ι ≃ ι'
i : ι
v : E
h :
  ∀ (x : ι'),
    Eq.{u_6 + 1} (α := E)
      (ofLp (p := p)
          ((LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e : (a : PiLp p fun (x : ι) ↦ E) → PiLp p fun (x : ι') ↦ E)
            (single p (β := fun (x : ι) ↦ E) i v))
          x :
        E)
      (ofLp (p := p) (single p (β := fun (x : ι') ↦ E) ((e : (a : ι) → ι') i) v) x : E)
⊢ Eq (α := PiLp.{u_5, u_6} p fun (x : ι') ↦ E)
    ((LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e : (a : PiLp p fun (x : ι) ↦ E) → PiLp p fun (x : ι') ↦ E)
        (single p (β := fun (x : ι) ↦ E) i v) :
      PiLp.{u_5, u_6} p fun (x : ι') ↦ E)
    (single p (β := fun (x : ι') ↦ E) ((e : (a : ι) → ι') i) v : PiLp.{u_5, u_6} p fun (x : ι') ↦ E)

Tactic:
ext x