-- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/'Who.20Killed.20Aunt.20Agatha'.20puzzle
-- https://gist.github.com/utensil/17159725e5335f6a9688b7443fe0b3aa
-- https://www.tptp.org/cgi-bin/SystemOnTPTP
import Batteries.Tactic.Init
-- import Batteries.Tactic.RCases
-- import Mathlib.Tactic
-- import Mathlib.Logic.Basic

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, ¬ hates x y)
-- variable (pel55_10a : ∀ x, ∃ y, lives y ∧ ¬ hates x y)
variable (pel55_11 : agatha ≠ butler)
-- variable (pel55_12 : agatha ≠ charles)
-- variable (pel55_13 : charles ≠ butler)
include hates pel55_1 pel55_3 pel55_4 pel55_5 pel55_6 pel55_7 pel55_8 pel55_9 pel55_10 pel55_11 charles in
theorem result : killed agatha agatha := by
Goals accomplished! 🐙
  have 
haa: hates agatha agatha
haa : 
hates: u → u → Prop
hates 
agatha: u
agatha 
agatha: u
agatha := 
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_7 
agatha: u
agatha 
pel55_11: agatha ≠ butler
pel55_11
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
killed agatha agatha
  have 
nkca: ¬killed charles agatha
nkca : ¬
killed: u → u → Prop
killed 
charles: u
charles 
agatha: u
agatha :=
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
killed agatha agatha by
Goals accomplished! 🐙
    by_contra 
kca: killed charles agatha
kca
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
kca: killed charles agatha
False
    have 
hca: hates charles agatha
hca := 
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_4 
charles: u
charles 
agatha: u
agatha 
kca: killed charles agatha
kca
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
kca: killed charles agatha
hca: hates charles agatha
False
    have 
nhca: ¬hates charles agatha
nhca := 
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_6 
agatha: u
agatha 
haa: hates agatha agatha
haa
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
kca: killed charles agatha
hca: hates charles agatha
nhca: ¬hates charles agatha
False
    contradiction
Goals accomplished! 🐙
  have ⟨
n: u
n, 
ln: lives n
ln, 
kna: killed n agatha
kna⟩ := 
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_1
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed n agatha
killed agatha agatha
  obtain 
la: n = agatha
la
la | lb | lc: n = butler ∨ n = charles
 | 
lb: n = butler
lb
la | lb | lc: n = butler ∨ n = charles
 | 
lc: n = charles
lc := 
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_3 
n: u
n 
ln: lives n
ln
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed n agatha
la: n = agatha
inl
killed agatha agatha
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed n agatha
lb: n = butler
inr.inl
killed agatha agatha
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed n agatha
lc: n = charles
inr.inr
killed agatha agatha
  .
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed n agatha
la: n = agatha
inl
killed agatha agatha rw [
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed n agatha
la: n = agatha
inl
killed agatha agatha
la: n = agatha
la
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed agatha agatha
la: n = agatha
inl
killed agatha agatha]
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed agatha agatha
la: n = agatha
inl
killed agatha agatha at 
kna: killed n agatha
kna
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed agatha agatha
la: n = agatha
inl
killed agatha agatha
    exact 
kna: killed agatha agatha
kna
Goals accomplished! 🐙
  .
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed n agatha
lb: n = butler
inr.inl
killed agatha agatha rw [
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed n agatha
lb: n = butler
inr.inl
killed agatha agatha
lb: n = butler
lb
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed butler agatha
lb: n = butler
inr.inl
killed agatha agatha]
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed butler agatha
lb: n = butler
inr.inl
killed agatha agatha at 
kna: killed n agatha
kna
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed butler agatha
lb: n = butler
inr.inl
killed agatha agatha
    have 
nrba: ¬richer butler agatha
nrba : ¬
richer: u → u → Prop
richer 
butler: u
butler 
agatha: u
agatha := 
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_5 
butler: u
butler 
agatha: u
agatha 
kna: killed butler agatha
kna
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed butler agatha
lb: n = butler
nrba: ¬richer butler agatha
inr.inl
killed agatha agatha
    have 
hbb: hates butler butler
hbb : 
hates: u → u → Prop
hates 
butler: u
butler 
butler: u
butler := 
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_8 
butler: u
butler 
nrba: ¬richer butler agatha
nrba
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed butler agatha
lb: n = butler
nrba: ¬richer butler agatha
hbb: hates butler butler
inr.inl
killed agatha agatha
    simp [
Classical.skolem: ∀ {α : Sort ?u.1350} {b : α → Sort ?u.1349} {p : (x : α) → b x → Prop},
  (∀ (x : α), ∃ y, p x y) ↔ ∃ f, ∀ (x : α), p x (f x)
Classical.skolem] at 
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_10
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed butler agatha
lb: n = butler
nrba: ¬richer butler agatha
hbb: hates butler butler
pel55_10: ∃ f, ∀ (x : u), ¬hates x (f x)
inr.inl
killed agatha agatha
    have ⟨
sk: u → u
sk, 
nhsk: ∀ (x : u), ¬hates x (sk x)
nhsk⟩ := 
pel55_10: ∃ f, ∀ (x : u), ¬hates x (f x)
pel55_10
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed butler agatha
lb: n = butler
nrba: ¬richer butler agatha
hbb: hates butler butler
pel55_10: ∃ f, ∀ (x : u), ¬hates x (f x)
sk: u → u
nhsk: ∀ (x : u), ¬hates x (sk x)
inr.inl
killed agatha agatha
    have 
nhbsk: ¬hates butler (sk butler)
nhbsk : ¬
hates: u → u → Prop
hates 
butler: u
butler (
sk: u → u
sk 
butler: u
butler) := 
nhsk: ∀ (x : u), ¬hates x (sk x)
nhsk 
butler: u
butler
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed butler agatha
lb: n = butler
nrba: ¬richer butler agatha
hbb: hates butler butler
pel55_10: ∃ f, ∀ (x : u), ¬hates x (f x)
sk: u → u
nhsk: ∀ (x : u), ¬hates x (sk x)
nhbsk: ¬hates butler (sk butler)
inr.inl
killed agatha agatha
    have 
nhask: ¬hates agatha (sk butler)
nhask : ¬
hates: u → u → Prop
hates 
agatha: u
agatha (
sk: u → u
sk 
butler: u
butler) :=
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed butler agatha
lb: n = butler
nrba: ¬richer butler agatha
hbb: hates butler butler
pel55_10: ∃ f, ∀ (x : u), ¬hates x (f x)
sk: u → u
nhsk: ∀ (x : u), ¬hates x (sk x)
nhbsk: ¬hates butler (sk butler)
inr.inl
killed agatha agatha by
Goals accomplished! 🐙
      by_contra 
hask: hates agatha (sk butler)
hask
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed butler agatha
lb: n = butler
nrba: ¬richer butler agatha
hbb: hates butler butler
pel55_10: ∃ f, ∀ (x : u), ¬hates x (f x)
sk: u → u
nhsk: ∀ (x : u), ¬hates x (sk x)
nhbsk: ¬hates butler (sk butler)
hask: hates agatha (sk butler)
False
      have 
hbsk: hates butler (sk butler)
hbsk := 
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_9 (
sk: u → u
sk 
butler: u
butler) 
hask: hates agatha (sk butler)
hask
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed butler agatha
lb: n = butler
nrba: ¬richer butler agatha
hbb: hates butler butler
pel55_10: ∃ f, ∀ (x : u), ¬hates x (f x)
sk: u → u
nhsk: ∀ (x : u), ¬hates x (sk x)
nhbsk: ¬hates butler (sk butler)
hask: hates agatha (sk butler)
hbsk: hates butler (sk butler)
False
      contradiction
Goals accomplished! 🐙
    have 
eqsk: sk butler = butler
eqsk : 
sk: u → u
sk 
butler: u
butler = 
butler: u
butler :=
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed butler agatha
lb: n = butler
nrba: ¬richer butler agatha
hbb: hates butler butler
pel55_10: ∃ f, ∀ (x : u), ¬hates x (f x)
sk: u → u
nhsk: ∀ (x : u), ¬hates x (sk x)
nhbsk: ¬hates butler (sk butler)
nhask: ¬hates agatha (sk butler)
inr.inl
killed agatha agatha by
Goals accomplished! 🐙
      by_contra 
nesk: ¬sk butler = butler
nesk
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed butler agatha
lb: n = butler
nrba: ¬richer butler agatha
hbb: hates butler butler
pel55_10: ∃ f, ∀ (x : u), ¬hates x (f x)
sk: u → u
nhsk: ∀ (x : u), ¬hates x (sk x)
nhbsk: ¬hates butler (sk butler)
nhask: ¬hates agatha (sk butler)
nesk: ¬sk butler = butler
False
      have 
hbsk: hates agatha (sk butler)
hbsk := 
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_7 (
sk: u → u
sk 
butler: u
butler) 
nesk: ¬sk butler = butler
nesk
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed butler agatha
lb: n = butler
nrba: ¬richer butler agatha
hbb: hates butler butler
pel55_10: ∃ f, ∀ (x : u), ¬hates x (f x)
sk: u → u
nhsk: ∀ (x : u), ¬hates x (sk x)
nhbsk: ¬hates butler (sk butler)
nhask: ¬hates agatha (sk butler)
nesk: ¬sk butler = butler
hbsk: hates agatha (sk butler)
False
      contradiction
Goals accomplished! 🐙
    have 
nhbb: ¬hates butler butler
nhbb := 
eqsk: sk butler = butler
eqsk ▸ 
nhbsk: ¬hates butler (sk butler)
nhbsk
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed butler agatha
lb: n = butler
nrba: ¬richer butler agatha
hbb: hates butler butler
pel55_10: ∃ f, ∀ (x : u), ¬hates x (f x)
sk: u → u
nhsk: ∀ (x : u), ¬hates x (sk x)
nhbsk: ¬hates butler (sk butler)
nhask: ¬hates agatha (sk butler)
eqsk: sk butler = butler
nhbb: ¬hates butler butler
inr.inl
killed agatha agatha
    contradiction
Goals accomplished! 🐙
  .
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed n agatha
lc: n = charles
inr.inr
killed agatha agatha rw [
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed n agatha
lc: n = charles
inr.inr
killed agatha agatha
lc: n = charles
lc
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed charles agatha
lc: n = charles
inr.inr
killed agatha agatha]
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed charles agatha
lc: n = charles
inr.inr
killed agatha agatha at 
kna: killed n agatha
kna
u: Type
lives: u → Prop
killed, hates, richer: u → u → Prop
agatha, butler, charles: u
pel55_1: ∃ x, lives x ∧ killed x agatha
pel55_3: ∀ (x : u), lives x → x = agatha ∨ x = butler ∨ x = charles
pel55_4: ∀ (x y : u), killed x y → hates x y
pel55_5: ∀ (x y : u), killed x y → ¬richer x y
pel55_6: ∀ (x : u), hates agatha x → ¬hates charles x
pel55_7: ∀ (x : u), x ≠ butler → hates agatha x
pel55_8: ∀ (x : u), ¬richer x agatha → hates butler x
pel55_9: ∀ (x : u), hates agatha x → hates butler x
pel55_10: ∀ (x : u), ∃ y, ¬hates x y
pel55_11: agatha ≠ butler
haa: hates agatha agatha
nkca: ¬killed charles agatha
n: u
ln: lives n
kna: killed charles agatha
lc: n = charles
inr.inr
killed agatha agatha
    contradiction
Goals accomplished! 🐙
  done
Goals accomplished! 🐙