complete_space by cases

Stream: general

[Rémy Degenne]

On branch#Lp_complete , I am working on a proof of completeness of Lp spaces. I did it separately for two cases (p infinite, or not). Now I want to put those together into one final theorem . However I encounter difficulties, illustrated in the following code in which I don't know how to replace the last sorry:

import measure_theory.lp_space

open measure_theory
open_locale ennreal

variables {α E : Type*} [measurable_space α] {p : ℝ≥0∞} {μ : measure α}
  [measurable_space E] [normed_group E] [borel_space E]
  [topological_space.second_countable_topology E] [complete_space E]

lemma complete_space_Lp_of_ne_top [hp : fact(1 ≤ p)] (hp_ne_top : p ≠ ∞) :
  complete_space (Lp E p μ) := sorry

lemma complete_space_Lp_top : complete_space (Lp E ∞ μ) := sorry

lemma complete_space_Lp [hp : fact(1 ≤ p)] : complete_space (Lp E p μ) :=
begin
  by_cases hp_top : p = ∞,
  { have h_eq : Lp E p μ = Lp E ∞ μ, by rw hp_top,
     -- I want to use `complete_space_Lp_top`
    sorry },
  { exact complete_space_Lp_of_ne_top hp_top, },
end

I can prove complete_space (Lp E ∞ μ), but I cannot find a way to get complete_space (Lp E p μ) from that and p = ∞.

[Sebastien Gouezel]

import measure_theory.lp_space

open measure_theory
open_locale ennreal

variables {α E : Type*} [measurable_space α] {p : ℝ≥0∞} {μ : measure α}
  [measurable_space E] [normed_group E] [borel_space E]
  [topological_space.second_countable_topology E] [complete_space E]

lemma complete_space_Lp_of_ne_top [hp : fact(1 ≤ p)] (hp_ne_top : p ≠ ∞) :
  complete_space (Lp E p μ) := sorry

lemma complete_space_Lp_top : complete_space (Lp E ∞ μ) := sorry

lemma complete_space_Lp [hp : fact(1 ≤ p)] : complete_space (Lp E p μ) :=
begin
  by_cases hp_top : p = ∞,
  { convert complete_space_Lp_top,
    apply_instance },
  { exact complete_space_Lp_of_ne_top hp_top, },
end

When you have something which looks like your goal, but in which some things are different from your goal, use convert: it will only leave you with proof goals saying that the things that look different are in fact the same.

[Rémy Degenne]

Thank you! I keep forgetting about that tactic.