no goals
α : Type u_1
β : Type ?u.61329
γ : Type ?u.61332
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
⊢ WellFounded r
classical
cases nonempty_fintype α;
exact
  have :
    ∀ x y, r x y → (univ.filter fun z => r z x).card < (univ.filter fun z => r z y).card :=
    fun x y hxy =>
    Finset.card_lt_card <| by
      simp only [Finset.lt_iff_ssubset.symm, lt_iff_le_not_le, Finset.le_iff_subset,
          Finset.subset_iff, mem_filter, true_and_iff, mem_univ, hxy];
      exact
        ⟨fun z hzx => _root_.trans hzx hxy,
          not_forall_of_exists_not ⟨x, not_imp.2 ⟨hxy, irrefl x⟩⟩⟩
  Subrelation.wf (this _ _) (measure _).wf
case intro
α : Type u_1
β : Type ?u.61329
γ : Type ?u.61332
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
⊢ WellFounded r
α : Type u_1
β : Type ?u.61329
γ : Type ?u.61332
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
⊢ WellFounded r
cases nonempty_fintype α
no goals
case intro
α : Type u_1
β : Type ?u.61329
γ : Type ?u.61332
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
⊢ WellFounded r
exact
  have :
    ∀ x y, r x y → (univ.filter fun z => r z x).card < (univ.filter fun z => r z y).card :=
    fun x y hxy =>
    Finset.card_lt_card <| by
      simp only [Finset.lt_iff_ssubset.symm, lt_iff_le_not_le, Finset.le_iff_subset,
          Finset.subset_iff, mem_filter, true_and_iff, mem_univ, hxy];
      exact
        ⟨fun z hzx => _root_.trans hzx hxy,
          not_forall_of_exists_not ⟨x, not_imp.2 ⟨hxy, irrefl x⟩⟩⟩
  Subrelation.wf (this _ _) (measure _).wf
α : Type u_1
β : Type ?u.61329
γ : Type ?u.61332
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ (∀ ⦃x_1 : α⦄, r x_1 x → r x_1 y) ∧ ¬∀ ⦃x_1 : α⦄, r x_1 y → r x_1 x
α : Type u_1
β : Type ?u.61329
γ : Type ?u.61332
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ filter (fun z => r z x) univ ⊂ filter (fun z => r z y) univ
simp only [Finset.lt_iff_ssubset.symm, lt_iff_le_not_le, Finset.le_iff_subset,
    Finset.subset_iff, mem_filter, true_and_iff, mem_univ, hxy]
no goals
α : Type u_1
β : Type ?u.61329
γ : Type ?u.61332
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ (∀ ⦃x_1 : α⦄, r x_1 x → r x_1 y) ∧ ¬∀ ⦃x_1 : α⦄, r x_1 y → r x_1 x
exact
  ⟨fun z hzx => _root_.trans hzx hxy,
    not_forall_of_exists_not ⟨x, not_imp.2 ⟨hxy, irrefl x⟩⟩⟩