awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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⁻¹
⊢ 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)
have 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⁻¹
Tactic: simp_rw [one_div, NNReal.rpow_inv_rpow this.ne', ← Finset.univ_sigma_univ, Finset.sum_sigma]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
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
⊢ Norm.norm (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)))) =
    Norm.norm (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))
have this : 0 < p.toReal
Tactic: have : 0 < p.toReal := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
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
⊢ Norm.norm (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)))) =
    Norm.norm (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))
have hpt : p ≠ ∞
Tactic: have hpt : p ≠ ⊤ := (toReal_pos_iff_ne_top p).mp this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
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‖₊
have this : Nonempty ι
Tactic: haveI : Nonempty ι := ⟨i⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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 ∞)
⊢ nnnorm (E := PiLp ∞ β) (single ∞ (β := β) i b) = ‖b‖₊
have top : ⨆ (i_1 : ι), ‖ofLp (p := ∞) (single ∞ (β := β) i b) i_1‖₊ = ‖b‖₊
Tactic: simp_rw [nnnorm_eq_ciSup]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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‖₊
have top : ∀ (j : ι), ‖ofLp (p := ∞) (single ∞ (β := β) i b) j‖₊ ≤ ‖b‖₊
Tactic: refine
      ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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‖₊
⊢ ⨆ (i_1 : ι), ‖ofLp (p := ∞) (single ∞ (β := β) i b) i_1‖₊ = ‖b‖₊
have top₁ : ∀ (n : ℝ≥0) (hn : n < ‖b‖₊), ‖b‖₊ = ‖ofLp (p := ∞) (single ∞ (β := β) i b) i‖₊
Tactic: refine
      ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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 : ι
⊢ ‖ofLp (p := ∞) (single ∞ (β := β) i b) j‖₊ ≤ ‖b‖₊
have top : ‖ofLp (p := ∞) (single ∞ (β := β) i b) i‖₊ ≤ ‖b‖₊
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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‖₊
⊢ ‖ofLp (p := ∞) (single ∞ (β := β) i b) j‖₊ ≤ ‖b‖₊
have top₁ : ∀ (hij : i ≠ j), ‖ofLp (p := ∞) (single ∞ (β := β) i b) j‖₊ ≤ ‖b‖₊
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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 ∞)
⊢ ‖ofLp (p := ∞) (single ∞ (β := β) i b) i‖₊ ≤ ‖b‖₊
have top : ‖b‖₊ ≤ ‖b‖₊
Tactic: rw [single_eq_same]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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‖₊
⊢ ‖b‖₊ = ‖ofLp (p := ∞) (single ∞ (β := β) i b) i‖₊
have top : ‖b‖₊ = ‖b‖₊
Tactic: rw [single_eq_same]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
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∞))
⊢ nnnorm (E := PiLp (↑p : ℝ≥0∞) β) (single (↑p : ℝ≥0∞) (β := β) i b) = ‖b‖₊
have hp0 : (↑p : ℝ) ≠ 0
Tactic: have hp0 : (p : ℝ) ≠ 0 :=
      mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ nnnorm (E := PiLp (↑p : ℝ≥0∞) β) (single (↑p : ℝ≥0∞) (β := β) i b) = ‖b‖₊
have coe : ∀ (x : ι), x ≠ i → ‖ofLp (p := (↑p : ℝ≥0∞)) (single (↑p : ℝ≥0∞) (β := β) i b) x‖₊ ^ (↑p : ℝ) = 0
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ ‖ofLp (p := (↑p : ℝ≥0∞)) (single (↑p : ℝ≥0∞) (β := β) i b) j‖₊ ^ (↑p : ℝ) = 0
have coe₁ : nnnorm.{u_4} (E := β j) 0 ^ (↑p : ℝ) = 0
Tactic: rw [toLp_apply, single_eq_of_ne _ hij, nnnorm_zero, NNReal.zero_rpow hp0]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ ‖ofLp (p := (↑p : ℝ≥0∞)) (single (↑p : ℝ≥0∞) (β := β) i b) j‖₊ ^ (↑p : ℝ) = 0
have coe₂ : HPow.hPow (α := ℝ≥0) 0 (↑p : ℝ) = 0
Tactic: rw [toLp_apply, single_eq_of_ne _ hij, nnnorm_zero, NNReal.zero_rpow hp0]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ ‖ofLp (p := (↑p : ℝ≥0∞)) (single (↑p : ℝ≥0∞) (β := β) i b) j‖₊ ^ (↑p : ℝ) = 0
have coe₃ : Eq (α := ℝ≥0) 0 0
Tactic: rw [toLp_apply, single_eq_of_ne _ hij, nnnorm_zero, NNReal.zero_rpow hp0]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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 ι
⊢ ‖single p (β := β) i b‖₊ = ‖b‖₊
have top : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)], nnnorm (E := PiLp ∞ β) (single ∞ (β := β) 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]
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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‖₊
⊢ ‖single p (β := β) i b‖₊ = ‖b‖₊
have coe : ∀ (p : ℝ≥0) [hp : Fact (1 ≤ (↑p : ℝ≥0∞))], nnnorm (E := PiLp (↑p : ℝ≥0∞) β) (single (↑p : ℝ≥0∞) (β := β) 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]
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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 (single p (β := β) i b₁) (single p (β := β) i b₂) = nndist b₁ b₂
have rw : ‖single p (β := β) i b₁ - single p (β := β) i b₂‖₊ = nndist b₁ b₂
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← single_sub, nnnorm_single]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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₂
⊢ nndist (single p (β := β) i b₁) (single p (β := β) i b₂) = nndist b₁ b₂
have rw₁ : ‖single p (β := β) i b₁ - single p (β := β) i b₂‖₊ = ‖b₁ - b₂‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← single_sub, nnnorm_single]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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₂‖₊
⊢ nndist (single p (β := β) i b₁) (single p (β := β) i b₂) = nndist b₁ b₂
have rw₂ : ‖single p (β := β) i (b₁ - b₂)‖₊ = ‖b₁ - b₂‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← single_sub, nnnorm_single]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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₂‖₊
⊢ nndist (single p (β := β) i b₁) (single p (β := β) i b₂) = nndist b₁ b₂
have rw₃ : ‖b₁ - b₂‖₊ = ‖b₁ - b₂‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← single_sub, nnnorm_single]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
have inl : ∀ (h : p = ∞), ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
Tactic: rcases p.dichotomy with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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‖₊
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
have inr : ∀ (h : 1 ≤ p.toReal),
  ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
Tactic: rcases p.dichotomy with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
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
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
have ne_zero : p.toReal ≠ 0
Tactic: have ne_zero : p.toReal ≠ 0 := (zero_lt_one.trans_le h).ne'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
have inr : HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖Function.const ι b x‖₊ ^ p.toReal) (1 / p.toReal) =
  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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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‖₊
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
have inr₁ : HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖b‖₊ ^ p.toReal) (1 / p.toReal) =
  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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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‖₊
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
have inr₂ : (Finset.card.{u_2} (α := ι) Finset.univ • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
  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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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‖₊
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
have inr₃ : (Fintype.card ι • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
  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]