In my Coq Proof, I've an hypothesis that say "A \/ A". Is there a way to simplify this in "A". Right now, I use destruct, but it duplicates the number of goals. I feel like this is a dumb question, but I don’t find how to do it.
You do not simplify it in A. You deduce A. Due to constructivism, it is better to say: you constuct A having A \/ A as your assumption.
Your deduction has to be sound, i.e. valid whenever A \/ A holds. There are two ways in which A \/ A can be true: either its left part is true or its right part is true (also, of course, both could be true at the same time, which we do not care about having both true implies having at least one of them - either left or right - true and that's sufficient). So in order to preserve soundness you must consider both cases and convince Coq's core machinery that both cases result in the construction of A.
If you want to get rid of A \/ A and replace it with A you can have a Lemma of the appropriate type and just apply this lemma. Like that:
Lemma OrAAImplA : forall (A : Prop), A \/ A -> A.
intros.
destruct H ; repeat assumption.
Qed.
And then just apply OrAAImplA to a hypothesis of type A \/ A, that's it.
As per the "real world", the code above is too verbose. You could replace destruct H ; repeat assumption with just tauto and that would do just fine.
Even better then: you could avoid having a named lemma at all by something like replace H with (a : A) by tauto. That would allow you to get rid of H : A \/ A and replace it by a : A (haven't checked it actually, might be a little bit more tricky to make it work; you have docs at your service!).
All of the above reduces to the same concept of construction, from which I started. The only difference is the amount of code to be written.
P.S. Normally you'd use Search to look up lemmas and theorems you expect to be in the standard library or imported packages. I would not be surprised if lemma of that sort already exists.