# Zulip Chat Archive

## Stream: new members

### Topic: refactoring proofs

#### Vasily Ilin (Apr 21 2022 at 01:02):

I have a proof that compiles but takes a while to do so. What tricks can I use to refactor the proof to make it as "minimal" as possible? Here is the proof (the last lemma):

```
import ring_theory.tensor_product
import tactic
open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial
universe u
variables (K : Type u) [comm_semiring K]
@[simp] lemma assoc_symm_tmul {R : Type u} [comm_semiring R] {A : Type u} [semiring A] [algebra R A] {B : Type u} [semiring B] [algebra R B] {C : Type u} [semiring C] [algebra R C] (a : A) (b : B) (c : C) :
(algebra.tensor_product.assoc R A B C).symm (a ⊗ₜ[R] (b ⊗ₜ[R] c)) = a ⊗ₜ[R] b ⊗ₜ[R] c :=
begin
apply_fun (algebra.tensor_product.assoc R A B C),
rw assoc_tmul,
rw alg_equiv.apply_symm_apply (algebra.tensor_product.assoc R A B C) (a ⊗ₜ[R] (b ⊗ₜ[R] c)),
simp,
unfold function.injective,
intros a b h,
exact h,
end
-- noncomputable def counit : K[X] →ₐ[K] K := polynomial.aeval 0
noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := aeval ((X ⊗ₜ 1) + (1 ⊗ₜ X))
@[simp] lemma comul_1 : comul K (1 : K[X]) = (1 ⊗ₜ 1 : K[X] ⊗[K] K[X]) :=
begin
rw alg_hom.map_one (comul K), -- ⊢ 1 = 1 ⊗ₜ[K] 1
refl,
end
@[simp] lemma comul_X : comul K X = X ⊗ₜ 1 + 1 ⊗ₜ X :=
begin
unfold comul,
rw aeval_X,
end
noncomputable def map1 : K[X] →ₐ[K] K[X] ⊗ K[X] ⊗ K[X] := (algebra.tensor_product.assoc K K[X] K[X] K[X]).symm.to_alg_hom.comp ((map (alg_hom.id K K[X]) (comul K)).comp (comul K))
noncomputable def map2 : (K[X] →ₐ[K] K[X] ⊗[K] K[X] ⊗[K] K[X] ) := (map (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X]) (alg_hom.id K K[X])).comp (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X])
. -- this tells Lean not to recompile definitions
lemma coassoc : map1 K = map2 K :=
begin
have P1 : map1 K X = X ⊗ₜ 1 ⊗ₜ 1 + 1 ⊗ₜ X ⊗ₜ 1 + 1 ⊗ₜ 1 ⊗ₜ X,
unfold map1,
simp [tensor_product.tmul_add, add_assoc],
have P2 : map2 K X = X ⊗ₜ 1 ⊗ₜ 1 + 1 ⊗ₜ X ⊗ₜ 1 + 1 ⊗ₜ 1 ⊗ₜ X,
unfold map2,
simp only [tensor_product.add_tmul, alg_hom.coe_comp, function.comp_app, comul_X, _root_.map_add, map_tmul, alg_hom.coe_id, id.def, comul_1],
ext,
rw P1,
rw P2,
end
```

#### Jireh Loreaux (Apr 21 2022 at 01:09):

I haven't played around with your file at all, but squeeze_simp is helpful, and `set_option profiler true`

can help determine where Lean is spending its time. You can also comment out portions of proofs (or use `sorry`

), especially if you use tactic blocks.

For example, you can (temporarily) skip the proofs of the two have statements as follows (I think you need Lean 3.41 or 3.42 for this). So if you can't speed up the proof enough, you can at least make it less painful to edit around the file.

```
lemma coassoc : map1 K = map2 K :=
begin
have P1 : map1 K X = X ⊗ₜ 1 ⊗ₜ 1 + 1 ⊗ₜ X ⊗ₜ 1 + 1 ⊗ₜ 1 ⊗ₜ X,
sorry { unfold map1,
simp [tensor_product.tmul_add, add_assoc] },
have P2 : map2 K X = X ⊗ₜ 1 ⊗ₜ 1 + 1 ⊗ₜ X ⊗ₜ 1 + 1 ⊗ₜ 1 ⊗ₜ X,
sorry { unfold map2,
simp only [tensor_product.add_tmul, alg_hom.coe_comp, function.comp_app, comul_X, _root_.map_add, map_tmul, alg_hom.coe_id, id.def, comul_1] },
ext,
rw P1,
rw P2,
end
```

#### Damiano Testa (Apr 21 2022 at 03:44):

I did not actually re-think proofs, I simply restructured the ones that you had and squeezed the simps, as Jireh also suggested. The last proof still take ~2-3 secs, but the file compiles faster than before:

```
import ring_theory.tensor_product
import tactic
open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial
universe u
variables (K : Type u) [comm_semiring K]
@[simp] lemma assoc_symm_tmul {R : Type u} [comm_semiring R] {A : Type u} [semiring A] [algebra R A] {B : Type u} [semiring B] [algebra R B] {C : Type u} [semiring C] [algebra R C] (a : A) (b : B) (c : C) :
(algebra.tensor_product.assoc R A B C).symm (a ⊗ₜ[R] (b ⊗ₜ[R] c)) = a ⊗ₜ[R] b ⊗ₜ[R] c :=
begin
apply_fun (algebra.tensor_product.assoc R A B C),
rw [assoc_tmul, alg_equiv.apply_symm_apply],
exact (embedding_like.comp_injective _ _).mpr (λ a b h, h),
end
-- noncomputable def counit : K[X] →ₐ[K] K := polynomial.aeval 0
noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := aeval ((X ⊗ₜ 1) + (1 ⊗ₜ X))
@[simp] lemma comul_1 : comul K (1 : K[X]) = (1 ⊗ₜ 1 : K[X] ⊗[K] K[X]) :=
begin
rw map_one, -- ⊢ 1 = 1 ⊗ₜ[K] 1
refl,
end
@[simp] lemma comul_X : comul K X = X ⊗ₜ 1 + 1 ⊗ₜ X :=
by rw [comul, aeval_X]
noncomputable def map1 : K[X] →ₐ[K] K[X] ⊗ K[X] ⊗ K[X] := (algebra.tensor_product.assoc K K[X] K[X] K[X]).symm.to_alg_hom.comp ((map (alg_hom.id K K[X]) (comul K)).comp (comul K))
noncomputable def map2 : (K[X] →ₐ[K] K[X] ⊗[K] K[X] ⊗[K] K[X] ) := (map (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X]) (alg_hom.id K K[X])).comp (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X])
. -- this tells Lean not to recompile definitions
lemma coassoc : map1 K = map2 K :=
begin
ext,
simp only [map1, map2, alg_equiv.to_alg_hom_eq_coe, alg_hom.coe_comp, alg_equiv.coe_alg_hom,
function.comp_app, comul_X, map_tmul, alg_hom.coe_id, id.def, comul_1,
tensor_product.tmul_add, add_assoc, assoc_symm_tmul, tensor_product.add_tmul, _root_.map_add],
end
```

#### Damiano Testa (Apr 21 2022 at 03:45):

Note that, placing `set_option profiler true`

somewhere in your file gives you information about all the subsequent compilation times.

#### Vasily Ilin (Apr 21 2022 at 04:47):

I am using `set_option profiler true`

as suggested and getting weird results. I have two lemmas that are exactly the same, with the same exact proof except that I give one a little more information. And the one I give more information takes 16 times longer! See the code below

```
import ring_theory.tensor_product
import tactic
open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial
universe u
variables (K : Type u) [comm_semiring K]
set_option profiler true
noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := aeval ((X ⊗ₜ 1) + (1 ⊗ₜ X))
@[simp] lemma comul_1 : comul K (1 : K[X]) = (1 ⊗ₜ 1 : K[X] ⊗[K] K[X]) := -- elaboration of comul_1 took 4.18s
begin
rw alg_hom.map_one (comul K), -- ⊢ 1 = 1 ⊗ₜ[K] 1
refl,
end
@[simp] lemma comul_1' : comul K (1 : K[X]) = (1 ⊗ₜ 1 : K[X] ⊗[K] K[X]) := -- elaboration of comul_1' took 189ms
begin
rw alg_hom.map_one,
refl,
end
```

#### Vasily Ilin (Apr 21 2022 at 05:04):

Also, doing something as simple as the following takes 3 seconds! This seems way too long, especially with all the types annotated

```
import ring_theory.tensor_product
import tactic
open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial
universe u
variables (K : Type u) [comm_semiring K]
set_option profiler true
noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := aeval ((X ⊗ₜ 1) + (1 ⊗ₜ X))
noncomputable def map2 : (K[X] →ₐ[K] K[X] ⊗[K] K[X] ⊗[K] K[X] ) := (map (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X]) (alg_hom.id K K[X])).comp (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X]) -- elaboration of map2 took 2.98s!
```

#### Vasily Ilin (Apr 21 2022 at 05:05):

@Damiano Testa , your proofs compile much faster than mine. How did you know to change the things you changed to make it faster? For example, why is `rw alg_hom.map_one`

faster than `rw alg_hom.map_one (comul K)`

?

#### Damiano Testa (Apr 21 2022 at 05:46):

Honestly, I do not know. I *think* that hints are generally good, but sometimes they get Lean into trying to prove some defeq that you want, but it is able to find more quickly some other way.

I have observed similar patterns with `localization, mv_polynomial, monoid_algebra`

. I suspect that the implementation has several layers of defeqs and lean can get confused.

#### Damiano Testa (Apr 21 2022 at 07:45):

Btw, on my computer (which is not particularly fast and is already over two years old), `map2`

elaborates in approximately .5s.

The slowness on your computer might be due to the fact that you have changed also some files imported by this PR and Lean has to struggle with some incomplete/missing `olean`

s. Maybe...

#### Eric Wieser (Apr 21 2022 at 10:18):

I would guess that `alg_hom.map_one (comul K)`

is slower than `alg_hom.map_one`

because the first one:

- Works out all the types for
`comul`

- Tries to match up all those types in the goal state
- Possibly has to unify defeq typeclass diamonds in doing so

while the second one:

- Tries to match any
`alg_hom`

in the goal, and deduces the type of`comul`

from there

#### Vasily Ilin (Apr 21 2022 at 16:05):

Damiano Testa said:

Btw, on my computer (which is not particularly fast and is already over two years old),

`map2`

elaborates in approximately .5s.The slowness on your computer might be due to the fact that you have changed also some files imported by this PR and Lean has to struggle with some incomplete/missing

`olean`

s. Maybe...

Huh, this is much faster than on mine. How would I fix this issue with `olean`

s you are referring to?

#### Vasily Ilin (Apr 21 2022 at 16:11):

I tried `leanproject build`

but it did not improve the elaboration speed

#### Damiano Testa (Apr 21 2022 at 17:56):

If leanproject built successfully your repository, then this should have taken care of the oleans... I'm not sure what explains the difference in performance, then.

#### Vasily Ilin (Apr 22 2022 at 00:00):

I have this proof, which is conceptually very simple: I have proof `coinv_left K`

that two algebra maps are equal, and I want to prove that two set maps that happen to be set_maps of the algebra morphisms are equal (`coinv_left'`

). It seems like it should be quite easy, maybe even just a `simp`

. But I wasn't able to refactor the proof below to something more elegant. Any suggestions?

```
lemma coinv_left' : (lmul' K) ∘ (map (coinv K) (alg_hom.id K K[X])) ∘ (comul K) = (algebra.of_id K K[X]) ∘ (counit K) :=
begin
let f' := (lmul' K).comp ((map (coinv K) (alg_hom.id K K[X])).comp (comul K)),
let g' := (algebra.of_id K K[X]).comp (counit K),
have h1 : f' = g',
exact coinv_left K,
have h2 : f'.to_fun = (lmul' K) ∘ (map (coinv K) (alg_hom.id K K[X])) ∘ (comul K),
simp only [alg_hom.to_fun_eq_coe, alg_hom.coe_comp],
have h3 : g'.to_fun = (algebra.of_id K K[X]) ∘ (counit K),
simp only [alg_hom.to_fun_eq_coe, alg_hom.coe_comp],
rw [← h2, ← h3],
simp only [h1],
end
```

#### Vasily Ilin (Apr 22 2022 at 00:02):

Here is the whole file:

```
import ring_theory.tensor_product
import tactic
open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial
variables (K : Type*) [comm_ring K]
@[simp] lemma assoc_symm_tmul {R : Type*} [comm_semiring R] {A : Type*} [semiring A] [algebra R A] {B : Type*} [semiring B] [algebra R B] {C : Type*} [semiring C] [algebra R C] (a : A) (b : B) (c : C) :
(algebra.tensor_product.assoc R A B C).symm (a ⊗ₜ[R] (b ⊗ₜ[R] c)) = a ⊗ₜ[R] b ⊗ₜ[R] c :=
begin
apply_fun (algebra.tensor_product.assoc R A B C),
rw [assoc_tmul, alg_equiv.apply_symm_apply],
exact (algebra.tensor_product.assoc R A B C).injective,
end
noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := aeval ((X ⊗ₜ 1) + (1 ⊗ₜ X))
@[simp] lemma comul_1 : comul K (1 : K[X]) = (1 ⊗ₜ 1 : K[X] ⊗[K] K[X]) :=
begin
rw alg_hom.map_one, -- ⊢ 1 = 1 ⊗ₜ[K] 1
refl,
end
@[simp] lemma comul_X : comul K X = X ⊗ₜ 1 + 1 ⊗ₜ X :=
begin
unfold comul,
rw aeval_X,
end
noncomputable def counit : K[X] →ₐ[K] K := aeval 0
@[simp] lemma counit_X : counit K X = 0 :=
begin
unfold counit,
simp only [coe_aeval_eq_eval, eval_X],
end
.
noncomputable def coinv : K[X] →ₐ[K] K[X] := aeval (-X)
@[simp] lemma coinv_X : coinv K X = -X :=
begin
unfold coinv,
rw aeval_X,
end
lemma coinv_left : (lmul' K).comp ((map (coinv K) (alg_hom.id K K[X])).comp (comul K) )= (algebra.of_id K K[X]).comp (counit K) :=
begin
ext,
simp only [alg_hom.coe_comp, function.comp_app, comul_X, _root_.map_add, map_tmul, coinv_X, alg_hom.coe_id, id.def, _root_.map_one, lmul'_apply_tmul, _root_.mul_one, _root_.one_mul, add_left_neg, counit_X, _root_.map_zero],
end
.
lemma coinv_left' : (lmul' K) ∘ (map (coinv K) (alg_hom.id K K[X])) ∘ (comul K) = (algebra.of_id K K[X]) ∘ (counit K) :=
begin
let f' := (lmul' K).comp ((map (coinv K) (alg_hom.id K K[X])).comp (comul K)),
let g' := (algebra.of_id K K[X]).comp (counit K),
have h1 : f' = g',
exact coinv_left K,
have h2 : f'.to_fun = (lmul' K) ∘ (map (coinv K) (alg_hom.id K K[X])) ∘ (comul K),
simp only [alg_hom.to_fun_eq_coe, alg_hom.coe_comp],
have h3 : g'.to_fun = (algebra.of_id K K[X]) ∘ (counit K),
simp only [alg_hom.to_fun_eq_coe, alg_hom.coe_comp],
rw [← h2, ← h3],
simp only [h1],
end
```

#### Damiano Testa (Apr 22 2022 at 00:08):

Does beginning with `ext`

or `funext`

work better?

#### Vasily Ilin (Apr 22 2022 at 00:14):

Damiano Testa said:

Does beginning with

`ext`

or`funext`

work better?

I think no, because it just gives me an arbitrary element x. I think I instead want to use the fact that the algebra maps are equal to imply that their set maps are equal. I came up with the following still-not-elegant proof:

```
lemma coinv_left' : (lmul' K) ∘ (map (coinv K) (alg_hom.id K K[X])) ∘ (comul K) = (algebra.of_id K K[X]) ∘ (counit K) :=
calc (lmul' K) ∘ (map (coinv K) (alg_hom.id K K[X])) ∘ (comul K)
= ((lmul' K).comp ((map (coinv K) (alg_hom.id K K[X])).comp (comul K))).to_fun : by simp only [alg_hom.to_fun_eq_coe, alg_hom.coe_comp]
... = ((algebra.of_id K K[X]).comp (counit K)).to_fun : by simp only [coinv_left]
... = (algebra.of_id K K[X]) ∘ (counit K) : by simp only [alg_hom.to_fun_eq_coe, alg_hom.coe_comp]
```

#### Vasily Ilin (Apr 22 2022 at 00:17):

Since I only use `simp`

s in the `calc`

block, I would expect this to work but it does not:

```
lemma coinv_left' : (lmul' K) ∘ (map (coinv K) (alg_hom.id K K[X])) ∘ (comul K) = (algebra.of_id K K[X]) ∘ (counit K) := by simp only [coinv_left, alg_hom.to_fun_eq_coe, alg_hom.coe_comp]
```

#### Damiano Testa (Apr 22 2022 at 00:20):

I am not sure if others agree, but I find it easier to work with "applied" functions, rather than non-applied ones, in Lean.

That was the reason for suggesting `funext`

. If it does not work, maybe this just means that this is the one time developing the API that you have to do something awkward... :shrug:

#### Vasily Ilin (Apr 22 2022 at 00:38):

I decided to change the definition of my class to require equality of algebra maps as opposed to set maps (even though mathematically it's equivalent). I had not realized that it is easier to prove equality of algebra maps than set maps...

#### Vasily Ilin (Apr 22 2022 at 00:41):

What should I do if `simp`

works but `squeeze_simp`

times out? I don't want to just keep `simp`

there since it will always take a long time to compile. Instead I want to switch it to `simp only [...]`

.

#### Damiano Testa (Apr 22 2022 at 00:42):

I sometimes save the file with the `squeeze_simp`

in, and the `lean --make <path_to_file>`

. This has a longer timeout threshold and will print the output.

#### Damiano Testa (Apr 22 2022 at 00:43):

Also, if you can guess what `simp`

will do first, you can try `simp only [your guesses], squeeze_simp`

.

#### Vasily Ilin (Apr 22 2022 at 00:44):

What if my guesses include like 20 things and `simp only [my guesses]`

solves it? How do I boil it down?

#### Damiano Testa (Apr 22 2022 at 00:45):

If you squeeze the `simp only`

, as in `squeeze_simp only [guesses]`

also times out?

#### Damiano Testa (Apr 22 2022 at 00:46):

(Anyways, if yes, I would go with the `lean --make`

step)

#### Damiano Testa (Apr 22 2022 at 00:47):

you can also mess with the timeout threshold on VSCode, but I usually prefer not to, since I want things to work quickly when I am proving stuff.

#### Damiano Testa (Apr 22 2022 at 00:48):

You can always put a sorry before the simp, if you know that simp will close the goal and leave it there while you develop the rest of the proof/file.

#### Vasily Ilin (Apr 22 2022 at 00:56):

Damiano Testa said:

If you squeeze the

`simp only`

, as in`squeeze_simp only [guesses]`

also times out?

yea

#### Vasily Ilin (Apr 22 2022 at 00:59):

I am also getting a timeout on something pretty unexpected. I include the full file below but only the last two instances and the lemma `coassoc`

are important. My instance times out when I include `coassoc K`

in it and does not time out otherwise. Does it mean I need to make `coassoc`

run faster? If so how can I do it?

```
import ring_theory.tensor_product
import tactic
open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial
variables (K : Type*) [comm_ring K]
variables (V : Type*) [comm_ring V] [algebra K V]
class hopf_algebra :=
(comul : V →ₐ[K] V ⊗[K] V)
(counit : V →ₐ[K] K)
(coinv : V →ₐ[K] V)
(coassoc : (algebra.tensor_product.assoc K V V V).to_alg_hom.comp ((map comul (alg_hom.id K V)).comp comul) = (map (alg_hom.id K V) comul).comp comul)
(counit_left : (algebra.tensor_product.lid K V).to_alg_hom.comp ((map counit (alg_hom.id K V)).comp comul) = (alg_hom.id K V))
(counit_right : (algebra.tensor_product.rid K V).to_alg_hom.comp ((map (alg_hom.id K V) counit).comp comul) = (alg_hom.id K V))
(coinv_right : (lmul' K).comp ((map (alg_hom.id K V) coinv).comp comul) = (algebra.of_id K V).comp counit)
(coinv_left : (lmul' K).comp ((map coinv (alg_hom.id K V)).comp comul) = (algebra.of_id K V).comp counit)
-- set_option profiler true -- time everything
noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := aeval ((X ⊗ₜ 1) + (1 ⊗ₜ X))
@[simp] lemma comul_1 : comul K (1 : K[X]) = (1 ⊗ₜ 1 : K[X] ⊗[K] K[X]) :=
begin
rw alg_hom.map_one, -- ⊢ 1 = 1 ⊗ₜ[K] 1
refl,
end
@[simp] lemma comul_X : comul K X = X ⊗ₜ 1 + 1 ⊗ₜ X :=
begin
unfold comul,
rw aeval_X,
end
lemma coassoc : (algebra.tensor_product.assoc K K[X] K[X] K[X]).to_alg_hom.comp ((map (comul K) (alg_hom.id K K[X])).comp (comul K)) = (map (alg_hom.id K K[X]) (comul K)).comp (comul K) := -- TODO this still takes 10 seconds to elaborate
begin
ext,
simp only [algebra.tensor_product.assoc_tmul, alg_equiv.to_alg_hom_eq_coe, alg_hom.coe_comp, alg_equiv.coe_alg_hom, function.comp_app, comul_X, map_tmul, alg_hom.coe_id, id.def, comul_1, tensor_product.tmul_add, add_assoc, tensor_product.add_tmul, _root_.map_add],
end
noncomputable def counit : K[X] →ₐ[K] K := aeval 0
@[simp] lemma counit_X : counit K X = 0 :=
begin
unfold counit,
simp only [coe_aeval_eq_eval, eval_X],
end
.
lemma counit_left : (algebra.tensor_product.lid K K[X]).to_alg_hom.comp ((map (counit K) (alg_hom.id K K[X])).comp (comul K)) = (alg_hom.id K K[X]) :=
begin
ext,
simp only [counit, alg_equiv.to_alg_hom_eq_coe, alg_hom.coe_comp, alg_equiv.coe_alg_hom, function.comp_app, comul_X, _root_.map_add, map_tmul, coe_aeval_eq_eval, eval_X, tensor_product.zero_tmul, eval_one, zero_add, lid_tmul, one_smul],
end
lemma counit_right : (algebra.tensor_product.rid K K[X]).to_alg_hom.comp ((map (alg_hom.id K K[X]) (counit K)).comp (comul K)) = (alg_hom.id K K[X]) :=
begin
ext,
simp only [counit, alg_equiv.to_alg_hom_eq_coe, alg_hom.coe_comp, alg_equiv.coe_alg_hom, function.comp_app, comul_X, _root_.map_add, map_tmul, coe_aeval_eq_eval, eval_one, eval_X, tensor_product.tmul_zero, add_zero, rid_tmul, one_smul],
end
noncomputable def coinv : K[X] →ₐ[K] K[X] := aeval (-X)
@[simp] lemma coinv_X : coinv K X = -X :=
begin
unfold coinv,
rw aeval_X,
end
lemma coinv_right : (lmul' K).comp ((map (alg_hom.id K K[X]) (coinv K)).comp (comul K)) = (algebra.of_id K K[X]).comp (counit K) :=
begin
ext,
simp only [alg_hom.coe_comp, function.comp_app, comul_X, _root_.map_add, map_tmul, alg_hom.coe_id, id.def, _root_.map_one, coinv_X, lmul'_apply_tmul, _root_.mul_one, _root_.one_mul, add_right_neg, counit_X, _root_.map_zero],
end
lemma coinv_left : (lmul' K).comp ((map (coinv K) (alg_hom.id K K[X])).comp (comul K) )= (algebra.of_id K K[X]).comp (counit K) :=
begin
ext,
simp only [alg_hom.coe_comp, function.comp_app, comul_X, _root_.map_add, map_tmul, coinv_X, alg_hom.coe_id, id.def, _root_.map_one, lmul'_apply_tmul, _root_.mul_one, _root_.one_mul, add_left_neg, counit_X, _root_.map_zero],
end
.
set_option profiler true -- time everything
noncomputable instance polynomial_hopf : hopf_algebra K K[X] := { -- TIMEOUT
comul := comul K,
counit := counit K,
coinv := coinv K,
coassoc := coassoc K,
counit_left := counit_left K,
counit_right := counit_right K,
coinv_right := coinv_right K,
coinv_left := coinv_left K,
}
noncomputable instance polynomial_hopf : hopf_algebra K K[X] := { -- elaboration of polynomial_hopf took 10.4s
comul := comul K,
counit := counit K,
coinv := coinv K,
coassoc := sorry,
counit_left := counit_left K,
counit_right := counit_right K,
coinv_right := coinv_right K,
coinv_left := coinv_left K,
}
```

#### Vasily Ilin (Apr 22 2022 at 01:03):

I did `lean --make src/polynomial_example.lean`

and it did not tell me that it timed out. So I guess it compiled it fine? Here is the output:

```
hopf_algebra :User\Github\Hopf\src\Hopf.lean: parsing at line 18←[2K
cumulative profiling times:
compilation 0.0022ms
decl post-processing 103ms
elaboration 27.4s
parsing 0.686ms
type checking 100ms
```

#### Damiano Testa (Apr 22 2022 at 01:48):

If there were an error, you would see what the error was. Since you are only seeing the output of the profiler, you are good.

#### Damiano Testa (Apr 22 2022 at 01:49):

On my computer, your first `noncomputable instance polynomial_hopf`

elaborates in 11s, while the one with the `sorry`

ed `coassoc`

elaborates in 3.5s.

I do not know why your times are so much higher, though.

#### Alex J. Best (Apr 22 2022 at 01:52):

What sort of computer are you using Vasily? Is it a laptop? If it was a small laptop it's conceivable that it could take a few times longer than for others i guess.

#### Vasily Ilin (Apr 22 2022 at 20:29):

@Alex J. Best , it's a surface pro 6 with Intel i5 CPU.

#### Alex J. Best (Apr 22 2022 at 21:19):

Yeah that's a fairly low power device so I'm not surprised lean is taking a long time for you compared with others.

Last updated: Dec 20 2023 at 11:08 UTC