Zulip Chat Archive

Stream: new members

Topic: tactic (solved)

Alex Zhang (Jun 20 2021 at 09:49):

How to apply the apply tactic to a hypothesis h in the context? (It seems that apply ... at h does not work)

OK.. I see. Apply apply to h is not logically correct in a proof.

Kevin Buzzard (Jun 20 2021 at 09:57):

I remember in 2017 having exactly the same question and answering it in the same way :-)

Kevin Buzzard (Jul 12 2021 at 18:32):

Are you confused about what the tactic does, or about the dot notation used in structures which means "if the user doesn't supply this field, then try this tactic to fill it in"?

Kevin Buzzard (Jul 12 2021 at 18:34):

def complete_graph (V : Type u) : simple_graph V :=
{ adj := ne }

means "let obviously prove sym and loopless because I can't be bothered to prove them myself"

Alex Zhang (Jul 12 2021 at 18:40):

Thank you, Kevin! (The reply is weirdly moved into another thread.)

Last updated: Dec 20 2023 at 11:08 UTC