awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_5
κ : ι → Type u_6
p : ℝ≥0∞
inst_1 : Fact (1 ≤ p)
inst_2 : Fintype ι
inst_3 : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst_4 : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst_5 : (i : ι) → (k : κ i) → Module.{u_1, u_7} 𝕜 (α i k)
f : PiLp p fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))
⊢ Eq (α := PiLp p fun (i : ι) ↦ PiLp p (α i))
    ((LinearIsometryEquiv.piLpCurry 𝕜 (κ := κ) p α :
          (a : PiLp p fun (i : Sigma κ) ↦ α i.fst i.snd) → PiLp p fun (i : ι) ↦ PiLp p (α i))
        f :
      PiLp p fun (i : ι) ↦ PiLp p (α i))
    (toLp p fun (i : ι) ↦ toLp p (Sigma.curry (β := κ) (γ := α) f.ofLp i) :
      WithLp p ((i : ι) → WithLp p ((y : κ i) → α i y)))

Tactic:
rfl

Premises used: Sigma.curry, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_5
κ : ι → Type u_6
p : ℝ≥0∞
inst_1 : Fact (1 ≤ p)
inst_2 : Fintype ι
inst_3 : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst_4 : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst_5 : (i : ι) → (k : κ i) → Module.{u_1, u_7} 𝕜 (α i k)
f : PiLp p fun (i : ι) ↦ PiLp p (α i)
⊢ Eq (α := PiLp p fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ)))
    ((LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCurry 𝕜 (κ := κ) p α) :
          (a : PiLp p fun (i : ι) ↦ PiLp p (α i)) → PiLp p fun (i : Sigma κ) ↦ α i.fst i.snd)
        f :
      PiLp p fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ)))
    (toLp p (Sigma.uncurry (β := κ) (γ := α) fun (i : ι) (j : κ i) ↦ (f.ofLp i).ofLp j) :
      WithLp p ((x : Sigma κ) → α (x.fst (β := κ)) (x.snd (β := κ))))

Tactic:
rfl

Premises used: Sigma.uncurry, rfl
-- 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
α : ι ⊕ κ → Type u_7
inst_6 : Fintype ι
inst_7 : Fintype κ
inst_8 : (i : ι ⊕ κ) → SeminormedAddCommGroup (α i)
inst_9 : (i : ι ⊕ κ) → Module.{u_1, u_7} 𝕜 (α i)
x : (i : ι ⊕ κ) → α i
inst_10 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
__LinearEquiv : WithLp ∞ ((i : ι ⊕ κ) → α i) ≃ₗ[𝕜]
  WithLp ∞ (WithLp ∞ ((i : ι) → α (Sum.inl i)) × WithLp ∞ ((i : κ) → α (Sum.inr i))) :=
  WithLp.linearEquiv ∞ 𝕜 ((i : ι ⊕ κ) → α i) ≪≫ₗ LinearEquiv.sumPiEquivProdPi 𝕜 ι κ α ≪≫ₗ
      LinearEquiv.prodCongr (LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((s : ι) → α (Sum.inl s))))
        (LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((t : κ) → α (Sum.inr t)))) ≪≫ₗ
    LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 (WithLp ∞ ((s : ι) → α (Sum.inl s)) × WithLp ∞ ((t : κ) → α (Sum.inr t))))
⊢ Norm.norm (E := WithLp ∞ (WithLp ∞ ((i : ι) → α (Sum.inl i)) × WithLp ∞ ((i : κ) → α (Sum.inr i))))
      ((WithLp.linearEquiv ∞ 𝕜 ((i : ι ⊕ κ) → α i) ≪≫ₗ LinearEquiv.sumPiEquivProdPi 𝕜 ι κ α ≪≫ₗ
                LinearEquiv.prodCongr (LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((s : ι) → α (Sum.inl s))))
                  (LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((t : κ) → α (Sum.inr t)))) ≪≫ₗ
              LinearEquiv.symm
                (WithLp.linearEquiv ∞ 𝕜 (WithLp ∞ ((s : ι) → α (Sum.inl s)) × WithLp ∞ ((t : κ) → α (Sum.inr t)))) :
            (a : WithLp ∞ ((i : ι ⊕ κ) → α i)) →
              WithLp ∞ (WithLp ∞ ((i : ι) → α (Sum.inl i)) × WithLp ∞ ((i : κ) → α (Sum.inr i))))
          (((LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((i : ι ⊕ κ) → α i)) :
                ((i : ι ⊕ κ) → α i) ≃ₗ[𝕜] WithLp ∞ ((i : ι ⊕ κ) → α i)) :
              (a : (i : ι ⊕ κ) → α i) → WithLp ∞ ((i : ι ⊕ κ) → α i))
            x) :
        WithLp ∞ (WithLp ∞ ((i : ι) → α (Sum.inl i)) × WithLp ∞ ((i : κ) → α (Sum.inr i)))) =
    Norm.norm (E := WithLp ∞ ((i : ι ⊕ κ) → α i))
      (((LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((i : ι ⊕ κ) → α i)) :
              ((i : ι ⊕ κ) → α i) ≃ₗ[𝕜] WithLp ∞ ((i : ι ⊕ κ) → α i)) :
            (a : (i : ι ⊕ κ) → α i) → WithLp ∞ ((i : ι ⊕ κ) → α i))
          x :
        WithLp ∞ ((i : ι ⊕ κ) → α i))

Tactic:
simp [← Finset.univ_disjSum_univ, Finset.sup_disjSum, Pi.norm_def]

Premises used: Finset.univ_disjSum_univ, Pi.norm_def, Finset.sup_disjSum
-- 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∞
α : ι ⊕ κ → Type u_7
inst_6 : Fintype ι
inst_7 : Fintype κ
inst_8 : Fact (1 ≤ p)
inst_9 : (i : ι ⊕ κ) → SeminormedAddCommGroup (α i)
inst_10 : (i : ι ⊕ κ) → Module.{u_1, u_7} 𝕜 (α i)
x : (i : ι ⊕ κ) → α i
hp : 1 ≤ p.toReal
⊢ 0 < p.toReal

Tactic:
positivity
-- 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∞
α : ι ⊕ κ → Type u_7
inst_6 : Fintype ι
inst_7 : Fintype κ
inst_8 : Fact (1 ≤ p)
inst_9 : (i : ι ⊕ κ) → SeminormedAddCommGroup (α i)
inst_10 : (i : ι ⊕ κ) → Module.{u_1, u_7} 𝕜 (α i)
x : (i : ι ⊕ κ) → α i
hp : 1 ≤ p.toReal
⊢ 0 < p.toReal

Tactic:
have : 0 < p.toReal := by positivity
-- 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∞
α : ι ⊕ κ → Type u_7
inst_6 : Fintype ι
inst_7 : Fintype κ
inst_8 : Fact (1 ≤ p)
inst_9 : (i : ι ⊕ κ) → SeminormedAddCommGroup (α i)
inst_10 : (i : ι ⊕ κ) → Module.{u_1, u_7} 𝕜 (α i)
x : (i : ι ⊕ κ) → α i
hp : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ p ≠ ∞

Tactic:
have hpt : p ≠ ⊤ := (toReal_pos_iff_ne_top p).mp this
-- 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∞
α : ι ⊕ κ → Type u_7
inst_6 : Fintype ι
inst_7 : Fintype κ
inst_8 : Fact (1 ≤ p)
inst_9 : (i : ι ⊕ κ) → SeminormedAddCommGroup (α i)
inst_10 : (i : ι ⊕ κ) → Module.{u_1, u_7} 𝕜 (α i)
x : (i : ι ⊕ κ) → α i
hp : 1 ≤ p.toReal
this : 0 < p.toReal
hpt : p ≠ ∞
⊢ nnnorm (E := WithLp p (WithLp p ((i : ι) → α (Sum.inl i)) × WithLp p ((i : κ) → α (Sum.inr i))))
      ((WithLp.linearEquiv p 𝕜 ((i : ι ⊕ κ) → α i) ≪≫ₗ LinearEquiv.sumPiEquivProdPi 𝕜 ι κ α ≪≫ₗ
                LinearEquiv.prodCongr (LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((s : ι) → α (Sum.inl s))))
                  (LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((t : κ) → α (Sum.inr t)))) ≪≫ₗ
              LinearEquiv.symm
                (WithLp.linearEquiv p 𝕜 (WithLp p ((s : ι) → α (Sum.inl s)) × WithLp p ((t : κ) → α (Sum.inr t)))) :
            (a : WithLp p ((i : ι ⊕ κ) → α i)) →
              WithLp p (WithLp p ((i : ι) → α (Sum.inl i)) × WithLp p ((i : κ) → α (Sum.inr i))))
          (((LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((i : ι ⊕ κ) → α i)) :
                ((i : ι ⊕ κ) → α i) ≃ₗ[𝕜] WithLp p ((i : ι ⊕ κ) → α i)) :
              (a : (i : ι ⊕ κ) → α i) → WithLp p ((i : ι ⊕ κ) → α i))
            x) :
        WithLp p (WithLp p ((i : ι) → α (Sum.inl i)) × WithLp p ((i : κ) → α (Sum.inr i)))) =
    nnnorm (E := WithLp p ((i : ι ⊕ κ) → α i))
      (((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 [nnnorm_eq_sum hpt, WithLp.prod_nnnorm_eq_add hpt, NNReal.rpow_inv_rpow this.ne']

Premises used: WithLp.prod_nnnorm_eq_add, NNReal.rpow_inv_rpow, LT.lt.ne', PiLp.nnnorm_eq_sum
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b : β i
⊢ Nonempty ι

Tactic:
haveI : Nonempty ι := ⟨i⟩
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
top : ⨆ (i_1 : ι), ‖ofLp (p := ∞) (single ∞ (β := β) i b) i_1‖₊ = ‖b‖₊
⊢ nnnorm (E := PiLp ∞ β) (single ∞ (β := β) i b) = ‖b‖₊

Tactic:
simp_rw [nnnorm_eq_ciSup]

Premises used: PiLp.nnnorm_eq_ciSup
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
⊢ ⨆ (i_1 : ι), ‖ofLp (p := ∞) (single ∞ (β := β) i b) i_1‖₊ = ‖b‖₊

Tactic:
ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩

Premises used: ciSup_eq_of_forall_le_of_forall_lt_exists_gt, LT.lt.trans_eq, Exists.intro
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
top : ∀ (j : ι), ‖ofLp (p := ∞) (single ∞ (β := β) i b) j‖₊ ≤ ‖b‖₊
top₁ : ∀ (n : ℝ≥0) (hn : n < ‖b‖₊), ‖b‖₊ = ‖ofLp (p := ∞) (single ∞ (β := β) i b) i‖₊
⊢ ⨆ (i_1 : ι), ‖ofLp (p := ∞) (single ∞ (β := β) i b) i_1‖₊ = ‖b‖₊

Tactic:
refine
      ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩

Premises used: ciSup_eq_of_forall_le_of_forall_lt_exists_gt, LT.lt.trans_eq, Exists.intro
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
j : ι
top : ‖ofLp (p := ∞) (single ∞ (β := β) i b) i‖₊ ≤ ‖b‖₊
top₁ : ∀ (hij : i ≠ j), ‖ofLp (p := ∞) (single ∞ (β := β) i b) j‖₊ ≤ ‖b‖₊
⊢ ‖ofLp (p := ∞) (single ∞ (β := β) i b) j‖₊ ≤ ‖b‖₊

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
top top₁ : ‖b‖₊ ≤ ‖b‖₊
⊢ ‖ofLp (p := ∞) (single ∞ (β := β) i b) i‖₊ ≤ ‖b‖₊

Tactic:
rw [single_eq_same]

Premises used: PiLp.single_eq_same
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
j : ι
hij : i ≠ j
⊢ ‖ofLp (p := ∞) (single ∞ (β := β) i b) j‖₊ ≤ ‖b‖₊

Tactic:
simp [hij]
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
n : ℝ≥0
hn : n < ‖b‖₊
top top₁ : ‖b‖₊ = ‖b‖₊
⊢ ‖b‖₊ = ‖ofLp (p := ∞) (single ∞ (β := β) i b) i‖₊

Tactic:
rw [single_eq_same]

Premises used: PiLp.single_eq_same
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ (↑p : ℝ≥0∞))
⊢ (↑p : ℝ) ≠ 0

Tactic:
have hp0 : (p : ℝ) ≠ 0 :=
      mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ (↑p : ℝ≥0∞))
hp0 : (↑p : ℝ) ≠ 0
coe : ∀ (x : ι), x ≠ i → ‖ofLp (p := (↑p : ℝ≥0∞)) (single (↑p : ℝ≥0∞) (β := β) i b) x‖₊ ^ (↑p : ℝ) = 0
⊢ nnnorm (E := PiLp (↑p : ℝ≥0∞) β) (single (↑p : ℝ≥0∞) (β := β) i b) = ‖b‖₊

Tactic:
rw [nnnorm_eq_sum ENNReal.coe_ne_top, ENNReal.coe_toReal, Fintype.sum_eq_single i,
      toLp_apply, single_eq_same, ← NNReal.rpow_mul, one_div,
      mul_inv_cancel₀ hp0, NNReal.rpow_one]

Premises used: mul_inv_cancel₀, ENNReal.coe_toReal, NNReal.rpow_mul, PiLp.single_eq_same, PiLp.toLp_apply, one_div, PiLp.nnnorm_eq_sum, NNReal.rpow_one, ENNReal.coe_ne_top, Fintype.sum_eq_single
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ (↑p : ℝ≥0∞))
hp0 : (↑p : ℝ) ≠ 0
j : ι
hij : j ≠ i
coe : ‖ofLp (p := (↑p : ℝ≥0∞)) (single (↑p : ℝ≥0∞) (β := β) i b) j‖₊ ^ (↑p : ℝ) = 0
coe₁ : nnnorm.{u_4} (E := β j) 0 ^ (↑p : ℝ) = 0
coe₂ : HPow.hPow (α := ℝ≥0) 0 (↑p : ℝ) = 0
coe₃ coe₄ : Eq (α := ℝ≥0) 0 0
⊢ ‖ofLp (p := (↑p : ℝ≥0∞)) (single (↑p : ℝ≥0∞) (β := β) i b) j‖₊ ^ (↑p : ℝ) = 0

Tactic:
rw [toLp_apply, single_eq_of_ne _ hij, nnnorm_zero, NNReal.zero_rpow hp0]

Premises used: NNReal.zero_rpow, PiLp.single_eq_of_ne, nnnorm_zero, PiLp.toLp_apply
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
top : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)], nnnorm (E := PiLp ∞ β) (single ∞ (β := β) i b) = ‖b‖₊
coe :
  ∀ (p : ℝ≥0) [hp : Fact (1 ≤ (↑p : ℝ≥0∞))], nnnorm (E := PiLp (↑p : ℝ≥0∞) β) (single (↑p : ℝ≥0∞) (β := β) i b) = ‖b‖₊
⊢ ‖single p (β := β) i b‖₊ = ‖b‖₊

Tactic:
induction p generalizing hp with
  | top =>
    simp_rw [nnnorm_eq_ciSup]
    refine
      ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩
    · obtain rfl | hij := Decidable.eq_or_ne i j
      · rw [single_eq_same]
      · simp [hij]
    · rw [single_eq_same]
  | coe p =>
    have hp0 : (p : ℝ) ≠ 0 :=
      mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
    rw [nnnorm_eq_sum ENNReal.coe_ne_top, ENNReal.coe_toReal, Fintype.sum_eq_single i,
      toLp_apply, single_eq_same, ← NNReal.rpow_mul, one_div,
      mul_inv_cancel₀ hp0, NNReal.rpow_one]
    intro j hij
    rw [toLp_apply, single_eq_of_ne _ hij, nnnorm_zero, NNReal.zero_rpow hp0]

Premises used: ciSup_eq_of_forall_le_of_forall_lt_exists_gt, ENNReal.coe_toReal, NNReal.rpow_mul, PiLp.nnnorm_eq_ciSup, LT.lt.trans_eq, nnnorm_zero, PiLp.single_eq_same, PiLp.toLp_apply, one_div, Exists.intro, NNReal.rpow_one, rfl, Fintype.sum_eq_single
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b : β i
⊢ ‖toLp p (Pi.single (M := β) i b)‖₊ = ‖b‖₊

Tactic:
nnnorm_single p β i b

Premises used: setOf, PiLp.nnnorm_single
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b : β i
⊢ ‖single p (β := β) i b‖ = ‖b‖

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_single p β i b

Premises used: congr_arg, PiLp.nnnorm_single, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b : β i
⊢ ‖toLp p (Pi.single (M := β) i b)‖ = ‖b‖

Tactic:
norm_single p β i b

Premises used: setOf, PiLp.norm_single
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b₁ b₂ : β i
rw : ‖single p (β := β) i b₁ - single p (β := β) i b₂‖₊ = nndist b₁ b₂
rw₁ : ‖single p (β := β) i b₁ - single p (β := β) i b₂‖₊ = ‖b₁ - b₂‖₊
rw₂ : ‖single p (β := β) i (b₁ - b₂)‖₊ = ‖b₁ - b₂‖₊
rw₃ rw₄ : ‖b₁ - b₂‖₊ = ‖b₁ - b₂‖₊
⊢ nndist (single p (β := β) i b₁) (single p (β := β) i b₂) = nndist b₁ b₂

Tactic:
rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← single_sub, nnnorm_single]

Premises used: PiLp.single_sub, PiLp.nnnorm_single, nndist_eq_nnnorm
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b₁ b₂ : β i
⊢ nndist (toLp p (Pi.single (M := β) i b₁)) (toLp p (Pi.single (M := β) i b₂)) = nndist b₁ b₂

Tactic:
nndist_single_same p β i b₁ b₂

Premises used: setOf, PiLp.nndist_single_same
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b₁ b₂ : β i
⊢ dist (single p (β := β) i b₁) (single p (β := β) i b₂) = dist b₁ b₂

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) <| nndist_single_same p β i b₁ b₂

Premises used: setOf, PiLp.nndist_single_same, congr_arg, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b₁ b₂ : β i
⊢ dist (toLp p (Pi.single (M := β) i b₁)) (toLp p (Pi.single (M := β) i b₂)) = dist b₁ b₂

Tactic:
dist_single_same p β i b₁ b₂

Premises used: PiLp.dist_single_same, setOf
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b₁ b₂ : β i
⊢ edist (single p (β := β) i b₁) (single p (β := β) i b₂) = edist b₁ b₂

Tactic:
simp only [edist_nndist, nndist_single_same p β i b₁ b₂]

Premises used: PiLp.nndist_single_same, edist_nndist
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : DecidableEq ι
i : ι
b₁ b₂ : β i
⊢ edist (toLp p (Pi.single (M := β) i b₁)) (toLp p (Pi.single (M := β) i b₂)) = edist b₁ b₂

Tactic:
edist_single_same p β i b₁ b₂

Premises used: setOf, PiLp.edist_single_same
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
inl :
  ∀ (h : p = ∞), ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr :
  ∀ (h : 1 ≤ p.toReal),
    ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊

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

Premises used: ENNReal.dichotomy
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
h : p = ∞
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊

Tactic:
False.elim (hp h)

Premises used: False.elim
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
h : p = ∞
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊

Tactic:
exact False.elim (hp h)

Premises used: False.elim
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
h : 1 ≤ p.toReal
⊢ p.toReal ≠ 0

Tactic:
have ne_zero : p.toReal ≠ 0 := (zero_lt_one.trans_le h).ne'
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
h : 1 ≤ p.toReal
ne_zero : p.toReal ≠ 0
inr :
  HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖Function.const ι b x‖₊ ^ p.toReal) (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₁ :
  HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖b‖₊ ^ p.toReal) (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₂ :
  (Finset.card.{u_2} (α := ι) Finset.univ • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₃ :
  (Fintype.card ι • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₄ :
  ((↑(Fintype.card ι) : ℝ≥0) * ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₅ :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * (‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₆ :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * ‖b‖₊ ^ (p.toReal * (1 / p.toReal)) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₇ :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * HPow.hPow (β := ℝ) ‖b‖₊ 1 =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₈ :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * ‖b‖₊ =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₉ :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * ‖b‖₊ =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (ENNReal.toReal 1 / p.toReal) * ‖b‖₊
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊

Tactic:
simp_rw [nnnorm_eq_sum hp, Function.const_apply, Finset.sum_const,
      Finset.card_univ, nsmul_eq_mul, NNReal.mul_rpow, ← NNReal.rpow_mul,
      mul_one_div_cancel ne_zero, NNReal.rpow_one, ENNReal.toReal_div, ENNReal.toReal_one]

Premises used: Function.const_apply, Finset.card_univ, ENNReal.toReal_one, NNReal.rpow_mul, mul_one_div_cancel, nsmul_eq_mul, PiLp.nnnorm_eq_sum, NNReal.rpow_one, ENNReal.toReal_div, NNReal.mul_rpow, Finset.sum_const
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
hp : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
inst_2 : Nonempty ι
b : β
inl :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)],
    nnnorm (E := WithLp ∞ (ι → β)) (toLp ∞ (Function.const ι b)) =
      HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (HDiv.hDiv (α := ℝ≥0∞) 1 ∞).toReal * ‖b‖₊
inr :
  ∀ (hp_1 : ¬p = ∞),
    ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊

Tactic:
rcases em <| p = ∞ with (rfl | hp)

Premises used: em, rfl