Application type mismatch

Stream: mathlib4

[María Inés de Frutos Fernández]

The following example is a bit long, since I need to introduce some definitions, so I am omitting the proofs. My question is about the last have in the code below. The Lean 3 version of this code worked, but in Lean 4 I get the error

application type mismatch
  @isNonarchimedean_finset_image_add ?m.281248 K NormedRing.toRing ?m.281251 ?m.281252 hna
argument
  hna
has type
  IsNonarchimedean norm : Prop
but is expected to have type
  IsNonarchimedean ⇑?m.281252 : Prop

My guess is that this is becauseIsNonarchimedean is defined for functions $R \to \mathbb{R}$ while the theorem isNonarchimedean_finset_image_add is stated in terms of AddGroupSeminormClass. Is this right? What would be the preferred way to fix this proof?

import Mathlib.Analysis.Normed.Ring.Seminorm
import Mathlib.Analysis.Seminorm
import Mathlib.Analysis.NormedSpace.BoundedLinearMaps

noncomputable section

/-- A function `f : R → ℝ≥0` is nonarchimedean if it satisfies the strong triangle inequality
  `f (r + s) ≤ max (f r) (f s)` for all `r s : R`. -/
def IsNonarchimedean {R : Type _} [AddGroup R] (f : R → ℝ) : Prop :=
  ∀ r s, f (r + s) ≤ max (f r) (f s)

open Finset
open scoped BigOperators

/-- Given a nonarchimedean additive group seminorm `f` on `α`, a function `g : β → α` and a finset
  `t : finset β`, we can always find `b : β`, belonging to `t` if `t` is nonempty, such that
  `f (t.sum g) ≤ f (g b)` . -/
theorem isNonarchimedean_finset_image_add {F α : Type _} [Ring α] [AddGroupSeminormClass F α ℝ]
    {f : F} (hna : IsNonarchimedean f) {β : Type _} [hβ : Nonempty β] (g : β → α) (t : Finset β) :
    ∃ (b : β) (_ : t.Nonempty → b ∈ t), f (t.sum g) ≤ f (g b) := by
  sorry

variable {K : Type _} [NormedField K] {L : Type _} [Field L] [Algebra K L]

/-- The function sending an element `x : L` to the maximum of the norms of its coefficients
  with respect to the `K`-basis `B` of `L`.-/
def Basis.norm {ι : Type _} [Fintype ι] [Nonempty ι] (B : Basis ι K L) : L → ℝ := fun x =>
  ‖B.equivFun x (Classical.choose (Finite.exists_max fun i : ι => ‖B.equivFun x i‖))‖

/-- Given a fintype `α`, a function `f : α → M` and a linear equivalence `g : M ≃ₛₗ[σ] N`, we have
  `g (∑ (i : α), f i) = ∑ (i : α), g (f i)`.  -/
theorem LinearEquiv.map_finset_sum {R S : Type _} {α : Sort _} [Fintype α] [Semiring R] [Semiring S]
    (σ : R →+* S) {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M N : Type _)
    [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S N] (g : M ≃ₛₗ[σ] N) (f : α → M) :
    g (∑ i : α, f i) = ∑ i : α, g (f i) := by
  sorry

/-- For any `K`-basis of `L`, `B.norm` is bounded with respect to multiplication. That is,
  `∃ (c : ℝ), c > 0` such that ` ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y`. -/
theorem norm_is_bdd {ι : Type _} [Fintype ι] [Nonempty ι] {B : Basis ι K L} {i : ι}
    (hBi : B i = (1 : L)) (hna : IsNonarchimedean (Norm.norm : K → ℝ)) :
    ∃ (c : ℝ) (hc : 0 < c), ∀ x y : L, B.norm (x * y) ≤ c * B.norm x * B.norm y := by
  classical
  -- The bounding constant `c` will be the maximum of the products `B.norm (B i * B j)`.
  set c := Classical.choose (Finite.exists_max fun i : ι × ι => B.norm (B i.1 * B i.2)) with hc_def
  have hc := Classical.choose_spec (Finite.exists_max fun i : ι × ι => B.norm (B i.1 * B i.2))
  use B.norm (B c.1 * B c.2)
  constructor
  -- ∀ (x y : L), B.norm (x * y) ≤ B.norm (⇑B c.fst * ⇑B c.snd) * B.norm x * B.norm y
  · intro x y
    -- `ixy` is an index for which `‖B.equivFun (x*y) i‖` is maximum.
    set ixy := Classical.choose (Finite.exists_max fun i : ι => ‖B.equivFun (x * y) i‖) with
      hixy_def
    -- We rewrite the LHS using `ixy`.
    conv_lhs =>
      simp only [Basis.norm]
      rw [← hixy_def, ← Basis.sum_equivFun B x, ← Basis.sum_equivFun B y]
    rw [sum_mul, LinearEquiv.map_finset_sum, sum_apply]
    simp_rw [smul_mul_assoc, LinearEquiv.map_smul, mul_sum, LinearEquiv.map_finset_sum,
      mul_smul_comm, LinearEquiv.map_smul]
    /- Since the norm is nonarchimidean, the norm of a finite sum is bounded by the maximum of the
          norms of the summands. -/
    have hk : ∃ (k : ι) (hk : (univ : Finset ι).Nonempty → k ∈ univ),
        ‖∑ i : ι, (B.equivFun x i • ∑ i_1 : ι, B.equivFun y i_1 • B.equivFun (B i * B i_1)) ixy‖ ≤
          ‖(B.equivFun x k • ∑ j : ι, B.equivFun y j • B.equivFun (B k * B j)) ixy‖ := by
      apply isNonarchimedean_finset_image_add hna
        (fun i => (B.equivFun x i • ∑ i_1 : ι, B.equivFun y i_1 • B.equivFun (B i * B i_1)) ixy)
        (univ : Finset ι) -- error
    sorry
  sorry

[Kevin Buzzard]

My guess: hna is a proof that norm is nonarchimedean, but apparently the function isNonarchimedean_finset_image_add which you're using wants a proof that (⇑(something)) is nonarchimedean, and in Lean 3 there was some definitional abuse going on which made it work fine, but because coercions have changed this trick no longer works.

So now let me show my ignorance: norm is this function K -> Real coming from the NormedField instance, but what should the type F be such that the instance AddGroupSeminormClass F K ℝ exists and there's some term of type F which will coerce to norm?

[María Inés de Frutos Fernández]

F could be MulRingNorm K (or AddGroupSeminorm K) and the term of type F that I want to use is NormedField.toMulRingNorm K. The problem is that, in Lean 4, even if I try to use an intermediate

have hna' : IsNonarchimedean (NormedField.toMulRingNorm K ) := hna

this hna' is a proof of

IsNonarchimedean (NormedField.toMulRingNorm K).toMulRingSeminorm.toAddGroupSeminorm.toFun)

while the type of the corresponding Lean 3 version was indeed

is_nonarchimedean ⇑(normed_field.to_mul_ring_norm K).

[Kevin Buzzard]

coercions in Lean 4 are still black magic to me, unfortunately :-(

[María Inés de Frutos Fernández]

I have managed to fix the proof by doing

have hna' : IsNonarchimedean (NormedField.toMulRingNorm K) := hna
rw [AddGroupSeminorm.toFun_eq_coe] at hna'

and then replacing hna by hna' in the call to isNonarchimedean_finset_image_add.

[Kevin Buzzard]

Nice! There is surely some more idiomatic way to do this but I don't know it