Swap a conjunction

1/4 ~10 minlean

Prove that conjunction is commutative in one direction.

2 lines · Lean 4

theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P := by
  sorry

start

1/3

Contexte local Γ

P Q : Prop

Objectif courant

⊢ P ∧ Q → Q ∧ P

Objectifs

Indices

Voir la solution

theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P := by
  intro h
  exact ⟨h.2, h.1⟩