and_self

Stream: mathlib4

[Kevin Buzzard]

Bleurgh and_self is Proppy in core Lean:

@[simp] theorem and_self (p : Prop) : (p ∧ p) = p := propext ⟨(·.1), fun h => ⟨h, h⟩⟩

but that's And not and! What do I call

theorem and_self (b : Bool) : (b && b) = b := by cases b <;> simp

in mathlib4?

[Scott Morrison]

Bool.and_self?

[Kevin Buzzard]

And can I tell #align that?

[Kevin Buzzard]

oh lol it's already there :-)

[Scott Morrison]

Yeah, increasingly, grepping for #align.*myWeirdlyNamedTheorem is going to be part of the workflow...