/- Clara Löh; 10/2023 -/

import Mathlib.Tactic.Contrapose -- for contrapose
open Mathlib.Tactic.Contrapose

/- The penguin axioms -/

structure penguins (a : Type) where
  is_penguin : a → Prop 
  is_bark :    a → Prop 
  is_bite :    a → Prop   
  penguins_that_bark_dont_bite : ∀ x : a, is_penguin x → (is_bark x → ¬ is_bite x) 

/- A simple proof using the penguin axioms -/

theorem tux_does_not_bark 
  (p : penguins a) 
  (Tux : a)
  (Tux_is_penguin : p.is_penguin Tux)
  (Tux_is_bite : p.is_bite Tux)
: (¬ p.is_bark Tux)
:= 
by 
  have if_Tux_barks_then_doesnt_bite : p.is_bark Tux → ¬ p.is_bite Tux 
  := by exact p.penguins_that_bark_dont_bite Tux Tux_is_penguin

  have if_Tux_bites_then_doesnt_bark : p.is_bite Tux → ¬ p.is_bark Tux 
  := by contrapose! 
        exact if_Tux_barks_then_doesnt_bite  

  show ¬ p.is_bark Tux
  exact if_Tux_bites_then_doesnt_bark Tux_is_bite