• My goal is ..., how can I prove it?
• My goal is a conjunction, how can I prove it?
• My goal contains a conjunction as a hypothesis, how can I use it?
• My goal is a disjunction, how can I prove it?
• My goal is an universally quantified statement, how can I prove it?
• My goal contains an universally quantified statement, how can I use it?
• My goal is an existential, how can I prove it?
• My goal is solvable by some lemma, how can I prove it?
• My goal contains False as a hypothesis, how can I prove it?
• My goal is an equality of two convertible terms, how can I prove it?
• My goal is a let x := a in ... , how can I prove it?
• My goal is a let (a, ..., b) := c in, how can I prove it?
• My goal contains some existential hypotheses, how can I use it?
• My goal is an equality, how can I swap the left and right hand terms?
• My hypothesis is an equality, how can I swap the left and right hand terms?
• My goal would be solvable using apply;assumption if it would not create meta-variables, how can I prove it?
• My goal is solvable by some lemma within a set of lemmas and I don't want to remember which one, how can I prove it?
• My goal is one of the hypotheses, how can I prove it?
• My goal appears twice in the hypotheses and I want to choose which one is used, how can I do it?
• What is the difference between applying one hypothesis or another in the context of the last question?
• My goal is a propositional tautology, how can I prove it?
• My goal is a first order formula, how can I prove it?
• My goal is solvable by a sequence of rewrites, how can I prove it?
• My goal is a disequality solvable by a sequence of rewrites, how can I prove it?
• My goal is an equality on some ring (e.g. natural numbers), how can I prove it?
• My goal is an equality on some field (e.g. real numbers), how can I prove it?
• My goal is an inequality on integers in Presburger's arithmetic (an expression built from +, -, constants and variables), how can I prove it?
• My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it?
• Tactics usage
• I want to state a fact that I will use later as a hypothesis, how can I do it?
• I want to state a fact that I will use later as an hypothesis and prove it later, how can I do it?
• What is the difference between Qed and Defined?
• How can I know what an automation tactic does in my example?
• Why doesn't auto work? How can I fix it?
• What is eauto?
• How can I speed up auto?
• What is the equivalent of tauto for classical logic?
• I want to replace some term with another in the goal, how can I do it?
• I want to replace some term with another in an hypothesis, how can I do it?
• I want to replace some symbol with its definition, how can I do it?
• How can I reduce some term?
• How can I declare a shortcut for some term?
• How can I perform case analysis?
• How can I prevent the case tactic from losing information?
• Why should I name my intros?
• How can I automatize the naming?
• I want to automatize the use of some tactic, how can I do it?
• I want to execute the proof with tactic only if it solves the goal, how can I do it?
• How can I do the opposite of the intro tactic?
• One of the hypotheses is an equality between a variable and some term. I want to get rid of this variable, how can I do it?
• What can I do if I get the message "generated subgoal term has metavariables in it"?
• How can I instantiate some metavariable?
• What is the use of the pattern tactic?
• What is the difference between assert, cut, and generalize?
• What can I do if Coqcan does not infer some implicit argument?
• How can I make explicit some implicit argument?
• Proof management
• How can I change the order of the subgoals?
• How can I change the order of the hypotheses?
• How can I change the name of a hypothesis?
• How can I delete hypotheses?
• How can I use a proof which is not finished?
• How can I state a conjecture?
• What is the difference between a lemma, a fact and a theorem?
• How can I organize my proofs?