Miraculous rw in Lean 3

Stream: mathlib4

[Patrick Massot]

Does anyone understand how rewriting using docs#linear_isometry_equiv.norm_map can succeed in https://github.com/leanprover-community/mathlib/blob/7fdeecc0d03cd40f7a165e6cf00a4d2286db599f/src/analysis/calculus/cont_diff.lean#L2419 and similar places? To me (and to Lean 4) it looks like it should fail just as the following will fail if you remove the first line:

example (f g h : ℕ → ℕ) (hf : ∀ x, f x = x) (x : ℕ) : h ((f ∘ g) x) = h (g x) :=
begin
  change h (f (g x)) = h (g x),
  rw hf,
end

[Patrick Massot]

Note this question already came in https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Analysis/Calculus/ContDiffDef.lean#L792

[Eric Wieser]

∘ is reducible in Lean 3, but not in Lean 4

[Patrick Massot]

The code snippet above is Lean 3 code and fails if you remove the change.

[Eric Wieser]

I guess there's something about the original scenario that somehow is allowed to unfold the reducible ∘ (but only in Lean 3), and isn't captured by your mwe

[Eric Wieser]

The proof you link to fails if you start with local attribute [semireducible] function.comp

[Kevin Buzzard]

The code snippet above is Lean 3 code

This thread is arguably in the wrong stream then :-)

I had real trouble getting that file to compile, even though I have all oleans. If I open the file on master and compile, I often get excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold) :-( Setting default memory limit to 16384 on a 32 gig machine (it was on 4096) seems to have solved it. I wonder how Lean 4 will cope with 3000 line files deep in the heirarchy. We'll find out soon enough I guess.

Here's the conundrum in a self-contained lean 3 file:

import analysis.calculus.cont_diff

universes u_1 u

example {𝕜 : Type u_1} {Du : Type u} {Eu : Type u} (i : ℕ)
  [nontrivially_normed_field 𝕜]
  [normed_add_comm_group Du]
  [normed_space 𝕜 Du]
  {s : set Du}
  {x : Du}
  [normed_add_comm_group Eu]
  [normed_space 𝕜 Eu]
  {f : Du → Eu}
 :
  ‖iterated_fderiv_within 𝕜 i (fderiv_within 𝕜 f s) s x‖ =
  ‖(⇑(continuous_multilinear_curry_right_equiv' 𝕜 i Du Eu) ∘
    iterated_fderiv_within 𝕜 i (λ (y : Du), fderiv_within 𝕜 f s y) s) x‖ :=
begin
  rw linear_isometry_equiv.norm_map, -- why does this work??
end

[Kevin Buzzard]

Mathlib-free:

class has_norm (E : Type*) := (norm : E → ℕ)

export has_norm (norm)

notation `‖` e `‖` := norm e

structure equiv (α : Sort*) (β : Sort*) :=
(to_fun    : α → β)
(inv_fun   : β → α)

infix ` ≃ `:25 := equiv

instance {α β : Type} : has_coe_to_fun (α ≃ β) (λ _, α → β) := ⟨equiv.to_fun⟩

lemma foo (A B : Type)  [has_norm A] [has_norm B]
 (e : A ≃ B) (x : A) : ‖e x‖ = ‖x‖ := sorry

example (A B C : Type) [has_norm A] [has_norm B]
  (e : A ≃ B) (φ : C → A) (x : C) : ‖(e ∘ φ) x‖ = ‖ φ x ‖  :=
begin
  rw foo, -- works?!
  done,
end

[Kevin Buzzard]

And it's not just because function.comp is @[inline, reducible]:

lemma bar (A : Type)
 (e : A ≃ A) (x : A) : e x = x := sorry

example (A C : Type)
  (e : A ≃ A) (φ : C → A) (x : C) : (e ∘ φ) x = φ x  :=
begin
  rw bar, -- fails
end