exercise 3.5.12 rewrite with nat literal fails again

Stream: Analysis I

[Rado Kirov]

I thought I understood nat literals but I am stuck on what appears a very basic rewriting again.

Screenshot 2025-07-19 at 8.44.11 AM.png

[Rado Kirov]

Screenshot 2025-07-19 at 8.48.08 AM.png

[Rado Kirov]

Am I correct that the ofNat part matches?
Screenshot 2025-07-19 at 8.52.35 AM.png

[Rado Kirov]

my hypothesis is that actually nat_equiv.symm has implicit args that don't

Screenshot 2025-07-19 at 8.53.30 AM.png

vs

Screenshot 2025-07-19 at 8.54.23 AM.png

but not sure how to resolve that (assuming that's the issue)

[Rado Kirov]

Not sure if this is even a problem because I have example : { x: Object // x ∈ nat } = Nat := by exact rfl

[Edward van de Meent]

well... looking at your first screenshot, i suspect that if you hover over the left 0 in this you'll see a second OfNat.ofNat, which doesn't match with your goal...

[Rado Kirov]

You are absolutely right
Screenshot 2025-07-19 at 9.10.02 AM.png

[Rado Kirov]

This from a lemma I wrote:

lemma nat_equiv_zero : SetTheory.nat_equiv.symm (ofNat(0):Nat) = (0:ℕ) := by
  rw [Equiv.symm_apply_eq]
  rfl

how should I write the lemma so that the rw works?

[Aaron Liu]

Just don't write ofNat(0), the ofNat(n) is for when n is a variable, you should just put 0 instead

[Rado Kirov]

Screenshot 2025-07-19 at 9.14.14 AM.png

[Rado Kirov]

So writing

lemma nat_equiv_zero : SetTheory.nat_equiv.symm 0 = (0:ℕ) := by
  rw [Equiv.symm_apply_eq]
  rfl

doesn't work for the reason above.

Writing

lemma nat_equiv_zero : SetTheory.nat_equiv.symm (0:Nat) = (0:ℕ) := by _

works for the lemma but the rw doesn't apply

[Edward van de Meent]

what is Nat.toSubtype?

[Rado Kirov]

https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_3_1.lean#L383

[Rado Kirov]

Various nat casts begin here - https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_3_1.lean#L583 but I don’t believe toSubtype is specialized on Nat

[Edward van de Meent]

could it be the case that the clue is that there's two nat_equivs? there's SetTheory.Set.nat_equiv (which shows as nat_equiv due to this line, whereas there also is SetTheory.nat_equiv which is a field of the SetTheory structure?

[Edward van de Meent]

i think that rewrite doesn't see through this

[Edward van de Meent]

it seemed weird to me that the infoview was inconsistent between showing nat_equiv with and without namespace

[Edward van de Meent]

all this together seems to suggest that using this lemma should work:

lemma nat_equiv_symm (n : ℕ) : Set.nat_equiv.symm ofNat(n) = ofNat(n) := by
  sorry

[Aaron Liu]

Rado Kirov said:

Screenshot 2025-07-19 at 9.14.14 AM.png

put (0 : Nat) instead of (ofNat(0):Nat)

[Rado Kirov]

Thank you all for the discussion! It gives me some more things to try and will update here when I get back to a computer.

[Rado Kirov]

Yeah, that did it

lemma nat_equiv_symm_zero : SetTheory.Set.nat_equiv.symm 0 = 0 := by

applies well!

[Rado Kirov]

The definitions is here https://github.com/teorth/analysis/blob/b3ee408ab67808b5a768ff808d345501e5b2f40f/analysis/Analysis/Section_3_1.lean#L583 and along with open SetTheory.Set there seems to be non-trivial aliasing. So now I wonder whether this should have been abbrev to avoid these type of issues. Very sharp edge for new learners, didn't even think to look into namespacing and aliasing, and blamed it all on literals.

[Rado Kirov]

Meta-question, could I have done something better debugging earlier - say I have at theorem f a = b that doesn't apply a rw in some complex expression where I 'believe' I see f a. Was there something to hint me that f doesn't match vs a? A slight variation is also some times f a looks that same, but the type of f or a doesn't match or some implicit parameter of f.

[Rado Kirov]

I don't know enough to be giving compiler authors advice, but I wonder if the error messages on rw can be improved with some 'partial matches' info. Here is an example of how TypeScript compiler shows different error message depending on how different branches of an union type match

https://www.typescriptlang.org/play/?#code/GYVwdgxgLglg9mABMAFADwFyIN4Gc4C2ApgPoAOATnGVnoaQCZFFnlU2K5QUxgDmAXwGIAPjnzEScKAAsiFNtVoTGzVpSWIwIAgCN5QgJQ4BAKFMAbIlERpEAXnH1FHOpKYtymgOTehAbktrRABPBydJaTkFDVcVEg91TQAGANNUNENA1BCs8ysbAC9w7D4AQwpdMr4iZWdElyxfNNRCrKA

[Aaron Liu]

There could be a trace option for this (but there isn't), it's not too hard to implement I think

[Aaron Liu]

The function that does the matching is called docs#Lean.Meta.kabstract

[Edward van de Meent]

Rado Kirov said:

So now I wonder whether this should have been abbrev to avoid these type of issues.

i don't think so, i believe you'd run into the same issue