Not able to use term of Required type for proof? Bug?

Stream: mathlib4

[Rahul Sahjwani]

So The Proof term requires a term of type \R as visisble in Goals, I get a value of type \R which I want to use for my proof. It's indeed of type \R according #check. Yet an error gets thrown when I try to use it for the proof. I have attached the code and the screenshots below:

Screenshot 2025-01-31 220710.png
Screenshot 2025-01-31 220733.png
Screenshot 2025-01-31 220740.png

import Mathlib.MeasureTheory.Function.EssSup
import Mathlib.MeasureTheory.Function.AEEqFun
import Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
import Mathlib.Analysis.NormedSpace.Multilinear.Basic
import Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
import Mathlib.MeasureTheory.Function.LpSpace
import Mathlib.Analysis.Normed.Module.Dual

import Mathlib.Analysis.Normed.Group.Hom
import Mathlib.Analysis.NormedSpace.IndicatorFunction
import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
import Mathlib.Data.Set.Image
import Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
import Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
import Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
import Mathlib.MeasureTheory.Measure.OpenPos
import Mathlib.MeasureTheory.Measure.Typeclasses
import Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace
import Mathlib.Topology.ContinuousMap.Compact
import Mathlib.Order.Filter.IndicatorFunction

import Mathlib.Analysis.Normed.Operator.LinearIsometry

import Mathlib.MeasureTheory.Integral.Bochner



open MeasureTheory MeasurableSpace VectorSpace Function ENNReal NNReal
 Topology MeasureTheory Uniformity symmDiff LinearIsometry Lp

noncomputable section

#check IsBoundedLinearMap
#check Isometry
#check Lp

/- Let α be our measure space, let μ be a measure on α,
 then our functions will take values over the field 𝕜. -/
variable {α : Type*} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type*}
 [NontriviallyNormedField 𝕜]

--Let r ∈ [0, ∞]
variable {r : ENNReal}

-- Let us use X to denote Lp(μ;𝕜)
variable {X : Lp 𝕜 r μ}
#check X
#check NormedSpace.Dual


/- We Define the Natural Duality paring between Lq and (Lr)* where r and q are
conjugate eponents -/

#check Memℒp
#check instCoeFun
#check Lp.memℒp

#check Memℒp.toLp
#check integral

def NaturalDualityPairing {α : Type*} {m : MeasurableSpace α} (μ : Measure α)
 {r q : ENNReal} (hrq : 1 = 1/q + 1/r)
 [Fact (1 ≤ r)] [Fact (1 ≤ q)] :
 (Lp ℝ q μ) →ₗᵢ[ℝ] (NormedSpace.Dual ℝ (Lp ℝ r μ) ) where
   toFun g := {
     toFun :=by {
        intro f
        let p := (1 : ENNReal)
        have hp : 1/p = 1 := by exact one_div_one
        have hpqr : 1/p = 1/q + 1/r :=by rw[hp]; apply hrq
        have hf : Memℒp f r μ :=by exact Lp.memℒp f
        have hg : Memℒp g q μ := by exact Lp.memℒp g
        let h  := Memℒp.mul hf hg hpqr
        let u (x : α) : ℝ := g (x) * f (x)
        have h' : Memℒp u 1 μ :=by exact h
        let (v : ↥(Lp ℝ 1 μ))  := Memℒp.toLp u h'
        let map_val := integral μ v
        #check map_val
        use map_val
     }
     map_add' := sorry
     map_smul' := sorry
     cont := sorry
   }
   map_add' := sorry
   map_smul' := sorry
   norm_map' := sorry

[Rahul Sahjwani]

I will try to get a minimal working example but I though I should post this just in case there is a simple fix.

[Kim Morrison]

I'm not sure why you are using use, instead of exact, which works here.

[Kim Morrison]

(I looks to me like a bug in use, in any case.)

[Rahul Sahjwani]

Ah sorry I didn't expect it work for exact if it didn't work for use. Thanks for your answer!

[Kyle Miller]

The use x tactic is like doing constructor; exact x (it's a bit more intelligent than that, but this is a first approximation). The issue is that docs#Real is a structure, so constructor succeeds, and the goal is a CauSeq.Completion.Cauchy abs.

[Kim Morrison]

Oops, I'm so used to using refine that I'd forgotten what use actually did.