Idiomatic way to discard hypothesis?

Stream: new members

[Andreas Nuyts]

When I prove a theorem by not using one of its hypotheses, Lean gives me a warning.
What is the idiomatic way of saying that just for this proof, I want to suppress the warning because I know what I'm doing?

[Eric Wieser]

Is it telling you that you didn't use it at all, or didn't refer to it by name?

[Kenny Lau]

@Andreas Nuyts

omit h1 h2 h3 in
theorem xxx

[Eric Wieser]

A #mwe would help here

[Kenny Lau]

oh wait, your title and your first message don't match :melt:

[Kenny Lau]

Andreas Nuyts said:

When I prove a theorem by not using one of its hypotheses, Lean gives me a warning.

so there's one that shows up in your face and gives you yellow underlines, which is likely the one you're seeing, and for that one you suppress it by putting an underscore in front of the variable name, such as (_n : Nat) instead of (n : Nat)

for the other one that is only active when you actively use the command #lint afterwards, that one is disabled by @[nolint unusedArguments] theorem xxx