!4#4120 Analysis.Convex.StrictConvexSpace

Stream: mathlib4

[Jeremy Tan]

!4#4120 there's one error left here, who can fix it?

[Jeremy Tan]

Last line of this – simp doesn't work

affineIsometryOfStrictConvexSpace {f : PF → PE} (hi : Isometry f) :
    PF →ᵃⁱ[ℝ] PE :=
  { AffineMap.ofMapMidpoint f
      (fun x y => by
        apply eq_midpoint_of_dist_eq_half
        · rw [hi.dist_eq, hi.dist_eq]
          simp only [dist_left_midpoint, Real.norm_of_nonneg zero_le_two, div_eq_inv_mul]
        · rw [hi.dist_eq, hi.dist_eq]
          simp only [dist_midpoint_right, Real.norm_of_nonneg zero_le_two, div_eq_inv_mul])
      hi.continuous with
    norm_map := fun x => by simp [AffineMap.ofMapMidpoint, ← dist_eq_norm_vsub E, hi.dist_eq] }

[Kevin Buzzard]

      simp [AffineMap.ofMapMidpoint, ← dist_eq_norm_vsub E, hi.dist_eq]
      rw [hi.dist_eq]
      simp

works (but obviously isn't mathlib-ready)

[Kevin Buzzard]

For some reason hi.dist_eq isn't triggering with simp but it works with rw. This is becoming a common occurrence.

[Scott Morrison]

We need to be collecting minimised examples...

[Kevin Buzzard]

We've been having a go at understanding an example of this here

[Jeremy Tan]

This works, and is what I have now:

simp [AffineMap.ofMapMidpoint, ← dist_eq_norm_vsub E]
rw [hi.dist_eq, dist_vadd_left]

[Kevin Buzzard]

Did you see that in the other thread I noted that changing Type _ to Type u made the original proof work?

[Jeremy Tan]

Kevin Buzzard said:

Did you see that in the other thread I noted that changing Type _ to Type u made the original proof work?

Is this (losing universe polymorphism) preferred over rw [hi.dist_eq, dist_vadd_left]?

[Eric Wieser]

Changing _ to u isn't losing polymorphism as long as you change each _ to a different name

[Jeremy Tan]

Eric Wieser said:

Changing _ to u isn't losing polymorphism as long as you change each _ to a different name

Right, I've changed it to Type u