What does ` . obviously` mean?

Stream: new members

[Justus Springer]

I've seen this a lot in the category theory library, e.g.

structure functor (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D] :
  Type (max v₁ v₂ u₁ u₂) :=
(obj []    : C → D)
(map       : Π {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y)))
(map_id'   : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
(map_comp' : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = (map f) ≫ (map g) . obviously)

What does . obviously mean?

[Greg Price]

It's explained here:
https://leanprover-community.github.io/mathlib_docs/tactic/obviously.html

[Greg Price]

Rather, the definition of obviously is

[Greg Price]

The . foo syntax it's being used in is a way of supplying a tactic that gets used to fill in the field by default, if you don't supply one at the time of constructing a structure

[Justus Springer]

Thank you!

[Justus Springer]

Greg Price said:

It's explained here:
https://leanprover-community.github.io/mathlib_docs/tactic/obviously.html

Somehow I missed that

[Greg Price]

Ah, to be clear, I didn't mean to suggest that you should have found that already!

[Greg Price]

The syntax especially is a bit, er, non-obvious until you've seen an explicit discussion of what it means

[Kevin Buzzard]

The . tactic notation is explained in the lean 3 reference manual here