awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
hs : IsChain r s
ht : IsAntichain r t
⊢ s ∩ t ⊆ s

Tactic:
simp
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
hs : IsChain r s
ht : IsAntichain r t
⊢ s ∩ t ⊆ t

Tactic:
simp
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
hs : IsAntichain r s
ht : IsChain r t
⊢ (s ∩ t).Subsingleton

Tactic:
inter_comm _ _ ▸ inter_subsingleton_of_isChain_of_isAntichain ht hs

Premises used: Eq.rec, Set.inter_comm, inter_subsingleton_of_isChain_of_isAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s : Set α
a b : α
inst : Preorder α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
ha : a ∈ s
hb : b ∈ s
⊢ ¬a < b

Tactic:
fun h => hs ha hb h.ne h.le

Premises used: LT.lt.le, Not, LT.lt.ne
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
a : α
inst : Preorder α
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) {a} ∧ IsLeast {a} a

Tactic:
⟨IsAntichain.singleton, isLeast_singleton⟩

Premises used: IsAntichain.singleton, And.intro, isLeast_singleton
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
a : α
inst : Preorder α
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) {a} ∧ IsLeast {a} a

Tactic:
exact ⟨IsAntichain.singleton, isLeast_singleton⟩
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
a : α
inst : Preorder α
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) {a} ∧ IsGreatest {a} a

Tactic:
⟨IsAntichain.singleton, isGreatest_singleton⟩

Premises used: IsAntichain.singleton, And.intro, isGreatest_singleton
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
a : α
inst : Preorder α
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) {a} ∧ IsGreatest {a} a

Tactic:
exact ⟨IsAntichain.singleton, isGreatest_singleton⟩
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s : Set α
a : α
inst : Preorder α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ IsLeast s a ↔ s = {a}

Tactic:
(and_iff_right hs).symm.trans isAntichain_and_least_iff

Premises used: isAntichain_and_least_iff, and_iff_right, Iff.trans, Iff.symm
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s : Set α
a : α
inst : Preorder α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ IsGreatest s a ↔ s = {a}

Tactic:
(and_iff_right hs).symm.trans isAntichain_and_greatest_iff

Premises used: and_iff_right, isAntichain_and_greatest_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s : Set α
a : α
inst : Preorder α
hs : IsLeast s a
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s ↔ s = {a}

Tactic:
(and_iff_left hs).symm.trans isAntichain_and_least_iff

Premises used: isAntichain_and_least_iff, and_iff_left, Iff.trans, Iff.symm
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s : Set α
a : α
inst : Preorder α
hs : IsGreatest s a
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s ↔ s = {a}

Tactic:
(and_iff_left hs).symm.trans isAntichain_and_greatest_iff

Premises used: and_iff_left, isAntichain_and_greatest_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s : Set α
inst : Preorder α
inst_1 : OrderBot α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ ⊥ ∈ s ↔ s = {⊥}

Tactic:
isLeast_bot_iff.symm.trans hs.least_iff

Premises used: Iff.trans, isLeast_bot_iff, IsAntichain.least_iff, Iff.symm
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s : Set α
inst : Preorder α
inst_1 : OrderTop α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ ⊤ ∈ s ↔ s = {⊤}

Tactic:
isGreatest_top_iff.symm.trans hs.greatest_iff

Premises used: isGreatest_top_iff, IsAntichain.greatest_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s : Set α
a : α
inst : Preorder α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Minimal (fun (x : α) ↦ x ∈ s) a ↔ a ∈ s

Tactic:
⟨fun h ↦ h.prop, fun h ↦ ⟨h, fun _ hys hyx ↦ (hs.eq hys h hyx).symm.le⟩⟩

Premises used: Minimal.prop, Eq.le, And.intro, Iff.intro, IsAntichain.eq, Eq.symm
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s : Set α
a : α
inst : Preorder α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Maximal (fun (x : α) ↦ x ∈ s) a ↔ a ∈ s

Tactic:
hs.to_dual.minimal_mem_iff

Premises used: Set.Mem, IsAntichain.minimal_mem_iff, IsAntichain.to_dual, Maximal, OrderDual
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s t : Set α
inst : Preorder α
ht : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun (x : α) ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun (x : α) ↦ x ∈ s) b
⊢ {x : α | Maximal (fun (x : α) ↦ x ∈ s) x} = t

Tactic:
Set.ext fun x ↦ ⟨h _, fun hx ↦ ?_⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s t : Set α
inst : Preorder α
ht : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun (x : α) ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun (x : α) ↦ x ∈ s) b
refine : ∀ (x : α) (hx : x ∈ t), Membership.mem (γ := Set α) {x : α | Maximal (fun (x : α) ↦ x ∈ s) x} x
⊢ {x : α | Maximal (fun (x : α) ↦ x ∈ s) x} = t

Tactic:
refine Set.ext fun x ↦ ⟨h _, fun hx ↦ ?_⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s t : Set α
inst : Preorder α
ht : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun (x : α) ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun (x : α) ↦ x ∈ s) b
x : α
hx : x ∈ t
obtain :
  ∀ (y : α) (hyx : y ≤ x) (hy : Maximal (fun (x : α) ↦ x ∈ s) y),
    Membership.mem (γ := Set α) {x : α | Maximal (fun (x : α) ↦ x ∈ s) x} x
⊢ Membership.mem (γ := Set α) {x : α | Maximal (fun (x : α) ↦ x ∈ s) x} x

Tactic:
obtain ⟨y, hyx, hy⟩ := hs x hx
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s t : Set α
inst : Preorder α
ht : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun (x : α) ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun (x : α) ↦ x ∈ s) b
x : α
hx : x ∈ t
y : α
hyx : y ≤ x
hy : Maximal (fun (x : α) ↦ x ∈ s) y
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Set α) {x : α | Maximal (fun (x : α) ↦ x ∈ s) x} y
⊢ Membership.mem (γ := Set α) {x : α | Maximal (fun (x : α) ↦ x ∈ s) x} x

Tactic:
rwa [← ht.eq (h y hy) hx hyx]

Premises used: IsAntichain.eq
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s t : Set α
inst : Preorder α
ht : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
h : ∀ (x : α), Minimal (fun (x : α) ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ (b : α), a ≤ b ∧ Minimal (fun (x : α) ↦ x ∈ s) b
⊢ {x : α | Minimal (fun (x : α) ↦ x ∈ s) x} = t

Tactic:
ht.to_dual.eq_setOf_maximal h hs

Premises used: Set.Mem, setOf, IsAntichain.to_dual, OrderDual, Minimal, IsAntichain.eq_setOf_maximal
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
s : Set α
hf : StrictMonoOn f s
hf' : AntitoneOn f s
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
fun _a ha _b hb hab' hab ↦ (hf ha hb <| hab.lt_of_ne hab').not_ge (hf' ha hb hab)

Premises used: Set.Pairwise, LE.le.lt_of_ne, IsAntichain, LT.lt.not_ge, Not
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : StrictAntiOn f s
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
fun _a ha _b hb hab' hab ↦ (hf ha hb hab).not_gt (hf' ha hb <| hab.lt_of_ne hab')

Premises used: Set.Pairwise, LE.le.lt_of_ne, LE.le.not_gt, IsAntichain, Not
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ¬a < b

Tactic:
⟨fun hs _ ha _ => hs.not_lt ha, fun hs _ ha _ hb h h' => hs ha hb <| h'.lt_of_ne h⟩

Premises used: LE.le.lt_of_ne, Iff.intro, IsAntichain.not_lt
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
inst : PartialOrder α
P : α → Prop
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) {x : α | Maximal P x}

Tactic:
fun _ hx _ ⟨hy, _⟩ hne hle ↦ hne (hle.antisymm <| hx.2 hy hle)

Premises used: False, LE.le.antisymm, _private.0.setOf_maximal_antichain.match_1, Set.Pairwise, And.right, IsAntichain, Not
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
inst : PartialOrder α
P : α → Prop
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) {x : α | Minimal P x}

Tactic:
(setOf_maximal_antichain (α := αᵒᵈ) P).swap

Premises used: setOf, IsAntichain.swap, OrderDual, Minimal, setOf_maximal_antichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
hs : IsStrongAntichain r s
h : t ⊆ s
⊢ IsStrongAntichain r t

Tactic:
hs.mono h

Premises used: Set.Pairwise.mono, IsStrongAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r₁ r₂ : α → α → Prop
s : Set α
hs : IsStrongAntichain r₁ s
h : r₂ ≤ r₁
⊢ IsStrongAntichain r₂ s

Tactic:
hs.mono' fun _ _ hab c => (hab c).imp (compl_le_compl h _ _) (compl_le_compl h _ _)

Premises used: Set.Pairwise.mono', IsStrongAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsStrongAntichain r s
a b c : α
ha : a ∈ s
hb : b ∈ s
hac : r a c
hbc : r b c
⊢ a = b

Tactic:
(Set.Pairwise.eq hs ha hb) fun h =>
    False.elim <| (h c).elim (not_not_intro hac) (not_not_intro hbc)

Premises used: False.elim, not_not_intro, Set.Pairwise.eq, Or.elim
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Refl r
h : IsStrongAntichain r s
⊢ IsAntichain r s

Tactic:
h.imp fun _ b hab => (hab b).resolve_right (not_not_intro <| refl _)

Premises used: not_not_intro, IsAntichain, Set.Pairwise.imp, Or.resolve_right, refl
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : IsDirected α r
h : IsStrongAntichain r s
⊢ s.Subsingleton

Tactic:
fun a ha b hb =>
  let ⟨_, hac, hbc⟩ := directed_of r a b
  h.eq ha hb hac hbc

Premises used: _private.0.IsStrongAntichain.subsingleton.match_1, Set.Subsingleton, directed_of, Eq, IsStrongAntichain.eq
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Symm r
hs : IsStrongAntichain r s
⊢ IsStrongAntichain (flip r) s

Tactic:
fun _ ha _ hb h c => (hs ha hb h c).imp (mt <| symm_of r) (mt <| symm_of r)

Premises used: mt, Set.Pairwise, symm_of, Or.imp, IsStrongAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Symm r
hs : IsStrongAntichain r s
⊢ IsStrongAntichain (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) s

Tactic:
hs.flip

Premises used: IsStrongAntichain.flip
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : β
obtain : ∀ (c : α), ¬r' (f a) (f c) ∨ ¬r' (f b) (f c)
⊢ ¬r' (f a) c ∨ ¬r' (f b) c

Tactic:
obtain ⟨c, rfl⟩ := hf c

Premises used: rfl
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : α
⊢ ¬r' (f a) (f c) ∨ ¬r' (f b) (f c)

Tactic:
(hs ha hb (ne_of_apply_ne _ hab) _).imp (mt <| h _ _) (mt <| h _ _)

Premises used: mt, ne_of_apply_ne, Or.imp
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : α
⊢ ¬r' (f a) (f c) ∨ ¬r' (f b) (f c)

Tactic:
exact (hs ha hb (ne_of_apply_ne _ hab) _).imp (mt <| h _ _) (mt <| h _ _)

Premises used: mt, ne_of_apply_ne, Or.imp
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : β → α
hf : Injective f
h : ∀ (a b : β), r' a b → r (f a) (f b)
⊢ IsStrongAntichain r' (f ⁻¹' s)

Tactic:
fun _ ha _ hb hab _ =>
  (hs ha hb (hf.ne hab) _).imp (mt <| h _ _) (mt <| h _ _)

Premises used: Function.Injective.ne, mt, Set.Pairwise, Or.imp, IsStrongAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
⊢ IsStrongAntichain r (insert a s) ↔ IsStrongAntichain r s ∧ ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ∀ (c : α), ¬r a c ∨ ¬r b c

Tactic:
Set.pairwise_insert_of_symmetric fun _ _ h c => (h c).symm

Premises used: Or.symm, Set.pairwise_insert_of_symmetric, IsStrongAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
hs : IsStrongAntichain r s
h : ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ∀ (c : α), ¬r a c ∨ ¬r b c
⊢ IsStrongAntichain r (insert a s)

Tactic:
isStrongAntichain_insert.2 ⟨hs, h⟩

Premises used: Iff.mpr, isStrongAntichain_insert, And.intro
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s : Set α
hs : s.Subsingleton
r : α → α → Prop
⊢ IsStrongAntichain r s

Tactic:
hs.pairwise _

Premises used: Set.Subsingleton.pairwise, IsStrongAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
⊢ IsAntichain r s

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxAntichain r c
t : Set β
ht : IsAntichain s t
hf : (⇑e : (a : α) → β) '' c ⊆ t
rw : c = (⇑e.toEquiv (r := r) (s := s).symm : (a : β) → α) '' t
⊢ (⇑e : (a : α) → β) '' c = t

Tactic:
rw [← e.coe_fn_toEquiv, ← e.toEquiv.eq_preimage_iff_image_eq, ← Equiv.image_symm_eq_preimage]

Premises used: Equiv.eq_preimage_iff_image_eq, RelIso.toEquiv, RelIso.coe_fn_toEquiv, Equiv.image_symm_eq_preimage
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxAntichain r c
t : Set β
ht : IsAntichain s t
hf : (⇑e : (a : α) → β) '' c ⊆ t
⊢ c = (⇑e.toEquiv (r := r) (s := s).symm : (a : β) → α) '' t

Tactic:
hc.2 (ht.image _ fun _ _ ↦ e.symm.map_rel_iff.mp)
      ((e.toEquiv.subset_symm_image _ _).2 hf)

Premises used: Iff.mpr, IsAntichain.image, RelIso.symm, And.right, RelIso.map_rel_iff, Iff.mp, Equiv.subset_symm_image, RelIso.toEquiv
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxAntichain r c
t : Set β
ht : IsAntichain s t
hf : (⇑e : (a : α) → β) '' c ⊆ t
⊢ c = (⇑e.toEquiv (r := r) (s := s).symm : (a : β) → α) '' t

Tactic:
exact hc.2 (ht.image _ fun _ _ ↦ e.symm.map_rel_iff.mp)
      ((e.toEquiv.subset_symm_image _ _).2 hf)

Premises used: Iff.mpr, IsAntichain.image, RelIso.symm, And.right, RelIso.map_rel_iff, Iff.mp, Equiv.subset_symm_image, RelIso.toEquiv
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
⊢ IsEmpty α ↔ s = ∅

Tactic:
⟨fun _ ↦ s.eq_empty_of_isEmpty, fun h' ↦ ?_⟩

Premises used: Iff.intro, Set.eq_empty_of_isEmpty
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
refine : ∀ (h' : s = ∅), IsEmpty α
⊢ IsEmpty α ↔ s = ∅

Tactic:
refine ⟨fun _ ↦ s.eq_empty_of_isEmpty, fun h' ↦ ?_⟩
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
h' : s = ∅
false : ∀ (a : α), False
⊢ IsEmpty α

Tactic:
constructor
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
h' : s = ∅
x : α
⊢ ∀ ⦃t : Set α⦄, IsAntichain r t → ∅ = t

Tactic:
simp only [IsMaxAntichain, h', IsAntichain.empty, empty_subset, forall_const, true_and] at h

Premises used: IsMaxAntichain, Set.empty_subset, forall_const, IsAntichain.empty, true_and
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h' : s = ∅
x : α
h : ∀ ⦃t : Set α⦄, IsAntichain r t → ∅ = t
⊢ False

Tactic:
singleton_ne_empty x (h IsAntichain.singleton).symm

Premises used: IsAntichain.singleton, Eq.symm, Set.singleton_ne_empty
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h' : s = ∅
x : α
h : ∀ ⦃t : Set α⦄, IsAntichain r t → ∅ = t
⊢ False

Tactic:
exact singleton_ne_empty x (h IsAntichain.singleton).symm

Premises used: IsAntichain.singleton, Eq.symm, Set.singleton_ne_empty
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
⊢ ¬Nonempty α ↔ ¬s.Nonempty

Tactic:
simpa [Set.not_nonempty_iff_eq_empty] using h.isEmpty_iff

Premises used: Set.not_nonempty_iff_eq_empty, IsMaxAntichain.isEmpty_iff
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
⊢ IsMaxAntichain (flip r) s

Tactic:
⟨h.isAntichain.flip, fun _ ht₁ ht₂ ↦ h.2 ht₁.flip ht₂⟩

Premises used: IsMaxAntichain, IsAntichain.flip, And.right, And.intro, IsMaxAntichain.isAntichain
-- Module: Mathlib.Order.Antichain
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
s t : Set ((i : ι) → α i)
hs : IsWeakAntichain (α := α) s
⊢ t ⊆ s → IsWeakAntichain (α := α) t

Tactic:
IsAntichain.subset hs

Premises used: IsWeakAntichain, IsAntichain.subset
-- Module: Mathlib.Order.Antichain
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
s : Set ((i : ι) → α i)
a b : (i : ι) → α i
hs : IsWeakAntichain (α := α) s
⊢ a ∈ s → b ∈ s → StrongLT (π := α) a b → a = b

Tactic:
IsAntichain.eq hs

Premises used: IsAntichain.eq
-- Module: Mathlib.Order.Antichain
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
s : Set ((i : ι) → α i)
a : (i : ι) → α i
hs : IsWeakAntichain (α := α) s
⊢ (∀ ⦃b : (i : ι) → α i⦄, b ∈ s → a ≠ b → ¬StrongLT (π := α) b a) →
    (∀ ⦃b : (i : ι) → α i⦄, b ∈ s → a ≠ b → ¬StrongLT (π := α) a b) → IsWeakAntichain (α := α) (insert a s)

Tactic:
IsAntichain.insert hs

Premises used: IsAntichain.insert, IsWeakAntichain
-- Module: Mathlib.Order.Antichain
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
s : Set ((i : ι) → α i)
a : (i : ι) → α i
⊢ IsWeakAntichain (α := α) (insert a s) ↔
    IsWeakAntichain (α := α) s ∧ ∀ ⦃b : (i : ι) → α i⦄, b ∈ s → a ≠ b → ¬StrongLT (π := α) a b ∧ ¬StrongLT (π := α) b a

Tactic:
isAntichain_insert

Premises used: IsWeakAntichain, isAntichain_insert
-- Module: Mathlib.Order.Antichain
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
s : Set ((i : ι) → α i)
hs : IsAntichain (fun (x1 x2 : (i : ι) → α i) ↦ x1 ≤ x2) s
⊢ IsWeakAntichain (α := α) s

Tactic:
hs.mono fun _ _ => le_of_strongLT

Premises used: IsWeakAntichain, IsAntichain.mono, le_of_strongLT
-- Module: Mathlib.Order.Antichain
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
s : Set ((i : ι) → α i)
hs : s.Subsingleton
⊢ IsWeakAntichain (α := α) s

Tactic:
hs.isAntichain _

Premises used: Set.Subsingleton.isAntichain, IsWeakAntichain
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
r : α → α → Prop
⊢ AntisymmRel (swap (φ := fun (a a_1 : α) ↦ Prop) r) = AntisymmRel r

Tactic:
funext₂ fun _ _ ↦ propext and_comm

Premises used: and_comm, funext₂, propext
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
r : α → α → Prop
⊢ AntisymmRel (swap (φ := fun (a a_1 : α) ↦ Prop) r) a b ↔ AntisymmRel r a b

Tactic:
and_comm

Premises used: and_comm, AntisymmRel
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
a : α
⊢ AntisymmRel r a a

Tactic:
⟨_root_.refl _, _root_.refl _⟩

Premises used: And.intro, AntisymmRel, refl
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
a : α
⊢ AntisymmRel r a a

Tactic:
.refl ..

Premises used: AntisymmRel.refl
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
a b : α
h : a = b
⊢ AntisymmRel r a b

Tactic:
h ▸ .rfl

Premises used: AntisymmRel.rfl, Eq.rec
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
r : α → α → Prop
⊢ AntisymmRel r a b → AntisymmRel r b a

Tactic:
And.symm

Premises used: AntisymmRel, And.symm
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
r : α → α → Prop
⊢ AntisymmRel r a b ↔ AntisymmRel r b a

Tactic:
And.comm

Premises used: And.comm, AntisymmRel
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
r : α → α → Prop
inst : IsTrans α r
hab : AntisymmRel r a b
hbc : AntisymmRel r b c
⊢ AntisymmRel r a c

Tactic:
⟨_root_.trans hab.1 hbc.1, _root_.trans hbc.2 hab.2⟩

Premises used: trans, And.right, And.left, And.intro, AntisymmRel
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
r : α → α → Prop
inst : Std.Refl r
inst_1 : Std.Antisymm r
⊢ AntisymmRel r a b ↔ a = b

Tactic:
antisymm_iff

Premises used: antisymm_iff, AntisymmRel
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_3
a b : α
r : α → α → Prop
h : AntisymmRel r a b
⊢ r a b

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_3
a b : α
r : α → α → Prop
h : AntisymmRel r a b
⊢ r b a

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
inst : LE α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ≤ b

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
inst : LE α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ b ≤ a

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
β : Type u_2
a b c d : α
r : α → α → Prop
inst : IsPreorder α r
inst_1 : Subsingleton α
⊢ Subsingleton.{u_1 + 1} (Antisymmetrization α r)

Tactic:
inferInstanceAs <| Subsingleton (Quotient _)

Premises used: _private.0.instSubsingletonAntisymmetrization._proof_1
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
p : Antisymmetrization α r → Prop
⊢ (∀ (a : α), p (toAntisymmetrization r a)) → ∀ (q : Antisymmetrization α r), p q

Tactic:
Quot.ind

Premises used: Quot.ind, Antisymmetrization, Quotient, toAntisymmetrization
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
p : Antisymmetrization α r → Prop
a : Antisymmetrization α r
h : ∀ (a : α), p (toAntisymmetrization r a)
⊢ p a

Tactic:
Quotient.inductionOn' a h

Premises used: Quotient.inductionOn'
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
r : α → α → Prop
inst : IsPreorder α r
a : Antisymmetrization α r
⊢ toAntisymmetrization r (ofAntisymmetrization r a) = a

Tactic:
Quotient.out_eq' _

Premises used: Quotient.out_eq', ofAntisymmetrization, Antisymmetrization, toAntisymmetrization
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
inst : Preorder α
rw : a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
⊢ a ≤ b ↔ a < b ∨ AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
rw [lt_iff_le_not_ge, AntisymmRel]

Premises used: lt_iff_le_not_ge, AntisymmRel
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
mpr : a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a → a ≤ b
mp₁ mp₂ : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
mp₃ : a ≤ b → ¬(a ≤ b ∧ ¬b ≤ a) → a ≤ b
mp₄ : a ≤ b → ¬(a ≤ b ∧ ¬b ≤ a) → b ≤ a
mpr₁ : a ≤ b → ¬b ≤ a → a ≤ b
mpr₂ : a ≤ b → b ≤ a → a ≤ b
mpr₃ : a ≤ b → ¬b ≤ a → a ≤ b
mpr₄ : a ≤ b → b ≤ a → a ≤ b
mpr₅ : a ≤ b → ¬b ≤ a → a ≤ b
mpr₆ : a ≤ b → b ≤ a → a ≤ b
mp₅ : a ≤ b → ¬a ≤ b → b ≤ a
mp₆ mp₇ mp₈ : a ≤ b → ¬¬b ≤ a → b ≤ a
mp₉ mp₁₀ mp₁₁ : a ≤ b → b ≤ a → b ≤ a
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a

Tactic:
tauto
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₁ : a ≤ b
h₂ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ a ≤ c

Tactic:
h₁.trans h₂.le

Premises used: AntisymmRel.le, LE.le.trans
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₁ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
h₂ : b ≤ c
⊢ a ≤ c

Tactic:
h₁.le.trans h₂

Premises used: AntisymmRel.le, LE.le.trans
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₁ : a < b
h₂ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ a < c

Tactic:
h₁.trans_le h₂.le

Premises used: AntisymmRel.le, LT.lt.trans_le
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₁ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
h₂ : b < c
⊢ a < c

Tactic:
h₁.le.trans_lt h₂

Premises used: AntisymmRel.le, LE.le.trans_lt