tactic (solved)

Stream: new members

[Alex Zhang]

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]

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

[Kevin Buzzard]

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]

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]

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