section
variable (A B C : Prop)

theorem example_1 : (A ∧ B) → C → B ∧ C := by 
  rintro h1 : A ∧ B
  rintro h2 : C
  apply And.intro
  . exact And.right h1
  . exact And.left h2

theorem example_2 : A ∧ B → B ∧ A := by
  sorry

theorem example_3 : B ∨ A → A ∨ B := by
  rintro h : B ∨ A
  apply Or.elim h
  . intro b; right; exact b
  . sorry

open Classical

theorem example_4 : A ∨ ¬ A := by
  apply byContradiction
  intro (h1 : ¬ (A ∨ ¬ A))
  have h2 : ¬ A := by
    intro (h3 : A)
    have h4 : A ∨ ¬ A := Or.inl h3
    show False
    exact h1 h4
  have h5 : A ∨ ¬ A := Or.inr h2
  show False
  exact h1 h5

end