slow elaboration of a proof

Stream: general

[Yakov Pechersky]

Consider the following on master:

import ring_theory.laurent_series

lemma is_unit_of_mem_non_zero_divisors {G₀ : Type*} [group_with_zero G₀]
  {x : G₀} (hx : x ∈ non_zero_divisors G₀) :
  is_unit x :=
⟨⟨x, x⁻¹, mul_inv_cancel (non_zero_divisors.ne_zero hx),
  inv_mul_cancel (non_zero_divisors.ne_zero hx)⟩, rfl⟩

set_option profiler true

instance {K : Type*} [field K] : is_fraction_ring (power_series K) (laurent_series K) :=
{ map_units := begin
    rintro ⟨y, hy⟩,
    rw [laurent_series.coe_algebra_map, subtype.coe_mk],
    refine is_unit_of_mem_non_zero_divisors _,
    have : function.injective (hahn_series.of_power_series ℤ K) :=
      hahn_series.of_power_series_injective,
    exact ring_hom.map_mem_non_zero_divisors (hahn_series.of_power_series ℤ K) this hy
  end,
  surj := sorry,
  eq_iff_exists := sorry }

#exit

On my machine it takes 40 seconds, where the offending line seems to be the one starting with exact ring_hom.... What's going on here?

[Yakov Pechersky]

Something else is up too -- if I change the proof to

{ map_units := begin
    rintro ⟨y, hy⟩,
    rw [laurent_series.coe_algebra_map],
    refine is_unit_of_mem_non_zero_divisors _,
    have : function.injective (algebra_map (power_series K) (laurent_series K)) :=
      hahn_series.of_power_series_injective,
    sorry,
  end,

that is also very slow

[Eric Rodriguez]

injective algebra maps and slow functions :) does specifying the TC arguments speed it up?

[Alex J. Best]

I don't know the root cause, but this is some sort of universe issue, changing to

universe u
instance {K : Type*} [field K] : is_fraction_ring (power_series K) (laurent_series K) :=
{ map_units := begin
    rintro ⟨y, hy⟩,
    rw [laurent_series.coe_algebra_map, subtype.coe_mk],
    refine is_unit_of_mem_non_zero_divisors _,
    have : function.injective (hahn_series.of_power_series ℤ K) :=
      hahn_series.of_power_series_injective,
    exact ring_hom.map_mem_non_zero_divisors (hahn_series.of_power_series ℤ K) this hy,
  end,
  surj := sorry,
  eq_iff_exists := sorry }

it becomes instant for me, edit: ok maybe not instant but seems way faster

[Yakov Pechersky]

@Eric Rodriguez which of the TC arguments? For which statement?

[Yakov Pechersky]

Even with universes, this is slow for me:

import ring_theory.laurent_series

universe u

lemma is_unit_of_mem_non_zero_divisors {G₀ : Type u} [group_with_zero G₀]
  {x : G₀} (hx : x ∈ non_zero_divisors G₀) :
  is_unit x :=
⟨⟨x, x⁻¹, mul_inv_cancel (non_zero_divisors.ne_zero hx),
  inv_mul_cancel (non_zero_divisors.ne_zero hx)⟩, rfl⟩

set_option profiler true

instance {K : Type u} [field K] : is_fraction_ring (power_series K) (laurent_series K) :=
{ map_units := begin
    rintro ⟨y, hy⟩,
    rw [laurent_series.coe_algebra_map],
    refine is_unit_of_mem_non_zero_divisors _,
    have : function.injective (algebra_map (power_series K) (laurent_series K)) :=
      hahn_series.of_power_series_injective,
    sorry,
  end,
  surj := sorry,
  eq_iff_exists := sorry }

#exit

[Yakov Pechersky]

But I can corroborate that {K : Type u} speeds it up!

[Alex J. Best]

Hm very strange, I have that exact file and it is only a second or so

[Yakov Pechersky]

Alex, with the exact line or the function.injective (algebra_map ...) line?

[Alex J. Best]

Oh right sorry, with exact + universes it is fast

[Alex J. Best]

But the second one is still slow

[Yakov Pechersky]

Strange. Gonna sweep it under the rug and just PR with the fast version. Thanks for the quick fix! #11220