[Merged by Bors] - feat: add (m)differentiableAt_of_(m)fderiv_injective

[grunweg]

and versions for (m)fderivWithin versions. This generalises the existing lemmas (m)differentiableAt_of_isInvertible_(m)fderiv and friends.

Extracted from #35078; from the path to immersions, embeddings and submanifolds.

---

[github-actions]

PR summary 4aa0616ac5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ differentiableAt_of_fderiv_injective
+ differentiableWithinAt_of_fderivWithin_injective
+ differentiableWithinAt_of_subsingleton
+ mdifferentiableAt_of_mfderiv_injective
+ mdifferentiableWithinAt_of_mfderivWithin_injective
+ mdifferentiableWithinAt_of_subsingleton
+ not_injective_const

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[grunweg]

Is it worth extracting a lemma "if a constant function to X is injective, then Subsingleton X"? (It is used twice.)

[ocfnash]

Yes I think so. Furthermore how about we add the following higher up:

@[nontriviality]
theorem differentiableWithinAt_of_subsingleton [Subsingleton E] :
    DifferentiableWithinAt 𝕜 f s x :=
  (differentiable_of_subsingleton x).differentiableWithinAt

(actually several existing lemmas above could do with the @[nontriviality] decorator)
and then:

@[simp] lemma not_injective_const {α β : Type*} [Nontrivial α] {b : β} :
    ¬ Injective (fun _ : α ↦ b) := by
  rw [not_injective_iff]
  obtain ⟨a₁, a₂, h⟩ := exists_pair_ne α
  use a₁, a₂

(in the right file)
so that the proof here can become:

  nontriviality E
  contrapose! hf
  rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
  exact not_injective_const -- Disappointing that `simp` cannot fire here but let's live with it

[grunweg]

@ocfnash I have an easy differential geometry PR to review - would you like to take a look in the coming days? Thanks!

[ocfnash]

Thanks!

bors d+

[ocfnash]

Yes I think so. Furthermore how about we add the following higher up:

@[nontriviality]
theorem differentiableWithinAt_of_subsingleton [Subsingleton E] :
    DifferentiableWithinAt 𝕜 f s x :=
  (differentiable_of_subsingleton x).differentiableWithinAt

(actually several existing lemmas above could do with the @[nontriviality] decorator)
and then:

@[simp] lemma not_injective_const {α β : Type*} [Nontrivial α] {b : β} :
    ¬ Injective (fun _ : α ↦ b) := by
  rw [not_injective_iff]
  obtain ⟨a₁, a₂, h⟩ := exists_pair_ne α
  use a₁, a₂

(in the right file)
so that the proof here can become:

  nontriviality E
  contrapose! hf
  rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
  exact not_injective_const -- Disappointing that `simp` cannot fire here but let's live with it

[mathlib-bors]

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[grunweg]

Great suggestions, all addressed - let's hope CI likes these changes (on the train, so I prefer avoiding a full rebuild locally).

[grunweg]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step