# Zulip Chat Archive

## Stream: general

### Topic: slow elaboration of a proof

#### Yakov Pechersky (Jan 03 2022 at 23:02):

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 (Jan 03 2022 at 23:03):

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 (Jan 03 2022 at 23:07):

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

#### Alex J. Best (Jan 03 2022 at 23:28):

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 (Jan 03 2022 at 23:28):

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

#### Yakov Pechersky (Jan 03 2022 at 23:29):

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 (Jan 03 2022 at 23:30):

But I can corroborate that `{K : Type u}`

speeds it up!

#### Alex J. Best (Jan 03 2022 at 23:31):

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

#### Yakov Pechersky (Jan 03 2022 at 23:32):

Alex, with the `exact`

line or the `function.injective (algebra_map ...)`

line?

#### Alex J. Best (Jan 03 2022 at 23:33):

Oh right sorry, with exact + universes it is fast

#### Alex J. Best (Jan 03 2022 at 23:34):

But the second one is still slow

#### Yakov Pechersky (Jan 03 2022 at 23:38):

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

Last updated: Dec 20 2023 at 11:08 UTC