by_contra

Stream: new members

[Faris Hafizhan Hakim]

hi, im trying to find the definition of by_contra but i can't seem to find it. firstly, the tactic doesn't work if i don't import Mathlib.Tactic, so i think it's not on the lean standard library. secondly, in the docs i could only find the definition of by_contra! in mathlib4/Mathlib/Tactic /ByContra.lean but not the regular one. appreciate if anyone could help me with this!

[Damiano Testa]

#help tactic "by_contra" may give more information.

[Ruben Van de Velde]

Hitting F12 on a use site jumps to .lake/packages/batteries/Batteries/Tactic/Init.lean

[Faris Hafizhan Hakim]

Thanks!