awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)

Tactic:
simp [LinearIsometryEquiv.piLpCongrLeft_apply, Equiv.piCongrLeft',
    Pi.single, Function.update, Equiv.symm_apply_eq]

Premises used: Function.update, LinearIsometryEquiv.piLpCongrLeft_apply, Equiv.symm_apply_eq, Pi.single, Equiv.piCongrLeft'
-- 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 : 𝕜
e : (i : ι) → LinearIsometryEquiv.{u_1, u_1, u_3, u_4} (RingHom.id 𝕜) (α i) (β i)
x : (i : ι) → α i
simp :
  Norm.norm (E := PiLp p β)
      (toLp p
          (((LinearEquiv.piCongrRight (φ := α) (ψ := β) fun (i : ι) ↦ (e i).toLinearEquiv :
                ((i : ι) → α i) ≃ₗ[𝕜] (i : ι) → β i) :
              (a : (i : ι) → α i) → (i : ι) → β i)
            x) :
        WithLp p ((i : ι) → β i)) =
    ‖toLp p x‖
⊢ Norm.norm (E := PiLp p β)
      (((WithLp.linearEquiv p 𝕜 ((i : ι) → α i) ≪≫ₗ
                LinearEquiv.piCongrRight (φ := α) (ψ := β) fun (i : ι) ↦ (e i).toLinearEquiv) ≪≫ₗ
              LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((i : ι) → β i)) :
            (a : PiLp p α) → PiLp p β)
          (((LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((i : ι) → α i)) :
                ((i : ι) → α i) ≃ₗ[𝕜] WithLp p ((i : ι) → α i)) :
              (a : (i : ι) → α i) → WithLp p ((i : ι) → α i))
            x) :
        PiLp p β) =
    Norm.norm (E := PiLp p α)
      (((LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((i : ι) → α i)) : ((i : ι) → α i) ≃ₗ[𝕜] WithLp p ((i : ι) → α i)) :
            (a : (i : ι) → α i) → WithLp p ((i : ι) → α i))
          x :
        WithLp p ((i : ι) → α i))

Tactic:
simp only [coe_symm_linearEquiv, LinearEquiv.trans_apply, coe_linearEquiv]

Premises used: WithLp.coe_linearEquiv, LinearEquiv.trans_apply, WithLp.coe_symm_linearEquiv
-- 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 : 𝕜
e : (i : ι) → LinearIsometryEquiv.{u_1, u_1, u_3, u_4} (RingHom.id 𝕜) (α i) (β i)
x : (i : ι) → α i
inl :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)],
    Norm.norm (E := PiLp ∞ β)
        (toLp ∞
            (((LinearEquiv.piCongrRight (φ := α) (ψ := β) fun (i : ι) ↦ (e i).toLinearEquiv :
                  ((i : ι) → α i) ≃ₗ[𝕜] (i : ι) → β i) :
                (a : (i : ι) → α i) → (i : ι) → β i)
              x) :
          WithLp ∞ ((i : ι) → β i)) =
      Norm.norm (E := PiLp ∞ α) (toLp ∞ x)
inr :
  ∀ (hp_1 : 1 ≤ p.toReal),
    Norm.norm (E := PiLp p β)
        (toLp p
            (((LinearEquiv.piCongrRight (φ := α) (ψ := β) fun (i : ι) ↦ (e i).toLinearEquiv :
                  ((i : ι) → α i) ≃ₗ[𝕜] (i : ι) → β i) :
                (a : (i : ι) → α i) → (i : ι) → β i)
              x) :
          WithLp p ((i : ι) → β i)) =
      ‖toLp p x‖
⊢ Norm.norm (E := PiLp p β)
      (toLp p
          (((LinearEquiv.piCongrRight (φ := α) (ψ := β) fun (i : ι) ↦ (e i).toLinearEquiv :
                ((i : ι) → α i) ≃ₗ[𝕜] (i : ι) → β i) :
              (a : (i : ι) → α i) → (i : ι) → β i)
            x) :
        WithLp p ((i : ι) → β i)) =
    ‖toLp p x‖

Tactic:
obtain rfl | hp := p.dichotomy

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 : 𝕜
e : (i : ι) → LinearIsometryEquiv.{u_1, u_1, u_3, u_4} (RingHom.id 𝕜) (α i) (β i)
x : (i : ι) → α i
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
__LinearEquiv : PiLp ∞ α ≃ₗ[𝕜] PiLp ∞ β :=
  (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → α i) ≪≫ₗ
      LinearEquiv.piCongrRight (φ := α) (ψ := β) fun (i : ι) ↦ (e i).toLinearEquiv) ≪≫ₗ
    LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → β i))
inl :
  Norm.norm (E := (i : ι) → β i)
      (((LinearEquiv.piCongrRight (φ := α) (ψ := β) fun (i : ι) ↦ (e i).toLinearEquiv :
              ((i : ι) → α i) ≃ₗ[𝕜] (i : ι) → β i) :
            (a : (i : ι) → α i) → (i : ι) → β i)
          x :
        (i : ι) → β i) =
    ‖x‖
inl₁ :
  (↑(Finset.sup Finset.univ fun (b : ι) ↦
          nnnorm.{u_4} (E := β b)
            (((LinearEquiv.piCongrRight (φ := α) (ψ := β) fun (i : ι) ↦ (e i).toLinearEquiv :
                    ((i : ι) → α i) ≃ₗ[𝕜] (i : ι) → β i) :
                  (a : (i : ι) → α i) → (i : ι) → β i)
                x b :
              β b)) :
      ℝ) =
    (↑(Finset.sup Finset.univ fun (b : ι) ↦ ‖x b‖₊) : ℝ)
inl₂ :
  (↑(Finset.sup Finset.univ fun (b : ι) ↦
          nnnorm.{u_4} (E := β b) (((e b).toLinearEquiv : (a : α b) → β b) (x b) : β b)) :
      ℝ) =
    (↑(Finset.sup Finset.univ fun (b : ι) ↦ ‖x b‖₊) : ℝ)
inl₃ :
  (↑(Finset.sup Finset.univ fun (b : ι) ↦ nnnorm.{u_4} (E := β b) ((e b : (a : α b) → β b) (x b) : β b)) : ℝ) =
    (↑(Finset.sup Finset.univ fun (b : ι) ↦ ‖x b‖₊) : ℝ)
⊢ Norm.norm (E := PiLp ∞ β)
      (toLp ∞
          (((LinearEquiv.piCongrRight (φ := α) (ψ := β) fun (i : ι) ↦ (e i).toLinearEquiv :
                ((i : ι) → α i) ≃ₗ[𝕜] (i : ι) → β i) :
              (a : (i : ι) → α i) → (i : ι) → β i)
            x) :
        WithLp ∞ ((i : ι) → β i)) =
    Norm.norm (E := PiLp ∞ α) (toLp ∞ x)

Tactic:
simp_rw [PiLp.norm_toLp, Pi.norm_def, LinearEquiv.piCongrRight_apply,
        LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.nnnorm_map]

Premises used: LinearEquiv.piCongrRight_apply, LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.nnnorm_map, Pi.norm_def, PiLp.norm_toLp
-- 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 : 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 : 𝕜
e : (i : ι) → LinearIsometryEquiv.{u_1, u_1, u_3, u_4} (RingHom.id 𝕜) (α i) (β i)
x : (i : ι) → α i
hp : 1 ≤ p.toReal
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 1 ≤ p.toReal
⊢ 1 ≤ p.toReal

Tactic:
norm_cast
-- 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 : 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 : 𝕜
e : (i : ι) → LinearIsometryEquiv.{u_1, u_1, u_3, u_4} (RingHom.id 𝕜) (α i) (β i)
x : (i : ι) → α i
hp : 1 ≤ p.toReal
⊢ 0 < p.toReal

Tactic:
have : 0 < p.toReal := zero_lt_one.trans_le <| by norm_cast
-- 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 : 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 : 𝕜
e : (i : ι) → LinearIsometryEquiv.{u_1, u_1, u_3, u_4} (RingHom.id 𝕜) (α i) (β i)
x : (i : ι) → α i
hp : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ Norm.norm (E := PiLp p β)
      (toLp p
          (((LinearEquiv.piCongrRight (φ := α) (ψ := β) fun (i : ι) ↦ (e i).toLinearEquiv :
                ((i : ι) → α i) ≃ₗ[𝕜] (i : ι) → β i) :
              (a : (i : ι) → α i) → (i : ι) → β i)
            x) :
        WithLp p ((i : ι) → β i)) =
    ‖toLp p x‖

Tactic:
simp only [PiLp.norm_eq_sum this, LinearEquiv.piCongrRight_apply,
        LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.norm_map, one_div]

Premises used: LinearEquiv.piCongrRight_apply, LinearIsometryEquiv.norm_map, LinearIsometryEquiv.coe_toLinearEquiv, PiLp.norm_eq_sum, one_div
-- 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)
e : (i : ι) → LinearIsometryEquiv.{u_1, u_1, u_3, u_4} (RingHom.id 𝕜) (α i) (β i)
x : PiLp p α
⊢ Eq (α := PiLp p β)
    ((LinearIsometryEquiv.piLpCongrRight p (α := α) (β := β) e : (a : PiLp p α) → PiLp p β) x : PiLp p β)
    (toLp p fun (i : ι) ↦ (e i : (a : α i) → β i) (x.ofLp i) : WithLp p ((i : ι) → β i))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : Semiring 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (α i)
⊢ Eq (α := PiLp p α ≃ₗᵢ[𝕜] PiLp p α)
    (LinearIsometryEquiv.piLpCongrRight p (α := α) (β := α) fun (i : ι) ↦ LinearIsometryEquiv.refl 𝕜 (α i))
    (LinearIsometryEquiv.refl 𝕜 (PiLp p α))

Tactic:
rfl

Premises used: LinearIsometryEquiv.refl, LinearIsometryEquiv.piLpCongrRight, LinearEquiv.refl, LinearEquiv.trans, 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)
e : (i : ι) → LinearIsometryEquiv.{u_1, u_1, u_3, u_4} (RingHom.id 𝕜) (α i) (β i)
⊢ Eq (α := PiLp p β ≃ₗᵢ[𝕜] PiLp p α)
    (LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrRight p (α := α) (β := β) e))
    (LinearIsometryEquiv.piLpCongrRight p (α := β) (β := α) fun (i : ι) ↦ (e i).symm)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, LinearIsometryEquiv.piLpCongrRight, LinearEquiv.trans, 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)
e : (i : ι) → LinearIsometryEquiv.{u_1, u_1, u_3, u_4} (RingHom.id 𝕜) (α i) (β i)
inst_6 : DecidableEq ι
i : ι
v : α i
⊢ Eq (α := PiLp p β)
    ((LinearIsometryEquiv.piLpCongrRight p (α := α) (β := β) e : (a : PiLp p α) → PiLp p β) (single p (β := α) i v) :
      PiLp p β)
    (single p (β := β) i ((e i : (a : α i) → β i) v) : PiLp p β)

Tactic:
PiLp.ext <| Pi.apply_single (e ·) (fun _ => map_zero _) _ _

Premises used: PiLp.ext, Pi.apply_single, map_zero, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι_1 : Type u_2
α_1 : ι_1 → Type u_3
β : ι_1 → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι_1
inst_1 : Semiring 𝕜
inst_2 : (i : ι_1) → SeminormedAddCommGroup (α_1 i)
inst_3 : (i : ι_1) → SeminormedAddCommGroup (β i)
inst_4 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (α_1 i)
inst_5 : (i : ι_1) → Module.{u_1, u_4} 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
inst_6 : Fintype ι
inst_7 : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst_8 : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst_9 : (i : ι) → (k : κ i) → Module.{u_1, u_7} 𝕜 (α i k)
x : (i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i
inst_10 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
__LinearEquiv : (PiLp ∞ fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) ≃ₗ[𝕜]
  PiLp ∞ fun (i : ι) ↦ PiLp ∞ (α i) :=
  (WithLp.linearEquiv ∞ 𝕜 ((i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i) ≪≫ₗ
        LinearEquiv.piCurry 𝕜 (κ := κ) α ≪≫ₗ
      LinearEquiv.piCongrRight (φ := fun (i : ι) ↦ (j : κ i) → α i j) (ψ := fun (x : ι) ↦ WithLp ∞ ((j : κ x) → α x j))
        fun (x : ι) ↦ LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((j : κ x) → α x j))) ≪≫ₗ
    LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → WithLp ∞ ((j : κ i) → α i j)))
inl :
  Eq (α := ℝ≥0)
    (Finset.sup Finset.univ fun (b : ι) ↦
      Finset.sup Finset.univ fun (b_1 : κ b) ↦
        nnnorm (E := α b b_1)
          (x (Sigma.mk (β := fun (i : ι) ↦ κ i) b b_1) :
            (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) (Sigma.mk (β := fun (i : ι) ↦ κ i) b b_1)))
    (Finset.sup Finset.univ fun (b : Sigma κ) ↦ ‖x b‖₊)
⊢ Eq (α := ℝ≥0)
    (Finset.sup Finset.univ fun (b : ι) ↦
      Finset.sup Finset.univ fun (b_1 : κ b) ↦
        nnnorm.{u_7} (E := α b b_1)
          (ofLp (p := ∞)
            (ofLp (p := ∞)
              (((WithLp.linearEquiv ∞ 𝕜 ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ))) ≪≫ₗ
                        LinearEquiv.piCurry 𝕜 (κ := κ) α ≪≫ₗ
                      LinearEquiv.piCongrRight (φ := fun (i : ι) ↦ (j : κ i) → α i j) (ψ := fun (x : ι) ↦
                        WithLp ∞ ((j : κ x) → α x j)) fun (x : ι) ↦
                        LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((j : κ x) → α x j))) ≪≫ₗ
                    LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → WithLp ∞ ((j : κ i) → α i j))) :
                  (a : PiLp ∞ fun (i : Sigma κ) ↦ α i.fst i.snd) → PiLp ∞ fun (i : ι) ↦ PiLp ∞ (α i))
                (Equiv.invFun
                  (AddEquiv.toEquiv (WithLp.addEquiv ∞ ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ))))) x))
              b)
            b_1))
    (Finset.sup Finset.univ fun (b : Sigma κ) ↦
      ‖ofLp (p := ∞)
          (Equiv.invFun (AddEquiv.toEquiv (WithLp.addEquiv ∞ ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ))))) x)
          b‖₊)

Tactic:
dsimp [Sigma.curry]

Premises used: Sigma.curry
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι_1 : Type u_2
α_1 : ι_1 → Type u_3
β : ι_1 → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι_1
inst_1 : Semiring 𝕜
inst_2 : (i : ι_1) → SeminormedAddCommGroup (α_1 i)
inst_3 : (i : ι_1) → SeminormedAddCommGroup (β i)
inst_4 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (α_1 i)
inst_5 : (i : ι_1) → Module.{u_1, u_4} 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
inst_6 : Fintype ι
inst_7 : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst_8 : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst_9 : (i : ι) → (k : κ i) → Module.{u_1, u_7} 𝕜 (α i k)
x : (i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i
inst_10 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
__LinearEquiv : (PiLp ∞ fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) ≃ₗ[𝕜]
  PiLp ∞ fun (i : ι) ↦ PiLp ∞ (α i) :=
  (WithLp.linearEquiv ∞ 𝕜 ((i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i) ≪≫ₗ
        LinearEquiv.piCurry 𝕜 (κ := κ) α ≪≫ₗ
      LinearEquiv.piCongrRight (φ := fun (i : ι) ↦ (j : κ i) → α i j) (ψ := fun (x : ι) ↦ WithLp ∞ ((j : κ x) → α x j))
        fun (x : ι) ↦ LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((j : κ x) → α x j))) ≪≫ₗ
    LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → WithLp ∞ ((j : κ i) → α i j)))
inl :
  Eq (α := ℝ≥0)
    (Finset.sup Finset.univ fun (b : ι) ↦
      Finset.sup Finset.univ fun (b_1 : κ b) ↦
        nnnorm (E := α b b_1)
          (x (Sigma.mk (β := fun (i : ι) ↦ κ i) b b_1) :
            (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) (Sigma.mk (β := fun (i : ι) ↦ κ i) b b_1)))
    (Finset.sup (Finset.sigma (α := κ) Finset.univ fun (x : ι) ↦ Finset.univ) fun (b : Sigma κ) ↦ ‖x b‖₊)
inl₁ inl₂ :
  Eq (α := ℝ≥0)
    (Finset.sup Finset.univ fun (b : ι) ↦
      Finset.sup Finset.univ fun (b_1 : κ b) ↦
        nnnorm (E := α b b_1)
          (x (Sigma.mk (β := fun (i : ι) ↦ κ i) b b_1) :
            (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) (Sigma.mk (β := fun (i : ι) ↦ κ i) b b_1)))
    (Finset.sup Finset.univ fun (i : ι) ↦
      Finset.sup Finset.univ fun (b : κ i) ↦
        nnnorm (E :=
          α ((Sigma.mk (β := fun (i : ι) ↦ κ i) i b).fst (β := κ))
            ((Sigma.mk (β := fun (i : ι) ↦ κ i) i b).snd (β := κ)))
          (x (Sigma.mk (β := fun (i : ι) ↦ κ i) i b)))
⊢ Eq (α := ℝ≥0)
    (Finset.sup Finset.univ fun (b : ι) ↦
      Finset.sup Finset.univ fun (b_1 : κ b) ↦
        nnnorm (E := α b b_1)
          (x (Sigma.mk (β := fun (i : ι) ↦ κ i) b b_1) :
            (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) (Sigma.mk (β := fun (i : ι) ↦ κ i) b b_1)))
    (Finset.sup Finset.univ fun (b : Sigma κ) ↦ ‖x b‖₊)

Tactic:
rw [← Finset.univ_sigma_univ, Finset.sup_sigma]

Premises used: Finset.univ_sigma_univ, Finset.sup_sigma
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p_1 : ℝ≥0∞
𝕜 : Type u_1
ι_1 : Type u_2
α_1 : ι_1 → Type u_3
β : ι_1 → Type u_4
hp_1 : Fact (1 ≤ p_1)
inst : Fintype ι_1
inst_1 : Semiring 𝕜
inst_2 : (i : ι_1) → SeminormedAddCommGroup (α_1 i)
inst_3 : (i : ι_1) → SeminormedAddCommGroup (β i)
inst_4 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (α_1 i)
inst_5 : (i : ι_1) → Module.{u_1, u_4} 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
inst_7 : Fintype ι
inst_8 : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst_9 : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst_10 : (i : ι) → (k : κ i) → Module.{u_1, u_7} 𝕜 (α i k)
x : (i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i
hp : p ≠ ∞
⊢ 0 < p.toReal

Tactic:
have : 0 < p.toReal := (toReal_pos_iff_ne_top _).mpr hp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p_1 : ℝ≥0∞
𝕜 : Type u_1
ι_1 : Type u_2
α_1 : ι_1 → Type u_3
β : ι_1 → Type u_4
hp_1 : Fact (1 ≤ p_1)
inst : Fintype ι_1
inst_1 : Semiring 𝕜
inst_2 : (i : ι_1) → SeminormedAddCommGroup (α_1 i)
inst_3 : (i : ι_1) → SeminormedAddCommGroup (β i)
inst_4 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (α_1 i)
inst_5 : (i : ι_1) → Module.{u_1, u_4} 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
inst_7 : Fintype ι
inst_8 : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst_9 : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst_10 : (i : ι) → (k : κ i) → Module.{u_1, u_7} 𝕜 (α i k)
x : (i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i
hp : p ≠ ∞
this : 0 < p.toReal
inr :
  HPow.hPow (α := ℝ≥0)
      (∑ x_1 : ι,
        HPow.hPow (α := ℝ≥0)
            (∑ i : κ x_1,
              nnnorm (E := α x_1 i)
                  (x (Sigma.mk (β := fun (i : ι) ↦ κ i) x_1 i) :
                    (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ)))
                      (Sigma.mk (β := fun (i : ι) ↦ κ i) x_1 i)) ^
                p.toReal)
            (1 / p.toReal) ^
          p.toReal)
      (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (∑ i : Sigma κ, ‖x i‖₊ ^ p.toReal) (1 / p.toReal)
⊢ HPow.hPow (α := ℝ≥0)
      (∑ x_1 : ι,
        HPow.hPow (α := ℝ≥0)
            (∑ i : κ x_1,
              nnnorm.{u_7} (E := α x_1 i)
                  (ofLp (p := p)
                    (ofLp (p := p)
                      (((WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ))) ≪≫ₗ
                                LinearEquiv.piCurry 𝕜 (κ := κ) α ≪≫ₗ
                              LinearEquiv.piCongrRight (φ := fun (i : ι) ↦ (j : κ i) → α i j) (ψ := fun (x : ι) ↦
                                WithLp p ((j : κ x) → α x j)) fun (x : ι) ↦
                                LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((j : κ x) → α x j))) ≪≫ₗ
                            LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((i : ι) → WithLp p ((j : κ i) → α i j))) :
                          (a : PiLp p fun (i : Sigma κ) ↦ α i.fst i.snd) → PiLp p fun (i : ι) ↦ PiLp p (α i))
                        (Equiv.invFun
                          (AddEquiv.toEquiv (WithLp.addEquiv p ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ)))))
                          x))
                      x_1)
                    i) ^
                p.toReal)
            (1 / p.toReal) ^
          p.toReal)
      (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0)
      (∑ i : Sigma κ,
        ‖(Equiv.invFun (AddEquiv.toEquiv (WithLp.addEquiv p ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ)))))
                  x).ofLp
              i‖₊ ^
          p.toReal)
      (1 / p.toReal)

Tactic:
dsimp [Sigma.curry]

Premises used: Sigma.curry
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p_1 : ℝ≥0∞
𝕜 : Type u_1
ι_1 : Type u_2
α_1 : ι_1 → Type u_3
β : ι_1 → Type u_4
hp_1 : Fact (1 ≤ p_1)
inst : Fintype ι_1
inst_1 : Semiring 𝕜
inst_2 : (i : ι_1) → SeminormedAddCommGroup (α_1 i)
inst_3 : (i : ι_1) → SeminormedAddCommGroup (β i)
inst_4 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (α_1 i)
inst_5 : (i : ι_1) → Module.{u_1, u_4} 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
inst_7 : Fintype ι
inst_8 : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst_9 : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst_10 : (i : ι) → (k : κ i) → Module.{u_1, u_7} 𝕜 (α i k)
x : (i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i
hp : p ≠ ∞
this : 0 < p.toReal
inr :
  HPow.hPow (α := ℝ≥0)
      (∑ x_1 : ι,
        HPow.hPow (α := ℝ≥0)
            (∑ i : κ x_1,
              nnnorm (E := α x_1 i)
                  (x (Sigma.mk (β := fun (i : ι) ↦ κ i) x_1 i) :
                    (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ)))
                      (Sigma.mk (β := fun (i : ι) ↦ κ i) x_1 i)) ^
                p.toReal)
            p.toReal⁻¹ ^
          p.toReal)
      p.toReal⁻¹ =
    HPow.hPow (α := ℝ≥0) (∑ i : Sigma κ, ‖x i‖₊ ^ p.toReal) p.toReal⁻¹
inr₁ :
  HPow.hPow (α := ℝ≥0)
      (∑ x_1 : ι,
        ∑ i : κ x_1,
          nnnorm (E := α x_1 i)
              (x (Sigma.mk (β := fun (i : ι) ↦ κ i) x_1 i) :
                (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) (Sigma.mk (β := fun (i : ι) ↦ κ i) x_1 i)) ^
            p.toReal)
      p.toReal⁻¹ =
    HPow.hPow (α := ℝ≥0) (∑ i : Sigma κ, ‖x i‖₊ ^ p.toReal) p.toReal⁻¹
inr₂ :
  HPow.hPow (α := ℝ≥0)
      (∑ x_1 : ι,
        ∑ i : κ x_1,
          nnnorm (E := α x_1 i)
              (x (Sigma.mk (β := fun (i : ι) ↦ κ i) x_1 i) :
                (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) (Sigma.mk (β := fun (i : ι) ↦ κ i) x_1 i)) ^
            p.toReal)
      p.toReal⁻¹ =
    HPow.hPow (α := ℝ≥0) (∑ i ∈ Finset.sigma (α := κ) Finset.univ fun (x : ι) ↦ Finset.univ, ‖x i‖₊ ^ p.toReal)
      p.toReal⁻¹
⊢ HPow.hPow (α := ℝ≥0)
      (∑ x_1 : ι,
        HPow.hPow (α := ℝ≥0)
            (∑ i : κ x_1,
              nnnorm (E := α x_1 i)
                  (x (Sigma.mk (β := fun (i : ι) ↦ κ i) x_1 i) :
                    (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ)))
                      (Sigma.mk (β := fun (i : ι) ↦ κ i) x_1 i)) ^
                p.toReal)
            (1 / p.toReal) ^
          p.toReal)
      (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (∑ i : Sigma κ, ‖x i‖₊ ^ p.toReal) (1 / p.toReal)

Tactic:
simp_rw [one_div, NNReal.rpow_inv_rpow this.ne', ← Finset.univ_sigma_univ, Finset.sum_sigma]

Premises used: NNReal.rpow_inv_rpow, Finset.sum_sigma, Finset.univ_sigma_univ, LT.lt.ne', one_div