Cannot close goal while present in tactic state

Stream: new members

[Josha Dekker]

I'm trying to prove the following. I know how to close the first sorry (but haven't done it yet as I first want to be sure that this will work), but I can't close the goal, even though h_sct is exactly this.

import Mathlib

lemma SecondCountableSpace_from_metric_Lindelof [MetricSpace X] [LindelofSpace X] :
    SecondCountableTopology X := by
  have h_dense : ∀ ε > 0, ∃ s : Set X, s.Countable ∧ ∀ x, ∃ y ∈ s, dist x y ≤ ε := by
    sorry -- cover by ε Metric.closedBall at each x, then extract countable subcover from Lindelöf property
  have h_sct := Metric.secondCountable_of_almost_dense_set h_dense
  sorry -- h_sct gives SecondCountableTopology X, but cannot close the goal through:
  -- exact h_sct
  -- apply h_sct
  -- simp
  -- aesop

If interested, the tactic state just before the second sorry is:

X: Type u_1
inst✝¹: MetricSpace X
inst✝: LindelofSpace X
h_dense: ∀ ε > 0, ∃ s, Set.Countable s ∧ ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε
h_sct: SecondCountableTopology X
⊢ SecondCountableTopology X

What am I doing wrong here?

[Johan Commelin]

What is the error?

[Johan Commelin]

Can you apply that Metric.secondCountable... lemma, without passing in h_dense?

[Josha Dekker]

This is weird: in my MWE above, apply Metric.secondCountable_of_almost_dense_set h_dense does close the goal. However, in Topology/Compactness/Lindelof, I get

tactic 'apply' failed, failed to unify
  SecondCountableTopology X
with
  SecondCountableTopology X
X: Type u
Y: Type v
ι: Type u_1
inst✝³: TopologicalSpace X
inst✝²: TopologicalSpace Y
st: Set X
inst✝¹: MetricSpace X
inst✝: LindelofSpace X
h_dense: ∀ ε > 0, ∃ s, Set.Countable s ∧ ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε
⊢ SecondCountableTopology X

[Josha Dekker]

Where I have:

lemma SecondCountableSpace_of_metric_Lindelof [MetricSpace X] [LindelofSpace X] :
    SecondCountableTopology X := by
  have h_dense : ∀ ε > 0, ∃ s : Set X, s.Countable ∧ ∀ x, ∃ y ∈ s, dist x y ≤ ε := by
    sorry -- cover by ε Metric.closedBall at each x, then extract countable subcover
  apply Metric.secondCountable_of_almost_dense_set h_dense

[Johan Commelin]

Maybe turn on pp.all, or try convert?

[Johan Commelin]

There's probably some implicit argument

[Josha Dekker]

convert reveals the problem:

lemma SecondCountableSpace_from_metric_Lindelof [MetricSpace X] [LindelofSpace X] :
    SecondCountableTopology X := by
  have h_dense : ∀ ε > 0, ∃ s : Set X, s.Countable ∧ ∀ x, ∃ y ∈ s, dist x y ≤ ε := by
    sorry -- cover by ε Metric.closedBall at each x, then extract countable subcover
  convert Metric.secondCountable_of_almost_dense_set h_dense

gives state

X: Type u
Y: Type v
ι: Type u_1
inst✝³: TopologicalSpace X
inst✝²: TopologicalSpace Y
st: Set X
inst✝¹: MetricSpace X
inst✝: LindelofSpace X
h_dense: ∀ ε > 0, ∃ s, Set.Countable s ∧ ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε
⊢ inst✝³ = UniformSpace.toTopologicalSpace

[Josha Dekker]

but I'm not sure how to proceed from there... pp.all gives

tactic 'apply' failed, failed to unify
  @SecondCountableTopology.{u} X
    (@UniformSpace.toTopologicalSpace.{u} X
      (@PseudoMetricSpace.toUniformSpace.{u} X (@MetricSpace.toPseudoMetricSpace.{u} X inst✝¹)))
with
  @SecondCountableTopology.{u} X inst✝³

after

apply Metric.secondCountable_of_almost_dense_set h_dense

[Josha Dekker]

Is Lean considering two different topologies on X here, first the one from [TopologicalSpace X] (present in the file) and then the canonical one from [MetricSpace X]?

[Johan Commelin]

Yes

[Johan Commelin]

So you need to state the lemma in such a way that TopologicalSpace X isn't picked up from the ambient context

[Josha Dekker]

Great, thank you! So I can probably just give it a different name like Z instead of X?

[Ruben Van de Velde]

Yeah

[Josha Dekker]

Thank you, that works!