Issues in !4#2123 (Topology.CompactOpen)

Stream: mathlib4

[Arien Malec]

I looked at !4#2123, and was able to fix a couple of issues. I left continuous_comp' in a place where it's mostly together, but line 148 has an error despite all the types lining up between the Lean 3 and 4 sides and no apparent implicit issues or such. It appears to be an issue where (φ, ψ).fst ∈ {φ : C(α, β) | ⇑φ '' K ⊆ interior L} can be seen as a subset relation in Lean 3 and fails to typecheck in Lean4. It's frustrating because when I give Lean 4 a placeholder, or use library_search I get back the same type that the proof is providing.

(The second issue is is also a mystery to me)...

[Adam Topaz]

It is quite strange, but here is a hacky workaround that works:

      use fun ⟨φ, ψ⟩ ⟨hφ, hψ⟩ =>
        subset_trans ?_ (interior_subset.trans <| image_subset_iff.mp hψ)
      exact hφ

[Adam Topaz]

Even better

      use fun ⟨φ, ψ⟩ ⟨hφ, hψ⟩ =>
        subset_trans (by exact hφ) (interior_subset.trans <| image_subset_iff.mp hψ)

[Kevin Buzzard]

In Lean 3 by exact just changed elaboration order a little (which was very occasionally the key idea)

[Johan Commelin]

Does (hφ:) work?

[Adam Topaz]

not in any way I tried, but I didn't try for too long

[Adam Topaz]

This fails

      use fun ⟨φ, ψ⟩ ⟨hφ, hψ⟩ =>
        subset_trans (hφ : φ '' K ⊆ interior L) (interior_subset.trans <| image_subset_iff.mp hψ)

[Adam Topaz]

Oh, this works:

      use fun ⟨φ, ψ⟩ ⟨(hφ : φ '' K ⊆ interior L), hψ⟩ =>
        subset_trans hφ (interior_subset.trans <| image_subset_iff.mp hψ)

[Adam Topaz]

This is as minimal as I could get it:

      use fun ⟨φ, ψ⟩ ⟨(hφ : _ ⊆ interior _), hψ⟩ =>
        subset_trans hφ (interior_subset.trans <| image_subset_iff.mp hψ)

[Adam Topaz]

maybe interior is the culprit?

[Adam Topaz]

Maybe not, since this also works

      use fun ⟨φ, ψ⟩ ⟨(hφ : _ '' _ ⊆ _), hψ⟩ =>
        subset_trans hφ (interior_subset.trans <| image_subset_iff.mp hψ)

[Arien Malec]

just push whichever of these workarounds you find the least objectionable. by exact hφ highlights the weirdness the best, IMHO

[Kevin Buzzard]

That's so weird that _ '' _ ⊆ _ and _ ⊆ interior _ both work. Presumably _ ⊆ _ does not work? (or you would have mentioned it) (if it works then it's not weird any more)

[Adam Topaz]

that's right, $$_ \subseteq _$$ doesn't work

[Adam Topaz]

I pushed the (hφ : φ '' K ⊆ interior L) variant.

[Adam Topaz]

I also fixed the other error in this file, which was in some calc block.

[Adam Topaz]

The following (from the mathport file) did not work

        calc
          f' x' ∈ f' '' s := mem_image_of_mem f' (us hx')
          _ ⊆ v := hf'
          _ ⊆ n := vn

it results in the following error (on the _ ⊆ v := hf' line)

invalid 'calc' step, failed to synthesize `Trans` instance
  Trans Membership.mem Subset ?m.23225

[Adam Topaz]

Finally, on line 238, we have

theorem compactOpen_eq_Inf_induced :
    (ContinuousMap.compactOpen : TopologicalSpace C(α, β)) =
      ⨅ (s : Set α) (hs : IsCompact s),
        TopologicalSpace.induced (ContinuousMap.restrict s) ContinuousMap.compactOpen := by

and hs results in an unused variables warning. If I replace hs with _ to try to get rid of the warning, I get the error:

elaboration function for 'Lean.Parser.Command.«termExpand_binders%(_=>_)_,_»' has not been implemented
  expand_binders% (f✝ => infᵢ✝ f✝) (_ : IsCompact s),
    TopologicalSpace.induced (ContinuousMap.restrict s) ContinuousMap.compactOpen

This seems like an actual issue that should be resolved IMO

[Matthew Ballard]

Adam Topaz said:

The following (from the mathport file) did not work

        calc
          f' x' ∈ f' '' s := mem_image_of_mem f' (us hx')
          _ ⊆ v := hf'
          _ ⊆ n := vn

it results in the following error (on the _ ⊆ v := hf' line)

invalid 'calc' step, failed to synthesize `Trans` instance
  Trans Membership.mem Subset ?m.23225

Basic question: @[trans] generates Transitive instance?

[Adam Topaz]

That's what it usually does in lean3, but I can only guess that the same holds for lean4 as I haven't done it myself

[Reid Barton]

Adam Topaz said:

If I replace hs with _ to try to get rid of the warning, I get the error:

Does it work with _hs?

[Adam Topaz]

yes it does!

[Adam Topaz]

okay I fixed the remaining errors/warnings

[Adam Topaz]

Why does _hs work but not _?

[Arien Malec]

Adam Topaz said:

okay I fixed the remaining errors/warnings

I already pushed these fixes -- sorry....

[Adam Topaz]

oops :)

[Adam Topaz]

well the file seems to still build even after we both fixed things twice :)

[Arien Malec]

we fixed in exactly the same way....

[Adam Topaz]

yeah I know

[Reid Barton]

I guess because _hs is an identifier and _ is a ... something else, for syntax purposes

[Adam Topaz]

Yeah that makes sense. But I think the syntax _ should be accepted in such situations.

[Ruben Van de Velde]

Yeah, this has been discussed a few times on zulip already. Can't find it now, though

[Pedro Sánchez Terraf]

Adam Topaz said:

The following (from the mathport file) did not work

        calc
          f' x' ∈ f' '' s := mem_image_of_mem f' (us hx')
          _ ⊆ v := hf'
          _ ⊆ n := vn

it results in the following error (on the _ ⊆ v := hf' line)

invalid 'calc' step, failed to synthesize `Trans` instance
  Trans Membership.mem Subset ?m.23225

What is the appropriate way to make this type of proof work again?
I tried putting something like

@[trans]
theorem mem_subset_trans {x : Set γ} (h : a ∈ x) (h' : x ⊆ y) : a ∈ y := by
  exact h' h

before my use case, but it didn't do the trick.

[Anatole Dedecker]

I think this is not the "right" trans. The attribute is for the tactic docs#Mathlib.Tactic.tacticTrans___, what you are looking for is probably docs#Trans.

[Pedro Sánchez Terraf]

Anatole Dedecker said:

I think this is not the "right" trans. The attribute is for the tactic docs#Mathlib.Tactic.tacticTrans___, what you are looking for is probably docs#Trans.

I added

instance : @Trans (Set γ) _ _ Set.Mem Set.Subset Set.Mem := ⟨mem_subset_trans⟩

after the theorem, but it didn't work either. Anyway, I can put it in just one line (is this preferred?) but I would like to know how to add such an instance.

EDIT: Also tried with

instance : @Trans _ (Set γ) _ Set.Mem Set.Subset Set.Mem := ⟨mem_subset_trans⟩

just in case I had messed with the order of variables.