Lean solution for TopProver #27 ( https://top-prover.top/problem/27 )

topprover27.lean

inductive Two : Type
| C21: Two
| C22: Two

inductive Three : Type
| C31: Three
| C32: Three
| C33: Three

definition at_most_two (t: Type): Prop
:= ∃ x y: t, ∀ z: t, z = x ∨ z = y

lemma two_is_am_two: at_most_two Two
:=
begin
  rewrite at_most_two,
  existsi Two.C21,
  existsi Two.C22,
  intro z,
  cases z,
  left, refl,
  right, refl
end

lemma three_is_not_am_two: ¬ at_most_two Three
:=
begin
  rewrite at_most_two,
  intro h,
  cases h with x h1,
  cases h1 with y h2,
  cases x; cases y,
  all_goals {
    try {
      cases h2 Three.C31,
      all_goals { contradiction },
    },
    try {
      cases h2 Three.C32,
      all_goals { contradiction },
    },
    try {
      cases h2 Three.C33,
      all_goals { contradiction },
    },
  },
end

example: Two ≠ Three
:=
begin
  intro h,
  apply three_is_not_am_two,
  rewrite <-h,
  exact two_is_am_two
end

lemma three_is_not_am_two: ¬ at_most_two Three
:=
begin
  rewrite at_most_two,
  intro h,
  cases h with x h1,
  cases h1 with y h2,
  cases x; cases y;
  {
    have := h2 Three.C31,
    have := h2 Three.C32,
    have := h2 Three.C33,
    simp * at *,
  },
end