port Analysis.NormedSpace.OperatorNorm !4#3708

Stream: mathlib4

[Scott Morrison]

I think port Analysis.NormedSpace.OperatorNorm !4#3708 is one is the most critical files for porting at the moment, and it's ... a bit of a disaster. There are huge timeouts going on. Some of these go away on reenableeta (see the branch reenableeta_OperatorNorm), but others do not!

I propose we try three concurrent things:
1) Fix the errors on the reenableeta_OperatorNorm branch (where it's actually possible to work...) and then transfer these over to the live branch. In particular mkContinuous₂ and le_norm_flip need fixing, and these are addressable on this branch.
2) Investigate the remaining timeouts on reenableeta_OperatorNorm, particularly toNormedAlgebra which is still really bad (however not actually need in this file, or at all until ContDiff, so it's not really a blocker). However flipₗᵢ' and flipₗᵢ are also still timing out.
3) Can we cut this file up in mathlib3? It is a huge file. If someone would like to investigate what the minimal prefix of analysis.normed_space.operator_norm is that still allows analysis.normed_space.multilinear to compile, I think we should cut the file at that point, so we can as rapidly as possible see what comes after this obstacle.

Please consider reenableeta_OperatorNorm a free-for-all branch. Feel free to reserve it here. I'll be hacking on it for a short while longer right now.

[Yaël Dillies]

@Eric Wieser, you're familiar with the material in analysis.normed_space.operator_norm, right?

[Eric Wieser]

Yes, somewhat. I'm on vacation today, but could have a look at obvious file splits this evening (11pm UTC)

[Scott Morrison]

I'm not fussed about the naturality of the split. I just want the minimal requirements for the next files in the graph. :-)

[Sebastien Gouezel]

It's typically the kind of file where !4#3840 is supposed to help.

[Scott Morrison]

Okay, I'm releasing my hold on reenableeta_OperatorNorm. I did fix lots of errors there, and have migrated all those fixes across to !4#3708, although I can't actually verify they work because that file is just too slow. :-)

[Scott Morrison]

There is still a timeout on toNormedAlgebra. I've just made a branch which is the sup of !4#3708 (OperatorNorm), reenableeta, and !4#3840 (Sebastien's refactor), to see if that gets anywhere. :-) But I hopefully I will go to sleep before that compiles!

[Scott Morrison]

Well, on this supremum-of-all-the-tricks-branch, toNormedAlgebra now runs with set_option maxHeartbeats 2000000 in (but not set_option maxHeartbeats 1600000 in). Perhaps we can have a look at this at the porting meeting tomorrow.

[Matthew Ballard]

I am guessing that ContinuousLinearMap.semiring should fire when the goal is Semiring (E →L[𝕜] E) right? Lol.

[Matthew Ballard]

This is fast but incomplete and complete (on !4#3708 itself)

set_option synthInstance.etaExperiment true in
private def bad : Algebra 𝕜 (E →L[𝕜] E) := inferInstance

set_option synthInstance.etaExperiment true in
-- /-- For a normed space `E`, continuous linear endomorphisms form a normed algebra with
-- respect to the operator norm. -/
instance toNormedAlgebra : NormedAlgebra 𝕜 (E →L[𝕜] E) :=
  { bad with
    norm_smul_le := by
      intro c f
      apply op_norm_smul_le c f}

[Matthew Ballard]

If I replace bad with ContinuousLinearMap.algebra then the timeouts commence. I am guessing that Lean has some preferred instances it has inferred in this file and they clash with those from ContinuousLinearMap.algebra, even though they might be unified as $t \to \infty$.

[Matthew Ballard]

Lean is also fatigued if I try to make the instance of the algebra structure a parameter of toNormedAlgebra

[Ruben Van de Velde]

I'm going to look at trimming some code from the end of operator_norm over at https://github.com/leanprover-community/mathlib/compare/operator_norm?expand=1

[Ruben Van de Velde]

Without much thinking, I got it down ~1000 lines to 775. I need to step out now; I might spend a little more time on it later

[Ruben Van de Velde]

Forward-porting all the code removal, I got the file compiling in lean4 :tada:

[Eric Wieser]

Have you made a mathlib3 PR?

[Ruben Van de Velde]

I'm stopping for today; if anyone wants to take over, that would be great.

All the code removed in https://github.com/leanprover-community/mathlib/compare/operator_norm?expand=1 will need to move to a new file, and imports added

https://github.com/leanprover-community/mathlib4/pull/new/port/Analysis.NormedSpace.OperatorNorm-minimal has the corresponding mathlib4 changes

[Eric Wieser]

Let's not get too excited and merge the mathlib4 PR until we've actually finished the mathlib3 split, and preferably let it propagate through mathport :)

[Ruben Van de Velde]

Yeah, no hurry on that side, but I wanted to check if I'd actually removed enough for it to help

[Scott Morrison]

Okay, the split may not be necessary after all.

[Scott Morrison]

I have the branch reenableeta_OperatorNorm (which contains the entirety of the file) down to just one error.

[Scott Morrison]

The main branch port/Analysis.NormedSpace.OperatorNorm in !4#3708 hopefully works too, but it is massively slow. I'm checking it now.

[Scott Morrison]

If anyone would like to have a look at the one remaining error on reenableeta_OperatorNorm that would be amazing. I'm a bit sick of this file for today. :-)

[Scott Morrison]

The remaining error is in:

set_option synthInstance.etaExperiment true in
theorem norm_precompR_le (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) : ‖precompR Eₗ L‖ ≤ ‖L‖ :=
  calc
    ‖precompR Eₗ L‖ ≤ ‖compL 𝕜 Eₗ Fₗ Gₗ‖ * ‖L‖ := op_norm_comp_le _ _
    _ ≤ 1 * ‖L‖ := (mul_le_mul_of_nonneg_right (norm_compL_le _ _ _ _) (norm_nonneg _))
    _ = ‖L‖ := by rw [one_mul]
#align continuous_linear_map.norm_precompR_le ContinuousLinearMap.norm_precompR_le

where it says failed to synthesize instance SeminormedAddCommGroup ((Eₗ →L[𝕜] Fₗ) →L[𝕜] Eₗ →L[𝕜] Gₗ) at op_norm_comp_le _ _ (the first proof in the calc block).

[Scott Morrison]

I experienced some similar errors elsewhere, which I worked around by adding things like

-- Porting note: this instance should just be `inferInstance`,
-- and indeed simply unneeded.
local instance : Norm (E →L[𝕜] (Eₗ →L[𝕜] Fₗ) →L[𝕜] Eₗ →L[𝕜] Gₗ) := by
  exact @hasOpNorm _ _ E ((Eₗ →L[𝕜] Fₗ) →L[𝕜] Eₗ →L[𝕜] Gₗ) _ _ _ _ _ _ _

(which I'd also like an explanation / solution for!), but I haven't been able to identify the correct incantation here.

[Scott Morrison]

Okay, it compiles with reenableeta.

[Scott Morrison]

Okay, I've now got Analysis.NormedSpace.OperatorNorm !4#3708 compiling, but it takes a ridiculously long time, and is cancelled because it exceed the 6 hour CI limit.

[Scott Morrison]

I've also made !4#3903, which is the supremum of the !4#3708 and !4#3414 (reenableeta) branches, which verifies that the same file takes only a few minutes to compile there.

[Scott Morrison]

Things to do:

• If anyone would like to hack at !4#3708 to see if some typeclass surgery can improve the situation, that would be great. @Sebastien Gouezel, I know you're good at this. :-)
• It would be very helpful if we can provide standalone examples of this scenario:
  • Requires etaExperiment
  • but is extremely slow
  • but is fast with !4#3414 (i.e. with lean-toolchain gebner/lean4:reenableeta230506)
• Maybe we can try to minimize down from OperatorNorm itself, but it feels like we are very far into Mathlib at this point!

[Matthew Ballard]

How does this

import Mathlib

set_option synthInstance.etaExperiment true in
#synth Zero ℤ

run on the other branch. It doesn't require etaExp but it does time out.

[Scott Morrison]

It is instant on reenableeta.

[Scott Morrison]

import Mathlib

#synth Zero ℤ -- works fine

set_option synthInstance.etaExperiment true in
#synth Zero ℤ -- but times out under `etaExperiment`.

set_option synthInstance.etaExperiment true in
set_option synthInstance.maxHeartbeats 60000 in -- usual limit is 20000
#synth Zero ℤ -- still works with a higher timelimit.

We should try to minimize the imports on this one.

[Scott Morrison]

Somewhat implausibly, it is a three body interaction:

import Mathlib.Data.Int.Basic
import Mathlib.Algebra.Ring.Regular
import Mathlib.Algebra.Field.Basic

#synth Zero ℤ -- works fine

set_option synthInstance.etaExperiment true in
#synth Zero ℤ -- but times out under `etaExperiment`.

set_option synthInstance.etaExperiment true in
set_option synthInstance.maxHeartbeats 60000 in -- usual limit is 20000
#synth Zero ℤ -- still works with a higher timelimit.

replacing any one of those three imports with its own imports causes the timeout to vanish. :-)

[Scott Morrison]

This is certainly a small enough set of imports that we could de-mathlib-ify it.

[Scott Morrison]

Halfway through de-mathlib-ing it, but have to head out for a while. Thanks for the example, @Matthew Ballard!

[Kevin Buzzard]

Looking at this now. The problematic declaration in Mathlib.Algebra.Field.Basic seems to be

-- see Note [lower instance priority]
instance (priority := 100) Field.isDomain : IsDomain K :=
  { DivisionRing.isDomain with }

Let me reiterate my frustration with being unable to turn off the "VS Code insists on reporting the total number of errors in open files as opposed to the number of errors in the scratch file you're working on" feature, because I'm in the middle of porting a file and I don't really want to start closing other tabs. It makes this debugging job just that little bit harder.

[Mauricio Collares]

Is this what you want?

[Kevin Buzzard]

I want what I had with Lean 3! (either that or I am hallucinating Lean 3 behaviour). I want "0 errors" in the blue line at the bottom if there are 0 errors in the file I have open, not "n errors" where n is the total number of errors in a random file I'm half way through porting in another tab.

Getting back to the issue at hand (which I don't want to derail), here are the problematic declarations:

-- import Mathlib.Data.Int.Basic

import Mathlib.Tactic.Convert
import Mathlib.Init.Data.Int.Order
import Mathlib.Data.Int.Cast.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Order.Monotone.Basic
import Mathlib.Logic.Nontrivial

-- import Mathlib.Algebra.Ring.Regular

import Mathlib.Algebra.Regular.Basic
import Mathlib.Algebra.Ring.Defs

-- import Mathlib.Algebra.Field.Basic

import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.GroupWithZero.Units.Lemmas
import Mathlib.Algebra.Hom.Ring
import Mathlib.Algebra.Ring.Commute

section Mathlib.Data.Int.Basic

namespace Int

instance : CommRing ℤ where
  zero_mul := Int.zero_mul
  mul_zero := Int.mul_zero
  mul_comm := Int.mul_comm
  left_distrib := Int.mul_add
  right_distrib := Int.add_mul
  mul_one := Int.mul_one
  one_mul := Int.one_mul
  npow n x := x ^ n
  npow_zero _ := rfl
  npow_succ _ _ := by rw [Int.mul_comm]; rfl
  mul_assoc := Int.mul_assoc
  add_comm := Int.add_comm
  add_assoc := Int.add_assoc
  add_zero := Int.add_zero
  zero_add := Int.zero_add
  add_left_neg := Int.add_left_neg
  nsmul := (·*·)
  nsmul_zero := Int.zero_mul
  nsmul_succ n x :=
    show (n + 1 : ℤ) * x = x + n * x
    by rw [Int.add_mul, Int.add_comm, Int.one_mul]
  zsmul := (·*·)
  zsmul_zero' := Int.zero_mul
  zsmul_succ' m n := by
    simp only [ofNat_eq_coe, ofNat_succ, Int.add_mul, Int.add_comm, Int.one_mul]
  zsmul_neg' m n := by simp only [negSucc_coe, ofNat_succ, Int.neg_mul]
  sub_eq_add_neg _ _ := Int.sub_eq_add_neg
  natCast := (·)
  natCast_zero := rfl
  natCast_succ _ := rfl
  intCast := (·)
  intCast_ofNat _ := rfl
  intCast_negSucc _ := rfl

end Int

end Mathlib.Data.Int.Basic

section Mathlib.Algebra.Ring.Regular

variable {α : Type _}

-- see Note [lower instance priority]
instance (priority := 100) IsDomain.toCancelCommMonoidWithZero [CommSemiring α] [IsDomain α] :
    CancelCommMonoidWithZero α :=
  { mul_left_cancel_of_ne_zero := IsLeftCancelMulZero.mul_left_cancel_of_ne_zero }

end Mathlib.Algebra.Ring.Regular

section Mathlib.Algebra.Field.Basic

variable {K : Type _}

-- see Note [lower instance priority]
instance (priority := 100) DivisionRing.isDomain [DivisionRing K] : IsDomain K :=
  NoZeroDivisors.to_isDomain _
#align division_ring.is_domain DivisionRing.isDomain

-- see Note [lower instance priority]
instance (priority := 100) Field.isDomain [Field K] : IsDomain K :=
  { DivisionRing.isDomain with }
#align field.is_domain Field.isDomain

end Mathlib.Algebra.Field.Basic

#synth Zero ℤ -- works fine

set_option synthInstance.etaExperiment true in
#synth Zero ℤ -- but times out under `etaExperiment`.

set_option synthInstance.etaExperiment true in
set_option synthInstance.maxHeartbeats 60000 in -- usual limit is 20000
#synth Zero ℤ -- still works with a higher timelimit.

(and now I also have to head out for a while)

[Scott Morrison]

I've mnimised this file, hopefully posting soon.

[Scott Morrison]

Okay, this is what I have! Please feel free to suggest further reductions.

/-!
# An etaExperiment timeout

The purpose of this file is to demonstrate a typeclass search that
* times out with `etaExperiment`
* is fast on `lean-toolchain` `gebner/lean4:reenableeta230506`
* is realistic, i.e. is a minimisation of something appearing in mathlib.

I've taken the example Matthew Ballard showed me:
```
import Mathlib

#synth Zero ℤ
```
and minimised it.

I've used `sorry` liberally,
but not changed the typeclass inheritance structure at all relative to mathlib4.
(It could probably be minimized further, but I think this is not the point?)

This file is minimised in the sense that:
* removing any command should either cause a new error, or remove the timeout.
* removing any field of a structure, and sorrying a field of an instance, should do the same.

Section titles correspond to the files the material came from the mathlib4/std4.
-/

section Std.Classes.Cast

class NatCast (R : Type u) where
class IntCast (R : Type u) where

end Std.Classes.Cast

section Std.Data.Int.Lemmas

namespace Int
theorem add_zero : ∀ a : Int, a + 0 = a := sorry
theorem mul_one (a : Int) : a * 1 = a := sorry
end Int

end Std.Data.Int.Lemmas

section Std.Classes.RatCast

class RatCast (K : Type u) where

end Std.Classes.RatCast

section Mathlib.Init.ZeroOne

class Zero.{u} (α : Type u) where
  zero : α
instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1
class One (α : Type u) where
  one : α
instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1

end Mathlib.Init.ZeroOne

section Mathlib.Algebra.Group.Defs

class Inv (α : Type u) where
class Semigroup (G : Type u) extends Mul G where
class AddSemigroup (G : Type u) extends Add G where
class CommSemigroup (G : Type u) extends Semigroup G where
  mul_comm : ∀ a b : G, a * b = b * a
class AddCommSemigroup (G : Type u) extends AddSemigroup G where
class MulOneClass (M : Type u) extends One M, Mul M where
  mul_one : ∀ a : M, a * 1 = a
class AddZeroClass (M : Type u) extends Zero M, Add M where
  add_zero : ∀ a : M, a + 0 = a
class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M where
class Monoid (M : Type u) extends Semigroup M, MulOneClass M where
class AddCommMonoid (M : Type u) extends AddMonoid M, AddCommSemigroup M
class CommMonoid (M : Type u) extends Monoid M, CommSemigroup M
class DivInvMonoid (G : Type u) extends Monoid G, Inv G, Div G where
class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G where
class Group (G : Type u) extends DivInvMonoid G where
class AddGroup (A : Type u) extends SubNegMonoid A where
class AddCommGroup (G : Type u) extends AddGroup G, AddCommMonoid G

end Mathlib.Algebra.Group.Defs

section Mathlib.Logic.Nontrivial

class Nontrivial (α : Type _) : Prop where

end Mathlib.Logic.Nontrivial

section Mathlib.Algebra.GroupWithZero.Defs

class MulZeroClass (M₀ : Type u) extends Mul M₀, Zero M₀ where
class IsLeftCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop where
class IsRightCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop where
class IsCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀]
  extends IsLeftCancelMulZero M₀, IsRightCancelMulZero M₀ : Prop
class NoZeroDivisors (M₀ : Type _) [Mul M₀] [Zero M₀] : Prop where
class SemigroupWithZero (S₀ : Type u) extends Semigroup S₀, MulZeroClass S₀
class MulZeroOneClass (M₀ : Type u) extends MulOneClass M₀, MulZeroClass M₀
class MonoidWithZero (M₀ : Type u) extends Monoid M₀, MulZeroOneClass M₀, SemigroupWithZero M₀
class CommMonoidWithZero (M₀ : Type _) extends CommMonoid M₀, MonoidWithZero M₀
class CancelCommMonoidWithZero (M₀ : Type _) extends CommMonoidWithZero M₀, IsLeftCancelMulZero M₀

end Mathlib.Algebra.GroupWithZero.Defs

section Mathlib.Data.Nat.Cast.Defs

class AddMonoidWithOne (R : Type u) extends NatCast R, AddMonoid R, One R where
class AddCommMonoidWithOne (R : Type _) extends AddMonoidWithOne R, AddCommMonoid R

end Mathlib.Data.Nat.Cast.Defs

section Mathlib.Data.Int.Cast.Defs

class AddGroupWithOne (R : Type u) extends IntCast R, AddMonoidWithOne R, AddGroup R where

end Mathlib.Data.Int.Cast.Defs

section Mathlib.Algebra.Ring.Defs

class NonUnitalNonAssocSemiring (α : Type u) extends AddCommMonoid α, MulZeroClass α
class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, SemigroupWithZero α
class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, MulZeroOneClass α,
    AddCommMonoidWithOne α
class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, MonoidWithZero α
class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R
class CommSemiring (R : Type u) extends Semiring R, CommMonoid R
class CommRing (α : Type u) extends Ring α, CommMonoid α
instance CommRing.toCommSemiring [s : CommRing α] : CommSemiring α :=
  { s with }
class IsDomain (α : Type u) [Semiring α] extends IsCancelMulZero α, Nontrivial α : Prop

end Mathlib.Algebra.Ring.Defs

section Mathlib.Data.Int.Basic

instance : CommRing Int where
  mul_comm := sorry
  mul_one := Int.mul_one -- Replacing this with `sorry` makes the timeout go away!
  add_zero := Int.add_zero -- Similarly here.

end Mathlib.Data.Int.Basic

section Mathlib.Algebra.Ring.Regular

section IsDomain

instance IsDomain.toCancelCommMonoidWithZero [CommSemiring α] [IsDomain α] :
    CancelCommMonoidWithZero α := { }

end IsDomain

end Mathlib.Algebra.Ring.Regular

section Mathlib.Algebra.Field.Defs

class DivisionRing (K : Type u) extends Ring K, DivInvMonoid K, Nontrivial K, RatCast K where
class Field (K : Type u) extends CommRing K, DivisionRing K

end Mathlib.Algebra.Field.Defs

section Mathlib.Algebra.Field.Basic

instance Field.isDomain [Field K] : IsDomain K :=
  sorry

end Mathlib.Algebra.Field.Basic

-- Finally, the example:

#synth Zero Int -- works fine

set_option synthInstance.etaExperiment true in
#synth Zero Int -- but times out under `etaExperiment`.

set_option synthInstance.etaExperiment true in
-- usual limit is 20000, and this takes even longer in real mathlib4
set_option synthInstance.maxHeartbeats 50000 in
#synth Zero Int -- still works with a higher timelimit.

[Scott Morrison]

If this is capturing what we want / people have had a chance to minimise, I'll post this as a Lean4 issue, as hopefully if reenableeta is viable then this file can become a test case.

(Alternatively we might learn that we're doing something stupid by looking at this example. :-)

[Scott Morrison]

If anyone is curious to see the typeclass trace, it is here. (I expanded out every node taking >0.1s.) I don't think it has any surprises: it repeating checks that two propositional fields are defeq (when it should already know because their types are the same), and then has to do defeq checks on instances again inside of that.

[Mauricio Collares]

Is the "checking same-type prop fields for defeq takes a long time" issue the same as lean4#2074 or does it just become much more visible due to lean4#2074? I don't know if the problem is checking if the types are actually the same, or if it is something else

[Scott Morrison]

Gabriel has just written up a great PR describing the issue at https://github.com/leanprover/lean4/pull/2210

[Kevin Buzzard]

I would be interested in trying this example against lean4#2210 but I don't know how to do this because when I invoke lean or lake it wants to download assets, and as far as I can see the branch doesn't have any assets because the corresponding version of lean is not a release. Does this make any sense?

I'd also like to be able to answer questions of the form "does lean4#2210 help with port/RingTheory.Polynomial.Quotient?" but again I don't know how to check this.

[Matthew Ballard]

Deleted for inaccurate info

[Scott Morrison]

@Kevin Buzzard, two options:

1. for this example, it's just a matter of editing lean-toolchain to say gebner/lean4:reenableeta230506.

2. if you want to work at the bleeding edge of mathlib, take the branch X you're interested in, run

   • git checkout -b X_reenableeta
   • git merge reenableeta
   • lake exe cache get
   • lake build

[Scott Morrison]

(Not my branch, Gabriel's. I've merged master into it a few times recently to keep it fresh.)

[Matthew Ballard]

Deleted for clarity.

[Matthew Ballard]

Ah ok. I see. I am not up to date.

[Kevin Buzzard]

I'm with Jujian right now who is also interested in this question and he also suggested editing lean-toolchain to gebner/lean4:reenableeta230506, but I'm very unclear about whether that release is anything to do with lean4#2210 (it was made a few days before the commits of that PR for example).

[Matthew Ballard]

lean4#2110 is coming from the branch that made the tool chain

[Kevin Buzzard]

OK thanks!

[Scott Morrison]

gebner/lean4:reenableeta230506 is based on a tag, not a branch, so it won't stay up to date with lean4#2210 if changes are made there, but I think it is safe to base your experiments of it for now.

[Matthew Ballard]

Also for RingTheory.Polynomial.Quotientthe dependencies are probably already in branch mathlib4/reenableeta. In this case, I usually checkout that branch and run

git checkout port/RingTheory.Polynomial.Quotient -- Mathlib/RingTheory/Polynomial/Quotient.lean

to pull in just that file. This might save some extraneous merge conflict resolution and/or building time.

[Matthew Ballard]

mathlib/reenableeta has been very useful to the porting effort. Are we planning on keeping up to date with master?

[Jujian Zhang]

I tried https://github.com/leanprover/lean4/pull/2210 on porting RingTheory.Polynomial.Quotient, it still times out, but it improved the issue enough so that if one just split proofs, the file compiles. The experiment is !4#3932. Without reenableeta, splitting the proof won't make the time out go away.

[Heather Macbeth]

#19015 is a split which should let us port the beginnings of integration theory without needing Analysis.NormedSpace.OperatorNorm.

[Jeremy Tan]

Why did Leo merge lean4#2210 without incorporating the second test file that was cowritten by Scott and me?

[Ruben Van de Velde]

Probably because it wasn't in the pr. You could make a new pr to add it to the test suite

[Jeremy Tan]

Then why was Scott's first file included?

[Mauricio Collares]

Because Gabriel added it to the PR four days ago

[Jeremy Tan]

Actually I now think the second test is redundant – the full OperatorNorm file is the real test

[Scott Morrison]

Yes, I think we'll be okay with just the one test. While we didn't know just how much of a test suite the Lean 4 devs would want, I think it was super helpful to keep making more, but if the timing didn't work out to get all of them included in the PR that's a fine outcome too! I appreciate your willingness to help out making my broken attempt at that test work properly. :-)