Zulip Chat Archive

Stream: general

Topic: and_or_imp


Johan Commelin (Dec 03 2021 at 14:19):

How does one prove this in a way that logic/basic.lean will accept?

lemma decidable.and_or_imp {α β γ : Prop} [decidable α] :
  (α  β)  (α  γ)  α  (β  γ) :=
by tauto

Ruben Van de Velde (Dec 03 2021 at 14:25):

Does this work?

import logic.basic

lemma decidable.and_or_imp {α β γ : Prop} [decidable α] :
  (α  β)  (α  γ)  α  (β  γ) :=
begin
  cases decidable.em α with a a,
  simp only [true_and, iff_self, a, forall_true_left],
  simp only [forall_false_left, false_or, iff_self, a, false_and],
end

Last updated: Dec 20 2023 at 11:08 UTC