ee (Feb 03 2024 at 07:18): ee (Feb 03 2024 at 07:18):"proof -
assume 1: "cinv f ga"
assume 2: "(∀f g.( cinv f g) ⟹ ((f ≈> g) ∧ (g ≈> f))) "
have "(f ≈> ga ∧ (ga ≈> f) )" using 1 by auto"
I have this in my proof yet it won't accept it. It's okay if I try to do
" have "(f ≈> ga )" using 1 by auto" . I'm just struggling a lot proving the simplest things, this has taken me 3 hours or so and I have still not succeded lol. Help pls. I feel like I'm missing some crucial information because this all should be a lot simpler than it is for me.
ee (Feb 03 2024 at 07:54):just posting my solution in case there's anyone else frazzled with these basic things
"
lemma sth4 :
assumes 1 : "(cinv f g)"
shows "(f ≈> g) ∧ (g ≈> f)"
proof-
have 1: "f ≈> g" using assms by auto
have 2: "cinv g f" using assms by (rule Inverse_relSym)
hence 3: "(g ≈> f)" using assms by auto
show "(f ≈> g) ∧ (g ≈> f)" using 1 3 by auto
qed"
tips to self and others:
I think using have, hence etc makes a difference
using numbers to name assumptions is super helpful
I hope it'll get easier in time, best of luck to all lol
Yong Kiam (Feb 05 2024 at 06:11):it would generally be helpful if you give more background of what you're trying to do
note that instead of writing the conjunction explicitly, you might like to write shows "(f ≈> g)" "(g ≈> f)" which I think is more canonically formatted if you later want to intro/elim with it
Last updated: Apr 28 2024 at 08:19 UTC