Theorem: Finite.converseWellFounded_of_trans_irrefl (Logic/Vorspiel/BinaryRelations.lean)

State before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
inst✝² : Finite α
inst✝¹ : IsTrans α rel
inst✝ : IsIrrefl α rel
⊢ ConverseWellFounded rel
Tactic:
apply @Finite.wellFounded_of_trans_of_irrefl _ _ _
  ⟨by intro a b c rba rcb; exact IsTrans.trans c b a rcb rba⟩
  ⟨by simp [flip, IsIrrefl.irrefl]⟩
State after:
no goals

State before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
inst✝² : Finite α
inst✝¹ : IsTrans α rel
inst✝ : IsIrrefl α rel
⊢ ∀ (a b c : α),
    flip (fun x x_1 => rel x x_1) a b → flip (fun x x_1 => rel x x_1) b c → flip (fun x x_1 => rel x x_1) a c
Tactic:
intro a b c rba rcb
State after:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
inst✝² : Finite α
inst✝¹ : IsTrans α rel
inst✝ : IsIrrefl α rel
a b c : α
rba : flip (fun x x_1 => rel x x_1) a b
rcb : flip (fun x x_1 => rel x x_1) b c
⊢ flip (fun x x_1 => rel x x_1) a c

State before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
inst✝² : Finite α
inst✝¹ : IsTrans α rel
inst✝ : IsIrrefl α rel
a b c : α
rba : flip (fun x x_1 => rel x x_1) a b
rcb : flip (fun x x_1 => rel x x_1) b c
⊢ flip (fun x x_1 => rel x x_1) a c
Tactic:
exact IsTrans.trans c b a rcb rba
State after:
no goals

State before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
inst✝² : Finite α
inst✝¹ : IsTrans α rel
inst✝ : IsIrrefl α rel
⊢ ∀ (a : α), ¬flip (fun x x_1 => rel x x_1) a a
Tactic:
simp [flip, IsIrrefl.irrefl]
State after:
no goals