Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p✝ : ℝ≥0∞
𝕜 : Type u_1
ι✝ : Type u_2
α✝ : ι✝ → Type u_3
β : ι✝ → Type u_4
hp : Fact (1 ≤ p✝)
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : Semiring 𝕜
inst✝⁸ : (i : ι✝) → SeminormedAddCommGroup (α✝ i)
inst✝⁷ : (i : ι✝) → SeminormedAddCommGroup (β i)
inst✝⁶ : (i : ι✝) → Module 𝕜 (α✝ i)
inst✝⁵ : (i : ι✝) → Module 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
p : ℝ≥0∞
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : Fintype ι
inst✝² : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst✝¹ : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst✝ : (i : ι) → (k : κ i) → Module 𝕜 (α i k)
x : (i : Sigma κ) → (fun i ↦ α i.fst i.snd) i
⊢ ‖((WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α i.fst i.snd) ≪≫ₗ LinearEquiv.piCurry 𝕜 α ≪≫ₗ
            LinearEquiv.piCongrRight fun x ↦ (WithLp.linearEquiv p 𝕜 ((j : κ x) → α x j)).symm) ≪≫ₗ
          (WithLp.linearEquiv p 𝕜 ((i : ι) → WithLp p ((j : κ i) → α i j))).symm)
        ((WithLp.addEquiv p ((i : Sigma κ) → α i.fst i.snd)).invFun x)‖₊ =
    ‖(WithLp.addEquiv p ((i : Sigma κ) → α i.fst i.snd)).invFun x‖₊

Tactic:
obtain rfl | hp := eq_or_ne p ⊤

Goal state after:
case inl
p : ℝ≥0∞
𝕜 : Type u_1
ι✝ : Type u_2
α✝ : ι✝ → Type u_3
β : ι✝ → Type u_4
hp : Fact (1 ≤ p)
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : Semiring 𝕜
inst✝⁸ : (i : ι✝) → SeminormedAddCommGroup (α✝ i)
inst✝⁷ : (i : ι✝) → SeminormedAddCommGroup (β i)
inst✝⁶ : (i : ι✝) → Module 𝕜 (α✝ i)
inst✝⁵ : (i : ι✝) → Module 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst✝² : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst✝¹ : (i : ι) → (k : κ i) → Module 𝕜 (α i k)
x : (i : Sigma κ) → (fun i ↦ α i.fst i.snd) i
inst✝ : Fact (1 ≤ ∞)
__LinearEquiv✝ : (PiLp ∞ fun i ↦ α i.fst i.snd) ≃ₗ[𝕜] PiLp ∞ fun i ↦ PiLp ∞ (α i) :=
  (WithLp.linearEquiv ∞ 𝕜 ((i : Sigma κ) → (fun i ↦ α i.fst i.snd) i) ≪≫ₗ LinearEquiv.piCurry 𝕜 α ≪≫ₗ
      LinearEquiv.piCongrRight fun x ↦ (WithLp.linearEquiv ∞ 𝕜 ((j : κ x) → α x j)).symm) ≪≫ₗ
    (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → WithLp ∞ ((j : κ i) → α i j))).symm
⊢ ‖((WithLp.linearEquiv ∞ 𝕜 ((i : Sigma κ) → α i.fst i.snd) ≪≫ₗ LinearEquiv.piCurry 𝕜 α ≪≫ₗ
            LinearEquiv.piCongrRight fun x ↦ (WithLp.linearEquiv ∞ 𝕜 ((j : κ x) → α x j)).symm) ≪≫ₗ
          (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → WithLp ∞ ((j : κ i) → α i j))).symm)
        ((WithLp.addEquiv ∞ ((i : Sigma κ) → α i.fst i.snd)).invFun x)‖₊ =
    ‖(WithLp.addEquiv ∞ ((i : Sigma κ) → α i.fst i.snd)).invFun x‖₊

case inr
p✝ : ℝ≥0∞
𝕜 : Type u_1
ι✝ : Type u_2
α✝ : ι✝ → Type u_3
β : ι✝ → Type u_4
hp✝ : Fact (1 ≤ p✝)
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : Semiring 𝕜
inst✝⁸ : (i : ι✝) → SeminormedAddCommGroup (α✝ i)
inst✝⁷ : (i : ι✝) → SeminormedAddCommGroup (β i)
inst✝⁶ : (i : ι✝) → Module 𝕜 (α✝ i)
inst✝⁵ : (i : ι✝) → Module 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
p : ℝ≥0∞
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : Fintype ι
inst✝² : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst✝¹ : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst✝ : (i : ι) → (k : κ i) → Module 𝕜 (α i k)
x : (i : Sigma κ) → (fun i ↦ α i.fst i.snd) i
hp : p ≠ ∞
⊢ ‖((WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α i.fst i.snd) ≪≫ₗ LinearEquiv.piCurry 𝕜 α ≪≫ₗ
            LinearEquiv.piCongrRight fun x ↦ (WithLp.linearEquiv p 𝕜 ((j : κ x) → α x j)).symm) ≪≫ₗ
          (WithLp.linearEquiv p 𝕜 ((i : ι) → WithLp p ((j : κ i) → α i j))).symm)
        ((WithLp.addEquiv p ((i : Sigma κ) → α i.fst i.snd)).invFun x)‖₊ =
    ‖(WithLp.addEquiv p ((i : Sigma κ) → α i.fst i.snd)).invFun x‖₊