Aunt Agatha

puz.lean

-- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/'Who.20Killed.20Aunt.20Agatha'.20puzzle

import Mathlib.Tactic

variable (u : Type)
variable (lives : u → Prop)
variable (killed hates richer : u → u → Prop)
variable (agatha butler charles : u)

variable (pel55_1 : ∃ x : u, lives x ∧ killed x agatha)
variable (pel55_2_1 : lives agatha)
variable (pel55_2_2 : lives butler)
variable (pel55_2_3 : lives charles)
variable (pel55_3 : ∀ x, lives x → x = agatha ∨ x = butler ∨ x = charles)

variable (pel55_4 : ∀ x y, killed x y → hates x y)
variable (pel55_5 : ∀ x y, killed x y → ¬ richer x y)
variable (pel55_6 : ∀ x, hates agatha x → ¬ hates charles x)
variable (pel55_7 : ∀ x, x ≠ butler → hates agatha x)

variable (pel55_8 : ∀ x, ¬ richer x agatha → hates butler x)
variable (pel55_9 : ∀ x, hates agatha x → hates butler x)

variable (pel55_10 : ∀ x, ∃ y, lives y ∧ ¬ hates x y)
variable (pel55_11 : agatha ≠ butler)
-- variable (pel55_12 : agatha ≠ charles)
variable (pel55_13 : charles ≠ butler)

theorem result : killed agatha agatha := by
  have haa : hates agatha agatha := by
    exact pel55_7 agatha pel55_11
  have nkca : ¬killed charles agatha := by
    by_contra kca
    have nhca : ¬hates charles agatha := by
      exact pel55_6 agatha haa
    have hca : hates charles agatha := by
      exact pel55_4 charles agatha kca
    contradiction
  have nkba : ¬killed butler agatha := by
    by_contra kba
    have rba : richer butler agatha := by
      by_contra nrba
      have hbb : hates butler butler := by
        exact pel55_8 butler nrba
      have nhbb : ¬hates butler butler := by
        by_contra hbb
        have hba : hates butler agatha := by
          exact pel55_9 agatha haa
        have hbc : hates butler charles := by
          exact pel55_9 charles (pel55_7 charles pel55_13)
        have hbe : ¬∃ y, lives y ∧ ¬hates butler y := by
          refine imp_false.mp ?_
          intro he
          rcases he with ⟨e, lnhbe⟩
          have labc := by exact pel55_3 e
          have ⟨le, nhbe⟩ := lnhbe
          have hl := labc le
          rcases hl with ha | hb | hc
          . rw [ha] at nhbe
            contradiction
          . rw [hb] at nhbe
            contradiction
          . rw [hc] at nhbe
            contradiction
        have nhbe : ∃ y, lives y ∧ ¬hates butler y := by
          exact pel55_10 butler
        contradiction
      contradiction
    have nrba :  ¬richer butler agatha := by
      exact pel55_5 butler agatha kba
    contradiction
  by_contra nkaa
  have nka : ¬∃ x : u, lives x ∧ killed x agatha := by
    refine imp_false.mp ?_
    intro ka
    rcases ka with ⟨e, lkea⟩
    have labc := by exact pel55_3 e
    have ⟨le, kea⟩ := lkea
    have hl := labc le
    rcases hl with ha | hb | hc
    . rw [ha] at kea
      contradiction
    . rw [hb] at kea
      contradiction
    . rw [hc] at kea
      contradiction
  contradiction