Tao's Analysis Ch3.3

Stream: Analysis I

[Rado Kirov]

I spend almost a whole day trying to work through ch3.3 exercises, and sadly had a lot less fun with those than ones from the previous chapters. The custom definition of Function(using a Property on x and y, that for a given x is only true for a single y) expands into a unreadable mess with simp, so I resorted to the following tactics:

• applying rewrites without being able to make sense of the intermediate state, hoping for a pass from the checker. Forced me to get a better mental model of how the core really works( also got some great insights from a chat @Chris Bailey at the Berkeley Lean camp)
• for some exercises just mapped in bulk to Mathlib's notion of functions using mk_fn and to_fn and proved it there (without using the built in theorems)
• in some places I tried to undo the automatic expansion, like ext; rw [\<- eval] so I can work with manageable goals

If anyone else is working on those or has solutions handy, would love to chat more - I have two unsolved problems left and probably a lot of clean up on the existing solutions github link.

I made a small repro for one for the more frustrating problems, I don't know how to prove 0 \in Nat or how to show 0 \neq 1 (where Nat is custom addition to the custom SetAxioms, but it has OfNat coersions).

lean4 web repro link

[Vlad]

example : 0 ∈ Nat := (SetTheory.nat_equiv.1 0).2
example : 1 ∈ Nat := (SetTheory.nat_equiv.1 1).2

example : (0 : Nat) ≠ (1 : Nat) := by
  apply SetTheory.nat_equiv.injective.ne; simp

[Rado Kirov]

Thanks! That got me through some counter-examples.

The next exercise I am stuck on has to with inclusion functions. Again the content of the functions is trivial but I am struggling with aligning the subsets/subtypes proofs. The definition of Function doesn't make things easy to see.

I extracted it to the lean4 web playground

[Vlad]

theorem Function.inclusion_comp (X Y Z:Set) (hXY: X ⊆ Y) (hYZ: Y ⊆ Z) :
    Function.inclusion hYZ ○ Function.inclusion hXY =
    Function.inclusion (SetTheory.Set.subset_trans hXY hYZ) := by
  ext x y; simp only [←eval, inclusion_eval, comp_eval]; congr! 1
  generalize_proofs _ h₁ _ h₂
  simp only [(Classical.choose_spec h₂).1, (Classical.choose_spec h₁).1]
  generalize_proofs h₁; rw [(Classical.choose_spec h₁).1]

[Rado Kirov]

Brilliant, some new tricks for me to learn, thanks!

[Terence Tao]

This is useful feedback. I am certainly aware that my textbook definition of a function is significantly more inconvenient to use in Lean than the idiomatic Mathlib functions, and starting from Sec 3.4 onwards I switch solely to the Mathlib functions, but I wanted to demonstrate that the textbook definition was actually implementable in Lean in a way that broadly captures the intended spirit of the book. The API to convert back and forth between the Section 3.3 functions and the Mathlib functions was certainly intended to assist with some of the more challenging proofs, and also to help prepare the reader for the imminent transition to Mathlib functions.

If you have suggestions for hints for some of the problems that can be inserted as comments to the Lean file, to allow other students of the text to focus on the mathematical content of the exercises in the spirit of the original text and not be unduly helpd up by purely technical Lean issues, I'd be happy to accept some PRs in this regard.

[Rado Kirov]

Will definitely try to contribute where I can. I can add some comment hints that would have helped me based on what I knew before starting the exercise and based on the solution I ended up with, but I don't know enough of Lean to know how idiomatic any of this is, so there is a danger to overfitting to my specific solutions. Will keep my eyes open on other new user threads here, and see if multiple journeys through the exercises could have been similarly helped, will contribute more.

Also, while not the goal of the book as you say, actually struggling through the casts, nat literals (as in the other thread by @Dan Abramov ) etc, is probably quite educational for me when I further work with Lean and Mathlib, so trying to fully hide everything Lean technicality from sight won't be right either.

The trouble is that for the Lean specific content unlike the math content, there is no helpful text to go with, no worked out exercises (though I appreciate that some of the math examples do come with proofs, that I can read and to emulated) and no slowly increasing difficulty gradient (admittedly hard to do that concurrently with the mathematical content).

I hope I don't come off as too negative, because I really like the approach of

I wanted to demonstrate that the textbook definition was actually implementable in Lean in a way that broadly captures the intended spirit of the book.

and exactly what I was looking for. The Lean companion has a "you could have invented/formalized Math" feel (like popular posts/articles [1] [2], etc). Of course, just like a lot these posts, there is a bit of sleight-of-hand, by not adding "but it probably won't be as ergonomic as the original" :)

[Dan Abramov]

I haven’t gotten to 3.3 myself yet so I haven’t looked at this discussion but wanted to respond to this:

The trouble is that for the Lean specific content unlike the math content, there is no helpful text to go with, no worked out exercises (though I appreciate that some of the math examples do come with proofs, that I can read and to emulated) and no slowly increasing difficulty gradient (admittedly hard to do that concurrently with the mathematical content).

I don’t think it would be appropriate for this book to spend a ton of space in comments explaining what’s going on, but IMO, there’s an opportunity to build up intuition about these things slightly more gradually. For example, after a block with lemmas for casting, it would help to have an example showing “this lets us do this and that”. So that you can see what these lemmas and casts and simps enable without also trying to solve some other problem later. It also gives a reference for something to “come back to” whenever you’re stuck because it would be a one-liner per pattern you use later.

[Rado Kirov]

With all the help here, I got finally to the last exercise in Ch3.3. I think it is the first time I am defining a function with if-else, and really struggling to expand it properly. The code looks something like this

theorem some_theorem {X Y Z:Set} (hXY: X ∩ Y = ∅) (f: Function X Z) (g: Function Y Z) (x: X): True := by
  set F : Function (X ∪ Y) Z := Function.mk_fn (fun z ↦
      if h : (z.val ∈ X) then f ⟨z.val, h⟩
      else g ⟨z.val, (by
        have h2 := z.property
        rw [SetTheory.Set.mem_union] at h2;
        tauto
      )⟩) with hF
  have hsub := (SetTheory.Set.subset_union_left X Y)
  have F_at_x : F ⟨x.val, hsub x x.property⟩ = f x := by
    simp [hF]
    sorry -- how to expand here?

  -- do same for Y and g
  -- rest of the proof
  tauto

The surrounding proof is just True, I need to learn how to expand F and I think I have hope for the rest of the exercise. Actually, very curious how would the disjoint condition come into play.

playground link

[Aaron Liu]

You can do simp only [F] or dsimp [F] or unfold F

[Rado Kirov]

none of those seem to work

[Aaron Liu]

maybe I forgot how set works

[Damiano Testa]

At some point there was an unfold_let that was later replaced by unfold. I don't remember if that worked with set as well.

[Aaron Liu]

You want to use Function.eval_of

[Rado Kirov]

both dsimp and unfold work as far as the definition is expanded, but the goal is not completed.

[Aaron Liu]

use Function.eval_of, it's stated in a weird way so it won't work with simp

[Rado Kirov]

adding simp [eval, eval_of] makes some changes after also doesn't complete

[Aaron Liu]

Do

    rw [hF, Function.eval_of, dif_pos x.property]

[Rado Kirov]

sadly no. It does work for a more trivial function like mk_fn fun x => f x, so I wonder if I need to something special for the if ... then ... else ...?

[Rado Kirov]

oh, didn't know about dif_pos

[Rado Kirov]

That did it, thanks!

[Rado Kirov]

Hopefully, that will help me complete the glue exercise 3.3.8 e), though still not sure where and how will I use the Disjoint X Y hypothesis.

One quick quesion what is the difference between the four ways here to expand the definition of F simp only [{F or hF}], rw [hF] or unfold F?

[Aaron Liu]

simp only will also do some beta and iota and all the other kinds of reduction

[Aaron Liu]

rw [F] does not work

[Aaron Liu]

rw [hF] will only work if the definition of F is irrelevant for type correctness of the expression being rewritten

[Aaron Liu]

unfold F will just unfold the definition of F

[Rado Kirov]

Hopefully, that will help me complete the glue exercise 3.3.8 e), though still not sure where and how will I use the Disjoint X Y hypothesis.

Ok, I answered my question and finally finished 3.3.8 e) Won't get style points and lot of things to go back to and clean up, but I know the pieces at play.

To answer my own question the disjoint hypothesis is used to prove x \nin X which is needed by dif_neg. It's like I need to drive a little programming language interpreter single evaluation step at time, and at each point I might need to pass some extra proofs to proceed.

One final observation, there is a missing include_eval theorem which is hard to state because it needs to generalize over subset membership information. I tried to add my own, but it is not useful as it only shows .val equality. So I started just extracting subhypothesis of include applications with have to proceed the evaluation without using eval which explodes the goal.

Thanks for all the help here! I plan to keep posting my questions here (or a new sub channel) as I continue working through the chapters.

[Terence Tao]

I'll accept a PR with this eval lemma as a helper lemma. (I didn't work too hard on providing an extensive API here since the Section 3.3 function machinery is to be deprecated by the next section, but it still makes sense to make a small illustration of what a reasonable API is supposed to look like.)

[Rado Kirov]

Sounds good, I will go back and clean up the solutions to attempt only use rw with *_eval theorems. I think I have a clearer picture now that it is best practice to have definitions that are only used by a key API theorems and exercises should only use APIs and seldomly expand underlying definitions.

[Notification Bot]

This topic was moved here from #new members > Tao's Analysis Ch3.3 by Johan Commelin.

[Dan Abramov]

Not sure if this is a related problem or not, but I find that whenever I have Classical.choose ... appearing in my InfoView, I have no idea what's going on and lose track of things.

Screenshot 2025-07-13 at 00.54.28.png

Maybe this is a sign of the proof itself going in the wrong direction, but the way InfoView chooses to fold things (which I'm guessing is another consequence of the chosen formalism) feels very confusing. Would be nice if there was some way to make these printed in some other way.

[Rado Kirov]

I learned that set_option pp.proofs true will configure the pretty-printer to not hide those with ellipsis, but indeed often what you find behind can be quite messy and could be a sign that one should use some theorems instead. Also, I found that sometimes the right helpful theorems (like _eval mentioned there) are missing when writing those you have to work with choose, and choose_spec.

[Dan Abramov]

Hmm ok yeah I shouldn't have waited so long to try that pp option, it does help

[Rado Kirov]

My tactics so far to deal with choose:
1) run some evals backwards to hide it again if possible. Sometimes simp will go too far.
2) create a local proof with have := choose_spec <expr> that will give you some statement about choose <expr> and you can work with that first instead of choose directly.

[Terence Tao]

I havent used it myself but the choose tactic may be friendlier for beginners here.

[Aaron Liu]

the choose tactic works great for me

[Aaron Liu]

but if you want to construct an expression using Classical.choose and then you go to prove stuff about it then I wouldn't recommend it

[Aaron Liu]

I only recommend it if the choice is confined to a proof

[Aaron Liu]

not if you want to write a definition using choice

[Dan Abramov]

With Claude's help I got this but I don't really understand why it works or how to arrive at it yet

/-- Compatibility with Mathlib's notion of inverse -/
theorem Function.inverse_eq {X Y: Set} [Nonempty X] {f: Function X Y} (h: f.bijective) :
    (f.inverse h).to_fn = Function.invFun f.to_fn := by
  ext y
  apply Subtype.eq_iff.mp
  set x_via_ml := Function.invFun f.to_fn y
  symm
  dsimp
  have hx := ((f.inverse h).unique y)
  apply (Classical.choose_spec hx).2
  unfold x_via_ml
  change f.to_fn (Function.invFun f.to_fn y) = y
  apply Function.invFun_eq
  obtain ⟨x, hx⟩ := h.2 y
  use x

Would the choice tactic help here? I've never used it yet

[Dan Abramov]

Ah I think I see why I was getting lost. Taken from @Rado Kirov's solution:

theorem Function.inverse_eq' {X Y: Set} [Nonempty X] {f: Function X Y} (h: f.bijective) :
    (f.inverse h).to_fn = Function.invFun f.to_fn := by
  ext y
  apply Subtype.eq_iff.mp
  set x := Function.invFun f.to_fn y
  symm
  -- ⊢ x = (f.inverse h).to_fn y
  rw [Function.inverse_eval]
  -- ⊢ (fun x ↦ Classical.choose (f.unique x)) x = y
  rw [← to_fn_eval]
  -- ⊢ f.to_fn x = y

As you can see, the first rw [Function.inverse_eval] actually "expands too much" so we have to rw [← to_fn_eval] right after. Otherwise, we lose information about this "just" being an f x call, and thus can't easily apply inverse transformations that operate on f and infFun f.

This was super non-obvious to me and I assumed I have to be dealing with Classical.choose myself.

[Aaron Liu]

fun x ↦ Classical.choose (f.unique x) should be its own definition, and this definition should be listed as CoeFun instead of what we have now which is the CoeFun instance being something complicated

[Dan Abramov]

Thanks for the tip. Fix incoming: https://github.com/teorth/analysis/pull/180

[Dan Abramov]

I finished my version of 3.3 solutions if you want to have a look: https://github.com/gaearon/analysis-solutions/pull/6

They ended up fairly clean IMO. The change @Aaron Liu suggested earlier helped quite a bit with keeping the goal on track. I got a bit lost with the last one due to missing open Classical so I sent https://github.com/teorth/analysis/pull/186 for that.

[Rado Kirov]

Nice, looks a lot cleaner than my solutions :) will rebase and rework with the new definitions.