Hi again! I found the 1960 edition in the library and in that this result is at 8.9.1 not 9.8.1. In any case I'm pretty sure you could find a shorter proof of hasFDerivWithinAt_of_partial_snd_continuousWithinAt_prod_open if you felt able to disregard Dieudonné and instead begin from hasFDerivWithinAt_uncurry_of_continuousWithinAt_snd in this WIP branch.

Thanks for the comment. Apologies for the slow reply. Yes, the theorem numbering is a typo, sorry. It seems to me that the theorems you prove in your WIP branch hasStrictFDerivAt_uncurry_coprod and hasFDerivWithinAt_uncurry_coprod_of_continuousWithinAt_snd are basically the same as what I proved in hasFDerivWithinAt_continuousWithinAt_of_partial_continuousWithinAt_open and hasFDerivWithinAt_of_partial_snd_continuousWithinAt_prod_open. At least I can't imagine that the logic is much different.

Sorry, I wasn't aware of your branch earlier. Did it predate my PR? Your proofs do look more streamlined than mine. What do you think should be done with these PRs given some amount of overlap?

Well the ‘implicit’ branch has existed since last September (forgotten most of that time), but as we discussed on Zulip, I hadn’t pushed any of these proofs. I only did so when I saw that your work was not going to cover the fact about strict differentiability that I wanted for the IFT. Then I guess I got carried away refactoring and ended up also proving the statement that looks a bit like yours.

We should combine our work! If you give me write access, I’ll push my four theorems to the top of your file. Then, if it suits, you could make use of them in what remains. Like you, I started with (x, y) : E × F but found it unnecessarily confusing when combined with projection notation. So let’s go with (x₁, x₂) : E₁ × E₂ instead (i.e. what’s currently in my branch).

In addition to giving a reference, could you sketch the proofs that you are implementing? I wouldn't expect a reader to go and open Dieudonne, so sketching the argument is always helpful.

Also, it's not completely clear to me if you are both happy with the current state of the PR, or if there are things you want to merge/improve. Could you tell about the current state of affairs?

Thanks for the preliminary review! Igor told me last week in DMs that he will be on holiday for a couple of weeks. For me, this PR still requires some work to integrate our contributions. As I said above, I think some of the proofs below the four newly introduced theorems could be made shorter by using them and some hypotheses could be dropped. Maybe even some theorems.

I think some of the proofs below the four newly introduced theorems could be made shorter by using them

After reorganisation, these four have become three at the top of Calculus.FDeriv.Partial and two at the bottom of Normed.Module.Convex.

Instead of using two points x_1 and x_2, could you use a single point x in E_1 \times E_2, with x.1 and x.2? This is strictly more general, as otherwise your statement wouldn't apply directly to a point which is not written as a pair (x_1, x_2).

Same thing below.

I am certainly happy to do this! But I'm also a little curious as to the rationale. It looks to me as if Lean can itself break apart an element x : E₁ × E₂ so as to use a statement like this one. For example the following already works:

variable {𝕜 E₁ E₂ F : Type*} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₂]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F]

variable {f : E₁ → E₂ → F} {f₁ : E₁ → E₂ → E₁ →L[𝕜] F} {f₂ : E₁ → E₂ → E₂ →L[𝕜] F} {x : E₁ × E₂}
  (cf₁ : ContinuousAt ↿f₁ x) (df₁ : ∀ᶠ y in 𝓝 x, HasFDerivAt (f · y.2) (f₁ y.1 y.2) y.1)
  (cf₂ : ContinuousAt ↿f₂ x) (df₂ : ∀ᶠ y in 𝓝 x, HasFDerivAt (f y.1 ·) (f₂ y.1 y.2) y.2)

#check (hasStrictFDerivAt_uncurry_coprod cf₁ df₁ cf₂ df₂ : HasStrictFDerivAt ↿f ((↿f₁ x).coprod (↿f₂ x)) x)

In addition to giving a reference, could you sketch the proofs that you are implementing? I wouldn't expect a reader to go and open Dieudonne, so sketching the argument is always helpful.

Also, it's not completely clear to me if you are both happy with the current state of the PR, or if there are things you want to merge/improve. Could you tell about the current state of affairs?

From this point on in the PR, indentation is often off. Could you have a look and try to fix it?

@igorkhavkine Arguments count as part of the statement so they should also be indented four spaces from the left margin. Also we have problems with CI but merging master might fix it according to Zulip. Best of luck with this PR! Back in September.

I'm a little bit confused: how does this theorem relate to hasFDerivWithinAt_uncurry_coprod_of_continuousWithinAt_snd?

Well hasFDerivWithinAt_uncurry_coprod_of_continuousWithinAt_snd is the more general version but perhaps it’s still worth keeping this? I don’t know. The only result I actually wanted for another purpose was the one on strict differentiability. Your opinion on the value of this and other theorems would be very welcome!