-- 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 : 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
inl :
  ∀ [inst : Fact (LE.le (α := ℝ≥0∞) 1 ∞)],
    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))
inr :
  ∀ (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))
⊢ 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))

Tactic:
obtain rfl | hp := p.dichotomy

Premises used: ENNReal.dichotomy, rfl