Anything.lean

axiom two_plus_two_is_five: 2 + 2 = 5

theorem i_can_prove_false: False := by
  have two_plus_two_is_four: 2 + 2 = 4 := by simp
  have contradiction := Eq.trans two_plus_two_is_five.symm two_plus_two_is_four
  exact absurd contradiction (by simp)

theorem i_can_prove_anything_1: 5 - 2 = 2 := by
  have: False → 5 - 2 = 2 := by simp
  exact this i_can_prove_false

theorem i_can_prove_anything_2: 5 - 2 = 3 := by
  have: False → 5 - 2 = 3 := by simp
  exact this i_can_prove_false

theorem i_can_prove_anything_3: 3 + 3 = 1 := by
  have: False → 3 + 3 = 1 := by simp
  exact this i_can_prove_false