awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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 ≠ ∞
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inr : Eq (α := ℝ≥0) (∑ i : ι, ‖(c • f).ofLp i‖₊ ^ p.toReal) (∑ i : ι, ‖c‖₊ ^ p.toReal * ‖f.ofLp i‖₊ ^ p.toReal)
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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 ≠ ∞
⊢ Eq (α := ℝ≥0) (∑ i : ι, ‖(c • f).ofLp i‖₊ ^ p.toReal) (∑ i : ι, ‖c‖₊ ^ p.toReal * ‖f.ofLp i‖₊ ^ p.toReal)
have inr : Eq (α := ℝ≥0) (∑ i : ι, ‖(c • f).ofLp i‖₊ ^ p.toReal) (∑ x : ι, (‖c‖₊ * ‖f.ofLp x‖₊) ^ p.toReal)
Tactic: simp_rw [← NNReal.mul_rpow, smul_apply, nnnorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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)
⊢ Eq (α := ℝ≥0) (∑ i : ι, ‖(c • f).ofLp i‖₊ ^ p.toReal) (∑ i : ι, ‖c‖₊ ^ p.toReal * ‖f.ofLp i‖₊ ^ p.toReal)
have inr₁ : Eq (α := ℝ≥0) (∑ x : ι, ‖c • f.ofLp x‖₊ ^ p.toReal) (∑ x : ι, (‖c‖₊ * ‖f.ofLp x‖₊) ^ p.toReal)
Tactic: simp_rw [← NNReal.mul_rpow, smul_apply, nnnorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ 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'‖
have 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'‖
Tactic: rcases p.dichotomy with (rfl | h)
Cleared hypotheses: p, hp, x'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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'‖
⊢ 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'‖
have 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'‖
Tactic: rcases p.dichotomy with (rfl | h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ 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'‖
have 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‖)
Tactic: simp_rw [norm_eq_ciSup]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ 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'‖
have 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)
Tactic: simp only [norm_eq_sum (zero_lt_one.trans_le h)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ 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)
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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 : ι ≃ ι'
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ 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)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ 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))
have 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‖
Tactic: simp only [coe_symm_linearEquiv, LinearEquiv.trans_apply, coe_linearEquiv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ 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‖
have 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)
Tactic: obtain rfl | hp := p.dichotomy
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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)
⊢ 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‖
have 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‖
Tactic: obtain rfl | hp := p.dichotomy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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))
⊢ 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)
have 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‖
Tactic: simp_rw [PiLp.norm_toLp, Pi.norm_def, LinearEquiv.piCongrRight_apply,
        LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.nnnorm_map]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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‖
⊢ 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)
have 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‖₊) : ℝ)
Tactic: simp_rw [PiLp.norm_toLp, Pi.norm_def, LinearEquiv.piCongrRight_apply,
        LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.nnnorm_map]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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‖₊) : ℝ)
⊢ 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)
have 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‖₊) : ℝ)
Tactic: simp_rw [PiLp.norm_toLp, Pi.norm_def, LinearEquiv.piCongrRight_apply,
        LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.nnnorm_map]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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‖₊) : ℝ)
⊢ 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)
have 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‖₊) : ℝ)
Tactic: simp_rw [PiLp.norm_toLp, Pi.norm_def, LinearEquiv.piCongrRight_apply,
        LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.nnnorm_map]