towers of algebras

Stream: new members

[Jon Eugster]

I think I could need some guidance of how Lean automatically finds -- or doesn't -- some implicit arguments.
With the following variables

import ring_theory.integral_closure
import ring_theory.localization

variables {A K L: Type*} [integral_domain A] [field L] [algebra (fraction_ring A) L]

it is true that $L$ is an $A$-algebra by combining the intermediate algebra maps $A \to \operatorname{Frac}(A) \to L$ and I can certainly state this:

def my_comp_of_algebras: algebra A L:=
begin
  refine ring_hom.to_algebra _,
  exact (algebra_map (fraction_ring A) L).comp (algebra_map A (fraction_ring A)),
end

But if I state other results, it doesn't automatically find the instance algebra A L (is 'instance' the correct terminology?):

example: algebra (integral_closure A (fraction_ring A)) (integral_closure A L) := sorry

(says failed to synthesize type class instance for algebra A L)

• attempt 1: I thought the thing labelled as def could be labelled as instance to fix this, but I seem to be misunderstanding instances as this leads to timeout errors.
• attempt 2: Then I thought I would have to add {algebra A L} or [algebra A L] to the preamble. From the former I hoped it would create it automatically, which it didn't, the latter works, but I have the feeling it just adds another $A$-algebra structure on $L$ instead of using the combined structure above, i.e. I can't show then that algebra A L = my_comp_of_algebras.
  example [algebra A L]: algebra (integral_closure A (fraction_ring A)) (integral_closure A L) := sorry

Could somebody please give me a hint on what I didn't understand yet and how to do this? Thank you for the help!

PS: Ultimately I am trying to get algebra maps (or just a linear map) A → (integral_closure A (fraction_field A)) → (integral_closure A L) and then split them (there's also more conditions, like $A$ being normal and $L$ being finite extension of $\operatorname{Frac}(K)$, but I thought they are irrelevant here).

[Anne Baanen]

Good questions! I have had similar struggles before, so let me take a look...

[Eric Wieser]

My guess would be that mathlib can infer algebra (fraction_ring A) L from algebra A Lbut not vice versa (assuming that's something that mathematically is possible)

[Eric Wieser]

Typeclass inference is used to build structures on complex objects out of structures on simpler ones

[Eric Wieser]

It's not allowed to go in both directions, as it can't handle loops

[Anne Baanen]

But if I state other results, it doesn't automatically find the instance algebra A L (is 'instance' the correct terminology?):

(instance is indeed the correct word here!) You're getting a missing instance error here because the typeclass system is only aware of declarations marked as instance, as you correctly tried to fix by replacing def with instance.

[Anne Baanen]

However, an instance of the form my_comp_of_algebras [algebra (fraction_ring A) L] : algebra A L cannot work automatically. This is because type class inference performs its search as follows:

• need to find instance algebra A L
• try to apply my_comp_of_algebras
  • need to find instance algebra (fraction_ring A) L
  • try to apply my_comp_of_algebras
    • need to find instance algebra (fraction_ring (fraction_ring A)) L
    • try to apply my_comp_of_algebras
      • ...

[Jon Eugster]

Eric Wieser said:

My guess would be that mathlib can infer algebra (fraction_ring A) L from algebra A Lbut not vice versa (assuming that's something that mathematically is possible)

Anne Baanen said:

However, an instance of the form my_comp_of_algebras [algebra (fraction_ring A) L] : algebra A L cannot work automatically. This is because type class inference performs its search as follows:

• need to find instance algebra A L
• try to apply my_comp_of_algebras
  • need to find instance algebra (fraction_ring A) L
  • try to apply my_comp_of_algebras
    • need to find instance algebra (fraction_ring (fraction_ring A)) L
    • try to apply my_comp_of_algebras
      • ...
        Oh I see the looping problem involved here.

[Jon Eugster]

Eric Wieser said:

My guess would be that mathlib can infer algebra (fraction_ring A) L from algebra A Lbut not vice versa (assuming that's something that mathematically is possible)

why is that?

[Anne Baanen]

Your solution is also on the right track: we can introduce a new algebra instance parameter, then try to show that this is indeed the correct one. I'm not completely sure whether this is always the case (would it follow from the universal property of fraction_ring?), but we can simply postulate that this holds:

import ring_theory.integral_closure
import ring_theory.localization

variables {A K L: Type*} [integral_domain A] [field L]  [algebra (fraction_ring A) L]

def my_comp_of_algebras : algebra A L:=
begin
refine ring_hom.to_algebra _,
exact (algebra_map (fraction_ring A) L).comp (algebra_map A (fraction_ring A)),
end

variables [algebra A L] [is_scalar_tower A (fraction_ring A) L]

example : (algebra_map (fraction_ring A) L).comp (algebra_map A (fraction_ring A)) = algebra_map A L :=
(is_scalar_tower.algebra_map_eq _ _ _).symm

[Anne Baanen]

Eric, there's an algebra map from A to fraction_ring A, not the other way. So mathematically going from algebra (fraction_ring A) L to algebra A L is the correct direction

[Anne Baanen]

(Fixed the example, sorry. I should run my code before posting it! :P)

[Jon Eugster]

Anne Baanen said:

variables [algebra A L] [is_scalar_tower A (fraction_ring A) L]

I did use is_scalar_tower at some point before, but hesitated on using too many conditions that seem to follow automatic from a maths perspective. In that case I just throw in a couple of them, thank you!

[Jon Eugster]

Can I also ask you about integral closure @Anne Baanen ? I found this [integrally_closed: integral_closure A (fraction_ring A) = ⊥] but I can't really use it. I don't have a MWE ready but essentially I want to say that I get a map integral_closure A (fraction_ring A) →+* A which is a bijection...

[Eric Wieser]

I agree with Anne's snippet, the way to set this up is indeed [algebra A L] [algebra (fraction_ring A) L] [is_scalar_tower A (fraction_ring A) L], as lean already provides docs#fraction_ring.algebra

[Jon Eugster]

thanks!

[Anne Baanen]

I think you want something like docs#algebra.bot_equiv_of_injective

[Jon Eugster]

Anne Baanen said:

I think you want something like docs#algebra.bot_equiv_of_injective

Looks like it, didn't see that before. Thanks for the help

[Anne Baanen]

I can't find anything that says that there's an equivalence between two equal subalgebras, which would give you your exact statement.

[Anne Baanen]

Let me see if I can build it easily...

[Eric Wieser]

If the subalgebras are equal then that's presumably just something like h \t alg_equiv.id?

[Eric Wieser]

Do we have that definition for other structures?: docs#linear_equiv.of_eq maybe exists?

[Anne Baanen]

/-- Two subalgebras that are equal are also equivalent as algebras. -/
@[simps]
def equiv_of_eq (S T : subalgebra R A) (h : S = T) : S ≃ₐ[R] T :=
{ to_fun := λ x, ⟨x, h ▸ x.2⟩,
  inv_fun := λ x, ⟨x, h.symm ▸ x.2⟩,
  map_mul' := λ _ _, rfl,
  commutes' := λ _, rfl,
  .. linear_equiv.of_eq _ _ (congr_arg to_submodule h) }

[Anne Baanen]

h \t alg_equiv.refl S doesn't work (looks like because it's not smart enough to see that only one S should become a T)

[Eric Wieser]

What you have is better definitionally anyway

[Eric Wieser]

I'd recommend simps apply and a manual lemma though, to match docs#linear_equiv.of_eq_symm:

@[simp] lemma of_eq_symm (h : p = q) : (of_eq p q h).symm = of_eq q p h.symm := rfl

[Anne Baanen]

Hmm, should it be called subalgebra.equiv_of_eq or alg_equiv.of_eq?

[Anne Baanen]

(The latter might not work so well with intermediate_field)

[Eric Wieser]

The latter is consistent with linear_equiv.of_eq

[Eric Wieser]

We already have duplicate names in this space; docs#equiv.set_congr and docs#equiv.set.of_eq are the same definition

[Anne Baanen]

I'll go with the former since there's not a lot of consensus, and maybe we want to make the same definition intermediate_field (where the appropriate equiv is still alg_equiv, which would cause name collisions).

[Anne Baanen]

#7590

[Jon Eugster]

So that means I can just update mathlib in my project once that has been accepted and it'll be in there? That is amazing :D

[Anne Baanen]

If everything goes well and the PR gets accepted, yes :) If you are impatient, you should be able to copy-paste the definitions into your own project:

/-- Two subalgebras that are equal are also equivalent as algebras.
This is the `subalgebra` version of `linear_equiv.of_eq` and `equiv.set.of_eq`. -/
@[simps apply]
def equiv_of_eq {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
  (S T : subalgebra R A) (h : S = T) : S ≃ₐ[R] T :=
{ to_fun := λ x, ⟨x, h ▸ x.2⟩,
  inv_fun := λ x, ⟨x, h.symm ▸ x.2⟩,
  map_mul' := λ _ _, rfl,
  commutes' := λ _, rfl,
  .. linear_equiv.of_eq _ _ (congr_arg to_submodule h) }

@[simp] lemma equiv_of_eq_symm {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
  (S T : subalgebra R A) (h : S = T) :
  (equiv_of_eq S T h).symm = equiv_of_eq T S h.symm :=
rfl

[Kevin Buzzard]

Just to note that if $L$ is an $A$-algebra then even if $L$ is a field it might not be an algebra for the field of fractions for $A$, e.g. $\Z/37\Z$ is an algebra for $\Z$ but cannot be given the structure of an algebra for $\mathbb{Q}$.

[Eric Rodriguez]

is there any conditions that allow it to be such?

[Anne Baanen]

Not 100% sure, but I suppose it's exactly when the algebra map from A to L maps every nonzero element of A to a unit in L, by the universal property of the localization.

[Jon Eugster]

Kevin Buzzard said:

Just to note that if $L$ is an $A$-algebra then even if $L$ is a field it might not be an algebra for the field of fractions for $A$, e.g. $\Z/37\Z$ is an algebra for $\Z$ but cannot be given the structure of an algebra for $\mathbb{Q}$.

Good point. I realised I don't actually need this map to be an algebra map/linear map, I only need to look at the composite of multiple maps.

[Jon Eugster]

Also, everything in my project is in equal characteristics (0,0), i.e. when you have $\mathbb{Q} \subset A$

[Kevin Buzzard]

that doesn't fix the maths problem, there are char 0 counterexamples, but this is not the point -- the answer to your question is this is_scalar_tower class. It's a bit of an adjustment coming from maths on paper to maths in Lean's type theory, you need to pick up a few basic tricks and this is one.

[Jon Eugster]

But it helps realising that certain things are wrong (and you don't even need them), so thanks for the comment! It's so easy to get lost in the code and try to proof things that don't hold

[Jon Eugster]

Anne Baanen said:

@[simps apply]
def equiv_of_eq {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
  (S T : subalgebra R A) (h : S = T) : S ≃ₐ[R] T :=
...

After putting that in I am left with two small conversion problems, which I unfortunately don't think I can solve with my own understanding.

I want to take an integral element in $K:=\operatorname{Frac}(A)$ and say that it is actually in $A$. (we have $A$ integrally closed.)

(For context that would help me to manually define then a function (integral_closure A L) →ₗ[A] A and manually check the map_add' and map_smul' conditions.)

Here are the steps I tried, the two I am stuck on are

1) going from is_integral A x to x:integral_closure A K (where x:K) and
2) going from z:↑⊥ to z:A (I think ↑⊥ is a subalgebra A K).

Moreover, is there better syntax for working on this? I am just treating it as if it was a Prop statement, which works but I think some tactics like library_search or hint don't like constructions like this...

Thank you once more for the help!

import ring_theory.integral_closure
import ring_theory.localization

variables {A K L: Type*} [integral_domain A] [field L]  [algebra (fraction_ring A) L]

def restrict_to_A  (x: (fraction_ring A)) [is_integral A x][integrally_closed: integral_closure A (fraction_ring A) = ⊥]: A :=
begin
  have y: integral_closure A (fraction_ring A) := sorry, -- that should be a straight forward conversion I haven't found yet.
  replace integrally_closed := equiv_of_eq (integral_closure A (fraction_ring A)) ⊥ integrally_closed,
  have z := integrally_closed.to_fun y,
  have y': A := sorry, -- I expect a conversion from elements in `↑⊥: subalgebra A (fraction_field A)` to elements of `A`.
  use y',
end

[Yakov Pechersky]

Does the following help?

def integral_closure.mk (x : fraction_ring A) (hx : is_integral A x) :
  integral_closure A (fraction_ring A) := ⟨x, hx⟩

[Kevin Buzzard]

@Jon Eugster I get an error on equiv_of_eq if I paste your code into VS Code.

[Jon Eugster]

Kevin Buzzard said:

Jon Eugster I get an error on equiv_of_eq if I paste your code into VS Code.

@[simps apply]
def equiv_of_eq {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
  (S T : subalgebra R A) (h : S = T) : S ≃ₐ[R] T :=
{ to_fun := λ x, ⟨x, h ▸ x.2⟩,
  inv_fun := λ x, ⟨x, h.symm ▸ x.2⟩,
  map_mul' := λ _ _, rfl,
  commutes' := λ _, rfl,
  .. linear_equiv.of_eq _ _ (congr_arg subalgebra.to_submodule h) }

There's a subalgebra.to_submodule in the proof that needs to be adjusted from what Anne wrote

[Kevin Buzzard]

Can you post a #mwe? Edit your original post

[Jon Eugster]

This is what I have in my file:

import ring_theory.integral_closure
import ring_theory.localization

variables {A K L: Type*} [integral_domain A] [field L]  [algebra (fraction_ring A) L]

@[simps apply]
def equiv_of_eq {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
  (S T : subalgebra R A) (h : S = T) : S ≃ₐ[R] T :=
{ to_fun := λ x, ⟨x, h ▸ x.2⟩,
  inv_fun := λ x, ⟨x, h.symm ▸ x.2⟩,
  map_mul' := λ _ _, rfl,
  commutes' := λ _, rfl,
  .. linear_equiv.of_eq _ _ (congr_arg subalgebra.to_submodule h) }

@[simp] lemma equiv_of_eq_symm {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
  (S T : subalgebra R A) (h : S = T) :
  (equiv_of_eq S T h).symm = equiv_of_eq T S h.symm :=
rfl

#check (⊥: subalgebra A (fraction_ring A))
def restrict_to_A (x: (fraction_ring A)) [is_integral A x][integrally_closed: integral_closure A (fraction_ring A) = ⊥]: A :=
begin
  have y: integral_closure A (fraction_ring A) := sorry, -- that should be a straight forward conversion I haven't found yet.
  replace integrally_closed := equiv_of_eq (integral_closure A (fraction_ring A)) ⊥ integrally_closed,
  have z := integrally_closed.to_fun y,
  have y': A := sorry, -- I expect a conversion from elements in `↑⊥: subalgebra A (fraction_field A)` to elements of `A`.
  use y',
end

[Jon Eugster]

Yakov Pechersky said:

Does the following help?

def integral_closure.mk (x : fraction_ring A) (hx : is_integral A x) :
  integral_closure A (fraction_ring A) := ⟨x, hx⟩

Yes, that seems to be the first sorry, thank you! The ⟨ ⟩ is still very mysterious to me

[Eric Wieser]

If you want to understand ⟨ ⟩, replace it with {! !}, click the lightbulb in vscode and "generate structure under consideration" or similar

[Eric Wieser]

In your case it will expand to { val := _, property := _ }. So on this line, ⟨x, hx⟩ is just short for { val := x, property := hx }

[Jon Eugster]

Eric Wieser said:

If you want to understand ⟨ ⟩, replace it with {! !}, click the lightbulb in vscode and "generate structure under consideration" or similar

oh that's neat!

[Eric Wieser]

Another way to think of ⟨ ⟩ is as it being like a term-mode version of the split or constructor tactic

[Jon Eugster]

Updated MWE on what's still left from my original question.

import ring_theory.integral_closure
import ring_theory.localization

variables {A K L: Type*} [integral_domain A] [field L]  [algebra (fraction_ring A) L]

-- I expect a conversion from elements in `↑⊥: subalgebra A (fraction_field A)` to elements of `A`.
def my_mk (x : integral_closure A (fraction_ring A)) [h: (integral_closure A (fraction_ring A)) ≃ₐ[A] (⊥:subalgebra A (fraction_ring A))]:
  A := sorry

[Yakov Pechersky]

A comment: [my hypothesis] should be really used only for things that the typeclass search can use, like [group G] [field K] [algebra A L]

[Jon Eugster]

so (...) for everything else?

[Yakov Pechersky]

And a ≃ₐ[A] is not actually a lemma, it is a def, it is a bundled combination of a function and its reverse and all of the proofs saying that it is an equivalence of algebras

[Yakov Pechersky]

I think somehow subalgebra.bot_equiv should help here

[Yakov Pechersky]

Using alg_equiv.trans. Basically, you compose several "canonical isomorphisms"

[Jon Eugster]

Thank you @Yakov Pechersky I think I managed to use the two statements you mentioned to get the desired result!

[Yakov Pechersky]

Can you share?

[Jon Eugster]

yep, give me a second to clean it up

[Jon Eugster]

Still a big mess, but here's roughly how all the help can be combined to get that an integral element in $\operatorname{Frac}(A)$ actually
lies in $A$.

import ring_theory.integral_closure
import ring_theory.localization
import algebra.algebra.subalgebra

variables {A K L: Type*} [integral_domain A] [field L]  [algebra (fraction_ring A) L]
variable (integrally_closed: integral_closure A (fraction_ring A) = ⊥)

-- Anne PRed this into mathlib, can be removed later.
@[simps apply]
def equiv_of_eq {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
  (S T : subalgebra R A) (h : S = T) : S ≃ₐ[R] T :=
{ to_fun := λ x, ⟨x, h ▸ x.2⟩,
  inv_fun := λ x, ⟨x, h.symm ▸ x.2⟩,
  map_mul' := λ _ _, rfl,
  commutes' := λ _, rfl,
  .. linear_equiv.of_eq _ _ (congr_arg subalgebra.to_submodule h) }


-- Thx Yakov Perchersky
def integral_closure.mk (x : fraction_ring A) (hx : is_integral A x) :
  integral_closure A (fraction_ring A) := ⟨x, hx⟩ --- {!   !} is useful!


-- assuming `A` is integrally closed in it's fraction field, this
-- is the corresponding equivalence of algebras
noncomputable def canoncial_equiv
(h: function.injective (algebra_map A (fraction_ring A))):
(integral_closure A (fraction_ring A)) ≃ₐ[A] A :=
alg_equiv.trans (equiv_of_eq (integral_closure A (fraction_ring A)) ⊥ integrally_closed) (algebra.bot_equiv_of_injective h)


-- This is how we can get an element in `A` from an integral element in `fraction_ring A`.
-- Injectivity should be deducable from something, `A: integral_domain`?
noncomputable def restriction_to_A (x: (fraction_ring A)) [h:is_integral A x] (h': function.injective (algebra_map A (fraction_ring A)))
(integrally_closed: integral_closure A (fraction_ring A) = ⊥)
: A :=
begin
  have y: integral_closure A (fraction_ring A) := integral_closure.mk x h,
  have z := (canoncial_equiv integrally_closed h').to_fun y,
  use z,
end

[Yakov Pechersky]

-- Thx Yakov Pechersky -- (only 1 `r`)
def integral_closure.mk (x : fraction_ring A) (hx : is_integral A x) :
  integral_closure A (fraction_ring A) := ⟨x, hx⟩ --- {!   !} is useful!


-- assuming `A` is integrally closed in it's fraction field, this
-- is the corresponding equivalence of algebras
noncomputable def canonical_equiv
  (h : function.injective (algebra_map A (fraction_ring A))):
  (integral_closure A (fraction_ring A)) ≃ₐ[A] A :=
(equiv_of_eq (integral_closure A (fraction_ring A)) ⊥ integrally_closed).trans
  (algebra.bot_equiv_of_injective h)


-- This is how we can get an element in `A` from an integral element in `fraction_ring A`.
-- Injectivity should be deducable from something, `A : integral_domain`?
noncomputable def restriction_to_A (integrally_closed : integral_closure A (fraction_ring A) = ⊥)
  (h' : function.injective (algebra_map A (fraction_ring A)))
  (x : fraction_ring A) (hx : is_integral A x) : A :=
canonical_equiv integrally_closed h' (integral_closure.mk x hx)

[Yakov Pechersky]

Try not to define def using tactic begin ... end mode

[Yakov Pechersky]

(to first pass)

[Yakov Pechersky]

We can use canonical_equiv or any ≃ₐ[A] (or any ≃) as a function, no need to use to_fun

[Yakov Pechersky]

@Eric Wieser What's wrong about this example?

example : function.injective (algebra_map A (fraction_ring A)) :=
begin
  convert (algebra_map _ _).injective
end
/-
type mismatch at application
  (algebra_map ?m_6 ?m_7).injective
term
  algebra_map ?m_1 ?m_2
has type
  @ring_hom ?m_1 ?m_2 (@comm_semiring.to_semiring ?m_1 ?m_3) ?m_4 : Type (max ? ?)
but is expected to have type
  @ring_hom ?m_1 ?m_2 (@ring.to_semiring ?m_1 (@division_ring.to_ring ?m_1 ?m_3)) ?m_4 : Type (max ? ?)
Additional information:
/home/yakov/code/mathlib/src/test.lean: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch at application
    (algebra_map ?m_6 ?m_7).injective
  term
    algebra_map ?m_1 ?m_2
  has type
    @ring_hom ?m_1 ?m_2 (@comm_semiring.to_semiring ?m_1 ?m_3) ?m_4 : Type (max ? ?)
  but is expected to have type
    @ring_hom ?m_1 ?m_2 (@ring.to_semiring ?m_1 (@division_ring.to_ring ?m_1 ?m_3)) ?m_4 : Type (max ? ?)
-/

[Eric Wieser]

docs#ring_hom.injective needs the algebra to be over a field division_ring, not just an integral_domain

[Kevin Buzzard]

There should be some lemma that for an integral domain the map into the field of fractions is injective

[Eric Wieser]

Perhaps, but docs#fraction_ring.algebra is the very last line in the file, so either mathlib doesn't have it, it's in a downstream file somewhere, or it's true more generally and we're looking for the wrong thing

[Kevin Buzzard]

docs#fraction_map.injective

[Eric Wieser]

Look's to me like we're missing the rfl-lemma that algebra_map A (fraction_ring A) = (fraction_map.of A).to_map:

lemma algebra_map_eq : algebra_map A (fraction_ring A) = (fraction_ring.of A).to_map := rfl

as then we would have found the injective lemma with library_search

[Eric Wieser]

But indeed that lemma closes the goal

example : function.injective (algebra_map A (fraction_ring A)) :=
fraction_map.injective _

[Yakov Pechersky]

Great!
Then you have just this

noncomputable def canonical_equiv :
  (integral_closure A (fraction_ring A)) ≃ₐ[A] A :=
(equiv_of_eq (integral_closure A (fraction_ring A)) ⊥ integrally_closed).trans
  (algebra.bot_equiv_of_injective (fraction_map.injective _))

[Yakov Pechersky]

But @Jon Eugster, why do you need to construct an A from something that you know only separately is of type fraction_map A and holds is_integral A?

[Yakov Pechersky]

Instead of working on such elements, perhaps you just need the right composition of functions/isos

[Jon Eugster]

Yakov Pechersky said:

Instead of working on such elements, perhaps you just need the right composition of functions/isos

Thanks for work above, I'll go through it tomorrow. Maybe I should explain more of the context. I thought I give it a shot and see how far I'd get formalising the direct summand conjecture; in equal characteristics (0,0) to start with. The proof reads like this
dsc.png

I did manage to construct the trace as map L →ₗ[K] K and show that it splits algebra_map K L, so know I would like to adapt this to a map (integral_closure A L) →ₗ[A] A. I guess there should be a way to combine this from different maps but the problem I encountered is that although you have a combination of maps (integral_closure A L) → L → K and (integral_closure A K) → A you don't have a map K→(integral_closure A K), but the composition of everything exists and is a linear map. So I thought as last resource I would give it a go and define this composition explicitly by constructing an element in A.

Another challenge is then the "we can enlarge $B$ to be the integral closure ..." but I haven't started on that yet.

So if you have any tips/tricks or opinions I am very happy to listen and learn :)

[Kevin Buzzard]

This is a great way of learning Lean! There are plenty of people here who know enough to be able to help you out.

The best way to ask a question here is to post fully working lean code including all imports etc and a sorry, and ask how to fill it in. You'll get stuck many times initially, but it will all begin to make sense later on as you learn the tricks.

[Jon Eugster]

Yakov Pechersky said:

Try not to define def using tactic begin ... end mode

So far I used begin ... end because it seems more iterative, i.e. you can create stuff step-by-step with have, and then once your done, you can rewrite it as a direct term without tactic mode, is there a better approach to do such constructions?

[Johan Commelin]

@Jon Eugster You can write

def foo : some_type :=
partial _ construction (of my _ definition)

and if you put your cursor on one of the _, then the goal window will show you the remaining goal.

[Eric Wieser]

Often it's still easier to use tactic mode first as Jon describes though, especially since sometimes it saves you from elaborator quirks