avoid writing (some?) simp-rfl lemmas

Stream: general

[Johan Commelin]

I've brought this up before, but I'dd really hope that there is a way to get rid of blocks like this:

section simp

section
variables {X Y : comma L₂ R} {f : X ⟶ Y} {l : L₁ ⟹ L₂}
@[simp] lemma map_left_obj_left  : ((map_left R l).obj X).left  = X.left                := rfl
@[simp] lemma map_left_obj_right : ((map_left R l).obj X).right = X.right               := rfl
@[simp] lemma map_left_obj_hom   : ((map_left R l).obj X).hom   = l.app X.left ≫ X.hom := rfl
@[simp] lemma map_left_map_left  : ((map_left R l).map f).left  = f.left                := rfl
@[simp] lemma map_left_map_right : ((map_left R l).map f).right = f.right               := rfl
end

section
variables {X Y : comma L R₁} {f : X ⟶ Y} {r : R₁ ⟹ R₂}
@[simp] lemma map_right_obj_left  : ((map_right L r).obj X).left  = X.left                 := rfl
@[simp] lemma map_right_obj_right : ((map_right L r).obj X).right = X.right                := rfl
@[simp] lemma map_right_obj_hom   : ((map_right L r).obj X).hom   = X.hom ≫ r.app X.right := rfl
@[simp] lemma map_right_map_left  : ((map_right L r).map f).left  = f.left                 := rfl
@[simp] lemma map_right_map_right : ((map_right L r).map f).right = f.right                := rfl
end

end simp

[Johan Commelin]

You define a new category, and afterwards you have to state pages of trivialities. There must be some structure to this, which we can abuse, so that automation just does this for us. Has there been any thought in this direction?

[Reid Barton]

You can put @[simp] on the thing you defined (I guess map_left, map_right)

[Johan Commelin]

Is that good practice? I thought it was some how considered evil, because it marked too much as simp?

[Mario Carneiro]

it's probably not what you want, because then it will unfold even when it is not being projected

[Johan Commelin]

Aha, so I want derive simp-projections

[Johan Commelin]

Is that possible?

[Mario Carneiro]

in theory

[Mario Carneiro]

it gets complicated with nested structures, but you could inspect the definition for a structure instance and extract the parts

[Mario Carneiro]

this would basically be the same thing that the equation compiler does

[Johan Commelin]

I see. I hope someone with a lot of tactic-fu will pop up and write something like this (-;