and_or_imp

Stream: general

[Johan Commelin]

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]

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